*** empty log message ***
authorwenzelm
Tue Aug 27 11:09:35 2002 +0200 (2002-08-27)
changeset 13535007559e981c7
parent 13534 ca6debb89d77
child 13536 825249a031c3
*** empty log message ***
src/ZF/AC/AC15_WO6.thy
src/ZF/AC/AC17_AC1.thy
src/ZF/Constructible/Formula.thy
src/ZF/Constructible/Relative.thy
src/ZF/Constructible/Satisfies_absolute.thy
src/ZF/Induct/FoldSet.ML
src/ZF/Induct/Multiset.ML
src/ZF/Induct/Tree_Forest.thy
src/ZF/Integ/Bin.ML
src/ZF/UNITY/WFair.ML
src/ZF/ex/Limit.thy
     1.1 --- a/src/ZF/AC/AC15_WO6.thy	Tue Aug 27 11:09:33 2002 +0200
     1.2 +++ b/src/ZF/AC/AC15_WO6.thy	Tue Aug 27 11:09:35 2002 +0200
     1.3 @@ -145,7 +145,7 @@
     1.4  lemma OUN_eq_UN: "Ord(x) ==> (\<Union>a<x. F(a)) = (\<Union>a \<in> x. F(a))"
     1.5  by (fast intro!: ltI dest!: ltD)
     1.6  
     1.7 -lemma lemma1:
     1.8 +lemma AC15_WO6_aux1:
     1.9       "\<forall>x \<in> Pow(A)-{0}. f`x\<noteq>0 & f`x \<subseteq> x & f`x \<lesssim> m 
    1.10        ==> (\<Union>i<LEAST x. HH(f,A,x)={A}. HH(f,A,i)) = A"
    1.11  apply (simp add: Ord_Least [THEN OUN_eq_UN])
    1.12 @@ -155,7 +155,7 @@
    1.13             intro!: f_subsets_imp_UN_HH_eq_x [THEN Diff_eq_0_iff [THEN iffD1]])
    1.14  done
    1.15  
    1.16 -lemma lemma2:
    1.17 +lemma AC15_WO6_aux2:
    1.18       "\<forall>x \<in> Pow(A)-{0}. f`x\<noteq>0 & f`x \<subseteq> x & f`x \<lesssim> m 
    1.19        ==> \<forall>x < (LEAST x. HH(f,A,x)={A}). HH(f,A,x) \<lesssim> m"
    1.20  apply (rule oallI)
    1.21 @@ -163,7 +163,7 @@
    1.22  apply (frule HH_subset_imp_eq)
    1.23  apply (erule ssubst)
    1.24  apply (blast dest!: HH_subset_x_imp_subset_Diff_UN [THEN not_emptyI2])
    1.25 -	(*but can't use del: DiffE despite the obvious conflictc*)
    1.26 +	(*but can't use del: DiffE despite the obvious conflict*)
    1.27  done
    1.28  
    1.29  theorem AC15_WO6: "AC15 ==> WO6"
    1.30 @@ -178,7 +178,7 @@
    1.31   apply (rule_tac x = "\<lambda>j \<in> (LEAST i. HH (f,A,i) ={A}) . HH (f,A,j) " in exI)
    1.32   apply (simp_all add: ltD)
    1.33  apply (fast intro!: Ord_Least lam_type [THEN domain_of_fun]
    1.34 -            elim!: less_Least_subset_x lemma1 lemma2) 
    1.35 +            elim!: less_Least_subset_x AC15_WO6_aux1 AC15_WO6_aux2) 
    1.36  done
    1.37  
    1.38  
     2.1 --- a/src/ZF/AC/AC17_AC1.thy	Tue Aug 27 11:09:33 2002 +0200
     2.2 +++ b/src/ZF/AC/AC17_AC1.thy	Tue Aug 27 11:09:35 2002 +0200
     2.3 @@ -78,7 +78,7 @@
     2.4  apply (blast intro: lam_type)
     2.5  done
     2.6  
     2.7 -lemma lemma1:
     2.8 +lemma AC17_AC1_aux1:
     2.9       "[| \<forall>f \<in> Pow(x) - {0} -> x. \<exists>u \<in> Pow(x) - {0}. f`u\<notin>u;   
    2.10           \<exists>f \<in> Pow(x)-{0}->x.  
    2.11              x - (\<Union>a \<in> (LEAST i. HH(\<lambda>X \<in> Pow(x)-{0}. {f`X},x,i)={x}).   
    2.12 @@ -94,18 +94,18 @@
    2.13  apply (blast dest: apply_type) 
    2.14  done
    2.15  
    2.16 -lemma lemma2:
    2.17 +lemma AC17_AC1_aux2:
    2.18        "~ (\<exists>f \<in> Pow(x)-{0}->x. x - F(f) = 0)   
    2.19         ==> (\<lambda>f \<in> Pow(x)-{0}->x . x - F(f))   
    2.20             \<in> (Pow(x) -{0} -> x) -> Pow(x) - {0}"
    2.21  by (fast intro!: lam_type dest!: Diff_eq_0_iff [THEN iffD1])
    2.22  
    2.23 -lemma lemma3:
    2.24 +lemma AC17_AC1_aux3:
    2.25       "[| f`Z \<in> Z; Z \<in> Pow(x)-{0} |] 
    2.26        ==> (\<lambda>X \<in> Pow(x)-{0}. {f`X})`Z \<in> Pow(Z)-{0}"
    2.27  by auto
    2.28  
    2.29 -lemma lemma4:
    2.30 +lemma AC17_AC1_aux4:
    2.31       "\<exists>f \<in> F. f`((\<lambda>f \<in> F. Q(f))`f) \<in> (\<lambda>f \<in> F. Q(f))`f   
    2.32        ==> \<exists>f \<in> F. f`Q(f) \<in> Q(f)"
    2.33  by simp
    2.34 @@ -117,15 +117,15 @@
    2.35  apply (case_tac 
    2.36         "\<exists>f \<in> Pow(x)-{0} -> x. 
    2.37          x - (\<Union>a \<in> (LEAST i. HH (\<lambda>X \<in> Pow (x) -{0}. {f`X},x,i) ={x}) . HH (\<lambda>X \<in> Pow (x) -{0}. {f`X},x,a)) = 0")
    2.38 -apply (erule lemma1, assumption)
    2.39 -apply (drule lemma2)
    2.40 +apply (erule AC17_AC1_aux1, assumption)
    2.41 +apply (drule AC17_AC1_aux2)
    2.42  apply (erule allE)
    2.43  apply (drule bspec, assumption)
    2.44 -apply (drule lemma4)
    2.45 +apply (drule AC17_AC1_aux4)
    2.46  apply (erule bexE)
    2.47  apply (drule apply_type, assumption)
    2.48  apply (simp add: HH_Least_eq_x del: Diff_iff ) 
    2.49 -apply (drule lemma3, assumption) 
    2.50 +apply (drule AC17_AC1_aux3, assumption) 
    2.51  apply (fast dest!: subst_elem [OF _ HH_Least_eq_x [symmetric]]
    2.52                     f_subset_imp_HH_subset elim!: mem_irrefl)
    2.53  done
    2.54 @@ -142,11 +142,11 @@
    2.55  (* AC1 ==> AC2                                                            *)
    2.56  (* ********************************************************************** *)
    2.57  
    2.58 -lemma lemma1:
    2.59 +lemma AC1_AC2_aux1:
    2.60       "[| f:(\<Pi>X \<in> A. X);  B \<in> A;  0\<notin>A |] ==> {f`B} \<subseteq> B Int {f`C. C \<in> A}"
    2.61  by (fast elim!: apply_type)
    2.62  
    2.63 -lemma lemma2: 
    2.64 +lemma AC1_AC2_aux2: 
    2.65          "[| pairwise_disjoint(A); B \<in> A; C \<in> A; D \<in> B; D \<in> C |] ==> f`B = f`C"
    2.66  by (unfold pairwise_disjoint_def, fast)
    2.67  
    2.68 @@ -156,8 +156,8 @@
    2.69  apply (rule impI)  
    2.70  apply (elim asm_rl conjE allE exE impE, assumption)
    2.71  apply (intro exI ballI equalityI)
    2.72 -prefer 2 apply (rule lemma1, assumption+)
    2.73 -apply (fast elim!: lemma2 elim: apply_type)
    2.74 +prefer 2 apply (rule AC1_AC2_aux1, assumption+)
    2.75 +apply (fast elim!: AC1_AC2_aux2 elim: apply_type)
    2.76  done
    2.77  
    2.78  
    2.79 @@ -165,30 +165,30 @@
    2.80  (* AC2 ==> AC1                                                            *)
    2.81  (* ********************************************************************** *)
    2.82  
    2.83 -lemma lemma1: "0\<notin>A ==> 0 \<notin> {B*{B}. B \<in> A}"
    2.84 +lemma AC2_AC1_aux1: "0\<notin>A ==> 0 \<notin> {B*{B}. B \<in> A}"
    2.85  by (fast dest!: sym [THEN Sigma_empty_iff [THEN iffD1]])
    2.86  
    2.87 -lemma lemma2: "[| X*{X} Int C = {y}; X \<in> A |]   
    2.88 +lemma AC2_AC1_aux2: "[| X*{X} Int C = {y}; X \<in> A |]   
    2.89                 ==> (THE y. X*{X} Int C = {y}): X*A"
    2.90  apply (rule subst_elem [of y])
    2.91  apply (blast elim!: equalityE)
    2.92  apply (auto simp add: singleton_eq_iff) 
    2.93  done
    2.94  
    2.95 -lemma lemma3:
    2.96 +lemma AC2_AC1_aux3:
    2.97       "\<forall>D \<in> {E*{E}. E \<in> A}. \<exists>y. D Int C = {y}   
    2.98        ==> (\<lambda>x \<in> A. fst(THE z. (x*{x} Int C = {z}))) \<in> (\<Pi>X \<in> A. X)"
    2.99  apply (rule lam_type)
   2.100  apply (drule bspec, blast)
   2.101 -apply (blast intro: lemma2 fst_type)
   2.102 +apply (blast intro: AC2_AC1_aux2 fst_type)
   2.103  done
   2.104  
   2.105  lemma AC2_AC1: "AC2 ==> AC1"
   2.106  apply (unfold AC1_def AC2_def pairwise_disjoint_def)
   2.107  apply (intro allI impI)
   2.108  apply (elim allE impE)
   2.109 -prefer 2 apply (fast elim!: lemma3) 
   2.110 -apply (blast intro!: lemma1)
   2.111 +prefer 2 apply (fast elim!: AC2_AC1_aux3) 
   2.112 +apply (blast intro!: AC2_AC1_aux1)
   2.113  done
   2.114  
   2.115  
   2.116 @@ -211,21 +211,21 @@
   2.117  (* AC4 ==> AC3                                                            *)
   2.118  (* ********************************************************************** *)
   2.119  
   2.120 -lemma lemma1: "f \<in> A->B ==> (\<Union>z \<in> A. {z}*f`z) \<subseteq> A*Union(B)"
   2.121 +lemma AC4_AC3_aux1: "f \<in> A->B ==> (\<Union>z \<in> A. {z}*f`z) \<subseteq> A*Union(B)"
   2.122  by (fast dest!: apply_type)
   2.123  
   2.124 -lemma lemma2: "domain(\<Union>z \<in> A. {z}*f(z)) = {a \<in> A. f(a)\<noteq>0}"
   2.125 +lemma AC4_AC3_aux2: "domain(\<Union>z \<in> A. {z}*f(z)) = {a \<in> A. f(a)\<noteq>0}"
   2.126  by blast
   2.127  
   2.128 -lemma lemma3: "x \<in> A ==> (\<Union>z \<in> A. {z}*f(z))``{x} = f(x)"
   2.129 +lemma AC4_AC3_aux3: "x \<in> A ==> (\<Union>z \<in> A. {z}*f(z))``{x} = f(x)"
   2.130  by fast
   2.131  
   2.132  lemma AC4_AC3: "AC4 ==> AC3"
   2.133  apply (unfold AC3_def AC4_def)
   2.134  apply (intro allI ballI)
   2.135  apply (elim allE impE)
   2.136 -apply (erule lemma1)
   2.137 -apply (simp add: lemma2 lemma3 cong add: Pi_cong)
   2.138 +apply (erule AC4_AC3_aux1)
   2.139 +apply (simp add: AC4_AC3_aux2 AC4_AC3_aux3 cong add: Pi_cong)
   2.140  done
   2.141  
   2.142  (* ********************************************************************** *)
   2.143 @@ -264,18 +264,18 @@
   2.144  (* AC5 ==> AC4, Rubin & Rubin, p. 11                                      *)
   2.145  (* ********************************************************************** *)
   2.146  
   2.147 -lemma lemma1: "R \<subseteq> A*B ==> (\<lambda>x \<in> R. fst(x)) \<in> R -> A"
   2.148 +lemma AC5_AC4_aux1: "R \<subseteq> A*B ==> (\<lambda>x \<in> R. fst(x)) \<in> R -> A"
   2.149  by (fast intro!: lam_type fst_type)
   2.150  
   2.151 -lemma lemma2: "R \<subseteq> A*B ==> range(\<lambda>x \<in> R. fst(x)) = domain(R)"
   2.152 +lemma AC5_AC4_aux2: "R \<subseteq> A*B ==> range(\<lambda>x \<in> R. fst(x)) = domain(R)"
   2.153  by (unfold lam_def, force)
   2.154  
   2.155 -lemma lemma3: "[| \<exists>f \<in> A->C. P(f,domain(f)); A=B |] ==>  \<exists>f \<in> B->C. P(f,B)"
   2.156 +lemma AC5_AC4_aux3: "[| \<exists>f \<in> A->C. P(f,domain(f)); A=B |] ==>  \<exists>f \<in> B->C. P(f,B)"
   2.157  apply (erule bexE)
   2.158  apply (frule domain_of_fun, fast)
   2.159  done
   2.160  
   2.161 -lemma lemma4: "[| R \<subseteq> A*B; g \<in> C->R; \<forall>x \<in> C. (\<lambda>z \<in> R. fst(z))` (g`x) = x |]  
   2.162 +lemma AC5_AC4_aux4: "[| R \<subseteq> A*B; g \<in> C->R; \<forall>x \<in> C. (\<lambda>z \<in> R. fst(z))` (g`x) = x |]  
   2.163                  ==> (\<lambda>x \<in> C. snd(g`x)): (\<Pi>x \<in> C. R``{x})"
   2.164  apply (rule lam_type)
   2.165  apply (force dest: apply_type)
   2.166 @@ -284,9 +284,9 @@
   2.167  lemma AC5_AC4: "AC5 ==> AC4"
   2.168  apply (unfold AC4_def AC5_def, clarify)
   2.169  apply (elim allE ballE)
   2.170 -apply (drule lemma3 [OF _ lemma2], assumption)
   2.171 -apply (fast elim!: lemma4)
   2.172 -apply (blast intro: lemma1) 
   2.173 +apply (drule AC5_AC4_aux3 [OF _ AC5_AC4_aux2], assumption)
   2.174 +apply (fast elim!: AC5_AC4_aux4)
   2.175 +apply (blast intro: AC5_AC4_aux1) 
   2.176  done
   2.177  
   2.178  
     3.1 --- a/src/ZF/Constructible/Formula.thy	Tue Aug 27 11:09:33 2002 +0200
     3.2 +++ b/src/ZF/Constructible/Formula.thy	Tue Aug 27 11:09:35 2002 +0200
     3.3 @@ -164,11 +164,6 @@
     3.4         ==> (P | Q) <-> sats(A, Or(p,q), env)"
     3.5  by (simp add: sats_Or_iff)
     3.6  
     3.7 -lemma imp_iff_sats:
     3.8 -      "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
     3.9 -       ==> (P --> Q) <-> sats(A, Implies(p,q), env)"
    3.10 -by (simp add: sats_Forall_iff) 
    3.11 -
    3.12  lemma iff_iff_sats:
    3.13        "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
    3.14         ==> (P <-> Q) <-> sats(A, Iff(p,q), env)"
    3.15 @@ -819,8 +814,6 @@
    3.16  apply (blast intro: doubleton_in_Lset) 
    3.17  done
    3.18  
    3.19 -lemmas zero_in_LLimit = Limit_has_0 [THEN ltD, THEN zero_in_Lset, standard]
    3.20 -
    3.21  lemma singleton_in_LLimit:
    3.22      "[| a: Lset(i);  Limit(i) |] ==> {a} : Lset(i)"
    3.23  apply (erule Limit_LsetE, assumption)
    3.24 @@ -974,7 +967,7 @@
    3.25  done
    3.26  
    3.27  text{*Kunen's VI, 1.12 *}
    3.28 -lemma Lset_subset_Vset: "i \<in> nat ==> Lset(i) = Vset(i)";
    3.29 +lemma Lset_subset_Vset': "i \<in> nat ==> Lset(i) = Vset(i)";
    3.30  apply (erule nat_induct)
    3.31   apply (simp add: Vfrom_0) 
    3.32  apply (simp add: Lset_succ Vset_succ Finite_Vset Finite_DPow_eq_Pow) 
     4.1 --- a/src/ZF/Constructible/Relative.thy	Tue Aug 27 11:09:33 2002 +0200
     4.2 +++ b/src/ZF/Constructible/Relative.thy	Tue Aug 27 11:09:35 2002 +0200
     4.3 @@ -802,14 +802,6 @@
     4.4        ==> is_nat_case(M, a, is_b, k, z) <-> is_nat_case(M, a', is_b', k', z')"
     4.5  by (simp add: is_nat_case_def) 
     4.6  
     4.7 -lemma (in M_triv_axioms) Inl_in_M_iff [iff]:
     4.8 -     "M(Inl(a)) <-> M(a)"
     4.9 -by (simp add: Inl_def) 
    4.10 -
    4.11 -lemma (in M_triv_axioms) Inr_in_M_iff [iff]:
    4.12 -     "M(Inr(a)) <-> M(a)"
    4.13 -by (simp add: Inr_def)
    4.14 -
    4.15  
    4.16  subsection{*Absoluteness for Ordinals*}
    4.17  text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*}
     5.1 --- a/src/ZF/Constructible/Satisfies_absolute.thy	Tue Aug 27 11:09:33 2002 +0200
     5.2 +++ b/src/ZF/Constructible/Satisfies_absolute.thy	Tue Aug 27 11:09:35 2002 +0200
     5.3 @@ -595,8 +595,8 @@
     5.4  done
     5.5  
     5.6  lemmas (in M_satisfies) 
     5.7 -    satisfies_closed = Formula_Rec.formula_rec_closed [OF Formula_Rec_M]
     5.8 -and satisfies_abs    = Formula_Rec.formula_rec_abs [OF Formula_Rec_M]
     5.9 +    satisfies_closed' = Formula_Rec.formula_rec_closed [OF Formula_Rec_M]
    5.10 +and satisfies_abs'    = Formula_Rec.formula_rec_abs [OF Formula_Rec_M]
    5.11  
    5.12  
    5.13  lemma (in M_satisfies) satisfies_closed:
     6.1 --- a/src/ZF/Induct/FoldSet.ML	Tue Aug 27 11:09:33 2002 +0200
     6.2 +++ b/src/ZF/Induct/FoldSet.ML	Tue Aug 27 11:09:35 2002 +0200
     6.3 @@ -301,7 +301,7 @@
     6.4  by (asm_simp_tac (simpset() addsimps [setsum_def]) 2);
     6.5  by (etac Finite_induct 1);
     6.6  by Auto_tac;
     6.7 -qed "setsum_0";
     6.8 +qed "setsum_K0";
     6.9  
    6.10  (*The reversed orientation looks more natural, but LOOPS as a simprule!*)
    6.11  Goal "[| Finite(C); Finite(D) |] \
     7.1 --- a/src/ZF/Induct/Multiset.ML	Tue Aug 27 11:09:33 2002 +0200
     7.2 +++ b/src/ZF/Induct/Multiset.ML	Tue Aug 27 11:09:35 2002 +0200
     7.3 @@ -206,7 +206,7 @@
     7.4  by (res_inst_tac [("x", "{x:A . 0<f`x}")] exI 1);
     7.5  by (auto_tac (claset() addIs [Collect_subset RS subset_Finite,
     7.6                                funrestrict_type], simpset()));
     7.7 -qed "normalize_multiset";
     7.8 +qed "multiset_normalize";
     7.9  
    7.10  (** Typechecking rules for union and difference of multisets **)
    7.11  
    7.12 @@ -231,7 +231,7 @@
    7.13  
    7.14  Goalw [mdiff_def]
    7.15  "multiset(M) ==> multiset(M -# N)";
    7.16 -by (res_inst_tac [("A", "mset_of(M)")] normalize_multiset 1);
    7.17 +by (res_inst_tac [("A", "mset_of(M)")] multiset_normalize 1);
    7.18  by (asm_simp_tac (simpset() addsimps [multiset_set_of_Finite]) 2);
    7.19  by (auto_tac (claset(), simpset() addsimps [mset_of_def, multiset_def]));
    7.20  by (auto_tac (claset() addSIs [lam_type], 
     8.1 --- a/src/ZF/Induct/Tree_Forest.thy	Tue Aug 27 11:09:33 2002 +0200
     8.2 +++ b/src/ZF/Induct/Tree_Forest.thy	Tue Aug 27 11:09:35 2002 +0200
     8.3 @@ -45,7 +45,7 @@
     8.4    apply (rule Part_subset)
     8.5    done
     8.6  
     8.7 -lemma treeI [TC]: "x \<in> forest(A) ==> x \<in> tree_forest(A)"
     8.8 +lemma treeI' [TC]: "x \<in> forest(A) ==> x \<in> tree_forest(A)"
     8.9    by (rule forest_subset_TF [THEN subsetD])
    8.10  
    8.11  lemma TF_equals_Un: "tree(A) \<union> forest(A) = tree_forest(A)"
     9.1 --- a/src/ZF/Integ/Bin.ML	Tue Aug 27 11:09:33 2002 +0200
     9.2 +++ b/src/ZF/Integ/Bin.ML	Tue Aug 27 11:09:35 2002 +0200
     9.3 @@ -412,10 +412,6 @@
     9.4  Delsimps [integ_of_Pls, integ_of_Min, integ_of_BIT];
     9.5  
     9.6  
     9.7 -bind_thms ("NCons_simps", 
     9.8 -	   [NCons_Pls_0, NCons_Pls_1, NCons_Min_0, NCons_Min_1, NCons_BIT]);
     9.9 -
    9.10 -
    9.11  bind_thms ("bin_arith_extra_simps",
    9.12      [integ_of_add RS sym,   (*invoke bin_add*)
    9.13       integ_of_minus RS sym, (*invoke bin_minus*)
    10.1 --- a/src/ZF/UNITY/WFair.ML	Tue Aug 27 11:09:33 2002 +0200
    10.2 +++ b/src/ZF/UNITY/WFair.ML	Tue Aug 27 11:09:35 2002 +0200
    10.3 @@ -387,7 +387,7 @@
    10.4  by (blast_tac (claset() addIs leadsTo_refl::prems) 1);
    10.5  by (rtac (major RS leadsTo_induct) 1);
    10.6  by (REPEAT (blast_tac (claset() addIs prems) 1));
    10.7 -qed "lemma";
    10.8 +qed "leadsTo_induct_pre_aux";
    10.9  
   10.10  
   10.11  val [major, zb_prem, basis_prem, union_prem] = Goal
   10.12 @@ -399,7 +399,7 @@
   10.13  by (cut_facts_tac [major] 1);
   10.14  by (subgoal_tac "(F : za leadsTo zb) & P(za)" 1);
   10.15  by (etac conjunct2 1);
   10.16 -by (rtac (major RS lemma) 1);
   10.17 +by (rtac (major RS leadsTo_induct_pre_aux) 1);
   10.18  by (blast_tac (claset() addDs [leadsToD2]
   10.19                          addIs [leadsTo_Union,union_prem]) 3);
   10.20  by (blast_tac (claset() addIs [leadsTo_Trans,basis_prem, leadsTo_Basis]) 2);
   10.21 @@ -501,7 +501,7 @@
   10.22  by (blast_tac (claset() addIs [leadsTo_cancel1, leadsTo_Un_duplicate]) 1);
   10.23  by (auto_tac (claset() addIs [leadsTo_UN], 
   10.24                simpset()  delsimps UN_simps addsimps [Int_UN_distrib]));
   10.25 -qed "lemma1";
   10.26 +qed "leadsTo_wf_induct_aux";
   10.27  
   10.28  (** Meta or object quantifier ? **)
   10.29  Goal "[| wf(r); \
   10.30 @@ -515,7 +515,7 @@
   10.31  by (res_inst_tac [("I", "I")] leadsTo_UN 2);
   10.32  by (REPEAT (assume_tac 2));
   10.33  by (Clarify_tac 2);
   10.34 -by (eres_inst_tac [("I", "I")] lemma1 2);
   10.35 +by (eres_inst_tac [("I", "I")] leadsTo_wf_induct_aux 2);
   10.36  by (REPEAT (assume_tac 2));
   10.37  by (rtac equalityI 1);
   10.38  by Safe_tac;
   10.39 @@ -602,7 +602,7 @@
   10.40  \   ==> F : (A1 Un A2 - C) co (A1 Un A2 Un C)";
   10.41  by (Clarify_tac 1);
   10.42  by (Blast_tac 1);
   10.43 -qed "lemma1";
   10.44 +qed "leadsTo_123_aux";
   10.45  
   10.46  (*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
   10.47  (* slightly different from the HOL one: B here is bounded *)
   10.48 @@ -615,7 +615,7 @@
   10.49  (*Trans*)
   10.50  by (Clarify_tac 1);
   10.51  by (res_inst_tac [("x", "Ba Un Bb")] bexI 1);
   10.52 -by (blast_tac (claset() addIs [lemma1,leadsTo_Un_Un, leadsTo_cancel1,
   10.53 +by (blast_tac (claset() addIs [leadsTo_123_aux,leadsTo_Un_Un, leadsTo_cancel1,
   10.54                                 leadsTo_Un_duplicate]) 1);
   10.55  by (Blast_tac 1);
   10.56  (*Union*)
    11.1 --- a/src/ZF/ex/Limit.thy	Tue Aug 27 11:09:33 2002 +0200
    11.2 +++ b/src/ZF/ex/Limit.thy	Tue Aug 27 11:09:35 2002 +0200
    11.3 @@ -542,12 +542,12 @@
    11.4                       matrix_chain_lub isub_lemma)
    11.5  done
    11.6  
    11.7 -lemma lemma1:
    11.8 +lemma lub_matrix_diag_aux1:
    11.9      "lub(D,(\<lambda>n \<in> nat. lub(D,\<lambda>m \<in> nat. M`n`m))) =
   11.10       (THE x. islub(D, (\<lambda>n \<in> nat. lub(D,\<lambda>m \<in> nat. M`n`m)), x))"
   11.11  by (simp add: lub_def)
   11.12  
   11.13 -lemma lemma2:
   11.14 +lemma lub_matrix_diag_aux2:
   11.15      "lub(D,(\<lambda>n \<in> nat. M`n`n)) =
   11.16       (THE x. islub(D, (\<lambda>n \<in> nat. M`n`n), x))"
   11.17  by (simp add: lub_def)
   11.18 @@ -556,7 +556,7 @@
   11.19      "[|matrix(D,M); cpo(D)|] 
   11.20       ==> lub(D,(\<lambda>n \<in> nat. lub(D,\<lambda>m \<in> nat. M`n`m))) =
   11.21           lub(D,(\<lambda>n \<in> nat. M`n`n))"
   11.22 -apply (simp (no_asm) add: lemma1 lemma2)
   11.23 +apply (simp (no_asm) add: lub_matrix_diag_aux1 lub_matrix_diag_aux2)
   11.24  apply (simp add: islub_def isub_eq)
   11.25  done
   11.26  
   11.27 @@ -876,7 +876,7 @@
   11.28  lemmas id_comp = fun_is_rel [THEN left_comp_id]
   11.29  and    comp_id = fun_is_rel [THEN right_comp_id]
   11.30  
   11.31 -lemma lemma1:
   11.32 +lemma projpair_unique_aux1:
   11.33      "[|cpo(D); cpo(E); projpair(D,E,e,p); projpair(D,E,e',p');
   11.34         rel(cf(D,E),e,e')|] ==> rel(cf(E,D),p',p)"
   11.35  apply (rule_tac b=p' in
   11.36 @@ -899,7 +899,7 @@
   11.37  
   11.38  text{*Proof's very like the previous one.  Is there a pattern that
   11.39        could be exploited?*}
   11.40 -lemma lemma2:
   11.41 +lemma projpair_unique_aux2:
   11.42      "[|cpo(D); cpo(E); projpair(D,E,e,p); projpair(D,E,e',p');
   11.43         rel(cf(E,D),p',p)|] ==> rel(cf(D,E),e,e')"
   11.44  apply (rule_tac b=e
   11.45 @@ -923,7 +923,7 @@
   11.46  lemma projpair_unique:
   11.47      "[|cpo(D); cpo(E); projpair(D,E,e,p); projpair(D,E,e',p')|] 
   11.48       ==> (e=e')<->(p=p')"
   11.49 -by (blast intro: cpo_antisym lemma1 lemma2 cpo_cf cont_cf
   11.50 +by (blast intro: cpo_antisym projpair_unique_aux1 projpair_unique_aux2 cpo_cf cont_cf
   11.51            dest: projpair_ep_cont)
   11.52  
   11.53  (* Slightly different, more asms, since THE chooses the unique element. *)
   11.54 @@ -1763,7 +1763,7 @@
   11.55  
   11.56  (* 32 vs 61, using safe_tac with imp in asm would be unfortunate (5steps) *)
   11.57  
   11.58 -lemma lemma1:
   11.59 +lemma eps1_aux1:
   11.60      "[|m le n; emb_chain(DD,ee); x \<in> set(Dinf(DD,ee)); m \<in> nat; n \<in> nat|] 
   11.61       ==> rel(DD`n,e_less(DD,ee,m,n)`(x`m),x`n)"
   11.62  apply (erule rev_mp) (* For induction proof *)
   11.63 @@ -1807,7 +1807,7 @@
   11.64  
   11.65  (* 18 vs 40 *)
   11.66  
   11.67 -lemma lemma2:
   11.68 +lemma eps1_aux2:
   11.69      "[|n le m; emb_chain(DD,ee); x \<in> set(Dinf(DD,ee)); m \<in> nat; n \<in> nat|] 
   11.70       ==> rel(DD`n,e_gr(DD,ee,m,n)`(x`m),x`n)"
   11.71  apply (erule rev_mp) (* For induction proof *)
   11.72 @@ -1835,7 +1835,7 @@
   11.73      "[|emb_chain(DD,ee); x \<in> set(Dinf(DD,ee)); m \<in> nat; n \<in> nat|] 
   11.74       ==> rel(DD`n,eps(DD,ee,m,n)`(x`m),x`n)"
   11.75  apply (simp add: eps_def)
   11.76 -apply (blast intro: lemma1 not_le_iff_lt [THEN iffD1, THEN leI, THEN lemma2]  
   11.77 +apply (blast intro: eps1_aux1 not_le_iff_lt [THEN iffD1, THEN leI, THEN eps1_aux2]
   11.78                      nat_into_Ord)
   11.79  done
   11.80  
   11.81 @@ -1894,7 +1894,7 @@
   11.82    "[| emb_chain(DD,ee); n \<in> nat |] ==> emb(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n))"
   11.83  by (auto simp add: emb_def intro: exI rho_projpair)
   11.84  
   11.85 -lemma commuteI: "[| emb_chain(DD,ee); n \<in> nat |] 
   11.86 +lemma rho_proj_cont: "[| emb_chain(DD,ee); n \<in> nat |] 
   11.87       ==> rho_proj(DD,ee,n) \<in> cont(Dinf(DD,ee),DD`n)"
   11.88  by (auto intro: rho_projpair projpair_p_cont)
   11.89