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
6 Collection of regression tests for locales.
7 *)
9 header {* Test of Locale Interpretation *}
11 theory LocaleTest
12 imports FOL
13 begin
15 ML {* set Toplevel.debug *}
16 ML {* set show_hyps *}
17 ML {* set show_sorts *}
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 *}
34 section {* Context Elements and Locale Expressions *}
36 text {* Naming convention for global objects: prefixes L and l *}
38 subsection {* Renaming with Syntax *}
40 locale LS = var mult +
41   assumes "mult(x, y) = mult(y, x)"
43 print_locale LS
45 locale LS' = LS mult (infixl "**" 60)
47 print_locale LS'
49 locale LT = var mult (infixl "**" 60) +
50   assumes "x ** y = y ** x"
52 locale LU = LT mult (infixl "**" 60) + LT add (infixl "++" 55) + var h +
53   assumes hom: "h(x ** y) = h(x) ++ h(y)"
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 *)
62 locale LV = LU _ add
64 locale LW = LU _ mult (infixl "**" 60)
67 subsection {* Constrains *}
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'
76 section {* Interpretation *}
78 text {* Naming convention for global objects: prefixes I and i *}
80 text {* interpretation input syntax *}
82 locale IL
83 locale IM = fixes a and b and c
85 interpretation test [simp]: IL + IM a b c [x y z] .
87 print_interps IL    (* output: test *)
88 print_interps IM    (* output: test *)
90 interpretation test [simp]: IL print_interps IM .
92 interpretation IL .
94 text {* Processing of locale expression *}
96 locale IA = fixes a assumes asm_A: "a = a"
98 locale IB = fixes b assumes asm_B [simp]: "b = b"
100 locale IC = IA + IB + assumes asm_C: "c = c"
101   (* TODO: independent type var in c, prohibit locale declaration *)
103 locale ID = IA + IB + fixes d defines def_D: "d == (a = b)"
105 theorem (in ID) True ..
107 typedecl i
108 arities i :: "term"
111 interpretation i1: IC ["X::i" "Y::i"] by unfold_locales auto
113 print_interps IA  (* output: i1 *)
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
119 ML {* check_thm "i1.a.asm_A" *}
121 (* without prefix *)
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 *)
127 print_interps IA  (* output: <no prefix>, i1 *)
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
132 ML {* check_thm "asm_C" *}
134 interpretation i2: ID [X "Y::i" "Y = X"]
135   by (simp add: eq_commute) unfold_locales
137 print_interps IA  (* output: <no prefix>, i1 *)
138 print_interps ID  (* output: i2 *)
141 interpretation i3: ID [X "Y::i"] by simp unfold_locales
143 (* duplicate: thm not added *)
145 (* thm i3.a.asm_A *)
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 *)
154 interpretation i10: ID + ID a' b' d' [X "Y::i" _ u "v::i" _] by intro_locales
156 corollary (in ID) th_x: True ..
158 (* possible accesses: for each registration *)
160 thm i2.th_x thm i3.th_x
162 ML {* check_thm "i2.th_x"; check_thm "i3.th_x" *}
164 lemma (in ID) th_y: "d == (a = b)" by (rule d_def)
166 thm i2.th_y thm i3.th_y
168 ML {* check_thm "i2.th_y"; check_thm "i3.th_y" *}
170 lemmas (in ID) th_z = th_y
172 thm i2.th_z
174 ML {* check_thm "i2.th_z" *}
177 subsection {* Interpretation in Proof Contexts *}
179 locale IF = fixes f assumes asm_F: "f & f --> f"
181 consts default :: "'a"
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
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
207 (* Definition involving free variable *)
209 ML {* reset show_sorts *}
211 locale IE = fixes e defines e_def: "e(x) == x & x"
212   notes e_def2 = e_def
214 lemma (in IE) True thm e_def by fast
216 interpretation i7: IE ["%x. x"] by simp
218 thm i7.e_def2 (* has no premise *)
220 ML {* check_thm "i7.e_def2" *}
222 locale IE' = fixes e defines e_def: "e == (%x. x & x)"
223   notes e_def2 = e_def
225 interpretation i7': IE' ["(%x. x)"] by simp
227 thm i7'.e_def2
229 ML {* check_thm "i7'.e_def2" *}
231 (* Definition involving free variable in assm *)
233 locale IG = fixes g assumes asm_G: "g --> x"
234   notes asm_G2 = asm_G
236 interpretation i8: IG ["False"] by unfold_locales fast
238 thm i8.asm_G2
240 ML {* check_thm "i8.asm_G2" *}
242 text {* Locale without assumptions *}
244 locale IL1 = notes rev_conjI [intro] = conjI [THEN iffD1 [OF conj_commute]]
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
253 locale IL11 = notes rev_conjI = conjI [THEN iffD1 [OF conj_commute]]
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
262 subsection {* Simple locale with assumptions *}
264 consts ibin :: "[i, i] => i" (infixl "#" 60)
266 axioms i_assoc: "(x # y) # z = x # (y # z)"
267   i_comm: "x # y = y # x"
269 locale IL2 =
270   fixes OP (infixl "+" 60)
271   assumes assoc: "(x + y) + z = x + (y + z)"
272     and comm: "x + y = y + x"
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
282 lemmas (in IL2) AC = comm assoc lcomm
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
290 subsection {* Nested locale with assumptions *}
292 locale IL3 =
293   fixes OP (infixl "+" 60)
294   assumes assoc: "(x + y) + z = x + (y + z)"
296 locale IL4 = IL3 +
297   assumes comm: "x + y = y + x"
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
307 lemmas (in IL4) AC = comm assoc lcomm
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
316 text {* Locale with definition *}
318 text {* This example is admittedly not very creative :-) *}
320 locale IL5 = IL4 + var A +
321   defines A_def: "A == True"
323 lemma (in IL5) lem: A
324   by (unfold A_def) rule
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
333 text {* Interpretation in a context with target *}
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
345 section {* Interpretation in Locales *}
347 text {* Naming convention for global objects: prefixes R and r *}
349 (* locale with many parameters ---
350    interpretations generate alternating group A5 *)
352 locale RA5 = var A + var B + var C + var D + var E +
353   assumes eq: "A <-> B <-> C <-> D <-> E"
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
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
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
370 interpretation RA5 < RA5 _ C D B _ .
371   (* Any even permutation of parameters is subsumed by the above. *)
373 (* circle of three locales, forward direction *)
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)"
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
389 (* circle of three locales, backward direction *)
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)"
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
405 lemma (in RB1) True
406   print_facts
407   ..
410 (* Group example *)
412 locale Rsemi = var prod (infixl "**" 65) +
413   assumes assoc: "(x ** y) ** z = x ** (y ** z)"
415 locale Rlgrp = Rsemi + var one + var inv +
416   assumes lone: "one ** x = x"
417     and linv: "inv(x) ** x = one"
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
427 locale Rrgrp = Rsemi + var one + var inv +
428   assumes rone: "x ** one = x"
429     and rinv: "x ** inv(x) = one"
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
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
456 (* effect on printed locale *)
458 print_locale! Rlgrp
460 (* use of derived theorem *)
462 lemma (in Rlgrp)
463   "y ** x = z ** x <-> y = z"
464   apply (rule rcancel)
465   print_interps Rrgrp thm lcancel rcancel
466   done
468 (* circular interpretation *)
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
486 (* effect on printed locale *)
488 print_locale! Rrgrp
489 print_locale! Rlgrp
491 subsection {* Interaction of Interpretation in Theories and Locales:
492   in Locale, then in Theory *}
494 consts
495   rone :: i
496   rinv :: "i => i"
498 axioms
499   r_one : "rone # x = x"
500   r_inv : "rinv(x) # x = rone"
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
514 (* derived elements *)
516 print_interps Rrgrp
517 print_interps Rlgrp
519 lemma "y # x = z # x <-> y = z" by (rule Rbool.rcancel)
521 (* adding lemma to derived element *)
523 lemma (in Rrgrp) new_cancel:
524   "b ** a = c ** a <-> b = c"
525   by (rule rcancel)
527 thm Rbool.new_cancel (* additional prems discharged!! *)
529 ML {* check_thm "Rbool.new_cancel" *}
531 lemma "b # a = c # a <-> b = c" by (rule Rbool.new_cancel)
534 subsection {* Interaction of Interpretation in Theories and Locales:
535   in Theory, then in Locale *}
537 (* Another copy of the group example *)
539 locale Rqsemi = var prod (infixl "**" 65) +
540   assumes assoc: "(x ** y) ** z = x ** (y ** z)"
542 locale Rqlgrp = Rqsemi + var one + var inv +
543   assumes lone: "one ** x = x"
544     and linv: "inv(x) ** x = one"
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
554 locale Rqrgrp = Rqsemi + var one + var inv +
555   assumes rone: "x ** one = x"
556     and rinv: "x ** inv(x) = one"
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
567 interpretation Rqrgrp < Rrgrp
568   apply unfold_locales
569   apply (rule assoc)
570   apply (rule rone)
571   apply (rule rinv)
572   done
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
582 print_interps Rqsemi
583 print_interps Rqlgrp
584 print_interps Rlgrp  (* no interpretations yet *)
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
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
610 ML {* check_thm "R2.rcancel"; check_thm "R2.lcancel" *}
613 subsection {* Generation of Witness Theorems for Transitive Interpretations *}
615 locale Rtriv = var x +
616   assumes x: "x = x"
618 locale Rtriv2 = var x + var y +
619   assumes x: "x = x" and y: "y = y"
621 interpretation Rtriv2 < Rtriv x
622   apply unfold_locales
623   apply (rule x)
624   done
626 interpretation Rtriv2 < Rtriv y
627   apply unfold_locales
628   apply (rule y)
629   done
631 print_locale Rtriv2
633 locale Rtriv3 = var x + var y + var z +
634   assumes x: "x = x" and y: "y = y" and z: "z = z"
636 interpretation Rtriv3 < Rtriv2 x y
637   apply unfold_locales
638   apply (rule x)
639   apply (rule y)
640   done
642 print_locale Rtriv3
644 interpretation Rtriv3 < Rtriv2 x z
645   apply unfold_locales
646   apply (rule x_y_z.x)
647   apply (rule z)
648   done
650 ML {* set show_types *}
652 print_locale Rtriv3
655 subsection {* Normalisation Replaces Assumed Element by Derived Element *}
657 typedecl ('a, 'b) pair
658 arities pair :: ("term", "term") "term"
660 consts
661   pair :: "['a, 'b] => ('a, 'b) pair"
662   fst :: "('a, 'b) pair => 'a"
663   snd :: "('a, 'b) pair => 'b"
665 axioms
666   fst [simp]: "fst(pair(x, y)) = x"
667   snd [simp]: "snd(pair(x, y)) = y"
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))"
672 locale Rpair_semi = Rpair + Rsemi
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
682 locale Rsemi_rev = Rsemi + var rprod (infixl "++" 65) +
683   defines r_def: "x ++ y == y ** x"
685 lemma (in Rsemi_rev) r_assoc:
686   "(x ++ y) ++ z = x ++ (y ++ z)"
687   by (simp add: r_def assoc)
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
697 subsection {* Import of Locales with Predicates as Interpretation *}
699 locale Ra =
700   assumes Ra: "True"
702 locale Rb = Ra +
703   assumes Rb: "True"
705 locale Rc = Rb +
706   assumes Rc: "True"
708 print_locale! Rc
711 section {* Interpretation of Defined Concepts *}
713 text {* Naming convention for global objects: prefixes D and d *}
716 subsection {* Simple examples *}
718 locale Da = fixes a :: o
719   assumes true: a
721 text {* In the following examples, @{term "~ a"} is the defined concept. *}
723 lemma (in Da) not_false: "~ a <-> False"
724   apply simp apply (rule true) done
726 interpretation D1: Da ["True"]
727   where "~ True == False"
728   apply -
729   apply unfold_locales  apply rule
730   by simp
732 thm D1.not_false
733 lemma "False <-> False" apply (rule D1.not_false) done
735 interpretation D2: Da ["x | ~ x"]
736   where "~ (x | ~ x) <-> ~ x & x"
737   apply -
738   apply unfold_locales  apply fast
739   by simp
741 thm D2.not_false
742 lemma "~ x & x <-> False" apply (rule D2.not_false) done
744 print_interps! Da
746 (* Subscriptions of interpretations *)
748 lemma (in Da) not_false2: "~a <-> False"
749   apply simp apply (rule true) done
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
755 (* Unfolding in attributes *)
757 locale Db = Da +
758   fixes b :: o
759   assumes a_iff_b: "~a <-> b"
761 lemmas (in Db) not_false_b = not_false [unfolded a_iff_b]
763 interpretation D2: Db ["x | ~ x" "~ (x <-> x)"]
764   apply unfold_locales apply fast done
766 thm D2.not_false_b
767 lemma "~(x <-> x) <-> False" apply (rule D2.not_false_b) done
769 (* Subscription and attributes *)
771 lemmas (in Db) not_false_b2 = not_false [unfolded a_iff_b]
773 thm D2.not_false_b2
774 lemma "~(x <-> x) <-> False" apply (rule D2.not_false_b2) done
776 end