src/FOL/ex/LocaleTest.thy

--- a/src/FOL/ex/LocaleTest.thy	Wed Aug 17 17:03:20 2005 +0200
+++ b/src/FOL/ex/LocaleTest.thy	Wed Aug 17 17:04:15 2005 +0200
@@ -544,7 +544,7 @@
 print_locale Rplgrp
 
 subsection {* Interaction of Interpretation in Theories and Locales:
-  in locale, then in theory *}
+  in Locale, then in Theory *}
 
 consts
   rone :: i
@@ -585,7 +585,7 @@
 
 
 subsection {* Interaction of Interpretation in Theories and Locales:
-  in theory, then in locale *}
+  in Theory, then in Locale *}
 
 (* Another copy of the group example *)
 
@@ -650,16 +650,94 @@
     }
   qed
 
-(*
-print_interps Rqrgrp
-thm R2.rcancel
-*)
+
+subsection {* Generation of Witness Theorems for Transitive Interpretations *}
+
+locale Rtriv = var x +
+  assumes x: "x = x"
+
+locale Rtriv2 = var x + var y +
+  assumes x: "x = x" and y: "y = y"
+
+interpretation Rtriv2 < Rtriv x
+  apply (rule Rtriv.intro)
+  apply (rule x)
+  done
+
+interpretation Rtriv2 < Rtriv y
+  apply (rule Rtriv.intro)
+  apply (rule y)
+  done
+
+print_locale Rtriv2
+
+locale Rtriv3 = var x + var y + var z +
+  assumes x: "x = x" and y: "y = y" and z: "z = z"
+
+interpretation Rtriv3 < Rtriv2 x y
+  apply (rule Rtriv2.intro)
+  apply (rule x)
+  apply (rule y)
+  done
+
+print_locale Rtriv3
+
+interpretation Rtriv3 < Rtriv2 x z
+  apply (rule Rtriv2.intro)
+  apply (rule x_y_z.x)
+  apply (rule z)
+  done
+
+ML {* set show_types *}
+
+print_locale Rtriv3
+
+
+subsection {* Normalisation Replaces Assumed Element by Derived Element *}
+
+typedecl ('a, 'b) pair
+arities pair :: ("term", "term") "term"
+
+consts
+  pair :: "['a, 'b] => ('a, 'b) pair"
+  fst :: "('a, 'b) pair => 'a"
+  snd :: "('a, 'b) pair => 'b"
+
+axioms
+  fst [simp]: "fst(pair(x, y)) = x"
+  snd [simp]: "snd(pair(x, y)) = y"
+
+locale Rpair = var prod (infixl "**" 65) + var prodP (infixl "***" 65) +
+  defines P_def: "x *** y == pair(fst(x) ** fst(y), snd(x) ** snd(y))"
+
+locale Rpair_semi = Rpair + Rpsemi
+
+interpretation Rpair_semi < Rpsemi prodP (infixl "***" 65)
+proof (rule Rpsemi.intro)
+  fix x y z
+  show "(x *** y) *** z = x *** (y *** z)"
+    by (unfold P_def) (simp add: assoc)
+qed
+
+locale Rsemi_rev = Rpsemi + var rprod (infixl "++" 65) +
+  defines r_def: "x ++ y == y ** x"
+
+lemma (in Rsemi_rev) r_assoc:
+  "(x ++ y) ++ z = x ++ (y ++ z)"
+  by (simp add: r_def assoc)
+
+lemma (in Rpair_semi)
+  includes Rsemi_rev prodP (infixl "***" 65) rprodP (infixl "+++" 65)
+  constrains prod :: "['a, 'a] => 'a"
+    and rprodP :: "[('a, 'a) pair, ('a, 'a) pair] => ('a, 'a) pair"
+  shows "(x +++ y) +++ z = x +++ (y +++ z)"
+  apply (rule r_assoc) done
 
 end
 
 (* Known problems:
 - var vs. fixes in locale to be interpreted (interpretation in locale)
-  (implicit locale expressions renerated by multiple registrations)
+  (implicit locale expressions generated by multiple registrations)
 - reprocess registrations in theory (after qed)?
 - current finish_global adds unwanted lemmas to theory/locale
 *)