1.1 --- a/src/FOL/ex/NewLocaleTest.thy	Thu Nov 27 10:29:07 2008 +0100
     1.2 +++ b/src/FOL/ex/NewLocaleTest.thy	Thu Nov 27 10:30:42 2008 +0100
     1.3 @@ -59,7 +59,6 @@
     1.4  locale semi =
     1.5    fixes prod (infixl "**" 65)
     1.6    assumes assoc: "(x ** y) ** z = x ** (y ** z)"
     1.7 -    and comm: "x ** y = y ** x"
     1.8  print_locale! semi thm semi_def
     1.9  
    1.10  locale lgrp = semi +
    1.11 @@ -163,4 +162,58 @@
    1.12    shows "?p <-> ?p"
    1.13    .
    1.14  
    1.15 +
    1.16 +text {* Interpretation between locales: sublocales *}
    1.17 +
    1.18 +sublocale lgrp < right: rgrp
    1.19 +print_facts
    1.20 +proof (intro rgrp.intro semi.intro rgrp_axioms.intro)
    1.21 +  {
    1.22 +    fix x
    1.23 +    have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
    1.24 +    then show "x ** one = x" by (simp add: assoc lcancel)
    1.25 +  }
    1.26 +  note rone = this
    1.27 +  {
    1.28 +    fix x
    1.29 +    have "inv(x) ** x ** inv(x) = inv(x) ** one"
    1.30 +      by (simp add: linv lone rone)
    1.31 +    then show "x ** inv(x) = one" by (simp add: assoc lcancel)
    1.32 +  }
    1.33 +qed (simp add: assoc)
    1.34 +
    1.35 +(* effect on printed locale *)
    1.36 +
    1.37 +print_locale! lgrp
    1.38 +
    1.39 +(* use of derived theorem *)
    1.40 +
    1.41 +lemma (in lgrp)
    1.42 +  "y ** x = z ** x <-> y = z"
    1.43 +  apply (rule rcancel)
    1.44 +  done
    1.45 +
    1.46 +(* circular interpretation *)
    1.47 +
    1.48 +sublocale rgrp < left: lgrp
    1.49 +  proof (intro lgrp.intro semi.intro lgrp_axioms.intro)
    1.50 +    {
    1.51 +      fix x
    1.52 +      have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
    1.53 +      then show "one ** x = x" by (simp add: assoc [symmetric] rcancel)
    1.54 +    }
    1.55 +    note lone = this
    1.56 +    {
    1.57 +      fix x
    1.58 +      have "inv(x) ** (x ** inv(x)) = one ** inv(x)"
    1.59 +	by (simp add: rinv lone rone)
    1.60 +      then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel)
    1.61 +    }
    1.62 +  qed (simp add: assoc)
    1.63 +
    1.64 +(* effect on printed locale *)
    1.65 +
    1.66 +print_locale! rgrp
    1.67 +print_locale! lgrp
    1.68 +
    1.69  end