# HG changeset patch # User ballarin # Date 1217839053 -7200 # Node ID 3a85bc6bfd739e32d2b3fd3aeafe761175438d0e # Parent 21bbd410ba0419d73330573af16b46bec2e7f1e0 Updated locale tests. diff -r 21bbd410ba04 -r 3a85bc6bfd73 src/FOL/ex/LocaleTest.thy --- a/src/FOL/ex/LocaleTest.thy Fri Aug 01 18:10:52 2008 +0200 +++ b/src/FOL/ex/LocaleTest.thy Mon Aug 04 10:37:33 2008 +0200 @@ -233,7 +233,7 @@ locale IG = fixes g assumes asm_G: "g --> x" notes asm_G2 = asm_G -interpretation i8: IG ["False"] by (rule IG.intro) fast +interpretation i8: IG ["False"] by unfold_locales fast thm i8.asm_G2 @@ -346,85 +346,6 @@ text {* Naming convention for global objects: prefixes R and r *} -locale Rsemi = var prod (infixl "**" 65) + - assumes assoc: "(x ** y) ** z = x ** (y ** z)" - -locale Rlgrp = Rsemi + var one + var inv + - assumes lone: "one ** x = x" - and linv: "inv(x) ** x = one" - -lemma (in Rlgrp) 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 - -locale Rrgrp = Rsemi + var one + var inv + - assumes rone: "x ** one = x" - and rinv: "x ** inv(x) = one" - -lemma (in Rrgrp) rcancel: - "y ** x = z ** x <-> y = z" -proof - assume "y ** x = z ** x" - then have "y ** (x ** inv(x)) = z ** (x ** inv(x))" - by (simp add: assoc [symmetric]) - then show "y = z" by (simp add: rone rinv) -qed simp - -interpretation Rlgrp < Rrgrp - proof - { - 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 - -(* effect on printed locale *) - -print_locale! Rlgrp - -(* use of derived theorem *) - -lemma (in Rlgrp) - "y ** x = z ** x <-> y = z" - apply (rule rcancel) - print_interps Rrgrp thm lcancel rcancel - done - -(* circular interpretation *) - -interpretation Rrgrp < Rlgrp - proof - { - 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 - -(* effect on printed locale *) - -print_locale! Rrgrp -print_locale! Rlgrp - (* locale with many parameters --- interpretations generate alternating group A5 *) @@ -486,16 +407,16 @@ .. -(* Group example revisited, with predicates *) +(* Group example *) -locale Rpsemi = var prod (infixl "**" 65) + +locale Rsemi = var prod (infixl "**" 65) + assumes assoc: "(x ** y) ** z = x ** (y ** z)" -locale Rplgrp = Rpsemi + var one + var inv + +locale Rlgrp = Rsemi + var one + var inv + assumes lone: "one ** x = x" and linv: "inv(x) ** x = one" -lemma (in Rplgrp) lcancel: +lemma (in Rlgrp) lcancel: "x ** y = x ** z <-> y = z" proof assume "x ** y = x ** z" @@ -503,11 +424,11 @@ then show "y = z" by (simp add: lone linv) qed simp -locale Rprgrp = Rpsemi + var one + var inv + +locale Rrgrp = Rsemi + var one + var inv + assumes rone: "x ** one = x" and rinv: "x ** inv(x) = one" -lemma (in Rprgrp) rcancel: +lemma (in Rrgrp) rcancel: "y ** x = z ** x <-> y = z" proof assume "y ** x = z ** x" @@ -516,7 +437,7 @@ then show "y = z" by (simp add: rone rinv) qed simp -interpretation Rplgrp < Rprgrp +interpretation Rlgrp < Rrgrp proof unfold_locales { fix x @@ -534,19 +455,19 @@ (* effect on printed locale *) -print_locale! Rplgrp +print_locale! Rlgrp (* use of derived theorem *) -lemma (in Rplgrp) +lemma (in Rlgrp) "y ** x = z ** x <-> y = z" apply (rule rcancel) - print_interps Rprgrp thm lcancel rcancel + print_interps Rrgrp thm lcancel rcancel done (* circular interpretation *) -interpretation Rprgrp < Rplgrp +interpretation Rrgrp < Rlgrp proof unfold_locales { fix x @@ -564,8 +485,8 @@ (* effect on printed locale *) -print_locale! Rprgrp -print_locale! Rplgrp +print_locale! Rrgrp +print_locale! Rlgrp subsection {* Interaction of Interpretation in Theories and Locales: in Locale, then in Theory *} @@ -643,7 +564,7 @@ then show "y = z" by (simp add: rone rinv) qed simp -interpretation Rqrgrp < Rprgrp +interpretation Rqrgrp < Rrgrp apply unfold_locales apply (rule assoc) apply (rule rone) @@ -660,7 +581,7 @@ print_interps Rqsemi print_interps Rqlgrp -print_interps Rplgrp (* no interpretations yet *) +print_interps Rlgrp (* no interpretations yet *) interpretation Rqlgrp < Rqrgrp @@ -680,9 +601,9 @@ qed print_interps! Rqrgrp -print_interps! Rpsemi (* witness must not have meta hyps *) -print_interps! Rprgrp (* witness must not have meta hyps *) -print_interps! Rplgrp (* witness must not have meta hyps *) +print_interps! Rsemi (* witness must not have meta hyps *) +print_interps! Rrgrp (* witness must not have meta hyps *) +print_interps! Rlgrp (* witness must not have meta hyps *) thm R2.rcancel thm R2.lcancel @@ -748,33 +669,29 @@ 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 +locale Rpair_semi = Rpair + Rsemi -interpretation Rpair_semi < Rpsemi prodP (infixl "***" 65) -proof (rule Rpsemi.intro) +interpretation Rpair_semi < Rsemi prodP (infixl "***" 65) +proof unfold_locales fix x y z show "(x *** y) *** z = x *** (y *** z)" apply (simp only: P_def) apply (simp add: assoc) (* FIXME: unfold P_def fails *) done qed -locale Rsemi_rev = Rpsemi + var rprod (infixl "++" 65) + +locale Rsemi_rev = Rsemi + 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) -(* -Test is obsolete. - 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 -*) subsection {* Import of Locales with Predicates as Interpretation *}