Keyword 'rewrites' identifies rewrite morphisms.
--- a/NEWS Wed Nov 04 08:13:49 2015 +0100
+++ b/NEWS Wed Nov 04 08:13:52 2015 +0100
@@ -271,6 +271,9 @@
regardless of the command. Previously, for 'locale' and 'sublocale'
the default was optional ('?'). INCOMPATIBILITY
+* Keyword 'rewrites' identifies rewrite morphisms in interpretation
+commands. Previously, the keyword was 'where'. INCOMPATIBILITY
+
* Command 'print_definitions' prints dependencies of definitional
specifications. This functionality used to be part of 'print_theory'.
--- a/src/Doc/Classes/Classes.thy Wed Nov 04 08:13:49 2015 +0100
+++ b/src/Doc/Classes/Classes.thy Wed Nov 04 08:13:52 2015 +0100
@@ -457,7 +457,7 @@
"replicate 0 _ = []"
| "replicate (Suc n) xs = xs @ replicate n xs"
-interpretation %quote list_monoid: monoid append "[]" where
+interpretation %quote list_monoid: monoid append "[]" rewrites
"monoid.pow_nat append [] = replicate"
proof -
interpret monoid append "[]" ..
--- a/src/Doc/Codegen/Further.thy Wed Nov 04 08:13:49 2015 +0100
+++ b/src/Doc/Codegen/Further.thy Wed Nov 04 08:13:52 2015 +0100
@@ -202,7 +202,7 @@
The interpretation itself is enriched with an equation @{text "t = c"}:
\<close>
-interpretation %quote fun_power: power "(\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)" where
+interpretation %quote fun_power: power "(\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)" rewrites
"power.powers (\<lambda>n f. f ^^ n) = funpows"
by unfold_locales
(simp_all add: fun_eq_iff funpow_mult mult.commute funpows_def)
--- a/src/Doc/Isar_Ref/Spec.thy Wed Nov 04 08:13:49 2015 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy Wed Nov 04 08:13:52 2015 +0100
@@ -676,10 +676,10 @@
@@{command print_interps} @{syntax nameref}
;
- equations: @'where' (@{syntax thmdecl}? @{syntax prop} + @'and')
+ equations: @'rewrites' (@{syntax thmdecl}? @{syntax prop} + @'and')
\<close>}
- \<^descr> @{command "interpretation"}~\<open>expr \<WHERE> eqns\<close>
+ \<^descr> @{command "interpretation"}~\<open>expr\<close>~@{keyword "rewrites"}~\<open>eqns\<close>
interprets \<open>expr\<close> in a global or local theory. The command
generates proof obligations for the instantiated specifications.
Once these are discharged by the user, instantiated declarations (in
@@ -720,14 +720,13 @@
concepts introduced through definitions. The equations must be
proved.
- \<^descr> @{command "interpret"}~\<open>expr \<WHERE> eqns\<close> interprets
+ \<^descr> @{command "interpret"}~\<open>expr\<close>~@{keyword "rewrites"}~\<open>eqns\<close> interprets
\<open>expr\<close> in the proof context and is otherwise similar to
interpretation in local theories. Note that for @{command
"interpret"} the \<open>eqns\<close> should be
explicitly universally quantified.
- \<^descr> @{command "sublocale"}~\<open>name \<subseteq> expr \<WHERE>
- eqns\<close>
+ \<^descr> @{command "sublocale"}~\<open>name \<subseteq> expr\<close>~@{keyword "rewrites"}~\<open>eqns\<close>
interprets \<open>expr\<close> in the locale \<open>name\<close>. A proof that
the specification of \<open>name\<close> implies the specification of
\<open>expr\<close> is required. As in the localized version of the
@@ -826,10 +825,10 @@
;
definitions: @'defining' (@{syntax thmdecl}? @{syntax name} \<newline>
@{syntax mixfix}? @'=' @{syntax term} + @'and');
- equations: @'where' (@{syntax thmdecl}? @{syntax prop} + @'and')
+ equations: @'rewrites' (@{syntax thmdecl}? @{syntax prop} + @'and')
\<close>}
- \<^descr> @{command "permanent_interpretation"}~\<open>expr \<DEFINING> defs \<WHERE> eqns\<close>
+ \<^descr> @{command "permanent_interpretation"}~\<open>expr \<DEFINING> defs\<close>~@{keyword "rewrites"}~\<open>eqns\<close>
interprets \<open>expr\<close> in the current local theory. The command
generates proof obligations for the instantiated specifications.
Instantiated declarations (in particular, facts) are added to the
--- a/src/Doc/Locales/Examples1.thy Wed Nov 04 08:13:49 2015 +0100
+++ b/src/Doc/Locales/Examples1.thy Wed Nov 04 08:13:52 2015 +0100
@@ -84,6 +84,6 @@
In order to allow for the desired replacement, interpretation
accepts \emph{equations} in addition to the parameter instantiation.
These follow the locale expression and are indicated with the
- keyword \isakeyword{where}. This is the revised interpretation:
+ keyword \isakeyword{rewrites}. This is the revised interpretation:
\<close>
end
--- a/src/Doc/Locales/Examples2.thy Wed Nov 04 08:13:49 2015 +0100
+++ b/src/Doc/Locales/Examples2.thy Wed Nov 04 08:13:52 2015 +0100
@@ -2,7 +2,7 @@
imports Examples
begin
interpretation %visible int: partial_order "op \<le> :: [int, int] \<Rightarrow> bool"
- where "int.less x y = (x < y)"
+ rewrites "int.less x y = (x < y)"
proof -
txt \<open>\normalsize The goals are now:
@{subgoals [display]}
--- a/src/Doc/Locales/Examples3.thy Wed Nov 04 08:13:49 2015 +0100
+++ b/src/Doc/Locales/Examples3.thy Wed Nov 04 08:13:52 2015 +0100
@@ -17,7 +17,7 @@
repeat the example from the previous section to illustrate this.\<close>
interpretation %visible int: partial_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
- where "int.less x y = (x < y)"
+ rewrites "int.less x y = (x < y)"
proof -
show "partial_order (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)"
by unfold_locales auto
@@ -47,7 +47,7 @@
so they can be used in a later example.\<close>
interpretation %visible int: lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
- where int_min_eq: "int.meet x y = min x y"
+ rewrites int_min_eq: "int.meet x y = min x y"
and int_max_eq: "int.join x y = max x y"
proof -
show "lattice (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)"
@@ -611,7 +611,7 @@
\textit{equation} & ::= & [ \textit{attr-name} ``\textbf{:}'' ]
\textit{prop} \\
- \textit{equations} & ::= & \textbf{where} \textit{equation} ( \textbf{and}
+ \textit{equations} & ::= & \textbf{rewrites} \textit{equation} ( \textbf{and}
\textit{equation} )$^*$ \\
\textit{toplevel} & ::=
& \textbf{sublocale} \textit{name} ( ``$<$'' $|$
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Wed Nov 04 08:13:49 2015 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Wed Nov 04 08:13:52 2015 +0100
@@ -504,7 +504,7 @@
end
interpretation x: logic_o "op \<and>" "Not"
- where bool_logic_o: "x.lor_o(x, y) \<longleftrightarrow> x \<or> y"
+ rewrites bool_logic_o: "x.lor_o(x, y) \<longleftrightarrow> x \<or> y"
proof -
show bool_logic_o: "PROP logic_o(op \<and>, Not)" by unfold_locales fast+
show "logic_o.lor_o(op \<and>, Not, x, y) \<longleftrightarrow> x \<or> y"
@@ -546,7 +546,7 @@
lemmas less_thm = less_def
end
-interpretation le: mixin gle where "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
+interpretation le: mixin gle rewrites "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
proof -
show "mixin(gle)" by unfold_locales (rule grefl)
note reflexive = this[unfolded mixin_def]
@@ -588,7 +588,7 @@
locale mixin4_mixin = mixin4_base
interpretation le: mixin4_mixin gle
- where "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
+ rewrites "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
proof -
show "mixin4_mixin(gle)" by unfold_locales (rule grefl)
note reflexive = this[unfolded mixin4_mixin_def mixin4_base_def mixin_def]
@@ -620,7 +620,7 @@
locale mixin5_inherited = mixin5_base
interpretation le5: mixin5_base gle
- where "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
+ rewrites "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
proof -
show "mixin5_base(gle)" by unfold_locales
note reflexive = this[unfolded mixin5_base_def mixin_def]
@@ -648,7 +648,7 @@
interpretation le6: mixin6_inherited gle
by unfold_locales
interpretation le6: mixin6_base gle
- where "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
+ rewrites "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
proof -
show "mixin6_base(gle)" by unfold_locales
note reflexive = this[unfolded mixin6_base_def mixin_def]
@@ -669,7 +669,7 @@
locale mixin7_inherited = reflexive
interpretation le7: mixin7_base gle
- where "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
+ rewrites "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
proof -
show "mixin7_base(gle)" by unfold_locales
note reflexive = this[unfolded mixin7_base_def mixin_def]
@@ -727,7 +727,7 @@
end
sublocale lgrp < "def"?: dgrp
- where one_equation: "dgrp.one(prod) = one" and inv_equation: "dgrp.inv(prod, x) = inv(x)"
+ rewrites one_equation: "dgrp.one(prod) = one" and inv_equation: "dgrp.inv(prod, x) = inv(x)"
proof -
show "dgrp(prod)" by unfold_locales
from this interpret d: dgrp .
@@ -766,7 +766,7 @@
locale roundup = fixes x assumes true: "x \<longleftrightarrow> True"
-sublocale roundup \<subseteq> sub: roundup x where "x \<longleftrightarrow> True \<and> True"
+sublocale roundup \<subseteq> sub: roundup x rewrites "x \<longleftrightarrow> True \<and> True"
apply unfold_locales apply (simp add: true) done
lemma (in roundup) "True \<and> True \<longleftrightarrow> True" by (rule sub.true)
@@ -816,7 +816,7 @@
and pnotnot: "\<And>x. pnot(pnot(x)) \<longleftrightarrow> x"
and por_def: "\<And>x y. por(x, y) \<longleftrightarrow> pnot(pand(pnot(x), pnot(y)))"
interpret loc: logic_o pand pnot
- where por_eq: "\<And>x y. logic_o.lor_o(pand, pnot, x, y) \<longleftrightarrow> por(x, y)" (* FIXME *)
+ rewrites por_eq: "\<And>x y. logic_o.lor_o(pand, pnot, x, y) \<longleftrightarrow> por(x, y)" (* FIXME *)
proof -
show logic_o: "PROP logic_o(pand, pnot)" using passoc pnotnot by unfold_locales
fix x y
--- a/src/FOL/ex/Locale_Test/Locale_Test2.thy Wed Nov 04 08:13:49 2015 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test2.thy Wed Nov 04 08:13:52 2015 +0100
@@ -9,7 +9,7 @@
begin
interpretation le1: mixin_thy_merge gle gle'
- where "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
+ rewrites "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
proof -
show "mixin_thy_merge(gle, gle')" by unfold_locales
note reflexive = this[unfolded mixin_thy_merge_def, THEN conjunct1]
--- a/src/FOL/ex/Locale_Test/Locale_Test3.thy Wed Nov 04 08:13:49 2015 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test3.thy Wed Nov 04 08:13:52 2015 +0100
@@ -9,7 +9,7 @@
begin
interpretation le2: mixin_thy_merge gle gle'
- where "reflexive.less(gle', x, y) \<longleftrightarrow> gless'(x, y)"
+ rewrites "reflexive.less(gle', x, y) \<longleftrightarrow> gless'(x, y)"
proof -
show "mixin_thy_merge(gle, gle')" by unfold_locales
note reflexive = this[unfolded mixin_thy_merge_def, THEN conjunct2]
--- a/src/HOL/Algebra/IntRing.thy Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/Algebra/IntRing.thy Wed Nov 04 08:13:52 2015 +0100
@@ -54,7 +54,7 @@
with as few assumptions as possible.\<close>
interpretation int: monoid \<Z>
- where "carrier \<Z> = UNIV"
+ rewrites "carrier \<Z> = UNIV"
and "mult \<Z> x y = x * y"
and "one \<Z> = 1"
and "pow \<Z> x n = x^n"
@@ -73,7 +73,7 @@
qed
interpretation int: comm_monoid \<Z>
- where "finprod \<Z> f A = setprod f A"
+ rewrites "finprod \<Z> f A = setprod f A"
proof -
-- "Specification"
show "comm_monoid \<Z>" by standard auto
@@ -88,7 +88,7 @@
qed
interpretation int: abelian_monoid \<Z>
- where int_carrier_eq: "carrier \<Z> = UNIV"
+ rewrites int_carrier_eq: "carrier \<Z> = UNIV"
and int_zero_eq: "zero \<Z> = 0"
and int_add_eq: "add \<Z> x y = x + y"
and int_finsum_eq: "finsum \<Z> f A = setsum f A"
@@ -114,7 +114,7 @@
Since the morphisms through which the abelian structures are interpreted are
not the identity, the equations of these interpretations are not inherited. *)
(* FIXME *)
- where "carrier \<Z> = UNIV"
+ rewrites "carrier \<Z> = UNIV"
and "zero \<Z> = 0"
and "add \<Z> x y = x + y"
and "finsum \<Z> f A = setsum f A"
@@ -147,7 +147,7 @@
qed (simp add: int_carrier_eq int_zero_eq int_add_eq int_finsum_eq)+
interpretation int: "domain" \<Z>
- where "carrier \<Z> = UNIV"
+ rewrites "carrier \<Z> = UNIV"
and "zero \<Z> = 0"
and "add \<Z> x y = x + y"
and "finsum \<Z> f A = setsum f A"
@@ -173,7 +173,7 @@
interpretation int (* FIXME [unfolded UNIV] *) :
partial_order "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
- where "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> = UNIV"
+ rewrites "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> = UNIV"
and "le \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x \<le> y)"
and "lless \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x < y)"
proof -
@@ -189,7 +189,7 @@
interpretation int (* FIXME [unfolded UNIV] *) :
lattice "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
- where "join \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = max x y"
+ rewrites "join \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = max x y"
and "meet \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = min x y"
proof -
let ?Z = "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
--- a/src/HOL/Algebra/Ring.thy Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/Algebra/Ring.thy Wed Nov 04 08:13:52 2015 +0100
@@ -95,7 +95,7 @@
sublocale abelian_monoid <
add!: monoid "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
- where "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
+ rewrites "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
and "mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = add G"
and "one \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = zero G"
by (rule a_monoid) auto
@@ -113,7 +113,7 @@
sublocale abelian_monoid <
add!: comm_monoid "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
- where "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
+ rewrites "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
and "mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = add G"
and "one \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = zero G"
and "finprod \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = finsum G"
@@ -169,7 +169,7 @@
sublocale abelian_group <
add!: group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
- where "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
+ rewrites "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
and "mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = add G"
and "one \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = zero G"
and "m_inv \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = a_inv G"
@@ -197,7 +197,7 @@
sublocale abelian_group <
add!: comm_group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
- where "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
+ rewrites "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
and "mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = add G"
and "one \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = zero G"
and "m_inv \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = a_inv G"
--- a/src/HOL/Finite_Set.thy Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/Finite_Set.thy Wed Nov 04 08:13:52 2015 +0100
@@ -1197,7 +1197,7 @@
"card = folding.F (\<lambda>_. Suc) 0"
interpretation card!: folding "\<lambda>_. Suc" 0
-where
+rewrites
"folding.F (\<lambda>_. Suc) 0 = card"
proof -
show "folding (\<lambda>_. Suc)" by standard rule
--- a/src/HOL/GCD.thy Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/GCD.thy Wed Nov 04 08:13:52 2015 +0100
@@ -1971,7 +1971,7 @@
interpretation gcd_lcm_complete_lattice_nat:
complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat"
-where "Inf.INFIMUM Gcd A f = Gcd (f ` A :: nat set)"
+rewrites "Inf.INFIMUM Gcd A f = Gcd (f ` A :: nat set)"
and "Sup.SUPREMUM Lcm A f = Lcm (f ` A)"
proof -
show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\<lambda>m n. m dvd n \<and> \<not> n dvd m) lcm 1 (0::nat)"
--- a/src/HOL/Groups_Big.thy Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/Groups_Big.thy Wed Nov 04 08:13:52 2015 +0100
@@ -472,7 +472,7 @@
"setsum = comm_monoid_set.F plus 0"
sublocale setsum!: comm_monoid_set plus 0
-where
+rewrites
"comm_monoid_set.F plus 0 = setsum"
proof -
show "comm_monoid_set plus 0" ..
@@ -1063,7 +1063,7 @@
"setprod = comm_monoid_set.F times 1"
sublocale setprod!: comm_monoid_set times 1
-where
+rewrites
"comm_monoid_set.F times 1 = setprod"
proof -
show "comm_monoid_set times 1" ..
--- a/src/HOL/Groups_List.thy Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/Groups_List.thy Wed Nov 04 08:13:52 2015 +0100
@@ -66,7 +66,7 @@
"listsum = monoid_list.F plus 0"
sublocale listsum!: monoid_list plus 0
-where
+rewrites
"monoid_list.F plus 0 = listsum"
proof -
show "monoid_list plus 0" ..
@@ -80,7 +80,7 @@
begin
sublocale listsum!: comm_monoid_list plus 0
-where
+rewrites
"monoid_list.F plus 0 = listsum"
proof -
show "comm_monoid_list plus 0" ..
@@ -89,7 +89,7 @@
qed
sublocale setsum!: comm_monoid_list_set plus 0
-where
+rewrites
"monoid_list.F plus 0 = listsum"
and "comm_monoid_set.F plus 0 = setsum"
proof -
@@ -333,7 +333,7 @@
"listprod = monoid_list.F times 1"
sublocale listprod!: monoid_list times 1
-where
+rewrites
"monoid_list.F times 1 = listprod"
proof -
show "monoid_list times 1" ..
@@ -347,7 +347,7 @@
begin
sublocale listprod!: comm_monoid_list times 1
-where
+rewrites
"monoid_list.F times 1 = listprod"
proof -
show "comm_monoid_list times 1" ..
@@ -356,7 +356,7 @@
qed
sublocale setprod!: comm_monoid_list_set times 1
-where
+rewrites
"monoid_list.F times 1 = listprod"
and "comm_monoid_set.F times 1 = setprod"
proof -
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Wed Nov 04 08:13:52 2015 +0100
@@ -405,7 +405,7 @@
qed
interpretation heap!: partial_function_definitions Heap_ord Heap_lub
- where "Heap_lub {} \<equiv> Heap Map.empty"
+ rewrites "Heap_lub {} \<equiv> Heap Map.empty"
by (fact heap_interpretation)(simp add: Heap_lub_empty)
lemma heap_step_admissible:
--- a/src/HOL/Lattices_Big.thy Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/Lattices_Big.thy Wed Nov 04 08:13:52 2015 +0100
@@ -319,7 +319,7 @@
"Inf_fin = semilattice_set.F inf"
sublocale Inf_fin!: semilattice_order_set inf less_eq less
-where
+rewrites
"semilattice_set.F inf = Inf_fin"
proof -
show "semilattice_order_set inf less_eq less" ..
@@ -337,7 +337,7 @@
"Sup_fin = semilattice_set.F sup"
sublocale Sup_fin!: semilattice_order_set sup greater_eq greater
-where
+rewrites
"semilattice_set.F sup = Sup_fin"
proof -
show "semilattice_order_set sup greater_eq greater" ..
@@ -492,7 +492,7 @@
sublocale Min!: semilattice_order_set min less_eq less
+ Max!: semilattice_order_set max greater_eq greater
-where
+rewrites
"semilattice_set.F min = Min"
and "semilattice_set.F max = Max"
proof -
--- a/src/HOL/Library/Function_Growth.thy Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/Library/Function_Growth.thy Wed Nov 04 08:13:52 2015 +0100
@@ -192,7 +192,7 @@
text \<open>This yields all lemmas relating @{text "\<lesssim>"}, @{text "\<prec>"} and @{text "\<cong>"}.\<close>
interpretation fun_order: preorder_equiv less_eq_fun less_fun
- where "preorder_equiv.equiv less_eq_fun = equiv_fun"
+ rewrites "preorder_equiv.equiv less_eq_fun = equiv_fun"
proof -
interpret preorder: preorder_equiv less_eq_fun less_fun
proof
--- a/src/HOL/Library/Multiset.thy Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/Library/Multiset.thy Wed Nov 04 08:13:52 2015 +0100
@@ -1060,7 +1060,7 @@
"mset_set = folding.F (\<lambda>x M. {#x#} + M) {#}"
interpretation mset_set!: folding "\<lambda>x M. {#x#} + M" "{#}"
-where
+rewrites
"folding.F (\<lambda>x M. {#x#} + M) {#} = mset_set"
proof -
interpret comp_fun_commute "\<lambda>x M. {#x#} + M"
@@ -1223,7 +1223,7 @@
where "msetsum = comm_monoid_mset.F plus 0"
sublocale msetsum!: comm_monoid_mset plus 0
- where "comm_monoid_mset.F plus 0 = msetsum"
+ rewrites "comm_monoid_mset.F plus 0 = msetsum"
proof -
show "comm_monoid_mset plus 0" ..
from msetsum_def show "comm_monoid_mset.F plus 0 = msetsum" ..
@@ -1281,7 +1281,7 @@
where "msetprod = comm_monoid_mset.F times 1"
sublocale msetprod!: comm_monoid_mset times 1
- where "comm_monoid_mset.F times 1 = msetprod"
+ rewrites "comm_monoid_mset.F times 1 = msetprod"
proof -
show "comm_monoid_mset times 1" ..
show "comm_monoid_mset.F times 1 = msetprod" using msetprod_def ..
--- a/src/HOL/Library/Saturated.thy Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/Library/Saturated.thy Wed Nov 04 08:13:52 2015 +0100
@@ -215,7 +215,7 @@
end
interpretation Inf_sat!: semilattice_neutr_set min "top :: 'a::len sat"
-where
+rewrites
"semilattice_neutr_set.F min (top :: 'a sat) = Inf"
proof -
show "semilattice_neutr_set min (top :: 'a sat)"
@@ -225,7 +225,7 @@
qed
interpretation Sup_sat!: semilattice_neutr_set max "bot :: 'a::len sat"
-where
+rewrites
"semilattice_neutr_set.F max (bot :: 'a sat) = Sup"
proof -
show "semilattice_neutr_set max (bot :: 'a sat)"
--- a/src/HOL/List.thy Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/List.thy Wed Nov 04 08:13:52 2015 +0100
@@ -5151,7 +5151,7 @@
"sorted_list_of_set = folding.F insort []"
sublocale sorted_list_of_set!: folding insort Nil
-where
+rewrites
"folding.F insort [] = sorted_list_of_set"
proof -
interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
--- a/src/HOL/Partial_Function.thy Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/Partial_Function.thy Wed Nov 04 08:13:52 2015 +0100
@@ -283,12 +283,12 @@
interpretation tailrec!:
partial_function_definitions "flat_ord undefined" "flat_lub undefined"
- where "flat_lub undefined {} \<equiv> undefined"
+ rewrites "flat_lub undefined {} \<equiv> undefined"
by (rule flat_interpretation)(simp add: flat_lub_def)
interpretation option!:
partial_function_definitions "flat_ord None" "flat_lub None"
- where "flat_lub None {} \<equiv> None"
+ rewrites "flat_lub None {} \<equiv> None"
by (rule flat_interpretation)(simp add: flat_lub_def)
--- a/src/HOL/ex/LocaleTest2.thy Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/ex/LocaleTest2.thy Wed Nov 04 08:13:52 2015 +0100
@@ -469,7 +469,7 @@
subsubsection \<open>Total order @{text "<="} on @{typ int}\<close>
interpretation int: dpo "op <= :: [int, int] => bool"
- where "(dpo.less (op <=) (x::int) y) = (x < y)"
+ rewrites "(dpo.less (op <=) (x::int) y) = (x < y)"
txt \<open>We give interpretation for less, but not @{text is_inf} and @{text is_sub}.\<close>
proof -
show "dpo (op <= :: [int, int] => bool)"
@@ -488,7 +488,7 @@
apply (rule int.abs_test) done
interpretation int: dlat "op <= :: [int, int] => bool"
- where meet_eq: "dlat.meet (op <=) (x::int) y = min x y"
+ rewrites meet_eq: "dlat.meet (op <=) (x::int) y = min x y"
and join_eq: "dlat.join (op <=) (x::int) y = max x y"
proof -
show "dlat (op <= :: [int, int] => bool)"
@@ -525,7 +525,7 @@
subsubsection \<open>Total order @{text "<="} on @{typ nat}\<close>
interpretation nat: dpo "op <= :: [nat, nat] => bool"
- where "dpo.less (op <=) (x::nat) y = (x < y)"
+ rewrites "dpo.less (op <=) (x::nat) y = (x < y)"
txt \<open>We give interpretation for less, but not @{text is_inf} and @{text is_sub}.\<close>
proof -
show "dpo (op <= :: [nat, nat] => bool)"
@@ -539,7 +539,7 @@
qed
interpretation nat: dlat "op <= :: [nat, nat] => bool"
- where "dlat.meet (op <=) (x::nat) y = min x y"
+ rewrites "dlat.meet (op <=) (x::nat) y = min x y"
and "dlat.join (op <=) (x::nat) y = max x y"
proof -
show "dlat (op <= :: [nat, nat] => bool)"
@@ -576,7 +576,7 @@
subsubsection \<open>Lattice @{text "dvd"} on @{typ nat}\<close>
interpretation nat_dvd: dpo "op dvd :: [nat, nat] => bool"
- where "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
+ rewrites "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
txt \<open>We give interpretation for less, but not @{text is_inf} and @{text is_sub}.\<close>
proof -
show "dpo (op dvd :: [nat, nat] => bool)"
@@ -590,7 +590,7 @@
qed
interpretation nat_dvd: dlat "op dvd :: [nat, nat] => bool"
- where "dlat.meet (op dvd) (x::nat) y = gcd x y"
+ rewrites "dlat.meet (op dvd) (x::nat) y = gcd x y"
and "dlat.join (op dvd) (x::nat) y = lcm x y"
proof -
show "dlat (op dvd :: [nat, nat] => bool)"
@@ -835,7 +835,7 @@
subsubsection \<open>Interpretation of Functions\<close>
interpretation Dfun: Dmonoid "op o" "id :: 'a => 'a"
- where "Dmonoid.unit (op o) id f = bij (f::'a => 'a)"
+ rewrites "Dmonoid.unit (op o) id f = bij (f::'a => 'a)"
(* and "Dmonoid.inv (op o) id" = "inv :: ('a => 'a) => ('a => 'a)" *)
proof -
show "Dmonoid op o (id :: 'a => 'a)" proof qed (simp_all add: o_assoc)
@@ -885,7 +885,7 @@
by rule simp
interpretation Dfun: Dgrp "op o" "id :: unit => unit"
- where "Dmonoid.inv (op o) id f = inv (f :: unit => unit)"
+ rewrites "Dmonoid.inv (op o) id f = inv (f :: unit => unit)"
proof -
have "Dmonoid op o (id :: 'a => 'a)" ..
note Dmonoid = this
--- a/src/Pure/Isar/isar_syn.ML Wed Nov 04 08:13:49 2015 +0100
+++ b/src/Pure/Isar/isar_syn.ML Wed Nov 04 08:13:52 2015 +0100
@@ -405,7 +405,7 @@
val interpretation_args =
Parse.!!! (Parse_Spec.locale_expression true) --
Scan.optional
- (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
+ (@{keyword "rewrites"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
val _ =
Outer_Syntax.command @{command_keyword sublocale}
--- a/src/Pure/Pure.thy Wed Nov 04 08:13:49 2015 +0100
+++ b/src/Pure/Pure.thy Wed Nov 04 08:13:52 2015 +0100
@@ -11,8 +11,8 @@
"\<subseteq>" "]" "assumes" "attach" "binder" "constrains"
"defines" "fixes" "for" "identifier" "if" "in" "includes" "infix"
"infixl" "infixr" "is" "notes" "obtains" "open" "output"
- "overloaded" "pervasive" "premises" "private" "qualified" "shows"
- "structure" "unchecked" "where" "when" "|"
+ "overloaded" "pervasive" "premises" "private" "qualified" "rewrites"
+ "shows" "structure" "unchecked" "where" "when" "|"
and "text" "txt" :: document_body
and "text_raw" :: document_raw
and "default_sort" :: thy_decl == ""