--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Mon Sep 02 17:57:56 2013 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Tue Sep 03 22:12:47 2013 +0200
@@ -484,7 +484,9 @@
by unfold_locales
-subsection {* Equations *}
+subsection {* Interpretation *}
+
+subsection {* Rewrite morphism *}
locale logic_o =
fixes land (infixl "&&" 55)
@@ -516,7 +518,7 @@
x.lor_triv
-subsection {* Inheritance of mixins *}
+subsection {* Inheritance of rewrite morphisms *}
locale reflexive =
fixes le :: "'a => 'a => o" (infix "\<sqsubseteq>" 50)
@@ -549,7 +551,7 @@
by (simp add: reflexive.less_def[OF reflexive] gless_def)
qed
-text {* Mixin propagated along the locale hierarchy *}
+text {* Rewrite morphism propagated along the locale hierarchy *}
locale mixin2 = mixin
begin
@@ -559,11 +561,11 @@
interpretation le: mixin2 gle
by unfold_locales
-thm le.less_thm2 (* mixin applied *)
+thm le.less_thm2 (* rewrite morphism applied *)
lemma "gless(x, y) <-> gle(x, y) & x ~= y"
by (rule le.less_thm2)
-text {* Mixin does not leak to a side branch. *}
+text {* Rewrite morphism does not leak to a side branch. *}
locale mixin3 = reflexive
begin
@@ -573,10 +575,10 @@
interpretation le: mixin3 gle
by unfold_locales
-thm le.less_thm3 (* mixin not applied *)
+thm le.less_thm3 (* rewrite morphism not applied *)
lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y" by (rule le.less_thm3)
-text {* Mixin only available in original context *}
+text {* Rewrite morphism only available in original context *}
locale mixin4_base = reflexive
@@ -604,11 +606,11 @@
interpretation le4: mixin4_combined gle' gle
by unfold_locales (rule grefl')
-thm le4.less_thm4' (* mixin not applied *)
+thm le4.less_thm4' (* rewrite morphism not applied *)
lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
by (rule le4.less_thm4')
-text {* Inherited mixin applied to new theorem *}
+text {* Inherited rewrite morphism applied to new theorem *}
locale mixin5_base = reflexive
@@ -628,11 +630,11 @@
lemmas (in mixin5_inherited) less_thm5 = less_def
-thm le5.less_thm5 (* mixin applied *)
+thm le5.less_thm5 (* rewrite morphism applied *)
lemma "gless(x, y) <-> gle(x, y) & x ~= y"
by (rule le5.less_thm5)
-text {* Mixin pushed down to existing inherited locale *}
+text {* Rewrite morphism pushed down to existing inherited locale *}
locale mixin6_base = reflexive
@@ -657,7 +659,7 @@
lemma "gless(x, y) <-> gle(x, y) & x ~= y"
by (rule le6.less_thm6)
-text {* Existing mixin inherited through sublocale relation *}
+text {* Existing rewrite morphism inherited through sublocale relation *}
locale mixin7_base = reflexive
@@ -677,7 +679,7 @@
lemmas (in mixin7_inherited) less_thm7 = less_def
-thm le7.less_thm7 (* before, mixin not applied *)
+thm le7.less_thm7 (* before, rewrite morphism not applied *)
lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
by (rule le7.less_thm7)
@@ -696,7 +698,7 @@
locale mixin_thy_merge = le: reflexive le + le': reflexive le' for le le'
-subsection {* Mixins in sublocale *}
+subsection {* Rewrite morphisms in sublocale *}
text {* Simulate a specification of left groups where unit and inverse are defined
rather than specified. This is possible, but not in FOL, due to the lack of a
@@ -745,7 +747,7 @@
lemma "dgrp.one(prod) = one" by (rule one_equation)
lemma "dgrp.inv(prod, x) = inv(x)" by (rule inv_equation)
-text {* Mixins applied *}
+text {* Rewrite morphisms applied *}
lemma "one = glob_one(prod)" by (rule one_def)
lemma "inv(x) = glob_inv(prod, x)" by (rule inv_def)
@@ -757,7 +759,7 @@
lemma "0 = glob_one (op +)" by (rule int.def.one_def)
lemma "- x = glob_inv(op +, x)" by (rule int.def.inv_def)
-text {* Roundup applies mixins at declaration level in DFS tree *}
+text {* Roundup applies rewrite morphisms at declaration level in DFS tree *}
locale roundup = fixes x assumes true: "x <-> True"