# HG changeset patch # User wenzelm # Date 1274958810 -7200 # Node ID 56e1b6976d0e2b43d531206eca005b363c83dec6 # Parent 8d231d3efcde7e0bdfe2c1d4f303bee8e9278acb# Parent 10ef4da1c314673919d05286a240615b505f394f merged diff -r 10ef4da1c314 -r 56e1b6976d0e src/FOL/IsaMakefile --- a/src/FOL/IsaMakefile Thu May 27 12:35:40 2010 +0200 +++ b/src/FOL/IsaMakefile Thu May 27 13:13:30 2010 +0200 @@ -46,7 +46,9 @@ $(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy ex/If.thy \ ex/Iff_Oracle.thy ex/Nat.thy ex/Nat_Class.thy ex/Natural_Numbers.thy \ - ex/LocaleTest.thy ex/Miniscope.thy ex/Prolog.thy ex/ROOT.ML \ + ex/Locale_Test/Locale_Test.thy ex/Locale_Test/Locale_Test1.thy \ + ex/Locale_Test/Locale_Test2.thy ex/Locale_Test/Locale_Test3.thy \ + ex/Miniscope.thy ex/Prolog.thy ex/ROOT.ML \ ex/Classical.thy ex/document/root.tex ex/Foundation.thy \ ex/Intuitionistic.thy ex/Intro.thy ex/Propositional_Int.thy \ ex/Propositional_Cla.thy ex/Quantifiers_Int.thy \ diff -r 10ef4da1c314 -r 56e1b6976d0e src/FOL/ex/LocaleTest.thy --- a/src/FOL/ex/LocaleTest.thy Thu May 27 12:35:40 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,712 +0,0 @@ -(* Title: FOL/ex/LocaleTest.thy - Author: Clemens Ballarin, TU Muenchen - -Test environment for the locale implementation. -*) - -theory LocaleTest -imports FOL -begin - -typedecl int arities int :: "term" -consts plus :: "int => int => int" (infixl "+" 60) - zero :: int ("0") - minus :: "int => int" ("- _") - -axioms - int_assoc: "(x + y::int) + z = x + (y + z)" - int_zero: "0 + x = x" - int_minus: "(-x) + x = 0" - int_minus2: "-(-x) = x" - -section {* Inference of parameter types *} - -locale param1 = fixes p -print_locale! param1 - -locale param2 = fixes p :: 'b -print_locale! param2 - -(* -locale param_top = param2 r for r :: "'b :: {}" - Fails, cannot generalise parameter. -*) - -locale param3 = fixes p (infix ".." 50) -print_locale! param3 - -locale param4 = fixes p :: "'a => 'a => 'a" (infix ".." 50) -print_locale! param4 - - -subsection {* Incremental type constraints *} - -locale constraint1 = - fixes prod (infixl "**" 65) - assumes l_id: "x ** y = x" - assumes assoc: "(x ** y) ** z = x ** (y ** z)" -print_locale! constraint1 - -locale constraint2 = - fixes p and q - assumes "p = q" -print_locale! constraint2 - - -section {* Inheritance *} - -locale semi = - fixes prod (infixl "**" 65) - assumes assoc: "(x ** y) ** z = x ** (y ** z)" -print_locale! semi thm semi_def - -locale lgrp = semi + - fixes one and inv - assumes lone: "one ** x = x" - and linv: "inv(x) ** x = one" -print_locale! lgrp thm lgrp_def lgrp_axioms_def - -locale add_lgrp = semi "op ++" for sum (infixl "++" 60) + - fixes zero and neg - assumes lzero: "zero ++ x = x" - and lneg: "neg(x) ++ x = zero" -print_locale! add_lgrp thm add_lgrp_def add_lgrp_axioms_def - -locale rev_lgrp = semi "%x y. y ++ x" for sum (infixl "++" 60) -print_locale! rev_lgrp thm rev_lgrp_def - -locale hom = f: semi f + g: semi g for f and g -print_locale! hom thm hom_def - -locale perturbation = semi + d: semi "%x y. delta(x) ** delta(y)" for delta -print_locale! perturbation thm perturbation_def - -locale pert_hom = d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2 -print_locale! pert_hom thm pert_hom_def - -text {* Alternative expression, obtaining nicer names in @{text "semi f"}. *} -locale pert_hom' = semi f + d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2 -print_locale! pert_hom' thm pert_hom'_def - - -section {* Syntax declarations *} - -locale logic = - fixes land (infixl "&&" 55) - and lnot ("-- _" [60] 60) - assumes assoc: "(x && y) && z = x && (y && z)" - and notnot: "-- (-- x) = x" -begin - -definition lor (infixl "||" 50) where - "x || y = --(-- x && -- y)" - -end -print_locale! logic - -locale use_decl = logic + semi "op ||" -print_locale! use_decl thm use_decl_def - -locale extra_type = - fixes a :: 'a - and P :: "'a => 'b => o" -begin - -definition test :: "'a => o" where - "test(x) <-> (ALL b. P(x, b))" - -end - -term extra_type.test thm extra_type.test_def - -interpretation var?: extra_type "0" "%x y. x = 0" . - -thm var.test_def - - -text {* Under which circumstances term syntax remains active. *} - -locale "syntax" = - fixes p1 :: "'a => 'b" - and p2 :: "'b => o" -begin - -definition d1 :: "'a => o" where "d1(x) <-> ~ p2(p1(x))" -definition d2 :: "'b => o" where "d2(x) <-> ~ p2(x)" - -thm d1_def d2_def - -end - -thm syntax.d1_def syntax.d2_def - -locale syntax' = "syntax" p1 p2 for p1 :: "'a => 'a" and p2 :: "'a => o" -begin - -thm d1_def d2_def (* should print as "d1(?x) <-> ..." and "d2(?x) <-> ..." *) - -ML {* - fun check_syntax ctxt thm expected = - let - val obtained = PrintMode.setmp [] (Display.string_of_thm ctxt) thm; - in - if obtained <> expected - then error ("Theorem syntax '" ^ obtained ^ "' obtained, but '" ^ expected ^ "' expected.") - else () - end; -*} - -ML {* - check_syntax @{context} @{thm d1_def} "d1(?x) <-> ~ p2(p1(?x))"; - check_syntax @{context} @{thm d2_def} "d2(?x) <-> ~ p2(?x)"; -*} - -end - -locale syntax'' = "syntax" p3 p2 for p3 :: "'a => 'b" and p2 :: "'b => o" -begin - -thm d1_def d2_def - (* should print as "syntax.d1(p3, p2, ?x) <-> ..." and "d2(?x) <-> ..." *) - -ML {* - check_syntax @{context} @{thm d1_def} "syntax.d1(p3, p2, ?x) <-> ~ p2(p3(?x))"; - check_syntax @{context} @{thm d2_def} "d2(?x) <-> ~ p2(?x)"; -*} - -end - - -section {* Foundational versions of theorems *} - -thm logic.assoc -thm logic.lor_def - - -section {* Defines *} - -locale logic_def = - fixes land (infixl "&&" 55) - and lor (infixl "||" 50) - and lnot ("-- _" [60] 60) - assumes assoc: "(x && y) && z = x && (y && z)" - and notnot: "-- (-- x) = x" - defines "x || y == --(-- x && -- y)" -begin - -thm lor_def - -lemma "x || y = --(-- x && --y)" - by (unfold lor_def) (rule refl) - -end - -(* Inheritance of defines *) - -locale logic_def2 = logic_def -begin - -lemma "x || y = --(-- x && --y)" - by (unfold lor_def) (rule refl) - -end - - -section {* Notes *} - -(* A somewhat arcane homomorphism example *) - -definition semi_hom where - "semi_hom(prod, sum, h) <-> (ALL x y. h(prod(x, y)) = sum(h(x), h(y)))" - -lemma semi_hom_mult: - "semi_hom(prod, sum, h) ==> h(prod(x, y)) = sum(h(x), h(y))" - by (simp add: semi_hom_def) - -locale semi_hom_loc = prod: semi prod + sum: semi sum - for prod and sum and h + - assumes semi_homh: "semi_hom(prod, sum, h)" - notes semi_hom_mult = semi_hom_mult [OF semi_homh] - -thm semi_hom_loc.semi_hom_mult -(* unspecified, attribute not applied in backgroud theory !!! *) - -lemma (in semi_hom_loc) "h(prod(x, y)) = sum(h(x), h(y))" - by (rule semi_hom_mult) - -(* Referring to facts from within a context specification *) - -lemma - assumes x: "P <-> P" - notes y = x - shows True .. - - -section {* Theorem statements *} - -lemma (in lgrp) 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 -print_locale! lgrp - - -locale rgrp = semi + - fixes one and inv - assumes rone: "x ** one = x" - and rinv: "x ** inv(x) = one" -begin - -lemma 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 - -end -print_locale! rgrp - - -subsection {* Patterns *} - -lemma (in rgrp) - assumes "y ** x = z ** x" (is ?a) - shows "y = z" (is ?t) -proof - - txt {* Weird proof involving patterns from context element and conclusion. *} - { - assume ?a - then have "y ** (x ** inv(x)) = z ** (x ** inv(x))" - by (simp add: assoc [symmetric]) - then have ?t by (simp add: rone rinv) - } - note x = this - show ?t by (rule x [OF `?a`]) -qed - - -section {* Interpretation between locales: sublocales *} - -sublocale lgrp < right: rgrp -print_facts -proof unfold_locales - { - 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! 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 unfold_locales - { - 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! rgrp -print_locale! lgrp - - -(* Duality *) - -locale order = - fixes less :: "'a => 'a => o" (infix "<<" 50) - assumes refl: "x << x" - and trans: "[| x << y; y << z |] ==> x << z" - -sublocale order < dual: order "%x y. y << x" - apply unfold_locales apply (rule refl) apply (blast intro: trans) - done - -print_locale! order (* Only two instances of order. *) - -locale order' = - fixes less :: "'a => 'a => o" (infix "<<" 50) - assumes refl: "x << x" - and trans: "[| x << y; y << z |] ==> x << z" - -locale order_with_def = order' -begin - -definition greater :: "'a => 'a => o" (infix ">>" 50) where - "x >> y <-> y << x" - -end - -sublocale order_with_def < dual: order' "op >>" - apply unfold_locales - unfolding greater_def - apply (rule refl) apply (blast intro: trans) - done - -print_locale! order_with_def -(* Note that decls come after theorems that make use of them. *) - - -(* locale with many parameters --- - interpretations generate alternating group A5 *) - - -locale A5 = - fixes A and B and C and D and E - assumes eq: "A <-> B <-> C <-> D <-> E" - -sublocale A5 < 1: A5 _ _ D E C -print_facts - using eq apply (blast intro: A5.intro) done - -sublocale A5 < 2: A5 C _ E _ A -print_facts - using eq apply (blast intro: A5.intro) done - -sublocale A5 < 3: A5 B C A _ _ -print_facts - using eq apply (blast intro: A5.intro) done - -(* Any even permutation of parameters is subsumed by the above. *) - -print_locale! A5 - - -(* Free arguments of instance *) - -locale trivial = - fixes P and Q :: o - assumes Q: "P <-> P <-> Q" -begin - -lemma Q_triv: "Q" using Q by fast - -end - -sublocale trivial < x: trivial x _ - apply unfold_locales using Q by fast - -print_locale! trivial - -context trivial begin thm x.Q [where ?x = True] end - -sublocale trivial < y: trivial Q Q - by unfold_locales - (* Succeeds since previous interpretation is more general. *) - -print_locale! trivial (* No instance for y created (subsumed). *) - - -subsection {* Sublocale, then interpretation in theory *} - -interpretation int?: lgrp "op +" "0" "minus" -proof unfold_locales -qed (rule int_assoc int_zero int_minus)+ - -thm int.assoc int.semi_axioms - -interpretation int2?: semi "op +" - by unfold_locales (* subsumed, thm int2.assoc not generated *) - -ML {* (PureThy.get_thms @{theory} "int2.assoc"; - error "thm int2.assoc was generated") - handle ERROR "Unknown fact \"int2.assoc\"" => ([]:thm list); *} - -thm int.lone int.right.rone - (* the latter comes through the sublocale relation *) - - -subsection {* Interpretation in theory, then sublocale *} - -interpretation fol: logic "op +" "minus" - by unfold_locales (rule int_assoc int_minus2)+ - -locale logic2 = - fixes land (infixl "&&" 55) - and lnot ("-- _" [60] 60) - assumes assoc: "(x && y) && z = x && (y && z)" - and notnot: "-- (-- x) = x" -begin - -definition lor (infixl "||" 50) where - "x || y = --(-- x && -- y)" - -end - -sublocale logic < two: logic2 - by unfold_locales (rule assoc notnot)+ - -thm fol.two.assoc - - -subsection {* Declarations and sublocale *} - -locale logic_a = logic -locale logic_b = logic - -sublocale logic_a < logic_b - by unfold_locales - - -subsection {* Equations *} - -locale logic_o = - fixes land (infixl "&&" 55) - and lnot ("-- _" [60] 60) - assumes assoc_o: "(x && y) && z <-> x && (y && z)" - and notnot_o: "-- (-- x) <-> x" -begin - -definition lor_o (infixl "||" 50) where - "x || y <-> --(-- x && -- y)" - -end - -interpretation x: logic_o "op &" "Not" - where bool_logic_o: "logic_o.lor_o(op &, Not, x, y) <-> x | y" -proof - - show bool_logic_o: "PROP logic_o(op &, Not)" by unfold_locales fast+ - show "logic_o.lor_o(op &, Not, x, y) <-> x | y" - by (unfold logic_o.lor_o_def [OF bool_logic_o]) fast -qed - -thm x.lor_o_def bool_logic_o - -lemma lor_triv: "z <-> z" .. - -lemma (in logic_o) lor_triv: "x || y <-> x || y" by fast - -thm lor_triv [where z = True] (* Check strict prefix. *) - x.lor_triv - - -subsection {* Inheritance of mixins *} - -locale reflexive = - fixes le :: "'a => 'a => o" (infix "\" 50) - assumes refl: "x \ x" -begin - -definition less (infix "\" 50) where "x \ y <-> x \ y & x ~= y" - -end - -consts - gle :: "'a => 'a => o" gless :: "'a => 'a => o" - gle' :: "'a => 'a => o" gless' :: "'a => 'a => o" - -axioms - grefl: "gle(x, x)" gless_def: "gless(x, y) <-> gle(x, y) & x ~= y" - grefl': "gle'(x, x)" gless'_def: "gless'(x, y) <-> gle'(x, y) & x ~= y" - -text {* Setup *} - -locale mixin = reflexive -begin -lemmas less_thm = less_def -end - -interpretation le: mixin gle where "reflexive.less(gle, x, y) <-> gless(x, y)" -proof - - show "mixin(gle)" by unfold_locales (rule grefl) - note reflexive = this[unfolded mixin_def] - show "reflexive.less(gle, x, y) <-> gless(x, y)" - by (simp add: reflexive.less_def[OF reflexive] gless_def) -qed - -text {* Mixin propagated along the locale hierarchy *} - -locale mixin2 = mixin -begin -lemmas less_thm2 = less_def -end - -interpretation le: mixin2 gle - by unfold_locales - -thm le.less_thm2 (* mixin applied *) -lemma "gless(x, y) <-> gle(x, y) & x ~= y" - by (rule le.less_thm2) - -text {* Mixin does not leak to a side branch. *} - -locale mixin3 = reflexive -begin -lemmas less_thm3 = less_def -end - -interpretation le: mixin3 gle - by unfold_locales - -thm le.less_thm3 (* mixin not applied *) -lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y" by (rule le.less_thm3) - -text {* Mixin only available in original context *} - -locale mixin4_base = reflexive - -locale mixin4_mixin = mixin4_base - -interpretation le: mixin4_mixin gle - where "reflexive.less(gle, x, y) <-> gless(x, y)" -proof - - show "mixin4_mixin(gle)" by unfold_locales (rule grefl) - note reflexive = this[unfolded mixin4_mixin_def mixin4_base_def mixin_def] - show "reflexive.less(gle, x, y) <-> gless(x, y)" - by (simp add: reflexive.less_def[OF reflexive] gless_def) -qed - -locale mixin4_copy = mixin4_base -begin -lemmas less_thm4 = less_def -end - -locale mixin4_combined = le1: mixin4_mixin le' + le2: mixin4_copy le for le' le -begin -lemmas less_thm4' = less_def -end - -interpretation le4: mixin4_combined gle' gle - by unfold_locales (rule grefl') - -thm le4.less_thm4' (* mixin not applied *) -lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y" - by (rule le4.less_thm4') - -text {* Inherited mixin applied to new theorem *} - -locale mixin5_base = reflexive - -locale mixin5_inherited = mixin5_base - -interpretation le5: mixin5_base gle - where "reflexive.less(gle, x, y) <-> gless(x, y)" -proof - - show "mixin5_base(gle)" by unfold_locales - note reflexive = this[unfolded mixin5_base_def mixin_def] - show "reflexive.less(gle, x, y) <-> gless(x, y)" - by (simp add: reflexive.less_def[OF reflexive] gless_def) -qed - -interpretation le5: mixin5_inherited gle - by unfold_locales - -lemmas (in mixin5_inherited) less_thm5 = less_def - -thm le5.less_thm5 (* mixin applied *) -lemma "gless(x, y) <-> gle(x, y) & x ~= y" - by (rule le5.less_thm5) - -text {* Mixin pushed down to existing inherited locale *} - -locale mixin6_base = reflexive - -locale mixin6_inherited = mixin5_base - -interpretation le6: mixin6_base gle - by unfold_locales -interpretation le6: mixin6_inherited gle - by unfold_locales -interpretation le6: mixin6_base gle - where "reflexive.less(gle, x, y) <-> gless(x, y)" -proof - - show "mixin6_base(gle)" by unfold_locales - note reflexive = this[unfolded mixin6_base_def mixin_def] - show "reflexive.less(gle, x, y) <-> gless(x, y)" - by (simp add: reflexive.less_def[OF reflexive] gless_def) -qed - -lemmas (in mixin6_inherited) less_thm6 = less_def - -thm le6.less_thm6 (* mixin applied *) -lemma "gless(x, y) <-> gle(x, y) & x ~= y" - by (rule le6.less_thm6) - -text {* Existing mixin inherited through sublocale relation *} - -locale mixin7_base = reflexive - -locale mixin7_inherited = reflexive - -interpretation le7: mixin7_base gle - where "reflexive.less(gle, x, y) <-> gless(x, y)" -proof - - show "mixin7_base(gle)" by unfold_locales - note reflexive = this[unfolded mixin7_base_def mixin_def] - show "reflexive.less(gle, x, y) <-> gless(x, y)" - by (simp add: reflexive.less_def[OF reflexive] gless_def) -qed - -interpretation le7: mixin7_inherited gle - by unfold_locales - -lemmas (in mixin7_inherited) less_thm7 = less_def - -thm le7.less_thm7 (* before, mixin not applied *) -lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y" - by (rule le7.less_thm7) - -sublocale mixin7_inherited < mixin7_base - by unfold_locales - -lemmas (in mixin7_inherited) less_thm7b = less_def - -thm le7.less_thm7b (* after, mixin applied *) -lemma "gless(x, y) <-> gle(x, y) & x ~= y" - by (rule le7.less_thm7b) - - -subsection {* Interpretation in proofs *} - -lemma True -proof - interpret "local": lgrp "op +" "0" "minus" - by unfold_locales (* subsumed *) - { - fix zero :: int - assume "!!x. zero + x = x" "!!x. (-x) + x = zero" - then interpret local_fixed: lgrp "op +" zero "minus" - by unfold_locales - thm local_fixed.lone - } - assume "!!x zero. zero + x = x" "!!x zero. (-x) + x = zero" - then interpret local_free: lgrp "op +" zero "minus" for zero - by unfold_locales - thm local_free.lone [where ?zero = 0] -qed - -end diff -r 10ef4da1c314 -r 56e1b6976d0e src/FOL/ex/Locale_Test/Locale_Test.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/FOL/ex/Locale_Test/Locale_Test.thy Thu May 27 13:13:30 2010 +0200 @@ -0,0 +1,24 @@ +(* Title: FOL/ex/Locale_Test/Locale_Test.thy + Author: Clemens Ballarin + +Test environment for the locale implementation. +*) + +theory Locale_Test +imports Locale_Test1 Locale_Test2 Locale_Test3 +begin + +text {* Result of theory merge with distinct but identical interpretations *} + +context mixin_thy_merge +begin +lemmas less_mixin_thy_merge1 = le.less_def +lemmas less_mixin_thy_merge2 = le'.less_def +end + +lemma "gless(x, y) <-> gle(x, y) & x ~= y" (* mixin from first interpretation applied *) + by (rule le1.less_mixin_thy_merge1) +lemma "gless'(x, y) <-> gle'(x, y) & x ~= y" (* mixin from second interpretation applied *) + by (rule le1.less_mixin_thy_merge2) + +end diff -r 10ef4da1c314 -r 56e1b6976d0e src/FOL/ex/Locale_Test/Locale_Test1.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Thu May 27 13:13:30 2010 +0200 @@ -0,0 +1,717 @@ +(* Title: FOL/ex/Locale_Test/Locale_Test1.thy + Author: Clemens Ballarin, TU Muenchen + +Test environment for the locale implementation. +*) + +theory Locale_Test1 +imports FOL +begin + +typedecl int arities int :: "term" +consts plus :: "int => int => int" (infixl "+" 60) + zero :: int ("0") + minus :: "int => int" ("- _") + +axioms + int_assoc: "(x + y::int) + z = x + (y + z)" + int_zero: "0 + x = x" + int_minus: "(-x) + x = 0" + int_minus2: "-(-x) = x" + +section {* Inference of parameter types *} + +locale param1 = fixes p +print_locale! param1 + +locale param2 = fixes p :: 'b +print_locale! param2 + +(* +locale param_top = param2 r for r :: "'b :: {}" + Fails, cannot generalise parameter. +*) + +locale param3 = fixes p (infix ".." 50) +print_locale! param3 + +locale param4 = fixes p :: "'a => 'a => 'a" (infix ".." 50) +print_locale! param4 + + +subsection {* Incremental type constraints *} + +locale constraint1 = + fixes prod (infixl "**" 65) + assumes l_id: "x ** y = x" + assumes assoc: "(x ** y) ** z = x ** (y ** z)" +print_locale! constraint1 + +locale constraint2 = + fixes p and q + assumes "p = q" +print_locale! constraint2 + + +section {* Inheritance *} + +locale semi = + fixes prod (infixl "**" 65) + assumes assoc: "(x ** y) ** z = x ** (y ** z)" +print_locale! semi thm semi_def + +locale lgrp = semi + + fixes one and inv + assumes lone: "one ** x = x" + and linv: "inv(x) ** x = one" +print_locale! lgrp thm lgrp_def lgrp_axioms_def + +locale add_lgrp = semi "op ++" for sum (infixl "++" 60) + + fixes zero and neg + assumes lzero: "zero ++ x = x" + and lneg: "neg(x) ++ x = zero" +print_locale! add_lgrp thm add_lgrp_def add_lgrp_axioms_def + +locale rev_lgrp = semi "%x y. y ++ x" for sum (infixl "++" 60) +print_locale! rev_lgrp thm rev_lgrp_def + +locale hom = f: semi f + g: semi g for f and g +print_locale! hom thm hom_def + +locale perturbation = semi + d: semi "%x y. delta(x) ** delta(y)" for delta +print_locale! perturbation thm perturbation_def + +locale pert_hom = d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2 +print_locale! pert_hom thm pert_hom_def + +text {* Alternative expression, obtaining nicer names in @{text "semi f"}. *} +locale pert_hom' = semi f + d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2 +print_locale! pert_hom' thm pert_hom'_def + + +section {* Syntax declarations *} + +locale logic = + fixes land (infixl "&&" 55) + and lnot ("-- _" [60] 60) + assumes assoc: "(x && y) && z = x && (y && z)" + and notnot: "-- (-- x) = x" +begin + +definition lor (infixl "||" 50) where + "x || y = --(-- x && -- y)" + +end +print_locale! logic + +locale use_decl = logic + semi "op ||" +print_locale! use_decl thm use_decl_def + +locale extra_type = + fixes a :: 'a + and P :: "'a => 'b => o" +begin + +definition test :: "'a => o" where + "test(x) <-> (ALL b. P(x, b))" + +end + +term extra_type.test thm extra_type.test_def + +interpretation var?: extra_type "0" "%x y. x = 0" . + +thm var.test_def + + +text {* Under which circumstances term syntax remains active. *} + +locale "syntax" = + fixes p1 :: "'a => 'b" + and p2 :: "'b => o" +begin + +definition d1 :: "'a => o" where "d1(x) <-> ~ p2(p1(x))" +definition d2 :: "'b => o" where "d2(x) <-> ~ p2(x)" + +thm d1_def d2_def + +end + +thm syntax.d1_def syntax.d2_def + +locale syntax' = "syntax" p1 p2 for p1 :: "'a => 'a" and p2 :: "'a => o" +begin + +thm d1_def d2_def (* should print as "d1(?x) <-> ..." and "d2(?x) <-> ..." *) + +ML {* + fun check_syntax ctxt thm expected = + let + val obtained = PrintMode.setmp [] (Display.string_of_thm ctxt) thm; + in + if obtained <> expected + then error ("Theorem syntax '" ^ obtained ^ "' obtained, but '" ^ expected ^ "' expected.") + else () + end; +*} + +ML {* + check_syntax @{context} @{thm d1_def} "d1(?x) <-> ~ p2(p1(?x))"; + check_syntax @{context} @{thm d2_def} "d2(?x) <-> ~ p2(?x)"; +*} + +end + +locale syntax'' = "syntax" p3 p2 for p3 :: "'a => 'b" and p2 :: "'b => o" +begin + +thm d1_def d2_def + (* should print as "syntax.d1(p3, p2, ?x) <-> ..." and "d2(?x) <-> ..." *) + +ML {* + check_syntax @{context} @{thm d1_def} "syntax.d1(p3, p2, ?x) <-> ~ p2(p3(?x))"; + check_syntax @{context} @{thm d2_def} "d2(?x) <-> ~ p2(?x)"; +*} + +end + + +section {* Foundational versions of theorems *} + +thm logic.assoc +thm logic.lor_def + + +section {* Defines *} + +locale logic_def = + fixes land (infixl "&&" 55) + and lor (infixl "||" 50) + and lnot ("-- _" [60] 60) + assumes assoc: "(x && y) && z = x && (y && z)" + and notnot: "-- (-- x) = x" + defines "x || y == --(-- x && -- y)" +begin + +thm lor_def + +lemma "x || y = --(-- x && --y)" + by (unfold lor_def) (rule refl) + +end + +(* Inheritance of defines *) + +locale logic_def2 = logic_def +begin + +lemma "x || y = --(-- x && --y)" + by (unfold lor_def) (rule refl) + +end + + +section {* Notes *} + +(* A somewhat arcane homomorphism example *) + +definition semi_hom where + "semi_hom(prod, sum, h) <-> (ALL x y. h(prod(x, y)) = sum(h(x), h(y)))" + +lemma semi_hom_mult: + "semi_hom(prod, sum, h) ==> h(prod(x, y)) = sum(h(x), h(y))" + by (simp add: semi_hom_def) + +locale semi_hom_loc = prod: semi prod + sum: semi sum + for prod and sum and h + + assumes semi_homh: "semi_hom(prod, sum, h)" + notes semi_hom_mult = semi_hom_mult [OF semi_homh] + +thm semi_hom_loc.semi_hom_mult +(* unspecified, attribute not applied in backgroud theory !!! *) + +lemma (in semi_hom_loc) "h(prod(x, y)) = sum(h(x), h(y))" + by (rule semi_hom_mult) + +(* Referring to facts from within a context specification *) + +lemma + assumes x: "P <-> P" + notes y = x + shows True .. + + +section {* Theorem statements *} + +lemma (in lgrp) 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 +print_locale! lgrp + + +locale rgrp = semi + + fixes one and inv + assumes rone: "x ** one = x" + and rinv: "x ** inv(x) = one" +begin + +lemma 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 + +end +print_locale! rgrp + + +subsection {* Patterns *} + +lemma (in rgrp) + assumes "y ** x = z ** x" (is ?a) + shows "y = z" (is ?t) +proof - + txt {* Weird proof involving patterns from context element and conclusion. *} + { + assume ?a + then have "y ** (x ** inv(x)) = z ** (x ** inv(x))" + by (simp add: assoc [symmetric]) + then have ?t by (simp add: rone rinv) + } + note x = this + show ?t by (rule x [OF `?a`]) +qed + + +section {* Interpretation between locales: sublocales *} + +sublocale lgrp < right: rgrp +print_facts +proof unfold_locales + { + 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! 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 unfold_locales + { + 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! rgrp +print_locale! lgrp + + +(* Duality *) + +locale order = + fixes less :: "'a => 'a => o" (infix "<<" 50) + assumes refl: "x << x" + and trans: "[| x << y; y << z |] ==> x << z" + +sublocale order < dual: order "%x y. y << x" + apply unfold_locales apply (rule refl) apply (blast intro: trans) + done + +print_locale! order (* Only two instances of order. *) + +locale order' = + fixes less :: "'a => 'a => o" (infix "<<" 50) + assumes refl: "x << x" + and trans: "[| x << y; y << z |] ==> x << z" + +locale order_with_def = order' +begin + +definition greater :: "'a => 'a => o" (infix ">>" 50) where + "x >> y <-> y << x" + +end + +sublocale order_with_def < dual: order' "op >>" + apply unfold_locales + unfolding greater_def + apply (rule refl) apply (blast intro: trans) + done + +print_locale! order_with_def +(* Note that decls come after theorems that make use of them. *) + + +(* locale with many parameters --- + interpretations generate alternating group A5 *) + + +locale A5 = + fixes A and B and C and D and E + assumes eq: "A <-> B <-> C <-> D <-> E" + +sublocale A5 < 1: A5 _ _ D E C +print_facts + using eq apply (blast intro: A5.intro) done + +sublocale A5 < 2: A5 C _ E _ A +print_facts + using eq apply (blast intro: A5.intro) done + +sublocale A5 < 3: A5 B C A _ _ +print_facts + using eq apply (blast intro: A5.intro) done + +(* Any even permutation of parameters is subsumed by the above. *) + +print_locale! A5 + + +(* Free arguments of instance *) + +locale trivial = + fixes P and Q :: o + assumes Q: "P <-> P <-> Q" +begin + +lemma Q_triv: "Q" using Q by fast + +end + +sublocale trivial < x: trivial x _ + apply unfold_locales using Q by fast + +print_locale! trivial + +context trivial begin thm x.Q [where ?x = True] end + +sublocale trivial < y: trivial Q Q + by unfold_locales + (* Succeeds since previous interpretation is more general. *) + +print_locale! trivial (* No instance for y created (subsumed). *) + + +subsection {* Sublocale, then interpretation in theory *} + +interpretation int?: lgrp "op +" "0" "minus" +proof unfold_locales +qed (rule int_assoc int_zero int_minus)+ + +thm int.assoc int.semi_axioms + +interpretation int2?: semi "op +" + by unfold_locales (* subsumed, thm int2.assoc not generated *) + +ML {* (PureThy.get_thms @{theory} "int2.assoc"; + error "thm int2.assoc was generated") + handle ERROR "Unknown fact \"int2.assoc\"" => ([]:thm list); *} + +thm int.lone int.right.rone + (* the latter comes through the sublocale relation *) + + +subsection {* Interpretation in theory, then sublocale *} + +interpretation fol: logic "op +" "minus" + by unfold_locales (rule int_assoc int_minus2)+ + +locale logic2 = + fixes land (infixl "&&" 55) + and lnot ("-- _" [60] 60) + assumes assoc: "(x && y) && z = x && (y && z)" + and notnot: "-- (-- x) = x" +begin + +definition lor (infixl "||" 50) where + "x || y = --(-- x && -- y)" + +end + +sublocale logic < two: logic2 + by unfold_locales (rule assoc notnot)+ + +thm fol.two.assoc + + +subsection {* Declarations and sublocale *} + +locale logic_a = logic +locale logic_b = logic + +sublocale logic_a < logic_b + by unfold_locales + + +subsection {* Equations *} + +locale logic_o = + fixes land (infixl "&&" 55) + and lnot ("-- _" [60] 60) + assumes assoc_o: "(x && y) && z <-> x && (y && z)" + and notnot_o: "-- (-- x) <-> x" +begin + +definition lor_o (infixl "||" 50) where + "x || y <-> --(-- x && -- y)" + +end + +interpretation x: logic_o "op &" "Not" + where bool_logic_o: "logic_o.lor_o(op &, Not, x, y) <-> x | y" +proof - + show bool_logic_o: "PROP logic_o(op &, Not)" by unfold_locales fast+ + show "logic_o.lor_o(op &, Not, x, y) <-> x | y" + by (unfold logic_o.lor_o_def [OF bool_logic_o]) fast +qed + +thm x.lor_o_def bool_logic_o + +lemma lor_triv: "z <-> z" .. + +lemma (in logic_o) lor_triv: "x || y <-> x || y" by fast + +thm lor_triv [where z = True] (* Check strict prefix. *) + x.lor_triv + + +subsection {* Inheritance of mixins *} + +locale reflexive = + fixes le :: "'a => 'a => o" (infix "\" 50) + assumes refl: "x \ x" +begin + +definition less (infix "\" 50) where "x \ y <-> x \ y & x ~= y" + +end + +consts + gle :: "'a => 'a => o" gless :: "'a => 'a => o" + gle' :: "'a => 'a => o" gless' :: "'a => 'a => o" + +axioms + grefl: "gle(x, x)" gless_def: "gless(x, y) <-> gle(x, y) & x ~= y" + grefl': "gle'(x, x)" gless'_def: "gless'(x, y) <-> gle'(x, y) & x ~= y" + +text {* Setup *} + +locale mixin = reflexive +begin +lemmas less_thm = less_def +end + +interpretation le: mixin gle where "reflexive.less(gle, x, y) <-> gless(x, y)" +proof - + show "mixin(gle)" by unfold_locales (rule grefl) + note reflexive = this[unfolded mixin_def] + show "reflexive.less(gle, x, y) <-> gless(x, y)" + by (simp add: reflexive.less_def[OF reflexive] gless_def) +qed + +text {* Mixin propagated along the locale hierarchy *} + +locale mixin2 = mixin +begin +lemmas less_thm2 = less_def +end + +interpretation le: mixin2 gle + by unfold_locales + +thm le.less_thm2 (* mixin applied *) +lemma "gless(x, y) <-> gle(x, y) & x ~= y" + by (rule le.less_thm2) + +text {* Mixin does not leak to a side branch. *} + +locale mixin3 = reflexive +begin +lemmas less_thm3 = less_def +end + +interpretation le: mixin3 gle + by unfold_locales + +thm le.less_thm3 (* mixin not applied *) +lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y" by (rule le.less_thm3) + +text {* Mixin only available in original context *} + +locale mixin4_base = reflexive + +locale mixin4_mixin = mixin4_base + +interpretation le: mixin4_mixin gle + where "reflexive.less(gle, x, y) <-> gless(x, y)" +proof - + show "mixin4_mixin(gle)" by unfold_locales (rule grefl) + note reflexive = this[unfolded mixin4_mixin_def mixin4_base_def mixin_def] + show "reflexive.less(gle, x, y) <-> gless(x, y)" + by (simp add: reflexive.less_def[OF reflexive] gless_def) +qed + +locale mixin4_copy = mixin4_base +begin +lemmas less_thm4 = less_def +end + +locale mixin4_combined = le1: mixin4_mixin le' + le2: mixin4_copy le for le' le +begin +lemmas less_thm4' = less_def +end + +interpretation le4: mixin4_combined gle' gle + by unfold_locales (rule grefl') + +thm le4.less_thm4' (* mixin not applied *) +lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y" + by (rule le4.less_thm4') + +text {* Inherited mixin applied to new theorem *} + +locale mixin5_base = reflexive + +locale mixin5_inherited = mixin5_base + +interpretation le5: mixin5_base gle + where "reflexive.less(gle, x, y) <-> gless(x, y)" +proof - + show "mixin5_base(gle)" by unfold_locales + note reflexive = this[unfolded mixin5_base_def mixin_def] + show "reflexive.less(gle, x, y) <-> gless(x, y)" + by (simp add: reflexive.less_def[OF reflexive] gless_def) +qed + +interpretation le5: mixin5_inherited gle + by unfold_locales + +lemmas (in mixin5_inherited) less_thm5 = less_def + +thm le5.less_thm5 (* mixin applied *) +lemma "gless(x, y) <-> gle(x, y) & x ~= y" + by (rule le5.less_thm5) + +text {* Mixin pushed down to existing inherited locale *} + +locale mixin6_base = reflexive + +locale mixin6_inherited = mixin5_base + +interpretation le6: mixin6_base gle + by unfold_locales +interpretation le6: mixin6_inherited gle + by unfold_locales +interpretation le6: mixin6_base gle + where "reflexive.less(gle, x, y) <-> gless(x, y)" +proof - + show "mixin6_base(gle)" by unfold_locales + note reflexive = this[unfolded mixin6_base_def mixin_def] + show "reflexive.less(gle, x, y) <-> gless(x, y)" + by (simp add: reflexive.less_def[OF reflexive] gless_def) +qed + +lemmas (in mixin6_inherited) less_thm6 = less_def + +thm le6.less_thm6 (* mixin applied *) +lemma "gless(x, y) <-> gle(x, y) & x ~= y" + by (rule le6.less_thm6) + +text {* Existing mixin inherited through sublocale relation *} + +locale mixin7_base = reflexive + +locale mixin7_inherited = reflexive + +interpretation le7: mixin7_base gle + where "reflexive.less(gle, x, y) <-> gless(x, y)" +proof - + show "mixin7_base(gle)" by unfold_locales + note reflexive = this[unfolded mixin7_base_def mixin_def] + show "reflexive.less(gle, x, y) <-> gless(x, y)" + by (simp add: reflexive.less_def[OF reflexive] gless_def) +qed + +interpretation le7: mixin7_inherited gle + by unfold_locales + +lemmas (in mixin7_inherited) less_thm7 = less_def + +thm le7.less_thm7 (* before, mixin not applied *) +lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y" + by (rule le7.less_thm7) + +sublocale mixin7_inherited < mixin7_base + by unfold_locales + +lemmas (in mixin7_inherited) less_thm7b = less_def + +thm le7.less_thm7b (* after, mixin applied *) +lemma "gless(x, y) <-> gle(x, y) & x ~= y" + by (rule le7.less_thm7b) + + +text {* This locale will be interpreted in later theories. *} + +locale mixin_thy_merge = le: reflexive le + le': reflexive le' for le le' + + +subsection {* Interpretation in proofs *} + +lemma True +proof + interpret "local": lgrp "op +" "0" "minus" + by unfold_locales (* subsumed *) + { + fix zero :: int + assume "!!x. zero + x = x" "!!x. (-x) + x = zero" + then interpret local_fixed: lgrp "op +" zero "minus" + by unfold_locales + thm local_fixed.lone + } + assume "!!x zero. zero + x = x" "!!x zero. (-x) + x = zero" + then interpret local_free: lgrp "op +" zero "minus" for zero + by unfold_locales + thm local_free.lone [where ?zero = 0] +qed + +end diff -r 10ef4da1c314 -r 56e1b6976d0e src/FOL/ex/Locale_Test/Locale_Test2.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/FOL/ex/Locale_Test/Locale_Test2.thy Thu May 27 13:13:30 2010 +0200 @@ -0,0 +1,20 @@ +(* Title: FOL/ex/Locale_Test/Locale_Test2.thy + Author: Clemens Ballarin, TU Muenchen + +Test environment for the locale implementation. +*) + +theory Locale_Test2 +imports Locale_Test1 +begin + +interpretation le1: mixin_thy_merge gle gle' + where "reflexive.less(gle, x, y) <-> gless(x, y)" +proof - + show "mixin_thy_merge(gle, gle')" by unfold_locales + note reflexive = this[unfolded mixin_thy_merge_def, THEN conjunct1] + show "reflexive.less(gle, x, y) <-> gless(x, y)" + by (simp add: reflexive.less_def[OF reflexive] gless_def) +qed + +end diff -r 10ef4da1c314 -r 56e1b6976d0e src/FOL/ex/Locale_Test/Locale_Test3.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/FOL/ex/Locale_Test/Locale_Test3.thy Thu May 27 13:13:30 2010 +0200 @@ -0,0 +1,20 @@ +(* Title: FOL/ex/Locale_Test/Locale_Test3.thy + Author: Clemens Ballarin + +Test environment for the locale implementation. +*) + +theory Locale_Test3 +imports Locale_Test1 +begin + +interpretation le2: mixin_thy_merge gle gle' + where "reflexive.less(gle', x, y) <-> gless'(x, y)" +proof - + show "mixin_thy_merge(gle, gle')" by unfold_locales + note reflexive = this[unfolded mixin_thy_merge_def, THEN conjunct2] + show "reflexive.less(gle', x, y) <-> gless'(x, y)" + by (simp add: reflexive.less_def[OF reflexive] gless'_def) +qed + +end diff -r 10ef4da1c314 -r 56e1b6976d0e src/FOL/ex/ROOT.ML --- a/src/FOL/ex/ROOT.ML Thu May 27 12:35:40 2010 +0200 +++ b/src/FOL/ex/ROOT.ML Thu May 27 13:13:30 2010 +0200 @@ -23,4 +23,4 @@ ]; (*regression test for locales -- sets several global flags!*) -no_document use_thy "LocaleTest"; +no_document use_thy "Locale_Test/Locale_Test"; diff -r 10ef4da1c314 -r 56e1b6976d0e src/HOL/Bali/AxExample.thy --- a/src/HOL/Bali/AxExample.thy Thu May 27 12:35:40 2010 +0200 +++ b/src/HOL/Bali/AxExample.thy Thu May 27 13:13:30 2010 +0200 @@ -189,7 +189,7 @@ apply (tactic "ax_tac 1") apply (rule_tac [2] ax_subst_Var_allI) apply (tactic {* inst1_tac @{context} "P'" "\vf l vfa. Normal (?P vf l vfa)" *}) -apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac" delsimps [split_paired_All, @{thm peek_and_def2}, @{thm heap_free_def2}, @{thm initd_def2}, @{thm normal_def2}, @{thm supd_lupd}]) 2 *}) +apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac" delsimps [@{thm split_paired_All}, @{thm peek_and_def2}, @{thm heap_free_def2}, @{thm initd_def2}, @{thm normal_def2}, @{thm supd_lupd}]) 2 *}) apply (tactic "ax_tac 2" (* NewA *)) apply (tactic "ax_tac 3" (* ax_Alloc_Arr *)) apply (tactic "ax_tac 3") diff -r 10ef4da1c314 -r 56e1b6976d0e src/HOL/Hoare/hoare_tac.ML --- a/src/HOL/Hoare/hoare_tac.ML Thu May 27 12:35:40 2010 +0200 +++ b/src/HOL/Hoare/hoare_tac.ML Thu May 27 13:13:30 2010 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Hoare/hoare_tac.ML - ID: $Id$ Author: Leonor Prensa Nieto & Tobias Nipkow Derivation of the proof rules and, most importantly, the VCG tactic. @@ -17,8 +16,8 @@ local open HOLogic in (** maps (%x1 ... xn. t) to [x1,...,xn] **) -fun abs2list (Const ("split",_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t - | abs2list (Abs(x,T,t)) = [Free (x, T)] +fun abs2list (Const (@{const_name split}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t + | abs2list (Abs (x, T, t)) = [Free (x, T)] | abs2list _ = []; (** maps {(x1,...,xn). t} to [x1,...,xn] **) @@ -33,7 +32,7 @@ else let val z = mk_abstupleC w body; val T2 = case z of Abs(_,T,_) => T | Const (_, Type (_,[_, Type (_,[T,_])])) $ _ => T; - in Const ("split", (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT) + in Const (@{const_name split}, (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT) $ absfree (n, T, z) end end; (** maps [x1,...,xn] to (x1,...,xn) and types**) @@ -91,7 +90,7 @@ val before_set2pred_simp_tac = (simp_tac (HOL_basic_ss addsimps [Collect_conj_eq RS sym, @{thm Compl_Collect}])); -val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [split_conv])); +val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [@{thm split_conv}])); (*****************************************************************************) (** set2pred_tac transforms sets inclusion into predicates implication, **) @@ -112,7 +111,7 @@ rtac CollectI i, dtac CollectD i, TRY (split_all_tac i) THEN_MAYBE - (rename_tac var_names i THEN full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)]); + (rename_tac var_names i THEN full_simp_tac (HOL_basic_ss addsimps [@{thm split_conv}]) i)]); (*****************************************************************************) (** BasicSimpTac is called to simplify all verification conditions. It does **) @@ -126,7 +125,7 @@ fun BasicSimpTac var_names tac = simp_tac - (HOL_basic_ss addsimps [mem_Collect_eq, split_conv] addsimprocs [record_simproc]) + (HOL_basic_ss addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [record_simproc]) THEN_MAYBE' MaxSimpTac var_names tac; diff -r 10ef4da1c314 -r 56e1b6976d0e src/HOL/Hoare_Parallel/OG_Tactics.thy --- a/src/HOL/Hoare_Parallel/OG_Tactics.thy Thu May 27 12:35:40 2010 +0200 +++ b/src/HOL/Hoare_Parallel/OG_Tactics.thy Thu May 27 13:13:30 2010 +0200 @@ -275,7 +275,7 @@ ML {* val before_interfree_simp_tac = (simp_tac (HOL_basic_ss addsimps [thm "com.simps", thm "post.simps"])) -val interfree_simp_tac = (asm_simp_tac (HOL_ss addsimps [thm "split", thm "ball_Un", thm "ball_empty"]@(thms "my_simp_list"))) +val interfree_simp_tac = (asm_simp_tac (HOL_ss addsimps [@{thm split}, thm "ball_Un", thm "ball_empty"]@(thms "my_simp_list"))) val ParallelConseq = (simp_tac (HOL_basic_ss addsimps (thms "ParallelConseq_list")@(thms "my_simp_list"))) *} diff -r 10ef4da1c314 -r 56e1b6976d0e src/HOL/MicroJava/J/Conform.thy --- a/src/HOL/MicroJava/J/Conform.thy Thu May 27 12:35:40 2010 +0200 +++ b/src/HOL/MicroJava/J/Conform.thy Thu May 27 13:13:30 2010 +0200 @@ -328,8 +328,8 @@ apply auto apply(rule hconfI) apply(drule conforms_heapD) -apply(tactic {* auto_tac (HOL_cs addEs [thm "oconf_hext"] - addDs [thm "hconfD"], @{simpset} delsimps [split_paired_All]) *}) +apply(tactic {* auto_tac (HOL_cs addEs [@{thm oconf_hext}] + addDs [@{thm hconfD}], @{simpset} delsimps [@{thm split_paired_All}]) *}) done lemma conforms_upd_local: diff -r 10ef4da1c314 -r 56e1b6976d0e src/HOL/Modelcheck/MuckeSyn.thy --- a/src/HOL/Modelcheck/MuckeSyn.thy Thu May 27 12:35:40 2010 +0200 +++ b/src/HOL/Modelcheck/MuckeSyn.thy Thu May 27 13:13:30 2010 +0200 @@ -228,7 +228,7 @@ EVERY [ REPEAT (etac thin_rl i), cut_facts_tac (mk_lam_defs defs) i, - full_simp_tac (Mucke_ss delsimps [not_iff,split_part]) i, + full_simp_tac (Mucke_ss delsimps [not_iff, @{thm split_part}]) i, move_mus i, call_mucke_tac i,atac i, REPEAT (rtac refl i)] state); *} diff -r 10ef4da1c314 -r 56e1b6976d0e src/HOL/Modelcheck/mucke_oracle.ML --- a/src/HOL/Modelcheck/mucke_oracle.ML Thu May 27 12:35:40 2010 +0200 +++ b/src/HOL/Modelcheck/mucke_oracle.ML Thu May 27 13:13:30 2010 +0200 @@ -323,7 +323,7 @@ let val VarAbs = Syntax.variant_abs(s,tp,trm); in get_decls sign (Const(fst VarAbs,tp)::Clist) (snd VarAbs) end - | get_decls sign Clist ((Const("split",_)) $ trm) = get_decls sign Clist trm + | get_decls sign Clist ((Const (@{const_name split}, _)) $ trm) = get_decls sign Clist trm | get_decls sign Clist trm = (Clist,trm); fun make_mu_def sign ((tt $ LHS) $ (ttt $ RHS)) = @@ -389,9 +389,9 @@ val t2 = t1 $ ParamDeclTerm in t2 end; -fun is_fundef (( Const("==",_) $ _) $ ((Const("split",_)) $ _)) = true | -is_fundef (( Const("==",_) $ _) $ Abs(x_T_t)) = true -| is_fundef _ = false; +fun is_fundef (Const("==", _) $ _ $ (Const (@{const_name split}, _) $ _)) = true + | is_fundef (Const("==", _) $ _ $ Abs _) = true + | is_fundef _ = false; fun make_mucke_fun_def sign ((_ $ LHS) $ RHS) = let (* fun dest_atom (Const t) = dest_Const (Const t) diff -r 10ef4da1c314 -r 56e1b6976d0e src/HOL/Nominal/nominal_induct.ML --- a/src/HOL/Nominal/nominal_induct.ML Thu May 27 12:35:40 2010 +0200 +++ b/src/HOL/Nominal/nominal_induct.ML Thu May 27 13:13:30 2010 +0200 @@ -23,7 +23,7 @@ val split_all_tuples = Simplifier.full_simplify (HOL_basic_ss addsimps - [split_conv, split_paired_all, unit_all_eq1, @{thm fresh_unit_elim}, @{thm fresh_prod_elim}] @ + [@{thm split_conv}, @{thm split_paired_all}, @{thm unit_all_eq1}, @{thm fresh_unit_elim}, @{thm fresh_prod_elim}] @ @{thms fresh_star_unit_elim} @ @{thms fresh_star_prod_elim}); diff -r 10ef4da1c314 -r 56e1b6976d0e src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Thu May 27 12:35:40 2010 +0200 +++ b/src/HOL/Product_Type.thy Thu May 27 13:13:30 2010 +0200 @@ -1147,101 +1147,6 @@ end *} - -subsection {* Legacy bindings *} - -ML {* -val Collect_split = thm "Collect_split"; -val Compl_Times_UNIV1 = thm "Compl_Times_UNIV1"; -val Compl_Times_UNIV2 = thm "Compl_Times_UNIV2"; -val PairE = thm "PairE"; -val Pair_Rep_inject = thm "Pair_Rep_inject"; -val Pair_def = thm "Pair_def"; -val Pair_eq = @{thm "prod.inject"}; -val Pair_fst_snd_eq = thm "Pair_fst_snd_eq"; -val ProdI = thm "ProdI"; -val SetCompr_Sigma_eq = thm "SetCompr_Sigma_eq"; -val SigmaD1 = thm "SigmaD1"; -val SigmaD2 = thm "SigmaD2"; -val SigmaE = thm "SigmaE"; -val SigmaE2 = thm "SigmaE2"; -val SigmaI = thm "SigmaI"; -val Sigma_Diff_distrib1 = thm "Sigma_Diff_distrib1"; -val Sigma_Diff_distrib2 = thm "Sigma_Diff_distrib2"; -val Sigma_Int_distrib1 = thm "Sigma_Int_distrib1"; -val Sigma_Int_distrib2 = thm "Sigma_Int_distrib2"; -val Sigma_Un_distrib1 = thm "Sigma_Un_distrib1"; -val Sigma_Un_distrib2 = thm "Sigma_Un_distrib2"; -val Sigma_Union = thm "Sigma_Union"; -val Sigma_def = thm "Sigma_def"; -val Sigma_empty1 = thm "Sigma_empty1"; -val Sigma_empty2 = thm "Sigma_empty2"; -val Sigma_mono = thm "Sigma_mono"; -val The_split = thm "The_split"; -val The_split_eq = thm "The_split_eq"; -val The_split_eq = thm "The_split_eq"; -val Times_Diff_distrib1 = thm "Times_Diff_distrib1"; -val Times_Int_distrib1 = thm "Times_Int_distrib1"; -val Times_Un_distrib1 = thm "Times_Un_distrib1"; -val Times_eq_cancel2 = thm "Times_eq_cancel2"; -val Times_subset_cancel2 = thm "Times_subset_cancel2"; -val UNIV_Times_UNIV = thm "UNIV_Times_UNIV"; -val UN_Times_distrib = thm "UN_Times_distrib"; -val Unity_def = thm "Unity_def"; -val cond_split_eta = thm "cond_split_eta"; -val fst_conv = thm "fst_conv"; -val fst_def = thm "fst_def"; -val fst_eqD = thm "fst_eqD"; -val inj_on_Abs_Prod = thm "inj_on_Abs_Prod"; -val mem_Sigma_iff = thm "mem_Sigma_iff"; -val mem_splitE = thm "mem_splitE"; -val mem_splitI = thm "mem_splitI"; -val mem_splitI2 = thm "mem_splitI2"; -val prod_eqI = thm "prod_eqI"; -val prod_fun = thm "prod_fun"; -val prod_fun_compose = thm "prod_fun_compose"; -val prod_fun_def = thm "prod_fun_def"; -val prod_fun_ident = thm "prod_fun_ident"; -val prod_fun_imageE = thm "prod_fun_imageE"; -val prod_fun_imageI = thm "prod_fun_imageI"; -val prod_induct = thm "prod.induct"; -val snd_conv = thm "snd_conv"; -val snd_def = thm "snd_def"; -val snd_eqD = thm "snd_eqD"; -val split = thm "split"; -val splitD = thm "splitD"; -val splitD' = thm "splitD'"; -val splitE = thm "splitE"; -val splitE' = thm "splitE'"; -val splitE2 = thm "splitE2"; -val splitI = thm "splitI"; -val splitI2 = thm "splitI2"; -val splitI2' = thm "splitI2'"; -val split_beta = thm "split_beta"; -val split_conv = thm "split_conv"; -val split_def = thm "split_def"; -val split_eta = thm "split_eta"; -val split_eta_SetCompr = thm "split_eta_SetCompr"; -val split_eta_SetCompr2 = thm "split_eta_SetCompr2"; -val split_paired_All = thm "split_paired_All"; -val split_paired_Ball_Sigma = thm "split_paired_Ball_Sigma"; -val split_paired_Bex_Sigma = thm "split_paired_Bex_Sigma"; -val split_paired_Ex = thm "split_paired_Ex"; -val split_paired_The = thm "split_paired_The"; -val split_paired_all = thm "split_paired_all"; -val split_part = thm "split_part"; -val split_split = thm "split_split"; -val split_split_asm = thm "split_split_asm"; -val split_tupled_all = thms "split_tupled_all"; -val split_weak_cong = thm "split_weak_cong"; -val surj_pair = thm "surj_pair"; -val surjective_pairing = thm "surjective_pairing"; -val unit_abs_eta_conv = thm "unit_abs_eta_conv"; -val unit_all_eq1 = thm "unit_all_eq1"; -val unit_all_eq2 = thm "unit_all_eq2"; -val unit_eq = thm "unit_eq"; -*} - use "Tools/inductive_set.ML" setup Inductive_Set.setup diff -r 10ef4da1c314 -r 56e1b6976d0e src/HOL/Tools/Datatype/datatype_realizer.ML --- a/src/HOL/Tools/Datatype/datatype_realizer.ML Thu May 27 12:35:40 2010 +0200 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Thu May 27 13:13:30 2010 +0200 @@ -113,7 +113,7 @@ val thm = OldGoals.simple_prove_goal_cterm (cert (Logic.list_implies (prems, concl))) (fn prems => - [rewrite_goals_tac (map mk_meta_eq [fst_conv, snd_conv]), + [rewrite_goals_tac (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]), rtac (cterm_instantiate inst induct) 1, ALLGOALS Object_Logic.atomize_prems_tac, rewrite_goals_tac (@{thm o_def} :: map mk_meta_eq rec_rewrites), diff -r 10ef4da1c314 -r 56e1b6976d0e src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu May 27 12:35:40 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu May 27 13:13:30 2010 +0200 @@ -2015,7 +2015,7 @@ | split_lambda (Const ("Product_Type.Unity", _)) t = Abs ("x", HOLogic.unitT, t) | split_lambda t _ = raise (TERM ("split_lambda", [t])) -fun strip_split_abs (Const ("split", _) $ t) = strip_split_abs t +fun strip_split_abs (Const (@{const_name split}, _) $ t) = strip_split_abs t | strip_split_abs (Abs (_, _, t)) = strip_split_abs t | strip_split_abs t = t diff -r 10ef4da1c314 -r 56e1b6976d0e src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu May 27 12:35:40 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu May 27 13:13:30 2010 +0200 @@ -179,7 +179,7 @@ |> maps (fn (res, (names, prems)) => flatten' (betapply (g, res)) (names, prems)) end) - | Const (@{const_name "split"}, _) => + | Const (@{const_name split}, _) => (let val (_, g :: res :: args) = strip_comb t val [res1, res2] = Name.variant_list names ["res1", "res2"] diff -r 10ef4da1c314 -r 56e1b6976d0e src/HOL/Tools/Quotient/quotient_term.ML --- a/src/HOL/Tools/Quotient/quotient_term.ML Thu May 27 12:35:40 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_term.ML Thu May 27 13:13:30 2010 +0200 @@ -560,12 +560,12 @@ end end - | (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))), - ((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) => + | (((t1 as Const (@{const_name split}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))), + ((t2 as Const (@{const_name split}, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) => regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2))) - | (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, s1)), - ((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , s2))) => + | (((t1 as Const (@{const_name split}, _)) $ Abs (v1, ty, s1)), + ((t2 as Const (@{const_name split}, _)) $ Abs (v2, _ , s2))) => regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2)) | (t1 $ t2, t1' $ t2') => diff -r 10ef4da1c314 -r 56e1b6976d0e src/HOL/Tools/TFL/rules.ML --- a/src/HOL/Tools/TFL/rules.ML Thu May 27 12:35:40 2010 +0200 +++ b/src/HOL/Tools/TFL/rules.ML Thu May 27 13:13:30 2010 +0200 @@ -623,7 +623,7 @@ val thm2 = forall_intr_list (map tych L) thm1 val thm3 = forall_elim_list (XFILL tych a vstr) thm2 in refl RS - rewrite_rule [Thm.symmetric (surjective_pairing RS eq_reflection)] thm3 + rewrite_rule [Thm.symmetric (@{thm surjective_pairing} RS eq_reflection)] thm3 end; fun PGEN tych a vstr th = @@ -663,7 +663,7 @@ fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th = let val globals = func::G val ss0 = Simplifier.global_context (Thm.theory_of_thm th) empty_ss - val pbeta_reduce = simpl_conv ss0 [split_conv RS eq_reflection]; + val pbeta_reduce = simpl_conv ss0 [@{thm split_conv} RS eq_reflection]; val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref val dummy = term_ref := [] val dummy = thm_ref := [] diff -r 10ef4da1c314 -r 56e1b6976d0e src/HOL/Tools/TFL/usyntax.ML --- a/src/HOL/Tools/TFL/usyntax.ML Thu May 27 12:35:40 2010 +0200 +++ b/src/HOL/Tools/TFL/usyntax.ML Thu May 27 13:13:30 2010 +0200 @@ -195,8 +195,8 @@ fun prod_ty ty1 ty2 = HOLogic.mk_prodT (ty1,ty2); local -fun mk_uncurry(xt,yt,zt) = - Const("split",(xt --> yt --> zt) --> prod_ty xt yt --> zt) +fun mk_uncurry (xt, yt, zt) = + Const(@{const_name split}, (xt --> yt --> zt) --> prod_ty xt yt --> zt) fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N} | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair" fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false @@ -276,7 +276,7 @@ | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"; -local fun ucheck t = (if #Name(dest_const t) = "split" then t +local fun ucheck t = (if #Name (dest_const t) = @{const_name split} then t else raise Match) in fun dest_pabs used tm = diff -r 10ef4da1c314 -r 56e1b6976d0e src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Thu May 27 12:35:40 2010 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Thu May 27 13:13:30 2010 +0200 @@ -389,7 +389,7 @@ end) (rlzs ~~ rnames); val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs')); - val rews = map mk_meta_eq (fst_conv :: snd_conv :: rec_thms); + val rews = map mk_meta_eq (@{thm fst_conv} :: @{thm snd_conv} :: rec_thms); val thm = Goal.prove_global thy [] prems concl (fn {prems, ...} => EVERY [rtac (#raw_induct ind_info) 1, rewrite_goals_tac rews, diff -r 10ef4da1c314 -r 56e1b6976d0e src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Thu May 27 12:35:40 2010 +0200 +++ b/src/HOL/Tools/inductive_set.ML Thu May 27 13:13:30 2010 +0200 @@ -44,7 +44,7 @@ ts = map Bound (length ps downto 0) then let val simp = full_simp_tac (Simplifier.inherit_context ss - (HOL_basic_ss addsimps [split_paired_all, split_conv])) 1 + (HOL_basic_ss addsimps [@{thm split_paired_all}, @{thm split_conv}])) 1 in SOME (Goal.prove (Simplifier.the_context ss) [] [] (Const ("==", T --> T --> propT) $ S $ S') @@ -92,7 +92,7 @@ mkop s T (m, p, mk_collect p T (head_of u), S) | decomp _ = NONE; val simp = full_simp_tac (Simplifier.inherit_context ss - (HOL_basic_ss addsimps [mem_Collect_eq, split_conv])) 1; + (HOL_basic_ss addsimps [mem_Collect_eq, @{thm split_conv}])) 1; fun mk_rew t = (case strip_abs_vars t of [] => NONE | xs => (case decomp (strip_abs_body t) of @@ -255,7 +255,7 @@ HOLogic.boolT (Bound 0))))] arg_cong' RS sym) end) in - Simplifier.simplify (HOL_basic_ss addsimps [mem_Collect_eq, split_conv] + Simplifier.simplify (HOL_basic_ss addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [collect_mem_simproc]) thm'' |> zero_var_indexes |> eta_contract_thm (equal p) end; @@ -343,7 +343,7 @@ thm |> Thm.instantiate ([], insts) |> Simplifier.full_simplify (HOL_basic_ss addsimprocs - [to_pred_simproc (mem_Collect_eq :: split_conv :: to_pred_simps)]) |> + [to_pred_simproc (mem_Collect_eq :: @{thm split_conv} :: to_pred_simps)]) |> eta_contract_thm (is_pred pred_arities) |> Rule_Cases.save thm end; @@ -396,7 +396,7 @@ then thm |> Simplifier.full_simplify (HOL_basic_ss addsimprocs - [to_pred_simproc (mem_Collect_eq :: split_conv :: to_pred_simps)]) |> + [to_pred_simproc (mem_Collect_eq :: @{thm split_conv} :: to_pred_simps)]) |> eta_contract_thm (is_pred pred_arities) else thm in map preproc end; @@ -463,7 +463,7 @@ end) |> split_list |>> split_list; val eqns' = eqns @ map (prop_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) - (mem_Collect_eq :: split_conv :: to_pred_simps); + (mem_Collect_eq :: @{thm split_conv} :: to_pred_simps); (* predicate version of the introduction rules *) val intros' = @@ -505,7 +505,7 @@ (HOLogic.mk_ptuple fs U (map Bound (length fs downto 0)), list_comb (c, params)))))) (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps - [def, mem_Collect_eq, split_conv]) 1)) + [def, mem_Collect_eq, @{thm split_conv}]) 1)) in lthy |> Local_Theory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"), [Attrib.internal (K pred_set_conv_att)]), diff -r 10ef4da1c314 -r 56e1b6976d0e src/HOL/Tools/quickcheck_generators.ML --- a/src/HOL/Tools/quickcheck_generators.ML Thu May 27 12:35:40 2010 +0200 +++ b/src/HOL/Tools/quickcheck_generators.ML Thu May 27 13:13:30 2010 +0200 @@ -188,7 +188,7 @@ fun tac { context = ctxt, prems = _ } = ALLGOALS (simp_tac (HOL_ss addsimps proj_simps)) THEN ALLGOALS (EqSubst.eqsubst_tac ctxt [0] [aux_simp]) - THEN ALLGOALS (simp_tac (HOL_ss addsimps [fst_conv, snd_conv])); + THEN ALLGOALS (simp_tac (HOL_ss addsimps [@{thm fst_conv}, @{thm snd_conv}])); in (map (fn prop => Skip_Proof.prove lthy [v] [] prop tac) eqs, lthy) end; in lthy diff -r 10ef4da1c314 -r 56e1b6976d0e src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Thu May 27 12:35:40 2010 +0200 +++ b/src/HOL/Tools/record.ML Thu May 27 13:13:30 2010 +0200 @@ -2215,7 +2215,7 @@ prove_standard [] cases_prop (fn _ => try_param_tac rN cases_scheme 1 THEN - simp_all_tac HOL_basic_ss [unit_all_eq1]); + simp_all_tac HOL_basic_ss [@{thm unit_all_eq1}]); val cases = timeit_msg "record cases proof:" cases_prf; fun surjective_prf () = diff -r 10ef4da1c314 -r 56e1b6976d0e src/HOLCF/IOA/Modelcheck/MuIOA.thy --- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy Thu May 27 12:35:40 2010 +0200 +++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy Thu May 27 13:13:30 2010 +0200 @@ -276,13 +276,13 @@ OldGoals.by (REPEAT (dtac eq_reflection 1)); (* Bis hierher wird im Kapitel 4 erl"autert, ab hier im Kapitel 5 *) OldGoals.by (full_simp_tac ((global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs) - delsimps [not_iff,split_part]) + delsimps [not_iff, @{thm split_part}]) addsimps (thl @ comp_simps @ restrict_simps @ hide_simps @ rename_simps @ ioa_simps @ asig_simps)) 1); OldGoals.by (full_simp_tac - (Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1); + (Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff, @{thm split_part}]) 1); OldGoals.by (REPEAT (if_full_simp_tac - (global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1)); + (global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff, @{thm split_part}]) 1)); OldGoals.by (call_mucke_tac 1); (* Bis hierher wird im Kapitel 5 erl"autert, ab hier wieder im Kapitel 4 *) OldGoals.by (atac 1); diff -r 10ef4da1c314 -r 56e1b6976d0e src/HOLCF/IOA/meta_theory/Sequence.thy --- a/src/HOLCF/IOA/meta_theory/Sequence.thy Thu May 27 12:35:40 2010 +0200 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Thu May 27 13:13:30 2010 +0200 @@ -1101,7 +1101,7 @@ THEN (REPEAT_DETERM (CHANGED (asm_simp_tac (simpset_of ctxt) i))); fun pair_tac ctxt s = - res_inst_tac ctxt [(("p", 0), s)] PairE + res_inst_tac ctxt [(("p", 0), s)] @{thm PairE} THEN' hyp_subst_tac THEN' asm_full_simp_tac (simpset_of ctxt); (* induction on a sequence of pairs with pairsplitting and simplification *) diff -r 10ef4da1c314 -r 56e1b6976d0e src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Thu May 27 12:35:40 2010 +0200 +++ b/src/Pure/Isar/locale.ML Thu May 27 13:13:30 2010 +0200 @@ -170,6 +170,31 @@ fun dependencies_of thy name = the_locale thy name |> #dependencies |> map fst; +(* Print instance and qualifiers *) + +fun pretty_reg thy (name, morph) = + let + val name' = extern thy name; + val ctxt = ProofContext.init_global thy; + fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?")); + fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block; + val prt_term = Pretty.quote o Syntax.pretty_term ctxt; + fun prt_term' t = if !show_types + then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::", + Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)] + else prt_term t; + fun prt_inst ts = + Pretty.block (Pretty.breaks (Pretty.str name' :: map prt_term' ts)); + + val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of; + val ts = instance_of thy name morph; + in + case qs of + [] => prt_inst ts + | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":", + Pretty.brk 1, prt_inst ts] + end; + (*** Activate context elements of locale ***) @@ -348,9 +373,23 @@ entries for empty lists may be omitted *) val empty = (Idtab.empty, Inttab.empty); val extend = I; - fun merge ((r1, m1), (r2, m2)) : T = - (Idtab.join (K (fst)) (r1, r2), (* pick left registration, FIXME? *) - Inttab.join (K (Library.merge (eq_snd op =))) (m1, m2)); + fun merge ((reg1, mix1), (reg2, mix2)) : T = + (Idtab.join (fn id => fn (r1 as (_, s1), r2 as (_, s2)) => + if s1 = s2 then raise Idtab.SAME else raise Idtab.DUP id) (reg1, reg2), + Inttab.join (K (Library.merge (eq_snd op =))) (mix1, mix2)) + handle Idtab.DUP id => + (* distinct interpretations with same base: merge their mixins *) + let + val (_, s1) = Idtab.lookup reg1 id |> the; + val (morph2, s2) = Idtab.lookup reg2 id |> the; + val reg2' = Idtab.update (id, (morph2, s1)) reg2; + val mix2' = case Inttab.lookup mix2 s2 of + NONE => mix2 | + SOME mxs => Inttab.delete s2 mix2 |> Inttab.update_new (s1, mxs); + val _ = warning "Removed duplicate interpretation after retrieving its mixins."; + (* FIXME print interpretations, + which is not straightforward without theory context *) + in merge ((reg1, mix1), (reg2', mix2')) end; (* FIXME consolidate with dependencies, consider one data slot only *) ); @@ -421,29 +460,6 @@ (* Diagnostic *) -fun pretty_reg thy (name, morph) = - let - val name' = extern thy name; - val ctxt = ProofContext.init_global thy; - fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?")); - fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block; - val prt_term = Pretty.quote o Syntax.pretty_term ctxt; - fun prt_term' t = if !show_types - then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::", - Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)] - else prt_term t; - fun prt_inst ts = - Pretty.block (Pretty.breaks (Pretty.str name' :: map prt_term' ts)); - - val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of; - val ts = instance_of thy name morph; - in - case qs of - [] => prt_inst ts - | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":", - Pretty.brk 1, prt_inst ts] - end; - fun print_registrations thy raw_name = (case these_registrations thy (intern thy raw_name) of [] => Pretty.str ("no interpretations")