src/FOL/ex/LocaleTest.thy
author ballarin
Tue Jun 20 15:53:44 2006 +0200 (2006-06-20)
changeset 19931 fb32b43e7f80
parent 19783 82f365a14960
child 19984 29bb4659f80a
permissions -rw-r--r--
Restructured locales with predicates: import is now an interpretation.
New method intro_locales.
     1 (*  Title:      FOL/ex/LocaleTest.thy
     2     ID:         $Id$
     3     Author:     Clemens Ballarin
     4     Copyright (c) 2005 by Clemens Ballarin
     5 
     6 Collection of regression tests for locales.
     7 *)
     8 
     9 header {* Test of Locale Interpretation *}
    10 
    11 theory LocaleTest
    12 imports FOL
    13 begin
    14 
    15 ML {* set quick_and_dirty *}    (* allow for thm command in batch mode *)
    16 ML {* set Toplevel.debug *}
    17 ML {* set show_hyps *}
    18 ML {* set show_sorts *}
    19 
    20 ML {*
    21   fun check_thm name = let
    22     val thy = the_context ();
    23     val thm = get_thm thy (Name name);
    24     val {prop, hyps, ...} = rep_thm thm;
    25     val prems = Logic.strip_imp_prems prop;
    26     val _ = if null hyps then ()
    27         else error ("Theorem " ^ quote name ^ " has meta hyps.\n" ^
    28           "Consistency check of locales package failed.");
    29     val _ = if null prems then ()
    30         else error ("Theorem " ^ quote name ^ " has premises.\n" ^
    31           "Consistency check of locales package failed.");
    32   in () end;
    33 *}
    34 
    35 section {* Context Elements and Locale Expressions *}
    36 
    37 text {* Naming convention for global objects: prefixes L and l *}
    38 
    39 subsection {* Renaming with Syntax *}
    40 
    41 locale (open) LS = var mult +
    42   assumes "mult(x, y) = mult(y, x)"
    43 
    44 print_locale LS
    45 
    46 locale LS' = LS mult (infixl "**" 60)
    47 
    48 print_locale LS'
    49 
    50 locale LT = var mult (infixl "**" 60) +
    51   assumes "x ** y = y ** x"
    52 
    53 locale LU = LT mult (infixl "**" 60) + LT add (infixl "++" 55) + var h +
    54   assumes hom: "h(x ** y) = h(x) ++ h(y)"
    55 
    56 (*
    57 Graceful handling of type errors?
    58 locale LY = LT mult (infixl "**" 60) + LT add (binder "++" 55) + var h +
    59   assumes "mult(x) == add"
    60 *)
    61 
    62 locale LV = LU _ add
    63 
    64 locale LW = LU _ mult (infixl "**" 60)
    65 
    66 
    67 subsection {* Constrains *}
    68 
    69 locale LZ = fixes a (structure)
    70 locale LZ' = LZ +
    71   constrains a :: "'a => 'b"
    72   assumes "a (x :: 'a) = a (y)"
    73 print_locale LZ'
    74 
    75 
    76 section {* Interpretation *}
    77 
    78 text {* Naming convention for global objects: prefixes I and i *}
    79 
    80 text {* interpretation input syntax *}
    81 
    82 locale IL
    83 locale IM = fixes a and b and c
    84 
    85 interpretation test [simp]: IL + IM a b c [x y z] .
    86 
    87 print_interps IL    (* output: test *)
    88 print_interps IM    (* output: test *)
    89 
    90 interpretation test [simp]: IL print_interps IM .
    91 
    92 interpretation IL .
    93 
    94 text {* Processing of locale expression *}
    95 
    96 locale IA = fixes a assumes asm_A: "a = a"
    97 
    98 locale (open) IB = fixes b assumes asm_B [simp]: "b = b"
    99 
   100 locale IC = IA + IB + assumes asm_C: "c = c"
   101   (* TODO: independent type var in c, prohibit locale declaration *)
   102 
   103 locale ID = IA + IB + fixes d defines def_D: "d == (a = b)"
   104 
   105 theorem (in IA)
   106   includes ID
   107   shows True
   108   print_interps! IA
   109   print_interps! ID
   110   ..
   111 
   112 theorem (in ID) True ..
   113 
   114 typedecl i
   115 arities i :: "term"
   116 
   117 
   118 interpretation i1: IC ["X::i" "Y::i"] by (intro_locales) auto
   119 
   120 print_interps IA  (* output: i1 *)
   121 
   122 (* possible accesses *)
   123 thm i1.a.asm_A thm LocaleTest.i1.a.asm_A
   124 thm i1.asm_A thm LocaleTest.i1.asm_A
   125 
   126 ML {* check_thm "i1.a.asm_A" *}
   127 
   128 (* without prefix *)
   129 
   130 interpretation IC ["W::i" "Z::i"] .  (* subsumed by i1: IC *)
   131 interpretation IC ["W::'a" "Z::i"] by intro_locales auto
   132   (* subsumes i1: IA and i1: IC *)
   133 
   134 print_interps IA  (* output: <no prefix>, i1 *)
   135 
   136 (* possible accesses *)
   137 thm asm_C thm a_b.asm_C thm LocaleTest.a_b.asm_C thm LocaleTest.a_b.asm_C
   138 
   139 ML {* check_thm "asm_C" *}
   140 
   141 interpretation i2: ID [X "Y::i" "Y = X"]
   142   by (simp add: eq_commute) intro_locales
   143 
   144 print_interps IA  (* output: <no prefix>, i1 *)
   145 print_interps ID  (* output: i2 *)
   146 
   147 
   148 interpretation i3: ID [X "Y::i"] by simp intro_locales
   149 
   150 (* duplicate: thm not added *)
   151 
   152 (* thm i3.a.asm_A *)
   153 
   154 
   155 print_interps IA  (* output: <no prefix>, i1 *)
   156 print_interps IB  (* output: i1 *)
   157 print_interps IC  (* output: <no prefix, i1 *)
   158 print_interps ID  (* output: i2, i3 *)
   159 
   160 (* schematic vars in instantiation not permitted *)
   161 (*
   162 interpretation i4: IA ["?x::?'a1"] apply (rule IA.intro) apply rule done
   163 print_interps IA
   164 *)
   165 
   166 interpretation i10: ID + ID a' b' d' [X "Y::i" _ u "v::i" _] .
   167 
   168 corollary (in ID) th_x: True ..
   169 
   170 (* possible accesses: for each registration *)
   171 
   172 thm i2.th_x thm i3.th_x
   173 
   174 ML {* check_thm "i2.th_x"; check_thm "i3.th_x" *}
   175 
   176 lemma (in ID) th_y: "d == (a = b)" .
   177 
   178 thm i2.th_y thm i3.th_y
   179 
   180 ML {* check_thm "i2.th_y"; check_thm "i3.th_y" *}
   181 
   182 lemmas (in ID) th_z = th_y
   183 
   184 thm i2.th_z
   185 
   186 ML {* check_thm "i2.th_z" *}
   187 
   188 
   189 subsection {* Interpretation in Proof Contexts *}
   190 
   191 locale IF = fixes f assumes asm_F: "f & f --> f"
   192 
   193 theorem True
   194 proof -
   195   fix alpha::i and beta::'a and gamma::o
   196   (* FIXME: omitting type of beta leads to error later at interpret i6 *)
   197   have alpha_A: "IA(alpha)" by intro_locales simp
   198   interpret i5: IA [alpha] .  (* subsumed *)
   199   print_interps IA  (* output: <no prefix>, i1 *)
   200   interpret i6: IC [alpha beta] by intro_locales auto
   201   print_interps IA   (* output: <no prefix>, i1 *)
   202   print_interps IC   (* output: <no prefix>, i1, i6 *)
   203   interpret i11: IF [gamma] by (fast intro: IF.intro)
   204   thm i11.asm_F      (* gamma is a Free *)
   205 qed rule
   206 
   207 theorem (in IA) True
   208 proof -
   209   print_interps! IA
   210   fix beta and gamma
   211   interpret i9: ID [a beta _]
   212     apply - apply assumption
   213     apply intro_locales
   214     apply (rule refl) done
   215 qed rule
   216 
   217 
   218 (* Definition involving free variable *)
   219 
   220 ML {* reset show_sorts *}
   221 
   222 locale IE = fixes e defines e_def: "e(x) == x & x"
   223   notes e_def2 = e_def
   224 
   225 lemma (in IE) True thm e_def by fast
   226 
   227 interpretation i7: IE ["%x. x"] by simp
   228 
   229 thm i7.e_def2 (* has no premise *)
   230 
   231 ML {* check_thm "i7.e_def2" *}
   232 
   233 locale IE' = fixes e defines e_def: "e == (%x. x & x)"
   234   notes e_def2 = e_def
   235 
   236 interpretation i7': IE' ["(%x. x)"] by simp
   237 
   238 thm i7'.e_def2
   239 
   240 ML {* check_thm "i7'.e_def2" *}
   241 
   242 (* Definition involving free variable in assm *)
   243 
   244 locale (open) IG = fixes g assumes asm_G: "g --> x"
   245   notes asm_G2 = asm_G
   246 
   247 interpretation i8: IG ["False"] by fast
   248 
   249 thm i8.asm_G2
   250 
   251 ML {* check_thm "i8.asm_G2" *}
   252 
   253 text {* Locale without assumptions *}
   254 
   255 locale IL1 = notes rev_conjI [intro] = conjI [THEN iffD1 [OF conj_commute]]
   256 
   257 lemma "[| P; Q |] ==> P & Q"
   258 proof -
   259   interpret my: IL1 .          txt {* No chained fact required. *}
   260   assume Q and P               txt {* order reversed *}
   261   then show "P & Q" ..         txt {* Applies @{thm my.rev_conjI}. *}
   262 qed
   263 
   264 locale IL11 = notes rev_conjI = conjI [THEN iffD1 [OF conj_commute]]
   265 
   266 lemma "[| P; Q |] ==> P & Q"
   267 proof -
   268   interpret [intro]: IL11 .     txt {* Attribute supplied at instantiation. *}
   269   assume Q and P
   270   then show "P & Q" ..
   271 qed
   272 
   273 subsection {* Simple locale with assumptions *}
   274 
   275 consts ibin :: "[i, i] => i" (infixl "#" 60)
   276 
   277 axioms i_assoc: "(x # y) # z = x # (y # z)"
   278   i_comm: "x # y = y # x"
   279 
   280 locale IL2 =
   281   fixes OP (infixl "+" 60)
   282   assumes assoc: "(x + y) + z = x + (y + z)"
   283     and comm: "x + y = y + x"
   284 
   285 lemma (in IL2) lcomm: "x + (y + z) = y + (x + z)"
   286 proof -
   287   have "x + (y + z) = (x + y) + z" by (simp add: assoc)
   288   also have "... = (y + x) + z" by (simp add: comm)
   289   also have "... = y + (x + z)" by (simp add: assoc)
   290   finally show ?thesis .
   291 qed
   292 
   293 lemmas (in IL2) AC = comm assoc lcomm
   294 
   295 lemma "(x::i) # y # z # w = y # x # w # z"
   296 proof -
   297   interpret my: IL2 ["op #"] by (rule IL2.intro [of "op #", OF i_assoc i_comm])
   298   show ?thesis by (simp only: my.OP.AC)  (* or my.AC *)
   299 qed
   300 
   301 subsection {* Nested locale with assumptions *}
   302 
   303 locale IL3 =
   304   fixes OP (infixl "+" 60)
   305   assumes assoc: "(x + y) + z = x + (y + z)"
   306 
   307 locale IL4 = IL3 +
   308   assumes comm: "x + y = y + x"
   309 
   310 lemma (in IL4) lcomm: "x + (y + z) = y + (x + z)"
   311 proof -
   312   have "x + (y + z) = (x + y) + z" by (simp add: assoc)
   313   also have "... = (y + x) + z" by (simp add: comm)
   314   also have "... = y + (x + z)" by (simp add: assoc)
   315   finally show ?thesis .
   316 qed
   317 
   318 lemmas (in IL4) AC = comm assoc lcomm
   319 
   320 lemma "(x::i) # y # z # w = y # x # w # z"
   321 proof -
   322   interpret my: IL4 ["op #"]
   323     by (auto intro: IL4.intro IL3.intro IL4_axioms.intro i_assoc i_comm)
   324   show ?thesis by (simp only: my.OP.AC)  (* or simply AC *)
   325 qed
   326 
   327 text {* Locale with definition *}
   328 
   329 text {* This example is admittedly not very creative :-) *}
   330 
   331 locale IL5 = IL4 + var A +
   332   defines A_def: "A == True"
   333 
   334 lemma (in IL5) lem: A
   335   by (unfold A_def) rule
   336 
   337 lemma "IL5(op #) ==> True"
   338 proof -
   339   assume "IL5(op #)"
   340   then interpret IL5 ["op #"] by (auto intro: IL5.axioms)
   341   show ?thesis by (rule lem)  (* lem instantiated to True *)
   342 qed
   343 
   344 text {* Interpretation in a context with target *}
   345 
   346 lemma (in IL4)
   347   fixes A (infixl "$" 60)
   348   assumes A: "IL4(A)"
   349   shows "(x::i) $ y $ z $ w = y $ x $ w $ z"
   350 proof -
   351   from A interpret A: IL4 ["A"] by (auto intro: IL4.axioms)
   352   show ?thesis by (simp only: A.OP.AC)
   353 qed
   354 
   355 
   356 section {* Interpretation in Locales *}
   357 
   358 text {* Naming convention for global objects: prefixes R and r *}
   359 
   360 locale (open) Rsemi = var prod (infixl "**" 65) +
   361   assumes assoc: "(x ** y) ** z = x ** (y ** z)"
   362 
   363 locale (open) Rlgrp = Rsemi + var one + var inv +
   364   assumes lone: "one ** x = x"
   365     and linv: "inv(x) ** x = one"
   366 
   367 lemma (in Rlgrp) lcancel:
   368   "x ** y = x ** z <-> y = z"
   369 proof
   370   assume "x ** y = x ** z"
   371   then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
   372   then show "y = z" by (simp add: lone linv)
   373 qed simp
   374 
   375 locale (open) Rrgrp = Rsemi + var one + var inv +
   376   assumes rone: "x ** one = x"
   377     and rinv: "x ** inv(x) = one"
   378 
   379 lemma (in Rrgrp) rcancel:
   380   "y ** x = z ** x <-> y = z"
   381 proof
   382   assume "y ** x = z ** x"
   383   then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
   384     by (simp add: assoc [symmetric])
   385   then show "y = z" by (simp add: rone rinv)
   386 qed simp
   387 
   388 interpretation Rlgrp < Rrgrp
   389   proof -
   390     {
   391       fix x
   392       have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
   393       then show "x ** one = x" by (simp add: assoc lcancel)
   394     }
   395     note rone = this
   396     {
   397       fix x
   398       have "inv(x) ** x ** inv(x) = inv(x) ** one"
   399 	by (simp add: linv lone rone)
   400       then show "x ** inv(x) = one" by (simp add: assoc lcancel)
   401     }
   402   qed
   403 
   404 (* effect on printed locale *)
   405 
   406 print_locale! Rlgrp
   407 
   408 (* use of derived theorem *)
   409 
   410 lemma (in Rlgrp)
   411   "y ** x = z ** x <-> y = z"
   412   apply (rule rcancel)
   413   print_interps Rrgrp thm lcancel rcancel
   414   done
   415 
   416 (* circular interpretation *)
   417 
   418 interpretation Rrgrp < Rlgrp
   419   proof -
   420     {
   421       fix x
   422       have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
   423       then show "one ** x = x" by (simp add: assoc [symmetric] rcancel)
   424     }
   425     note lone = this
   426     {
   427       fix x
   428       have "inv(x) ** (x ** inv(x)) = one ** inv(x)"
   429 	by (simp add: rinv lone rone)
   430       then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel)
   431     }
   432   qed
   433 
   434 (* effect on printed locale *)
   435 
   436 print_locale! Rrgrp
   437 print_locale! Rlgrp
   438 
   439 (* locale with many parameters ---
   440    interpretations generate alternating group A5 *)
   441 
   442 locale RA5 = var A + var B + var C + var D + var E +
   443   assumes eq: "A <-> B <-> C <-> D <-> E"
   444 
   445 interpretation RA5 < RA5 _ _ D E C
   446 print_facts
   447 print_interps RA5
   448   using A_B_C_D_E.eq apply (blast intro: RA5.intro) done
   449 
   450 interpretation RA5 < RA5 C _ E _ A
   451 print_facts
   452 print_interps RA5
   453   using A_B_C_D_E.eq apply (blast intro: RA5.intro) done
   454 
   455 interpretation RA5 < RA5 B C A _ _
   456 print_facts
   457 print_interps RA5
   458   using A_B_C_D_E.eq apply (blast intro: RA5.intro) done
   459 
   460 interpretation RA5 < RA5 _ C D B _ .
   461   (* Any even permutation of parameters is subsumed by the above. *)
   462 
   463 (* circle of three locales, forward direction *)
   464 
   465 locale (open) RA1 = var A + var B + assumes p: "A <-> B"
   466 locale (open) RA2 = var A + var B + assumes q: "A & B | ~ A & ~ B"
   467 locale (open) RA3 = var A + var B + assumes r: "(A --> B) & (B --> A)"
   468 
   469 interpretation RA1 < RA2
   470   print_facts
   471   using p apply fast done
   472 interpretation RA2 < RA3
   473   print_facts
   474   using q apply fast done
   475 interpretation RA3 < RA1
   476   print_facts
   477   using r apply fast done
   478 
   479 (* circle of three locales, backward direction *)
   480 
   481 locale (open) RB1 = var A + var B + assumes p: "A <-> B"
   482 locale (open) RB2 = var A + var B + assumes q: "A & B | ~ A & ~ B"
   483 locale (open) RB3 = var A + var B + assumes r: "(A --> B) & (B --> A)"
   484 
   485 interpretation RB1 < RB2
   486   print_facts
   487   using p apply fast done
   488 interpretation RB3 < RB1
   489   print_facts
   490   using r apply fast done
   491 interpretation RB2 < RB3
   492   print_facts
   493   using q apply fast done
   494 
   495 lemma (in RB1) True
   496   print_facts
   497   ..
   498 
   499 
   500 (* Group example revisited, with predicates *)
   501 
   502 locale Rpsemi = var prod (infixl "**" 65) +
   503   assumes assoc: "(x ** y) ** z = x ** (y ** z)"
   504 
   505 locale Rplgrp = Rpsemi + var one + var inv +
   506   assumes lone: "one ** x = x"
   507     and linv: "inv(x) ** x = one"
   508 
   509 lemma (in Rplgrp) lcancel:
   510   "x ** y = x ** z <-> y = z"
   511 proof
   512   assume "x ** y = x ** z"
   513   then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
   514   then show "y = z" by (simp add: lone linv)
   515 qed simp
   516 
   517 locale Rprgrp = Rpsemi + var one + var inv +
   518   assumes rone: "x ** one = x"
   519     and rinv: "x ** inv(x) = one"
   520 
   521 lemma (in Rprgrp) rcancel:
   522   "y ** x = z ** x <-> y = z"
   523 proof
   524   assume "y ** x = z ** x"
   525   then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
   526     by (simp add: assoc [symmetric])
   527   then show "y = z" by (simp add: rone rinv)
   528 qed simp
   529 
   530 interpretation Rplgrp < Rprgrp
   531   proof intro_locales
   532     {
   533       fix x
   534       have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
   535       then show "x ** one = x" by (simp add: assoc lcancel)
   536     }
   537     note rone = this
   538     {
   539       fix x
   540       have "inv(x) ** x ** inv(x) = inv(x) ** one"
   541 	by (simp add: linv lone rone)
   542       then show "x ** inv(x) = one" by (simp add: assoc lcancel)
   543     }
   544   qed
   545 
   546 (* effect on printed locale *)
   547 
   548 print_locale! Rplgrp
   549 
   550 (* use of derived theorem *)
   551 
   552 lemma (in Rplgrp)
   553   "y ** x = z ** x <-> y = z"
   554   apply (rule rcancel)
   555   print_interps Rprgrp thm lcancel rcancel
   556   done
   557 
   558 (* circular interpretation *)
   559 
   560 interpretation Rprgrp < Rplgrp
   561   proof intro_locales
   562     {
   563       fix x
   564       have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
   565       then show "one ** x = x" by (simp add: assoc [symmetric] rcancel)
   566     }
   567     note lone = this
   568     {
   569       fix x
   570       have "inv(x) ** (x ** inv(x)) = one ** inv(x)"
   571 	by (simp add: rinv lone rone)
   572       then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel)
   573     }
   574   qed
   575 
   576 (* effect on printed locale *)
   577 
   578 print_locale! Rprgrp
   579 print_locale! Rplgrp
   580 
   581 subsection {* Interaction of Interpretation in Theories and Locales:
   582   in Locale, then in Theory *}
   583 
   584 consts
   585   rone :: i
   586   rinv :: "i => i"
   587 
   588 axioms
   589   r_one : "rone # x = x"
   590   r_inv : "rinv(x) # x = rone"
   591 
   592 interpretation Rbool: Rlgrp ["op #" "rone" "rinv"]
   593 proof -
   594   fix x y z
   595   {
   596     show "(x # y) # z = x # (y # z)" by (rule i_assoc)
   597   next
   598     show "rone # x = x" by (rule r_one)
   599   next
   600     show "rinv(x) # x = rone" by (rule r_inv)
   601   }
   602 qed
   603 
   604 (* derived elements *)
   605 
   606 print_interps Rrgrp
   607 print_interps Rlgrp
   608 
   609 lemma "y # x = z # x <-> y = z" by (rule Rbool.rcancel)
   610 
   611 (* adding lemma to derived element *)
   612 
   613 lemma (in Rrgrp) new_cancel:
   614   "b ** a = c ** a <-> b = c"
   615   by (rule rcancel)
   616 
   617 thm Rbool.new_cancel (* additional prems discharged!! *)
   618 
   619 ML {* check_thm "Rbool.new_cancel" *}
   620 
   621 lemma "b # a = c # a <-> b = c" by (rule Rbool.new_cancel)
   622 
   623 
   624 subsection {* Interaction of Interpretation in Theories and Locales:
   625   in Theory, then in Locale *}
   626 
   627 (* Another copy of the group example *)
   628 
   629 locale Rqsemi = var prod (infixl "**" 65) +
   630   assumes assoc: "(x ** y) ** z = x ** (y ** z)"
   631 
   632 locale Rqlgrp = Rqsemi + var one + var inv +
   633   assumes lone: "one ** x = x"
   634     and linv: "inv(x) ** x = one"
   635 
   636 lemma (in Rqlgrp) lcancel:
   637   "x ** y = x ** z <-> y = z"
   638 proof
   639   assume "x ** y = x ** z"
   640   then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
   641   then show "y = z" by (simp add: lone linv)
   642 qed simp
   643 
   644 locale Rqrgrp = Rqsemi + var one + var inv +
   645   assumes rone: "x ** one = x"
   646     and rinv: "x ** inv(x) = one"
   647 
   648 lemma (in Rqrgrp) rcancel:
   649   "y ** x = z ** x <-> y = z"
   650 proof
   651   assume "y ** x = z ** x"
   652   then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
   653     by (simp add: assoc [symmetric])
   654   then show "y = z" by (simp add: rone rinv)
   655 qed simp
   656 
   657 interpretation Rqrgrp < Rprgrp
   658   apply intro_locales
   659   apply (rule assoc)
   660   apply (rule rone)
   661   apply (rule rinv)
   662   done
   663 
   664 interpretation R2: Rqlgrp ["op #" "rone" "rinv"] 
   665   apply intro_locales  (* FIXME: intro_locales is too eager and shouldn't
   666                           solve this. *)
   667   done
   668 
   669 print_interps Rqsemi
   670 print_interps Rqlgrp
   671 print_interps Rplgrp  (* no interpretations yet *)
   672 
   673 
   674 interpretation Rqlgrp < Rqrgrp
   675   proof intro_locales
   676     {
   677       fix x
   678       have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
   679       then show "x ** one = x" by (simp add: assoc lcancel)
   680     }
   681     note rone = this
   682     {
   683       fix x
   684       have "inv(x) ** x ** inv(x) = inv(x) ** one"
   685 	by (simp add: linv lone rone)
   686       then show "x ** inv(x) = one" by (simp add: assoc lcancel)
   687     }
   688   qed
   689 
   690 print_interps! Rqrgrp
   691 print_interps! Rpsemi  (* witness must not have meta hyps *)
   692 print_interps! Rprgrp  (* witness must not have meta hyps *)
   693 print_interps! Rplgrp  (* witness must not have meta hyps *)
   694 thm R2.rcancel
   695 thm R2.lcancel
   696 
   697 ML {* check_thm "R2.rcancel"; check_thm "R2.lcancel" *}
   698 
   699 
   700 subsection {* Generation of Witness Theorems for Transitive Interpretations *}
   701 
   702 locale Rtriv = var x +
   703   assumes x: "x = x"
   704 
   705 locale Rtriv2 = var x + var y +
   706   assumes x: "x = x" and y: "y = y"
   707 
   708 interpretation Rtriv2 < Rtriv x
   709   apply intro_locales
   710   apply (rule x)
   711   done
   712 
   713 interpretation Rtriv2 < Rtriv y
   714   apply intro_locales
   715   apply (rule y)
   716   done
   717 
   718 print_locale Rtriv2
   719 
   720 locale Rtriv3 = var x + var y + var z +
   721   assumes x: "x = x" and y: "y = y" and z: "z = z"
   722 
   723 interpretation Rtriv3 < Rtriv2 x y
   724   apply intro_locales
   725   apply (rule x)
   726   apply (rule y)
   727   done
   728 
   729 print_locale Rtriv3
   730 
   731 interpretation Rtriv3 < Rtriv2 x z
   732   apply intro_locales
   733   apply (rule x_y_z.x)
   734   apply (rule z)
   735   done
   736 
   737 ML {* set show_types *}
   738 
   739 print_locale Rtriv3
   740 
   741 
   742 subsection {* Normalisation Replaces Assumed Element by Derived Element *}
   743 
   744 typedecl ('a, 'b) pair
   745 arities pair :: ("term", "term") "term"
   746 
   747 consts
   748   pair :: "['a, 'b] => ('a, 'b) pair"
   749   fst :: "('a, 'b) pair => 'a"
   750   snd :: "('a, 'b) pair => 'b"
   751 
   752 axioms
   753   fst [simp]: "fst(pair(x, y)) = x"
   754   snd [simp]: "snd(pair(x, y)) = y"
   755 
   756 locale Rpair = var prod (infixl "**" 65) + var prodP (infixl "***" 65) +
   757   defines P_def: "x *** y == pair(fst(x) ** fst(y), snd(x) ** snd(y))"
   758 
   759 locale Rpair_semi = Rpair + Rpsemi
   760 
   761 interpretation Rpair_semi < Rpsemi prodP (infixl "***" 65)
   762 proof (rule Rpsemi.intro)
   763   fix x y z
   764   show "(x *** y) *** z = x *** (y *** z)"
   765     apply (simp only: P_def) apply (simp add: assoc) (* FIXME: unfold P_def fails *)
   766     done
   767 qed
   768 
   769 locale Rsemi_rev = Rpsemi + var rprod (infixl "++" 65) +
   770   defines r_def: "x ++ y == y ** x"
   771 
   772 lemma (in Rsemi_rev) r_assoc:
   773   "(x ++ y) ++ z = x ++ (y ++ z)"
   774   by (simp add: r_def assoc)
   775 
   776 lemma (in Rpair_semi)
   777   includes Rsemi_rev prodP (infixl "***" 65) rprodP (infixl "+++" 65)
   778   constrains prod :: "['a, 'a] => 'a"
   779     and rprodP :: "[('a, 'a) pair, ('a, 'a) pair] => ('a, 'a) pair"
   780   shows "(x +++ y) +++ z = x +++ (y +++ z)"
   781   apply (rule r_assoc) done
   782 
   783 end