# HG changeset patch # User haftmann # Date 1447487152 -3600 # Node ID 20d4cd2ceab2b473f74635ec2702b92e3610f6c7 # Parent 301e0b4ecd4522409f5a5ac27288b514bd402d29 prefer "rewrites" and "defines" to note rewrite morphisms diff -r 301e0b4ecd45 -r 20d4cd2ceab2 src/Doc/Codegen/Further.thy --- a/src/Doc/Codegen/Further.thy Sat Nov 14 08:45:52 2015 +0100 +++ b/src/Doc/Codegen/Further.thy Sat Nov 14 08:45:52 2015 +0100 @@ -229,7 +229,7 @@ (*>*) permanent_interpretation %quote fun_power: power "(\n (f :: 'a \ 'a). f ^^ n)" - defining funpows = "fun_power.powers :: nat list \ ('a \ 'a) \ 'a \ 'a" + defines funpows = "fun_power.powers :: nat list \ ('a \ 'a) \ 'a \ 'a" by unfold_locales (simp_all add: fun_eq_iff funpow_mult mult.commute) (*<*) diff -r 301e0b4ecd45 -r 20d4cd2ceab2 src/Doc/Isar_Ref/Spec.thy --- a/src/Doc/Isar_Ref/Spec.thy Sat Nov 14 08:45:52 2015 +0100 +++ b/src/Doc/Isar_Ref/Spec.thy Sat Nov 14 08:45:52 2015 +0100 @@ -756,12 +756,12 @@ @@{command permanent_interpretation} @{syntax locale_expr} \ definitions? equations? ; - definitions: @'defining' (@{syntax thmdecl}? @{syntax name} \ + definitions: @'defines' (@{syntax thmdecl}? @{syntax name} \ @{syntax mixfix}? @'=' @{syntax term} + @'and'); equations: @'rewrites' (@{syntax thmdecl}? @{syntax prop} + @'and') \} - \<^descr> \<^theory_text>\permanent_interpretation expr defining "defs" rewrites eqns\ interprets + \<^descr> \<^theory_text>\permanent_interpretation expr defines "defs" rewrites eqns\ interprets \expr\ in the current local theory. The command generates proof obligations for the instantiated specifications. Instantiated declarations (in particular, facts) are added to the local theory's underlying target in a diff -r 301e0b4ecd45 -r 20d4cd2ceab2 src/Doc/isar.sty --- a/src/Doc/isar.sty Sat Nov 14 08:45:52 2015 +0100 +++ b/src/Doc/isar.sty Sat Nov 14 08:45:52 2015 +0100 @@ -18,7 +18,6 @@ \newcommand{\isasymAND}{\isakeyword{and}} \newcommand{\isasymIS}{\isakeyword{is}} \newcommand{\isasymWHERE}{\isakeyword{where}} -\newcommand{\isasymDEFINING}{\isakeyword{defining}} \newcommand{\isasymBEGIN}{\isakeyword{begin}} \newcommand{\isasymIMPORTS}{\isakeyword{imports}} \newcommand{\isasymIN}{\isakeyword{in}} diff -r 301e0b4ecd45 -r 20d4cd2ceab2 src/HOL/IMP/Abs_Int1_const.thy --- a/src/HOL/IMP/Abs_Int1_const.thy Sat Nov 14 08:45:52 2015 +0100 +++ b/src/HOL/IMP/Abs_Int1_const.thy Sat Nov 14 08:45:52 2015 +0100 @@ -68,7 +68,7 @@ permanent_interpretation Abs_Int where \ = \_const and num' = Const and plus' = plus_const -defining AI_const = AI and step_const = step' and aval'_const = aval' +defines AI_const = AI and step_const = step' and aval'_const = aval' .. diff -r 301e0b4ecd45 -r 20d4cd2ceab2 src/HOL/IMP/Abs_Int1_parity.thy --- a/src/HOL/IMP/Abs_Int1_parity.thy Sat Nov 14 08:45:52 2015 +0100 +++ b/src/HOL/IMP/Abs_Int1_parity.thy Sat Nov 14 08:45:52 2015 +0100 @@ -126,7 +126,7 @@ permanent_interpretation Abs_Int where \ = \_parity and num' = num_parity and plus' = plus_parity -defining aval_parity = aval' and step_parity = step' and AI_parity = AI +defines aval_parity = aval' and step_parity = step' and AI_parity = AI .. diff -r 301e0b4ecd45 -r 20d4cd2ceab2 src/HOL/IMP/Abs_Int2_ivl.thy --- a/src/HOL/IMP/Abs_Int2_ivl.thy Sat Nov 14 08:45:52 2015 +0100 +++ b/src/HOL/IMP/Abs_Int2_ivl.thy Sat Nov 14 08:45:52 2015 +0100 @@ -320,7 +320,7 @@ permanent_interpretation Val_lattice_gamma where \ = \_ivl and num' = num_ivl and plus' = "op +" -defining aval_ivl = aval' +defines aval_ivl = aval' proof (standard, goal_cases) case 1 show ?case by(simp add: \_inf) next @@ -354,7 +354,7 @@ where \ = \_ivl and num' = num_ivl and plus' = "op +" and test_num' = in_ivl and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl -defining inv_aval_ivl = inv_aval' +defines inv_aval_ivl = inv_aval' and inv_bval_ivl = inv_bval' and step_ivl = step' and AI_ivl = AI diff -r 301e0b4ecd45 -r 20d4cd2ceab2 src/HOL/IMP/Abs_Int3.thy --- a/src/HOL/IMP/Abs_Int3.thy Sat Nov 14 08:45:52 2015 +0100 +++ b/src/HOL/IMP/Abs_Int3.thy Sat Nov 14 08:45:52 2015 +0100 @@ -260,7 +260,7 @@ where \ = \_ivl and num' = num_ivl and plus' = "op +" and test_num' = in_ivl and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl -defining AI_wn_ivl = AI_wn +defines AI_wn_ivl = AI_wn .. diff -r 301e0b4ecd45 -r 20d4cd2ceab2 src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Sat Nov 14 08:45:52 2015 +0100 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Sat Nov 14 08:45:52 2015 +0100 @@ -62,7 +62,7 @@ qed permanent_interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)" -defining AI_const = AI +defines AI_const = AI and aval'_const = aval' proof qed (auto simp: iter'_pfp_above) diff -r 301e0b4ecd45 -r 20d4cd2ceab2 src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Sat Nov 14 08:45:52 2015 +0100 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Sat Nov 14 08:45:52 2015 +0100 @@ -202,7 +202,7 @@ permanent_interpretation Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3)" -defining afilter_ivl = afilter +defines afilter_ivl = afilter and bfilter_ivl = bfilter and AI_ivl = AI and aval_ivl = aval' diff -r 301e0b4ecd45 -r 20d4cd2ceab2 src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Sat Nov 14 08:45:52 2015 +0100 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Sat Nov 14 08:45:52 2015 +0100 @@ -194,7 +194,7 @@ permanent_interpretation Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3 2)" -defining afilter_ivl' = afilter +defines afilter_ivl' = afilter and bfilter_ivl' = bfilter and AI_ivl' = AI and aval_ivl' = aval' diff -r 301e0b4ecd45 -r 20d4cd2ceab2 src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy Sat Nov 14 08:45:52 2015 +0100 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy Sat Nov 14 08:45:52 2015 +0100 @@ -68,7 +68,7 @@ permanent_interpretation Abs_Int where \ = \_const and num' = Const and plus' = plus_const -defining AI_const = AI and step_const = step' and aval'_const = aval' +defines AI_const = AI and step_const = step' and aval'_const = aval' .. diff -r 301e0b4ecd45 -r 20d4cd2ceab2 src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy Sat Nov 14 08:45:52 2015 +0100 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy Sat Nov 14 08:45:52 2015 +0100 @@ -115,7 +115,7 @@ permanent_interpretation Abs_Int where \ = \_parity and num' = num_parity and plus' = plus_parity -defining aval_parity = aval' and step_parity = step' and AI_parity = AI +defines aval_parity = aval' and step_parity = step' and AI_parity = AI .. diff -r 301e0b4ecd45 -r 20d4cd2ceab2 src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Sat Nov 14 08:45:52 2015 +0100 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Sat Nov 14 08:45:52 2015 +0100 @@ -181,7 +181,7 @@ permanent_interpretation Val_abs1_gamma where \ = \_ivl and num' = num_ivl and plus' = plus_ivl -defining aval_ivl = aval' +defines aval_ivl = aval' proof case goal1 thus ?case by(auto simp add: \_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split) @@ -219,7 +219,7 @@ where \ = \_ivl and num' = num_ivl and plus' = plus_ivl and test_num' = in_ivl and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl -defining afilter_ivl = afilter +defines afilter_ivl = afilter and bfilter_ivl = bfilter and step_ivl = step' and AI_ivl = AI diff -r 301e0b4ecd45 -r 20d4cd2ceab2 src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy Sat Nov 14 08:45:52 2015 +0100 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy Sat Nov 14 08:45:52 2015 +0100 @@ -229,7 +229,7 @@ where \ = \_ivl and num' = num_ivl and plus' = plus_ivl and test_num' = in_ivl and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl -defining AI_ivl' = AI_wn +defines AI_ivl' = AI_wn .. diff -r 301e0b4ecd45 -r 20d4cd2ceab2 src/HOL/Library/Groups_Big_Fun.thy --- a/src/HOL/Library/Groups_Big_Fun.thy Sat Nov 14 08:45:52 2015 +0100 +++ b/src/HOL/Library/Groups_Big_Fun.thy Sat Nov 14 08:45:52 2015 +0100 @@ -225,7 +225,7 @@ "Sum_any = comm_monoid_fun.G plus 0" permanent_interpretation Sum_any: comm_monoid_fun plus 0 -where +rewrites "comm_monoid_fun.G plus 0 = Sum_any" and "comm_monoid_set.F plus 0 = setsum" proof - @@ -298,7 +298,7 @@ "Prod_any = comm_monoid_fun.G times 1" permanent_interpretation Prod_any: comm_monoid_fun times 1 -where +rewrites "comm_monoid_fun.G times 1 = Prod_any" and "comm_monoid_set.F times 1 = setprod" proof - diff -r 301e0b4ecd45 -r 20d4cd2ceab2 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Sat Nov 14 08:45:52 2015 +0100 +++ b/src/Pure/Isar/isar_syn.ML Sat Nov 14 08:45:52 2015 +0100 @@ -419,10 +419,10 @@ val _ = Outer_Syntax.local_theory_to_proof @{command_keyword permanent_interpretation} "prove interpretation of locale expression into named theory" - (Parse.!!! (Parse_Spec.locale_expression true) -- - Scan.optional (@{keyword "defining"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" + (Parse.!!! Parse_Spec.locale_expression -- + Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "="} -- Parse.term))) [] -- - Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [] + Scan.optional (@{keyword "rewrites"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [] >> (fn ((expr, defs), eqns) => Interpretation.permanent_interpretation_cmd expr defs eqns)); val _ = diff -r 301e0b4ecd45 -r 20d4cd2ceab2 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Sat Nov 14 08:45:52 2015 +0100 +++ b/src/Pure/Pure.thy Sat Nov 14 08:45:52 2015 +0100 @@ -9,7 +9,7 @@ "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\" "\" "\" "\" "\" "\" "]" "assumes" "attach" "binder" "constrains" - "defines" "defining" "fixes" "for" "identifier" "if" "in" "includes" "infix" + "defines" "rewrites" "fixes" "for" "identifier" "if" "in" "includes" "infix" "infixl" "infixr" "is" "notes" "obtains" "open" "output" "overloaded" "pervasive" "premises" "private" "qualified" "rewrites" "shows" "structure" "unchecked" "where" "when" "|"