1006 done |
1006 done |
1007 |
1007 |
1008 subsubsection{*For L to satisfy Powerset *} |
1008 subsubsection{*For L to satisfy Powerset *} |
1009 |
1009 |
1010 lemma LPow_env_typing: |
1010 lemma LPow_env_typing: |
1011 "[| y : Lset(i); Ord(i); y \<subseteq> X |] ==> y \<in> (\<Union>y\<in>Pow(X). Lset(succ(lrank(y))))" |
1011 "[| y : Lset(i); Ord(i); y \<subseteq> X |] |
|
1012 ==> \<exists>z \<in> Pow(X). y \<in> Lset(succ(lrank(z)))" |
1012 by (auto intro: L_I iff: Lset_succ_lrank_iff) |
1013 by (auto intro: L_I iff: Lset_succ_lrank_iff) |
1013 |
1014 |
1014 lemma LPow_in_Lset: |
1015 lemma LPow_in_Lset: |
1015 "[|X \<in> Lset(i); Ord(i)|] ==> \<exists>j. Ord(j) & {y \<in> Pow(X). L(y)} \<in> Lset(j)" |
1016 "[|X \<in> Lset(i); Ord(i)|] ==> \<exists>j. Ord(j) & {y \<in> Pow(X). L(y)} \<in> Lset(j)" |
1016 apply (rule_tac x="succ(\<Union>y \<in> Pow(X). succ(lrank(y)))" in exI) |
1017 apply (rule_tac x="succ(\<Union>y \<in> Pow(X). succ(lrank(y)))" in exI) |
1017 apply simp |
1018 apply simp |
1018 apply (rule LsetI [OF succI1]) |
1019 apply (rule LsetI [OF succI1]) |
1019 apply (simp add: DPow_def) |
1020 apply (simp add: DPow_def) |
1020 apply (intro conjI, clarify) |
1021 apply (intro conjI, clarify) |
1021 apply (rule_tac a=x in UN_I, simp+) |
1022 apply (rule_tac a=x in UN_I, simp+) |
1022 txt{*Now to create the formula @{term "y \<subseteq> X"} *} |
1023 txt{*Now to create the formula @{term "y \<subseteq> X"} *} |
1023 apply (rule_tac x="Cons(X,Nil)" in bexI) |
1024 apply (rule_tac x="Cons(X,Nil)" in bexI) |
1024 apply (rule_tac x="subset_fm(0,1)" in bexI) |
1025 apply (rule_tac x="subset_fm(0,1)" in bexI) |
1025 apply typecheck |
1026 apply typecheck |
1026 apply (rule conjI) |
1027 apply (rule conjI) |
1027 apply (simp add: succ_Un_distrib [symmetric]) |
1028 apply (simp add: succ_Un_distrib [symmetric]) |
1028 apply (rule equality_iffI) |
1029 apply (rule equality_iffI) |
1029 apply (simp add: Transset_UN [OF Transset_Lset] list.Cons [OF LPow_env_typing]) |
1030 apply (simp add: Transset_UN [OF Transset_Lset] LPow_env_typing) |
1030 apply (auto intro: L_I iff: Lset_succ_lrank_iff) |
1031 apply (auto intro: L_I iff: Lset_succ_lrank_iff) |
1031 done |
1032 done |
1032 |
1033 |
1033 theorem LPow_in_L: "L(X) ==> L({y \<in> Pow(X). L(y)})" |
1034 theorem LPow_in_L: "L(X) ==> L({y \<in> Pow(X). L(y)})" |
1034 by (blast intro: L_I dest: L_D LPow_in_Lset) |
1035 by (blast intro: L_I dest: L_D LPow_in_Lset) |