author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46953  2b6e55924af3 
child 58860  fee7cfa69c50 
permissions  rwrr 
13505  1 
(* Title: ZF/Constructible/Formula.thy 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

3 
*) 

4 

13223  5 
header {* FirstOrder Formulas and the Definition of the Class L *} 
6 

16417  7 
theory Formula imports Main begin 
13223  8 

13291  9 
subsection{*Internalized formulas of FOL*} 
10 

11 
text{*De Bruijn representation. 

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

13223  13 

14 
consts formula :: i 

15 
datatype 

46953  16 
"formula" = Member ("x \<in> nat", "y \<in> nat") 
17 
 Equal ("x \<in> nat", "y \<in> nat") 

18 
 Nand ("p \<in> formula", "q \<in> formula") 

19 
 Forall ("p \<in> formula") 

13223  20 

21 
declare formula.intros [TC] 

22 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

23 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

24 
Neg :: "i=>i" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

25 
"Neg(p) == Nand(p,p)" 
13398
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset

26 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

27 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

28 
And :: "[i,i]=>i" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

29 
"And(p,q) == Neg(Nand(p,q))" 
13398
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset

30 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

31 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

32 
Or :: "[i,i]=>i" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

33 
"Or(p,q) == Nand(Neg(p),Neg(q))" 
13223  34 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

35 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

36 
Implies :: "[i,i]=>i" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

37 
"Implies(p,q) == Nand(p,Neg(q))" 
13223  38 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

39 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

40 
Iff :: "[i,i]=>i" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

41 
"Iff(p,q) == And(Implies(p,q), Implies(q,p))" 
13291  42 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

43 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

44 
Exists :: "i=>i" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

45 
"Exists(p) == Neg(Forall(Neg(p)))"; 
13223  46 

13398
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset

47 
lemma Neg_type [TC]: "p \<in> formula ==> Neg(p) \<in> formula" 
46823  48 
by (simp add: Neg_def) 
13398
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset

49 

1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset

50 
lemma And_type [TC]: "[ p \<in> formula; q \<in> formula ] ==> And(p,q) \<in> formula" 
46823  51 
by (simp add: And_def) 
13398
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset

52 

13223  53 
lemma Or_type [TC]: "[ p \<in> formula; q \<in> formula ] ==> Or(p,q) \<in> formula" 
46823  54 
by (simp add: Or_def) 
13223  55 

56 
lemma Implies_type [TC]: 

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

46823  58 
by (simp add: Implies_def) 
13223  59 

13291  60 
lemma Iff_type [TC]: 
61 
"[ p \<in> formula; q \<in> formula ] ==> Iff(p,q) \<in> formula" 

46823  62 
by (simp add: Iff_def) 
13291  63 

13223  64 
lemma Exists_type [TC]: "p \<in> formula ==> Exists(p) \<in> formula" 
46823  65 
by (simp add: Exists_def) 
13223  66 

67 

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

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

46823  70 
"satisfies(A,Member(x,y)) = 
13223  71 
(\<lambda>env \<in> list(A). bool_of_o (nth(x,env) \<in> nth(y,env)))" 
72 

46823  73 
"satisfies(A,Equal(x,y)) = 
13223  74 
(\<lambda>env \<in> list(A). bool_of_o (nth(x,env) = nth(y,env)))" 
75 

13398
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset

76 
"satisfies(A,Nand(p,q)) = 
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset

77 
(\<lambda>env \<in> list(A). not ((satisfies(A,p)`env) and (satisfies(A,q)`env)))" 
13223  78 

46823  79 
"satisfies(A,Forall(p)) = 
13223  80 
(\<lambda>env \<in> list(A). bool_of_o (\<forall>x\<in>A. satisfies(A,p) ` (Cons(x,env)) = 1))" 
81 

82 

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

21233  84 
by (induct set: formula) simp_all 
13223  85 

21233  86 
abbreviation 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

87 
sats :: "[i,i,i] => o" where 
21233  88 
"sats(A,p,env) == satisfies(A,p)`env = 1" 
13223  89 

90 
lemma [simp]: 

46823  91 
"env \<in> list(A) 
92 
==> sats(A, Member(x,y), env) \<longleftrightarrow> nth(x,env) \<in> nth(y,env)" 

13223  93 
by simp 
94 

95 
lemma [simp]: 

46823  96 
"env \<in> list(A) 
97 
==> sats(A, Equal(x,y), env) \<longleftrightarrow> nth(x,env) = nth(y,env)" 

13223  98 
by simp 
99 

13398
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset

100 
lemma sats_Nand_iff [simp]: 
46823  101 
"env \<in> list(A) 
102 
==> (sats(A, Nand(p,q), env)) \<longleftrightarrow> ~ (sats(A,p,env) & sats(A,q,env))" 

103 
by (simp add: Bool.and_def Bool.not_def cond_def) 

13223  104 

105 
lemma sats_Forall_iff [simp]: 

46823  106 
"env \<in> list(A) 
107 
==> sats(A, Forall(p), env) \<longleftrightarrow> (\<forall>x\<in>A. sats(A, p, Cons(x,env)))" 

13223  108 
by simp 
109 

46823  110 
declare satisfies.simps [simp del]; 
13223  111 

13298  112 
subsection{*Dividing line between primitive and derived connectives*} 
13223  113 

13398
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset

114 
lemma sats_Neg_iff [simp]: 
46823  115 
"env \<in> list(A) 
116 
==> sats(A, Neg(p), env) \<longleftrightarrow> ~ sats(A,p,env)" 

117 
by (simp add: Neg_def) 

13398
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset

118 

1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset

119 
lemma sats_And_iff [simp]: 
46823  120 
"env \<in> list(A) 
121 
==> (sats(A, And(p,q), env)) \<longleftrightarrow> sats(A,p,env) & sats(A,q,env)" 

122 
by (simp add: And_def) 

13398
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset

123 

13223  124 
lemma sats_Or_iff [simp]: 
46823  125 
"env \<in> list(A) 
126 
==> (sats(A, Or(p,q), env)) \<longleftrightarrow> sats(A,p,env)  sats(A,q,env)" 

13223  127 
by (simp add: Or_def) 
128 

129 
lemma sats_Implies_iff [simp]: 

46823  130 
"env \<in> list(A) 
131 
==> (sats(A, Implies(p,q), env)) \<longleftrightarrow> (sats(A,p,env) \<longrightarrow> sats(A,q,env))" 

132 
by (simp add: Implies_def, blast) 

13291  133 

134 
lemma sats_Iff_iff [simp]: 

46823  135 
"env \<in> list(A) 
136 
==> (sats(A, Iff(p,q), env)) \<longleftrightarrow> (sats(A,p,env) \<longleftrightarrow> sats(A,q,env))" 

137 
by (simp add: Iff_def, blast) 

13223  138 

139 
lemma sats_Exists_iff [simp]: 

46823  140 
"env \<in> list(A) 
141 
==> sats(A, Exists(p), env) \<longleftrightarrow> (\<exists>x\<in>A. sats(A, p, Cons(x,env)))" 

13223  142 
by (simp add: Exists_def) 
143 

144 

13291  145 
subsubsection{*Derived rules to help build up formulas*} 
146 

147 
lemma mem_iff_sats: 

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

46823  149 
==> (x\<in>y) \<longleftrightarrow> sats(A, Member(i,j), env)" 
13291  150 
by (simp add: satisfies.simps) 
151 

13298  152 
lemma equal_iff_sats: 
153 
"[ nth(i,env) = x; nth(j,env) = y; env \<in> list(A)] 

46823  154 
==> (x=y) \<longleftrightarrow> sats(A, Equal(i,j), env)" 
13298  155 
by (simp add: satisfies.simps) 
156 

13316  157 
lemma not_iff_sats: 
46823  158 
"[ P \<longleftrightarrow> sats(A,p,env); env \<in> list(A)] 
159 
==> (~P) \<longleftrightarrow> sats(A, Neg(p), env)" 

13316  160 
by simp 
161 

13291  162 
lemma conj_iff_sats: 
46823  163 
"[ P \<longleftrightarrow> sats(A,p,env); Q \<longleftrightarrow> sats(A,q,env); env \<in> list(A)] 
164 
==> (P & Q) \<longleftrightarrow> sats(A, And(p,q), env)" 

13291  165 
by (simp add: sats_And_iff) 
166 

167 
lemma disj_iff_sats: 

46823  168 
"[ P \<longleftrightarrow> sats(A,p,env); Q \<longleftrightarrow> sats(A,q,env); env \<in> list(A)] 
169 
==> (P  Q) \<longleftrightarrow> sats(A, Or(p,q), env)" 

13291  170 
by (simp add: sats_Or_iff) 
171 

172 
lemma iff_iff_sats: 

46823  173 
"[ P \<longleftrightarrow> sats(A,p,env); Q \<longleftrightarrow> sats(A,q,env); env \<in> list(A)] 
174 
==> (P \<longleftrightarrow> Q) \<longleftrightarrow> sats(A, Iff(p,q), env)" 

175 
by (simp add: sats_Forall_iff) 

13291  176 

177 
lemma imp_iff_sats: 

46823  178 
"[ P \<longleftrightarrow> sats(A,p,env); Q \<longleftrightarrow> sats(A,q,env); env \<in> list(A)] 
179 
==> (P \<longrightarrow> Q) \<longleftrightarrow> sats(A, Implies(p,q), env)" 

180 
by (simp add: sats_Forall_iff) 

13291  181 

182 
lemma ball_iff_sats: 

46823  183 
"[ !!x. x\<in>A ==> P(x) \<longleftrightarrow> sats(A, p, Cons(x, env)); env \<in> list(A)] 
184 
==> (\<forall>x\<in>A. P(x)) \<longleftrightarrow> sats(A, Forall(p), env)" 

185 
by (simp add: sats_Forall_iff) 

13291  186 

187 
lemma bex_iff_sats: 

46823  188 
"[ !!x. x\<in>A ==> P(x) \<longleftrightarrow> sats(A, p, Cons(x, env)); env \<in> list(A)] 
189 
==> (\<exists>x\<in>A. P(x)) \<longleftrightarrow> sats(A, Exists(p), env)" 

190 
by (simp add: sats_Exists_iff) 

13291  191 

46823  192 
lemmas FOL_iff_sats = 
13316  193 
mem_iff_sats equal_iff_sats not_iff_sats conj_iff_sats 
194 
disj_iff_sats imp_iff_sats iff_iff_sats imp_iff_sats ball_iff_sats 

195 
bex_iff_sats 

13223  196 

13647  197 

198 
subsection{*Arity of a Formula: Maximum Free de Bruijn Index*} 

199 

200 
consts arity :: "i=>i" 

201 
primrec 

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

203 

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

205 

206 
"arity(Nand(p,q)) = arity(p) \<union> arity(q)" 

207 

208 
"arity(Forall(p)) = Arith.pred(arity(p))" 

209 

210 

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

46823  212 
by (induct_tac p, simp_all) 
13647  213 

214 
lemma arity_Neg [simp]: "arity(Neg(p)) = arity(p)" 

46823  215 
by (simp add: Neg_def) 
13647  216 

217 
lemma arity_And [simp]: "arity(And(p,q)) = arity(p) \<union> arity(q)" 

46823  218 
by (simp add: And_def) 
13647  219 

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

46823  221 
by (simp add: Or_def) 
13647  222 

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

46823  224 
by (simp add: Implies_def) 
13647  225 

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

227 
by (simp add: Iff_def, blast) 

228 

229 
lemma arity_Exists [simp]: "arity(Exists(p)) = Arith.pred(arity(p))" 

46823  230 
by (simp add: Exists_def) 
13647  231 

232 

233 
lemma arity_sats_iff [rule_format]: 

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

46823  235 
==> \<forall>env \<in> list(A). 
236 
arity(p) \<le> length(env) \<longrightarrow> 

237 
sats(A, p, env @ extra) \<longleftrightarrow> sats(A, p, env)" 

13647  238 
apply (induct_tac p) 
239 
apply (simp_all add: Arith.pred_def nth_append Un_least_lt_iff nat_imp_quasinat 

46823  240 
split: split_nat_case, auto) 
13647  241 
done 
242 

243 
lemma arity_sats1_iff: 

46823  244 
"[ arity(p) \<le> succ(length(env)); p \<in> formula; x \<in> A; env \<in> list(A); 
13647  245 
extra \<in> list(A) ] 
46823  246 
==> sats(A, p, Cons(x, env @ extra)) \<longleftrightarrow> sats(A, p, Cons(x, env))" 
13647  247 
apply (insert arity_sats_iff [of p extra A "Cons(x,env)"]) 
46823  248 
apply simp 
13647  249 
done 
250 

251 

252 
subsection{*Renaming Some de Bruijn Variables*} 

253 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

254 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

255 
incr_var :: "[i,i]=>i" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

256 
"incr_var(x,nq) == if x<nq then x else succ(x)" 
13223  257 

13687  258 
lemma incr_var_lt: "x<nq ==> incr_var(x,nq) = x" 
13223  259 
by (simp add: incr_var_def) 
260 

13687  261 
lemma incr_var_le: "nq\<le>x ==> incr_var(x,nq) = succ(x)" 
46823  262 
apply (simp add: incr_var_def) 
263 
apply (blast dest: lt_trans1) 

13223  264 
done 
265 

266 
consts incr_bv :: "i=>i" 

267 
primrec 

46823  268 
"incr_bv(Member(x,y)) = 
13687  269 
(\<lambda>nq \<in> nat. Member (incr_var(x,nq), incr_var(y,nq)))" 
13223  270 

46823  271 
"incr_bv(Equal(x,y)) = 
13687  272 
(\<lambda>nq \<in> nat. Equal (incr_var(x,nq), incr_var(y,nq)))" 
13223  273 

13398
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset

274 
"incr_bv(Nand(p,q)) = 
13687  275 
(\<lambda>nq \<in> nat. Nand (incr_bv(p)`nq, incr_bv(q)`nq))" 
13223  276 

46823  277 
"incr_bv(Forall(p)) = 
13687  278 
(\<lambda>nq \<in> nat. Forall (incr_bv(p) ` succ(nq)))" 
13223  279 

280 

13687  281 
lemma [TC]: "x \<in> nat ==> incr_var(x,nq) \<in> nat" 
46823  282 
by (simp add: incr_var_def) 
13223  283 

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

46823  285 
by (induct_tac p, simp_all) 
13223  286 

13647  287 
text{*Obviously, @{term DPow} is closed under complements and finite 
288 
intersections and unions. Needs an inductive lemma to allow two lists of 

289 
parameters to be combined.*} 

13223  290 

291 
lemma sats_incr_bv_iff [rule_format]: 

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

46823  293 
==> \<forall>bvs \<in> list(A). 
294 
sats(A, incr_bv(p) ` length(bvs), bvs @ Cons(x,env)) \<longleftrightarrow> 

13223  295 
sats(A, p, bvs@env)" 
296 
apply (induct_tac p) 

297 
apply (simp_all add: incr_var_def nth_append succ_lt_iff length_type) 

298 
apply (auto simp add: diff_succ not_lt_iff_le) 

299 
done 

300 

301 

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

303 
lemma incr_var_lemma: 

13687  304 
"[ x \<in> nat; y \<in> nat; nq \<le> x ] 
305 
==> succ(x) \<union> incr_var(y,nq) = succ(x \<union> y)" 

13223  306 
apply (simp add: incr_var_def Ord_Un_if, auto) 
307 
apply (blast intro: leI) 

46823  308 
apply (simp add: not_lt_iff_le) 
309 
apply (blast intro: le_anti_sym) 

310 
apply (blast dest: lt_trans2) 

13223  311 
done 
312 

313 
lemma incr_And_lemma: 

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

46823  315 
apply (simp add: Ord_Un_if lt_Ord lt_Ord2 succ_lt_iff) 
316 
apply (blast dest: lt_asym) 

13223  317 
done 
318 

319 
lemma arity_incr_bv_lemma [rule_format]: 

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

13223  322 
(if n < arity(p) then succ(arity(p)) else arity(p))" 
46823  323 
apply (induct_tac p) 
13223  324 
apply (simp_all add: imp_disj not_lt_iff_le Un_least_lt_iff lt_Un_iff le_Un_iff 
325 
succ_Un_distrib [symmetric] incr_var_lt incr_var_le 

13647  326 
Un_commute incr_var_lemma Arith.pred_def nat_imp_quasinat 
46823  327 
split: split_nat_case) 
13269  328 
txt{*the Forall case reduces to linear arithmetic*} 
329 
prefer 2 

46823  330 
apply clarify 
331 
apply (blast dest: lt_trans1) 

13269  332 
txt{*left with the And case*} 
13223  333 
apply safe 
46823  334 
apply (blast intro: incr_And_lemma lt_trans1) 
13223  335 
apply (subst incr_And_lemma) 
46823  336 
apply (blast intro: lt_trans1) 
13269  337 
apply (simp add: Un_commute) 
13223  338 
done 
339 

340 

13647  341 
subsection{*Renaming all but the First de Bruijn Variable*} 
13223  342 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

343 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

344 
incr_bv1 :: "i => i" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

345 
"incr_bv1(p) == incr_bv(p)`1" 
13223  346 

347 

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

46823  349 
by (simp add: incr_bv1_def) 
13223  350 

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

13647  352 
lemma sats_incr_bv1_iff: 
13223  353 
"[ p \<in> formula; env \<in> list(A); x \<in> A; y \<in> A ] 
46823  354 
==> sats(A, incr_bv1(p), Cons(x, Cons(y, env))) \<longleftrightarrow> 
13223  355 
sats(A, p, Cons(x,env))" 
356 
apply (insert sats_incr_bv_iff [of p env A y "Cons(x,Nil)"]) 

46823  357 
apply (simp add: incr_bv1_def) 
13223  358 
done 
359 

360 
lemma formula_add_params1 [rule_format]: 

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

46823  362 
==> \<forall>bvs \<in> list(A). \<forall>env \<in> list(A). 
363 
length(bvs) = n \<longrightarrow> 

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

13223  365 
sats(A, p, Cons(x,env))" 
46823  366 
apply (induct_tac n, simp, clarify) 
13223  367 
apply (erule list.cases) 
46823  368 
apply (simp_all add: sats_incr_bv1_iff) 
13223  369 
done 
370 

371 

372 
lemma arity_incr_bv1_eq: 

373 
"p \<in> formula 

374 
==> arity(incr_bv1(p)) = 

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

376 
apply (insert arity_incr_bv_lemma [of p 1]) 

46823  377 
apply (simp add: incr_bv1_def) 
13223  378 
done 
379 

380 
lemma arity_iterates_incr_bv1_eq: 

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

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

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

46823  384 
apply (induct_tac n) 
13298  385 
apply (simp_all add: arity_incr_bv1_eq) 
13223  386 
apply (simp add: not_lt_iff_le) 
46823  387 
apply (blast intro: le_trans add_le_self2 arity_type) 
13223  388 
done 
389 

390 

13647  391 

392 
subsection{*Definable Powerset*} 

393 

394 
text{*The definable powerset operation: Kunen's definition VI 1.1, page 165.*} 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

395 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

396 
DPow :: "i => i" where 
46823  397 
"DPow(A) == {X \<in> Pow(A). 
398 
\<exists>env \<in> list(A). \<exists>p \<in> formula. 

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

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

402 
lemma DPowI: 

13291  403 
"[env \<in> list(A); p \<in> formula; arity(p) \<le> succ(length(env))] 
13223  404 
==> {x\<in>A. sats(A, p, Cons(x,env))} \<in> DPow(A)" 
46823  405 
by (simp add: DPow_def, blast) 
13223  406 

13291  407 
text{*With this rule we can specify @{term p} later.*} 
408 
lemma DPowI2 [rule_format]: 

46823  409 
"[\<forall>x\<in>A. P(x) \<longleftrightarrow> sats(A, p, Cons(x,env)); 
13291  410 
env \<in> list(A); p \<in> formula; arity(p) \<le> succ(length(env))] 
411 
==> {x\<in>A. P(x)} \<in> DPow(A)" 

46823  412 
by (simp add: DPow_def, blast) 
13291  413 

13223  414 
lemma DPowD: 
46823  415 
"X \<in> DPow(A) 
416 
==> X \<subseteq> A & 

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

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

13223  419 
X = {x\<in>A. sats(A, p, Cons(x,env))})" 
46823  420 
by (simp add: DPow_def) 
13223  421 

422 
lemmas DPow_imp_subset = DPowD [THEN conjunct1] 

423 

13647  424 
(*Kunen's Lemma VI 1.2*) 
46823  425 
lemma "[ p \<in> formula; env \<in> list(A); arity(p) \<le> succ(length(env)) ] 
13223  426 
==> {x\<in>A. sats(A, p, Cons(x,env))} \<in> DPow(A)" 
427 
by (blast intro: DPowI) 

428 

46823  429 
lemma DPow_subset_Pow: "DPow(A) \<subseteq> Pow(A)" 
13223  430 
by (simp add: DPow_def, blast) 
431 

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

433 
apply (simp add: DPow_def) 

46823  434 
apply (rule_tac x=Nil in bexI) 
435 
apply (rule_tac x="Neg(Equal(0,0))" in bexI) 

436 
apply (auto simp add: Un_least_lt_iff) 

13223  437 
done 
438 

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

46823  440 
apply (simp add: DPow_def, clarify, auto) 
441 
apply (rule bexI) 

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

443 
apply auto 

13223  444 
done 
445 

46823  446 
lemma Int_in_DPow: "[ X \<in> DPow(A); Y \<in> DPow(A) ] ==> X \<inter> Y \<in> DPow(A)" 
447 
apply (simp add: DPow_def, auto) 

448 
apply (rename_tac envp p envq q) 

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

13223  450 
apply (rule_tac x="And(p, iterates(incr_bv1,length(envp),q))" in bexI) 
451 
apply typecheck 

46823  452 
apply (rule conjI) 
13223  453 
(*finally check the arity!*) 
454 
apply (simp add: arity_iterates_incr_bv1_eq length_app Un_least_lt_iff) 

46823  455 
apply (force intro: add_le_self le_trans) 
456 
apply (simp add: arity_sats1_iff formula_add_params1, blast) 

13223  457 
done 
458 

46823  459 
lemma Un_in_DPow: "[ X \<in> DPow(A); Y \<in> DPow(A) ] ==> X \<union> Y \<in> DPow(A)" 
460 
apply (subgoal_tac "X \<union> Y = A  ((AX) \<inter> (AY))") 

461 
apply (simp add: Int_in_DPow Compl_in_DPow) 

462 
apply (simp add: DPow_def, blast) 

13223  463 
done 
464 

13651
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

465 
lemma singleton_in_DPow: "a \<in> A ==> {a} \<in> DPow(A)" 
13223  466 
apply (simp add: DPow_def) 
46823  467 
apply (rule_tac x="Cons(a,Nil)" in bexI) 
468 
apply (rule_tac x="Equal(0,1)" in bexI) 

13223  469 
apply typecheck 
46823  470 
apply (force simp add: succ_Un_distrib [symmetric]) 
13223  471 
done 
472 

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

46823  474 
apply (rule cons_eq [THEN subst]) 
475 
apply (blast intro: singleton_in_DPow Un_in_DPow) 

13223  476 
done 
477 

478 
(*Part of Lemma 1.3*) 

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

46823  480 
apply (erule Fin.induct) 
481 
apply (rule empty_in_DPow) 

482 
apply (blast intro: cons_in_DPow) 

13223  483 
done 
484 

13651
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

485 
text{*@{term DPow} is not monotonic. For example, let @{term A} be some 
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

486 
nonconstructible set of natural numbers, and let @{term B} be @{term nat}. 
46823  487 
Then @{term "A<=B"} and obviously @{term "A \<in> DPow(A)"} but @{term "A \<notin> 
13651
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

488 
DPow(B)"}.*} 
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

489 

46823  490 
(*This may be true but the proof looks difficult, requiring relativization 
46953  491 
lemma DPow_insert: "DPow (cons(a,A)) = DPow(A) \<union> {cons(a,X) . X \<in> DPow(A)}" 
13651
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

492 
apply (rule equalityI, safe) 
13223  493 
oops 
13651
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

494 
*) 
13223  495 

46823  496 
lemma Finite_Pow_subset_Pow: "Finite(A) ==> Pow(A) \<subseteq> DPow(A)" 
13223  497 
by (blast intro: Fin_into_DPow Finite_into_Fin Fin_subset) 
498 

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

46823  500 
apply (rule equalityI) 
501 
apply (rule DPow_subset_Pow) 

502 
apply (erule Finite_Pow_subset_Pow) 

13223  503 
done 
504 

13651
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

505 

ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

506 
subsection{*Internalized Formulas for the Ordinals*} 
13223  507 

13651
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

508 
text{*The @{text sats} theorems below differ from the usual form in that they 
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

509 
include an element of absoluteness. That is, they relate internalized 
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

510 
formulas to real concepts such as the subset relation, rather than to the 
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

511 
relativized concepts defined in theory @{text Relative}. This lets us prove 
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

512 
the theorem as @{text Ords_in_DPow} without first having to instantiate the 
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

513 
locale @{text M_trivial}. Note that the present theory does not even take 
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

514 
@{text Relative} as a parent.*} 
13298  515 

516 
subsubsection{*The subset relation*} 

517 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

518 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

519 
subset_fm :: "[i,i]=>i" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

520 
"subset_fm(x,y) == Forall(Implies(Member(0,succ(x)), Member(0,succ(y))))" 
13298  521 

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

46823  523 
by (simp add: subset_fm_def) 
13298  524 

525 
lemma arity_subset_fm [simp]: 

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

46823  527 
by (simp add: subset_fm_def succ_Un_distrib [symmetric]) 
13298  528 

529 
lemma sats_subset_fm [simp]: 

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

46823  531 
==> sats(A, subset_fm(x,y), env) \<longleftrightarrow> nth(x,env) \<subseteq> nth(y,env)" 
532 
apply (frule lt_length_in_nat, assumption) 

533 
apply (simp add: subset_fm_def Transset_def) 

534 
apply (blast intro: nth_type) 

13298  535 
done 
536 

537 
subsubsection{*Transitive sets*} 

538 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

539 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

540 
transset_fm :: "i=>i" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

541 
"transset_fm(x) == Forall(Implies(Member(0,succ(x)), subset_fm(0,succ(x))))" 
13298  542 

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

46823  544 
by (simp add: transset_fm_def) 
13298  545 

546 
lemma arity_transset_fm [simp]: 

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

46823  548 
by (simp add: transset_fm_def succ_Un_distrib [symmetric]) 
13298  549 

550 
lemma sats_transset_fm [simp]: 

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

46823  552 
==> sats(A, transset_fm(x), env) \<longleftrightarrow> Transset(nth(x,env))" 
553 
apply (frule lt_nat_in_nat, erule length_type) 

554 
apply (simp add: transset_fm_def Transset_def) 

555 
apply (blast intro: nth_type) 

13298  556 
done 
557 

558 
subsubsection{*Ordinals*} 

559 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

560 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

561 
ordinal_fm :: "i=>i" where 
46823  562 
"ordinal_fm(x) == 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

563 
And(transset_fm(x), Forall(Implies(Member(0,succ(x)), transset_fm(0))))" 
13298  564 

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

46823  566 
by (simp add: ordinal_fm_def) 
13298  567 

568 
lemma arity_ordinal_fm [simp]: 

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

46823  570 
by (simp add: ordinal_fm_def succ_Un_distrib [symmetric]) 
13298  571 

13306  572 
lemma sats_ordinal_fm: 
13298  573 
"[x < length(env); env \<in> list(A); Transset(A)] 
46823  574 
==> sats(A, ordinal_fm(x), env) \<longleftrightarrow> Ord(nth(x,env))" 
575 
apply (frule lt_nat_in_nat, erule length_type) 

13298  576 
apply (simp add: ordinal_fm_def Ord_def Transset_def) 
46823  577 
apply (blast intro: nth_type) 
13298  578 
done 
579 

13651
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

580 
text{*The subset consisting of the ordinals is definable. Essential lemma for 
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

581 
@{text Ord_in_Lset}. This result is the objective of the present subsection.*} 
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

582 
theorem Ords_in_DPow: "Transset(A) ==> {x \<in> A. Ord(x)} \<in> DPow(A)" 
46823  583 
apply (simp add: DPow_def Collect_subset) 
584 
apply (rule_tac x=Nil in bexI) 

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

13651
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

586 
apply (simp_all add: sats_ordinal_fm) 
46823  587 
done 
13651
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

588 

13298  589 

13223  590 
subsection{* Constant Lset: Levels of the Constructible Universe *} 
591 

21233  592 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

593 
Lset :: "i=>i" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

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

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

596 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

597 
L :: "i=>o" where {*Kunen's definition VI 1.5, page 167*} 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

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

13223  600 
text{*NOT SUITABLE FOR REWRITING  RECURSIVE!*} 
46823  601 
lemma Lset: "Lset(i) = (\<Union>j\<in>i. DPow(Lset(j)))" 
13223  602 
by (subst Lset_def [THEN def_transrec], simp) 
603 

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

605 
by (subst Lset, blast) 

606 

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

46823  608 
apply (insert Lset [of x]) 
609 
apply (blast intro: elim: equalityE) 

13223  610 
done 
611 

612 
subsubsection{* Transitivity *} 

613 

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

615 
apply (simp add: Transset_def DPow_def) 

46823  616 
apply (rule_tac x="[X]" in bexI) 
617 
apply (rule_tac x="Member(0,1)" in bexI) 

618 
apply (auto simp add: Un_least_lt_iff) 

13223  619 
done 
620 

46823  621 
lemma Transset_subset_DPow: "Transset(A) ==> A \<subseteq> DPow(A)" 
622 
apply clarify 

13223  623 
apply (simp add: Transset_def) 
46823  624 
apply (blast intro: elem_subset_in_DPow) 
13223  625 
done 
626 

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

46823  628 
apply (simp add: Transset_def) 
629 
apply (blast intro: elem_subset_in_DPow dest: DPowD) 

13223  630 
done 
631 

13651
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

632 
text{*Kunen's VI 1.6 (a)*} 
13223  633 
lemma Transset_Lset: "Transset(Lset(i))" 
634 
apply (rule_tac a=i in eps_induct) 

635 
apply (subst Lset) 

636 
apply (blast intro!: Transset_Union_family Transset_Un Transset_DPow) 

637 
done 

638 

13291  639 
lemma mem_Lset_imp_subset_Lset: "a \<in> Lset(i) ==> a \<subseteq> Lset(i)" 
46823  640 
apply (insert Transset_Lset) 
641 
apply (simp add: Transset_def) 

13291  642 
done 
643 

13223  644 
subsubsection{* Monotonicity *} 
645 

13651
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

646 
text{*Kunen's VI 1.6 (b)*} 
13223  647 
lemma Lset_mono [rule_format]: 
46823  648 
"\<forall>j. i<=j \<longrightarrow> Lset(i) \<subseteq> Lset(j)" 
15481  649 
proof (induct i rule: eps_induct, intro allI impI) 
650 
fix x j 

651 
assume "\<forall>y\<in>x. \<forall>j. y \<subseteq> j \<longrightarrow> Lset(y) \<subseteq> Lset(j)" 

652 
and "x \<subseteq> j" 

653 
thus "Lset(x) \<subseteq> Lset(j)" 

46823  654 
by (force simp add: Lset [of x] Lset [of j]) 
15481  655 
qed 
13223  656 

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

658 
lemma Lset_mono_mem [rule_format]: 

46953  659 
"\<forall>j. i \<in> j \<longrightarrow> Lset(i) \<subseteq> Lset(j)" 
15481  660 
proof (induct i rule: eps_induct, intro allI impI) 
661 
fix x j 

662 
assume "\<forall>y\<in>x. \<forall>j. y \<in> j \<longrightarrow> Lset(y) \<subseteq> Lset(j)" 

663 
and "x \<in> j" 

664 
thus "Lset(x) \<subseteq> Lset(j)" 

46823  665 
by (force simp add: Lset [of j] 
666 
intro!: bexI intro: elem_subset_in_DPow dest: LsetD DPowD) 

15481  667 
qed 
668 

13223  669 

13291  670 
text{*Useful with Reflection to bump up the ordinal*} 
671 
lemma subset_Lset_ltD: "[A \<subseteq> Lset(i); i < j] ==> A \<subseteq> Lset(j)" 

46823  672 
by (blast dest: ltD [THEN Lset_mono_mem]) 
13291  673 

13651
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

674 
subsubsection{* 0, successor and limit equations for Lset *} 
13223  675 

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

677 
by (subst Lset, blast) 

678 

46823  679 
lemma Lset_succ_subset1: "DPow(Lset(i)) \<subseteq> Lset(succ(i))" 
13223  680 
by (subst Lset, rule succI1 [THEN RepFunI, THEN Union_upper]) 
681 

46823  682 
lemma Lset_succ_subset2: "Lset(succ(i)) \<subseteq> DPow(Lset(i))" 
13223  683 
apply (subst Lset, rule UN_least) 
46823  684 
apply (erule succE) 
685 
apply blast 

13223  686 
apply clarify 
687 
apply (rule elem_subset_in_DPow) 

688 
apply (subst Lset) 

46823  689 
apply blast 
690 
apply (blast intro: dest: DPowD Lset_mono_mem) 

13223  691 
done 
692 

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

46823  694 
by (intro equalityI Lset_succ_subset1 Lset_succ_subset2) 
13223  695 

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

697 
apply (subst Lset) 

698 
apply (rule equalityI) 

699 
txt{*first inclusion*} 

700 
apply (rule UN_least) 

701 
apply (erule UnionE) 

702 
apply (rule subset_trans) 

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

704 
txt{*opposite inclusion*} 

705 
apply (rule UN_least) 

706 
apply (subst Lset, blast) 

707 
done 

708 

709 
subsubsection{* Lset applied to Limit ordinals *} 

710 

711 
lemma Limit_Lset_eq: 

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

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

714 

46953  715 
lemma lt_LsetI: "[ a \<in> Lset(j); j<i ] ==> a \<in> Lset(i)" 
13223  716 
by (blast dest: Lset_mono [OF le_imp_subset [OF leI]]) 
717 

718 
lemma Limit_LsetE: 

46953  719 
"[ a \<in> Lset(i); ~R ==> Limit(i); 
720 
!!x. [ x<i; a \<in> Lset(x) ] ==> R 

13223  721 
] ==> R" 
722 
apply (rule classical) 

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

724 
prefer 2 apply assumption 

46823  725 
apply blast 
13223  726 
apply (blast intro: ltI Limit_is_Ord) 
727 
done 

728 

729 
subsubsection{* Basic closure properties *} 

730 

46953  731 
lemma zero_in_Lset: "y \<in> x ==> 0 \<in> Lset(x)" 
13223  732 
by (subst Lset, blast intro: empty_in_DPow) 
733 

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

735 
apply (rule_tac a=x in eps_induct) 

736 
apply (subst Lset) 

46823  737 
apply (blast dest: DPowD) 
13223  738 
done 
739 

740 

13651
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

741 
subsection{*Constructible Ordinals: Kunen's VI 1.9 (b)*} 
13223  742 

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

744 
apply (erule trans_induct3) 

745 
apply (simp_all add: Lset_succ Limit_Lset_eq Limit_Union_eq) 

46823  746 
txt{*The successor case remains.*} 
13223  747 
apply (rule equalityI) 
748 
txt{*First inclusion*} 

46823  749 
apply clarify 
750 
apply (erule Ord_linear_lt, assumption) 

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

752 
apply blast 

13223  753 
apply (blast dest: ltD) 
754 
txt{*Opposite inclusion, @{term "succ(x) \<subseteq> DPow(Lset(x)) \<inter> ON"}*} 

755 
apply auto 

756 
txt{*Key case: *} 

46823  757 
apply (erule subst, rule Ords_in_DPow [OF Transset_Lset]) 
758 
apply (blast intro: elem_subset_in_DPow dest: OrdmemD elim: equalityE) 

759 
apply (blast intro: Ord_in_Ord) 

13223  760 
done 
761 

762 

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

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

765 

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

767 
apply (simp add: Lset_succ) 

46823  768 
apply (subst Ords_of_Lset_eq [symmetric], assumption, 
769 
rule Ords_in_DPow [OF Transset_Lset]) 

13223  770 
done 
771 

13651
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

772 
lemma Ord_in_L: "Ord(i) ==> L(i)" 
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

773 
by (simp add: L_def, blast intro: Ord_in_Lset) 
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

774 

13223  775 
subsubsection{* Unions *} 
776 

777 
lemma Union_in_Lset: 

46823  778 
"X \<in> Lset(i) ==> \<Union>(X) \<in> Lset(succ(i))" 
13223  779 
apply (insert Transset_Lset) 
780 
apply (rule LsetI [OF succI1]) 

46823  781 
apply (simp add: Transset_def DPow_def) 
13223  782 
apply (intro conjI, blast) 
783 
txt{*Now to create the formula @{term "\<exists>y. y \<in> X \<and> x \<in> y"} *} 

46823  784 
apply (rule_tac x="Cons(X,Nil)" in bexI) 
785 
apply (rule_tac x="Exists(And(Member(0,2), Member(1,0)))" in bexI) 

13223  786 
apply typecheck 
46823  787 
apply (simp add: succ_Un_distrib [symmetric], blast) 
13223  788 
done 
789 

46823  790 
theorem Union_in_L: "L(X) ==> L(\<Union>(X))" 
791 
by (simp add: L_def, blast dest: Union_in_Lset) 

13651
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

792 

13223  793 
subsubsection{* Finite sets and ordered pairs *} 
794 

46953  795 
lemma singleton_in_Lset: "a \<in> Lset(i) ==> {a} \<in> Lset(succ(i))" 
46823  796 
by (simp add: Lset_succ singleton_in_DPow) 
13223  797 

798 
lemma doubleton_in_Lset: 

46953  799 
"[ a \<in> Lset(i); b \<in> Lset(i) ] ==> {a,b} \<in> Lset(succ(i))" 
46823  800 
by (simp add: Lset_succ empty_in_DPow cons_in_DPow) 
13223  801 

802 
lemma Pair_in_Lset: 

46953  803 
"[ a \<in> Lset(i); b \<in> Lset(i); Ord(i) ] ==> <a,b> \<in> Lset(succ(succ(i)))" 
13223  804 
apply (unfold Pair_def) 
46823  805 
apply (blast intro: doubleton_in_Lset) 
13223  806 
done 
807 

45602  808 
lemmas Lset_UnI1 = Un_upper1 [THEN Lset_mono [THEN subsetD]] 
809 
lemmas Lset_UnI2 = Un_upper2 [THEN Lset_mono [THEN subsetD]] 

13223  810 

46953  811 
text{*Hard work is finding a single @{term"j \<in> i"} such that @{term"{a,b} \<subseteq> Lset(j)"}*} 
13223  812 
lemma doubleton_in_LLimit: 
46953  813 
"[ a \<in> Lset(i); b \<in> Lset(i); Limit(i) ] ==> {a,b} \<in> Lset(i)" 
13223  814 
apply (erule Limit_LsetE, assumption) 
815 
apply (erule Limit_LsetE, assumption) 

13269  816 
apply (blast intro: lt_LsetI [OF doubleton_in_Lset] 
817 
Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt) 

13223  818 
done 
819 

13651
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

820 
theorem doubleton_in_L: "[ L(a); L(b) ] ==> L({a, b})" 
46823  821 
apply (simp add: L_def, clarify) 
822 
apply (drule Ord2_imp_greater_Limit, assumption) 

823 
apply (blast intro: lt_LsetI doubleton_in_LLimit Limit_is_Ord) 

13651
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

824 
done 
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

825 

13223  826 
lemma Pair_in_LLimit: 
46953  827 
"[ a \<in> Lset(i); b \<in> Lset(i); Limit(i) ] ==> <a,b> \<in> Lset(i)" 
13223  828 
txt{*Infer that a, b occur at ordinals x,xa < i.*} 
829 
apply (erule Limit_LsetE, assumption) 

830 
apply (erule Limit_LsetE, assumption) 

46823  831 
txt{*Infer that @{term"succ(succ(x \<union> xa)) < i"} *} 
13223  832 
apply (blast intro: lt_Ord lt_LsetI [OF Pair_in_Lset] 
833 
Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt) 

834 
done 

835 

836 

837 

13651
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

838 
text{*The rank function for the constructible universe*} 
21233  839 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

840 
lrank :: "i=>i" where {*Kunen's definition VI 1.7*} 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

841 
"lrank(x) == \<mu> i. x \<in> Lset(succ(i))" 
13223  842 

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

844 
by (simp add: L_def, blast) 

845 

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

847 
by (simp add: L_def) 

848 

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

850 
by (simp add: lrank_def) 

851 

46823  852 
lemma Lset_lrank_lt [rule_format]: "Ord(i) ==> x \<in> Lset(i) \<longrightarrow> lrank(x) < i" 
13223  853 
apply (erule trans_induct3) 
46823  854 
apply simp 
855 
apply (simp only: lrank_def) 

856 
apply (blast intro: Least_le) 

857 
apply (simp_all add: Limit_Lset_eq) 

858 
apply (blast intro: ltI Limit_is_Ord lt_trans) 

13223  859 
done 
860 

13651
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

861 
text{*Kunen's VI 1.8. The proof is much harder than the text would 
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

862 
suggest. For a start, it needs the previous lemma, which is proved by 
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

863 
induction.*} 
46823  864 
lemma Lset_iff_lrank_lt: "Ord(i) ==> x \<in> Lset(i) \<longleftrightarrow> L(x) & lrank(x) < i" 
865 
apply (simp add: L_def, auto) 

866 
apply (blast intro: Lset_lrank_lt) 

867 
apply (unfold lrank_def) 

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

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

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

13223  871 
done 
872 

46823  873 
lemma Lset_succ_lrank_iff [simp]: "x \<in> Lset(succ(lrank(x))) \<longleftrightarrow> L(x)" 
13223  874 
by (simp add: Lset_iff_lrank_lt) 
875 

13651
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

876 
text{*Kunen's VI 1.9 (a)*} 
13223  877 
lemma lrank_of_Ord: "Ord(i) ==> lrank(i) = i" 
46823  878 
apply (unfold lrank_def) 
879 
apply (rule Least_equality) 

880 
apply (erule Ord_in_Lset) 

13223  881 
apply assumption 
46823  882 
apply (insert notin_Lset [of i]) 
883 
apply (blast intro!: le_imp_subset Lset_mono [THEN subsetD]) 

13223  884 
done 
885 

13245  886 

13223  887 
text{*This is lrank(lrank(a)) = lrank(a) *} 
888 
declare Ord_lrank [THEN lrank_of_Ord, simp] 

889 

13651
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

890 
text{*Kunen's VI 1.10 *} 
13223  891 
lemma Lset_in_Lset_succ: "Lset(i) \<in> Lset(succ(i))"; 
46823  892 
apply (simp add: Lset_succ DPow_def) 
893 
apply (rule_tac x=Nil in bexI) 

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

895 
apply auto 

13223  896 
done 
897 

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

46823  899 
apply (unfold lrank_def) 
900 
apply (rule Least_equality) 

901 
apply (rule Lset_in_Lset_succ) 

13223  902 
apply assumption 
46823  903 
apply clarify 
904 
apply (subgoal_tac "Lset(succ(ia)) \<subseteq> Lset(i)") 

905 
apply (blast dest: mem_irrefl) 

906 
apply (blast intro!: le_imp_subset Lset_mono) 

13223  907 
done 
908 

13651
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

909 
text{*Kunen's VI 1.11 *} 
46823  910 
lemma Lset_subset_Vset: "Ord(i) ==> Lset(i) \<subseteq> Vset(i)"; 
13223  911 
apply (erule trans_induct) 
46823  912 
apply (subst Lset) 
913 
apply (subst Vset) 

914 
apply (rule UN_mono [OF subset_refl]) 

915 
apply (rule subset_trans [OF DPow_subset_Pow]) 

916 
apply (rule Pow_mono, blast) 

13223  917 
done 
918 

13651
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

919 
text{*Kunen's VI 1.12 *} 
13535  920 
lemma Lset_subset_Vset': "i \<in> nat ==> Lset(i) = Vset(i)"; 
13223  921 
apply (erule nat_induct) 
46823  922 
apply (simp add: Vfrom_0) 
923 
apply (simp add: Lset_succ Vset_succ Finite_Vset Finite_DPow_eq_Pow) 

13223  924 
done 
925 

46823  926 
text{*Every set of constructible sets is included in some @{term Lset}*} 
13291  927 
lemma subset_Lset: 
928 
"(\<forall>x\<in>A. L(x)) ==> \<exists>i. Ord(i) & A \<subseteq> Lset(i)" 

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

930 

931 
lemma subset_LsetE: 

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

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

934 
==> P" 

46823  935 
by (blast dest: subset_Lset) 
13291  936 

13651
ac80e101306a
Cosmetic changes suggested by writing the paper. Deleted some
paulson
parents:
13647
diff
changeset

937 
subsubsection{*For L to satisfy the Powerset axiom *} 
13223  938 

939 
lemma LPow_env_typing: 

46823  940 
"[ y \<in> Lset(i); Ord(i); y \<subseteq> X ] 
13511  941 
==> \<exists>z \<in> Pow(X). y \<in> Lset(succ(lrank(z)))" 
46823  942 
by (auto intro: L_I iff: Lset_succ_lrank_iff) 
13223  943 

944 
lemma LPow_in_Lset: 

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

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

46823  947 
apply simp 
13223  948 
apply (rule LsetI [OF succI1]) 
46823  949 
apply (simp add: DPow_def) 
950 
apply (intro conjI, clarify) 

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

13223  952 
txt{*Now to create the formula @{term "y \<subseteq> X"} *} 
46823  953 
apply (rule_tac x="Cons(X,Nil)" in bexI) 
954 
apply (rule_tac x="subset_fm(0,1)" in bexI) 

13223  955 
apply typecheck 
46823  956 
apply (rule conjI) 
957 
apply (simp add: succ_Un_distrib [symmetric]) 

958 
apply (rule equality_iffI) 

13511  959 
apply (simp add: Transset_UN [OF Transset_Lset] LPow_env_typing) 
46823  960 
apply (auto intro: L_I iff: Lset_succ_lrank_iff) 
13223  961 
done 
962 

13245  963 
theorem LPow_in_L: "L(X) ==> L({y \<in> Pow(X). L(y)})" 
13223  964 
by (blast intro: L_I dest: L_D LPow_in_Lset) 
965 

13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

966 

31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

967 
subsection{*Eliminating @{term arity} from the Definition of @{term Lset}*} 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

968 

31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

969 
lemma nth_zero_eq_0: "n \<in> nat ==> nth(n,[0]) = 0" 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

970 
by (induct_tac n, auto) 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

971 

31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

972 
lemma sats_app_0_iff [rule_format]: 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

973 
"[ p \<in> formula; 0 \<in> A ] 
46823  974 
==> \<forall>env \<in> list(A). sats(A,p, env@[0]) \<longleftrightarrow> sats(A,p,env)" 
13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

975 
apply (induct_tac p) 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

976 
apply (simp_all del: app_Cons add: app_Cons [symmetric] 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

977 
add: nth_zero_eq_0 nth_append not_lt_iff_le nth_eq_0) 
13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

978 
done 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

979 

31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

980 
lemma sats_app_zeroes_iff: 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

981 
"[ p \<in> formula; 0 \<in> A; env \<in> list(A); n \<in> nat ] 
46823  982 
==> sats(A,p,env @ repeat(0,n)) \<longleftrightarrow> sats(A,p,env)" 
983 
apply (induct_tac n, simp) 

13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

984 
apply (simp del: repeat.simps 
46823  985 
add: repeat_succ_app sats_app_0_iff app_assoc [symmetric]) 
13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

986 
done 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

987 

31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

988 
lemma exists_bigger_env: 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

989 
"[ p \<in> formula; 0 \<in> A; env \<in> list(A) ] 
46823  990 
==> \<exists>env' \<in> list(A). arity(p) \<le> succ(length(env')) & 
991 
(\<forall>a\<in>A. sats(A,p,Cons(a,env')) \<longleftrightarrow> sats(A,p,Cons(a,env)))" 

992 
apply (rule_tac x="env @ repeat(0,arity(p))" in bexI) 

13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

993 
apply (simp del: app_Cons add: app_Cons [symmetric] 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

994 
add: length_repeat sats_app_zeroes_iff, typecheck) 
13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

995 
done 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

996 

31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

997 

31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

998 
text{*A simpler version of @{term DPow}: no arity check!*} 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

999 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

1000 
DPow' :: "i => i" where 
46823  1001 
"DPow'(A) == {X \<in> Pow(A). 
1002 
\<exists>env \<in> list(A). \<exists>p \<in> formula. 

13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

1003 
X = {x\<in>A. sats(A, p, Cons(x,env))}}" 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

1004 

46823  1005 
lemma DPow_subset_DPow': "DPow(A) \<subseteq> DPow'(A)"; 
13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

1006 
by (simp add: DPow_def DPow'_def, blast) 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

1007 

31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

1008 
lemma DPow'_0: "DPow'(0) = {0}" 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

1009 
by (auto simp add: DPow'_def) 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

1010 

31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

1011 
lemma DPow'_subset_DPow: "0 \<in> A ==> DPow'(A) \<subseteq> DPow(A)" 
46823  1012 
apply (auto simp add: DPow'_def DPow_def) 
1013 
apply (frule exists_bigger_env, assumption+, force) 

13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

1014 
done 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

1015 

31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

1016 
lemma DPow_eq_DPow': "Transset(A) ==> DPow(A) = DPow'(A)" 
46823  1017 
apply (drule Transset_0_disj) 
1018 
apply (erule disjE) 

1019 
apply (simp add: DPow'_0 Finite_DPow_eq_Pow) 

13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

1020 
apply (rule equalityI) 
46823  1021 
apply (rule DPow_subset_DPow') 
1022 
apply (erule DPow'_subset_DPow) 

13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

1023 
done 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

1024 

31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

1025 
text{*And thus we can relativize @{term Lset} without bothering with 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

1026 
@{term arity} and @{term length}*} 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

1027 
lemma Lset_eq_transrec_DPow': "Lset(i) = transrec(i, %x f. \<Union>y\<in>x. DPow'(f`y))" 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

1028 
apply (rule_tac a=i in eps_induct) 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

1029 
apply (subst Lset) 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

1030 
apply (subst transrec) 
46823  1031 
apply (simp only: DPow_eq_DPow' [OF Transset_Lset], simp) 
13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

1032 
done 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

1033 

31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

1034 
text{*With this rule we can specify @{term p} later and don't worry about 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

1035 
arities at all!*} 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

1036 
lemma DPow_LsetI [rule_format]: 
46823  1037 
"[\<forall>x\<in>Lset(i). P(x) \<longleftrightarrow> sats(Lset(i), p, Cons(x,env)); 
13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

1038 
env \<in> list(Lset(i)); p \<in> formula] 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

1039 
==> {x\<in>Lset(i). P(x)} \<in> DPow(Lset(i))" 
46823  1040 
by (simp add: DPow_eq_DPow' [OF Transset_Lset] DPow'_def, blast) 
13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset

1041 

13223  1042 
end 