# HG changeset patch
# User paulson
# Date 1011267936 -3600
# Node ID 6842f90972da14050fd2cb43393a3543ff4bdcd0
# Parent  3ecbc37befab76abe6eb45a629481dbb45d39ae3
made proofs more robust

diff -r 3ecbc37befab -r 6842f90972da src/ZF/AC/AC15_WO6.thy
--- a/src/ZF/AC/AC15_WO6.thy	Thu Jan 17 10:35:59 2002 +0100
+++ b/src/ZF/AC/AC15_WO6.thy	Thu Jan 17 12:45:36 2002 +0100
@@ -54,15 +54,15 @@
 by (unfold pairwise_disjoint_def, blast) 
 
 lemma lemma3: 
-        "\<forall>B \<in> {cons(0, x*nat). x \<in> A}. pairwise_disjoint(f`B) &   
-                sets_of_size_between(f`B, 2, n) & Union(f`B)=B   
-        ==> \<forall>B \<in> A. \<exists>! u. u \<in> f`cons(0, B*nat) & u \<subseteq> cons(0, B*nat) &   
-                0 \<in> u & 2 \<lesssim> u & u \<lesssim> n"
+     "\<forall>B \<in> {cons(0, x*nat). x \<in> A}. pairwise_disjoint(f`B) &   
+	     sets_of_size_between(f`B, 2, n) & Union(f`B)=B   
+     ==> \<forall>B \<in> A. \<exists>! u. u \<in> f`cons(0, B*nat) & u \<subseteq> cons(0, B*nat) &   
+	     0 \<in> u & 2 \<lesssim> u & u \<lesssim> n"
 apply (unfold sets_of_size_between_def)
 apply (rule ballI)
-apply (erule ballE)
-prefer 2 apply blast 
-apply (blast dest: lemma1 intro!: lemma2) 
+apply (erule_tac x="cons(0, B*nat)" in ballE)
+ apply (blast dest: lemma1 intro!: lemma2) 
+apply blast
 done
 
 lemma lemma4: "[| A \<lesssim> i; Ord(i) |] ==> {P(a). a \<in> A} \<lesssim> i"
@@ -120,21 +120,21 @@
 (* AC10(n) ==> AC11                                                       *)
 (* ********************************************************************** *)
 
-lemma AC10_AC11: "[| n \<in> nat; 1\<le>n; AC10(n) |] ==> AC11"
+theorem AC10_AC11: "[| n \<in> nat; 1\<le>n; AC10(n) |] ==> AC11"
 by (unfold AC10_def AC11_def, blast)
 
 (* ********************************************************************** *)
 (* AC11 ==> AC12                                                          *)
 (* ********************************************************************** *)
 
-lemma AC11_AC12: "AC11 ==> AC12"
+theorem AC11_AC12: "AC11 ==> AC12"
 by (unfold AC10_def AC11_def AC11_def AC12_def, blast)
 
 (* ********************************************************************** *)
 (* AC12 ==> AC15                                                          *)
 (* ********************************************************************** *)
 
-lemma AC12_AC15: "AC12 ==> AC15"
+theorem AC12_AC15: "AC12 ==> AC15"
 apply (unfold AC12_def AC15_def)
 apply (blast del: ballI 
              intro!: cons_times_nat_not_Finite ex_fun_AC13_AC15)
@@ -168,7 +168,7 @@
 	(*but can't use del: DiffE despite the obvious conflictc*)
 done
 
-lemma AC15_WO6: "AC15 ==> WO6"
+theorem AC15_WO6: "AC15 ==> WO6"
 apply (unfold AC15_def WO6_def)
 apply (rule allI)
 apply (erule_tac x = "Pow (A) -{0}" in allE)
@@ -196,7 +196,7 @@
 (* AC10(n) implies AC13(n) for (1\<le>n)                                   *)
 (* ********************************************************************** *)
 
-lemma AC10_AC13: "[| n \<in> nat; 1\<le>n; AC10(n) |] ==> AC13(n)"
+theorem AC10_AC13: "[| n \<in> nat; 1\<le>n; AC10(n) |] ==> AC13(n)"
 apply (unfold AC10_def AC13_def, safe)
 apply (erule allE) 
 apply (erule impE [OF _ cons_times_nat_not_Finite], assumption); 
@@ -241,14 +241,14 @@
 (* AC13(n) ==> AC14  if 1 \<subseteq> n                                            *)
 (* ********************************************************************** *)
 
-lemma AC13_AC14: "[| n \<in> nat; 1\<le>n; AC13(n) |] ==> AC14"
+theorem AC13_AC14: "[| n \<in> nat; 1\<le>n; AC13(n) |] ==> AC14"
 by (unfold AC13_def AC14_def, auto)
 
 (* ********************************************************************** *)
 (* AC14 ==> AC15                                                          *)
 (* ********************************************************************** *)
 
-lemma AC14_AC15: "AC14 ==> AC15"
+theorem AC14_AC15: "AC14 ==> AC15"
 by (unfold AC13_def AC14_def AC15_def, fast)
 
 (* ********************************************************************** *)
@@ -272,7 +272,7 @@
 apply (simp add: the_element)
 done
 
-lemma AC13_AC1: "AC13(1) ==> AC1"
+theorem AC13_AC1: "AC13(1) ==> AC1"
 apply (unfold AC13_def AC1_def)
 apply (fast elim!: AC13_AC1_lemma)
 done
@@ -281,7 +281,7 @@
 (* AC11 ==> AC14                                                          *)
 (* ********************************************************************** *)
 
-lemma AC11_AC14: "AC11 ==> AC14"
+theorem AC11_AC14: "AC11 ==> AC14"
 apply (unfold AC11_def AC14_def)
 apply (fast intro!: AC10_AC13)
 done
diff -r 3ecbc37befab -r 6842f90972da src/ZF/Induct/Ntree.thy
--- a/src/ZF/Induct/Ntree.thy	Thu Jan 17 10:35:59 2002 +0100
+++ b/src/ZF/Induct/Ntree.thy	Thu Jan 17 12:45:36 2002 +0100
@@ -46,7 +46,7 @@
 *}
 
 lemma ntree_unfold: "ntree(A) = A \<times> (\<Union>n \<in> nat. n -> ntree(A))"
-  by (fast intro!: ntree.intros [unfolded ntree.con_defs]
+  by (blast intro: ntree.intros [unfolded ntree.con_defs]
     elim: ntree.cases [unfolded ntree.con_defs])
 
 lemma ntree_induct [induct set: ntree]: