prefer "rewrites" and "defines" to note rewrite morphisms
authorhaftmann
Sat Nov 14 08:45:52 2015 +0100 (2015-11-14)
changeset 6167120d4cd2ceab2
parent 61670 301e0b4ecd45
child 61672 87203a0f0041
prefer "rewrites" and "defines" to note rewrite morphisms
src/Doc/Codegen/Further.thy
src/Doc/Isar_Ref/Spec.thy
src/Doc/isar.sty
src/HOL/IMP/Abs_Int1_const.thy
src/HOL/IMP/Abs_Int1_parity.thy
src/HOL/IMP/Abs_Int2_ivl.thy
src/HOL/IMP/Abs_Int3.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy
src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy
src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy
src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy
src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy
src/HOL/Library/Groups_Big_Fun.thy
src/Pure/Isar/isar_syn.ML
src/Pure/Pure.thy
     1.1 --- a/src/Doc/Codegen/Further.thy	Sat Nov 14 08:45:52 2015 +0100
     1.2 +++ b/src/Doc/Codegen/Further.thy	Sat Nov 14 08:45:52 2015 +0100
     1.3 @@ -229,7 +229,7 @@
     1.4  
     1.5  (*>*)
     1.6  permanent_interpretation %quote fun_power: power "(\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)"
     1.7 -  defining funpows = "fun_power.powers :: nat list \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
     1.8 +  defines funpows = "fun_power.powers :: nat list \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
     1.9    by unfold_locales
    1.10      (simp_all add: fun_eq_iff funpow_mult mult.commute) (*<*)
    1.11  
     2.1 --- a/src/Doc/Isar_Ref/Spec.thy	Sat Nov 14 08:45:52 2015 +0100
     2.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Sat Nov 14 08:45:52 2015 +0100
     2.3 @@ -756,12 +756,12 @@
     2.4      @@{command permanent_interpretation} @{syntax locale_expr} \<newline>
     2.5        definitions? equations?
     2.6      ;
     2.7 -    definitions: @'defining' (@{syntax thmdecl}? @{syntax name} \<newline>
     2.8 +    definitions: @'defines' (@{syntax thmdecl}? @{syntax name} \<newline>
     2.9        @{syntax mixfix}? @'=' @{syntax term} + @'and');
    2.10      equations: @'rewrites' (@{syntax thmdecl}? @{syntax prop} + @'and')
    2.11    \<close>}
    2.12  
    2.13 -  \<^descr> \<^theory_text>\<open>permanent_interpretation expr defining "defs" rewrites eqns\<close> interprets
    2.14 +  \<^descr> \<^theory_text>\<open>permanent_interpretation expr defines "defs" rewrites eqns\<close> interprets
    2.15    \<open>expr\<close> in the current local theory. The command generates proof obligations
    2.16    for the instantiated specifications. Instantiated declarations (in
    2.17    particular, facts) are added to the local theory's underlying target in a
     3.1 --- a/src/Doc/isar.sty	Sat Nov 14 08:45:52 2015 +0100
     3.2 +++ b/src/Doc/isar.sty	Sat Nov 14 08:45:52 2015 +0100
     3.3 @@ -18,7 +18,6 @@
     3.4  \newcommand{\isasymAND}{\isakeyword{and}}
     3.5  \newcommand{\isasymIS}{\isakeyword{is}}
     3.6  \newcommand{\isasymWHERE}{\isakeyword{where}}
     3.7 -\newcommand{\isasymDEFINING}{\isakeyword{defining}}
     3.8  \newcommand{\isasymBEGIN}{\isakeyword{begin}}
     3.9  \newcommand{\isasymIMPORTS}{\isakeyword{imports}}
    3.10  \newcommand{\isasymIN}{\isakeyword{in}}
     4.1 --- a/src/HOL/IMP/Abs_Int1_const.thy	Sat Nov 14 08:45:52 2015 +0100
     4.2 +++ b/src/HOL/IMP/Abs_Int1_const.thy	Sat Nov 14 08:45:52 2015 +0100
     4.3 @@ -68,7 +68,7 @@
     4.4  
     4.5  permanent_interpretation Abs_Int
     4.6  where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
     4.7 -defining AI_const = AI and step_const = step' and aval'_const = aval'
     4.8 +defines AI_const = AI and step_const = step' and aval'_const = aval'
     4.9  ..
    4.10  
    4.11  
     5.1 --- a/src/HOL/IMP/Abs_Int1_parity.thy	Sat Nov 14 08:45:52 2015 +0100
     5.2 +++ b/src/HOL/IMP/Abs_Int1_parity.thy	Sat Nov 14 08:45:52 2015 +0100
     5.3 @@ -126,7 +126,7 @@
     5.4  
     5.5  permanent_interpretation Abs_Int
     5.6  where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
     5.7 -defining aval_parity = aval' and step_parity = step' and AI_parity = AI
     5.8 +defines aval_parity = aval' and step_parity = step' and AI_parity = AI
     5.9  ..
    5.10  
    5.11  
     6.1 --- a/src/HOL/IMP/Abs_Int2_ivl.thy	Sat Nov 14 08:45:52 2015 +0100
     6.2 +++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Sat Nov 14 08:45:52 2015 +0100
     6.3 @@ -320,7 +320,7 @@
     6.4  
     6.5  permanent_interpretation Val_lattice_gamma
     6.6  where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
     6.7 -defining aval_ivl = aval'
     6.8 +defines aval_ivl = aval'
     6.9  proof (standard, goal_cases)
    6.10    case 1 show ?case by(simp add: \<gamma>_inf)
    6.11  next
    6.12 @@ -354,7 +354,7 @@
    6.13  where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
    6.14  and test_num' = in_ivl
    6.15  and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
    6.16 -defining inv_aval_ivl = inv_aval'
    6.17 +defines inv_aval_ivl = inv_aval'
    6.18  and inv_bval_ivl = inv_bval'
    6.19  and step_ivl = step'
    6.20  and AI_ivl = AI
     7.1 --- a/src/HOL/IMP/Abs_Int3.thy	Sat Nov 14 08:45:52 2015 +0100
     7.2 +++ b/src/HOL/IMP/Abs_Int3.thy	Sat Nov 14 08:45:52 2015 +0100
     7.3 @@ -260,7 +260,7 @@
     7.4  where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
     7.5  and test_num' = in_ivl
     7.6  and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
     7.7 -defining AI_wn_ivl = AI_wn
     7.8 +defines AI_wn_ivl = AI_wn
     7.9  ..
    7.10  
    7.11  
     8.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy	Sat Nov 14 08:45:52 2015 +0100
     8.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy	Sat Nov 14 08:45:52 2015 +0100
     8.3 @@ -62,7 +62,7 @@
     8.4  qed
     8.5  
     8.6  permanent_interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)"
     8.7 -defining AI_const = AI
     8.8 +defines AI_const = AI
     8.9  and aval'_const = aval'
    8.10  proof qed (auto simp: iter'_pfp_above)
    8.11  
     9.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy	Sat Nov 14 08:45:52 2015 +0100
     9.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy	Sat Nov 14 08:45:52 2015 +0100
     9.3 @@ -202,7 +202,7 @@
     9.4  
     9.5  permanent_interpretation
     9.6    Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3)"
     9.7 -defining afilter_ivl = afilter
     9.8 +defines afilter_ivl = afilter
     9.9  and bfilter_ivl = bfilter
    9.10  and AI_ivl = AI
    9.11  and aval_ivl = aval'
    10.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy	Sat Nov 14 08:45:52 2015 +0100
    10.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy	Sat Nov 14 08:45:52 2015 +0100
    10.3 @@ -194,7 +194,7 @@
    10.4  
    10.5  permanent_interpretation
    10.6    Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3 2)"
    10.7 -defining afilter_ivl' = afilter
    10.8 +defines afilter_ivl' = afilter
    10.9  and bfilter_ivl' = bfilter
   10.10  and AI_ivl' = AI
   10.11  and aval_ivl' = aval'
    11.1 --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy	Sat Nov 14 08:45:52 2015 +0100
    11.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy	Sat Nov 14 08:45:52 2015 +0100
    11.3 @@ -68,7 +68,7 @@
    11.4  
    11.5  permanent_interpretation Abs_Int
    11.6  where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
    11.7 -defining AI_const = AI and step_const = step' and aval'_const = aval'
    11.8 +defines AI_const = AI and step_const = step' and aval'_const = aval'
    11.9  ..
   11.10  
   11.11  
    12.1 --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy	Sat Nov 14 08:45:52 2015 +0100
    12.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy	Sat Nov 14 08:45:52 2015 +0100
    12.3 @@ -115,7 +115,7 @@
    12.4  
    12.5  permanent_interpretation Abs_Int
    12.6  where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
    12.7 -defining aval_parity = aval' and step_parity = step' and AI_parity = AI
    12.8 +defines aval_parity = aval' and step_parity = step' and AI_parity = AI
    12.9  ..
   12.10  
   12.11  
    13.1 --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy	Sat Nov 14 08:45:52 2015 +0100
    13.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy	Sat Nov 14 08:45:52 2015 +0100
    13.3 @@ -181,7 +181,7 @@
    13.4  
    13.5  permanent_interpretation Val_abs1_gamma
    13.6  where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
    13.7 -defining aval_ivl = aval'
    13.8 +defines aval_ivl = aval'
    13.9  proof
   13.10    case goal1 thus ?case
   13.11      by(auto simp add: \<gamma>_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
   13.12 @@ -219,7 +219,7 @@
   13.13  where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
   13.14  and test_num' = in_ivl
   13.15  and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
   13.16 -defining afilter_ivl = afilter
   13.17 +defines afilter_ivl = afilter
   13.18  and bfilter_ivl = bfilter
   13.19  and step_ivl = step'
   13.20  and AI_ivl = AI
    14.1 --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy	Sat Nov 14 08:45:52 2015 +0100
    14.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy	Sat Nov 14 08:45:52 2015 +0100
    14.3 @@ -229,7 +229,7 @@
    14.4  where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
    14.5  and test_num' = in_ivl
    14.6  and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
    14.7 -defining AI_ivl' = AI_wn
    14.8 +defines AI_ivl' = AI_wn
    14.9  ..
   14.10  
   14.11  
    15.1 --- a/src/HOL/Library/Groups_Big_Fun.thy	Sat Nov 14 08:45:52 2015 +0100
    15.2 +++ b/src/HOL/Library/Groups_Big_Fun.thy	Sat Nov 14 08:45:52 2015 +0100
    15.3 @@ -225,7 +225,7 @@
    15.4    "Sum_any = comm_monoid_fun.G plus 0"
    15.5  
    15.6  permanent_interpretation Sum_any: comm_monoid_fun plus 0
    15.7 -where
    15.8 +rewrites
    15.9    "comm_monoid_fun.G plus 0 = Sum_any" and
   15.10    "comm_monoid_set.F plus 0 = setsum"
   15.11  proof -
   15.12 @@ -298,7 +298,7 @@
   15.13    "Prod_any = comm_monoid_fun.G times 1"
   15.14  
   15.15  permanent_interpretation Prod_any: comm_monoid_fun times 1
   15.16 -where
   15.17 +rewrites
   15.18    "comm_monoid_fun.G times 1 = Prod_any" and
   15.19    "comm_monoid_set.F times 1 = setprod"
   15.20  proof -
    16.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Nov 14 08:45:52 2015 +0100
    16.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Nov 14 08:45:52 2015 +0100
    16.3 @@ -419,10 +419,10 @@
    16.4  val _ =
    16.5    Outer_Syntax.local_theory_to_proof @{command_keyword permanent_interpretation}
    16.6      "prove interpretation of locale expression into named theory"
    16.7 -    (Parse.!!! (Parse_Spec.locale_expression true) --
    16.8 -      Scan.optional (@{keyword "defining"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
    16.9 +    (Parse.!!! Parse_Spec.locale_expression --
   16.10 +      Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
   16.11          -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "="} -- Parse.term))) [] --
   16.12 -      Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
   16.13 +      Scan.optional (@{keyword "rewrites"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
   16.14        >> (fn ((expr, defs), eqns) => Interpretation.permanent_interpretation_cmd expr defs eqns));
   16.15  
   16.16  val _ =
    17.1 --- a/src/Pure/Pure.thy	Sat Nov 14 08:45:52 2015 +0100
    17.2 +++ b/src/Pure/Pure.thy	Sat Nov 14 08:45:52 2015 +0100
    17.3 @@ -9,7 +9,7 @@
    17.4      "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<comment>" "\<equiv>"
    17.5      "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
    17.6      "\<subseteq>" "]" "assumes" "attach" "binder" "constrains"
    17.7 -    "defines" "defining" "fixes" "for" "identifier" "if" "in" "includes" "infix"
    17.8 +    "defines" "rewrites" "fixes" "for" "identifier" "if" "in" "includes" "infix"
    17.9      "infixl" "infixr" "is" "notes" "obtains" "open" "output"
   17.10      "overloaded" "pervasive" "premises" "private" "qualified" "rewrites"
   17.11      "shows" "structure" "unchecked" "where" "when" "|"