# HG changeset patch # User Lars Hupel # Date 1465659652 -7200 # Node ID 26134a00d06015c7271d842ac95b8674ca210e7e # Parent e0513d6e4916fe83a843c8bc31f2f6bc3351b183# Parent 0835067b9b3975002848b1759b0015fdff14c8a4 merged diff -r e0513d6e4916 -r 26134a00d060 NEWS --- a/NEWS Sat Jun 11 17:23:24 2016 +0200 +++ b/NEWS Sat Jun 11 17:40:52 2016 +0200 @@ -93,7 +93,7 @@ 'definition', 'inductive', 'function'. * Toplevel theorem statements support eigen-context notation with 'if' / -'for' (in postix), which corresponds to 'assumes' / 'fixes' in the +'for' (in postfix), which corresponds to 'assumes' / 'fixes' in the traditional long statement form (in prefix). Local premises are called "that" or "assms", respectively. Empty premises are *not* bound in the context: INCOMPATIBILITY. diff -r e0513d6e4916 -r 26134a00d060 lib/texinputs/isabellesym.sty --- a/lib/texinputs/isabellesym.sty Sat Jun 11 17:23:24 2016 +0200 +++ b/lib/texinputs/isabellesym.sty Sat Jun 11 17:40:52 2016 +0200 @@ -359,11 +359,11 @@ \newcommand{\isasymhungarumlaut}{\isatext{\H\relax}} \newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}} \newcommand{\isasymsome}{\isamath{\epsilon\,}} +\newcommand{\isasymhole}{\isatext{\rm\wasylozenge}} %requires wasysym \newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}} \newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}} -\newcommand{\isasymhole}{\isatext{\rm\wasylozenge}} %requires wasysym -\newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}} \newcommand{\isasymopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}} \newcommand{\isasymclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}} +\newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}} \newcommand{\isasymcomment}{\isatext{---}} \newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}} diff -r e0513d6e4916 -r 26134a00d060 src/Doc/Isar_Ref/HOL_Specific.thy --- a/src/Doc/Isar_Ref/HOL_Specific.thy Sat Jun 11 17:23:24 2016 +0200 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy Sat Jun 11 17:40:52 2016 +0200 @@ -108,7 +108,7 @@ @{rail \ (@@{command (HOL) inductive} | @@{command (HOL) inductive_set} | @@{command (HOL) coinductive} | @@{command (HOL) coinductive_set}) - @{syntax "fixes"} @{syntax "for_fixes"} \ + @{syntax vars} @{syntax for_fixes} \ (@'where' @{syntax multi_specs})? (@'monos' @{syntax thms})? ; @@{command print_inductives} ('!'?) diff -r e0513d6e4916 -r 26134a00d060 src/Doc/Isar_Ref/Outer_Syntax.thy --- a/src/Doc/Isar_Ref/Outer_Syntax.thy Sat Jun 11 17:23:24 2016 +0200 +++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Sat Jun 11 17:40:52 2016 +0200 @@ -346,7 +346,9 @@ to introduce multiple such items simultaneously. @{rail \ - @{syntax_def vars}: (@{syntax name} +) ('::' @{syntax type})? + @{syntax_def vars}: + (((@{syntax name} +) ('::' @{syntax type})? | + @{syntax name} ('::' @{syntax type})? @{syntax mixfix}) + @'and') ; @{syntax_def props}: @{syntax thmdecl}? (@{syntax prop} @{syntax prop_pat}? +) ; @@ -361,20 +363,6 @@ another level of iteration, with explicit @{keyword_ref "and"} separators; e.g.\ see @{command "fix"} and @{command "assume"} in \secref{sec:proof-context}. - - @{rail \ - @{syntax_def "fixes"}: - ((@{syntax name} ('::' @{syntax type})? @{syntax mixfix}? | @{syntax vars}) + @'and') - ; - @{syntax_def "for_fixes"}: (@'for' @{syntax "fixes"})? - \} - - The category @{syntax "fixes"} is a richer variant of @{syntax vars}: it - admits specification of mixfix syntax for the entities that are introduced - into the context. An optional suffix ``@{keyword "for"}~\fixes\'' is - admitted in many situations to indicate a so-called ``eigen-context'' of a - formal element: the result will be exported and thus generalized over the - given variables. \ @@ -463,6 +451,8 @@ @{rail \ + @{syntax_def for_fixes}: (@'for' @{syntax vars})? + ; @{syntax_def multi_specs}: (@{syntax structured_spec} + '|') ; @{syntax_def structured_spec}: @@ -470,7 +460,7 @@ ; @{syntax_def spec_prems}: (@'if' ((@{syntax prop}+) + @'and'))? ; - @{syntax_def specification}: @{syntax "fixes"} @'where' @{syntax multi_specs} + @{syntax_def specification}: @{syntax vars} @'where' @{syntax multi_specs} \} \ diff -r e0513d6e4916 -r 26134a00d060 src/Doc/Isar_Ref/Proof.thy --- a/src/Doc/Isar_Ref/Proof.thy Sat Jun 11 17:23:24 2016 +0200 +++ b/src/Doc/Isar_Ref/Proof.thy Sat Jun 11 17:40:52 2016 +0200 @@ -159,7 +159,7 @@ \[t]\. @{rail \ - @@{command fix} @{syntax "fixes"} + @@{command fix} @{syntax vars} ; (@@{command assume} | @@{command presume}) concl prems @{syntax for_fixes} ; @@ -167,8 +167,8 @@ ; prems: (@'if' (@{syntax props'} + @'and'))? ; - @@{command define} (@{syntax "fixes"} + @'and') - @'where' (@{syntax props} + @'and') @{syntax for_fixes} + @@{command define} @{syntax vars} @'where' + (@{syntax props} + @'and') @{syntax for_fixes} ; @@{command def} (def + @'and') ; @@ -417,7 +417,7 @@ ; @{syntax_def obtain_clauses}: (@{syntax par_name}? obtain_case + '|') ; - @{syntax_def obtain_case}: (@{syntax vars} + @'and') @'where' + @{syntax_def obtain_case}: @{syntax vars} @'where' (@{syntax thmdecl}? (@{syntax prop}+) + @'and') \} @@ -1335,14 +1335,14 @@ @{rail \ @@{command consider} @{syntax obtain_clauses} ; - @@{command obtain} @{syntax par_name}? (@{syntax "fixes"} + @'and') \ + @@{command obtain} @{syntax par_name}? @{syntax vars} \ @'where' concl prems @{syntax for_fixes} ; concl: (@{syntax props} + @'and') ; prems: (@'if' (@{syntax props'} + @'and'))? ; - @@{command guess} (@{syntax "fixes"} + @'and') + @@{command guess} @{syntax vars} \} \<^descr> @{command consider}~\(a) \<^vec>x \ \<^vec>A \<^vec>x | (b) diff -r e0513d6e4916 -r 26134a00d060 src/Doc/Isar_Ref/Quick_Reference.thy --- a/src/Doc/Isar_Ref/Quick_Reference.thy Sat Jun 11 17:23:24 2016 +0200 +++ b/src/Doc/Isar_Ref/Quick_Reference.thy Sat Jun 11 17:40:52 2016 +0200 @@ -13,17 +13,20 @@ text \ \begin{tabular}{rcl} \main\ & = & \<^theory_text>\notepad begin "statement\<^sup>*" end\ \\ - & \|\ & \<^theory_text>\theorem name: props "proof"\ \\ + & \|\ & \<^theory_text>\theorem name: props if props for vars "proof"\ \\ & \|\ & \<^theory_text>\theorem name:\ \\ - & & \quad\<^theory_text>\fixes "var\<^sup>+"\ \\ + & & \quad\<^theory_text>\fixes vars\ \\ & & \quad\<^theory_text>\assumes name: props\ \\ & & \quad\<^theory_text>\shows name: props "proof"\ \\ + & \|\ & \<^theory_text>\theorem name:\ \\ + & & \quad\<^theory_text>\fixes vars\ \\ + & & \quad\<^theory_text>\assumes name: props\ \\ + & & \quad\<^theory_text>\obtains (name) vars where props | \ "proof"\ \\ \proof\ & = & \<^theory_text>\"refinement\<^sup>*" proof "method\<^sup>?" "statement\<^sup>*" qed "method\<^sup>?"\ \\ & \|\ & \<^theory_text>\"refinement\<^sup>*" done\ \\ \refinement\ & = & \<^theory_text>\apply method\ \\ & \|\ & \<^theory_text>\supply facts\ \\ - & \|\ & \<^theory_text>\subgoal "proof"\ \\ - & \|\ & \<^theory_text>\subgoal for "var\<^sup>+" "proof"\ \\ + & \|\ & \<^theory_text>\subgoal premises name for vars "proof"\ \\ & \|\ & \<^theory_text>\using facts\ \\ & \|\ & \<^theory_text>\unfolding facts\ \\ \statement\ & = & \<^theory_text>\{ "statement\<^sup>*" }\ \\ @@ -31,14 +34,11 @@ & \|\ & \<^theory_text>\note name = facts\ \\ & \|\ & \<^theory_text>\let "term" = "term"\ \\ & \|\ & \<^theory_text>\write name (mixfix)\ \\ - & \|\ & \<^theory_text>\fix "var\<^sup>+"\ \\ - & \|\ & \<^theory_text>\assume name: props\ \\ - & \|\ & \<^theory_text>\assume name: props if props for "var\<^sup>+"\ \\ + & \|\ & \<^theory_text>\fix vars\ \\ + & \|\ & \<^theory_text>\assume name: props if props for vars\ \\ & \|\ & \<^theory_text>\then"\<^sup>?" goal\ \\ - \goal\ & = & \<^theory_text>\have name: props "proof"\ \\ - & \|\ & \<^theory_text>\have name: props if name: props for "var\<^sup>+" "proof"\ \\ - & \|\ & \<^theory_text>\show name: props "proof"\ \\ - & \|\ & \<^theory_text>\show name: props if name: props for "var\<^sup>+" "proof"\ \\ + \goal\ & = & \<^theory_text>\have name: props if name: props for vars "proof"\ \\ + & \|\ & \<^theory_text>\show name: props if name: props for vars "proof"\ \\ \end{tabular} \ diff -r e0513d6e4916 -r 26134a00d060 src/Doc/Isar_Ref/Spec.thy --- a/src/Doc/Isar_Ref/Spec.thy Sat Jun 11 17:23:24 2016 +0200 +++ b/src/Doc/Isar_Ref/Spec.thy Sat Jun 11 17:40:52 2016 +0200 @@ -354,7 +354,7 @@ \end{matharray} @{rail \ - @@{command axiomatization} @{syntax "fixes"}? (@'where' axiomatization)? + @@{command axiomatization} @{syntax vars}? (@'where' axiomatization)? ; axiomatization: (@{syntax thmdecl} @{syntax prop} + @'and') @{syntax spec_prems} @{syntax for_fixes} @@ -516,7 +516,7 @@ @{syntax locale_expr} ('+' (@{syntax context_elem}+))? ; @{syntax_def context_elem}: - @'fixes' @{syntax "fixes"} | + @'fixes' @{syntax vars} | @'constrains' (@{syntax name} '::' @{syntax type} + @'and') | @'assumes' (@{syntax props} + @'and') | @'defines' (@{syntax thmdecl}? @{syntax prop} @{syntax prop_pat}? + @'and') | diff -r e0513d6e4916 -r 26134a00d060 src/HOL/HOLCF/Tools/fixrec.ML --- a/src/HOL/HOLCF/Tools/fixrec.ML Sat Jun 11 17:23:24 2016 +0200 +++ b/src/HOL/HOLCF/Tools/fixrec.ML Sat Jun 11 17:40:52 2016 +0200 @@ -400,7 +400,7 @@ val _ = Outer_Syntax.local_theory @{command_keyword fixrec} "define recursive functions (HOLCF)" - (Parse.fixes -- (Parse.where_ |-- Parse.!!! multi_specs') - >> (fn (fixes, specs) => add_fixrec_cmd fixes specs)) + (Parse.vars -- (Parse.where_ |-- Parse.!!! multi_specs') + >> (fn (vars, specs) => add_fixrec_cmd vars specs)) end diff -r e0513d6e4916 -r 26134a00d060 src/HOL/Library/rewrite.ML --- a/src/HOL/Library/rewrite.ML Sat Jun 11 17:23:24 2016 +0200 +++ b/src/HOL/Library/rewrite.ML Sat Jun 11 17:40:52 2016 +0200 @@ -333,7 +333,7 @@ val sep = (Args.$$$ "at" >> K At) || (Args.$$$ "in" >> K In) val atom = (Args.$$$ "asm" >> K Asm) || (Args.$$$ "concl" >> K Concl) || - (Args.$$$ "for" |-- Args.parens (Scan.optional Parse.fixes []) >> For) || + (Args.$$$ "for" |-- Args.parens (Scan.optional Parse.vars []) >> For) || (Parse.term >> Term) val sep_atom = sep -- atom >> (fn (s,a) => [s,a]) diff -r e0513d6e4916 -r 26134a00d060 src/HOL/Nominal/nominal_primrec.ML --- a/src/HOL/Nominal/nominal_primrec.ML Sat Jun 11 17:23:24 2016 +0200 +++ b/src/HOL/Nominal/nominal_primrec.ML Sat Jun 11 17:40:52 2016 +0200 @@ -403,8 +403,8 @@ val _ = Outer_Syntax.local_theory_to_proof @{command_keyword nominal_primrec} "define primitive recursive functions on nominal datatypes" - (options -- Parse.fixes -- Parse.for_fixes -- Parse_Spec.where_multi_specs - >> (fn ((((invs, fctxt), fixes), params), specs) => - primrec_cmd invs fctxt fixes params specs)); + (options -- Parse.vars -- Parse.for_fixes -- Parse_Spec.where_multi_specs + >> (fn ((((invs, fctxt), vars), params), specs) => + primrec_cmd invs fctxt vars params specs)); end; diff -r e0513d6e4916 -r 26134a00d060 src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Sat Jun 11 17:23:24 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Sat Jun 11 17:40:52 2016 +0200 @@ -2394,13 +2394,13 @@ val _ = Outer_Syntax.local_theory @{command_keyword corec} "define nonprimitive corecursive functions" ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser) - --| @{keyword ")"}) []) -- (Parse.fixes --| Parse.where_ -- Parse.prop) + --| @{keyword ")"}) []) -- (Parse.vars --| Parse.where_ -- Parse.prop) >> uncurry corec_cmd); val _ = Outer_Syntax.local_theory_to_proof @{command_keyword corecursive} "define nonprimitive corecursive functions" ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser) - --| @{keyword ")"}) []) -- (Parse.fixes --| Parse.where_ -- Parse.prop) + --| @{keyword ")"}) []) -- (Parse.vars --| Parse.where_ -- Parse.prop) >> uncurry corecursive_cmd); val _ = Outer_Syntax.local_theory_to_proof @{command_keyword friend_of_corec} diff -r e0513d6e4916 -r 26134a00d060 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Sat Jun 11 17:23:24 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Sat Jun 11 17:40:52 2016 +0200 @@ -1615,13 +1615,13 @@ "define primitive corecursive functions" ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser) --| @{keyword ")"}) []) -- - (Parse.fixes -- where_alt_props_of_parser) >> uncurry primcorecursive_cmd); + (Parse.vars -- where_alt_props_of_parser) >> uncurry primcorecursive_cmd); val _ = Outer_Syntax.local_theory @{command_keyword primcorec} "define primitive corecursive functions" ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser) --| @{keyword ")"}) []) -- - (Parse.fixes -- where_alt_props_of_parser) >> uncurry primcorec_cmd); + (Parse.vars -- where_alt_props_of_parser) >> uncurry primcorec_cmd); val _ = Theory.setup (gfp_rec_sugar_interpretation transfer_plugin gfp_rec_sugar_transfer_interpretation); diff -r e0513d6e4916 -r 26134a00d060 src/HOL/Tools/Function/partial_function.ML --- a/src/HOL/Tools/Function/partial_function.ML Sat Jun 11 17:23:24 2016 +0200 +++ b/src/HOL/Tools/Function/partial_function.ML Sat Jun 11 17:40:52 2016 +0200 @@ -313,7 +313,7 @@ val _ = Outer_Syntax.local_theory @{command_keyword partial_function} "define partial function" - ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.simple_spec))) - >> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec)); + ((mode -- (Parse.vars -- (Parse.where_ |-- Parse_Spec.simple_spec))) + >> (fn (mode, (vars, spec)) => add_partial_function_cmd mode vars spec)); end; diff -r e0513d6e4916 -r 26134a00d060 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Sat Jun 11 17:23:24 2016 +0200 +++ b/src/HOL/Tools/inductive.ML Sat Jun 11 17:40:52 2016 +0200 @@ -1169,7 +1169,7 @@ (** outer syntax **) fun gen_ind_decl mk_def coind = - Parse.fixes -- Parse.for_fixes -- + Parse.vars -- Parse.for_fixes -- Scan.optional Parse_Spec.where_multi_specs [] -- Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.thms1) [] >> (fn (((preds, params), specs), monos) => diff -r e0513d6e4916 -r 26134a00d060 src/Pure/Isar/parse.ML --- a/src/Pure/Isar/parse.ML Sat Jun 11 17:23:24 2016 +0200 +++ b/src/Pure/Isar/parse.ML Sat Jun 11 17:40:52 2016 +0200 @@ -88,7 +88,7 @@ val const_decl: (string * string * mixfix) parser val const_binding: (binding * string * mixfix) parser val params: (binding * string option * mixfix) list parser - val fixes: (binding * string option * mixfix) list parser + val vars: (binding * string option * mixfix) list parser val for_fixes: (binding * string option * mixfix) list parser val ML_source: Input.source parser val document_source: Input.source parser @@ -374,8 +374,9 @@ >> (fn ((x, ys), T) => (x, Option.map #1 T, NoSyn) :: map (fn y => (y, Option.map #2 T, NoSyn)) ys); -val fixes = and_list1 (param_mixfix || params) >> flat; -val for_fixes = Scan.optional ($$$ "for" |-- !!! fixes) []; +val vars = and_list1 (param_mixfix || params) >> flat; + +val for_fixes = Scan.optional ($$$ "for" |-- !!! vars) []; (* embedded source text *) diff -r e0513d6e4916 -r 26134a00d060 src/Pure/Isar/parse_spec.ML --- a/src/Pure/Isar/parse_spec.ML Sat Jun 11 17:23:24 2016 +0200 +++ b/src/Pure/Isar/parse_spec.ML Sat Jun 11 17:40:52 2016 +0200 @@ -67,7 +67,7 @@ val where_multi_specs = Parse.where_ |-- Parse.!!! multi_specs; -val specification = Parse.fixes -- where_multi_specs; +val specification = Parse.vars -- where_multi_specs; (* basic constant specifications *) @@ -157,7 +157,7 @@ val obtain_case = Parse.parbinding -- - (Scan.optional (Parse.and_list1 Parse.fixes --| Parse.where_ >> flat) [] -- + (Scan.optional (Parse.and_list1 Parse.vars --| Parse.where_ >> flat) [] -- (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat)); val obtains = Parse.enum1 "|" obtain_case; diff -r e0513d6e4916 -r 26134a00d060 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Sat Jun 11 17:23:24 2016 +0200 +++ b/src/Pure/Pure.thy Sat Jun 11 17:40:52 2016 +0200 @@ -359,7 +359,7 @@ val _ = Outer_Syntax.command @{command_keyword axiomatization} "axiomatic constant specification" - (Scan.optional Parse.fixes [] -- + (Scan.optional Parse.vars [] -- Scan.optional (Parse.where_ |-- Parse.!!! axiomatization) ([], [], []) >> (fn (a, (b, c, d)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c d))); @@ -756,7 +756,7 @@ val _ = Outer_Syntax.command @{command_keyword fix} "fix local variables (Skolem constants)" - (Parse.fixes >> (Toplevel.proof o Proof.fix_cmd)); + (Parse.vars >> (Toplevel.proof o Proof.fix_cmd)); val _ = Outer_Syntax.command @{command_keyword assume} "assume propositions" @@ -768,7 +768,7 @@ val _ = Outer_Syntax.command @{command_keyword define} "local definition (non-polymorphic)" - ((Parse.fixes --| Parse.where_) -- Parse_Spec.statement -- Parse.for_fixes + ((Parse.vars --| Parse.where_) -- Parse_Spec.statement -- Parse.for_fixes >> (fn ((a, b), c) => Toplevel.proof (Proof.define_cmd a c b))); val _ = @@ -786,12 +786,12 @@ val _ = Outer_Syntax.command @{command_keyword obtain} "generalized elimination" - (Parse.parbinding -- Scan.optional (Parse.fixes --| Parse.where_) [] -- structured_statement + (Parse.parbinding -- Scan.optional (Parse.vars --| Parse.where_) [] -- structured_statement >> (fn ((a, b), (c, d, e)) => Toplevel.proof' (Obtain.obtain_cmd a b c d e))); val _ = Outer_Syntax.command @{command_keyword guess} "wild guessing (unstructured)" - (Scan.optional Parse.fixes [] >> (Toplevel.proof' o Obtain.guess_cmd)); + (Scan.optional Parse.vars [] >> (Toplevel.proof' o Obtain.guess_cmd)); val _ = Outer_Syntax.command @{command_keyword let} "bind text variables"