Structured and calculation-based proofs (with new trans rules!)
authorpaulson
Thu Mar 08 16:43:29 2012 +0000 (2012-03-08)
changeset 4684149b91b716cbe
parent 46823 57bf0cecb366
child 46842 52e9770e0107
Structured and calculation-based proofs (with new trans rules!)
src/ZF/Cardinal.thy
src/ZF/CardinalArith.thy
src/ZF/Int_ZF.thy
src/ZF/OrderType.thy
src/ZF/Ordinal.thy
src/ZF/pair.thy
     1.1 --- a/src/ZF/Cardinal.thy	Tue Mar 06 17:01:37 2012 +0000
     1.2 +++ b/src/ZF/Cardinal.thy	Thu Mar 08 16:43:29 2012 +0000
     1.3 @@ -101,7 +101,7 @@
     1.4  apply (blast intro: bij_converse_bij)
     1.5  done
     1.6  
     1.7 -lemma eqpoll_trans:
     1.8 +lemma eqpoll_trans [trans]:
     1.9      "[| X \<approx> Y;  Y \<approx> Z |] ==> X \<approx> Z"
    1.10  apply (unfold eqpoll_def)
    1.11  apply (blast intro: comp_bij)
    1.12 @@ -122,11 +122,17 @@
    1.13  lemma eqpoll_imp_lepoll: "X \<approx> Y ==> X \<lesssim> Y"
    1.14  by (unfold eqpoll_def bij_def lepoll_def, blast)
    1.15  
    1.16 -lemma lepoll_trans: "[| X \<lesssim> Y;  Y \<lesssim> Z |] ==> X \<lesssim> Z"
    1.17 +lemma lepoll_trans [trans]: "[| X \<lesssim> Y;  Y \<lesssim> Z |] ==> X \<lesssim> Z"
    1.18  apply (unfold lepoll_def)
    1.19  apply (blast intro: comp_inj)
    1.20  done
    1.21  
    1.22 +lemma eq_lepoll_trans [trans]: "[| X \<approx> Y;  Y \<lesssim> Z |] ==> X \<lesssim> Z"
    1.23 + by (blast intro: eqpoll_imp_lepoll lepoll_trans) 
    1.24 +
    1.25 +lemma lepoll_eq_trans [trans]: "[| X \<lesssim> Y;  Y \<approx> Z |] ==> X \<lesssim> Z"
    1.26 + by (blast intro: eqpoll_imp_lepoll lepoll_trans) 
    1.27 +
    1.28  (*Asymmetry law*)
    1.29  lemma eqpollI: "[| X \<lesssim> Y;  Y \<lesssim> X |] ==> X \<approx> Y"
    1.30  apply (unfold lepoll_def eqpoll_def)
    1.31 @@ -194,7 +200,7 @@
    1.32  done
    1.33  
    1.34  lemma inj_not_surj_succ:
    1.35 -  "[| f \<in> inj(A, succ(m)); f \<notin> surj(A, succ(m)) |] ==> \<exists>f. f:inj(A,m)"
    1.36 +  "[| f \<in> inj(A, succ(m)); f \<notin> surj(A, succ(m)) |] ==> \<exists>f. f \<in> inj(A,m)"
    1.37  apply (unfold inj_def surj_def)
    1.38  apply (safe del: succE)
    1.39  apply (erule swap, rule exI)
    1.40 @@ -208,24 +214,32 @@
    1.41  
    1.42  (** Variations on transitivity **)
    1.43  
    1.44 -lemma lesspoll_trans:
    1.45 +lemma lesspoll_trans [trans]:
    1.46        "[| X \<prec> Y; Y \<prec> Z |] ==> X \<prec> Z"
    1.47  apply (unfold lesspoll_def)
    1.48  apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
    1.49  done
    1.50  
    1.51 -lemma lesspoll_trans1:
    1.52 +lemma lesspoll_trans1 [trans]:
    1.53        "[| X \<lesssim> Y; Y \<prec> Z |] ==> X \<prec> Z"
    1.54  apply (unfold lesspoll_def)
    1.55  apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
    1.56  done
    1.57  
    1.58 -lemma lesspoll_trans2:
    1.59 +lemma lesspoll_trans2 [trans]:
    1.60        "[| X \<prec> Y; Y \<lesssim> Z |] ==> X \<prec> Z"
    1.61  apply (unfold lesspoll_def)
    1.62  apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
    1.63  done
    1.64  
    1.65 +lemma eq_lesspoll_trans [trans]:
    1.66 +      "[| X \<approx> Y; Y \<prec> Z |] ==> X \<prec> Z"
    1.67 +  by (blast intro: eqpoll_imp_lepoll lesspoll_trans1) 
    1.68 +
    1.69 +lemma lesspoll_eq_trans [trans]:
    1.70 +      "[| X \<prec> Y; Y \<approx> Z |] ==> X \<prec> Z"
    1.71 +  by (blast intro: eqpoll_imp_lepoll lesspoll_trans2) 
    1.72 +
    1.73  
    1.74  (** LEAST -- the least number operator [from HOL/Univ.ML] **)
    1.75  
    1.76 @@ -311,6 +325,9 @@
    1.77  (* @{term"Ord(A) ==> |A| \<approx> A"} *)
    1.78  lemmas Ord_cardinal_eqpoll = well_ord_Memrel [THEN well_ord_cardinal_eqpoll]
    1.79  
    1.80 +lemma Ord_cardinal_idem: "Ord(A) \<Longrightarrow> ||A|| = |A|"
    1.81 + by (rule Ord_cardinal_eqpoll [THEN cardinal_cong])
    1.82 +
    1.83  lemma well_ord_cardinal_eqE:
    1.84       "[| well_ord(X,r);  well_ord(Y,s);  |X| = |Y| |] ==> X \<approx> Y"
    1.85  apply (rule eqpoll_sym [THEN eqpoll_trans])
    1.86 @@ -335,7 +352,7 @@
    1.87  apply (erule sym)
    1.88  done
    1.89  
    1.90 -(* Could replace the  @{term"~(j \<approx> i)"}  by  @{term"~(i \<lesssim> j)"}. *)
    1.91 +(* Could replace the  @{term"~(j \<approx> i)"}  by  @{term"~(i \<preceq> j)"}. *)
    1.92  lemma CardI: "[| Ord(i);  !!j. j<i ==> ~(j \<approx> i) |] ==> Card(i)"
    1.93  apply (unfold Card_def cardinal_def)
    1.94  apply (subst Least_equality)
    1.95 @@ -399,15 +416,18 @@
    1.96  done
    1.97  
    1.98  (*Kunen's Lemma 10.5*)
    1.99 -lemma cardinal_eq_lemma: "[| |i| \<le> j;  j \<le> i |] ==> |j| = |i|"
   1.100 -apply (rule eqpollI [THEN cardinal_cong])
   1.101 -apply (erule le_imp_lepoll)
   1.102 -apply (rule lepoll_trans)
   1.103 -apply (erule_tac [2] le_imp_lepoll)
   1.104 -apply (rule eqpoll_sym [THEN eqpoll_imp_lepoll])
   1.105 -apply (rule Ord_cardinal_eqpoll)
   1.106 -apply (elim ltE Ord_succD)
   1.107 -done
   1.108 +lemma cardinal_eq_lemma: 
   1.109 +  assumes i:"|i| \<le> j" and j: "j \<le> i" shows "|j| = |i|"
   1.110 +proof (rule eqpollI [THEN cardinal_cong])
   1.111 +  show "j \<lesssim> i" by (rule le_imp_lepoll [OF j])
   1.112 +next
   1.113 +  have Oi: "Ord(i)" using j by (rule le_Ord2)
   1.114 +  hence "i \<approx> |i|" 
   1.115 +    by (blast intro: Ord_cardinal_eqpoll eqpoll_sym) 
   1.116 +  also have "... \<lesssim> j" 
   1.117 +    by (blast intro: le_imp_lepoll i) 
   1.118 +  finally show "i \<lesssim> j" .
   1.119 +qed
   1.120  
   1.121  lemma cardinal_mono: "i \<le> j ==> |i| \<le> |j|"
   1.122  apply (rule_tac i = "|i|" and j = "|j|" in Ord_linear_le)
   1.123 @@ -438,19 +458,20 @@
   1.124  
   1.125  (*Can use AC or finiteness to discharge first premise*)
   1.126  lemma well_ord_lepoll_imp_Card_le:
   1.127 -     "[| well_ord(B,r);  A \<lesssim> B |] ==> |A| \<le> |B|"
   1.128 -apply (rule_tac i = "|A|" and j = "|B|" in Ord_linear_le)
   1.129 -apply (safe intro!: Ord_cardinal le_eqI)
   1.130 -apply (rule eqpollI [THEN cardinal_cong], assumption)
   1.131 -apply (rule lepoll_trans)
   1.132 -apply (rule well_ord_cardinal_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll], assumption)
   1.133 -apply (erule le_imp_lepoll [THEN lepoll_trans])
   1.134 -apply (rule eqpoll_imp_lepoll)
   1.135 -apply (unfold lepoll_def)
   1.136 -apply (erule exE)
   1.137 -apply (rule well_ord_cardinal_eqpoll)
   1.138 -apply (erule well_ord_rvimage, assumption)
   1.139 -done
   1.140 +  assumes wB: "well_ord(B,r)" and AB: "A \<lesssim> B"
   1.141 +  shows "|A| \<le> |B|"
   1.142 +proof (rule Ord_linear_le [of "|A|" "|B|", OF Ord_cardinal Ord_cardinal], assumption)
   1.143 +  assume BA: "|B| \<le> |A|"
   1.144 +  from lepoll_well_ord [OF AB wB]
   1.145 +  obtain s where s: "well_ord(A, s)" by blast
   1.146 +  have "B  \<approx> |B|" by (blast intro: wB eqpoll_sym well_ord_cardinal_eqpoll) 
   1.147 +  also have "... \<lesssim> |A|" by (rule le_imp_lepoll [OF BA])
   1.148 +  also have "... \<approx> A" by (rule well_ord_cardinal_eqpoll [OF s])
   1.149 +  finally have "B \<lesssim> A" .
   1.150 +  hence "A \<approx> B" by (blast intro: eqpollI AB) 
   1.151 +  hence "|A| = |B|" by (rule cardinal_cong)
   1.152 +  thus ?thesis by simp
   1.153 +qed
   1.154  
   1.155  lemma lepoll_cardinal_le: "[| A \<lesssim> i; Ord(i) |] ==> |A| \<le> i"
   1.156  apply (rule le_trans)
   1.157 @@ -535,14 +556,6 @@
   1.158  lemma succ_lepoll_natE: "[| succ(n) \<lesssim> n;  n:nat |] ==> P"
   1.159  by (rule nat_lepoll_imp_le [THEN lt_irrefl], auto)
   1.160  
   1.161 -lemma n_lesspoll_nat: "n \<in> nat ==> n \<prec> nat"
   1.162 -apply (unfold lesspoll_def)
   1.163 -apply (fast elim!: Ord_nat [THEN [2] ltI [THEN leI, THEN le_imp_lepoll]]
   1.164 -                   eqpoll_sym [THEN eqpoll_imp_lepoll]
   1.165 -    intro: Ord_nat [THEN [2] nat_succI [THEN ltI], THEN leI,
   1.166 -                 THEN le_imp_lepoll, THEN lepoll_trans, THEN succ_lepoll_natE])
   1.167 -done
   1.168 -
   1.169  lemma nat_lepoll_imp_ex_eqpoll_n:
   1.170       "[| n \<in> nat;  nat \<lesssim> X |] ==> \<exists>Y. Y \<subseteq> X & n \<approx> Y"
   1.171  apply (unfold lepoll_def eqpoll_def)
   1.172 @@ -627,6 +640,9 @@
   1.173  apply (erule cardinal_mono)
   1.174  done
   1.175  
   1.176 +lemma n_lesspoll_nat: "n \<in> nat ==> n \<prec> nat"
   1.177 +  by (blast intro: Ord_nat Card_nat ltI lt_Card_imp_lesspoll)
   1.178 +
   1.179  
   1.180  subsection{*Towards Cardinal Arithmetic *}
   1.181  (** Congruence laws for successor, cardinal addition and multiplication **)
     2.1 --- a/src/ZF/CardinalArith.thy	Tue Mar 06 17:01:37 2012 +0000
     2.2 +++ b/src/ZF/CardinalArith.thy	Thu Mar 08 16:43:29 2012 +0000
     2.3 @@ -48,36 +48,38 @@
     2.4    cmult  (infixl "\<otimes>" 70)
     2.5  
     2.6  
     2.7 -lemma Card_Union [simp,intro,TC]: "(\<forall>x\<in>A. Card(x)) ==> Card(\<Union>(A))"
     2.8 -apply (rule CardI)
     2.9 - apply (simp add: Card_is_Ord)
    2.10 -apply (clarify dest!: ltD)
    2.11 -apply (drule bspec, assumption)
    2.12 -apply (frule lt_Card_imp_lesspoll, blast intro: ltI Card_is_Ord)
    2.13 -apply (drule eqpoll_sym [THEN eqpoll_imp_lepoll])
    2.14 -apply (drule lesspoll_trans1, assumption)
    2.15 -apply (subgoal_tac "B \<lesssim> \<Union>A")
    2.16 - apply (drule lesspoll_trans1, assumption, blast)
    2.17 -apply (blast intro: subset_imp_lepoll)
    2.18 -done
    2.19 +lemma Card_Union [simp,intro,TC]: 
    2.20 +  assumes A: "\<And>x. x\<in>A \<Longrightarrow> Card(x)" shows "Card(\<Union>(A))"
    2.21 +proof (rule CardI)
    2.22 +  show "Ord(\<Union>A)" using A 
    2.23 +    by (simp add: Card_is_Ord)
    2.24 +next
    2.25 +  fix j
    2.26 +  assume j: "j < \<Union>A"
    2.27 +  hence "\<exists>c\<in>A. j < c & Card(c)" using A
    2.28 +    by (auto simp add: lt_def intro: Card_is_Ord)
    2.29 +  then obtain c where c: "c\<in>A" "j < c" "Card(c)"
    2.30 +    by blast
    2.31 +  hence jls: "j \<prec> c" 
    2.32 +    by (simp add: lt_Card_imp_lesspoll) 
    2.33 +  { assume eqp: "j \<approx> \<Union>A"
    2.34 +    hence Uls: "\<Union>A \<prec> c" using jls
    2.35 +      by (blast intro: eqpoll_sym eqpoll_imp_lepoll lesspoll_trans1)
    2.36 +    moreover have  "c \<lesssim> \<Union>A" using c
    2.37 +      by (blast intro: subset_imp_lepoll)
    2.38 +    ultimately have "c \<prec> c"
    2.39 +      by (blast intro: lesspoll_trans1) 
    2.40 +    hence False 
    2.41 +      by auto
    2.42 +  } thus "\<not> j \<approx> \<Union>A" by blast
    2.43 +qed
    2.44  
    2.45  lemma Card_UN: "(!!x. x:A ==> Card(K(x))) ==> Card(\<Union>x\<in>A. K(x))"
    2.46 -by (blast intro: Card_Union)
    2.47 +  by blast
    2.48  
    2.49  lemma Card_OUN [simp,intro,TC]:
    2.50       "(!!x. x:A ==> Card(K(x))) ==> Card(\<Union>x<A. K(x))"
    2.51 -by (simp add: OUnion_def Card_0)
    2.52 -
    2.53 -lemma n_lesspoll_nat: "n \<in> nat ==> n \<prec> nat"
    2.54 -apply (unfold lesspoll_def)
    2.55 -apply (rule conjI)
    2.56 -apply (erule OrdmemD [THEN subset_imp_lepoll], rule Ord_nat)
    2.57 -apply (rule notI)
    2.58 -apply (erule eqpollE)
    2.59 -apply (rule succ_lepoll_natE)
    2.60 -apply (blast intro: nat_succI [THEN OrdmemD, THEN subset_imp_lepoll]
    2.61 -                    lepoll_trans, assumption)
    2.62 -done
    2.63 +  by (auto simp add: OUnion_def Card_0)
    2.64  
    2.65  lemma in_Card_imp_lesspoll: "[| Card(K); b \<in> K |] ==> b \<prec> K"
    2.66  apply (unfold lesspoll_def)
    2.67 @@ -103,11 +105,10 @@
    2.68  subsubsection{*Cardinal addition is commutative*}
    2.69  
    2.70  lemma sum_commute_eqpoll: "A+B \<approx> B+A"
    2.71 -apply (unfold eqpoll_def)
    2.72 -apply (rule exI)
    2.73 -apply (rule_tac c = "case(Inr,Inl)" and d = "case(Inr,Inl)" in lam_bijective)
    2.74 -apply auto
    2.75 -done
    2.76 +proof (unfold eqpoll_def, rule exI)
    2.77 +  show "(\<lambda>z\<in>A+B. case(Inr,Inl,z)) \<in> bij(A+B, B+A)"
    2.78 +    by (auto intro: lam_bijective [where d = "case(Inr,Inl)"]) 
    2.79 +qed
    2.80  
    2.81  lemma cadd_commute: "i \<oplus> j = j \<oplus> i"
    2.82  apply (unfold cadd_def)
    2.83 @@ -153,10 +154,10 @@
    2.84  subsubsection{*Addition by another cardinal*}
    2.85  
    2.86  lemma sum_lepoll_self: "A \<lesssim> A+B"
    2.87 -apply (unfold lepoll_def inj_def)
    2.88 -apply (rule_tac x = "\<lambda>x\<in>A. Inl (x) " in exI)
    2.89 -apply simp
    2.90 -done
    2.91 +proof (unfold lepoll_def, rule exI)
    2.92 +  show "(\<lambda>x\<in>A. Inl (x)) \<in> inj(A, A + B)"
    2.93 +    by (simp add: inj_def) 
    2.94 +qed
    2.95  
    2.96  (*Could probably weaken the premises to well_ord(K,r), or removing using AC*)
    2.97  
     3.1 --- a/src/ZF/Int_ZF.thy	Tue Mar 06 17:01:37 2012 +0000
     3.2 +++ b/src/ZF/Int_ZF.thy	Thu Mar 08 16:43:29 2012 +0000
     3.3 @@ -707,7 +707,7 @@
     3.4  apply auto
     3.5  done
     3.6  
     3.7 -lemma zless_trans: "[| x $< y; y $< z |] ==> x $< z"
     3.8 +lemma zless_trans [trans]: "[| x $< y; y $< z |] ==> x $< z"
     3.9  apply (subgoal_tac "intify (x) $< intify (z) ")
    3.10  apply (rule_tac [2] y = "intify (y) " in zless_trans_lemma)
    3.11  apply auto
    3.12 @@ -750,19 +750,19 @@
    3.13  apply (blast intro: zless_trans)
    3.14  done
    3.15  
    3.16 -lemma zle_trans: "[| x $<= y; y $<= z |] ==> x $<= z"
    3.17 +lemma zle_trans [trans]: "[| x $<= y; y $<= z |] ==> x $<= z"
    3.18  apply (subgoal_tac "intify (x) $<= intify (z) ")
    3.19  apply (rule_tac [2] y = "intify (y) " in zle_trans_lemma)
    3.20  apply auto
    3.21  done
    3.22  
    3.23 -lemma zle_zless_trans: "[| i $<= j; j $< k |] ==> i $< k"
    3.24 +lemma zle_zless_trans [trans]: "[| i $<= j; j $< k |] ==> i $< k"
    3.25  apply (auto simp add: zle_def)
    3.26  apply (blast intro: zless_trans)
    3.27  apply (simp add: zless_def zdiff_def zadd_def)
    3.28  done
    3.29  
    3.30 -lemma zless_zle_trans: "[| i $< j; j $<= k |] ==> i $< k"
    3.31 +lemma zless_zle_trans [trans]: "[| i $< j; j $<= k |] ==> i $< k"
    3.32  apply (auto simp add: zle_def)
    3.33  apply (blast intro: zless_trans)
    3.34  apply (simp add: zless_def zdiff_def zminus_def)
     4.1 --- a/src/ZF/OrderType.thy	Tue Mar 06 17:01:37 2012 +0000
     4.2 +++ b/src/ZF/OrderType.thy	Thu Mar 08 16:43:29 2012 +0000
     4.3 @@ -74,8 +74,7 @@
     4.4    The smaller ordinal is an initial segment of the larger *)
     4.5  lemma lt_pred_Memrel:
     4.6      "j<i ==> pred(i, j, Memrel(i)) = j"
     4.7 -apply (unfold pred_def lt_def)
     4.8 -apply (simp (no_asm_simp))
     4.9 +apply (simp add: pred_def lt_def)
    4.10  apply (blast intro: Ord_trans)
    4.11  done
    4.12  
     5.1 --- a/src/ZF/Ordinal.thy	Tue Mar 06 17:01:37 2012 +0000
     5.2 +++ b/src/ZF/Ordinal.thy	Thu Mar 08 16:43:29 2012 +0000
     5.3 @@ -9,7 +9,7 @@
     5.4  
     5.5  definition
     5.6    Memrel        :: "i=>i"  where
     5.7 -    "Memrel(A)   == {z: A*A . \<exists>x y. z=<x,y> & x:y }"
     5.8 +    "Memrel(A)   == {z\<in>A*A . \<exists>x y. z=<x,y> & x\<in>y }"
     5.9  
    5.10  definition
    5.11    Transset  :: "i=>o"  where
    5.12 @@ -21,7 +21,7 @@
    5.13  
    5.14  definition
    5.15    lt        :: "[i,i] => o"  (infixl "<" 50)   (*less-than on ordinals*)  where
    5.16 -    "i<j         == i:j & Ord(j)"
    5.17 +    "i<j         == i\<in>j & Ord(j)"
    5.18  
    5.19  definition
    5.20    Limit         :: "i=>o"  where
    5.21 @@ -56,11 +56,11 @@
    5.22  subsubsection{*Consequences of Downwards Closure*}
    5.23  
    5.24  lemma Transset_doubleton_D:
    5.25 -    "[| Transset(C); {a,b}: C |] ==> a:C & b: C"
    5.26 +    "[| Transset(C); {a,b}: C |] ==> a\<in>C & b\<in>C"
    5.27  by (unfold Transset_def, blast)
    5.28  
    5.29  lemma Transset_Pair_D:
    5.30 -    "[| Transset(C); <a,b>: C |] ==> a:C & b: C"
    5.31 +    "[| Transset(C); <a,b>\<in>C |] ==> a\<in>C & b\<in>C"
    5.32  apply (simp add: Pair_def)
    5.33  apply (blast dest: Transset_doubleton_D)
    5.34  done
    5.35 @@ -96,11 +96,11 @@
    5.36  by (unfold Transset_def, blast)
    5.37  
    5.38  lemma Transset_Union_family:
    5.39 -    "[| !!i. i:A ==> Transset(i) |] ==> Transset(\<Union>(A))"
    5.40 +    "[| !!i. i\<in>A ==> Transset(i) |] ==> Transset(\<Union>(A))"
    5.41  by (unfold Transset_def, blast)
    5.42  
    5.43  lemma Transset_Inter_family:
    5.44 -    "[| !!i. i:A ==> Transset(i) |] ==> Transset(\<Inter>(A))"
    5.45 +    "[| !!i. i\<in>A ==> Transset(i) |] ==> Transset(\<Inter>(A))"
    5.46  by (unfold Inter_def Transset_def, blast)
    5.47  
    5.48  lemma Transset_UN:
    5.49 @@ -115,22 +115,22 @@
    5.50  subsection{*Lemmas for Ordinals*}
    5.51  
    5.52  lemma OrdI:
    5.53 -    "[| Transset(i);  !!x. x:i ==> Transset(x) |]  ==>  Ord(i)"
    5.54 +    "[| Transset(i);  !!x. x\<in>i ==> Transset(x) |]  ==>  Ord(i)"
    5.55  by (simp add: Ord_def)
    5.56  
    5.57  lemma Ord_is_Transset: "Ord(i) ==> Transset(i)"
    5.58  by (simp add: Ord_def)
    5.59  
    5.60  lemma Ord_contains_Transset:
    5.61 -    "[| Ord(i);  j:i |] ==> Transset(j) "
    5.62 +    "[| Ord(i);  j\<in>i |] ==> Transset(j) "
    5.63  by (unfold Ord_def, blast)
    5.64  
    5.65  
    5.66 -lemma Ord_in_Ord: "[| Ord(i);  j:i |] ==> Ord(j)"
    5.67 +lemma Ord_in_Ord: "[| Ord(i);  j\<in>i |] ==> Ord(j)"
    5.68  by (unfold Ord_def Transset_def, blast)
    5.69  
    5.70  (*suitable for rewriting PROVIDED i has been fixed*)
    5.71 -lemma Ord_in_Ord': "[| j:i; Ord(i) |] ==> Ord(j)"
    5.72 +lemma Ord_in_Ord': "[| j\<in>i; Ord(i) |] ==> Ord(j)"
    5.73  by (blast intro: Ord_in_Ord)
    5.74  
    5.75  (* Ord(succ(j)) ==> Ord(j) *)
    5.76 @@ -139,13 +139,13 @@
    5.77  lemma Ord_subset_Ord: "[| Ord(i);  Transset(j);  j<=i |] ==> Ord(j)"
    5.78  by (simp add: Ord_def Transset_def, blast)
    5.79  
    5.80 -lemma OrdmemD: "[| j:i;  Ord(i) |] ==> j<=i"
    5.81 +lemma OrdmemD: "[| j\<in>i;  Ord(i) |] ==> j<=i"
    5.82  by (unfold Ord_def Transset_def, blast)
    5.83  
    5.84 -lemma Ord_trans: "[| i:j;  j:k;  Ord(k) |] ==> i:k"
    5.85 +lemma Ord_trans: "[| i\<in>j;  j\<in>k;  Ord(k) |] ==> i\<in>k"
    5.86  by (blast dest: OrdmemD)
    5.87  
    5.88 -lemma Ord_succ_subsetI: "[| i:j;  Ord(j) |] ==> succ(i) \<subseteq> j"
    5.89 +lemma Ord_succ_subsetI: "[| i\<in>j;  Ord(j) |] ==> succ(i) \<subseteq> j"
    5.90  by (blast dest: OrdmemD)
    5.91  
    5.92  
    5.93 @@ -172,28 +172,33 @@
    5.94  apply (blast intro!: Transset_Int)
    5.95  done
    5.96  
    5.97 -(*There is no set of all ordinals, for then it would contain itself*)
    5.98 -lemma ON_class: "~ (\<forall>i. i:X <-> Ord(i))"
    5.99 -apply (rule notI)
   5.100 -apply (frule_tac x = X in spec)
   5.101 -apply (safe elim!: mem_irrefl)
   5.102 -apply (erule swap, rule OrdI [OF _ Ord_is_Transset])
   5.103 -apply (simp add: Transset_def)
   5.104 -apply (blast intro: Ord_in_Ord)+
   5.105 -done
   5.106 +text{*There is no set of all ordinals, for then it would contain itself*}
   5.107 +lemma ON_class: "~ (\<forall>i. i\<in>X <-> Ord(i))"
   5.108 +proof (rule notI)
   5.109 +  assume X: "\<forall>i. i \<in> X \<longleftrightarrow> Ord(i)"
   5.110 +  have "\<forall>x y. x\<in>X \<longrightarrow> y\<in>x \<longrightarrow> y\<in>X"
   5.111 +    by (simp add: X, blast intro: Ord_in_Ord)
   5.112 +  hence "Transset(X)"
   5.113 +     by (auto simp add: Transset_def)
   5.114 +  moreover have "\<And>x. x \<in> X \<Longrightarrow> Transset(x)"
   5.115 +     by (simp add: X Ord_def)
   5.116 +  ultimately have "Ord(X)" by (rule OrdI)
   5.117 +  hence "X \<in> X" by (simp add: X)
   5.118 +  thus "False" by (rule mem_irrefl)
   5.119 +qed
   5.120  
   5.121  subsection{*< is 'less Than' for Ordinals*}
   5.122  
   5.123 -lemma ltI: "[| i:j;  Ord(j) |] ==> i<j"
   5.124 +lemma ltI: "[| i\<in>j;  Ord(j) |] ==> i<j"
   5.125  by (unfold lt_def, blast)
   5.126  
   5.127  lemma ltE:
   5.128 -    "[| i<j;  [| i:j;  Ord(i);  Ord(j) |] ==> P |] ==> P"
   5.129 +    "[| i<j;  [| i\<in>j;  Ord(i);  Ord(j) |] ==> P |] ==> P"
   5.130  apply (unfold lt_def)
   5.131  apply (blast intro: Ord_in_Ord)
   5.132  done
   5.133  
   5.134 -lemma ltD: "i<j ==> i:j"
   5.135 +lemma ltD: "i<j ==> i\<in>j"
   5.136  by (erule ltE, assumption)
   5.137  
   5.138  lemma not_lt0 [simp]: "~ i<0"
   5.139 @@ -211,7 +216,7 @@
   5.140  (* i<0 ==> R *)
   5.141  lemmas lt0E = not_lt0 [THEN notE, elim!]
   5.142  
   5.143 -lemma lt_trans: "[| i<j;  j<k |] ==> i<k"
   5.144 +lemma lt_trans [trans]: "[| i<j;  j<k |] ==> i<k"
   5.145  by (blast intro!: ltI elim!: ltE intro: Ord_trans)
   5.146  
   5.147  lemma lt_not_sym: "i<j ==> ~ (j<i)"
   5.148 @@ -238,10 +243,10 @@
   5.149  
   5.150  (*Equivalently, i<j ==> i < succ(j)*)
   5.151  lemma leI: "i<j ==> i \<le> j"
   5.152 -by (simp (no_asm_simp) add: le_iff)
   5.153 +by (simp add: le_iff)
   5.154  
   5.155  lemma le_eqI: "[| i=j;  Ord(j) |] ==> i \<le> j"
   5.156 -by (simp (no_asm_simp) add: le_iff)
   5.157 +by (simp add: le_iff)
   5.158  
   5.159  lemmas le_refl = refl [THEN le_eqI]
   5.160  
   5.161 @@ -268,7 +273,7 @@
   5.162  subsection{*Natural Deduction Rules for Memrel*}
   5.163  
   5.164  (*The lemmas MemrelI/E give better speed than [iff] here*)
   5.165 -lemma Memrel_iff [simp]: "<a,b> \<in> Memrel(A) <-> a:b & a:A & b:A"
   5.166 +lemma Memrel_iff [simp]: "<a,b> \<in> Memrel(A) <-> a\<in>b & a\<in>A & b\<in>A"
   5.167  by (unfold Memrel_def, blast)
   5.168  
   5.169  lemma MemrelI [intro!]: "[| a: b;  a: A;  b: A |] ==> <a,b> \<in> Memrel(A)"
   5.170 @@ -276,7 +281,7 @@
   5.171  
   5.172  lemma MemrelE [elim!]:
   5.173      "[| <a,b> \<in> Memrel(A);
   5.174 -        [| a: A;  b: A;  a:b |]  ==> P |]
   5.175 +        [| a: A;  b: A;  a\<in>b |]  ==> P |]
   5.176       ==> P"
   5.177  by auto
   5.178  
   5.179 @@ -314,7 +319,7 @@
   5.180  
   5.181  (*If Transset(A) then Memrel(A) internalizes the membership relation below A*)
   5.182  lemma Transset_Memrel_iff:
   5.183 -    "Transset(A) ==> <a,b> \<in> Memrel(A) <-> a:b & b:A"
   5.184 +    "Transset(A) ==> <a,b> \<in> Memrel(A) <-> a\<in>b & b\<in>A"
   5.185  by (unfold Transset_def, blast)
   5.186  
   5.187  
   5.188 @@ -352,7 +357,7 @@
   5.189  subsubsection{*Proving That < is a Linear Ordering on the Ordinals*}
   5.190  
   5.191  lemma Ord_linear [rule_format]:
   5.192 -     "Ord(i) ==> (\<forall>j. Ord(j) \<longrightarrow> i:j | i=j | j:i)"
   5.193 +     "Ord(i) ==> (\<forall>j. Ord(j) \<longrightarrow> i\<in>j | i=j | j\<in>i)"
   5.194  apply (erule trans_induct)
   5.195  apply (rule impI [THEN allI])
   5.196  apply (erule_tac i=j in trans_induct)
   5.197 @@ -386,7 +391,7 @@
   5.198  
   5.199  subsubsection{*Some Rewrite Rules for <, le*}
   5.200  
   5.201 -lemma Ord_mem_iff_lt: "Ord(j) ==> i:j <-> i<j"
   5.202 +lemma Ord_mem_iff_lt: "Ord(j) ==> i\<in>j <-> i<j"
   5.203  by (unfold lt_def, blast)
   5.204  
   5.205  lemma not_lt_iff_le: "[| Ord(i);  Ord(j) |] ==> ~ i<j <-> j \<le> i"
   5.206 @@ -508,7 +513,7 @@
   5.207  done
   5.208  
   5.209  lemma Un_least_mem_iff:
   5.210 -    "[| Ord(i); Ord(j); Ord(k) |] ==> i \<union> j \<in> k  <->  i:k & j:k"
   5.211 +    "[| Ord(i); Ord(j); Ord(k) |] ==> i \<union> j \<in> k  <->  i\<in>k & j\<in>k"
   5.212  apply (insert Un_least_lt_iff [of i j k])
   5.213  apply (simp add: lt_def)
   5.214  done
   5.215 @@ -529,13 +534,13 @@
   5.216  by (simp add: Ord_Un_if lt_Ord le_Ord2)
   5.217  
   5.218  lemma lt_Un_iff:
   5.219 -     "[| Ord(i); Ord(j) |] ==> k < i \<union> j <-> k < i | k < j";
   5.220 +     "[| Ord(i); Ord(j) |] ==> k < i \<union> j <-> k < i | k < j"
   5.221  apply (simp add: Ord_Un_if not_lt_iff_le)
   5.222  apply (blast intro: leI lt_trans2)+
   5.223  done
   5.224  
   5.225  lemma le_Un_iff:
   5.226 -     "[| Ord(i); Ord(j) |] ==> k \<le> i \<union> j <-> k \<le> i | k \<le> j";
   5.227 +     "[| Ord(i); Ord(j) |] ==> k \<le> i \<union> j <-> k \<le> i | k \<le> j"
   5.228  by (simp add: succ_Un_distrib lt_Un_iff [symmetric])
   5.229  
   5.230  lemma Un_upper1_lt: "[|k < i; Ord(j)|] ==> k < i \<union> j"
   5.231 @@ -551,17 +556,17 @@
   5.232  
   5.233  subsection{*Results about Limits*}
   5.234  
   5.235 -lemma Ord_Union [intro,simp,TC]: "[| !!i. i:A ==> Ord(i) |] ==> Ord(\<Union>(A))"
   5.236 +lemma Ord_Union [intro,simp,TC]: "[| !!i. i\<in>A ==> Ord(i) |] ==> Ord(\<Union>(A))"
   5.237  apply (rule Ord_is_Transset [THEN Transset_Union_family, THEN OrdI])
   5.238  apply (blast intro: Ord_contains_Transset)+
   5.239  done
   5.240  
   5.241  lemma Ord_UN [intro,simp,TC]:
   5.242 -     "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(\<Union>x\<in>A. B(x))"
   5.243 +     "[| !!x. x\<in>A ==> Ord(B(x)) |] ==> Ord(\<Union>x\<in>A. B(x))"
   5.244  by (rule Ord_Union, blast)
   5.245  
   5.246  lemma Ord_Inter [intro,simp,TC]:
   5.247 -    "[| !!i. i:A ==> Ord(i) |] ==> Ord(\<Inter>(A))"
   5.248 +    "[| !!i. i\<in>A ==> Ord(i) |] ==> Ord(\<Inter>(A))"
   5.249  apply (rule Transset_Inter_family [THEN OrdI])
   5.250  apply (blast intro: Ord_is_Transset)
   5.251  apply (simp add: Inter_def)
   5.252 @@ -569,19 +574,19 @@
   5.253  done
   5.254  
   5.255  lemma Ord_INT [intro,simp,TC]:
   5.256 -    "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(\<Inter>x\<in>A. B(x))"
   5.257 +    "[| !!x. x\<in>A ==> Ord(B(x)) |] ==> Ord(\<Inter>x\<in>A. B(x))"
   5.258  by (rule Ord_Inter, blast)
   5.259  
   5.260  
   5.261  (* No < version of this theorem: consider that @{term"(\<Union>i\<in>nat.i)=nat"}! *)
   5.262  lemma UN_least_le:
   5.263 -    "[| Ord(i);  !!x. x:A ==> b(x) \<le> i |] ==> (\<Union>x\<in>A. b(x)) \<le> i"
   5.264 +    "[| Ord(i);  !!x. x\<in>A ==> b(x) \<le> i |] ==> (\<Union>x\<in>A. b(x)) \<le> i"
   5.265  apply (rule le_imp_subset [THEN UN_least, THEN subset_imp_le])
   5.266  apply (blast intro: Ord_UN elim: ltE)+
   5.267  done
   5.268  
   5.269  lemma UN_succ_least_lt:
   5.270 -    "[| j<i;  !!x. x:A ==> b(x)<j |] ==> (\<Union>x\<in>A. succ(b(x))) < i"
   5.271 +    "[| j<i;  !!x. x\<in>A ==> b(x)<j |] ==> (\<Union>x\<in>A. succ(b(x))) < i"
   5.272  apply (rule ltE, assumption)
   5.273  apply (rule UN_least_le [THEN lt_trans2])
   5.274  apply (blast intro: succ_leI)+
   5.275 @@ -608,7 +613,7 @@
   5.276  done
   5.277  
   5.278  lemma le_implies_UN_le_UN:
   5.279 -    "[| !!x. x:A ==> c(x) \<le> d(x) |] ==> (\<Union>x\<in>A. c(x)) \<le> (\<Union>x\<in>A. d(x))"
   5.280 +    "[| !!x. x\<in>A ==> c(x) \<le> d(x) |] ==> (\<Union>x\<in>A. c(x)) \<le> (\<Union>x\<in>A. d(x))"
   5.281  apply (rule UN_least_le)
   5.282  apply (rule_tac [2] UN_upper_le)
   5.283  apply (blast intro: Ord_UN le_Ord2)+
   5.284 @@ -664,13 +669,18 @@
   5.285  done
   5.286  
   5.287  lemma non_succ_LimitI:
   5.288 -    "[| 0<i;  \<forall>y. succ(y) \<noteq> i |] ==> Limit(i)"
   5.289 -apply (unfold Limit_def)
   5.290 -apply (safe del: subsetI)
   5.291 -apply (rule_tac [2] not_le_iff_lt [THEN iffD1])
   5.292 -apply (simp_all add: lt_Ord lt_Ord2)
   5.293 -apply (blast elim: leE lt_asym)
   5.294 -done
   5.295 +  assumes i: "0<i" and nsucc: "\<And>y. succ(y) \<noteq> i"
   5.296 +  shows "Limit(i)"
   5.297 +proof -
   5.298 +  have Oi: "Ord(i)" using i by (simp add: lt_def)
   5.299 +  { fix y
   5.300 +    assume yi: "y<i"
   5.301 +    hence Osy: "Ord(succ(y))" by (simp add: lt_Ord Ord_succ)
   5.302 +    have "~ i \<le> y" using yi by (blast dest: le_imp_not_lt) 
   5.303 +    hence "succ(y) < i" using nsucc [of y] 
   5.304 +      by (blast intro: Ord_linear_lt [OF Osy Oi]) }
   5.305 +  thus ?thesis using i Oi by (auto simp add: Limit_def) 
   5.306 +qed
   5.307  
   5.308  lemma succ_LimitE [elim!]: "Limit(succ(i)) ==> P"
   5.309  apply (rule lt_irrefl)
   5.310 @@ -712,25 +722,41 @@
   5.311  
   5.312  text{*A set of ordinals is either empty, contains its own union, or its
   5.313  union is a limit ordinal.*}
   5.314 +
   5.315 +lemma Union_le: "[| !!x. x\<in>I ==> x\<le>j; Ord(j) |] ==> \<Union>(I) \<le> j"
   5.316 +  by (auto simp add: le_subset_iff Union_least) 
   5.317 +
   5.318  lemma Ord_set_cases:
   5.319 -   "\<forall>i\<in>I. Ord(i) ==> I=0 \<or> \<Union>(I) \<in> I \<or> (\<Union>(I) \<notin> I \<and> Limit(\<Union>(I)))"
   5.320 -apply (clarify elim!: not_emptyE)
   5.321 -apply (cases "\<Union>(I)" rule: Ord_cases)
   5.322 -   apply (blast intro: Ord_Union)
   5.323 -  apply (blast intro: subst_elem)
   5.324 - apply auto
   5.325 -apply (clarify elim!: equalityE succ_subsetE)
   5.326 -apply (simp add: Union_subset_iff)
   5.327 -apply (subgoal_tac "B = succ(j)", blast)
   5.328 -apply (rule le_anti_sym)
   5.329 - apply (simp add: le_subset_iff)
   5.330 -apply (simp add: ltI)
   5.331 -done
   5.332 +  assumes I: "\<forall>i\<in>I. Ord(i)"
   5.333 +  shows "I=0 \<or> \<Union>(I) \<in> I \<or> (\<Union>(I) \<notin> I \<and> Limit(\<Union>(I)))"
   5.334 +proof (cases "\<Union>(I)" rule: Ord_cases)
   5.335 +  show "Ord(\<Union>I)" using I by (blast intro: Ord_Union)
   5.336 +next
   5.337 +  assume "\<Union>I = 0" thus ?thesis by (simp, blast intro: subst_elem)
   5.338 +next
   5.339 +  fix j
   5.340 +  assume j: "Ord(j)" and UIj:"\<Union>(I) = succ(j)"
   5.341 +  { assume "\<forall>i\<in>I. i\<le>j" 
   5.342 +    hence "\<Union>(I) \<le> j" 
   5.343 +      by (simp add: Union_le j) 
   5.344 +    hence False 
   5.345 +      by (simp add: UIj lt_not_refl) }
   5.346 +  then obtain i where i: "i \<in> I" "succ(j) \<le> i" using I j
   5.347 +    by (atomize, auto simp add: not_le_iff_lt) 
   5.348 +  have "\<Union>(I) \<le> succ(j)" using UIj j by auto
   5.349 +  hence "i \<le> succ(j)" using i
   5.350 +    by (simp add: le_subset_iff Union_subset_iff) 
   5.351 +  hence "succ(j) = i" using i 
   5.352 +    by (blast intro: le_anti_sym) 
   5.353 +  hence "succ(j) \<in> I" by (simp add: i)
   5.354 +  thus ?thesis by (simp add: UIj) 
   5.355 +next
   5.356 +  assume "Limit(\<Union>I)" thus ?thesis by auto
   5.357 +qed
   5.358  
   5.359 -text{*If the union of a set of ordinals is a successor, then it is
   5.360 -an element of that set.*}
   5.361 +text{*If the union of a set of ordinals is a successor, then it is an element of that set.*}
   5.362  lemma Ord_Union_eq_succD: "[|\<forall>x\<in>X. Ord(x);  \<Union>X = succ(j)|] ==> succ(j) \<in> X"
   5.363 -by (drule Ord_set_cases, auto)
   5.364 +  by (drule Ord_set_cases, auto)
   5.365  
   5.366  lemma Limit_Union [rule_format]: "[| I \<noteq> 0;  \<forall>i\<in>I. Limit(i) |] ==> Limit(\<Union>I)"
   5.367  apply (simp add: Limit_def lt_def)
     6.1 --- a/src/ZF/pair.thy	Tue Mar 06 17:01:37 2012 +0000
     6.2 +++ b/src/ZF/pair.thy	Thu Mar 08 16:43:29 2012 +0000
     6.3 @@ -58,18 +58,22 @@
     6.4  declare sym [THEN Pair_neq_0, elim!]
     6.5  
     6.6  lemma Pair_neq_fst: "<a,b>=a ==> P"
     6.7 -apply (unfold Pair_def)
     6.8 -apply (rule consI1 [THEN mem_asym, THEN FalseE])
     6.9 -apply (erule subst)
    6.10 -apply (rule consI1)
    6.11 -done
    6.12 +proof (unfold Pair_def)
    6.13 +  assume eq: "{{a, a}, {a, b}} = a"
    6.14 +  have  "{a, a} \<in> {{a, a}, {a, b}}" by (rule consI1)
    6.15 +  hence "{a, a} \<in> a" by (simp add: eq)
    6.16 +  moreover have "a \<in> {a, a}" by (rule consI1)
    6.17 +  ultimately show "P" by (rule mem_asym) 
    6.18 +qed
    6.19  
    6.20  lemma Pair_neq_snd: "<a,b>=b ==> P"
    6.21 -apply (unfold Pair_def)
    6.22 -apply (rule consI1 [THEN consI2, THEN mem_asym, THEN FalseE])
    6.23 -apply (erule subst)
    6.24 -apply (rule consI1 [THEN consI2])
    6.25 -done
    6.26 +proof (unfold Pair_def)
    6.27 +  assume eq: "{{a, a}, {a, b}} = b"
    6.28 +  have  "{a, b} \<in> {{a, a}, {a, b}}" by blast
    6.29 +  hence "{a, b} \<in> b" by (simp add: eq)
    6.30 +  moreover have "b \<in> {a, b}" by blast
    6.31 +  ultimately show "P" by (rule mem_asym) 
    6.32 +qed
    6.33  
    6.34  
    6.35  subsection{*Sigma: Disjoint Union of a Family of Sets*}
    6.36 @@ -145,15 +149,12 @@
    6.37      "[|  p:Sigma(A,B);    
    6.38           !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>)  
    6.39       |] ==> split(%x y. c(x,y), p) \<in> C(p)"
    6.40 -apply (erule SigmaE, auto) 
    6.41 -done
    6.42 +by (erule SigmaE, auto) 
    6.43  
    6.44  lemma expand_split: 
    6.45    "u: A*B ==>    
    6.46          R(split(c,u)) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. u = <x,y> \<longrightarrow> R(c(x,y)))"
    6.47 -apply (simp add: split_def)
    6.48 -apply auto
    6.49 -done
    6.50 +by (auto simp add: split_def)
    6.51  
    6.52  
    6.53  subsection{*A version of @{term split} for Formulae: Result Type @{typ o}*}
    6.54 @@ -165,9 +166,7 @@
    6.55      "[| split(R,z);  z:Sigma(A,B);                       
    6.56          !!x y. [| z = <x,y>;  R(x,y) |] ==> P            
    6.57       |] ==> P"
    6.58 -apply (simp add: split_def)
    6.59 -apply (erule SigmaE, force) 
    6.60 -done
    6.61 +by (auto simp add: split_def)
    6.62  
    6.63  lemma splitD: "split(R,<a,b>) ==> R(a,b)"
    6.64  by (simp add: split_def)