13223

1 
header {* FirstOrder Formulas and the Definition of the Class L *}


2 


3 
theory Formula = Main:


4 

13291

5 
subsection{*Internalized formulas of FOL*}


6 


7 
text{*De Bruijn representation.


8 
Unbound variables get their denotations from an environment.*}

13223

9 


10 
consts formula :: i


11 
datatype


12 
"formula" = Member ("x: nat", "y: nat")


13 
 Equal ("x: nat", "y: nat")


14 
 Neg ("p: formula")


15 
 And ("p: formula", "q: formula")


16 
 Forall ("p: formula")


17 


18 
declare formula.intros [TC]


19 


20 
constdefs Or :: "[i,i]=>i"


21 
"Or(p,q) == Neg(And(Neg(p),Neg(q)))"


22 


23 
constdefs Implies :: "[i,i]=>i"


24 
"Implies(p,q) == Neg(And(p,Neg(q)))"


25 

13291

26 
constdefs Iff :: "[i,i]=>i"


27 
"Iff(p,q) == And(Implies(p,q), Implies(q,p))"


28 

13223

29 
constdefs Exists :: "i=>i"


30 
"Exists(p) == Neg(Forall(Neg(p)))";


31 


32 
lemma Or_type [TC]: "[ p \<in> formula; q \<in> formula ] ==> Or(p,q) \<in> formula"


33 
by (simp add: Or_def)


34 


35 
lemma Implies_type [TC]:


36 
"[ p \<in> formula; q \<in> formula ] ==> Implies(p,q) \<in> formula"


37 
by (simp add: Implies_def)


38 

13291

39 
lemma Iff_type [TC]:


40 
"[ p \<in> formula; q \<in> formula ] ==> Iff(p,q) \<in> formula"


41 
by (simp add: Iff_def)


42 

13223

43 
lemma Exists_type [TC]: "p \<in> formula ==> Exists(p) \<in> formula"


44 
by (simp add: Exists_def)


45 


46 


47 
consts satisfies :: "[i,i]=>i"


48 
primrec (*explicit lambda is required because the environment varies*)


49 
"satisfies(A,Member(x,y)) =


50 
(\<lambda>env \<in> list(A). bool_of_o (nth(x,env) \<in> nth(y,env)))"


51 


52 
"satisfies(A,Equal(x,y)) =


53 
(\<lambda>env \<in> list(A). bool_of_o (nth(x,env) = nth(y,env)))"


54 


55 
"satisfies(A,Neg(p)) =


56 
(\<lambda>env \<in> list(A). not(satisfies(A,p)`env))"


57 


58 
"satisfies(A,And(p,q)) =


59 
(\<lambda>env \<in> list(A). (satisfies(A,p)`env) and (satisfies(A,q)`env))"


60 


61 
"satisfies(A,Forall(p)) =


62 
(\<lambda>env \<in> list(A). bool_of_o (\<forall>x\<in>A. satisfies(A,p) ` (Cons(x,env)) = 1))"


63 


64 


65 
lemma "p \<in> formula ==> satisfies(A,p) \<in> list(A) > bool"


66 
by (induct_tac p, simp_all)


67 


68 
syntax sats :: "[i,i,i] => o"


69 
translations "sats(A,p,env)" == "satisfies(A,p)`env = 1"


70 


71 
lemma [simp]:


72 
"env \<in> list(A)


73 
==> sats(A, Member(x,y), env) <> nth(x,env) \<in> nth(y,env)"


74 
by simp


75 


76 
lemma [simp]:


77 
"env \<in> list(A)


78 
==> sats(A, Equal(x,y), env) <> nth(x,env) = nth(y,env)"


79 
by simp


80 


81 
lemma sats_Neg_iff [simp]:


82 
"env \<in> list(A)


83 
==> sats(A, Neg(p), env) <> ~ sats(A,p,env)"


84 
by (simp add: Bool.not_def cond_def)


85 


86 
lemma sats_And_iff [simp]:


87 
"env \<in> list(A)


88 
==> (sats(A, And(p,q), env)) <> sats(A,p,env) & sats(A,q,env)"


89 
by (simp add: Bool.and_def cond_def)


90 


91 
lemma sats_Forall_iff [simp]:


92 
"env \<in> list(A)


93 
==> sats(A, Forall(p), env) <> (\<forall>x\<in>A. sats(A, p, Cons(x,env)))"


94 
by simp


95 


96 
declare satisfies.simps [simp del];


97 

13298

98 
subsection{*Dividing line between primitive and derived connectives*}

13223

99 


100 
lemma sats_Or_iff [simp]:


101 
"env \<in> list(A)


102 
==> (sats(A, Or(p,q), env)) <> sats(A,p,env)  sats(A,q,env)"


103 
by (simp add: Or_def)


104 


105 
lemma sats_Implies_iff [simp]:


106 
"env \<in> list(A)


107 
==> (sats(A, Implies(p,q), env)) <> (sats(A,p,env) > sats(A,q,env))"

13291

108 
by (simp add: Implies_def, blast)


109 


110 
lemma sats_Iff_iff [simp]:


111 
"env \<in> list(A)


112 
==> (sats(A, Iff(p,q), env)) <> (sats(A,p,env) <> sats(A,q,env))"


113 
by (simp add: Iff_def, blast)

13223

114 


115 
lemma sats_Exists_iff [simp]:


116 
"env \<in> list(A)


117 
==> sats(A, Exists(p), env) <> (\<exists>x\<in>A. sats(A, p, Cons(x,env)))"


118 
by (simp add: Exists_def)


119 


120 

13291

121 
subsubsection{*Derived rules to help build up formulas*}


122 


123 
lemma mem_iff_sats:


124 
"[ nth(i,env) = x; nth(j,env) = y; env \<in> list(A)]


125 
==> (x\<in>y) <> sats(A, Member(i,j), env)"


126 
by (simp add: satisfies.simps)


127 

13298

128 
lemma equal_iff_sats:


129 
"[ nth(i,env) = x; nth(j,env) = y; env \<in> list(A)]


130 
==> (x=y) <> sats(A, Equal(i,j), env)"


131 
by (simp add: satisfies.simps)


132 

13316

133 
lemma not_iff_sats:


134 
"[ P <> sats(A,p,env); env \<in> list(A)]


135 
==> (~P) <> sats(A, Neg(p), env)"


136 
by simp


137 

13291

138 
lemma conj_iff_sats:


139 
"[ P <> sats(A,p,env); Q <> sats(A,q,env); env \<in> list(A)]


140 
==> (P & Q) <> sats(A, And(p,q), env)"


141 
by (simp add: sats_And_iff)


142 


143 
lemma disj_iff_sats:


144 
"[ P <> sats(A,p,env); Q <> sats(A,q,env); env \<in> list(A)]


145 
==> (P  Q) <> sats(A, Or(p,q), env)"


146 
by (simp add: sats_Or_iff)


147 


148 
lemma imp_iff_sats:


149 
"[ P <> sats(A,p,env); Q <> sats(A,q,env); env \<in> list(A)]


150 
==> (P > Q) <> sats(A, Implies(p,q), env)"


151 
by (simp add: sats_Forall_iff)


152 


153 
lemma iff_iff_sats:


154 
"[ P <> sats(A,p,env); Q <> sats(A,q,env); env \<in> list(A)]


155 
==> (P <> Q) <> sats(A, Iff(p,q), env)"


156 
by (simp add: sats_Forall_iff)


157 


158 
lemma imp_iff_sats:


159 
"[ P <> sats(A,p,env); Q <> sats(A,q,env); env \<in> list(A)]


160 
==> (P > Q) <> sats(A, Implies(p,q), env)"


161 
by (simp add: sats_Forall_iff)


162 


163 
lemma ball_iff_sats:


164 
"[ !!x. x\<in>A ==> P(x) <> sats(A, p, Cons(x, env)); env \<in> list(A)]


165 
==> (\<forall>x\<in>A. P(x)) <> sats(A, Forall(p), env)"


166 
by (simp add: sats_Forall_iff)


167 


168 
lemma bex_iff_sats:


169 
"[ !!x. x\<in>A ==> P(x) <> sats(A, p, Cons(x, env)); env \<in> list(A)]


170 
==> (\<exists>x\<in>A. P(x)) <> sats(A, Exists(p), env)"


171 
by (simp add: sats_Exists_iff)


172 

13316

173 
lemmas FOL_iff_sats =


174 
mem_iff_sats equal_iff_sats not_iff_sats conj_iff_sats


175 
disj_iff_sats imp_iff_sats iff_iff_sats imp_iff_sats ball_iff_sats


176 
bex_iff_sats

13223

177 


178 
constdefs incr_var :: "[i,i]=>i"


179 
"incr_var(x,lev) == if x<lev then x else succ(x)"


180 


181 
lemma incr_var_lt: "x<lev ==> incr_var(x,lev) = x"


182 
by (simp add: incr_var_def)


183 


184 
lemma incr_var_le: "lev\<le>x ==> incr_var(x,lev) = succ(x)"


185 
apply (simp add: incr_var_def)


186 
apply (blast dest: lt_trans1)


187 
done


188 


189 
consts incr_bv :: "i=>i"


190 
primrec


191 
"incr_bv(Member(x,y)) =


192 
(\<lambda>lev \<in> nat. Member (incr_var(x,lev), incr_var(y,lev)))"


193 


194 
"incr_bv(Equal(x,y)) =


195 
(\<lambda>lev \<in> nat. Equal (incr_var(x,lev), incr_var(y,lev)))"


196 


197 
"incr_bv(Neg(p)) =


198 
(\<lambda>lev \<in> nat. Neg(incr_bv(p)`lev))"


199 


200 
"incr_bv(And(p,q)) =


201 
(\<lambda>lev \<in> nat. And (incr_bv(p)`lev, incr_bv(q)`lev))"


202 


203 
"incr_bv(Forall(p)) =


204 
(\<lambda>lev \<in> nat. Forall (incr_bv(p) ` succ(lev)))"


205 


206 


207 
constdefs incr_boundvars :: "i => i"


208 
"incr_boundvars(p) == incr_bv(p)`0"


209 


210 


211 
lemma [TC]: "x \<in> nat ==> incr_var(x,lev) \<in> nat"


212 
by (simp add: incr_var_def)


213 


214 
lemma incr_bv_type [TC]: "p \<in> formula ==> incr_bv(p) \<in> nat > formula"


215 
by (induct_tac p, simp_all)


216 


217 
lemma incr_boundvars_type [TC]: "p \<in> formula ==> incr_boundvars(p) \<in> formula"


218 
by (simp add: incr_boundvars_def)


219 


220 
(*Obviously DPow is closed under complements and finite intersections and


221 
unions. Needs an inductive lemma to allow two lists of parameters to


222 
be combined.*)


223 


224 
lemma sats_incr_bv_iff [rule_format]:


225 
"[ p \<in> formula; env \<in> list(A); x \<in> A ]


226 
==> \<forall>bvs \<in> list(A).


227 
sats(A, incr_bv(p) ` length(bvs), bvs @ Cons(x,env)) <>


228 
sats(A, p, bvs@env)"


229 
apply (induct_tac p)


230 
apply (simp_all add: incr_var_def nth_append succ_lt_iff length_type)


231 
apply (auto simp add: diff_succ not_lt_iff_le)


232 
done


233 


234 
(*UNUSED*)


235 
lemma sats_incr_boundvars_iff:


236 
"[ p \<in> formula; env \<in> list(A); x \<in> A ]


237 
==> sats(A, incr_boundvars(p), Cons(x,env)) <> sats(A, p, env)"


238 
apply (insert sats_incr_bv_iff [of p env A x Nil])


239 
apply (simp add: incr_boundvars_def)


240 
done


241 


242 
(*UNUSED


243 
lemma formula_add_params [rule_format]:


244 
"[ p \<in> formula; n \<in> nat ]


245 
==> \<forall>bvs \<in> list(A). \<forall>env \<in> list(A).


246 
length(bvs) = n >


247 
sats(A, iterates(incr_boundvars,n,p), bvs@env) <> sats(A, p, env)"


248 
apply (induct_tac n, simp, clarify)


249 
apply (erule list.cases)


250 
apply (auto simp add: sats_incr_boundvars_iff)


251 
done


252 
*)


253 


254 
consts arity :: "i=>i"


255 
primrec


256 
"arity(Member(x,y)) = succ(x) \<union> succ(y)"


257 


258 
"arity(Equal(x,y)) = succ(x) \<union> succ(y)"


259 


260 
"arity(Neg(p)) = arity(p)"


261 


262 
"arity(And(p,q)) = arity(p) \<union> arity(q)"


263 

13269

264 
"arity(Forall(p)) = nat_case(0, %x. x, arity(p))"

13223

265 


266 


267 
lemma arity_type [TC]: "p \<in> formula ==> arity(p) \<in> nat"


268 
by (induct_tac p, simp_all)


269 


270 
lemma arity_Or [simp]: "arity(Or(p,q)) = arity(p) \<union> arity(q)"


271 
by (simp add: Or_def)


272 


273 
lemma arity_Implies [simp]: "arity(Implies(p,q)) = arity(p) \<union> arity(q)"


274 
by (simp add: Implies_def)


275 

13291

276 
lemma arity_Iff [simp]: "arity(Iff(p,q)) = arity(p) \<union> arity(q)"


277 
by (simp add: Iff_def, blast)


278 

13269

279 
lemma arity_Exists [simp]: "arity(Exists(p)) = nat_case(0, %x. x, arity(p))"

13223

280 
by (simp add: Exists_def)


281 


282 


283 
lemma arity_sats_iff [rule_format]:


284 
"[ p \<in> formula; extra \<in> list(A) ]


285 
==> \<forall>env \<in> list(A).


286 
arity(p) \<le> length(env) >


287 
sats(A, p, env @ extra) <> sats(A, p, env)"


288 
apply (induct_tac p)

13269

289 
apply (simp_all add: nth_append Un_least_lt_iff arity_type nat_imp_quasinat


290 
split: split_nat_case, auto)

13223

291 
done


292 


293 
lemma arity_sats1_iff:


294 
"[ arity(p) \<le> succ(length(env)); p \<in> formula; x \<in> A; env \<in> list(A);


295 
extra \<in> list(A) ]


296 
==> sats(A, p, Cons(x, env @ extra)) <> sats(A, p, Cons(x, env))"


297 
apply (insert arity_sats_iff [of p extra A "Cons(x,env)"])


298 
apply simp


299 
done


300 


301 
(*the following two lemmas prevent huge case splits in arity_incr_bv_lemma*)


302 
lemma incr_var_lemma:


303 
"[ x \<in> nat; y \<in> nat; lev \<le> x ]


304 
==> succ(x) \<union> incr_var(y,lev) = succ(x \<union> y)"


305 
apply (simp add: incr_var_def Ord_Un_if, auto)


306 
apply (blast intro: leI)


307 
apply (simp add: not_lt_iff_le)


308 
apply (blast intro: le_anti_sym)


309 
apply (blast dest: lt_trans2)


310 
done


311 


312 
lemma incr_And_lemma:


313 
"y < x ==> y \<union> succ(x) = succ(x \<union> y)"


314 
apply (simp add: Ord_Un_if lt_Ord lt_Ord2 succ_lt_iff)


315 
apply (blast dest: lt_asym)


316 
done


317 


318 
lemma arity_incr_bv_lemma [rule_format]:


319 
"p \<in> formula


320 
==> \<forall>n \<in> nat. arity (incr_bv(p) ` n) =


321 
(if n < arity(p) then succ(arity(p)) else arity(p))"


322 
apply (induct_tac p)


323 
apply (simp_all add: imp_disj not_lt_iff_le Un_least_lt_iff lt_Un_iff le_Un_iff


324 
succ_Un_distrib [symmetric] incr_var_lt incr_var_le

13269

325 
Un_commute incr_var_lemma arity_type nat_imp_quasinat


326 
split: split_nat_case)


327 
txt{*the Forall case reduces to linear arithmetic*}


328 
prefer 2


329 
apply clarify


330 
apply (blast dest: lt_trans1)


331 
txt{*left with the And case*}

13223

332 
apply safe


333 
apply (blast intro: incr_And_lemma lt_trans1)


334 
apply (subst incr_And_lemma)

13269

335 
apply (blast intro: lt_trans1)


336 
apply (simp add: Un_commute)

13223

337 
done


338 


339 
lemma arity_incr_boundvars_eq:


340 
"p \<in> formula


341 
==> arity(incr_boundvars(p)) =


342 
(if 0 < arity(p) then succ(arity(p)) else arity(p))"


343 
apply (insert arity_incr_bv_lemma [of p 0])


344 
apply (simp add: incr_boundvars_def)


345 
done


346 


347 
lemma arity_iterates_incr_boundvars_eq:


348 
"[ p \<in> formula; n \<in> nat ]


349 
==> arity(incr_boundvars^n(p)) =


350 
(if 0 < arity(p) then n #+ arity(p) else arity(p))"


351 
apply (induct_tac n)


352 
apply (simp_all add: arity_incr_boundvars_eq not_lt_iff_le)


353 
done


354 


355 

13298

356 
subsection{*Renaming all but the first bound variable*}

13223

357 


358 
constdefs incr_bv1 :: "i => i"


359 
"incr_bv1(p) == incr_bv(p)`1"


360 


361 


362 
lemma incr_bv1_type [TC]: "p \<in> formula ==> incr_bv1(p) \<in> formula"


363 
by (simp add: incr_bv1_def)


364 


365 
(*For renaming all but the bound variable at level 0*)


366 
lemma sats_incr_bv1_iff [rule_format]:


367 
"[ p \<in> formula; env \<in> list(A); x \<in> A; y \<in> A ]


368 
==> sats(A, incr_bv1(p), Cons(x, Cons(y, env))) <>


369 
sats(A, p, Cons(x,env))"


370 
apply (insert sats_incr_bv_iff [of p env A y "Cons(x,Nil)"])


371 
apply (simp add: incr_bv1_def)


372 
done


373 


374 
lemma formula_add_params1 [rule_format]:


375 
"[ p \<in> formula; n \<in> nat; x \<in> A ]


376 
==> \<forall>bvs \<in> list(A). \<forall>env \<in> list(A).


377 
length(bvs) = n >


378 
sats(A, iterates(incr_bv1, n, p), Cons(x, bvs@env)) <>


379 
sats(A, p, Cons(x,env))"


380 
apply (induct_tac n, simp, clarify)


381 
apply (erule list.cases)


382 
apply (simp_all add: sats_incr_bv1_iff)


383 
done


384 


385 


386 
lemma arity_incr_bv1_eq:


387 
"p \<in> formula


388 
==> arity(incr_bv1(p)) =


389 
(if 1 < arity(p) then succ(arity(p)) else arity(p))"


390 
apply (insert arity_incr_bv_lemma [of p 1])


391 
apply (simp add: incr_bv1_def)


392 
done


393 


394 
lemma arity_iterates_incr_bv1_eq:


395 
"[ p \<in> formula; n \<in> nat ]


396 
==> arity(incr_bv1^n(p)) =


397 
(if 1 < arity(p) then n #+ arity(p) else arity(p))"


398 
apply (induct_tac n)

13298

399 
apply (simp_all add: arity_incr_bv1_eq)

13223

400 
apply (simp add: not_lt_iff_le)


401 
apply (blast intro: le_trans add_le_self2 arity_type)


402 
done


403 


404 


405 
(*Definable powerset operation: Kunen's definition 1.1, page 165.*)


406 
constdefs DPow :: "i => i"


407 
"DPow(A) == {X \<in> Pow(A).


408 
\<exists>env \<in> list(A). \<exists>p \<in> formula.


409 
arity(p) \<le> succ(length(env)) &


410 
X = {x\<in>A. sats(A, p, Cons(x,env))}}"


411 


412 
lemma DPowI:

13291

413 
"[env \<in> list(A); p \<in> formula; arity(p) \<le> succ(length(env))]

13223

414 
==> {x\<in>A. sats(A, p, Cons(x,env))} \<in> DPow(A)"


415 
by (simp add: DPow_def, blast)


416 

13291

417 
text{*With this rule we can specify @{term p} later.*}


418 
lemma DPowI2 [rule_format]:


419 
"[\<forall>x\<in>A. P(x) <> sats(A, p, Cons(x,env));


420 
env \<in> list(A); p \<in> formula; arity(p) \<le> succ(length(env))]


421 
==> {x\<in>A. P(x)} \<in> DPow(A)"


422 
by (simp add: DPow_def, blast)


423 

13223

424 
lemma DPowD:


425 
"X \<in> DPow(A)


426 
==> X <= A &


427 
(\<exists>env \<in> list(A).


428 
\<exists>p \<in> formula. arity(p) \<le> succ(length(env)) &


429 
X = {x\<in>A. sats(A, p, Cons(x,env))})"


430 
by (simp add: DPow_def)


431 


432 
lemmas DPow_imp_subset = DPowD [THEN conjunct1]


433 


434 
(*Lemma 1.2*)


435 
lemma "[ p \<in> formula; env \<in> list(A); arity(p) \<le> succ(length(env)) ]


436 
==> {x\<in>A. sats(A, p, Cons(x,env))} \<in> DPow(A)"


437 
by (blast intro: DPowI)


438 


439 
lemma DPow_subset_Pow: "DPow(A) <= Pow(A)"


440 
by (simp add: DPow_def, blast)


441 


442 
lemma empty_in_DPow: "0 \<in> DPow(A)"


443 
apply (simp add: DPow_def)


444 
apply (rule_tac x="Nil" in bexI)


445 
apply (rule_tac x="Neg(Equal(0,0))" in bexI)


446 
apply (auto simp add: Un_least_lt_iff)


447 
done


448 


449 
lemma Compl_in_DPow: "X \<in> DPow(A) ==> (AX) \<in> DPow(A)"


450 
apply (simp add: DPow_def, clarify, auto)


451 
apply (rule bexI)


452 
apply (rule_tac x="Neg(p)" in bexI)


453 
apply auto


454 
done


455 


456 
lemma Int_in_DPow: "[ X \<in> DPow(A); Y \<in> DPow(A) ] ==> X Int Y \<in> DPow(A)"


457 
apply (simp add: DPow_def, auto)


458 
apply (rename_tac envp p envq q)


459 
apply (rule_tac x="envp@envq" in bexI)


460 
apply (rule_tac x="And(p, iterates(incr_bv1,length(envp),q))" in bexI)


461 
apply typecheck


462 
apply (rule conjI)


463 
(*finally check the arity!*)


464 
apply (simp add: arity_iterates_incr_bv1_eq length_app Un_least_lt_iff)


465 
apply (force intro: add_le_self le_trans)


466 
apply (simp add: arity_sats1_iff formula_add_params1, blast)


467 
done


468 


469 
lemma Un_in_DPow: "[ X \<in> DPow(A); Y \<in> DPow(A) ] ==> X Un Y \<in> DPow(A)"


470 
apply (subgoal_tac "X Un Y = A  ((AX) Int (AY))")


471 
apply (simp add: Int_in_DPow Compl_in_DPow)


472 
apply (simp add: DPow_def, blast)


473 
done


474 


475 
lemma singleton_in_DPow: "x \<in> A ==> {x} \<in> DPow(A)"


476 
apply (simp add: DPow_def)


477 
apply (rule_tac x="Cons(x,Nil)" in bexI)


478 
apply (rule_tac x="Equal(0,1)" in bexI)


479 
apply typecheck


480 
apply (force simp add: succ_Un_distrib [symmetric])


481 
done


482 


483 
lemma cons_in_DPow: "[ a \<in> A; X \<in> DPow(A) ] ==> cons(a,X) \<in> DPow(A)"


484 
apply (rule cons_eq [THEN subst])


485 
apply (blast intro: singleton_in_DPow Un_in_DPow)


486 
done


487 


488 
(*Part of Lemma 1.3*)


489 
lemma Fin_into_DPow: "X \<in> Fin(A) ==> X \<in> DPow(A)"


490 
apply (erule Fin.induct)


491 
apply (rule empty_in_DPow)


492 
apply (blast intro: cons_in_DPow)


493 
done


494 


495 
(*DPow is not monotonic. For example, let A be some nonconstructible set


496 
of natural numbers, and let B be nat. Then A<=B and obviously A : DPow(A)


497 
but A ~: DPow(B).*)


498 
lemma DPow_mono: "A : DPow(B) ==> DPow(A) <= DPow(B)"


499 
apply (simp add: DPow_def, auto)


500 
(*must use the formula defining A in B to relativize the new formula...*)


501 
oops


502 


503 
lemma DPow_0: "DPow(0) = {0}"


504 
by (blast intro: empty_in_DPow dest: DPow_imp_subset)


505 


506 
lemma Finite_Pow_subset_Pow: "Finite(A) ==> Pow(A) <= DPow(A)"


507 
by (blast intro: Fin_into_DPow Finite_into_Fin Fin_subset)


508 


509 
lemma Finite_DPow_eq_Pow: "Finite(A) ==> DPow(A) = Pow(A)"


510 
apply (rule equalityI)


511 
apply (rule DPow_subset_Pow)


512 
apply (erule Finite_Pow_subset_Pow)


513 
done


514 


515 
(*This may be true but the proof looks difficult, requiring relativization


516 
lemma DPow_insert: "DPow (cons(a,A)) = DPow(A) Un {cons(a,X) . X: DPow(A)}"


517 
apply (rule equalityI, safe)


518 
oops


519 
*)


520 

13298

521 


522 
subsection{*Internalized formulas for basic concepts*}


523 


524 
subsubsection{*The subset relation*}


525 


526 
constdefs subset_fm :: "[i,i]=>i"


527 
"subset_fm(x,y) == Forall(Implies(Member(0,succ(x)), Member(0,succ(y))))"


528 


529 
lemma subset_type [TC]: "[ x \<in> nat; y \<in> nat ] ==> subset_fm(x,y) \<in> formula"


530 
by (simp add: subset_fm_def)


531 


532 
lemma arity_subset_fm [simp]:


533 
"[ x \<in> nat; y \<in> nat ] ==> arity(subset_fm(x,y)) = succ(x) \<union> succ(y)"


534 
by (simp add: subset_fm_def succ_Un_distrib [symmetric])


535 


536 
lemma sats_subset_fm [simp]:


537 
"[x < length(env); y \<in> nat; env \<in> list(A); Transset(A)]


538 
==> sats(A, subset_fm(x,y), env) <> nth(x,env) \<subseteq> nth(y,env)"


539 
apply (frule lt_length_in_nat, assumption)


540 
apply (simp add: subset_fm_def Transset_def)


541 
apply (blast intro: nth_type)


542 
done


543 


544 
subsubsection{*Transitive sets*}


545 


546 
constdefs transset_fm :: "i=>i"


547 
"transset_fm(x) == Forall(Implies(Member(0,succ(x)), subset_fm(0,succ(x))))"


548 


549 
lemma transset_type [TC]: "x \<in> nat ==> transset_fm(x) \<in> formula"


550 
by (simp add: transset_fm_def)


551 


552 
lemma arity_transset_fm [simp]:


553 
"x \<in> nat ==> arity(transset_fm(x)) = succ(x)"


554 
by (simp add: transset_fm_def succ_Un_distrib [symmetric])


555 


556 
lemma sats_transset_fm [simp]:


557 
"[x < length(env); env \<in> list(A); Transset(A)]


558 
==> sats(A, transset_fm(x), env) <> Transset(nth(x,env))"


559 
apply (frule lt_nat_in_nat, erule length_type)


560 
apply (simp add: transset_fm_def Transset_def)


561 
apply (blast intro: nth_type)


562 
done


563 


564 
subsubsection{*Ordinals*}


565 


566 
constdefs ordinal_fm :: "i=>i"


567 
"ordinal_fm(x) ==


568 
And(transset_fm(x), Forall(Implies(Member(0,succ(x)), transset_fm(0))))"


569 


570 
lemma ordinal_type [TC]: "x \<in> nat ==> ordinal_fm(x) \<in> formula"


571 
by (simp add: ordinal_fm_def)


572 


573 
lemma arity_ordinal_fm [simp]:


574 
"x \<in> nat ==> arity(ordinal_fm(x)) = succ(x)"


575 
by (simp add: ordinal_fm_def succ_Un_distrib [symmetric])


576 

13306

577 
lemma sats_ordinal_fm:

13298

578 
"[x < length(env); env \<in> list(A); Transset(A)]


579 
==> sats(A, ordinal_fm(x), env) <> Ord(nth(x,env))"


580 
apply (frule lt_nat_in_nat, erule length_type)


581 
apply (simp add: ordinal_fm_def Ord_def Transset_def)


582 
apply (blast intro: nth_type)


583 
done


584 


585 

13223

586 
subsection{* Constant Lset: Levels of the Constructible Universe *}


587 


588 
constdefs Lset :: "i=>i"


589 
"Lset(i) == transrec(i, %x f. \<Union>y\<in>x. DPow(f`y))"


590 


591 
text{*NOT SUITABLE FOR REWRITING  RECURSIVE!*}


592 
lemma Lset: "Lset(i) = (UN j:i. DPow(Lset(j)))"


593 
by (subst Lset_def [THEN def_transrec], simp)


594 


595 
lemma LsetI: "[y\<in>x; A \<in> DPow(Lset(y))] ==> A \<in> Lset(x)";


596 
by (subst Lset, blast)


597 


598 
lemma LsetD: "A \<in> Lset(x) ==> \<exists>y\<in>x. A \<in> DPow(Lset(y))";


599 
apply (insert Lset [of x])


600 
apply (blast intro: elim: equalityE)


601 
done


602 


603 
subsubsection{* Transitivity *}


604 


605 
lemma elem_subset_in_DPow: "[X \<in> A; X \<subseteq> A] ==> X \<in> DPow(A)"


606 
apply (simp add: Transset_def DPow_def)


607 
apply (rule_tac x="[X]" in bexI)


608 
apply (rule_tac x="Member(0,1)" in bexI)


609 
apply (auto simp add: Un_least_lt_iff)


610 
done


611 


612 
lemma Transset_subset_DPow: "Transset(A) ==> A <= DPow(A)"


613 
apply clarify


614 
apply (simp add: Transset_def)


615 
apply (blast intro: elem_subset_in_DPow)


616 
done


617 


618 
lemma Transset_DPow: "Transset(A) ==> Transset(DPow(A))"


619 
apply (simp add: Transset_def)


620 
apply (blast intro: elem_subset_in_DPow dest: DPowD)


621 
done


622 


623 
text{*Kunen's VI, 1.6 (a)*}


624 
lemma Transset_Lset: "Transset(Lset(i))"


625 
apply (rule_tac a=i in eps_induct)


626 
apply (subst Lset)


627 
apply (blast intro!: Transset_Union_family Transset_Un Transset_DPow)


628 
done


629 

13291

630 
lemma mem_Lset_imp_subset_Lset: "a \<in> Lset(i) ==> a \<subseteq> Lset(i)"


631 
apply (insert Transset_Lset)


632 
apply (simp add: Transset_def)


633 
done


634 

13223

635 
subsubsection{* Monotonicity *}


636 


637 
text{*Kunen's VI, 1.6 (b)*}


638 
lemma Lset_mono [rule_format]:


639 
"ALL j. i<=j > Lset(i) <= Lset(j)"


640 
apply (rule_tac a=i in eps_induct)


641 
apply (rule impI [THEN allI])


642 
apply (subst Lset)


643 
apply (subst Lset, blast)


644 
done


645 


646 
text{*This version lets us remove the premise @{term "Ord(i)"} sometimes.*}


647 
lemma Lset_mono_mem [rule_format]:


648 
"ALL j. i:j > Lset(i) <= Lset(j)"


649 
apply (rule_tac a=i in eps_induct)


650 
apply (rule impI [THEN allI])


651 
apply (subst Lset, auto)


652 
apply (rule rev_bexI, assumption)


653 
apply (blast intro: elem_subset_in_DPow dest: LsetD DPowD)


654 
done


655 

13291

656 
text{*Useful with Reflection to bump up the ordinal*}


657 
lemma subset_Lset_ltD: "[A \<subseteq> Lset(i); i < j] ==> A \<subseteq> Lset(j)"


658 
by (blast dest: ltD [THEN Lset_mono_mem])


659 

13223

660 
subsubsection{* 0, successor and limit equations fof Lset *}


661 


662 
lemma Lset_0 [simp]: "Lset(0) = 0"


663 
by (subst Lset, blast)


664 


665 
lemma Lset_succ_subset1: "DPow(Lset(i)) <= Lset(succ(i))"


666 
by (subst Lset, rule succI1 [THEN RepFunI, THEN Union_upper])


667 


668 
lemma Lset_succ_subset2: "Lset(succ(i)) <= DPow(Lset(i))"


669 
apply (subst Lset, rule UN_least)


670 
apply (erule succE)


671 
apply blast


672 
apply clarify


673 
apply (rule elem_subset_in_DPow)


674 
apply (subst Lset)


675 
apply blast


676 
apply (blast intro: dest: DPowD Lset_mono_mem)


677 
done


678 


679 
lemma Lset_succ: "Lset(succ(i)) = DPow(Lset(i))"


680 
by (intro equalityI Lset_succ_subset1 Lset_succ_subset2)


681 


682 
lemma Lset_Union [simp]: "Lset(\<Union>(X)) = (\<Union>y\<in>X. Lset(y))"


683 
apply (subst Lset)


684 
apply (rule equalityI)


685 
txt{*first inclusion*}


686 
apply (rule UN_least)


687 
apply (erule UnionE)


688 
apply (rule subset_trans)


689 
apply (erule_tac [2] UN_upper, subst Lset, erule UN_upper)


690 
txt{*opposite inclusion*}


691 
apply (rule UN_least)


692 
apply (subst Lset, blast)


693 
done


694 


695 
subsubsection{* Lset applied to Limit ordinals *}


696 


697 
lemma Limit_Lset_eq:


698 
"Limit(i) ==> Lset(i) = (\<Union>y\<in>i. Lset(y))"


699 
by (simp add: Lset_Union [symmetric] Limit_Union_eq)


700 


701 
lemma lt_LsetI: "[ a: Lset(j); j<i ] ==> a : Lset(i)"


702 
by (blast dest: Lset_mono [OF le_imp_subset [OF leI]])


703 


704 
lemma Limit_LsetE:


705 
"[ a: Lset(i); ~R ==> Limit(i);


706 
!!x. [ x<i; a: Lset(x) ] ==> R


707 
] ==> R"


708 
apply (rule classical)


709 
apply (rule Limit_Lset_eq [THEN equalityD1, THEN subsetD, THEN UN_E])


710 
prefer 2 apply assumption


711 
apply blast


712 
apply (blast intro: ltI Limit_is_Ord)


713 
done


714 


715 
subsubsection{* Basic closure properties *}


716 


717 
lemma zero_in_Lset: "y:x ==> 0 : Lset(x)"


718 
by (subst Lset, blast intro: empty_in_DPow)


719 


720 
lemma notin_Lset: "x \<notin> Lset(x)"


721 
apply (rule_tac a=x in eps_induct)


722 
apply (subst Lset)


723 
apply (blast dest: DPowD)


724 
done


725 


726 

13298

727 
subsection{*Constructible Ordinals: Kunen's VI, 1.9 (b)*}

13223

728 


729 
text{*The subset consisting of the ordinals is definable.*}


730 
lemma Ords_in_DPow: "Transset(A) ==> {x \<in> A. Ord(x)} \<in> DPow(A)"


731 
apply (simp add: DPow_def Collect_subset)


732 
apply (rule_tac x="Nil" in bexI)


733 
apply (rule_tac x="ordinal_fm(0)" in bexI)


734 
apply (simp_all add: sats_ordinal_fm)


735 
done


736 


737 
lemma Ords_of_Lset_eq: "Ord(i) ==> {x\<in>Lset(i). Ord(x)} = i"


738 
apply (erule trans_induct3)


739 
apply (simp_all add: Lset_succ Limit_Lset_eq Limit_Union_eq)


740 
txt{*The successor case remains.*}


741 
apply (rule equalityI)


742 
txt{*First inclusion*}


743 
apply clarify


744 
apply (erule Ord_linear_lt, assumption)


745 
apply (blast dest: DPow_imp_subset ltD notE [OF notin_Lset])


746 
apply blast


747 
apply (blast dest: ltD)


748 
txt{*Opposite inclusion, @{term "succ(x) \<subseteq> DPow(Lset(x)) \<inter> ON"}*}


749 
apply auto


750 
txt{*Key case: *}


751 
apply (erule subst, rule Ords_in_DPow [OF Transset_Lset])


752 
apply (blast intro: elem_subset_in_DPow dest: OrdmemD elim: equalityE)


753 
apply (blast intro: Ord_in_Ord)


754 
done


755 


756 


757 
lemma Ord_subset_Lset: "Ord(i) ==> i \<subseteq> Lset(i)"


758 
by (subst Ords_of_Lset_eq [symmetric], assumption, fast)


759 


760 
lemma Ord_in_Lset: "Ord(i) ==> i \<in> Lset(succ(i))"


761 
apply (simp add: Lset_succ)


762 
apply (subst Ords_of_Lset_eq [symmetric], assumption,


763 
rule Ords_in_DPow [OF Transset_Lset])


764 
done


765 


766 
subsubsection{* Unions *}


767 


768 
lemma Union_in_Lset:


769 
"X \<in> Lset(j) ==> Union(X) \<in> Lset(succ(j))"


770 
apply (insert Transset_Lset)


771 
apply (rule LsetI [OF succI1])


772 
apply (simp add: Transset_def DPow_def)


773 
apply (intro conjI, blast)


774 
txt{*Now to create the formula @{term "\<exists>y. y \<in> X \<and> x \<in> y"} *}


775 
apply (rule_tac x="Cons(X,Nil)" in bexI)


776 
apply (rule_tac x="Exists(And(Member(0,2), Member(1,0)))" in bexI)


777 
apply typecheck


778 
apply (simp add: succ_Un_distrib [symmetric], blast)


779 
done


780 


781 
lemma Union_in_LLimit:


782 
"[ X: Lset(i); Limit(i) ] ==> Union(X) : Lset(i)"


783 
apply (rule Limit_LsetE, assumption+)


784 
apply (blast intro: Limit_has_succ lt_LsetI Union_in_Lset)


785 
done


786 


787 
subsubsection{* Finite sets and ordered pairs *}


788 


789 
lemma singleton_in_Lset: "a: Lset(i) ==> {a} : Lset(succ(i))"


790 
by (simp add: Lset_succ singleton_in_DPow)


791 


792 
lemma doubleton_in_Lset:


793 
"[ a: Lset(i); b: Lset(i) ] ==> {a,b} : Lset(succ(i))"


794 
by (simp add: Lset_succ empty_in_DPow cons_in_DPow)


795 


796 
lemma Pair_in_Lset:


797 
"[ a: Lset(i); b: Lset(i); Ord(i) ] ==> <a,b> : Lset(succ(succ(i)))"


798 
apply (unfold Pair_def)


799 
apply (blast intro: doubleton_in_Lset)


800 
done


801 


802 
lemmas zero_in_LLimit = Limit_has_0 [THEN ltD, THEN zero_in_Lset, standard]


803 


804 
lemma singleton_in_LLimit:


805 
"[ a: Lset(i); Limit(i) ] ==> {a} : Lset(i)"


806 
apply (erule Limit_LsetE, assumption)


807 
apply (erule singleton_in_Lset [THEN lt_LsetI])


808 
apply (blast intro: Limit_has_succ)


809 
done


810 


811 
lemmas Lset_UnI1 = Un_upper1 [THEN Lset_mono [THEN subsetD], standard]


812 
lemmas Lset_UnI2 = Un_upper2 [THEN Lset_mono [THEN subsetD], standard]


813 


814 
text{*Hard work is finding a single j:i such that {a,b}<=Lset(j)*}


815 
lemma doubleton_in_LLimit:


816 
"[ a: Lset(i); b: Lset(i); Limit(i) ] ==> {a,b} : Lset(i)"


817 
apply (erule Limit_LsetE, assumption)


818 
apply (erule Limit_LsetE, assumption)

13269

819 
apply (blast intro: lt_LsetI [OF doubleton_in_Lset]


820 
Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt)

13223

821 
done


822 


823 
lemma Pair_in_LLimit:


824 
"[ a: Lset(i); b: Lset(i); Limit(i) ] ==> <a,b> : Lset(i)"


825 
txt{*Infer that a, b occur at ordinals x,xa < i.*}


826 
apply (erule Limit_LsetE, assumption)


827 
apply (erule Limit_LsetE, assumption)


828 
txt{*Infer that succ(succ(x Un xa)) < i *}


829 
apply (blast intro: lt_Ord lt_LsetI [OF Pair_in_Lset]


830 
Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt)


831 
done


832 


833 
lemma product_LLimit: "Limit(i) ==> Lset(i) * Lset(i) <= Lset(i)"


834 
by (blast intro: Pair_in_LLimit)


835 


836 
lemmas Sigma_subset_LLimit = subset_trans [OF Sigma_mono product_LLimit]


837 


838 
lemma nat_subset_LLimit: "Limit(i) ==> nat \<subseteq> Lset(i)"


839 
by (blast dest: Ord_subset_Lset nat_le_Limit le_imp_subset Limit_is_Ord)


840 


841 
lemma nat_into_LLimit: "[ n: nat; Limit(i) ] ==> n : Lset(i)"


842 
by (blast intro: nat_subset_LLimit [THEN subsetD])


843 


844 


845 
subsubsection{* Closure under disjoint union *}


846 


847 
lemmas zero_in_LLimit = Limit_has_0 [THEN ltD, THEN zero_in_Lset, standard]


848 


849 
lemma one_in_LLimit: "Limit(i) ==> 1 : Lset(i)"


850 
by (blast intro: nat_into_LLimit)


851 


852 
lemma Inl_in_LLimit:


853 
"[ a: Lset(i); Limit(i) ] ==> Inl(a) : Lset(i)"


854 
apply (unfold Inl_def)


855 
apply (blast intro: zero_in_LLimit Pair_in_LLimit)


856 
done


857 


858 
lemma Inr_in_LLimit:


859 
"[ b: Lset(i); Limit(i) ] ==> Inr(b) : Lset(i)"


860 
apply (unfold Inr_def)


861 
apply (blast intro: one_in_LLimit Pair_in_LLimit)


862 
done


863 


864 
lemma sum_LLimit: "Limit(i) ==> Lset(i) + Lset(i) <= Lset(i)"


865 
by (blast intro!: Inl_in_LLimit Inr_in_LLimit)


866 


867 
lemmas sum_subset_LLimit = subset_trans [OF sum_mono sum_LLimit]


868 


869 


870 
text{*The constructible universe and its rank function*}


871 
constdefs


872 
L :: "i=>o" {*Kunen's definition VI, 1.5, page 167*}


873 
"L(x) == \<exists>i. Ord(i) & x \<in> Lset(i)"


874 


875 
lrank :: "i=>i" {*Kunen's definition VI, 1.7*}


876 
"lrank(x) == \<mu>i. x \<in> Lset(succ(i))"


877 


878 
lemma L_I: "[x \<in> Lset(i); Ord(i)] ==> L(x)"


879 
by (simp add: L_def, blast)


880 


881 
lemma L_D: "L(x) ==> \<exists>i. Ord(i) & x \<in> Lset(i)"


882 
by (simp add: L_def)


883 


884 
lemma Ord_lrank [simp]: "Ord(lrank(a))"


885 
by (simp add: lrank_def)


886 


887 
lemma Lset_lrank_lt [rule_format]: "Ord(i) ==> x \<in> Lset(i) > lrank(x) < i"


888 
apply (erule trans_induct3)


889 
apply simp


890 
apply (simp only: lrank_def)


891 
apply (blast intro: Least_le)


892 
apply (simp_all add: Limit_Lset_eq)


893 
apply (blast intro: ltI Limit_is_Ord lt_trans)


894 
done


895 


896 
text{*Kunen's VI, 1.8, and the proof is much less trivial than the text


897 
would suggest. For a start it need the previous lemma, proved by induction.*}


898 
lemma Lset_iff_lrank_lt: "Ord(i) ==> x \<in> Lset(i) <> L(x) & lrank(x) < i"


899 
apply (simp add: L_def, auto)


900 
apply (blast intro: Lset_lrank_lt)


901 
apply (unfold lrank_def)


902 
apply (drule succI1 [THEN Lset_mono_mem, THEN subsetD])


903 
apply (drule_tac P="\<lambda>i. x \<in> Lset(succ(i))" in LeastI, assumption)


904 
apply (blast intro!: le_imp_subset Lset_mono [THEN subsetD])


905 
done


906 


907 
lemma Lset_succ_lrank_iff [simp]: "x \<in> Lset(succ(lrank(x))) <> L(x)"


908 
by (simp add: Lset_iff_lrank_lt)


909 


910 
text{*Kunen's VI, 1.9 (a)*}


911 
lemma lrank_of_Ord: "Ord(i) ==> lrank(i) = i"


912 
apply (unfold lrank_def)


913 
apply (rule Least_equality)


914 
apply (erule Ord_in_Lset)


915 
apply assumption


916 
apply (insert notin_Lset [of i])


917 
apply (blast intro!: le_imp_subset Lset_mono [THEN subsetD])


918 
done


919 

13245

920 


921 
lemma Ord_in_L: "Ord(i) ==> L(i)"


922 
by (blast intro: Ord_in_Lset L_I)


923 

13223

924 
text{*This is lrank(lrank(a)) = lrank(a) *}


925 
declare Ord_lrank [THEN lrank_of_Ord, simp]


926 


927 
text{*Kunen's VI, 1.10 *}


928 
lemma Lset_in_Lset_succ: "Lset(i) \<in> Lset(succ(i))";


929 
apply (simp add: Lset_succ DPow_def)


930 
apply (rule_tac x="Nil" in bexI)


931 
apply (rule_tac x="Equal(0,0)" in bexI)


932 
apply auto


933 
done


934 


935 
lemma lrank_Lset: "Ord(i) ==> lrank(Lset(i)) = i"


936 
apply (unfold lrank_def)


937 
apply (rule Least_equality)


938 
apply (rule Lset_in_Lset_succ)


939 
apply assumption


940 
apply clarify


941 
apply (subgoal_tac "Lset(succ(ia)) <= Lset(i)")


942 
apply (blast dest: mem_irrefl)


943 
apply (blast intro!: le_imp_subset Lset_mono)


944 
done


945 


946 
text{*Kunen's VI, 1.11 *}


947 
lemma Lset_subset_Vset: "Ord(i) ==> Lset(i) <= Vset(i)";


948 
apply (erule trans_induct)


949 
apply (subst Lset)


950 
apply (subst Vset)


951 
apply (rule UN_mono [OF subset_refl])


952 
apply (rule subset_trans [OF DPow_subset_Pow])


953 
apply (rule Pow_mono, blast)


954 
done


955 


956 
text{*Kunen's VI, 1.12 *}


957 
lemma Lset_subset_Vset: "i \<in> nat ==> Lset(i) = Vset(i)";


958 
apply (erule nat_induct)


959 
apply (simp add: Vfrom_0)


960 
apply (simp add: Lset_succ Vset_succ Finite_Vset Finite_DPow_eq_Pow)


961 
done


962 

13291

963 
text{*Every set of constructible sets is included in some @{term Lset}*}


964 
lemma subset_Lset:


965 
"(\<forall>x\<in>A. L(x)) ==> \<exists>i. Ord(i) & A \<subseteq> Lset(i)"


966 
by (rule_tac x = "\<Union>x\<in>A. succ(lrank(x))" in exI, force)


967 


968 
lemma subset_LsetE:


969 
"[\<forall>x\<in>A. L(x);


970 
!!i. [Ord(i); A \<subseteq> Lset(i)] ==> P]


971 
==> P"


972 
by (blast dest: subset_Lset)


973 

13223

974 
subsection{*For L to satisfy the ZF axioms*}


975 

13245

976 
theorem Union_in_L: "L(X) ==> L(Union(X))"

13223

977 
apply (simp add: L_def, clarify)


978 
apply (drule Ord_imp_greater_Limit)


979 
apply (blast intro: lt_LsetI Union_in_LLimit Limit_is_Ord)


980 
done


981 

13245

982 
theorem doubleton_in_L: "[ L(a); L(b) ] ==> L({a, b})"

13223

983 
apply (simp add: L_def, clarify)


984 
apply (drule Ord2_imp_greater_Limit, assumption)


985 
apply (blast intro: lt_LsetI doubleton_in_LLimit Limit_is_Ord)


986 
done


987 


988 
subsubsection{*For L to satisfy Powerset *}


989 


990 
lemma LPow_env_typing:


991 
"[ y : Lset(i); Ord(i); y \<subseteq> X ] ==> y \<in> (\<Union>y\<in>Pow(X). Lset(succ(lrank(y))))"


992 
by (auto intro: L_I iff: Lset_succ_lrank_iff)


993 


994 
lemma LPow_in_Lset:


995 
"[X \<in> Lset(i); Ord(i)] ==> \<exists>j. Ord(j) & {y \<in> Pow(X). L(y)} \<in> Lset(j)"


996 
apply (rule_tac x="succ(\<Union>y \<in> Pow(X). succ(lrank(y)))" in exI)


997 
apply simp


998 
apply (rule LsetI [OF succI1])


999 
apply (simp add: DPow_def)


1000 
apply (intro conjI, clarify)


1001 
apply (rule_tac a="x" in UN_I, simp+)


1002 
txt{*Now to create the formula @{term "y \<subseteq> X"} *}


1003 
apply (rule_tac x="Cons(X,Nil)" in bexI)


1004 
apply (rule_tac x="subset_fm(0,1)" in bexI)


1005 
apply typecheck


1006 
apply (rule conjI)


1007 
apply (simp add: succ_Un_distrib [symmetric])


1008 
apply (rule equality_iffI)


1009 
apply (simp add: Transset_UN [OF Transset_Lset] list.Cons [OF LPow_env_typing])


1010 
apply (auto intro: L_I iff: Lset_succ_lrank_iff)


1011 
done


1012 

13245

1013 
theorem LPow_in_L: "L(X) ==> L({y \<in> Pow(X). L(y)})"

13223

1014 
by (blast intro: L_I dest: L_D LPow_in_Lset)


1015 


1016 
end
