# HG changeset patch # User wenzelm # Date 1272556211 -7200 # Node ID 2584289edbb078f29be113dd7ee46048c27258ed # Parent 3909002beca5afb8b2fb6dffe1052f43739c6fc4# Parent 03d2a2d0ee4a25f463518ce0c74357f846cc5672 merged diff -r 3909002beca5 -r 2584289edbb0 NEWS --- a/NEWS Thu Apr 29 09:06:35 2010 +0200 +++ b/NEWS Thu Apr 29 17:50:11 2010 +0200 @@ -64,6 +64,11 @@ * Type constructors admit general mixfix syntax, not just infix. +* Concrete syntax may be attached to local entities without a proof +body, too. This works via regular mixfix annotations for 'fix', +'def', 'obtain' etc. or via the explicit 'write' command, which is +similar to the 'notation' command in theory specifications. + * Use of cumulative prems via "!" in some proof methods has been discontinued (legacy feature). @@ -7004,3 +7009,5 @@ types; :mode=text:wrap=hard:maxLineLen=72: + + LocalWords: def diff -r 3909002beca5 -r 2584289edbb0 doc-src/IsarRef/Thy/Inner_Syntax.thy --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Apr 29 09:06:35 2010 +0200 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Apr 29 17:50:11 2010 +0200 @@ -365,6 +365,7 @@ @{command_def "no_type_notation"} & : & @{text "local_theory \ local_theory"} \\ @{command_def "notation"} & : & @{text "local_theory \ local_theory"} \\ @{command_def "no_notation"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "write"} & : & @{text "proof(state) \ proof(state)"} \\ \end{matharray} \begin{rail} @@ -372,6 +373,8 @@ ; ('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and') ; + 'write' mode? (nameref structmixfix + 'and') + ; \end{rail} \begin{description} @@ -392,12 +395,14 @@ but removes the specified syntax annotation from the present context. + \item @{command "write"} is similar to @{command "notation"}, but + works within an Isar proof body. + \end{description} - Compared to the underlying @{command "syntax"} and @{command - "no_syntax"} primitives (\secref{sec:syn-trans}), the above commands - provide explicit checking wrt.\ the logical context, and work within - general local theory targets, not just the global theory. + Note that the more primitive commands @{command "syntax"} and + @{command "no_syntax"} (\secref{sec:syn-trans}) provide raw access + to the syntax tables of a global theory. *} diff -r 3909002beca5 -r 2584289edbb0 doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Thu Apr 29 09:06:35 2010 +0200 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Thu Apr 29 17:50:11 2010 +0200 @@ -388,6 +388,7 @@ \indexdef{}{command}{no\_type\_notation}\hypertarget{command.no-type-notation}{\hyperlink{command.no-type-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}type{\isacharunderscore}notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ \indexdef{}{command}{notation}\hypertarget{command.notation}{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ \indexdef{}{command}{no\_notation}\hypertarget{command.no-notation}{\hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ + \indexdef{}{command}{write}\hypertarget{command.write}{\hyperlink{command.write}{\mbox{\isa{\isacommand{write}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}} \\ \end{matharray} \begin{rail} @@ -395,6 +396,8 @@ ; ('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and') ; + 'write' mode? (nameref structmixfix + 'and') + ; \end{rail} \begin{description} @@ -414,11 +417,14 @@ but removes the specified syntax annotation from the present context. + \item \hyperlink{command.write}{\mbox{\isa{\isacommand{write}}}} is similar to \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}, but + works within an Isar proof body. + \end{description} - Compared to the underlying \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} and \hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}} primitives (\secref{sec:syn-trans}), the above commands - provide explicit checking wrt.\ the logical context, and work within - general local theory targets, not just the global theory.% + Note that the more primitive commands \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} and + \hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}} (\secref{sec:syn-trans}) provide raw access + to the syntax tables of a global theory.% \end{isamarkuptext}% \isamarkuptrue% % diff -r 3909002beca5 -r 2584289edbb0 etc/isar-keywords-ZF.el --- a/etc/isar-keywords-ZF.el Thu Apr 29 09:06:35 2010 +0200 +++ b/etc/isar-keywords-ZF.el Thu Apr 29 17:50:11 2010 +0200 @@ -210,6 +210,7 @@ "using" "welcome" "with" + "write" "{" "}")) @@ -486,7 +487,8 @@ "txt" "txt_raw" "unfolding" - "using")) + "using" + "write")) (defconst isar-keywords-proof-asm '("assume" diff -r 3909002beca5 -r 2584289edbb0 etc/isar-keywords.el --- a/etc/isar-keywords.el Thu Apr 29 09:06:35 2010 +0200 +++ b/etc/isar-keywords.el Thu Apr 29 17:50:11 2010 +0200 @@ -273,6 +273,7 @@ "values" "welcome" "with" + "write" "{" "}")) @@ -628,7 +629,8 @@ "txt" "txt_raw" "unfolding" - "using")) + "using" + "write")) (defconst isar-keywords-proof-asm '("assume" diff -r 3909002beca5 -r 2584289edbb0 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Thu Apr 29 09:06:35 2010 +0200 +++ b/src/HOL/Statespace/state_space.ML Thu Apr 29 17:50:11 2010 +0200 @@ -198,7 +198,7 @@ if Variable.is_fixed ctxt name orelse Variable.is_declared ctxt name then let val n' = lookupI (op =) (Variable.fixes_of ctxt) name - in SOME (Free (n',ProofContext.infer_type ctxt n')) end + in SOME (Free (n',ProofContext.infer_type ctxt (n', dummyT))) end else NONE @@ -430,7 +430,7 @@ let fun upd (n,v) = let - val nT = ProofContext.infer_type (Local_Theory.target_of lthy) n + val nT = ProofContext.infer_type (Local_Theory.target_of lthy) (n, dummyT) in Context.proof_map (update_declinfo (Morphism.term phi (Free (n,nT)),v)) end; diff -r 3909002beca5 -r 2584289edbb0 src/HOL/TLA/Memory/MemoryParameters.thy --- a/src/HOL/TLA/Memory/MemoryParameters.thy Thu Apr 29 09:06:35 2010 +0200 +++ b/src/HOL/TLA/Memory/MemoryParameters.thy Thu Apr 29 17:50:11 2010 +0200 @@ -12,7 +12,7 @@ begin (* the memory operations *) -datatype memOp = read Locs | write Locs Vals +datatype memOp = read Locs | "write" Locs Vals consts (* memory locations and contents *) diff -r 3909002beca5 -r 2584289edbb0 src/HOL/Unix/Unix.thy --- a/src/HOL/Unix/Unix.thy Thu Apr 29 09:06:35 2010 +0200 +++ b/src/HOL/Unix/Unix.thy Thu Apr 29 17:50:11 2010 +0200 @@ -358,7 +358,7 @@ read: "access root path uid {Readable} = Some (Val (att, text)) \ root \(Read uid text path)\ root" | - write: + "write": "access root path uid {Writable} = Some (Val (att, text')) \ root \(Write uid text path)\ update path (Some (Val (att, text))) root" | @@ -436,7 +436,7 @@ case read with root' show ?thesis by cases auto next - case write + case "write" with root' show ?thesis by cases auto next case chmod diff -r 3909002beca5 -r 2584289edbb0 src/Pure/Isar/args.ML --- a/src/Pure/Isar/args.ML Thu Apr 29 09:06:35 2010 +0200 +++ b/src/Pure/Isar/args.ML Thu Apr 29 17:50:11 2010 +0200 @@ -205,7 +205,7 @@ >> (fn Type (c, _) => c | TFree (a, _) => a | _ => ""); fun const strict = - Scan.peek (fn ctxt => named_term (ProofContext.read_const (Context.proof_of ctxt) strict)) + Scan.peek (fn ctxt => named_term (ProofContext.read_const (Context.proof_of ctxt) strict dummyT)) >> (fn Const (c, _) => c | Free (x, _) => x | _ => ""); fun const_proper strict = diff -r 3909002beca5 -r 2584289edbb0 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Thu Apr 29 09:06:35 2010 +0200 +++ b/src/Pure/Isar/isar_syn.ML Thu Apr 29 17:50:11 2010 +0200 @@ -225,22 +225,22 @@ >> (fn (mode, args) => Specification.abbreviation_cmd mode args)); val _ = - OuterSyntax.local_theory "type_notation" "add notation for type constructors" K.thy_decl + OuterSyntax.local_theory "type_notation" "add concrete syntax for type constructors" K.thy_decl (opt_mode -- P.and_list1 (P.xname -- P.mixfix) >> (fn (mode, args) => Specification.type_notation_cmd true mode args)); val _ = - OuterSyntax.local_theory "no_type_notation" "delete notation for type constructors" K.thy_decl + OuterSyntax.local_theory "no_type_notation" "delete concrete syntax for type constructors" K.thy_decl (opt_mode -- P.and_list1 (P.xname -- P.mixfix) >> (fn (mode, args) => Specification.type_notation_cmd false mode args)); val _ = - OuterSyntax.local_theory "notation" "add notation for constants / fixed variables" K.thy_decl + OuterSyntax.local_theory "notation" "add concrete syntax for constants / fixed variables" K.thy_decl (opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix) >> (fn (mode, args) => Specification.notation_cmd true mode args)); val _ = - OuterSyntax.local_theory "no_notation" "delete notation for constants / fixed variables" K.thy_decl + OuterSyntax.local_theory "no_notation" "delete concrete syntax for constants / fixed variables" K.thy_decl (opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix) >> (fn (mode, args) => Specification.notation_cmd false mode args)); @@ -615,6 +615,12 @@ (P.and_list1 (P.and_list1 P.term -- (P.$$$ "=" |-- P.term)) >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind_cmd))); +val _ = + OuterSyntax.command "write" "add concrete syntax for constants / fixed variables" + (K.tag_proof K.prf_decl) + (opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix) + >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args))); + val case_spec = (P.$$$ "(" |-- P.!!! (P.xname -- Scan.repeat1 (P.maybe P.name) --| P.$$$ ")") || P.xname >> rpair []) -- SpecParse.opt_attribs >> P.triple1; diff -r 3909002beca5 -r 2584289edbb0 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Thu Apr 29 09:06:35 2010 +0200 +++ b/src/Pure/Isar/proof.ML Thu Apr 29 17:50:11 2010 +0200 @@ -43,6 +43,8 @@ val simple_goal: state -> {context: context, goal: thm} val let_bind: (term list * term) list -> state -> state val let_bind_cmd: (string list * string) list -> state -> state + val write: Syntax.mode -> (term * mixfix) list -> state -> state + val write_cmd: Syntax.mode -> (string * mixfix) list -> state -> state val fix: (binding * typ option * mixfix) list -> state -> state val fix_cmd: (binding * string option * mixfix) list -> state -> state val assm: Assumption.export -> @@ -539,6 +541,26 @@ end; +(* concrete syntax *) + +local + +fun gen_write prep_arg mode args = + assert_forward + #> map_context (fn ctxt => ctxt |> ProofContext.notation true mode (map (prep_arg ctxt) args)) + #> put_facts NONE; + +in + +val write = gen_write (K I); + +val write_cmd = + gen_write (fn ctxt => fn (c, mx) => + (ProofContext.read_const ctxt false (Syntax.mixfixT mx) c, mx)); + +end; + + (* fix *) local diff -r 3909002beca5 -r 2584289edbb0 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Apr 29 09:06:35 2010 +0200 +++ b/src/Pure/Isar/proof_context.ML Thu Apr 29 17:50:11 2010 +0200 @@ -55,13 +55,13 @@ val cert_typ_abbrev: Proof.context -> typ -> typ val get_skolem: Proof.context -> string -> string val revert_skolem: Proof.context -> string -> string - val infer_type: Proof.context -> string -> typ + val infer_type: Proof.context -> string * typ -> typ val inferred_param: string -> Proof.context -> typ * Proof.context val inferred_fixes: Proof.context -> (string * typ) list * Proof.context val read_type_name: Proof.context -> bool -> string -> typ val read_type_name_proper: Proof.context -> bool -> string -> typ val read_const_proper: Proof.context -> bool -> string -> term - val read_const: Proof.context -> bool -> string -> term + val read_const: Proof.context -> bool -> typ -> string -> term val allow_dummies: Proof.context -> Proof.context val check_tvar: Proof.context -> indexname * sort -> indexname * sort val check_tfree: Proof.context -> string * sort -> string * sort @@ -438,11 +438,10 @@ (* inferred types of parameters *) fun infer_type ctxt x = - Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt)) - (Free (x, dummyT))); + Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt)) (Free x)); fun inferred_param x ctxt = - let val T = infer_type ctxt x + let val T = infer_type ctxt (x, dummyT) in (T, ctxt |> Variable.declare_term (Free (x, T))) end; fun inferred_fixes ctxt = @@ -505,13 +504,13 @@ fun read_const_proper ctxt strict = prep_const_proper ctxt strict o token_content; -fun read_const ctxt strict text = +fun read_const ctxt strict ty text = let val (c, pos) = token_content text in (case (lookup_skolem ctxt c, Variable.is_const ctxt c) of (SOME x, false) => (Position.report (Markup.name x (if can Name.dest_skolem x then Markup.skolem else Markup.free)) pos; - Free (x, infer_type ctxt x)) + Free (x, infer_type ctxt (x, ty))) | _ => prep_const_proper ctxt strict (c, pos)) end; @@ -738,7 +737,7 @@ let val (syms, pos) = Syntax.parse_token Markup.sort text; val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (syms, pos) - handle ERROR msg => cat_error msg ("Failed to parse sort" ^ Position.str_of pos) + handle ERROR msg => cat_error msg ("Failed to parse sort" ^ Position.str_of pos) in Type.minimize_sort (tsig_of ctxt) S end; fun parse_typ ctxt text = @@ -1175,16 +1174,6 @@ (* fixes *) -local - -fun prep_mixfix (x, T, mx) = - if mx <> NoSyn andalso mx <> Structure andalso - (can Name.dest_internal x orelse can Name.dest_skolem x) then - error ("Illegal mixfix syntax for internal/skolem constant " ^ quote x) - else (Local_Syntax.Fixed, (x, T, mx)); - -in - fun add_fixes raw_vars ctxt = let val (vars, _) = cert_vars raw_vars ctxt; @@ -1192,13 +1181,11 @@ val ctxt'' = ctxt' |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars) - |-> (map_syntax o Local_Syntax.add_syntax (theory_of ctxt) o map prep_mixfix); + |-> (map_syntax o Local_Syntax.add_syntax (theory_of ctxt) o map (pair Local_Syntax.Fixed)); val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') => Context_Position.report_visible ctxt (Markup.fixed_decl x') (Binding.pos_of b)); in (xs', ctxt'') end; -end; - (* fixes vs. frees *) diff -r 3909002beca5 -r 2584289edbb0 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Thu Apr 29 09:06:35 2010 +0200 +++ b/src/Pure/Isar/specification.ML Thu Apr 29 17:50:11 2010 +0200 @@ -284,7 +284,7 @@ val type_notation_cmd = gen_type_notation (fn ctxt => ProofContext.read_type_name ctxt false); val notation = gen_notation (K I); -val notation_cmd = gen_notation (fn ctxt => ProofContext.read_const ctxt false); +val notation_cmd = gen_notation (fn ctxt => ProofContext.read_const ctxt false dummyT); end; diff -r 3909002beca5 -r 2584289edbb0 src/Pure/Syntax/syn_trans.ML --- a/src/Pure/Syntax/syn_trans.ML Thu Apr 29 09:06:35 2010 +0200 +++ b/src/Pure/Syntax/syn_trans.ML Thu Apr 29 17:50:11 2010 +0200 @@ -567,14 +567,7 @@ Term.list_comb (term_of ast, map term_of asts) | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]); - val free_fixed = Term.map_aterms - (fn t as Const (c, T) => - (case try Lexicon.unmark_fixed c of - NONE => t - | SOME x => Free (x, T)) - | t => t); - - val exn_results = map (Exn.capture (term_of #> free_fixed)) asts; + val exn_results = map (Exn.capture term_of) asts; val exns = map_filter Exn.get_exn exn_results; val results = map_filter Exn.get_result exn_results in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end; diff -r 3909002beca5 -r 2584289edbb0 src/Pure/Syntax/type_ext.ML --- a/src/Pure/Syntax/type_ext.ML Thu Apr 29 09:06:35 2010 +0200 +++ b/src/Pure/Syntax/type_ext.ML Thu Apr 29 17:50:11 2010 +0200 @@ -120,11 +120,14 @@ | decode (Abs (x, T, t)) = Abs (x, T, decode t) | decode (t $ u) = decode t $ decode u | decode (Const (a, T)) = - let val c = - (case try Lexicon.unmark_const a of - SOME c => c - | NONE => snd (map_const a)) - in Const (c, T) end + (case try Lexicon.unmark_fixed a of + SOME x => Free (x, T) + | NONE => + let val c = + (case try Lexicon.unmark_const a of + SOME c => c + | NONE => snd (map_const a)) + in Const (c, T) end) | decode (Free (a, T)) = (case (map_free a, map_const a) of (SOME x, _) => Free (x, T)