13223

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


2 


3 
theory Formula = Main:


4 


5 


6 
(*??for Bool.thy**)


7 
constdefs bool_of_o :: "o=>i"


8 
"bool_of_o(P) == (if P then 1 else 0)"


9 


10 
lemma [simp]: "bool_of_o(True) = 1"


11 
by (simp add: bool_of_o_def)


12 


13 
lemma [simp]: "bool_of_o(False) = 0"


14 
by (simp add: bool_of_o_def)


15 


16 
lemma [simp,TC]: "bool_of_o(P) \<in> bool"


17 
by (simp add: bool_of_o_def)


18 


19 
lemma [simp]: "(bool_of_o(P) = 1) <> P"


20 
by (simp add: bool_of_o_def)


21 


22 
lemma [simp]: "(bool_of_o(P) = 0) <> ~P"


23 
by (simp add: bool_of_o_def)


24 


25 
(*????????????????Cardinal.ML*)


26 
lemma Finite_cons_iff [iff]: "Finite(cons(y,x)) <> Finite(x)"


27 
by (blast intro: Finite_cons subset_Finite)


28 


29 
lemma Finite_succ_iff [iff]: "Finite(succ(x)) <> Finite(x)"


30 
by (simp add: succ_def)


31 


32 
declare Finite_0 [simp]


33 


34 
lemma Finite_RepFun: "Finite(A) ==> Finite(RepFun(A,f))"


35 
by (erule Finite_induct, simp_all)


36 


37 
lemma Finite_RepFun_lemma [rule_format]:


38 
"[Finite(x); !!x y. f(x)=f(y) ==> x=y]


39 
==> \<forall>A. x = RepFun(A,f) > Finite(A)"


40 
apply (erule Finite_induct)


41 
apply clarify


42 
apply (case_tac "A=0", simp)


43 
apply (blast del: allE, clarify)


44 
apply (subgoal_tac "\<exists>z\<in>A. x = f(z)")


45 
prefer 2 apply (blast del: allE elim: equalityE, clarify)


46 
apply (subgoal_tac "B = {f(u) . u \<in> A  {z}}")


47 
apply (blast intro: Diff_sing_Finite)


48 
apply (thin_tac "\<forall>A. ?P(A) > Finite(A)")


49 
apply (rule equalityI)


50 
apply (blast intro: elim: equalityE)


51 
apply (blast intro: elim: equalityCE)


52 
done


53 


54 
text{*I don't know why, but if the premise is expressed using metaconnectives


55 
then the simplifier cannot prove it automatically in conditional rewriting.*}


56 
lemma Finite_RepFun_iff:


57 
"(\<forall>x y. f(x)=f(y) > x=y) ==> Finite(RepFun(A,f)) <> Finite(A)"


58 
by (blast intro: Finite_RepFun Finite_RepFun_lemma [of _ f])


59 


60 
lemma Finite_Pow: "Finite(A) ==> Finite(Pow(A))"


61 
apply (erule Finite_induct)


62 
apply (simp_all add: Pow_insert Finite_Un Finite_RepFun)


63 
done


64 


65 
lemma Finite_Pow_imp_Finite: "Finite(Pow(A)) ==> Finite(A)"


66 
apply (subgoal_tac "Finite({{x} . x \<in> A})")


67 
apply (simp add: Finite_RepFun_iff )


68 
apply (blast intro: subset_Finite)


69 
done


70 


71 
lemma Finite_Pow_iff [iff]: "Finite(Pow(A)) <> Finite(A)"


72 
by (blast intro: Finite_Pow Finite_Pow_imp_Finite)


73 


74 
lemma Finite_Vset: "i \<in> nat ==> Finite(Vset(i))";


75 
apply (erule nat_induct)


76 
apply (simp add: Vfrom_0)


77 
apply (simp add: Vset_succ)


78 
done


79 


80 
(*???Ordinal maybe, but some lemmas seem to be in CardinalArith??*)


81 
text{*Every ordinal is exceeded by some limit ordinal.*}


82 
lemma Ord_imp_greater_Limit: "Ord(i) ==> \<exists>k. i<k & Limit(k)"


83 
apply (rule_tac x="i ++ nat" in exI)


84 
apply (blast intro: oadd_LimitI oadd_lt_self Limit_nat [THEN Limit_has_0])


85 
done


86 


87 
lemma Ord2_imp_greater_Limit: "[Ord(i); Ord(j)] ==> \<exists>k. i<k & j<k & Limit(k)"


88 
apply (insert Ord_Un [of i j, THEN Ord_imp_greater_Limit])


89 
apply (simp add: Un_least_lt_iff)


90 
done


91 


92 


93 


94 
(*Internalized formulas of FOL. De Bruijn representation.


95 
Unbound variables get their denotations from an environment.*)


96 


97 
consts formula :: i


98 
datatype


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


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


101 
 Neg ("p: formula")


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


103 
 Forall ("p: formula")


104 


105 
declare formula.intros [TC]


106 


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


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


109 


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


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


112 


113 
constdefs Exists :: "i=>i"


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


115 


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


117 
by (simp add: Or_def)


118 


119 
lemma Implies_type [TC]:


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


121 
by (simp add: Implies_def)


122 


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


124 
by (simp add: Exists_def)


125 


126 


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


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


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


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


131 


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


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


134 


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


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


137 


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


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


140 


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


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


143 


144 


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


146 
by (induct_tac p, simp_all)


147 


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


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


150 


151 
lemma [simp]:


152 
"env \<in> list(A)


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


154 
by simp


155 


156 
lemma [simp]:


157 
"env \<in> list(A)


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


159 
by simp


160 


161 
lemma sats_Neg_iff [simp]:


162 
"env \<in> list(A)


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


164 
by (simp add: Bool.not_def cond_def)


165 


166 
lemma sats_And_iff [simp]:


167 
"env \<in> list(A)


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


169 
by (simp add: Bool.and_def cond_def)


170 


171 
lemma sats_Forall_iff [simp]:


172 
"env \<in> list(A)


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


174 
by simp


175 


176 
declare satisfies.simps [simp del];


177 


178 
(**** DIVIDING LINE BETWEEN PRIMITIVE AND DERIVED CONNECTIVES ****)


179 


180 
lemma sats_Or_iff [simp]:


181 
"env \<in> list(A)


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


183 
by (simp add: Or_def)


184 


185 
lemma sats_Implies_iff [simp]:


186 
"env \<in> list(A)


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


188 
apply (simp add: Implies_def, blast)


189 
done


190 


191 
lemma sats_Exists_iff [simp]:


192 
"env \<in> list(A)


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


194 
by (simp add: Exists_def)


195 


196 


197 


198 


199 
(*pretty but unnecessary


200 
constdefs sat :: "[i,i] => o"


201 
"sat(A,p) == satisfies(A,p)`[] = 1"


202 


203 
syntax "_sat" :: "[i,i] => o" (infixl "=" 50)


204 
translations "A = p" == "sat(A,p)"


205 


206 
lemma [simp]: "(A = Neg(p)) <> ~ (A = p)"


207 
by (simp add: sat_def)


208 


209 
lemma [simp]: "(A = And(p,q)) <> A=p & A=q"


210 
by (simp add: sat_def)


211 
*)


212 


213 


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


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


216 


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


218 
by (simp add: incr_var_def)


219 


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


221 
apply (simp add: incr_var_def)


222 
apply (blast dest: lt_trans1)


223 
done


224 


225 
consts incr_bv :: "i=>i"


226 
primrec


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


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


229 


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


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


232 


233 
"incr_bv(Neg(p)) =


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


235 


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


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


238 


239 
"incr_bv(Forall(p)) =


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


241 


242 


243 
constdefs incr_boundvars :: "i => i"


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


245 


246 


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


248 
by (simp add: incr_var_def)


249 


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


251 
by (induct_tac p, simp_all)


252 


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


254 
by (simp add: incr_boundvars_def)


255 


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


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


258 
be combined.*)


259 


260 
lemma sats_incr_bv_iff [rule_format]:


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


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


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


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


265 
apply (induct_tac p)


266 
apply (simp_all add: incr_var_def nth_append succ_lt_iff length_type)


267 
apply (auto simp add: diff_succ not_lt_iff_le)


268 
done


269 


270 
(*UNUSED*)


271 
lemma sats_incr_boundvars_iff:


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


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


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


275 
apply (simp add: incr_boundvars_def)


276 
done


277 


278 
(*UNUSED


279 
lemma formula_add_params [rule_format]:


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


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


282 
length(bvs) = n >


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


284 
apply (induct_tac n, simp, clarify)


285 
apply (erule list.cases)


286 
apply (auto simp add: sats_incr_boundvars_iff)


287 
done


288 
*)


289 


290 
consts arity :: "i=>i"


291 
primrec


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


293 


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


295 


296 
"arity(Neg(p)) = arity(p)"


297 


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


299 


300 
"arity(Forall(p)) = nat_case3(0, %x. x, arity(p))"


301 


302 


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


304 
by (induct_tac p, simp_all)


305 


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


307 
by (simp add: Or_def)


308 


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


310 
by (simp add: Implies_def)


311 


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


313 
by (simp add: Exists_def)


314 


315 


316 
lemma arity_sats_iff [rule_format]:


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


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


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


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


321 
apply (induct_tac p)


322 
apply (simp_all add: nth_append Un_least_lt_iff arity_type


323 
split: split_nat_case3, auto)


324 
done


325 


326 
lemma arity_sats1_iff:


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


328 
extra \<in> list(A) ]


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


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


331 
apply simp


332 
done


333 


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


335 
lemma incr_var_lemma:


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


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


338 
apply (simp add: incr_var_def Ord_Un_if, auto)


339 
apply (blast intro: leI)


340 
apply (simp add: not_lt_iff_le)


341 
apply (blast intro: le_anti_sym)


342 
apply (blast dest: lt_trans2)


343 
done


344 


345 
lemma incr_And_lemma:


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


347 
apply (simp add: Ord_Un_if lt_Ord lt_Ord2 succ_lt_iff)


348 
apply (blast dest: lt_asym)


349 
done


350 


351 
lemma arity_incr_bv_lemma [rule_format]:


352 
"p \<in> formula


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


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


355 
apply (induct_tac p)


356 
apply (simp_all add: imp_disj not_lt_iff_le Un_least_lt_iff lt_Un_iff le_Un_iff


357 
succ_Un_distrib [symmetric] incr_var_lt incr_var_le


358 
Un_commute incr_var_lemma arity_type


359 
split: split_nat_case3)


360 
(*left with the And case*)


361 
apply safe


362 
apply (blast intro: incr_And_lemma lt_trans1)


363 
apply (subst incr_And_lemma)


364 
apply (blast intro: lt_trans1)


365 
apply (simp add: Un_commute)


366 
done


367 


368 
lemma arity_incr_boundvars_eq:


369 
"p \<in> formula


370 
==> arity(incr_boundvars(p)) =


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


372 
apply (insert arity_incr_bv_lemma [of p 0])


373 
apply (simp add: incr_boundvars_def)


374 
done


375 


376 
lemma arity_iterates_incr_boundvars_eq:


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


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


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


380 
apply (induct_tac n)


381 
apply (simp_all add: arity_incr_boundvars_eq not_lt_iff_le)


382 
done


383 


384 


385 
(**** TRYING INCR_BV1 AGAIN ****)


386 


387 
constdefs incr_bv1 :: "i => i"


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


389 


390 


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


392 
by (simp add: incr_bv1_def)


393 


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


395 
lemma sats_incr_bv1_iff [rule_format]:


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


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


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


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


400 
apply (simp add: incr_bv1_def)


401 
done


402 


403 
lemma formula_add_params1 [rule_format]:


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


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


406 
length(bvs) = n >


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


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


409 
apply (induct_tac n, simp, clarify)


410 
apply (erule list.cases)


411 
apply (simp_all add: sats_incr_bv1_iff)


412 
done


413 


414 


415 
lemma arity_incr_bv1_eq:


416 
"p \<in> formula


417 
==> arity(incr_bv1(p)) =


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


419 
apply (insert arity_incr_bv_lemma [of p 1])


420 
apply (simp add: incr_bv1_def)


421 
done


422 


423 
lemma arity_iterates_incr_bv1_eq:


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


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


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


427 
apply (induct_tac n)


428 
apply (simp_all add: arity_incr_bv1_eq )


429 
apply (simp add: not_lt_iff_le)


430 
apply (blast intro: le_trans add_le_self2 arity_type)


431 
done


432 


433 


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


435 
constdefs DPow :: "i => i"


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


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


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


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


440 


441 
lemma DPowI:


442 
"[X <= A; env \<in> list(A); p \<in> formula;


443 
arity(p) \<le> succ(length(env))]


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


445 
by (simp add: DPow_def, blast)


446 


447 
lemma DPowD:


448 
"X \<in> DPow(A)


449 
==> X <= A &


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


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


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


453 
by (simp add: DPow_def)


454 


455 
lemmas DPow_imp_subset = DPowD [THEN conjunct1]


456 


457 
(*Lemma 1.2*)


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


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


460 
by (blast intro: DPowI)


461 


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


463 
by (simp add: DPow_def, blast)


464 


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


466 
apply (simp add: DPow_def)


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


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


469 
apply (auto simp add: Un_least_lt_iff)


470 
done


471 


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


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


474 
apply (rule bexI)


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


476 
apply auto


477 
done


478 


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


480 
apply (simp add: DPow_def, auto)


481 
apply (rename_tac envp p envq q)


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


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


484 
apply typecheck


485 
apply (rule conjI)


486 
(*finally check the arity!*)


487 
apply (simp add: arity_iterates_incr_bv1_eq length_app Un_least_lt_iff)


488 
apply (force intro: add_le_self le_trans)


489 
apply (simp add: arity_sats1_iff formula_add_params1, blast)


490 
done


491 


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


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


494 
apply (simp add: Int_in_DPow Compl_in_DPow)


495 
apply (simp add: DPow_def, blast)


496 
done


497 


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


499 
apply (simp add: DPow_def)


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


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


502 
apply typecheck


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


504 
done


505 


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


507 
apply (rule cons_eq [THEN subst])


508 
apply (blast intro: singleton_in_DPow Un_in_DPow)


509 
done


510 


511 
(*Part of Lemma 1.3*)


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


513 
apply (erule Fin.induct)


514 
apply (rule empty_in_DPow)


515 
apply (blast intro: cons_in_DPow)


516 
done


517 


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


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


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


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


522 
apply (simp add: DPow_def, auto)


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


524 
oops


525 


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


527 
by (blast intro: empty_in_DPow dest: DPow_imp_subset)


528 


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


530 
by (blast intro: Fin_into_DPow Finite_into_Fin Fin_subset)


531 


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


533 
apply (rule equalityI)


534 
apply (rule DPow_subset_Pow)


535 
apply (erule Finite_Pow_subset_Pow)


536 
done


537 


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


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


540 
apply (rule equalityI, safe)


541 
oops


542 
*)


543 


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


545 


546 
constdefs Lset :: "i=>i"


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


548 


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


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


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


552 


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


554 
by (subst Lset, blast)


555 


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


557 
apply (insert Lset [of x])


558 
apply (blast intro: elim: equalityE)


559 
done


560 


561 
subsubsection{* Transitivity *}


562 


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


564 
apply (simp add: Transset_def DPow_def)


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


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


567 
apply (auto simp add: Un_least_lt_iff)


568 
done


569 


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


571 
apply clarify


572 
apply (simp add: Transset_def)


573 
apply (blast intro: elem_subset_in_DPow)


574 
done


575 


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


577 
apply (simp add: Transset_def)


578 
apply (blast intro: elem_subset_in_DPow dest: DPowD)


579 
done


580 


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


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


583 
apply (rule_tac a=i in eps_induct)


584 
apply (subst Lset)


585 
apply (blast intro!: Transset_Union_family Transset_Un Transset_DPow)


586 
done


587 


588 
subsubsection{* Monotonicity *}


589 


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


591 
lemma Lset_mono [rule_format]:


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


593 
apply (rule_tac a=i in eps_induct)


594 
apply (rule impI [THEN allI])


595 
apply (subst Lset)


596 
apply (subst Lset, blast)


597 
done


598 


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


600 
lemma Lset_mono_mem [rule_format]:


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


602 
apply (rule_tac a=i in eps_induct)


603 
apply (rule impI [THEN allI])


604 
apply (subst Lset, auto)


605 
apply (rule rev_bexI, assumption)


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


607 
done


608 


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


610 


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


612 
by (subst Lset, blast)


613 


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


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


616 


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


618 
apply (subst Lset, rule UN_least)


619 
apply (erule succE)


620 
apply blast


621 
apply clarify


622 
apply (rule elem_subset_in_DPow)


623 
apply (subst Lset)


624 
apply blast


625 
apply (blast intro: dest: DPowD Lset_mono_mem)


626 
done


627 


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


629 
by (intro equalityI Lset_succ_subset1 Lset_succ_subset2)


630 


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


632 
apply (subst Lset)


633 
apply (rule equalityI)


634 
txt{*first inclusion*}


635 
apply (rule UN_least)


636 
apply (erule UnionE)


637 
apply (rule subset_trans)


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


639 
txt{*opposite inclusion*}


640 
apply (rule UN_least)


641 
apply (subst Lset, blast)


642 
done


643 


644 
subsubsection{* Lset applied to Limit ordinals *}


645 


646 
lemma Limit_Lset_eq:


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


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


649 


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


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


652 


653 
lemma Limit_LsetE:


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


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


656 
] ==> R"


657 
apply (rule classical)


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


659 
prefer 2 apply assumption


660 
apply blast


661 
apply (blast intro: ltI Limit_is_Ord)


662 
done


663 


664 
subsubsection{* Basic closure properties *}


665 


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


667 
by (subst Lset, blast intro: empty_in_DPow)


668 


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


670 
apply (rule_tac a=x in eps_induct)


671 
apply (subst Lset)


672 
apply (blast dest: DPowD)


673 
done


674 


675 


676 


677 
text{*Kunen's VI, 1.9 (b)*}


678 


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


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


681 


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


683 
by (simp add: subset_fm_def)


684 


685 
lemma arity_subset_fm [simp]:


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


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


688 


689 
lemma sats_subset_fm [simp]:


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


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


692 
apply (frule lt_nat_in_nat, erule length_type)


693 
apply (simp add: subset_fm_def Transset_def)


694 
apply (blast intro: nth_type )


695 
done


696 


697 
constdefs transset_fm :: "i=>i"


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


699 


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


701 
by (simp add: transset_fm_def)


702 


703 
lemma arity_transset_fm [simp]:


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


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


706 


707 
lemma sats_transset_fm [simp]:


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


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


710 
apply (frule lt_nat_in_nat, erule length_type)


711 
apply (simp add: transset_fm_def Transset_def)


712 
apply (blast intro: nth_type )


713 
done


714 


715 
constdefs ordinal_fm :: "i=>i"


716 
"ordinal_fm(x) ==


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


718 


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


720 
by (simp add: ordinal_fm_def)


721 


722 
lemma arity_ordinal_fm [simp]:


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


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


725 


726 
lemma sats_ordinal_fm [simp]:


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


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


729 
apply (frule lt_nat_in_nat, erule length_type)


730 
apply (simp add: ordinal_fm_def Ord_def Transset_def)


731 
apply (blast intro: nth_type )


732 
done


733 


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


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


736 
apply (simp add: DPow_def Collect_subset)


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


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


739 
apply (simp_all add: sats_ordinal_fm)


740 
done


741 


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


743 
apply (erule trans_induct3)


744 
apply (simp_all add: Lset_succ Limit_Lset_eq Limit_Union_eq)


745 
txt{*The successor case remains.*}


746 
apply (rule equalityI)


747 
txt{*First inclusion*}


748 
apply clarify


749 
apply (erule Ord_linear_lt, assumption)


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


751 
apply blast


752 
apply (blast dest: ltD)


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


754 
apply auto


755 
txt{*Key case: *}


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


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


758 
apply (blast intro: Ord_in_Ord)


759 
done


760 


761 


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


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


764 


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


766 
apply (simp add: Lset_succ)


767 
apply (subst Ords_of_Lset_eq [symmetric], assumption,


768 
rule Ords_in_DPow [OF Transset_Lset])


769 
done


770 


771 
subsubsection{* Unions *}


772 


773 
lemma Union_in_Lset:


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


775 
apply (insert Transset_Lset)


776 
apply (rule LsetI [OF succI1])


777 
apply (simp add: Transset_def DPow_def)


778 
apply (intro conjI, blast)


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


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


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


782 
apply typecheck


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


784 
done


785 


786 
lemma Union_in_LLimit:


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


788 
apply (rule Limit_LsetE, assumption+)


789 
apply (blast intro: Limit_has_succ lt_LsetI Union_in_Lset)


790 
done


791 


792 
subsubsection{* Finite sets and ordered pairs *}


793 


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


795 
by (simp add: Lset_succ singleton_in_DPow)


796 


797 
lemma doubleton_in_Lset:


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


799 
by (simp add: Lset_succ empty_in_DPow cons_in_DPow)


800 


801 
lemma Pair_in_Lset:


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


803 
apply (unfold Pair_def)


804 
apply (blast intro: doubleton_in_Lset)


805 
done


806 


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


808 


809 
lemma singleton_in_LLimit:


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


811 
apply (erule Limit_LsetE, assumption)


812 
apply (erule singleton_in_Lset [THEN lt_LsetI])


813 
apply (blast intro: Limit_has_succ)


814 
done


815 


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


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


818 


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


820 
lemma doubleton_in_LLimit:


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


822 
apply (erule Limit_LsetE, assumption)


823 
apply (erule Limit_LsetE, assumption)


824 
apply (blast intro: lt_LsetI [OF doubleton_in_Lset]


825 
Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt)


826 
done


827 


828 
lemma Pair_in_LLimit:


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


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


831 
apply (erule Limit_LsetE, assumption)


832 
apply (erule Limit_LsetE, assumption)


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


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


835 
Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt)


836 
done


837 


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


839 
by (blast intro: Pair_in_LLimit)


840 


841 
lemmas Sigma_subset_LLimit = subset_trans [OF Sigma_mono product_LLimit]


842 


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


844 
by (blast dest: Ord_subset_Lset nat_le_Limit le_imp_subset Limit_is_Ord)


845 


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


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


848 


849 


850 
subsubsection{* Closure under disjoint union *}


851 


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


853 


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


855 
by (blast intro: nat_into_LLimit)


856 


857 
lemma Inl_in_LLimit:


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


859 
apply (unfold Inl_def)


860 
apply (blast intro: zero_in_LLimit Pair_in_LLimit)


861 
done


862 


863 
lemma Inr_in_LLimit:


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


865 
apply (unfold Inr_def)


866 
apply (blast intro: one_in_LLimit Pair_in_LLimit)


867 
done


868 


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


870 
by (blast intro!: Inl_in_LLimit Inr_in_LLimit)


871 


872 
lemmas sum_subset_LLimit = subset_trans [OF sum_mono sum_LLimit]


873 


874 


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


876 
constdefs


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


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


879 


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


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


882 


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


884 
by (simp add: L_def, blast)


885 


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


887 
by (simp add: L_def)


888 


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


890 
by (simp add: lrank_def)


891 


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


893 
apply (erule trans_induct3)


894 
apply simp


895 
apply (simp only: lrank_def)


896 
apply (blast intro: Least_le)


897 
apply (simp_all add: Limit_Lset_eq)


898 
apply (blast intro: ltI Limit_is_Ord lt_trans)


899 
done


900 


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


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


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


904 
apply (simp add: L_def, auto)


905 
apply (blast intro: Lset_lrank_lt)


906 
apply (unfold lrank_def)


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


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


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


910 
done


911 


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


913 
by (simp add: Lset_iff_lrank_lt)


914 


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


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


917 
apply (unfold lrank_def)


918 
apply (rule Least_equality)


919 
apply (erule Ord_in_Lset)


920 
apply assumption


921 
apply (insert notin_Lset [of i])


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


923 
done


924 


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


926 
declare Ord_lrank [THEN lrank_of_Ord, simp]


927 


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


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


930 
apply (simp add: Lset_succ DPow_def)


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


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


933 
apply auto


934 
done


935 


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


937 
apply (unfold lrank_def)


938 
apply (rule Least_equality)


939 
apply (rule Lset_in_Lset_succ)


940 
apply assumption


941 
apply clarify


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


943 
apply (blast dest: mem_irrefl)


944 
apply (blast intro!: le_imp_subset Lset_mono)


945 
done


946 


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


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


949 
apply (erule trans_induct)


950 
apply (subst Lset)


951 
apply (subst Vset)


952 
apply (rule UN_mono [OF subset_refl])


953 
apply (rule subset_trans [OF DPow_subset_Pow])


954 
apply (rule Pow_mono, blast)


955 
done


956 


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


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


959 
apply (erule nat_induct)


960 
apply (simp add: Vfrom_0)


961 
apply (simp add: Lset_succ Vset_succ Finite_Vset Finite_DPow_eq_Pow)


962 
done


963 


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


965 


966 
lemma Union_in_L: "L(X) ==> L(Union(X))"


967 
apply (simp add: L_def, clarify)


968 
apply (drule Ord_imp_greater_Limit)


969 
apply (blast intro: lt_LsetI Union_in_LLimit Limit_is_Ord)


970 
done


971 


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


973 
apply (simp add: L_def, clarify)


974 
apply (drule Ord2_imp_greater_Limit, assumption)


975 
apply (blast intro: lt_LsetI doubleton_in_LLimit Limit_is_Ord)


976 
done


977 


978 
subsubsection{*For L to satisfy Powerset *}


979 


980 
lemma LPow_env_typing:


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


982 
by (auto intro: L_I iff: Lset_succ_lrank_iff)


983 


984 
lemma LPow_in_Lset:


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


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


987 
apply simp


988 
apply (rule LsetI [OF succI1])


989 
apply (simp add: DPow_def)


990 
apply (intro conjI, clarify)


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


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


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


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


995 
apply typecheck


996 
apply (rule conjI)


997 
apply (simp add: succ_Un_distrib [symmetric])


998 
apply (rule equality_iffI)


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


1000 
apply (auto intro: L_I iff: Lset_succ_lrank_iff)


1001 
done


1002 


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


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


1005 


1006 
end
