src/FOL/ex/Locale_Test/Locale_Test1.thy
author wenzelm
Mon Mar 10 21:58:54 2014 +0100 (2014-03-10)
changeset 56036 6c3fc3b5592a
parent 55380 4de48353034e
child 56138 f42de6d8ed8e
permissions -rw-r--r--
enabled test in PIDE interaction;
     1 (*  Title:      FOL/ex/Locale_Test/Locale_Test1.thy
     2     Author:     Clemens Ballarin, TU Muenchen
     3 
     4 Test environment for the locale implementation.
     5 *)
     6 
     7 theory Locale_Test1
     8 imports FOL
     9 begin
    10 
    11 typedecl int
    12 instance int :: "term" ..
    13 
    14 consts plus :: "int => int => int" (infixl "+" 60)
    15   zero :: int ("0")
    16   minus :: "int => int" ("- _")
    17 
    18 axiomatization where
    19   int_assoc: "(x + y::int) + z = x + (y + z)" and
    20   int_zero: "0 + x = x" and
    21   int_minus: "(-x) + x = 0" and
    22   int_minus2: "-(-x) = x"
    23 
    24 section {* Inference of parameter types *}
    25 
    26 locale param1 = fixes p
    27 print_locale! param1
    28 
    29 locale param2 = fixes p :: 'b
    30 print_locale! param2
    31 
    32 (*
    33 locale param_top = param2 r for r :: "'b :: {}"
    34   Fails, cannot generalise parameter.
    35 *)
    36 
    37 locale param3 = fixes p (infix ".." 50)
    38 print_locale! param3
    39 
    40 locale param4 = fixes p :: "'a => 'a => 'a" (infix ".." 50)
    41 print_locale! param4
    42 
    43 
    44 subsection {* Incremental type constraints *}
    45 
    46 locale constraint1 =
    47   fixes  prod (infixl "**" 65)
    48   assumes l_id: "x ** y = x"
    49   assumes assoc: "(x ** y) ** z = x ** (y ** z)"
    50 print_locale! constraint1
    51 
    52 locale constraint2 =
    53   fixes p and q
    54   assumes "p = q"
    55 print_locale! constraint2
    56 
    57 
    58 section {* Inheritance *}
    59 
    60 locale semi =
    61   fixes prod (infixl "**" 65)
    62   assumes assoc: "(x ** y) ** z = x ** (y ** z)"
    63 print_locale! semi thm semi_def
    64 
    65 locale lgrp = semi +
    66   fixes one and inv
    67   assumes lone: "one ** x = x"
    68     and linv: "inv(x) ** x = one"
    69 print_locale! lgrp thm lgrp_def lgrp_axioms_def
    70 
    71 locale add_lgrp = semi "op ++" for sum (infixl "++" 60) +
    72   fixes zero and neg
    73   assumes lzero: "zero ++ x = x"
    74     and lneg: "neg(x) ++ x = zero"
    75 print_locale! add_lgrp thm add_lgrp_def add_lgrp_axioms_def
    76 
    77 locale rev_lgrp = semi "%x y. y ++ x" for sum (infixl "++" 60)
    78 print_locale! rev_lgrp thm rev_lgrp_def
    79 
    80 locale hom = f: semi f + g: semi g for f and g
    81 print_locale! hom thm hom_def
    82 
    83 locale perturbation = semi + d: semi "%x y. delta(x) ** delta(y)" for delta
    84 print_locale! perturbation thm perturbation_def
    85 
    86 locale pert_hom = d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2
    87 print_locale! pert_hom thm pert_hom_def
    88 
    89 text {* Alternative expression, obtaining nicer names in @{text "semi f"}. *}
    90 locale pert_hom' = semi f + d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2
    91 print_locale! pert_hom' thm pert_hom'_def
    92 
    93 
    94 section {* Syntax declarations *}
    95 
    96 locale logic =
    97   fixes land (infixl "&&" 55)
    98     and lnot ("-- _" [60] 60)
    99   assumes assoc: "(x && y) && z = x && (y && z)"
   100     and notnot: "-- (-- x) = x"
   101 begin
   102 
   103 definition lor (infixl "||" 50) where
   104   "x || y = --(-- x && -- y)"
   105 
   106 end
   107 print_locale! logic
   108 
   109 locale use_decl = l: logic + semi "op ||"
   110 print_locale! use_decl thm use_decl_def
   111 
   112 locale extra_type =
   113   fixes a :: 'a
   114     and P :: "'a => 'b => o"
   115 begin
   116 
   117 definition test :: "'a => o" where
   118   "test(x) <-> (ALL b. P(x, b))"
   119 
   120 end
   121 
   122 term extra_type.test thm extra_type.test_def
   123 
   124 interpretation var?: extra_type "0" "%x y. x = 0" .
   125 
   126 thm var.test_def
   127 
   128 
   129 text {* Under which circumstances term syntax remains active. *}
   130 
   131 locale "syntax" =
   132   fixes p1 :: "'a => 'b"
   133     and p2 :: "'b => o"
   134 begin
   135 
   136 definition d1 :: "'a => o" where "d1(x) <-> ~ p2(p1(x))"
   137 definition d2 :: "'b => o" where "d2(x) <-> ~ p2(x)"
   138 
   139 thm d1_def d2_def
   140 
   141 end
   142 
   143 thm syntax.d1_def syntax.d2_def
   144 
   145 locale syntax' = "syntax" p1 p2 for p1 :: "'a => 'a" and p2 :: "'a => o"
   146 begin
   147 
   148 thm d1_def d2_def  (* should print as "d1(?x) <-> ..." and "d2(?x) <-> ..." *)
   149 
   150 ML {*
   151   fun check_syntax ctxt thm expected =
   152     let
   153       val obtained =
   154         Print_Mode.setmp [] (Display.string_of_thm (Config.put show_markup false ctxt)) thm;
   155     in
   156       if obtained <> expected
   157       then error ("Theorem syntax '" ^ obtained ^ "' obtained, but '" ^ expected ^ "' expected.")
   158       else ()
   159     end;
   160 *}
   161 
   162 declare [[show_hyps]]
   163 
   164 ML {*
   165   check_syntax @{context} @{thm d1_def} "d1(?x) <-> ~ p2(p1(?x))";
   166   check_syntax @{context} @{thm d2_def} "d2(?x) <-> ~ p2(?x)";
   167 *}
   168 
   169 end
   170 
   171 locale syntax'' = "syntax" p3 p2 for p3 :: "'a => 'b" and p2 :: "'b => o"
   172 begin
   173 
   174 thm d1_def d2_def
   175   (* should print as "syntax.d1(p3, p2, ?x) <-> ..." and "d2(?x) <-> ..." *)
   176 
   177 ML {*
   178   check_syntax @{context} @{thm d1_def} "syntax.d1(p3, p2, ?x) <-> ~ p2(p3(?x))";
   179   check_syntax @{context} @{thm d2_def} "d2(?x) <-> ~ p2(?x)";
   180 *}
   181 
   182 end
   183 
   184 
   185 section {* Foundational versions of theorems *}
   186 
   187 thm logic.assoc
   188 thm logic.lor_def
   189 
   190 
   191 section {* Defines *}
   192 
   193 locale logic_def =
   194   fixes land (infixl "&&" 55)
   195     and lor (infixl "||" 50)
   196     and lnot ("-- _" [60] 60)
   197   assumes assoc: "(x && y) && z = x && (y && z)"
   198     and notnot: "-- (-- x) = x"
   199   defines "x || y == --(-- x && -- y)"
   200 begin
   201 
   202 thm lor_def
   203 
   204 lemma "x || y = --(-- x && --y)"
   205   by (unfold lor_def) (rule refl)
   206 
   207 end
   208 
   209 (* Inheritance of defines *)
   210 
   211 locale logic_def2 = logic_def
   212 begin
   213 
   214 lemma "x || y = --(-- x && --y)"
   215   by (unfold lor_def) (rule refl)
   216 
   217 end
   218 
   219 
   220 section {* Notes *}
   221 
   222 (* A somewhat arcane homomorphism example *)
   223 
   224 definition semi_hom where
   225   "semi_hom(prod, sum, h) <-> (ALL x y. h(prod(x, y)) = sum(h(x), h(y)))"
   226 
   227 lemma semi_hom_mult:
   228   "semi_hom(prod, sum, h) ==> h(prod(x, y)) = sum(h(x), h(y))"
   229   by (simp add: semi_hom_def)
   230 
   231 locale semi_hom_loc = prod: semi prod + sum: semi sum
   232   for prod and sum and h +
   233   assumes semi_homh: "semi_hom(prod, sum, h)"
   234   notes semi_hom_mult = semi_hom_mult [OF semi_homh]
   235 
   236 thm semi_hom_loc.semi_hom_mult
   237 (* unspecified, attribute not applied in backgroud theory !!! *)
   238 
   239 lemma (in semi_hom_loc) "h(prod(x, y)) = sum(h(x), h(y))"
   240   by (rule semi_hom_mult)
   241 
   242 (* Referring to facts from within a context specification *)
   243 
   244 lemma
   245   assumes x: "P <-> P"
   246   notes y = x
   247   shows True ..
   248 
   249 
   250 section {* Theorem statements *}
   251 
   252 lemma (in lgrp) lcancel:
   253   "x ** y = x ** z <-> y = z"
   254 proof
   255   assume "x ** y = x ** z"
   256   then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
   257   then show "y = z" by (simp add: lone linv)
   258 qed simp
   259 print_locale! lgrp
   260 
   261 
   262 locale rgrp = semi +
   263   fixes one and inv
   264   assumes rone: "x ** one = x"
   265     and rinv: "x ** inv(x) = one"
   266 begin
   267 
   268 lemma rcancel:
   269   "y ** x = z ** x <-> y = z"
   270 proof
   271   assume "y ** x = z ** x"
   272   then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
   273     by (simp add: assoc [symmetric])
   274   then show "y = z" by (simp add: rone rinv)
   275 qed simp
   276 
   277 end
   278 print_locale! rgrp
   279 
   280 
   281 subsection {* Patterns *}
   282 
   283 lemma (in rgrp)
   284   assumes "y ** x = z ** x" (is ?a)
   285   shows "y = z" (is ?t)
   286 proof -
   287   txt {* Weird proof involving patterns from context element and conclusion. *}
   288   {
   289     assume ?a
   290     then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
   291       by (simp add: assoc [symmetric])
   292     then have ?t by (simp add: rone rinv)
   293   }
   294   note x = this
   295   show ?t by (rule x [OF `?a`])
   296 qed
   297 
   298 
   299 section {* Interpretation between locales: sublocales *}
   300 
   301 sublocale lgrp < right: rgrp
   302 print_facts
   303 proof unfold_locales
   304   {
   305     fix x
   306     have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
   307     then show "x ** one = x" by (simp add: assoc lcancel)
   308   }
   309   note rone = this
   310   {
   311     fix x
   312     have "inv(x) ** x ** inv(x) = inv(x) ** one"
   313       by (simp add: linv lone rone)
   314     then show "x ** inv(x) = one" by (simp add: assoc lcancel)
   315   }
   316 qed
   317 
   318 (* effect on printed locale *)
   319 
   320 print_locale! lgrp
   321 
   322 (* use of derived theorem *)
   323 
   324 lemma (in lgrp)
   325   "y ** x = z ** x <-> y = z"
   326   apply (rule rcancel)
   327   done
   328 
   329 (* circular interpretation *)
   330 
   331 sublocale rgrp < left: lgrp
   332 proof unfold_locales
   333   {
   334     fix x
   335     have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
   336     then show "one ** x = x" by (simp add: assoc [symmetric] rcancel)
   337   }
   338   note lone = this
   339   {
   340     fix x
   341     have "inv(x) ** (x ** inv(x)) = one ** inv(x)"
   342       by (simp add: rinv lone rone)
   343     then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel)
   344   }
   345 qed
   346 
   347 (* effect on printed locale *)
   348 
   349 print_locale! rgrp
   350 print_locale! lgrp
   351 
   352 
   353 (* Duality *)
   354 
   355 locale order =
   356   fixes less :: "'a => 'a => o" (infix "<<" 50)
   357   assumes refl: "x << x"
   358     and trans: "[| x << y; y << z |] ==> x << z"
   359 
   360 sublocale order < dual: order "%x y. y << x"
   361   apply unfold_locales apply (rule refl) apply (blast intro: trans)
   362   done
   363 
   364 print_locale! order  (* Only two instances of order. *)
   365 
   366 locale order' =
   367   fixes less :: "'a => 'a => o" (infix "<<" 50)
   368   assumes refl: "x << x"
   369     and trans: "[| x << y; y << z |] ==> x << z"
   370 
   371 locale order_with_def = order'
   372 begin
   373 
   374 definition greater :: "'a => 'a => o" (infix ">>" 50) where
   375   "x >> y <-> y << x"
   376 
   377 end
   378 
   379 sublocale order_with_def < dual: order' "op >>"
   380   apply unfold_locales
   381   unfolding greater_def
   382   apply (rule refl) apply (blast intro: trans)
   383   done
   384 
   385 print_locale! order_with_def
   386 (* Note that decls come after theorems that make use of them. *)
   387 
   388 
   389 (* locale with many parameters ---
   390    interpretations generate alternating group A5 *)
   391 
   392 
   393 locale A5 =
   394   fixes A and B and C and D and E
   395   assumes eq: "A <-> B <-> C <-> D <-> E"
   396 
   397 sublocale A5 < 1: A5 _ _ D E C
   398 print_facts
   399   using eq apply (blast intro: A5.intro) done
   400 
   401 sublocale A5 < 2: A5 C _ E _ A
   402 print_facts
   403   using eq apply (blast intro: A5.intro) done
   404 
   405 sublocale A5 < 3: A5 B C A _ _
   406 print_facts
   407   using eq apply (blast intro: A5.intro) done
   408 
   409 (* Any even permutation of parameters is subsumed by the above. *)
   410 
   411 print_locale! A5
   412 
   413 
   414 (* Free arguments of instance *)
   415 
   416 locale trivial =
   417   fixes P and Q :: o
   418   assumes Q: "P <-> P <-> Q"
   419 begin
   420 
   421 lemma Q_triv: "Q" using Q by fast
   422 
   423 end
   424 
   425 sublocale trivial < x: trivial x _
   426   apply unfold_locales using Q by fast
   427 
   428 print_locale! trivial
   429 
   430 context trivial begin thm x.Q [where ?x = True] end
   431 
   432 sublocale trivial < y: trivial Q Q
   433   by unfold_locales
   434   (* Succeeds since previous interpretation is more general. *)
   435 
   436 print_locale! trivial  (* No instance for y created (subsumed). *)
   437 
   438 
   439 subsection {* Sublocale, then interpretation in theory *}
   440 
   441 interpretation int?: lgrp "op +" "0" "minus"
   442 proof unfold_locales
   443 qed (rule int_assoc int_zero int_minus)+
   444 
   445 thm int.assoc int.semi_axioms
   446 
   447 interpretation int2?: semi "op +"
   448   by unfold_locales  (* subsumed, thm int2.assoc not generated *)
   449 
   450 ML {* (Global_Theory.get_thms @{theory} "int2.assoc";
   451     error "thm int2.assoc was generated")
   452   handle ERROR "Unknown fact \"int2.assoc\"" => ([]:thm list); *}
   453 
   454 thm int.lone int.right.rone
   455   (* the latter comes through the sublocale relation *)
   456 
   457 
   458 subsection {* Interpretation in theory, then sublocale *}
   459 
   460 interpretation fol: logic "op +" "minus"
   461   by unfold_locales (rule int_assoc int_minus2)+
   462 
   463 locale logic2 =
   464   fixes land (infixl "&&" 55)
   465     and lnot ("-- _" [60] 60)
   466   assumes assoc: "(x && y) && z = x && (y && z)"
   467     and notnot: "-- (-- x) = x"
   468 begin
   469 
   470 definition lor (infixl "||" 50) where
   471   "x || y = --(-- x && -- y)"
   472 
   473 end
   474 
   475 sublocale logic < two: logic2
   476   by unfold_locales (rule assoc notnot)+
   477 
   478 thm fol.two.assoc
   479 
   480 
   481 subsection {* Declarations and sublocale *}
   482 
   483 locale logic_a = logic
   484 locale logic_b = logic
   485 
   486 sublocale logic_a < logic_b
   487   by unfold_locales
   488 
   489 
   490 subsection {* Interpretation *}
   491 
   492 subsection {* Rewrite morphism *}
   493 
   494 locale logic_o =
   495   fixes land (infixl "&&" 55)
   496     and lnot ("-- _" [60] 60)
   497   assumes assoc_o: "(x && y) && z <-> x && (y && z)"
   498     and notnot_o: "-- (-- x) <-> x"
   499 begin
   500 
   501 definition lor_o (infixl "||" 50) where
   502   "x || y <-> --(-- x && -- y)"
   503 
   504 end
   505 
   506 interpretation x: logic_o "op &" "Not"
   507   where bool_logic_o: "x.lor_o(x, y) <-> x | y"
   508 proof -
   509   show bool_logic_o: "PROP logic_o(op &, Not)" by unfold_locales fast+
   510   show "logic_o.lor_o(op &, Not, x, y) <-> x | y"
   511     by (unfold logic_o.lor_o_def [OF bool_logic_o]) fast
   512 qed
   513 
   514 thm x.lor_o_def bool_logic_o
   515 
   516 lemma lor_triv: "z <-> z" ..
   517 
   518 lemma (in logic_o) lor_triv: "x || y <-> x || y" by fast
   519 
   520 thm lor_triv [where z = True] (* Check strict prefix. *)
   521   x.lor_triv
   522 
   523 
   524 subsection {* Inheritance of rewrite morphisms *}
   525 
   526 locale reflexive =
   527   fixes le :: "'a => 'a => o" (infix "\<sqsubseteq>" 50)
   528   assumes refl: "x \<sqsubseteq> x"
   529 begin
   530 
   531 definition less (infix "\<sqsubset>" 50) where "x \<sqsubset> y <-> x \<sqsubseteq> y & x ~= y"
   532 
   533 end
   534 
   535 axiomatization
   536   gle :: "'a => 'a => o" and gless :: "'a => 'a => o" and
   537   gle' :: "'a => 'a => o" and gless' :: "'a => 'a => o"
   538 where
   539   grefl: "gle(x, x)" and gless_def: "gless(x, y) <-> gle(x, y) & x ~= y" and
   540   grefl': "gle'(x, x)" and gless'_def: "gless'(x, y) <-> gle'(x, y) & x ~= y"
   541 
   542 text {* Setup *}
   543 
   544 locale mixin = reflexive
   545 begin
   546 lemmas less_thm = less_def
   547 end
   548 
   549 interpretation le: mixin gle where "reflexive.less(gle, x, y) <-> gless(x, y)"
   550 proof -
   551   show "mixin(gle)" by unfold_locales (rule grefl)
   552   note reflexive = this[unfolded mixin_def]
   553   show "reflexive.less(gle, x, y) <-> gless(x, y)"
   554     by (simp add: reflexive.less_def[OF reflexive] gless_def)
   555 qed
   556 
   557 text {* Rewrite morphism propagated along the locale hierarchy *}
   558 
   559 locale mixin2 = mixin
   560 begin
   561 lemmas less_thm2 = less_def
   562 end
   563 
   564 interpretation le: mixin2 gle
   565   by unfold_locales
   566 
   567 thm le.less_thm2  (* rewrite morphism applied *)
   568 lemma "gless(x, y) <-> gle(x, y) & x ~= y"
   569   by (rule le.less_thm2)
   570 
   571 text {* Rewrite morphism does not leak to a side branch. *}
   572 
   573 locale mixin3 = reflexive
   574 begin
   575 lemmas less_thm3 = less_def
   576 end
   577 
   578 interpretation le: mixin3 gle
   579   by unfold_locales
   580 
   581 thm le.less_thm3  (* rewrite morphism not applied *)
   582 lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y" by (rule le.less_thm3)
   583 
   584 text {* Rewrite morphism only available in original context *}
   585 
   586 locale mixin4_base = reflexive
   587 
   588 locale mixin4_mixin = mixin4_base
   589 
   590 interpretation le: mixin4_mixin gle
   591   where "reflexive.less(gle, x, y) <-> gless(x, y)"
   592 proof -
   593   show "mixin4_mixin(gle)" by unfold_locales (rule grefl)
   594   note reflexive = this[unfolded mixin4_mixin_def mixin4_base_def mixin_def]
   595   show "reflexive.less(gle, x, y) <-> gless(x, y)"
   596     by (simp add: reflexive.less_def[OF reflexive] gless_def)
   597 qed
   598 
   599 locale mixin4_copy = mixin4_base
   600 begin
   601 lemmas less_thm4 = less_def
   602 end
   603 
   604 locale mixin4_combined = le1: mixin4_mixin le' + le2: mixin4_copy le for le' le
   605 begin
   606 lemmas less_thm4' = less_def
   607 end
   608 
   609 interpretation le4: mixin4_combined gle' gle
   610   by unfold_locales (rule grefl')
   611 
   612 thm le4.less_thm4' (* rewrite morphism not applied *)
   613 lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
   614   by (rule le4.less_thm4')
   615 
   616 text {* Inherited rewrite morphism applied to new theorem *}
   617 
   618 locale mixin5_base = reflexive
   619 
   620 locale mixin5_inherited = mixin5_base
   621 
   622 interpretation le5: mixin5_base gle
   623   where "reflexive.less(gle, x, y) <-> gless(x, y)"
   624 proof -
   625   show "mixin5_base(gle)" by unfold_locales
   626   note reflexive = this[unfolded mixin5_base_def mixin_def]
   627   show "reflexive.less(gle, x, y) <-> gless(x, y)"
   628     by (simp add: reflexive.less_def[OF reflexive] gless_def)
   629 qed
   630 
   631 interpretation le5: mixin5_inherited gle
   632   by unfold_locales
   633 
   634 lemmas (in mixin5_inherited) less_thm5 = less_def
   635 
   636 thm le5.less_thm5  (* rewrite morphism applied *)
   637 lemma "gless(x, y) <-> gle(x, y) & x ~= y"
   638   by (rule le5.less_thm5)
   639 
   640 text {* Rewrite morphism pushed down to existing inherited locale *}
   641 
   642 locale mixin6_base = reflexive
   643 
   644 locale mixin6_inherited = mixin5_base
   645 
   646 interpretation le6: mixin6_base gle
   647   by unfold_locales
   648 interpretation le6: mixin6_inherited gle
   649   by unfold_locales
   650 interpretation le6: mixin6_base gle
   651   where "reflexive.less(gle, x, y) <-> gless(x, y)"
   652 proof -
   653   show "mixin6_base(gle)" by unfold_locales
   654   note reflexive = this[unfolded mixin6_base_def mixin_def]
   655   show "reflexive.less(gle, x, y) <-> gless(x, y)"
   656     by (simp add: reflexive.less_def[OF reflexive] gless_def)
   657 qed
   658 
   659 lemmas (in mixin6_inherited) less_thm6 = less_def
   660 
   661 thm le6.less_thm6  (* mixin applied *)
   662 lemma "gless(x, y) <-> gle(x, y) & x ~= y"
   663   by (rule le6.less_thm6)
   664 
   665 text {* Existing rewrite morphism inherited through sublocale relation *}
   666 
   667 locale mixin7_base = reflexive
   668 
   669 locale mixin7_inherited = reflexive
   670 
   671 interpretation le7: mixin7_base gle
   672   where "reflexive.less(gle, x, y) <-> gless(x, y)"
   673 proof -
   674   show "mixin7_base(gle)" by unfold_locales
   675   note reflexive = this[unfolded mixin7_base_def mixin_def]
   676   show "reflexive.less(gle, x, y) <-> gless(x, y)"
   677     by (simp add: reflexive.less_def[OF reflexive] gless_def)
   678 qed
   679 
   680 interpretation le7: mixin7_inherited gle
   681   by unfold_locales
   682 
   683 lemmas (in mixin7_inherited) less_thm7 = less_def
   684 
   685 thm le7.less_thm7  (* before, rewrite morphism not applied *)
   686 lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
   687   by (rule le7.less_thm7)
   688 
   689 sublocale mixin7_inherited < mixin7_base
   690   by unfold_locales
   691 
   692 lemmas (in mixin7_inherited) less_thm7b = less_def
   693 
   694 thm le7.less_thm7b  (* after, mixin applied *)
   695 lemma "gless(x, y) <-> gle(x, y) & x ~= y"
   696   by (rule le7.less_thm7b)
   697 
   698 
   699 text {* This locale will be interpreted in later theories. *}
   700 
   701 locale mixin_thy_merge = le: reflexive le + le': reflexive le' for le le'
   702 
   703 
   704 subsection {* Rewrite morphisms in sublocale *}
   705 
   706 text {* Simulate a specification of left groups where unit and inverse are defined
   707   rather than specified.  This is possible, but not in FOL, due to the lack of a
   708   selection operator. *}
   709 
   710 axiomatization glob_one and glob_inv
   711   where glob_lone: "prod(glob_one(prod), x) = x"
   712     and glob_linv: "prod(glob_inv(prod, x), x) = glob_one(prod)"
   713 
   714 locale dgrp = semi
   715 begin
   716 
   717 definition one where "one = glob_one(prod)"
   718 
   719 lemma lone: "one ** x = x"
   720   unfolding one_def by (rule glob_lone)
   721 
   722 definition inv where "inv(x) = glob_inv(prod, x)"
   723 
   724 lemma linv: "inv(x) ** x = one"
   725   unfolding one_def inv_def by (rule glob_linv)
   726 
   727 end
   728 
   729 sublocale lgrp < "def": dgrp
   730   where one_equation: "dgrp.one(prod) = one" and inv_equation: "dgrp.inv(prod, x) = inv(x)"
   731 proof -
   732   show "dgrp(prod)" by unfold_locales
   733   from this interpret d: dgrp .
   734   -- Unit
   735   have "dgrp.one(prod) = glob_one(prod)" by (rule d.one_def)
   736   also have "... = glob_one(prod) ** one" by (simp add: rone)
   737   also have "... = one" by (simp add: glob_lone)
   738   finally show "dgrp.one(prod) = one" .
   739   -- Inverse
   740   then have "dgrp.inv(prod, x) ** x = inv(x) ** x" by (simp add: glob_linv d.linv linv)
   741   then show "dgrp.inv(prod, x) = inv(x)" by (simp add: rcancel)
   742 qed
   743 
   744 print_locale! lgrp
   745 
   746 context lgrp begin
   747 
   748 text {* Equations stored in target *}
   749 
   750 lemma "dgrp.one(prod) = one" by (rule one_equation)
   751 lemma "dgrp.inv(prod, x) = inv(x)" by (rule inv_equation)
   752 
   753 text {* Rewrite morphisms applied *}
   754 
   755 lemma "one = glob_one(prod)" by (rule one_def)
   756 lemma "inv(x) = glob_inv(prod, x)" by (rule inv_def)
   757 
   758 end
   759 
   760 text {* Interpreted versions *}
   761 
   762 lemma "0 = glob_one (op +)" by (rule int.def.one_def)
   763 lemma "- x = glob_inv(op +, x)" by (rule int.def.inv_def)
   764 
   765 text {* Roundup applies rewrite morphisms at declaration level in DFS tree *}
   766 
   767 locale roundup = fixes x assumes true: "x <-> True"
   768 
   769 sublocale roundup \<subseteq> sub: roundup x where "x <-> True & True"
   770   apply unfold_locales apply (simp add: true) done
   771 lemma (in roundup) "True & True <-> True" by (rule sub.true)
   772 
   773 
   774 section {* Interpretation in named contexts *}
   775 
   776 locale container
   777 begin
   778 interpretation private!: roundup True by unfold_locales rule
   779 lemmas true_copy = private.true
   780 end
   781 
   782 context container begin
   783 ML {* (Context.>> (fn generic => let val context = Context.proof_of generic
   784   val _ = Proof_Context.get_thms context "private.true" in generic end);
   785   error "thm private.true was persisted")
   786   handle ERROR "Unknown fact \"private.true\"" => ([]:thm list); *}
   787 thm true_copy
   788 end
   789 
   790 
   791 section {* Interpretation in proofs *}
   792 
   793 lemma True
   794 proof
   795   interpret "local": lgrp "op +" "0" "minus"
   796     by unfold_locales  (* subsumed *)
   797   {
   798     fix zero :: int
   799     assume "!!x. zero + x = x" "!!x. (-x) + x = zero"
   800     then interpret local_fixed: lgrp "op +" zero "minus"
   801       by unfold_locales
   802     thm local_fixed.lone
   803     print_dependencies! lgrp "op +" 0 minus + lgrp "op +" zero minus
   804   }
   805   assume "!!x zero. zero + x = x" "!!x zero. (-x) + x = zero"
   806   then interpret local_free: lgrp "op +" zero "minus" for zero
   807     by unfold_locales
   808   thm local_free.lone [where ?zero = 0]
   809 qed
   810 
   811 lemma True
   812 proof
   813   {
   814     fix pand and pnot and por
   815     assume passoc: "!!x y z. pand(pand(x, y), z) <-> pand(x, pand(y, z))"
   816       and pnotnot: "!!x. pnot(pnot(x)) <-> x"
   817       and por_def: "!!x y. por(x, y) <-> pnot(pand(pnot(x), pnot(y)))"
   818     interpret loc: logic_o pand pnot
   819       where por_eq: "!!x y. logic_o.lor_o(pand, pnot, x, y) <-> por(x, y)"  (* FIXME *)
   820     proof -
   821       show logic_o: "PROP logic_o(pand, pnot)" using passoc pnotnot by unfold_locales
   822       fix x y
   823       show "logic_o.lor_o(pand, pnot, x, y) <-> por(x, y)"
   824         by (unfold logic_o.lor_o_def [OF logic_o]) (rule por_def [symmetric])
   825     qed
   826     print_interps logic_o
   827     have "!!x y. por(x, y) <-> pnot(pand(pnot(x), pnot(y)))" by (rule loc.lor_o_def)
   828   }
   829 qed
   830 
   831 end