# HG changeset patch
# User paulson
# Date 1331225009 0
# Node ID 49b91b716cbeab62e5302a0579d8ca74db9e7a9d
# Parent  57bf0cecb36609fe4b0e82870e8bf33520c605c7
Structured and calculation-based proofs (with new trans rules!)

diff -r 57bf0cecb366 -r 49b91b716cbe src/ZF/Cardinal.thy
--- a/src/ZF/Cardinal.thy	Tue Mar 06 17:01:37 2012 +0000
+++ b/src/ZF/Cardinal.thy	Thu Mar 08 16:43:29 2012 +0000
@@ -101,7 +101,7 @@
 apply (blast intro: bij_converse_bij)
 done
 
-lemma eqpoll_trans:
+lemma eqpoll_trans [trans]:
     "[| X \<approx> Y;  Y \<approx> Z |] ==> X \<approx> Z"
 apply (unfold eqpoll_def)
 apply (blast intro: comp_bij)
@@ -122,11 +122,17 @@
 lemma eqpoll_imp_lepoll: "X \<approx> Y ==> X \<lesssim> Y"
 by (unfold eqpoll_def bij_def lepoll_def, blast)
 
-lemma lepoll_trans: "[| X \<lesssim> Y;  Y \<lesssim> Z |] ==> X \<lesssim> Z"
+lemma lepoll_trans [trans]: "[| X \<lesssim> Y;  Y \<lesssim> Z |] ==> X \<lesssim> Z"
 apply (unfold lepoll_def)
 apply (blast intro: comp_inj)
 done
 
+lemma eq_lepoll_trans [trans]: "[| X \<approx> Y;  Y \<lesssim> Z |] ==> X \<lesssim> Z"
+ by (blast intro: eqpoll_imp_lepoll lepoll_trans) 
+
+lemma lepoll_eq_trans [trans]: "[| X \<lesssim> Y;  Y \<approx> Z |] ==> X \<lesssim> Z"
+ by (blast intro: eqpoll_imp_lepoll lepoll_trans) 
+
 (*Asymmetry law*)
 lemma eqpollI: "[| X \<lesssim> Y;  Y \<lesssim> X |] ==> X \<approx> Y"
 apply (unfold lepoll_def eqpoll_def)
@@ -194,7 +200,7 @@
 done
 
 lemma inj_not_surj_succ:
-  "[| f \<in> inj(A, succ(m)); f \<notin> surj(A, succ(m)) |] ==> \<exists>f. f:inj(A,m)"
+  "[| f \<in> inj(A, succ(m)); f \<notin> surj(A, succ(m)) |] ==> \<exists>f. f \<in> inj(A,m)"
 apply (unfold inj_def surj_def)
 apply (safe del: succE)
 apply (erule swap, rule exI)
@@ -208,24 +214,32 @@
 
 (** Variations on transitivity **)
 
-lemma lesspoll_trans:
+lemma lesspoll_trans [trans]:
       "[| X \<prec> Y; Y \<prec> Z |] ==> X \<prec> Z"
 apply (unfold lesspoll_def)
 apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
 done
 
-lemma lesspoll_trans1:
+lemma lesspoll_trans1 [trans]:
       "[| X \<lesssim> Y; Y \<prec> Z |] ==> X \<prec> Z"
 apply (unfold lesspoll_def)
 apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
 done
 
-lemma lesspoll_trans2:
+lemma lesspoll_trans2 [trans]:
       "[| X \<prec> Y; Y \<lesssim> Z |] ==> X \<prec> Z"
 apply (unfold lesspoll_def)
 apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
 done
 
+lemma eq_lesspoll_trans [trans]:
+      "[| X \<approx> Y; Y \<prec> Z |] ==> X \<prec> Z"
+  by (blast intro: eqpoll_imp_lepoll lesspoll_trans1) 
+
+lemma lesspoll_eq_trans [trans]:
+      "[| X \<prec> Y; Y \<approx> Z |] ==> X \<prec> Z"
+  by (blast intro: eqpoll_imp_lepoll lesspoll_trans2) 
+
 
 (** LEAST -- the least number operator [from HOL/Univ.ML] **)
 
@@ -311,6 +325,9 @@
 (* @{term"Ord(A) ==> |A| \<approx> A"} *)
 lemmas Ord_cardinal_eqpoll = well_ord_Memrel [THEN well_ord_cardinal_eqpoll]
 
+lemma Ord_cardinal_idem: "Ord(A) \<Longrightarrow> ||A|| = |A|"
+ by (rule Ord_cardinal_eqpoll [THEN cardinal_cong])
+
 lemma well_ord_cardinal_eqE:
      "[| well_ord(X,r);  well_ord(Y,s);  |X| = |Y| |] ==> X \<approx> Y"
 apply (rule eqpoll_sym [THEN eqpoll_trans])
@@ -335,7 +352,7 @@
 apply (erule sym)
 done
 
-(* Could replace the  @{term"~(j \<approx> i)"}  by  @{term"~(i \<lesssim> j)"}. *)
+(* Could replace the  @{term"~(j \<approx> i)"}  by  @{term"~(i \<preceq> j)"}. *)
 lemma CardI: "[| Ord(i);  !!j. j<i ==> ~(j \<approx> i) |] ==> Card(i)"
 apply (unfold Card_def cardinal_def)
 apply (subst Least_equality)
@@ -399,15 +416,18 @@
 done
 
 (*Kunen's Lemma 10.5*)
-lemma cardinal_eq_lemma: "[| |i| \<le> j;  j \<le> i |] ==> |j| = |i|"
-apply (rule eqpollI [THEN cardinal_cong])
-apply (erule le_imp_lepoll)
-apply (rule lepoll_trans)
-apply (erule_tac [2] le_imp_lepoll)
-apply (rule eqpoll_sym [THEN eqpoll_imp_lepoll])
-apply (rule Ord_cardinal_eqpoll)
-apply (elim ltE Ord_succD)
-done
+lemma cardinal_eq_lemma: 
+  assumes i:"|i| \<le> j" and j: "j \<le> i" shows "|j| = |i|"
+proof (rule eqpollI [THEN cardinal_cong])
+  show "j \<lesssim> i" by (rule le_imp_lepoll [OF j])
+next
+  have Oi: "Ord(i)" using j by (rule le_Ord2)
+  hence "i \<approx> |i|" 
+    by (blast intro: Ord_cardinal_eqpoll eqpoll_sym) 
+  also have "... \<lesssim> j" 
+    by (blast intro: le_imp_lepoll i) 
+  finally show "i \<lesssim> j" .
+qed
 
 lemma cardinal_mono: "i \<le> j ==> |i| \<le> |j|"
 apply (rule_tac i = "|i|" and j = "|j|" in Ord_linear_le)
@@ -438,19 +458,20 @@
 
 (*Can use AC or finiteness to discharge first premise*)
 lemma well_ord_lepoll_imp_Card_le:
-     "[| well_ord(B,r);  A \<lesssim> B |] ==> |A| \<le> |B|"
-apply (rule_tac i = "|A|" and j = "|B|" in Ord_linear_le)
-apply (safe intro!: Ord_cardinal le_eqI)
-apply (rule eqpollI [THEN cardinal_cong], assumption)
-apply (rule lepoll_trans)
-apply (rule well_ord_cardinal_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll], assumption)
-apply (erule le_imp_lepoll [THEN lepoll_trans])
-apply (rule eqpoll_imp_lepoll)
-apply (unfold lepoll_def)
-apply (erule exE)
-apply (rule well_ord_cardinal_eqpoll)
-apply (erule well_ord_rvimage, assumption)
-done
+  assumes wB: "well_ord(B,r)" and AB: "A \<lesssim> B"
+  shows "|A| \<le> |B|"
+proof (rule Ord_linear_le [of "|A|" "|B|", OF Ord_cardinal Ord_cardinal], assumption)
+  assume BA: "|B| \<le> |A|"
+  from lepoll_well_ord [OF AB wB]
+  obtain s where s: "well_ord(A, s)" by blast
+  have "B  \<approx> |B|" by (blast intro: wB eqpoll_sym well_ord_cardinal_eqpoll) 
+  also have "... \<lesssim> |A|" by (rule le_imp_lepoll [OF BA])
+  also have "... \<approx> A" by (rule well_ord_cardinal_eqpoll [OF s])
+  finally have "B \<lesssim> A" .
+  hence "A \<approx> B" by (blast intro: eqpollI AB) 
+  hence "|A| = |B|" by (rule cardinal_cong)
+  thus ?thesis by simp
+qed
 
 lemma lepoll_cardinal_le: "[| A \<lesssim> i; Ord(i) |] ==> |A| \<le> i"
 apply (rule le_trans)
@@ -535,14 +556,6 @@
 lemma succ_lepoll_natE: "[| succ(n) \<lesssim> n;  n:nat |] ==> P"
 by (rule nat_lepoll_imp_le [THEN lt_irrefl], auto)
 
-lemma n_lesspoll_nat: "n \<in> nat ==> n \<prec> nat"
-apply (unfold lesspoll_def)
-apply (fast elim!: Ord_nat [THEN [2] ltI [THEN leI, THEN le_imp_lepoll]]
-                   eqpoll_sym [THEN eqpoll_imp_lepoll]
-    intro: Ord_nat [THEN [2] nat_succI [THEN ltI], THEN leI,
-                 THEN le_imp_lepoll, THEN lepoll_trans, THEN succ_lepoll_natE])
-done
-
 lemma nat_lepoll_imp_ex_eqpoll_n:
      "[| n \<in> nat;  nat \<lesssim> X |] ==> \<exists>Y. Y \<subseteq> X & n \<approx> Y"
 apply (unfold lepoll_def eqpoll_def)
@@ -627,6 +640,9 @@
 apply (erule cardinal_mono)
 done
 
+lemma n_lesspoll_nat: "n \<in> nat ==> n \<prec> nat"
+  by (blast intro: Ord_nat Card_nat ltI lt_Card_imp_lesspoll)
+
 
 subsection{*Towards Cardinal Arithmetic *}
 (** Congruence laws for successor, cardinal addition and multiplication **)
diff -r 57bf0cecb366 -r 49b91b716cbe src/ZF/CardinalArith.thy
--- a/src/ZF/CardinalArith.thy	Tue Mar 06 17:01:37 2012 +0000
+++ b/src/ZF/CardinalArith.thy	Thu Mar 08 16:43:29 2012 +0000
@@ -48,36 +48,38 @@
   cmult  (infixl "\<otimes>" 70)
 
 
-lemma Card_Union [simp,intro,TC]: "(\<forall>x\<in>A. Card(x)) ==> Card(\<Union>(A))"
-apply (rule CardI)
- apply (simp add: Card_is_Ord)
-apply (clarify dest!: ltD)
-apply (drule bspec, assumption)
-apply (frule lt_Card_imp_lesspoll, blast intro: ltI Card_is_Ord)
-apply (drule eqpoll_sym [THEN eqpoll_imp_lepoll])
-apply (drule lesspoll_trans1, assumption)
-apply (subgoal_tac "B \<lesssim> \<Union>A")
- apply (drule lesspoll_trans1, assumption, blast)
-apply (blast intro: subset_imp_lepoll)
-done
+lemma Card_Union [simp,intro,TC]: 
+  assumes A: "\<And>x. x\<in>A \<Longrightarrow> Card(x)" shows "Card(\<Union>(A))"
+proof (rule CardI)
+  show "Ord(\<Union>A)" using A 
+    by (simp add: Card_is_Ord)
+next
+  fix j
+  assume j: "j < \<Union>A"
+  hence "\<exists>c\<in>A. j < c & Card(c)" using A
+    by (auto simp add: lt_def intro: Card_is_Ord)
+  then obtain c where c: "c\<in>A" "j < c" "Card(c)"
+    by blast
+  hence jls: "j \<prec> c" 
+    by (simp add: lt_Card_imp_lesspoll) 
+  { assume eqp: "j \<approx> \<Union>A"
+    hence Uls: "\<Union>A \<prec> c" using jls
+      by (blast intro: eqpoll_sym eqpoll_imp_lepoll lesspoll_trans1)
+    moreover have  "c \<lesssim> \<Union>A" using c
+      by (blast intro: subset_imp_lepoll)
+    ultimately have "c \<prec> c"
+      by (blast intro: lesspoll_trans1) 
+    hence False 
+      by auto
+  } thus "\<not> j \<approx> \<Union>A" by blast
+qed
 
 lemma Card_UN: "(!!x. x:A ==> Card(K(x))) ==> Card(\<Union>x\<in>A. K(x))"
-by (blast intro: Card_Union)
+  by blast
 
 lemma Card_OUN [simp,intro,TC]:
      "(!!x. x:A ==> Card(K(x))) ==> Card(\<Union>x<A. K(x))"
-by (simp add: OUnion_def Card_0)
-
-lemma n_lesspoll_nat: "n \<in> nat ==> n \<prec> nat"
-apply (unfold lesspoll_def)
-apply (rule conjI)
-apply (erule OrdmemD [THEN subset_imp_lepoll], rule Ord_nat)
-apply (rule notI)
-apply (erule eqpollE)
-apply (rule succ_lepoll_natE)
-apply (blast intro: nat_succI [THEN OrdmemD, THEN subset_imp_lepoll]
-                    lepoll_trans, assumption)
-done
+  by (auto simp add: OUnion_def Card_0)
 
 lemma in_Card_imp_lesspoll: "[| Card(K); b \<in> K |] ==> b \<prec> K"
 apply (unfold lesspoll_def)
@@ -103,11 +105,10 @@
 subsubsection{*Cardinal addition is commutative*}
 
 lemma sum_commute_eqpoll: "A+B \<approx> B+A"
-apply (unfold eqpoll_def)
-apply (rule exI)
-apply (rule_tac c = "case(Inr,Inl)" and d = "case(Inr,Inl)" in lam_bijective)
-apply auto
-done
+proof (unfold eqpoll_def, rule exI)
+  show "(\<lambda>z\<in>A+B. case(Inr,Inl,z)) \<in> bij(A+B, B+A)"
+    by (auto intro: lam_bijective [where d = "case(Inr,Inl)"]) 
+qed
 
 lemma cadd_commute: "i \<oplus> j = j \<oplus> i"
 apply (unfold cadd_def)
@@ -153,10 +154,10 @@
 subsubsection{*Addition by another cardinal*}
 
 lemma sum_lepoll_self: "A \<lesssim> A+B"
-apply (unfold lepoll_def inj_def)
-apply (rule_tac x = "\<lambda>x\<in>A. Inl (x) " in exI)
-apply simp
-done
+proof (unfold lepoll_def, rule exI)
+  show "(\<lambda>x\<in>A. Inl (x)) \<in> inj(A, A + B)"
+    by (simp add: inj_def) 
+qed
 
 (*Could probably weaken the premises to well_ord(K,r), or removing using AC*)
 
diff -r 57bf0cecb366 -r 49b91b716cbe src/ZF/Int_ZF.thy
--- a/src/ZF/Int_ZF.thy	Tue Mar 06 17:01:37 2012 +0000
+++ b/src/ZF/Int_ZF.thy	Thu Mar 08 16:43:29 2012 +0000
@@ -707,7 +707,7 @@
 apply auto
 done
 
-lemma zless_trans: "[| x $< y; y $< z |] ==> x $< z"
+lemma zless_trans [trans]: "[| x $< y; y $< z |] ==> x $< z"
 apply (subgoal_tac "intify (x) $< intify (z) ")
 apply (rule_tac [2] y = "intify (y) " in zless_trans_lemma)
 apply auto
@@ -750,19 +750,19 @@
 apply (blast intro: zless_trans)
 done
 
-lemma zle_trans: "[| x $<= y; y $<= z |] ==> x $<= z"
+lemma zle_trans [trans]: "[| x $<= y; y $<= z |] ==> x $<= z"
 apply (subgoal_tac "intify (x) $<= intify (z) ")
 apply (rule_tac [2] y = "intify (y) " in zle_trans_lemma)
 apply auto
 done
 
-lemma zle_zless_trans: "[| i $<= j; j $< k |] ==> i $< k"
+lemma zle_zless_trans [trans]: "[| i $<= j; j $< k |] ==> i $< k"
 apply (auto simp add: zle_def)
 apply (blast intro: zless_trans)
 apply (simp add: zless_def zdiff_def zadd_def)
 done
 
-lemma zless_zle_trans: "[| i $< j; j $<= k |] ==> i $< k"
+lemma zless_zle_trans [trans]: "[| i $< j; j $<= k |] ==> i $< k"
 apply (auto simp add: zle_def)
 apply (blast intro: zless_trans)
 apply (simp add: zless_def zdiff_def zminus_def)
diff -r 57bf0cecb366 -r 49b91b716cbe src/ZF/OrderType.thy
--- a/src/ZF/OrderType.thy	Tue Mar 06 17:01:37 2012 +0000
+++ b/src/ZF/OrderType.thy	Thu Mar 08 16:43:29 2012 +0000
@@ -74,8 +74,7 @@
   The smaller ordinal is an initial segment of the larger *)
 lemma lt_pred_Memrel:
     "j<i ==> pred(i, j, Memrel(i)) = j"
-apply (unfold pred_def lt_def)
-apply (simp (no_asm_simp))
+apply (simp add: pred_def lt_def)
 apply (blast intro: Ord_trans)
 done
 
diff -r 57bf0cecb366 -r 49b91b716cbe src/ZF/Ordinal.thy
--- a/src/ZF/Ordinal.thy	Tue Mar 06 17:01:37 2012 +0000
+++ b/src/ZF/Ordinal.thy	Thu Mar 08 16:43:29 2012 +0000
@@ -9,7 +9,7 @@
 
 definition
   Memrel        :: "i=>i"  where
-    "Memrel(A)   == {z: A*A . \<exists>x y. z=<x,y> & x:y }"
+    "Memrel(A)   == {z\<in>A*A . \<exists>x y. z=<x,y> & x\<in>y }"
 
 definition
   Transset  :: "i=>o"  where
@@ -21,7 +21,7 @@
 
 definition
   lt        :: "[i,i] => o"  (infixl "<" 50)   (*less-than on ordinals*)  where
-    "i<j         == i:j & Ord(j)"
+    "i<j         == i\<in>j & Ord(j)"
 
 definition
   Limit         :: "i=>o"  where
@@ -56,11 +56,11 @@
 subsubsection{*Consequences of Downwards Closure*}
 
 lemma Transset_doubleton_D:
-    "[| Transset(C); {a,b}: C |] ==> a:C & b: C"
+    "[| Transset(C); {a,b}: C |] ==> a\<in>C & b\<in>C"
 by (unfold Transset_def, blast)
 
 lemma Transset_Pair_D:
-    "[| Transset(C); <a,b>: C |] ==> a:C & b: C"
+    "[| Transset(C); <a,b>\<in>C |] ==> a\<in>C & b\<in>C"
 apply (simp add: Pair_def)
 apply (blast dest: Transset_doubleton_D)
 done
@@ -96,11 +96,11 @@
 by (unfold Transset_def, blast)
 
 lemma Transset_Union_family:
-    "[| !!i. i:A ==> Transset(i) |] ==> Transset(\<Union>(A))"
+    "[| !!i. i\<in>A ==> Transset(i) |] ==> Transset(\<Union>(A))"
 by (unfold Transset_def, blast)
 
 lemma Transset_Inter_family:
-    "[| !!i. i:A ==> Transset(i) |] ==> Transset(\<Inter>(A))"
+    "[| !!i. i\<in>A ==> Transset(i) |] ==> Transset(\<Inter>(A))"
 by (unfold Inter_def Transset_def, blast)
 
 lemma Transset_UN:
@@ -115,22 +115,22 @@
 subsection{*Lemmas for Ordinals*}
 
 lemma OrdI:
-    "[| Transset(i);  !!x. x:i ==> Transset(x) |]  ==>  Ord(i)"
+    "[| Transset(i);  !!x. x\<in>i ==> Transset(x) |]  ==>  Ord(i)"
 by (simp add: Ord_def)
 
 lemma Ord_is_Transset: "Ord(i) ==> Transset(i)"
 by (simp add: Ord_def)
 
 lemma Ord_contains_Transset:
-    "[| Ord(i);  j:i |] ==> Transset(j) "
+    "[| Ord(i);  j\<in>i |] ==> Transset(j) "
 by (unfold Ord_def, blast)
 
 
-lemma Ord_in_Ord: "[| Ord(i);  j:i |] ==> Ord(j)"
+lemma Ord_in_Ord: "[| Ord(i);  j\<in>i |] ==> Ord(j)"
 by (unfold Ord_def Transset_def, blast)
 
 (*suitable for rewriting PROVIDED i has been fixed*)
-lemma Ord_in_Ord': "[| j:i; Ord(i) |] ==> Ord(j)"
+lemma Ord_in_Ord': "[| j\<in>i; Ord(i) |] ==> Ord(j)"
 by (blast intro: Ord_in_Ord)
 
 (* Ord(succ(j)) ==> Ord(j) *)
@@ -139,13 +139,13 @@
 lemma Ord_subset_Ord: "[| Ord(i);  Transset(j);  j<=i |] ==> Ord(j)"
 by (simp add: Ord_def Transset_def, blast)
 
-lemma OrdmemD: "[| j:i;  Ord(i) |] ==> j<=i"
+lemma OrdmemD: "[| j\<in>i;  Ord(i) |] ==> j<=i"
 by (unfold Ord_def Transset_def, blast)
 
-lemma Ord_trans: "[| i:j;  j:k;  Ord(k) |] ==> i:k"
+lemma Ord_trans: "[| i\<in>j;  j\<in>k;  Ord(k) |] ==> i\<in>k"
 by (blast dest: OrdmemD)
 
-lemma Ord_succ_subsetI: "[| i:j;  Ord(j) |] ==> succ(i) \<subseteq> j"
+lemma Ord_succ_subsetI: "[| i\<in>j;  Ord(j) |] ==> succ(i) \<subseteq> j"
 by (blast dest: OrdmemD)
 
 
@@ -172,28 +172,33 @@
 apply (blast intro!: Transset_Int)
 done
 
-(*There is no set of all ordinals, for then it would contain itself*)
-lemma ON_class: "~ (\<forall>i. i:X <-> Ord(i))"
-apply (rule notI)
-apply (frule_tac x = X in spec)
-apply (safe elim!: mem_irrefl)
-apply (erule swap, rule OrdI [OF _ Ord_is_Transset])
-apply (simp add: Transset_def)
-apply (blast intro: Ord_in_Ord)+
-done
+text{*There is no set of all ordinals, for then it would contain itself*}
+lemma ON_class: "~ (\<forall>i. i\<in>X <-> Ord(i))"
+proof (rule notI)
+  assume X: "\<forall>i. i \<in> X \<longleftrightarrow> Ord(i)"
+  have "\<forall>x y. x\<in>X \<longrightarrow> y\<in>x \<longrightarrow> y\<in>X"
+    by (simp add: X, blast intro: Ord_in_Ord)
+  hence "Transset(X)"
+     by (auto simp add: Transset_def)
+  moreover have "\<And>x. x \<in> X \<Longrightarrow> Transset(x)"
+     by (simp add: X Ord_def)
+  ultimately have "Ord(X)" by (rule OrdI)
+  hence "X \<in> X" by (simp add: X)
+  thus "False" by (rule mem_irrefl)
+qed
 
 subsection{*< is 'less Than' for Ordinals*}
 
-lemma ltI: "[| i:j;  Ord(j) |] ==> i<j"
+lemma ltI: "[| i\<in>j;  Ord(j) |] ==> i<j"
 by (unfold lt_def, blast)
 
 lemma ltE:
-    "[| i<j;  [| i:j;  Ord(i);  Ord(j) |] ==> P |] ==> P"
+    "[| i<j;  [| i\<in>j;  Ord(i);  Ord(j) |] ==> P |] ==> P"
 apply (unfold lt_def)
 apply (blast intro: Ord_in_Ord)
 done
 
-lemma ltD: "i<j ==> i:j"
+lemma ltD: "i<j ==> i\<in>j"
 by (erule ltE, assumption)
 
 lemma not_lt0 [simp]: "~ i<0"
@@ -211,7 +216,7 @@
 (* i<0 ==> R *)
 lemmas lt0E = not_lt0 [THEN notE, elim!]
 
-lemma lt_trans: "[| i<j;  j<k |] ==> i<k"
+lemma lt_trans [trans]: "[| i<j;  j<k |] ==> i<k"
 by (blast intro!: ltI elim!: ltE intro: Ord_trans)
 
 lemma lt_not_sym: "i<j ==> ~ (j<i)"
@@ -238,10 +243,10 @@
 
 (*Equivalently, i<j ==> i < succ(j)*)
 lemma leI: "i<j ==> i \<le> j"
-by (simp (no_asm_simp) add: le_iff)
+by (simp add: le_iff)
 
 lemma le_eqI: "[| i=j;  Ord(j) |] ==> i \<le> j"
-by (simp (no_asm_simp) add: le_iff)
+by (simp add: le_iff)
 
 lemmas le_refl = refl [THEN le_eqI]
 
@@ -268,7 +273,7 @@
 subsection{*Natural Deduction Rules for Memrel*}
 
 (*The lemmas MemrelI/E give better speed than [iff] here*)
-lemma Memrel_iff [simp]: "<a,b> \<in> Memrel(A) <-> a:b & a:A & b:A"
+lemma Memrel_iff [simp]: "<a,b> \<in> Memrel(A) <-> a\<in>b & a\<in>A & b\<in>A"
 by (unfold Memrel_def, blast)
 
 lemma MemrelI [intro!]: "[| a: b;  a: A;  b: A |] ==> <a,b> \<in> Memrel(A)"
@@ -276,7 +281,7 @@
 
 lemma MemrelE [elim!]:
     "[| <a,b> \<in> Memrel(A);
-        [| a: A;  b: A;  a:b |]  ==> P |]
+        [| a: A;  b: A;  a\<in>b |]  ==> P |]
      ==> P"
 by auto
 
@@ -314,7 +319,7 @@
 
 (*If Transset(A) then Memrel(A) internalizes the membership relation below A*)
 lemma Transset_Memrel_iff:
-    "Transset(A) ==> <a,b> \<in> Memrel(A) <-> a:b & b:A"
+    "Transset(A) ==> <a,b> \<in> Memrel(A) <-> a\<in>b & b\<in>A"
 by (unfold Transset_def, blast)
 
 
@@ -352,7 +357,7 @@
 subsubsection{*Proving That < is a Linear Ordering on the Ordinals*}
 
 lemma Ord_linear [rule_format]:
-     "Ord(i) ==> (\<forall>j. Ord(j) \<longrightarrow> i:j | i=j | j:i)"
+     "Ord(i) ==> (\<forall>j. Ord(j) \<longrightarrow> i\<in>j | i=j | j\<in>i)"
 apply (erule trans_induct)
 apply (rule impI [THEN allI])
 apply (erule_tac i=j in trans_induct)
@@ -386,7 +391,7 @@
 
 subsubsection{*Some Rewrite Rules for <, le*}
 
-lemma Ord_mem_iff_lt: "Ord(j) ==> i:j <-> i<j"
+lemma Ord_mem_iff_lt: "Ord(j) ==> i\<in>j <-> i<j"
 by (unfold lt_def, blast)
 
 lemma not_lt_iff_le: "[| Ord(i);  Ord(j) |] ==> ~ i<j <-> j \<le> i"
@@ -508,7 +513,7 @@
 done
 
 lemma Un_least_mem_iff:
-    "[| Ord(i); Ord(j); Ord(k) |] ==> i \<union> j \<in> k  <->  i:k & j:k"
+    "[| Ord(i); Ord(j); Ord(k) |] ==> i \<union> j \<in> k  <->  i\<in>k & j\<in>k"
 apply (insert Un_least_lt_iff [of i j k])
 apply (simp add: lt_def)
 done
@@ -529,13 +534,13 @@
 by (simp add: Ord_Un_if lt_Ord le_Ord2)
 
 lemma lt_Un_iff:
-     "[| Ord(i); Ord(j) |] ==> k < i \<union> j <-> k < i | k < j";
+     "[| Ord(i); Ord(j) |] ==> k < i \<union> j <-> k < i | k < j"
 apply (simp add: Ord_Un_if not_lt_iff_le)
 apply (blast intro: leI lt_trans2)+
 done
 
 lemma le_Un_iff:
-     "[| Ord(i); Ord(j) |] ==> k \<le> i \<union> j <-> k \<le> i | k \<le> j";
+     "[| Ord(i); Ord(j) |] ==> k \<le> i \<union> j <-> k \<le> i | k \<le> j"
 by (simp add: succ_Un_distrib lt_Un_iff [symmetric])
 
 lemma Un_upper1_lt: "[|k < i; Ord(j)|] ==> k < i \<union> j"
@@ -551,17 +556,17 @@
 
 subsection{*Results about Limits*}
 
-lemma Ord_Union [intro,simp,TC]: "[| !!i. i:A ==> Ord(i) |] ==> Ord(\<Union>(A))"
+lemma Ord_Union [intro,simp,TC]: "[| !!i. i\<in>A ==> Ord(i) |] ==> Ord(\<Union>(A))"
 apply (rule Ord_is_Transset [THEN Transset_Union_family, THEN OrdI])
 apply (blast intro: Ord_contains_Transset)+
 done
 
 lemma Ord_UN [intro,simp,TC]:
-     "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(\<Union>x\<in>A. B(x))"
+     "[| !!x. x\<in>A ==> Ord(B(x)) |] ==> Ord(\<Union>x\<in>A. B(x))"
 by (rule Ord_Union, blast)
 
 lemma Ord_Inter [intro,simp,TC]:
-    "[| !!i. i:A ==> Ord(i) |] ==> Ord(\<Inter>(A))"
+    "[| !!i. i\<in>A ==> Ord(i) |] ==> Ord(\<Inter>(A))"
 apply (rule Transset_Inter_family [THEN OrdI])
 apply (blast intro: Ord_is_Transset)
 apply (simp add: Inter_def)
@@ -569,19 +574,19 @@
 done
 
 lemma Ord_INT [intro,simp,TC]:
-    "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(\<Inter>x\<in>A. B(x))"
+    "[| !!x. x\<in>A ==> Ord(B(x)) |] ==> Ord(\<Inter>x\<in>A. B(x))"
 by (rule Ord_Inter, blast)
 
 
 (* No < version of this theorem: consider that @{term"(\<Union>i\<in>nat.i)=nat"}! *)
 lemma UN_least_le:
-    "[| Ord(i);  !!x. x:A ==> b(x) \<le> i |] ==> (\<Union>x\<in>A. b(x)) \<le> i"
+    "[| Ord(i);  !!x. x\<in>A ==> b(x) \<le> i |] ==> (\<Union>x\<in>A. b(x)) \<le> i"
 apply (rule le_imp_subset [THEN UN_least, THEN subset_imp_le])
 apply (blast intro: Ord_UN elim: ltE)+
 done
 
 lemma UN_succ_least_lt:
-    "[| j<i;  !!x. x:A ==> b(x)<j |] ==> (\<Union>x\<in>A. succ(b(x))) < i"
+    "[| j<i;  !!x. x\<in>A ==> b(x)<j |] ==> (\<Union>x\<in>A. succ(b(x))) < i"
 apply (rule ltE, assumption)
 apply (rule UN_least_le [THEN lt_trans2])
 apply (blast intro: succ_leI)+
@@ -608,7 +613,7 @@
 done
 
 lemma le_implies_UN_le_UN:
-    "[| !!x. x:A ==> c(x) \<le> d(x) |] ==> (\<Union>x\<in>A. c(x)) \<le> (\<Union>x\<in>A. d(x))"
+    "[| !!x. x\<in>A ==> c(x) \<le> d(x) |] ==> (\<Union>x\<in>A. c(x)) \<le> (\<Union>x\<in>A. d(x))"
 apply (rule UN_least_le)
 apply (rule_tac [2] UN_upper_le)
 apply (blast intro: Ord_UN le_Ord2)+
@@ -664,13 +669,18 @@
 done
 
 lemma non_succ_LimitI:
-    "[| 0<i;  \<forall>y. succ(y) \<noteq> i |] ==> Limit(i)"
-apply (unfold Limit_def)
-apply (safe del: subsetI)
-apply (rule_tac [2] not_le_iff_lt [THEN iffD1])
-apply (simp_all add: lt_Ord lt_Ord2)
-apply (blast elim: leE lt_asym)
-done
+  assumes i: "0<i" and nsucc: "\<And>y. succ(y) \<noteq> i"
+  shows "Limit(i)"
+proof -
+  have Oi: "Ord(i)" using i by (simp add: lt_def)
+  { fix y
+    assume yi: "y<i"
+    hence Osy: "Ord(succ(y))" by (simp add: lt_Ord Ord_succ)
+    have "~ i \<le> y" using yi by (blast dest: le_imp_not_lt) 
+    hence "succ(y) < i" using nsucc [of y] 
+      by (blast intro: Ord_linear_lt [OF Osy Oi]) }
+  thus ?thesis using i Oi by (auto simp add: Limit_def) 
+qed
 
 lemma succ_LimitE [elim!]: "Limit(succ(i)) ==> P"
 apply (rule lt_irrefl)
@@ -712,25 +722,41 @@
 
 text{*A set of ordinals is either empty, contains its own union, or its
 union is a limit ordinal.*}
+
+lemma Union_le: "[| !!x. x\<in>I ==> x\<le>j; Ord(j) |] ==> \<Union>(I) \<le> j"
+  by (auto simp add: le_subset_iff Union_least) 
+
 lemma Ord_set_cases:
-   "\<forall>i\<in>I. Ord(i) ==> I=0 \<or> \<Union>(I) \<in> I \<or> (\<Union>(I) \<notin> I \<and> Limit(\<Union>(I)))"
-apply (clarify elim!: not_emptyE)
-apply (cases "\<Union>(I)" rule: Ord_cases)
-   apply (blast intro: Ord_Union)
-  apply (blast intro: subst_elem)
- apply auto
-apply (clarify elim!: equalityE succ_subsetE)
-apply (simp add: Union_subset_iff)
-apply (subgoal_tac "B = succ(j)", blast)
-apply (rule le_anti_sym)
- apply (simp add: le_subset_iff)
-apply (simp add: ltI)
-done
+  assumes I: "\<forall>i\<in>I. Ord(i)"
+  shows "I=0 \<or> \<Union>(I) \<in> I \<or> (\<Union>(I) \<notin> I \<and> Limit(\<Union>(I)))"
+proof (cases "\<Union>(I)" rule: Ord_cases)
+  show "Ord(\<Union>I)" using I by (blast intro: Ord_Union)
+next
+  assume "\<Union>I = 0" thus ?thesis by (simp, blast intro: subst_elem)
+next
+  fix j
+  assume j: "Ord(j)" and UIj:"\<Union>(I) = succ(j)"
+  { assume "\<forall>i\<in>I. i\<le>j" 
+    hence "\<Union>(I) \<le> j" 
+      by (simp add: Union_le j) 
+    hence False 
+      by (simp add: UIj lt_not_refl) }
+  then obtain i where i: "i \<in> I" "succ(j) \<le> i" using I j
+    by (atomize, auto simp add: not_le_iff_lt) 
+  have "\<Union>(I) \<le> succ(j)" using UIj j by auto
+  hence "i \<le> succ(j)" using i
+    by (simp add: le_subset_iff Union_subset_iff) 
+  hence "succ(j) = i" using i 
+    by (blast intro: le_anti_sym) 
+  hence "succ(j) \<in> I" by (simp add: i)
+  thus ?thesis by (simp add: UIj) 
+next
+  assume "Limit(\<Union>I)" thus ?thesis by auto
+qed
 
-text{*If the union of a set of ordinals is a successor, then it is
-an element of that set.*}
+text{*If the union of a set of ordinals is a successor, then it is an element of that set.*}
 lemma Ord_Union_eq_succD: "[|\<forall>x\<in>X. Ord(x);  \<Union>X = succ(j)|] ==> succ(j) \<in> X"
-by (drule Ord_set_cases, auto)
+  by (drule Ord_set_cases, auto)
 
 lemma Limit_Union [rule_format]: "[| I \<noteq> 0;  \<forall>i\<in>I. Limit(i) |] ==> Limit(\<Union>I)"
 apply (simp add: Limit_def lt_def)
diff -r 57bf0cecb366 -r 49b91b716cbe src/ZF/pair.thy
--- a/src/ZF/pair.thy	Tue Mar 06 17:01:37 2012 +0000
+++ b/src/ZF/pair.thy	Thu Mar 08 16:43:29 2012 +0000
@@ -58,18 +58,22 @@
 declare sym [THEN Pair_neq_0, elim!]
 
 lemma Pair_neq_fst: "<a,b>=a ==> P"
-apply (unfold Pair_def)
-apply (rule consI1 [THEN mem_asym, THEN FalseE])
-apply (erule subst)
-apply (rule consI1)
-done
+proof (unfold Pair_def)
+  assume eq: "{{a, a}, {a, b}} = a"
+  have  "{a, a} \<in> {{a, a}, {a, b}}" by (rule consI1)
+  hence "{a, a} \<in> a" by (simp add: eq)
+  moreover have "a \<in> {a, a}" by (rule consI1)
+  ultimately show "P" by (rule mem_asym) 
+qed
 
 lemma Pair_neq_snd: "<a,b>=b ==> P"
-apply (unfold Pair_def)
-apply (rule consI1 [THEN consI2, THEN mem_asym, THEN FalseE])
-apply (erule subst)
-apply (rule consI1 [THEN consI2])
-done
+proof (unfold Pair_def)
+  assume eq: "{{a, a}, {a, b}} = b"
+  have  "{a, b} \<in> {{a, a}, {a, b}}" by blast
+  hence "{a, b} \<in> b" by (simp add: eq)
+  moreover have "b \<in> {a, b}" by blast
+  ultimately show "P" by (rule mem_asym) 
+qed
 
 
 subsection{*Sigma: Disjoint Union of a Family of Sets*}
@@ -145,15 +149,12 @@
     "[|  p:Sigma(A,B);    
          !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>)  
      |] ==> split(%x y. c(x,y), p) \<in> C(p)"
-apply (erule SigmaE, auto) 
-done
+by (erule SigmaE, auto) 
 
 lemma expand_split: 
   "u: A*B ==>    
         R(split(c,u)) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. u = <x,y> \<longrightarrow> R(c(x,y)))"
-apply (simp add: split_def)
-apply auto
-done
+by (auto simp add: split_def)
 
 
 subsection{*A version of @{term split} for Formulae: Result Type @{typ o}*}
@@ -165,9 +166,7 @@
     "[| split(R,z);  z:Sigma(A,B);                       
         !!x y. [| z = <x,y>;  R(x,y) |] ==> P            
      |] ==> P"
-apply (simp add: split_def)
-apply (erule SigmaE, force) 
-done
+by (auto simp add: split_def)
 
 lemma splitD: "split(R,<a,b>) ==> R(a,b)"
 by (simp add: split_def)