new proof needed now
authorpaulson
Wed Aug 21 15:56:37 2002 +0200 (2002-08-21)
changeset 13511e4b129eaa9c6
parent 13510 0a0f37f9c031
child 13512 80edb859fd24
new proof needed now
src/ZF/Constructible/Formula.thy
     1.1 --- a/src/ZF/Constructible/Formula.thy	Wed Aug 21 15:55:59 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Formula.thy	Wed Aug 21 15:56:37 2002 +0200
     1.3 @@ -1008,7 +1008,8 @@
     1.4  subsubsection{*For L to satisfy Powerset *}
     1.5  
     1.6  lemma LPow_env_typing:
     1.7 -     "[| y : Lset(i); Ord(i); y \<subseteq> X |] ==> y \<in> (\<Union>y\<in>Pow(X). Lset(succ(lrank(y))))"
     1.8 +    "[| y : Lset(i); Ord(i); y \<subseteq> X |] 
     1.9 +     ==> \<exists>z \<in> Pow(X). y \<in> Lset(succ(lrank(z)))"
    1.10  by (auto intro: L_I iff: Lset_succ_lrank_iff) 
    1.11  
    1.12  lemma LPow_in_Lset:
    1.13 @@ -1018,15 +1019,15 @@
    1.14  apply (rule LsetI [OF succI1])
    1.15  apply (simp add: DPow_def) 
    1.16  apply (intro conjI, clarify) 
    1.17 -apply (rule_tac a=x in UN_I, simp+)  
    1.18 + apply (rule_tac a=x in UN_I, simp+)  
    1.19  txt{*Now to create the formula @{term "y \<subseteq> X"} *}
    1.20  apply (rule_tac x="Cons(X,Nil)" in bexI) 
    1.21   apply (rule_tac x="subset_fm(0,1)" in bexI) 
    1.22    apply typecheck
    1.23 -apply (rule conjI) 
    1.24 + apply (rule conjI) 
    1.25  apply (simp add: succ_Un_distrib [symmetric]) 
    1.26  apply (rule equality_iffI) 
    1.27 -apply (simp add: Transset_UN [OF Transset_Lset] list.Cons [OF LPow_env_typing])
    1.28 +apply (simp add: Transset_UN [OF Transset_Lset] LPow_env_typing)
    1.29  apply (auto intro: L_I iff: Lset_succ_lrank_iff) 
    1.30  done
    1.31