# HG changeset patch
# User ballarin
# Date 1227778242 -3600
# Node ID f30016592375f8d2f0d7080eae399a7450f30907
# Parent  4e2914c2f8c515a418ebceebc8d4a2c748467825
Tests for sublocale command.

diff -r 4e2914c2f8c5 -r f30016592375 src/FOL/ex/NewLocaleTest.thy
--- a/src/FOL/ex/NewLocaleTest.thy	Thu Nov 27 10:29:07 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy	Thu Nov 27 10:30:42 2008 +0100
@@ -59,7 +59,6 @@
 locale semi =
   fixes prod (infixl "**" 65)
   assumes assoc: "(x ** y) ** z = x ** (y ** z)"
-    and comm: "x ** y = y ** x"
 print_locale! semi thm semi_def
 
 locale lgrp = semi +
@@ -163,4 +162,58 @@
   shows "?p <-> ?p"
   .
 
+
+text {* Interpretation between locales: sublocales *}
+
+sublocale lgrp < right: rgrp
+print_facts
+proof (intro rgrp.intro semi.intro rgrp_axioms.intro)
+  {
+    fix x
+    have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
+    then show "x ** one = x" by (simp add: assoc lcancel)
+  }
+  note rone = this
+  {
+    fix x
+    have "inv(x) ** x ** inv(x) = inv(x) ** one"
+      by (simp add: linv lone rone)
+    then show "x ** inv(x) = one" by (simp add: assoc lcancel)
+  }
+qed (simp add: assoc)
+
+(* effect on printed locale *)
+
+print_locale! lgrp
+
+(* use of derived theorem *)
+
+lemma (in lgrp)
+  "y ** x = z ** x <-> y = z"
+  apply (rule rcancel)
+  done
+
+(* circular interpretation *)
+
+sublocale rgrp < left: lgrp
+  proof (intro lgrp.intro semi.intro lgrp_axioms.intro)
+    {
+      fix x
+      have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
+      then show "one ** x = x" by (simp add: assoc [symmetric] rcancel)
+    }
+    note lone = this
+    {
+      fix x
+      have "inv(x) ** (x ** inv(x)) = one ** inv(x)"
+	by (simp add: rinv lone rone)
+      then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel)
+    }
+  qed (simp add: assoc)
+
+(* effect on printed locale *)
+
+print_locale! rgrp
+print_locale! lgrp
+
 end