New file for locale regression tests.

--- a/src/HOL/IsaMakefile	Fri Apr 13 09:23:35 2007 +0200
+++ b/src/HOL/IsaMakefile	Fri Apr 13 10:00:04 2007 +0200
@@ -626,7 +626,8 @@
   ex/Fundefs.thy ex/Guess.thy ex/Hebrew.thy ex/Binary.thy                       \
   ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy ex/InSort.thy		\
   ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy			\
-  ex/Intuitionistic.thy ex/Lagrange.thy ex/Locales.thy ex/MT.ML			\
+  ex/Intuitionistic.thy ex/Lagrange.thy ex/Locales.thy				\
+  ex/LocaleTest2.thy ex/MT.ML							\
   ex/MT.thy ex/MergeSort.thy ex/MonoidGroup.thy ex/Multiquote.thy		\
   ex/NatSum.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy			\
   ex/Puzzle.thy ex/Qsort.thy ex/Quickcheck_Examples.thy				\

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/LocaleTest2.thy	Fri Apr 13 10:00:04 2007 +0200
@@ -0,0 +1,159 @@
+(*  Title:      HOL/ex/LocaleTest2.thy
+    ID:         $Id$
+    Author:     Clemens Ballarin
+    Copyright (c) 2007 by Clemens Ballarin
+
+More regression tests for locales.
+Definitions are less natural in FOL, since there is no selection operator.
+Hence we do them in HOL, not in the main test suite for locales:
+FOL/ex/LocaleTest.thy
+*)
+
+header {* Test of Locale Interpretation *}
+
+theory LocaleTest2
+imports Main
+begin
+
+ML {* set quick_and_dirty *}    (* allow for thm command in batch mode *)
+ML {* set Toplevel.debug *}
+ML {* set show_hyps *}
+ML {* set show_sorts *}
+
+section {* Interpretation of Defined Concepts *}
+
+text {* Naming convention for global objects: prefixes D and d *}
+
+(* Group example with defined operation inv *)
+
+locale Dsemi =
+  fixes prod (infixl "**" 65)
+  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
+
+locale Dmonoid = Dsemi +
+  fixes one
+  assumes lone: "one ** x = x"
+    and rone: "x ** one = x"
+
+definition (in Dmonoid)
+  inv where "inv(x) == THE y. x ** y = one & y ** x = one"
+
+lemma (in Dmonoid) inv_unique:
+  assumes eq: "y ** x = one" "x ** y' = one"
+  shows "y = y'"
+proof -
+  from eq have "y = y ** (x ** y')" by (simp add: rone)
+  also have "... = (y ** x) ** y'" by (simp add: assoc)
+  also from eq have "... = y'" by (simp add: lone)
+  finally show ?thesis .
+qed
+
+locale Dgrp = Dmonoid +
+  assumes linv_ex: "EX y. y ** x = one"
+    and rinv_ex: "EX y. x ** y = one"
+
+lemma (in Dgrp) linv:
+  "inv x ** x = one"
+apply (unfold inv_def)
+apply (insert rinv_ex [where x = x])
+apply (insert linv_ex [where x = x])
+apply (erule exE) apply (erule exE)
+apply (rule theI2)
+apply rule apply assumption
+apply (frule inv_unique, assumption)
+apply simp
+apply (rule inv_unique)
+apply fast+
+done
+
+lemma (in Dgrp) rinv:
+  "x ** inv x = one"
+apply (unfold inv_def)
+apply (insert rinv_ex [where x = x])
+apply (insert linv_ex [where x = x])
+apply (erule exE) apply (erule exE)
+apply (rule theI2)
+apply rule apply assumption
+apply (frule inv_unique, assumption)
+apply simp
+apply (rule inv_unique)
+apply fast+
+done
+
+lemma (in Dgrp) lcancel:
+  "x ** y = x ** z <-> y = z"
+proof
+  assume "x ** y = x ** z"
+  then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
+  then show "y = z" by (simp add: lone linv)
+qed simp
+
+interpretation Dint: Dmonoid ["op +" "0::int"]
+  where "Dmonoid.inv (op +) (0::int)" = "uminus"
+proof -
+  show "Dmonoid (op +) (0::int)" by unfold_locales auto
+  note Dint = this (* should have this as an assumption in further goals *)
+  {
+    fix x
+    have "Dmonoid.inv (op +) (0::int) x = - x"
+      by (auto simp: Dmonoid.inv_def [OF Dint])
+  }
+  then show "Dmonoid.inv (op +) (0::int) == uminus"
+    by (rule_tac eq_reflection) (fast intro: ext)
+qed
+
+thm Dmonoid.inv_def Dint.inv_def
+
+lemma "- x \<equiv> THE y. x + y = 0 \<and> y + x = (0::int)"
+  apply (rule Dint.inv_def) done
+
+interpretation Dclass: Dmonoid ["op +" "0::'a::ab_group_add"]
+  where "Dmonoid.inv (op +) (0::'a::ab_group_add)" = "uminus"
+proof -
+  show "Dmonoid (op +) (0::'b::ab_group_add)" by unfold_locales auto
+  note Dclass = this (* should have this as an assumption in further goals *)
+  {
+    fix x
+    have "Dmonoid.inv (op +) (0::'b::ab_group_add) x = - x"
+      by (auto simp: Dmonoid.inv_def [OF Dclass] equals_zero_I [symmetric])
+  }
+  then show "Dmonoid.inv (op +) (0::'b::ab_group_add) == uminus"
+    by (rule_tac eq_reflection) (fast intro: ext)
+qed
+
+interpretation Dclass: Dgrp ["op +" "0::'a::ring"]
+apply unfold_locales
+apply (rule_tac x="-x" in exI) apply simp
+apply (rule_tac x="-x" in exI) apply simp
+done
+
+(* Equation for inverse from Dclass: Dmonoid effective. *)
+
+thm Dclass.linv
+lemma "-x + x = (0::'a::ring)" apply (rule Dclass.linv) done
+
+(* Equations have effect in "subscriptions" *)
+
+(* In the same module *)
+
+lemma (in Dmonoid) trivial:
+  "inv one = inv one"
+  by rule
+
+thm Dclass.trivial
+
+(* Inherited: interpretation *)
+
+lemma (in Dgrp) inv_inv:
+  "inv (inv x) = x"
+proof -
+  have "inv x ** inv (inv x) = inv x ** x"
+    by (simp add: linv rinv)
+  then show ?thesis by (simp add: lcancel)
+qed
+
+thm Dclass.inv_inv
+lemma "- (- x) = (x::'a::ring)"
+  apply (rule Dclass.inv_inv) done
+
+end

--- a/src/HOL/ex/ROOT.ML	Fri Apr 13 09:23:35 2007 +0200
+++ b/src/HOL/ex/ROOT.ML	Fri Apr 13 10:00:04 2007 +0200
@@ -23,6 +23,7 @@
 time_use_thy "InductiveInvariant_examples";
 time_use_thy "Primrec";
 time_use_thy "Locales";
+time_use_thy "LocaleTest2";
 time_use_thy "Records";
 time_use_thy "MonoidGroup";
 time_use_thy "BinEx";