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