--- 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:
--- 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)
--- 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
--- 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