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