# HG changeset patch
# User wenzelm
# Date 1020774459 -7200
# Node ID 8743cc8472244a5d5ce28b91598b405cd97ef7a5
# Parent  f6561b003a35d8885c6dfabdc0bf04aa54f37469
tuned presentation;

diff -r f6561b003a35 -r 8743cc847224 src/HOL/Induct/LFilter.thy
--- a/src/HOL/Induct/LFilter.thy	Tue May 07 14:27:07 2002 +0200
+++ b/src/HOL/Induct/LFilter.thy	Tue May 07 14:27:39 2002 +0200
@@ -29,7 +29,7 @@
                                           | LCons y z => Some(y,z))"
 
 
-subsection {* findRel: basic laws *}
+subsection {* @{text findRel}: basic laws *}
 
 inductive_cases
   findRel_LConsE [elim!]: "(LCons x l, l'') \<in> findRel p"
@@ -47,7 +47,7 @@
 by (blast elim: findRel.cases)
 
 
-subsection {* Properties of Domain (findRel p) *}
+subsection {* Properties of @{text "Domain (findRel p)"} *}
 
 lemma LCons_Domain_findRel [simp]:
      "LCons x l \<in> Domain(findRel p) = (p x | l \<in> Domain(findRel p))"
@@ -64,7 +64,7 @@
 done
 
 
-subsection {* find: basic equations *}
+subsection {* @{text find}: basic equations *}
 
 lemma find_LNil [simp]: "find p LNil = LNil"
 by (unfold find_def, blast)
@@ -92,7 +92,7 @@
 
 
 
-subsection {* lfilter: basic equations *}
+subsection {* @{text lfilter}: basic equations *}
 
 lemma lfilter_LNil [simp]: "lfilter p LNil = LNil"
 by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp)
@@ -144,7 +144,7 @@
 done
 
 
-subsection {* lfilter: simple facts by coinduction *}
+subsection {* @{text lfilter}: simple facts by coinduction *}
 
 lemma lfilter_K_True: "lfilter (%x. True) l = l"
 by (rule_tac l = "l" in llist_fun_equalityI, simp_all)
@@ -152,7 +152,7 @@
 lemma lfilter_idem: "lfilter p (lfilter p l) = lfilter p l"
 apply (rule_tac l = "l" in llist_fun_equalityI, simp_all)
 apply safe
-txt{*Cases: p x is true or false*}
+txt{*Cases: @{text "p x"} is true or false*}
 apply (rule lfilter_cases [THEN disjE])
  apply (erule ssubst, auto)
 done
@@ -204,21 +204,22 @@
 apply (case_tac "l \<in> Domain (findRel q)")
  apply (subgoal_tac [2] "l ~: Domain (findRel (%x. p x & q x))")
   prefer 3 apply (blast intro: rev_subsetD [OF _ Domain_findRel_mono])
- txt{*There are no qs in l: both lists are LNil*}
+ txt{*There are no @{text qs} in @{text l}: both lists are @{text LNil}*}
  apply (simp_all add: Domain_findRel_iff, clarify) 
-txt{*case q x*}
+txt{*case @{text "q x"}*}
 apply (case_tac "p x")
  apply (simp_all add: findRel_conj [THEN findRel_imp_lfilter])
- txt{*case q x and ~(p x) *}
+ txt{*case @{text "q x"} and @{text "~(p x)"} *}
 apply (case_tac "l' \<in> Domain (findRel (%x. p x & q x))")
- txt{*subcase: there is no p&q in l' and therefore none in l*}
+ txt{*subcase: there is no @{text "p & q"} in @{text l'} and therefore none in @{text l}*}
  apply (subgoal_tac [2] "l ~: Domain (findRel (%x. p x & q x))")
   prefer 3 apply (blast intro: findRel_not_conj_Domain)
  apply (subgoal_tac [2] "lfilter q l' ~: Domain (findRel p) ")
   prefer 3 apply (blast intro: findRel_lfilter_Domain_conj)
- txt{*    ...and therefore too, no p in lfilter q l'.  Both results are Lnil*}
+ txt{*    {\dots} and therefore too, no @{text p} in @{text "lfilter q l'"}.
+   Both results are @{text LNil}*}
  apply (simp_all add: Domain_findRel_iff, clarify) 
-txt{*subcase: there is a p&q in l' and therefore also one in l*}
+txt{*subcase: there is a @{text "p & q"} in @{text l'} and therefore also one in @{text l} *}
 apply (subgoal_tac " (l, LCons xa l'a) \<in> findRel (%x. p x & q x) ")
  prefer 2 apply (blast intro: findRel_conj2)
 apply (subgoal_tac " (lfilter q l', LCons xa (lfilter q l'a)) \<in> findRel p")
@@ -234,7 +235,7 @@
 
 
 subsection {* Numerous lemmas required to prove ??:
-     lfilter p (lmap f l) = lmap f (lfilter (%x. p(f x)) l)
+     @{text "lfilter p (lmap f l) = lmap f (lfilter (%x. p(f x)) l)"}
  *}
 
 lemma findRel_lmap_Domain:
diff -r f6561b003a35 -r 8743cc847224 src/HOL/Induct/LList.thy
--- a/src/HOL/Induct/LList.thy	Tue May 07 14:27:07 2002 +0200
+++ b/src/HOL/Induct/LList.thy	Tue May 07 14:27:39 2002 +0200
@@ -21,7 +21,7 @@
        (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))`r)"
 *)
 
-header {*Definition of type 'a llist by a greatest fixed point*}
+header {*Definition of type llist by a greatest fixed point*}
 
 theory LList = Main + SList:
 
@@ -95,12 +95,12 @@
 
 
 
-text{*The case syntax for type 'a llist*}
+text{* The case syntax for type @{text "'a llist"} *}
 translations
   "case p of LNil => a | LCons x l => b" == "llist_case a (%x l. b) p"
 
 
-subsubsection{* Sample function definitions.  Item-based ones start with L *}
+subsubsection{* Sample function definitions.  Item-based ones start with @{text L} *}
 
 constdefs
   Lmap       :: "('a item => 'b item) => ('a item => 'b item)"
@@ -134,7 +134,7 @@
 *}
 
 text{*
-SHOULD LListD_Fun_CONS_I, etc., be equations (for rewriting)?
+SHOULD @{text LListD_Fun_CONS_I}, etc., be equations (for rewriting)?
 *}
 
 lemmas UN1_I = UNIV_I [THEN UN_I, standard]
@@ -156,8 +156,11 @@
            elim: llist.cases [unfolded NIL_def CONS_def])
 
 
-subsection{* Type checking by coinduction, using list_Fun 
-     THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS!
+subsection{* Type checking by coinduction *}
+
+text {*
+  {\dots} using @{text list_Fun} THE COINDUCTIVE DEFINITION PACKAGE
+  COULD DO THIS!
 *}
 
 lemma llist_coinduct: 
@@ -176,7 +179,7 @@
 done
 
 
-text{*Utilise the "strong" part, i.e. gfp(f)*}
+text{*Utilise the ``strong'' part, i.e. @{text "gfp(f)"}*}
 lemma list_Fun_llist_I: "M \<in> llist(A) ==> M \<in> list_Fun A (X Un llist(A))"
 apply (unfold llist.defs list_Fun_def)
 apply (rule gfp_fun_UnI2) 
@@ -184,7 +187,7 @@
 apply assumption
 done
 
-subsection{* LList_corec satisfies the desired recurion equation *}
+subsection{* @{text LList_corec} satisfies the desired recurion equation *}
 
 text{*A continuity result?*}
 lemma CONS_UN1: "CONS M (\<Union>x. f(x)) = (\<Union>x. CONS M (f x))"
@@ -220,7 +223,7 @@
 apply (rule_tac a="Suc(?k)" in UN_I, simp, simp)+ 
 done
 
-text{*the recursion equation for LList_corec -- NOT SUITABLE FOR REWRITING!*}
+text{*the recursion equation for @{text LList_corec} -- NOT SUITABLE FOR REWRITING!*}
 lemma LList_corec:
      "LList_corec a f =   
       (case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f))"
@@ -232,8 +235,8 @@
       ==> h(a) = (case f a of None => NIL | Some(z,w) => CONS z (h w))"
 by (simp add: LList_corec)
 
-text{*A typical use of co-induction to show membership in the gfp. 
-  Bisimulation is  range(%x. LList_corec x f) *}
+text{*A typical use of co-induction to show membership in the @{text gfp}. 
+  Bisimulation is @{text "range(%x. LList_corec x f)"} *}
 lemma LList_corec_type: "LList_corec a f \<in> llist UNIV"
 apply (rule_tac X = "range (%x. LList_corec x ?g) " in llist_coinduct)
 apply (rule rangeI, safe)
@@ -241,7 +244,7 @@
 done
 
 
-subsection{* llist equality as a gfp; the bisimulation principle *}
+subsection{* @{text llist} equality as a @{text gfp}; the bisimulation principle *}
 
 text{*This theorem is actually used, unlike the many similar ones in ZF*}
 lemma LListD_unfold: "LListD r = dsum (diag {Numb 0}) (dprod r (LListD r))"
@@ -260,17 +263,17 @@
 apply (simp_all add: CONS_def less_Suc_eq)
 done
 
-text{*The domain of the LListD relation*}
+text{*The domain of the @{text LListD} relation*}
 lemma Domain_LListD: 
     "Domain (LListD(diag A)) <= llist(A)"
 apply (unfold llist.defs NIL_def CONS_def)
 apply (rule gfp_upperbound)
-txt{*avoids unfolding LListD on the rhs*}
+txt{*avoids unfolding @{text LListD} on the rhs*}
 apply (rule_tac P = "%x. Domain x <= ?B" in LListD_unfold [THEN ssubst], simp)
 apply blast 
 done
 
-text{*This inclusion justifies the use of coinduction to show M=N*}
+text{*This inclusion justifies the use of coinduction to show @{text "M = N"}*}
 lemma LListD_subset_diag: "LListD(diag A) <= diag(llist(A))"
 apply (rule subsetI)
 apply (rule_tac p = "x" in PairE, safe)
@@ -280,9 +283,9 @@
 done
 
 
-subsubsection{* Coinduction, using LListD_Fun
-    THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS!
- *}
+subsubsection{* Coinduction, using @{text LListD_Fun} *}
+
+text {* THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS! *}
 
 lemma LListD_Fun_mono: "A<=B ==> LListD_Fun r A <= LListD_Fun r B"
 apply (unfold LListD_Fun_def)
@@ -304,7 +307,7 @@
 apply (unfold LListD_Fun_def CONS_def, blast)
 done
 
-text{*Utilise the "strong" part, i.e. gfp(f)*}
+text{*Utilise the "strong" part, i.e. @{text "gfp(f)"}*}
 lemma LListD_Fun_LListD_I:
      "M \<in> LListD(r) ==> M \<in> LListD_Fun r (X Un LListD(r))"
 apply (unfold LListD.defs LListD_Fun_def)
@@ -314,7 +317,7 @@
 done
 
 
-text{*This converse inclusion helps to strengthen LList_equalityI*}
+text{*This converse inclusion helps to strengthen @{text LList_equalityI}*}
 lemma diag_subset_LListD: "diag(llist(A)) <= LListD(diag A)"
 apply (rule subsetI)
 apply (erule LListD_coinduct)
@@ -338,7 +341,7 @@
 
 subsubsection{* To show two LLists are equal, exhibit a bisimulation! 
       [also admits true equality]
-   Replace "A" by some particular set, like {x.True}??? *}
+   Replace @{text A} by some particular set, like @{text "{x. True}"}??? *}
 lemma LList_equalityI:
      "[| (M,N) \<in> r;  r <= LListD_Fun (diag A) (r Un diag(llist(A))) |] 
       ==>  M=N"
@@ -348,10 +351,10 @@
 done
 
 
-subsection{* Finality of llist(A): Uniqueness of functions defined by corecursion *}
+subsection{* Finality of @{text "llist(A)"}: Uniqueness of functions defined by corecursion *}
 
-text{*We must remove Pair_eq because it may turn an instance of reflexivity
-  (h1 b, h2 b) = (h1 ?x17, h2 ?x17) into a conjunction! 
+text{*We must remove @{text Pair_eq} because it may turn an instance of reflexivity
+  @{text "(h1 b, h2 b) = (h1 ?x17, h2 ?x17)"} into a conjunction! 
   (or strengthen the Solver?) 
 *}
 declare Pair_eq [simp del]
@@ -407,7 +410,7 @@
 done
 
 
-subsection{*Lconst: defined directly by lfp *}
+subsection{*Lconst: defined directly by @{text lfp} *}
 
 text{*But it could be defined by corecursion.*}
 
@@ -416,11 +419,11 @@
 apply assumption 
 done
 
-text{* Lconst(M) = CONS M (Lconst M) *}
+text{* @{text "Lconst(M) = CONS M (Lconst M)"} *}
 lemmas Lconst = Lconst_fun_mono [THEN Lconst_def [THEN def_lfp_unfold]]
 
 text{*A typical use of co-induction to show membership in the gfp.
-  The containing set is simply the singleton {Lconst(M)}. *}
+  The containing set is simply the singleton @{text "{Lconst(M)}"}. *}
 lemma Lconst_type: "M\<in>A ==> Lconst(M): llist(A)"
 apply (rule singletonI [THEN llist_coinduct], safe)
 apply (rule_tac P = "%u. u \<in> ?A" in Lconst [THEN ssubst])
@@ -478,7 +481,7 @@
             rangeI Rep_LList [THEN LListD])+
 done
 
-subsubsection{* Injectiveness of CONS and LCons *}
+subsubsection{* Injectiveness of @{text CONS} and @{text LCons} *}
 
 lemma CONS_CONS_eq2: "(CONS M N=CONS M' N') = (M=M' & N=N')"
 apply (unfold CONS_def)
@@ -505,9 +508,9 @@
 done
 
 
-subsection{* Reasoning about llist(A) *}
+subsection{* Reasoning about @{text "llist(A)"} *}
 
-text{*A special case of list_equality for functions over lazy lists*}
+text{*A special case of @{text list_equality} for functions over lazy lists*}
 lemma LList_fun_equalityI:
  "[| M \<in> llist(A); g(NIL): llist(A);                              
      f(NIL)=g(NIL);                                              
@@ -524,7 +527,7 @@
 done
 
 
-subsection{* The functional "Lmap" *}
+subsection{* The functional @{text Lmap} *}
 
 lemma Lmap_NIL [simp]: "Lmap f NIL = NIL"
 by (rule Lmap_def [THEN def_LList_corec, THEN trans], simp)
@@ -541,13 +544,13 @@
 apply (erule llist.cases, simp_all)
 done
 
-text{*This type checking rule synthesises a sufficiently large set for f*}
+text{*This type checking rule synthesises a sufficiently large set for @{text f}*}
 lemma Lmap_type2: "M \<in> llist(A) ==> Lmap f M \<in> llist(f`A)"
 apply (erule Lmap_type)
 apply (erule imageI)
 done
 
-subsubsection{* Two easy results about Lmap *}
+subsubsection{* Two easy results about @{text Lmap} *}
 
 lemma Lmap_compose: "M \<in> llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)"
 apply (unfold o_def)
@@ -567,7 +570,7 @@
 done
 
 
-subsection{* Lappend -- its two arguments cause some complications! *}
+subsection{* @{text Lappend} -- its two arguments cause some complications! *}
 
 lemma Lappend_NIL_NIL [simp]: "Lappend NIL NIL = NIL"
 apply (unfold Lappend_def)
@@ -597,7 +600,7 @@
 by (erule LList_fun_equalityI, simp_all)
 
 
-subsubsection{* Alternative type-checking proofs for Lappend *}
+subsubsection{* Alternative type-checking proofs for @{text Lappend} *}
 
 text{*weak co-induction: bisimulation and case analysis on both variables*}
 lemma Lappend_type: "[| M \<in> llist(A); N \<in> llist(A) |] ==> Lappend M N \<in> llist(A)"
@@ -618,9 +621,9 @@
 apply (simp add: list_Fun_llist_I, simp)
 done
 
-subsection{* Lazy lists as the type 'a llist -- strongly typed versions of above *}
+subsection{* Lazy lists as the type @{text "'a llist"} -- strongly typed versions of above *}
 
-subsubsection{* llist_case: case analysis for 'a llist *}
+subsubsection{* @{text llist_case}: case analysis for @{text "'a llist"} *}
 
 declare LListI [THEN Abs_LList_inverse, simp]
 declare Rep_LList_inverse [simp]
@@ -644,9 +647,9 @@
 apply (simp add: Rep_LList_LCons [symmetric] Rep_LList_inject, blast) 
 done
 
-subsubsection{* llist_corec: corecursion for 'a llist *}
+subsubsection{* @{text llist_corec}: corecursion for @{text "'a llist"} *}
 
-text{*Lemma for the proof of llist_corec*}
+text{*Lemma for the proof of @{text llist_corec}*}
 lemma LList_corec_type2:
      "LList_corec a  
            (%z. case f z of None => None | Some(v,w) => Some(Leaf(v),w)) 
@@ -672,9 +675,9 @@
       h(a) = (case f a of None => LNil | Some(z,w) => LCons z (h w))"
 by (simp add: llist_corec)
 
-subsection{* Proofs about type 'a llist functions *}
+subsection{* Proofs about type @{text "'a llist"} functions *}
 
-subsection{* Deriving llist_equalityI -- llist equality is a bisimulation *}
+subsection{* Deriving @{text llist_equalityI} -- @{text llist} equality is a bisimulation *}
 
 lemma LListD_Fun_subset_Times_llist: 
     "r <= (llist A) <*> (llist A) ==>  
@@ -704,7 +707,7 @@
 apply (fast elim: LListI [THEN Abs_LList_inverse, THEN subst])
 done
 
-text{*Used with lfilter*}
+text{*Used with @{text lfilter}*}
 lemma llistD_Fun_mono: 
     "A<=B ==> llistD_Fun A <= llistD_Fun B"
 apply (unfold llistD_Fun_def prod_fun_def, auto)
@@ -730,7 +733,7 @@
 apply (rule diag_subset_Times)
 done
 
-subsubsection{* Rules to prove the 2nd premise of llist_equalityI *}
+subsubsection{* Rules to prove the 2nd premise of @{text llist_equalityI} *}
 lemma llistD_Fun_LNil_I [simp]: "(LNil,LNil) \<in> llistD_Fun(r)"
 apply (unfold llistD_Fun_def LNil_def)
 apply (rule LListD_Fun_NIL_I [THEN prod_fun_imageI])
@@ -743,7 +746,7 @@
 apply (erule prod_fun_imageI)
 done
 
-text{*Utilise the "strong" part, i.e. gfp(f)*}
+text{*Utilise the "strong" part, i.e. @{text "gfp(f)"}*}
 lemma llistD_Fun_range_I: "(l,l) \<in> llistD_Fun(r Un range(%x.(x,x)))"
 apply (unfold llistD_Fun_def)
 apply (rule Rep_LList_inverse [THEN subst])
@@ -753,7 +756,7 @@
 apply (rule Rep_LList [THEN LListD, THEN LListD_Fun_diag_I])
 done
 
-text{*A special case of list_equality for functions over lazy lists*}
+text{*A special case of @{text list_equality} for functions over lazy lists*}
 lemma llist_fun_equalityI:
      "[| f(LNil)=g(LNil);                                                 
          !!x l. (f(LCons x l),g(LCons x l)) 
@@ -766,7 +769,7 @@
 done
 
 
-subsection{* The functional "lmap" *}
+subsection{* The functional @{text lmap} *}
 
 lemma lmap_LNil [simp]: "lmap f LNil = LNil"
 by (rule lmap_def [THEN def_llist_corec, THEN trans], simp)
@@ -775,7 +778,7 @@
 by (rule lmap_def [THEN def_llist_corec, THEN trans], simp)
 
 
-subsubsection{* Two easy results about lmap *}
+subsubsection{* Two easy results about @{text lmap} *}
 
 lemma lmap_compose [simp]: "lmap (f o g) l = lmap f (lmap g l)"
 by (rule_tac l = "l" in llist_fun_equalityI, simp_all)
@@ -784,7 +787,7 @@
 by (rule_tac l = "l" in llist_fun_equalityI, simp_all)
 
 
-subsection{* iterates -- llist_fun_equalityI cannot be used! *}
+subsection{* iterates -- @{text llist_fun_equalityI} cannot be used! *}
 
 lemma iterates: "iterates f x = LCons x (iterates f (f x))"
 by (rule iterates_def [THEN def_llist_corec, THEN trans], simp)
@@ -803,7 +806,8 @@
 
 subsection{* A rather complex proof about iterates -- cf Andy Pitts *}
 
-subsubsection{* Two lemmas about natrec n x (%m.g), which is essentially (g^n)(x) *}
+subsubsection{* Two lemmas about @{text "natrec n x (%m. g)"}, which is essentially
+  @{text "(g^n)(x)"} *}
 
 lemma fun_power_lmap: "nat_rec (LCons b l) (%m. lmap(f)) n =       
      LCons (nat_rec b (%m. f) n) (nat_rec l (%m. lmap(f)) n)"
@@ -816,8 +820,8 @@
 lemmas Pair_cong = refl [THEN cong, THEN cong, of concl: Pair]
 
 
-text{*The bisimulation consists of {(lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u)))}
-  for all u and all n::nat.*}
+text{*The bisimulation consists of @{text "{(lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u)))}"}
+  for all @{text u} and all @{text "n::nat"}.*}
 lemma iterates_equality:
      "(!!x. h(x) = LCons x (lmap f (h x))) ==> h = iterates(f)"
 apply (rule ext)
@@ -839,7 +843,7 @@
 done
 
 
-subsection{* lappend -- its two arguments cause some complications! *}
+subsection{* @{text lappend} -- its two arguments cause some complications! *}
 
 lemma lappend_LNil_LNil [simp]: "lappend LNil LNil = LNil"
 apply (unfold lappend_def)
@@ -873,7 +877,7 @@
 apply (subst iterates, simp)
 done
 
-subsubsection{* Two proofs that lmap distributes over lappend *}
+subsubsection{* Two proofs that @{text lmap} distributes over lappend *}
 
 text{*Long proof requiring case analysis on both both arguments*}
 lemma lmap_lappend_distrib:
@@ -888,7 +892,7 @@
 apply (blast intro: llistD_Fun_LCons_I) 
 done
 
-text{*Shorter proof of theorem above using llist_equalityI as strong coinduction*}
+text{*Shorter proof of theorem above using @{text llist_equalityI} as strong coinduction*}
 lemma lmap_lappend_distrib:
      "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)"
 apply (rule_tac l = "l" in llist_fun_equalityI, simp)
diff -r f6561b003a35 -r 8743cc847224 src/HOL/ex/Locales.thy
--- a/src/HOL/ex/Locales.thy	Tue May 07 14:27:07 2002 +0200
+++ b/src/HOL/ex/Locales.thy	Tue May 07 14:27:39 2002 +0200
@@ -338,9 +338,10 @@
 lemma
   includes group G
   includes group H
-  shows "x \<cdot> y \<cdot> \<one> = prod G (prod G x y) (one G)" and
-  "x \<cdot>\<^sub>2 y \<cdot>\<^sub>2 \<one>\<^sub>2 = prod H (prod H x y) (one H)" and
-  "x \<cdot> \<one>\<^sub>2 = prod G x (one H)" by (rule refl)+
+  shows "x \<cdot> y \<cdot> \<one> = prod G (prod G x y) (one G)"
+    and "x \<cdot>\<^sub>2 y \<cdot>\<^sub>2 \<one>\<^sub>2 = prod H (prod H x y) (one H)"
+    and "x \<cdot> \<one>\<^sub>2 = prod G x (one H)"
+  by (rule refl)+
 
 text {*
   Note that the trivial statements above need to be given as a
diff -r f6561b003a35 -r 8743cc847224 src/HOL/ex/set.thy
--- a/src/HOL/ex/set.thy	Tue May 07 14:27:07 2002 +0200
+++ b/src/HOL/ex/set.thy	Tue May 07 14:27:39 2002 +0200
@@ -2,176 +2,190 @@
     ID:         $Id$
     Author:     Tobias Nipkow and Lawrence C Paulson
     Copyright   1991  University of Cambridge
+*)
 
-Set Theory examples: Cantor's Theorem, Schroeder-Berstein Theorem, etc.
-*)
+header {* Set Theory examples: Cantor's Theorem, Schröder-Berstein Theorem, etc. *}
 
 theory set = Main:
 
-text{*These two are cited in Benzmueller and Kohlhase's system description 
-of LEO, CADE-15, 1998 (pages 139-143) as theorems LEO could not prove.*}
+text{*
+  These two are cited in Benzmueller and Kohlhase's system description
+  of LEO, CADE-15, 1998 (pages 139-143) as theorems LEO could not
+  prove.
+*}
 
-lemma "(X = Y Un Z) = (Y<=X & Z<=X & (ALL V. Y<=V & Z<=V --> X<=V))"
-by blast
-
-lemma "(X = Y Int Z) = (X<=Y & X<=Z & (ALL V. V<=Y & V<=Z --> V<=X))"
-by blast
+lemma "(X = Y \<union> Z) =
+    (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
+  by blast
 
-text{*trivial example of term synthesis: apparently hard for some provers!*}
-lemma "a ~= b ==> a:?X & b ~: ?X"
-by blast
+lemma "(X = Y \<inter> Z) =
+    (X \<subseteq> Y \<and> X \<subseteq> Z \<and> (\<forall>V. V \<subseteq> Y \<and> V \<subseteq> Z \<longrightarrow> V \<subseteq> X))"
+  by blast
 
-(** Examples for the Blast_tac paper **)
+text {*
+  Trivial example of term synthesis: apparently hard for some provers!
+*}
 
-text{*Union-image, called Un_Union_image on equalities.ML*}
-lemma "(UN x:C. f(x) Un g(x)) = Union(f`C)  Un  Union(g`C)"
-by blast
+lemma "a \<noteq> b \<Longrightarrow> a \<in> ?X \<and> b \<notin> ?X"
+  by blast
+
+
+subsection {* Examples for the @{text blast} paper *}
 
-text{*Inter-image, called Int_Inter_image on equalities.ML*}
-lemma "(INT x:C. f(x) Int g(x)) = Inter(f`C) Int Inter(g`C)"
-by blast
+lemma "(\<Union>x \<in> C. f x \<union> g x) = \<Union>(f ` C)  \<union>  \<Union>(g ` C)"
+  -- {* Union-image, called @{text Un_Union_image} in Main HOL *}
+  by blast
 
-text{*Singleton I.  Nice demonstration of blast_tac--and its limitations.
-For some unfathomable reason, UNIV_I increases the search space greatly*}
-lemma "!!S::'a set set. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}"
-by (blast del: UNIV_I)
+lemma "(\<Inter>x \<in> C. f x \<inter> g x) = \<Inter>(f ` C) \<inter> \<Inter>(g ` C)"
+  -- {* Inter-image, called @{text Int_Inter_image} in Main HOL *}
+  by blast
 
-text{*Singleton II.  variant of the benchmark above*}
-lemma "ALL x:S. Union(S) <= x ==> EX z. S <= {z}"
-by (blast del: UNIV_I)
-
-text{* A unique fixpoint theorem --- fast/best/meson all fail *}
+lemma "\<And>S::'a set set. \<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
+  -- {* Singleton I.  Nice demonstration of @{text blast}--and its limitations. *}
+  -- {* For some unfathomable reason, @{text UNIV_I} increases the search space greatly. *}
+  by (blast del: UNIV_I)
 
-lemma "EX! x. f(g(x))=x ==> EX! y. g(f(y))=y"
-apply (erule ex1E, rule ex1I, erule arg_cong)
-apply (rule subst, assumption, erule allE, rule arg_cong, erule mp) 
-apply (erule arg_cong) 
-done
+lemma "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
+  -- {*Singleton II.  Variant of the benchmark above. *}
+  by (blast del: UNIV_I)
+
+lemma "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
+  -- {* A unique fixpoint theorem --- @{text fast}/@{text best}/@{text meson} all fail. *}
+  apply (erule ex1E, rule ex1I, erule arg_cong)
+  apply (rule subst, assumption, erule allE, rule arg_cong, erule mp)
+  apply (erule arg_cong)
+  done
 
 
 
-text{* Cantor's Theorem: There is no surjection from a set to its powerset. *}
+subsection {* Cantor's Theorem: There is no surjection from a set to its powerset *}
 
-text{*requires best-first search because it is undirectional*}
-lemma cantor1: "~ (EX f:: 'a=>'a set. ALL S. EX x. f(x) = S)"
-by best
+lemma cantor1: "\<not> (\<exists>f:: 'a \<Rightarrow> 'a set. \<forall>S. \<exists>x. f x = S)"
+  -- {* Requires best-first search because it is undirectional. *}
+  by best
 
-text{*This form displays the diagonal term*}
-lemma "ALL f:: 'a=>'a set. ALL x. f(x) ~= ?S(f)"
-by best
+lemma "\<forall>f:: 'a \<Rightarrow> 'a set. \<forall>x. f x \<noteq> ?S f"
+  -- {*This form displays the diagonal term. *}
+  by best
 
-text{*This form exploits the set constructs*}
-lemma "?S ~: range(f :: 'a=>'a set)"
-by (rule notI, erule rangeE, best)  
+lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
+  -- {* This form exploits the set constructs. *}
+  by (rule notI, erule rangeE, best)
 
-text{*Or just this!*}
-lemma "?S ~: range(f :: 'a=>'a set)"
-by best
+lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
+  -- {* Or just this! *}
+  by best
+
 
-text{* The Schroeder-Berstein Theorem *}
+subsection {* The Schröder-Berstein Theorem *}
 
-lemma disj_lemma: "[| -(f`X) = g`(-X);  f(a)=g(b);  a:X |] ==> b:X"
-by blast
+lemma disj_lemma: "- (f ` X) = g ` (-X) \<Longrightarrow> f a = g b \<Longrightarrow> a \<in> X \<Longrightarrow> b \<in> X"
+  by blast
 
 lemma surj_if_then_else:
-     "-(f`X) = g`(-X) ==> surj(%z. if z:X then f(z) else g(z))"
-by (simp add: surj_def, blast)
+  "-(f ` X) = g ` (-X) \<Longrightarrow> surj (\<lambda>z. if z \<in> X then f z else g z)"
+  by (simp add: surj_def) blast
 
-lemma bij_if_then_else: 
-     "[| inj_on f X;  inj_on g (-X);  -(f`X) = g`(-X);  
-         h = (%z. if z:X then f(z) else g(z)) |]        
-      ==> inj(h) & surj(h)"
-apply (unfold inj_on_def)
-apply (simp add: surj_if_then_else)
-apply (blast dest: disj_lemma sym)
-done
+lemma bij_if_then_else:
+  "inj_on f X \<Longrightarrow> inj_on g (-X) \<Longrightarrow> -(f ` X) = g ` (-X) \<Longrightarrow>
+    h = (\<lambda>z. if z \<in> X then f z else g z) \<Longrightarrow> inj h \<and> surj h"
+  apply (unfold inj_on_def)
+  apply (simp add: surj_if_then_else)
+  apply (blast dest: disj_lemma sym)
+  done
 
-lemma decomposition: "EX X. X = - (g`(- (f`X)))"
-apply (rule exI)
-apply (rule lfp_unfold)
-apply (rule monoI, blast) 
-done
+lemma decomposition: "\<exists>X. X = - (g ` (- (f ` X)))"
+  apply (rule exI)
+  apply (rule lfp_unfold)
+  apply (rule monoI, blast)
+  done
 
-text{*Schroeder-Bernstein Theorem*}
-lemma "[| inj (f:: 'a=>'b);  inj (g:: 'b=>'a) |]  
-       ==> EX h:: 'a=>'b. inj(h) & surj(h)"
-apply (rule decomposition [THEN exE])
-apply (rule exI)
-apply (rule bij_if_then_else)
-   apply (rule_tac [4] refl)
-  apply (rule_tac [2] inj_on_inv)
-  apply (erule subset_inj_on [OF subset_UNIV]) 
-  txt{*tricky variable instantiations!*}
- apply (erule ssubst, subst double_complement)
- apply (rule subsetI, erule imageE, erule ssubst, rule rangeI) 
-apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])
-done
+theorem Schroeder_Bernstein:
+  "inj (f :: 'a \<Rightarrow> 'b) \<Longrightarrow> inj (g :: 'b \<Rightarrow> 'a)
+    \<Longrightarrow> \<exists>h:: 'a \<Rightarrow> 'b. inj h \<and> surj h"
+  apply (rule decomposition [THEN exE])
+  apply (rule exI)
+  apply (rule bij_if_then_else)
+     apply (rule_tac [4] refl)
+    apply (rule_tac [2] inj_on_inv)
+    apply (erule subset_inj_on [OF subset_UNIV])
+   txt {* Tricky variable instantiations! *}
+   apply (erule ssubst, subst double_complement)
+   apply (rule subsetI, erule imageE, erule ssubst, rule rangeI)
+  apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])
+  done
 
 
-text{*Set variable instantiation examples from 
-W. W. Bledsoe and Guohui Feng, SET-VAR.
-JAR 11 (3), 1993, pages 293-314.
+subsection {* Set variable instantiation examples *}
 
-Isabelle can prove the easy examples without any special mechanisms, but it
-can't prove the hard ones.
+text {*
+  From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages
+  293-314.
+
+  Isabelle can prove the easy examples without any special mechanisms,
+  but it can't prove the hard ones.
 *}
 
-text{*Example 1, page 295.*}
-lemma "(EX A. (ALL x:A. x <= (0::int)))"
-by force 
+lemma "\<exists>A. (\<forall>x \<in> A. x \<le> (0::int))"
+  -- {* Example 1, page 295. *}
+  by force
 
-text{*Example 2*}
-lemma "D : F --> (EX G. (ALL A:G. EX B:F. A <= B))";
-by force 
+lemma "D \<in> F \<Longrightarrow> \<exists>G. \<forall>A \<in> G. \<exists>B \<in> F. A \<subseteq> B"
+  -- {* Example 2. *}
+  by force
 
-text{*Example 3*}
-lemma "P(a) --> (EX A. (ALL x:A. P(x)) & (EX y. y:A))";
-by force 
+lemma "P a \<Longrightarrow> \<exists>A. (\<forall>x \<in> A. P x) \<and> (\<exists>y. y \<in> A)"
+  -- {* Example 3. *}
+  by force
 
-text{*Example 4*}
-lemma "a<b & b<(c::int) --> (EX A. a~:A & b:A & c~: A)"
-by force 
+lemma "a < b \<and> b < (c::int) \<Longrightarrow> \<exists>A. a \<notin> A \<and> b \<in> A \<and> c \<notin> A"
+  -- {* Example 4. *}
+  by force
 
-text{*Example 5, page 298.*}
-lemma "P(f(b)) --> (EX s A. (ALL x:A. P(x)) & f(s):A)";
-by force 
+lemma "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
+  -- {*Example 5, page 298. *}
+  by force
 
-text{*Example 6*}
-lemma "P(f(b)) --> (EX s A. (ALL x:A. P(x)) & f(s):A)";
-by force 
+lemma "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
+  -- {* Example 6. *}
+  by force
 
-text{*Example 7*}
-lemma "EX A. a ~: A"
-by force 
+lemma "\<exists>A. a \<notin> A"
+  -- {* Example 7. *}
+  by force
 
-text{*Example 8*}
-lemma "(ALL u v. u < (0::int) --> u ~= abs v) --> (EX A::int set. (ALL y. abs y ~: A) & -2 : A)"
-by force  text{*not blast, which can't simplify -2<0*}
+lemma "(\<forall>u v. u < (0::int) \<longrightarrow> u \<noteq> abs v)
+    \<longrightarrow> (\<exists>A::int set. (\<forall>y. abs y \<notin> A) \<and> -2 \<in> A)"
+  -- {* Example 8. *}
+  by force  -- {* not @{text blast}, which can't simplify @{text "-2 < 0"} *}
 
-text{*Example 9 omitted (requires the reals)*}
+text {* Example 9 omitted (requires the reals). *}
 
-text{*The paper has no Example 10!*}
+text {* The paper has no Example 10! *}
 
-text{*Example 11: needs a hint*}
-lemma "(ALL A. 0:A & (ALL x:A. Suc(x):A) --> n:A) & 
-       P(0) & (ALL x. P(x) --> P(Suc(x))) --> P(n)"
-apply clarify
-apply (drule_tac x="{x. P x}" in spec)
-by force  
+lemma "(\<forall>A. 0 \<in> A \<and> (\<forall>x \<in> A. Suc x \<in> A) \<longrightarrow> n \<in> A) \<and>
+  P 0 \<and> (\<forall>x. P x \<longrightarrow> P (Suc x)) \<longrightarrow> P n"
+  -- {* Example 11: needs a hint. *}
+  apply clarify
+  apply (drule_tac x = "{x. P x}" in spec)
+  apply force
+  done
 
-text{*Example 12*}
-lemma "(ALL A. (0,0):A & (ALL x y. (x,y):A --> (Suc(x),Suc(y)):A) --> (n,m):A)
-       & P(n) --> P(m)"
-by auto 
+lemma
+  "(\<forall>A. (0, 0) \<in> A \<and> (\<forall>x y. (x, y) \<in> A \<longrightarrow> (Suc x, Suc y) \<in> A) \<longrightarrow> (n, m) \<in> A)
+    \<and> P n \<longrightarrow> P m"
+  -- {* Example 12. *}
+  by auto
 
-text{*Example EO1: typo in article, and with the obvious fix it seems
-      to require arithmetic reasoning.*}
-lemma "(ALL x. (EX u. x=2*u) = (~(EX v. Suc x = 2*v))) --> 
-       (EX A. ALL x. (x : A) = (Suc x ~: A))"
-apply clarify 
-apply (rule_tac x="{x. EX u. x = 2*u}" in exI, auto) 
-apply (case_tac v, auto)
-apply (drule_tac x="Suc v" and P="%x. ?a(x) ~= ?b(x)" in spec, force) 
-done
+lemma
+  "(\<forall>x. (\<exists>u. x = 2 * u) = (\<not> (\<exists>v. Suc x = 2 * v))) \<longrightarrow>
+    (\<exists>A. \<forall>x. (x \<in> A) = (Suc x \<notin> A))"
+  -- {* Example EO1: typo in article, and with the obvious fix it seems
+      to require arithmetic reasoning. *}
+  apply clarify
+  apply (rule_tac x = "{x. \<exists>u. x = 2 * u}" in exI, auto)
+   apply (case_tac v, auto)
+  apply (drule_tac x = "Suc v" and P = "\<lambda>x. ?a x \<noteq> ?b x" in spec, force)
+  done
 
 end