author | paulson |
Wed, 21 Aug 2002 15:56:37 +0200 | |
changeset 13511 | e4b129eaa9c6 |
parent 13505 | 52a16cb7fefb |
child 13535 | 007559e981c7 |
permissions | -rw-r--r-- |
13505 | 1 |
(* Title: ZF/Constructible/Formula.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 2002 University of Cambridge |
|
5 |
*) |
|
6 |
||
13223 | 7 |
header {* First-Order Formulas and the Definition of the Class L *} |
8 |
||
9 |
theory Formula = Main: |
|
10 |
||
13291 | 11 |
subsection{*Internalized formulas of FOL*} |
12 |
||
13 |
text{*De Bruijn representation. |
|
14 |
Unbound variables get their denotations from an environment.*} |
|
13223 | 15 |
|
16 |
consts formula :: i |
|
17 |
datatype |
|
18 |
"formula" = Member ("x: nat", "y: nat") |
|
19 |
| Equal ("x: nat", "y: nat") |
|
13398
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
20 |
| Nand ("p: formula", "q: formula") |
13223 | 21 |
| Forall ("p: formula") |
22 |
||
23 |
declare formula.intros [TC] |
|
24 |
||
13398
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
25 |
constdefs Neg :: "i=>i" |
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
26 |
"Neg(p) == Nand(p,p)" |
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
27 |
|
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
28 |
constdefs And :: "[i,i]=>i" |
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
29 |
"And(p,q) == Neg(Nand(p,q))" |
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
30 |
|
13223 | 31 |
constdefs Or :: "[i,i]=>i" |
13398
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
32 |
"Or(p,q) == Nand(Neg(p),Neg(q))" |
13223 | 33 |
|
34 |
constdefs Implies :: "[i,i]=>i" |
|
13398
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
35 |
"Implies(p,q) == Nand(p,Neg(q))" |
13223 | 36 |
|
13291 | 37 |
constdefs Iff :: "[i,i]=>i" |
38 |
"Iff(p,q) == And(Implies(p,q), Implies(q,p))" |
|
39 |
||
13223 | 40 |
constdefs Exists :: "i=>i" |
41 |
"Exists(p) == Neg(Forall(Neg(p)))"; |
|
42 |
||
13398
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
43 |
lemma Neg_type [TC]: "p \<in> formula ==> Neg(p) \<in> formula" |
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
44 |
by (simp add: Neg_def) |
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
45 |
|
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
46 |
lemma And_type [TC]: "[| p \<in> formula; q \<in> formula |] ==> And(p,q) \<in> formula" |
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
47 |
by (simp add: And_def) |
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
48 |
|
13223 | 49 |
lemma Or_type [TC]: "[| p \<in> formula; q \<in> formula |] ==> Or(p,q) \<in> formula" |
50 |
by (simp add: Or_def) |
|
51 |
||
52 |
lemma Implies_type [TC]: |
|
53 |
"[| p \<in> formula; q \<in> formula |] ==> Implies(p,q) \<in> formula" |
|
54 |
by (simp add: Implies_def) |
|
55 |
||
13291 | 56 |
lemma Iff_type [TC]: |
57 |
"[| p \<in> formula; q \<in> formula |] ==> Iff(p,q) \<in> formula" |
|
58 |
by (simp add: Iff_def) |
|
59 |
||
13223 | 60 |
lemma Exists_type [TC]: "p \<in> formula ==> Exists(p) \<in> formula" |
61 |
by (simp add: Exists_def) |
|
62 |
||
63 |
||
64 |
consts satisfies :: "[i,i]=>i" |
|
65 |
primrec (*explicit lambda is required because the environment varies*) |
|
66 |
"satisfies(A,Member(x,y)) = |
|
67 |
(\<lambda>env \<in> list(A). bool_of_o (nth(x,env) \<in> nth(y,env)))" |
|
68 |
||
69 |
"satisfies(A,Equal(x,y)) = |
|
70 |
(\<lambda>env \<in> list(A). bool_of_o (nth(x,env) = nth(y,env)))" |
|
71 |
||
13398
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
72 |
"satisfies(A,Nand(p,q)) = |
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
73 |
(\<lambda>env \<in> list(A). not ((satisfies(A,p)`env) and (satisfies(A,q)`env)))" |
13223 | 74 |
|
75 |
"satisfies(A,Forall(p)) = |
|
76 |
(\<lambda>env \<in> list(A). bool_of_o (\<forall>x\<in>A. satisfies(A,p) ` (Cons(x,env)) = 1))" |
|
77 |
||
78 |
||
79 |
lemma "p \<in> formula ==> satisfies(A,p) \<in> list(A) -> bool" |
|
80 |
by (induct_tac p, simp_all) |
|
81 |
||
82 |
syntax sats :: "[i,i,i] => o" |
|
83 |
translations "sats(A,p,env)" == "satisfies(A,p)`env = 1" |
|
84 |
||
85 |
lemma [simp]: |
|
86 |
"env \<in> list(A) |
|
87 |
==> sats(A, Member(x,y), env) <-> nth(x,env) \<in> nth(y,env)" |
|
88 |
by simp |
|
89 |
||
90 |
lemma [simp]: |
|
91 |
"env \<in> list(A) |
|
92 |
==> sats(A, Equal(x,y), env) <-> nth(x,env) = nth(y,env)" |
|
93 |
by simp |
|
94 |
||
13398
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
95 |
lemma sats_Nand_iff [simp]: |
13223 | 96 |
"env \<in> list(A) |
13398
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
97 |
==> (sats(A, Nand(p,q), env)) <-> ~ (sats(A,p,env) & sats(A,q,env))" |
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
98 |
by (simp add: Bool.and_def Bool.not_def cond_def) |
13223 | 99 |
|
100 |
lemma sats_Forall_iff [simp]: |
|
101 |
"env \<in> list(A) |
|
102 |
==> sats(A, Forall(p), env) <-> (\<forall>x\<in>A. sats(A, p, Cons(x,env)))" |
|
103 |
by simp |
|
104 |
||
105 |
declare satisfies.simps [simp del]; |
|
106 |
||
13298 | 107 |
subsection{*Dividing line between primitive and derived connectives*} |
13223 | 108 |
|
13398
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
109 |
lemma sats_Neg_iff [simp]: |
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
110 |
"env \<in> list(A) |
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
111 |
==> sats(A, Neg(p), env) <-> ~ sats(A,p,env)" |
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
112 |
by (simp add: Neg_def) |
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
113 |
|
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
114 |
lemma sats_And_iff [simp]: |
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
115 |
"env \<in> list(A) |
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
116 |
==> (sats(A, And(p,q), env)) <-> sats(A,p,env) & sats(A,q,env)" |
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
117 |
by (simp add: And_def) |
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
118 |
|
13223 | 119 |
lemma sats_Or_iff [simp]: |
120 |
"env \<in> list(A) |
|
121 |
==> (sats(A, Or(p,q), env)) <-> sats(A,p,env) | sats(A,q,env)" |
|
122 |
by (simp add: Or_def) |
|
123 |
||
124 |
lemma sats_Implies_iff [simp]: |
|
125 |
"env \<in> list(A) |
|
126 |
==> (sats(A, Implies(p,q), env)) <-> (sats(A,p,env) --> sats(A,q,env))" |
|
13291 | 127 |
by (simp add: Implies_def, blast) |
128 |
||
129 |
lemma sats_Iff_iff [simp]: |
|
130 |
"env \<in> list(A) |
|
131 |
==> (sats(A, Iff(p,q), env)) <-> (sats(A,p,env) <-> sats(A,q,env))" |
|
132 |
by (simp add: Iff_def, blast) |
|
13223 | 133 |
|
134 |
lemma sats_Exists_iff [simp]: |
|
135 |
"env \<in> list(A) |
|
136 |
==> sats(A, Exists(p), env) <-> (\<exists>x\<in>A. sats(A, p, Cons(x,env)))" |
|
137 |
by (simp add: Exists_def) |
|
138 |
||
139 |
||
13291 | 140 |
subsubsection{*Derived rules to help build up formulas*} |
141 |
||
142 |
lemma mem_iff_sats: |
|
143 |
"[| nth(i,env) = x; nth(j,env) = y; env \<in> list(A)|] |
|
144 |
==> (x\<in>y) <-> sats(A, Member(i,j), env)" |
|
145 |
by (simp add: satisfies.simps) |
|
146 |
||
13298 | 147 |
lemma equal_iff_sats: |
148 |
"[| nth(i,env) = x; nth(j,env) = y; env \<in> list(A)|] |
|
149 |
==> (x=y) <-> sats(A, Equal(i,j), env)" |
|
150 |
by (simp add: satisfies.simps) |
|
151 |
||
13316 | 152 |
lemma not_iff_sats: |
153 |
"[| P <-> sats(A,p,env); env \<in> list(A)|] |
|
154 |
==> (~P) <-> sats(A, Neg(p), env)" |
|
155 |
by simp |
|
156 |
||
13291 | 157 |
lemma conj_iff_sats: |
158 |
"[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|] |
|
159 |
==> (P & Q) <-> sats(A, And(p,q), env)" |
|
160 |
by (simp add: sats_And_iff) |
|
161 |
||
162 |
lemma disj_iff_sats: |
|
163 |
"[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|] |
|
164 |
==> (P | Q) <-> sats(A, Or(p,q), env)" |
|
165 |
by (simp add: sats_Or_iff) |
|
166 |
||
167 |
lemma imp_iff_sats: |
|
168 |
"[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|] |
|
169 |
==> (P --> Q) <-> sats(A, Implies(p,q), env)" |
|
170 |
by (simp add: sats_Forall_iff) |
|
171 |
||
172 |
lemma iff_iff_sats: |
|
173 |
"[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|] |
|
174 |
==> (P <-> Q) <-> sats(A, Iff(p,q), env)" |
|
175 |
by (simp add: sats_Forall_iff) |
|
176 |
||
177 |
lemma imp_iff_sats: |
|
178 |
"[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|] |
|
179 |
==> (P --> Q) <-> sats(A, Implies(p,q), env)" |
|
180 |
by (simp add: sats_Forall_iff) |
|
181 |
||
182 |
lemma ball_iff_sats: |
|
183 |
"[| !!x. x\<in>A ==> P(x) <-> sats(A, p, Cons(x, env)); env \<in> list(A)|] |
|
184 |
==> (\<forall>x\<in>A. P(x)) <-> sats(A, Forall(p), env)" |
|
185 |
by (simp add: sats_Forall_iff) |
|
186 |
||
187 |
lemma bex_iff_sats: |
|
188 |
"[| !!x. x\<in>A ==> P(x) <-> sats(A, p, Cons(x, env)); env \<in> list(A)|] |
|
189 |
==> (\<exists>x\<in>A. P(x)) <-> sats(A, Exists(p), env)" |
|
190 |
by (simp add: sats_Exists_iff) |
|
191 |
||
13316 | 192 |
lemmas FOL_iff_sats = |
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 |
|
197 |
constdefs incr_var :: "[i,i]=>i" |
|
198 |
"incr_var(x,lev) == if x<lev then x else succ(x)" |
|
199 |
||
200 |
lemma incr_var_lt: "x<lev ==> incr_var(x,lev) = x" |
|
201 |
by (simp add: incr_var_def) |
|
202 |
||
203 |
lemma incr_var_le: "lev\<le>x ==> incr_var(x,lev) = succ(x)" |
|
204 |
apply (simp add: incr_var_def) |
|
205 |
apply (blast dest: lt_trans1) |
|
206 |
done |
|
207 |
||
208 |
consts incr_bv :: "i=>i" |
|
209 |
primrec |
|
210 |
"incr_bv(Member(x,y)) = |
|
211 |
(\<lambda>lev \<in> nat. Member (incr_var(x,lev), incr_var(y,lev)))" |
|
212 |
||
213 |
"incr_bv(Equal(x,y)) = |
|
214 |
(\<lambda>lev \<in> nat. Equal (incr_var(x,lev), incr_var(y,lev)))" |
|
215 |
||
13398
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
216 |
"incr_bv(Nand(p,q)) = |
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
217 |
(\<lambda>lev \<in> nat. Nand (incr_bv(p)`lev, incr_bv(q)`lev))" |
13223 | 218 |
|
219 |
"incr_bv(Forall(p)) = |
|
220 |
(\<lambda>lev \<in> nat. Forall (incr_bv(p) ` succ(lev)))" |
|
221 |
||
222 |
||
223 |
constdefs incr_boundvars :: "i => i" |
|
224 |
"incr_boundvars(p) == incr_bv(p)`0" |
|
225 |
||
226 |
||
227 |
lemma [TC]: "x \<in> nat ==> incr_var(x,lev) \<in> nat" |
|
228 |
by (simp add: incr_var_def) |
|
229 |
||
230 |
lemma incr_bv_type [TC]: "p \<in> formula ==> incr_bv(p) \<in> nat -> formula" |
|
231 |
by (induct_tac p, simp_all) |
|
232 |
||
233 |
lemma incr_boundvars_type [TC]: "p \<in> formula ==> incr_boundvars(p) \<in> formula" |
|
234 |
by (simp add: incr_boundvars_def) |
|
235 |
||
236 |
(*Obviously DPow is closed under complements and finite intersections and |
|
237 |
unions. Needs an inductive lemma to allow two lists of parameters to |
|
238 |
be combined.*) |
|
239 |
||
240 |
lemma sats_incr_bv_iff [rule_format]: |
|
241 |
"[| p \<in> formula; env \<in> list(A); x \<in> A |] |
|
242 |
==> \<forall>bvs \<in> list(A). |
|
243 |
sats(A, incr_bv(p) ` length(bvs), bvs @ Cons(x,env)) <-> |
|
244 |
sats(A, p, bvs@env)" |
|
245 |
apply (induct_tac p) |
|
246 |
apply (simp_all add: incr_var_def nth_append succ_lt_iff length_type) |
|
247 |
apply (auto simp add: diff_succ not_lt_iff_le) |
|
248 |
done |
|
249 |
||
250 |
(*UNUSED*) |
|
251 |
lemma sats_incr_boundvars_iff: |
|
252 |
"[| p \<in> formula; env \<in> list(A); x \<in> A |] |
|
253 |
==> sats(A, incr_boundvars(p), Cons(x,env)) <-> sats(A, p, env)" |
|
254 |
apply (insert sats_incr_bv_iff [of p env A x Nil]) |
|
255 |
apply (simp add: incr_boundvars_def) |
|
256 |
done |
|
257 |
||
258 |
(*UNUSED |
|
259 |
lemma formula_add_params [rule_format]: |
|
260 |
"[| p \<in> formula; n \<in> nat |] |
|
261 |
==> \<forall>bvs \<in> list(A). \<forall>env \<in> list(A). |
|
262 |
length(bvs) = n --> |
|
263 |
sats(A, iterates(incr_boundvars,n,p), bvs@env) <-> sats(A, p, env)" |
|
264 |
apply (induct_tac n, simp, clarify) |
|
265 |
apply (erule list.cases) |
|
266 |
apply (auto simp add: sats_incr_boundvars_iff) |
|
267 |
done |
|
268 |
*) |
|
269 |
||
270 |
consts arity :: "i=>i" |
|
271 |
primrec |
|
272 |
"arity(Member(x,y)) = succ(x) \<union> succ(y)" |
|
273 |
||
274 |
"arity(Equal(x,y)) = succ(x) \<union> succ(y)" |
|
275 |
||
13398
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
276 |
"arity(Nand(p,q)) = arity(p) \<union> arity(q)" |
13223 | 277 |
|
13269 | 278 |
"arity(Forall(p)) = nat_case(0, %x. x, arity(p))" |
13223 | 279 |
|
280 |
||
281 |
lemma arity_type [TC]: "p \<in> formula ==> arity(p) \<in> nat" |
|
282 |
by (induct_tac p, simp_all) |
|
283 |
||
13398
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
284 |
lemma arity_Neg [simp]: "arity(Neg(p)) = arity(p)" |
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
285 |
by (simp add: Neg_def) |
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
286 |
|
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
287 |
lemma arity_And [simp]: "arity(And(p,q)) = arity(p) \<union> arity(q)" |
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
288 |
by (simp add: And_def) |
1cadd412da48
Towards relativization and absoluteness of formula_rec
paulson
parents:
13385
diff
changeset
|
289 |
|
13223 | 290 |
lemma arity_Or [simp]: "arity(Or(p,q)) = arity(p) \<union> arity(q)" |
291 |
by (simp add: Or_def) |
|
292 |
||
293 |
lemma arity_Implies [simp]: "arity(Implies(p,q)) = arity(p) \<union> arity(q)" |
|
294 |
by (simp add: Implies_def) |
|
295 |
||
13291 | 296 |
lemma arity_Iff [simp]: "arity(Iff(p,q)) = arity(p) \<union> arity(q)" |
297 |
by (simp add: Iff_def, blast) |
|
298 |
||
13269 | 299 |
lemma arity_Exists [simp]: "arity(Exists(p)) = nat_case(0, %x. x, arity(p))" |
13223 | 300 |
by (simp add: Exists_def) |
301 |
||
302 |
||
303 |
lemma arity_sats_iff [rule_format]: |
|
304 |
"[| p \<in> formula; extra \<in> list(A) |] |
|
305 |
==> \<forall>env \<in> list(A). |
|
306 |
arity(p) \<le> length(env) --> |
|
307 |
sats(A, p, env @ extra) <-> sats(A, p, env)" |
|
308 |
apply (induct_tac p) |
|
13269 | 309 |
apply (simp_all add: nth_append Un_least_lt_iff arity_type nat_imp_quasinat |
310 |
split: split_nat_case, auto) |
|
13223 | 311 |
done |
312 |
||
313 |
lemma arity_sats1_iff: |
|
314 |
"[| arity(p) \<le> succ(length(env)); p \<in> formula; x \<in> A; env \<in> list(A); |
|
315 |
extra \<in> list(A) |] |
|
316 |
==> sats(A, p, Cons(x, env @ extra)) <-> sats(A, p, Cons(x, env))" |
|
317 |
apply (insert arity_sats_iff [of p extra A "Cons(x,env)"]) |
|
318 |
apply simp |
|
319 |
done |
|
320 |
||
321 |
(*the following two lemmas prevent huge case splits in arity_incr_bv_lemma*) |
|
322 |
lemma incr_var_lemma: |
|
323 |
"[| x \<in> nat; y \<in> nat; lev \<le> x |] |
|
324 |
==> succ(x) \<union> incr_var(y,lev) = succ(x \<union> y)" |
|
325 |
apply (simp add: incr_var_def Ord_Un_if, auto) |
|
326 |
apply (blast intro: leI) |
|
327 |
apply (simp add: not_lt_iff_le) |
|
328 |
apply (blast intro: le_anti_sym) |
|
329 |
apply (blast dest: lt_trans2) |
|
330 |
done |
|
331 |
||
332 |
lemma incr_And_lemma: |
|
333 |
"y < x ==> y \<union> succ(x) = succ(x \<union> y)" |
|
334 |
apply (simp add: Ord_Un_if lt_Ord lt_Ord2 succ_lt_iff) |
|
335 |
apply (blast dest: lt_asym) |
|
336 |
done |
|
337 |
||
338 |
lemma arity_incr_bv_lemma [rule_format]: |
|
339 |
"p \<in> formula |
|
340 |
==> \<forall>n \<in> nat. arity (incr_bv(p) ` n) = |
|
341 |
(if n < arity(p) then succ(arity(p)) else arity(p))" |
|
342 |
apply (induct_tac p) |
|
343 |
apply (simp_all add: imp_disj not_lt_iff_le Un_least_lt_iff lt_Un_iff le_Un_iff |
|
344 |
succ_Un_distrib [symmetric] incr_var_lt incr_var_le |
|
13269 | 345 |
Un_commute incr_var_lemma arity_type nat_imp_quasinat |
346 |
split: split_nat_case) |
|
347 |
txt{*the Forall case reduces to linear arithmetic*} |
|
348 |
prefer 2 |
|
349 |
apply clarify |
|
350 |
apply (blast dest: lt_trans1) |
|
351 |
txt{*left with the And case*} |
|
13223 | 352 |
apply safe |
353 |
apply (blast intro: incr_And_lemma lt_trans1) |
|
354 |
apply (subst incr_And_lemma) |
|
13269 | 355 |
apply (blast intro: lt_trans1) |
356 |
apply (simp add: Un_commute) |
|
13223 | 357 |
done |
358 |
||
359 |
lemma arity_incr_boundvars_eq: |
|
360 |
"p \<in> formula |
|
361 |
==> arity(incr_boundvars(p)) = |
|
362 |
(if 0 < arity(p) then succ(arity(p)) else arity(p))" |
|
363 |
apply (insert arity_incr_bv_lemma [of p 0]) |
|
364 |
apply (simp add: incr_boundvars_def) |
|
365 |
done |
|
366 |
||
367 |
lemma arity_iterates_incr_boundvars_eq: |
|
368 |
"[| p \<in> formula; n \<in> nat |] |
|
369 |
==> arity(incr_boundvars^n(p)) = |
|
370 |
(if 0 < arity(p) then n #+ arity(p) else arity(p))" |
|
371 |
apply (induct_tac n) |
|
372 |
apply (simp_all add: arity_incr_boundvars_eq not_lt_iff_le) |
|
373 |
done |
|
374 |
||
375 |
||
13298 | 376 |
subsection{*Renaming all but the first bound variable*} |
13223 | 377 |
|
378 |
constdefs incr_bv1 :: "i => i" |
|
379 |
"incr_bv1(p) == incr_bv(p)`1" |
|
380 |
||
381 |
||
382 |
lemma incr_bv1_type [TC]: "p \<in> formula ==> incr_bv1(p) \<in> formula" |
|
383 |
by (simp add: incr_bv1_def) |
|
384 |
||
385 |
(*For renaming all but the bound variable at level 0*) |
|
386 |
lemma sats_incr_bv1_iff [rule_format]: |
|
387 |
"[| p \<in> formula; env \<in> list(A); x \<in> A; y \<in> A |] |
|
388 |
==> sats(A, incr_bv1(p), Cons(x, Cons(y, env))) <-> |
|
389 |
sats(A, p, Cons(x,env))" |
|
390 |
apply (insert sats_incr_bv_iff [of p env A y "Cons(x,Nil)"]) |
|
391 |
apply (simp add: incr_bv1_def) |
|
392 |
done |
|
393 |
||
394 |
lemma formula_add_params1 [rule_format]: |
|
395 |
"[| p \<in> formula; n \<in> nat; x \<in> A |] |
|
396 |
==> \<forall>bvs \<in> list(A). \<forall>env \<in> list(A). |
|
397 |
length(bvs) = n --> |
|
398 |
sats(A, iterates(incr_bv1, n, p), Cons(x, bvs@env)) <-> |
|
399 |
sats(A, p, Cons(x,env))" |
|
400 |
apply (induct_tac n, simp, clarify) |
|
401 |
apply (erule list.cases) |
|
402 |
apply (simp_all add: sats_incr_bv1_iff) |
|
403 |
done |
|
404 |
||
405 |
||
406 |
lemma arity_incr_bv1_eq: |
|
407 |
"p \<in> formula |
|
408 |
==> arity(incr_bv1(p)) = |
|
409 |
(if 1 < arity(p) then succ(arity(p)) else arity(p))" |
|
410 |
apply (insert arity_incr_bv_lemma [of p 1]) |
|
411 |
apply (simp add: incr_bv1_def) |
|
412 |
done |
|
413 |
||
414 |
lemma arity_iterates_incr_bv1_eq: |
|
415 |
"[| p \<in> formula; n \<in> nat |] |
|
416 |
==> arity(incr_bv1^n(p)) = |
|
417 |
(if 1 < arity(p) then n #+ arity(p) else arity(p))" |
|
418 |
apply (induct_tac n) |
|
13298 | 419 |
apply (simp_all add: arity_incr_bv1_eq) |
13223 | 420 |
apply (simp add: not_lt_iff_le) |
421 |
apply (blast intro: le_trans add_le_self2 arity_type) |
|
422 |
done |
|
423 |
||
424 |
||
425 |
(*Definable powerset operation: Kunen's definition 1.1, page 165.*) |
|
426 |
constdefs DPow :: "i => i" |
|
427 |
"DPow(A) == {X \<in> Pow(A). |
|
428 |
\<exists>env \<in> list(A). \<exists>p \<in> formula. |
|
429 |
arity(p) \<le> succ(length(env)) & |
|
430 |
X = {x\<in>A. sats(A, p, Cons(x,env))}}" |
|
431 |
||
432 |
lemma DPowI: |
|
13291 | 433 |
"[|env \<in> list(A); p \<in> formula; arity(p) \<le> succ(length(env))|] |
13223 | 434 |
==> {x\<in>A. sats(A, p, Cons(x,env))} \<in> DPow(A)" |
435 |
by (simp add: DPow_def, blast) |
|
436 |
||
13291 | 437 |
text{*With this rule we can specify @{term p} later.*} |
438 |
lemma DPowI2 [rule_format]: |
|
439 |
"[|\<forall>x\<in>A. P(x) <-> sats(A, p, Cons(x,env)); |
|
440 |
env \<in> list(A); p \<in> formula; arity(p) \<le> succ(length(env))|] |
|
441 |
==> {x\<in>A. P(x)} \<in> DPow(A)" |
|
442 |
by (simp add: DPow_def, blast) |
|
443 |
||
13223 | 444 |
lemma DPowD: |
445 |
"X \<in> DPow(A) |
|
446 |
==> X <= A & |
|
447 |
(\<exists>env \<in> list(A). |
|
448 |
\<exists>p \<in> formula. arity(p) \<le> succ(length(env)) & |
|
449 |
X = {x\<in>A. sats(A, p, Cons(x,env))})" |
|
450 |
by (simp add: DPow_def) |
|
451 |
||
452 |
lemmas DPow_imp_subset = DPowD [THEN conjunct1] |
|
453 |
||
454 |
(*Lemma 1.2*) |
|
455 |
lemma "[| p \<in> formula; env \<in> list(A); arity(p) \<le> succ(length(env)) |] |
|
456 |
==> {x\<in>A. sats(A, p, Cons(x,env))} \<in> DPow(A)" |
|
457 |
by (blast intro: DPowI) |
|
458 |
||
459 |
lemma DPow_subset_Pow: "DPow(A) <= Pow(A)" |
|
460 |
by (simp add: DPow_def, blast) |
|
461 |
||
462 |
lemma empty_in_DPow: "0 \<in> DPow(A)" |
|
463 |
apply (simp add: DPow_def) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13328
diff
changeset
|
464 |
apply (rule_tac x=Nil in bexI) |
13223 | 465 |
apply (rule_tac x="Neg(Equal(0,0))" in bexI) |
466 |
apply (auto simp add: Un_least_lt_iff) |
|
467 |
done |
|
468 |
||
469 |
lemma Compl_in_DPow: "X \<in> DPow(A) ==> (A-X) \<in> DPow(A)" |
|
470 |
apply (simp add: DPow_def, clarify, auto) |
|
471 |
apply (rule bexI) |
|
472 |
apply (rule_tac x="Neg(p)" in bexI) |
|
473 |
apply auto |
|
474 |
done |
|
475 |
||
476 |
lemma Int_in_DPow: "[| X \<in> DPow(A); Y \<in> DPow(A) |] ==> X Int Y \<in> DPow(A)" |
|
477 |
apply (simp add: DPow_def, auto) |
|
478 |
apply (rename_tac envp p envq q) |
|
479 |
apply (rule_tac x="envp@envq" in bexI) |
|
480 |
apply (rule_tac x="And(p, iterates(incr_bv1,length(envp),q))" in bexI) |
|
481 |
apply typecheck |
|
482 |
apply (rule conjI) |
|
483 |
(*finally check the arity!*) |
|
484 |
apply (simp add: arity_iterates_incr_bv1_eq length_app Un_least_lt_iff) |
|
485 |
apply (force intro: add_le_self le_trans) |
|
486 |
apply (simp add: arity_sats1_iff formula_add_params1, blast) |
|
487 |
done |
|
488 |
||
489 |
lemma Un_in_DPow: "[| X \<in> DPow(A); Y \<in> DPow(A) |] ==> X Un Y \<in> DPow(A)" |
|
490 |
apply (subgoal_tac "X Un Y = A - ((A-X) Int (A-Y))") |
|
491 |
apply (simp add: Int_in_DPow Compl_in_DPow) |
|
492 |
apply (simp add: DPow_def, blast) |
|
493 |
done |
|
494 |
||
495 |
lemma singleton_in_DPow: "x \<in> A ==> {x} \<in> DPow(A)" |
|
496 |
apply (simp add: DPow_def) |
|
497 |
apply (rule_tac x="Cons(x,Nil)" in bexI) |
|
498 |
apply (rule_tac x="Equal(0,1)" in bexI) |
|
499 |
apply typecheck |
|
500 |
apply (force simp add: succ_Un_distrib [symmetric]) |
|
501 |
done |
|
502 |
||
503 |
lemma cons_in_DPow: "[| a \<in> A; X \<in> DPow(A) |] ==> cons(a,X) \<in> DPow(A)" |
|
504 |
apply (rule cons_eq [THEN subst]) |
|
505 |
apply (blast intro: singleton_in_DPow Un_in_DPow) |
|
506 |
done |
|
507 |
||
508 |
(*Part of Lemma 1.3*) |
|
509 |
lemma Fin_into_DPow: "X \<in> Fin(A) ==> X \<in> DPow(A)" |
|
510 |
apply (erule Fin.induct) |
|
511 |
apply (rule empty_in_DPow) |
|
512 |
apply (blast intro: cons_in_DPow) |
|
513 |
done |
|
514 |
||
515 |
(*DPow is not monotonic. For example, let A be some non-constructible set |
|
516 |
of natural numbers, and let B be nat. Then A<=B and obviously A : DPow(A) |
|
517 |
but A ~: DPow(B).*) |
|
518 |
lemma DPow_mono: "A : DPow(B) ==> DPow(A) <= DPow(B)" |
|
519 |
apply (simp add: DPow_def, auto) |
|
520 |
(*must use the formula defining A in B to relativize the new formula...*) |
|
521 |
oops |
|
522 |
||
523 |
lemma DPow_0: "DPow(0) = {0}" |
|
524 |
by (blast intro: empty_in_DPow dest: DPow_imp_subset) |
|
525 |
||
526 |
lemma Finite_Pow_subset_Pow: "Finite(A) ==> Pow(A) <= DPow(A)" |
|
527 |
by (blast intro: Fin_into_DPow Finite_into_Fin Fin_subset) |
|
528 |
||
529 |
lemma Finite_DPow_eq_Pow: "Finite(A) ==> DPow(A) = Pow(A)" |
|
530 |
apply (rule equalityI) |
|
531 |
apply (rule DPow_subset_Pow) |
|
532 |
apply (erule Finite_Pow_subset_Pow) |
|
533 |
done |
|
534 |
||
535 |
(*This may be true but the proof looks difficult, requiring relativization |
|
536 |
lemma DPow_insert: "DPow (cons(a,A)) = DPow(A) Un {cons(a,X) . X: DPow(A)}" |
|
537 |
apply (rule equalityI, safe) |
|
538 |
oops |
|
539 |
*) |
|
540 |
||
13298 | 541 |
|
542 |
subsection{*Internalized formulas for basic concepts*} |
|
543 |
||
544 |
subsubsection{*The subset relation*} |
|
545 |
||
546 |
constdefs subset_fm :: "[i,i]=>i" |
|
547 |
"subset_fm(x,y) == Forall(Implies(Member(0,succ(x)), Member(0,succ(y))))" |
|
548 |
||
549 |
lemma subset_type [TC]: "[| x \<in> nat; y \<in> nat |] ==> subset_fm(x,y) \<in> formula" |
|
550 |
by (simp add: subset_fm_def) |
|
551 |
||
552 |
lemma arity_subset_fm [simp]: |
|
553 |
"[| x \<in> nat; y \<in> nat |] ==> arity(subset_fm(x,y)) = succ(x) \<union> succ(y)" |
|
554 |
by (simp add: subset_fm_def succ_Un_distrib [symmetric]) |
|
555 |
||
556 |
lemma sats_subset_fm [simp]: |
|
557 |
"[|x < length(env); y \<in> nat; env \<in> list(A); Transset(A)|] |
|
558 |
==> sats(A, subset_fm(x,y), env) <-> nth(x,env) \<subseteq> nth(y,env)" |
|
559 |
apply (frule lt_length_in_nat, assumption) |
|
560 |
apply (simp add: subset_fm_def Transset_def) |
|
561 |
apply (blast intro: nth_type) |
|
562 |
done |
|
563 |
||
564 |
subsubsection{*Transitive sets*} |
|
565 |
||
566 |
constdefs transset_fm :: "i=>i" |
|
567 |
"transset_fm(x) == Forall(Implies(Member(0,succ(x)), subset_fm(0,succ(x))))" |
|
568 |
||
569 |
lemma transset_type [TC]: "x \<in> nat ==> transset_fm(x) \<in> formula" |
|
570 |
by (simp add: transset_fm_def) |
|
571 |
||
572 |
lemma arity_transset_fm [simp]: |
|
573 |
"x \<in> nat ==> arity(transset_fm(x)) = succ(x)" |
|
574 |
by (simp add: transset_fm_def succ_Un_distrib [symmetric]) |
|
575 |
||
576 |
lemma sats_transset_fm [simp]: |
|
577 |
"[|x < length(env); env \<in> list(A); Transset(A)|] |
|
578 |
==> sats(A, transset_fm(x), env) <-> Transset(nth(x,env))" |
|
579 |
apply (frule lt_nat_in_nat, erule length_type) |
|
580 |
apply (simp add: transset_fm_def Transset_def) |
|
581 |
apply (blast intro: nth_type) |
|
582 |
done |
|
583 |
||
584 |
subsubsection{*Ordinals*} |
|
585 |
||
586 |
constdefs ordinal_fm :: "i=>i" |
|
587 |
"ordinal_fm(x) == |
|
588 |
And(transset_fm(x), Forall(Implies(Member(0,succ(x)), transset_fm(0))))" |
|
589 |
||
590 |
lemma ordinal_type [TC]: "x \<in> nat ==> ordinal_fm(x) \<in> formula" |
|
591 |
by (simp add: ordinal_fm_def) |
|
592 |
||
593 |
lemma arity_ordinal_fm [simp]: |
|
594 |
"x \<in> nat ==> arity(ordinal_fm(x)) = succ(x)" |
|
595 |
by (simp add: ordinal_fm_def succ_Un_distrib [symmetric]) |
|
596 |
||
13306 | 597 |
lemma sats_ordinal_fm: |
13298 | 598 |
"[|x < length(env); env \<in> list(A); Transset(A)|] |
599 |
==> sats(A, ordinal_fm(x), env) <-> Ord(nth(x,env))" |
|
600 |
apply (frule lt_nat_in_nat, erule length_type) |
|
601 |
apply (simp add: ordinal_fm_def Ord_def Transset_def) |
|
602 |
apply (blast intro: nth_type) |
|
603 |
done |
|
604 |
||
605 |
||
13223 | 606 |
subsection{* Constant Lset: Levels of the Constructible Universe *} |
607 |
||
608 |
constdefs Lset :: "i=>i" |
|
609 |
"Lset(i) == transrec(i, %x f. \<Union>y\<in>x. DPow(f`y))" |
|
610 |
||
611 |
text{*NOT SUITABLE FOR REWRITING -- RECURSIVE!*} |
|
612 |
lemma Lset: "Lset(i) = (UN j:i. DPow(Lset(j)))" |
|
613 |
by (subst Lset_def [THEN def_transrec], simp) |
|
614 |
||
615 |
lemma LsetI: "[|y\<in>x; A \<in> DPow(Lset(y))|] ==> A \<in> Lset(x)"; |
|
616 |
by (subst Lset, blast) |
|
617 |
||
618 |
lemma LsetD: "A \<in> Lset(x) ==> \<exists>y\<in>x. A \<in> DPow(Lset(y))"; |
|
619 |
apply (insert Lset [of x]) |
|
620 |
apply (blast intro: elim: equalityE) |
|
621 |
done |
|
622 |
||
623 |
subsubsection{* Transitivity *} |
|
624 |
||
625 |
lemma elem_subset_in_DPow: "[|X \<in> A; X \<subseteq> A|] ==> X \<in> DPow(A)" |
|
626 |
apply (simp add: Transset_def DPow_def) |
|
627 |
apply (rule_tac x="[X]" in bexI) |
|
628 |
apply (rule_tac x="Member(0,1)" in bexI) |
|
629 |
apply (auto simp add: Un_least_lt_iff) |
|
630 |
done |
|
631 |
||
632 |
lemma Transset_subset_DPow: "Transset(A) ==> A <= DPow(A)" |
|
633 |
apply clarify |
|
634 |
apply (simp add: Transset_def) |
|
635 |
apply (blast intro: elem_subset_in_DPow) |
|
636 |
done |
|
637 |
||
638 |
lemma Transset_DPow: "Transset(A) ==> Transset(DPow(A))" |
|
639 |
apply (simp add: Transset_def) |
|
640 |
apply (blast intro: elem_subset_in_DPow dest: DPowD) |
|
641 |
done |
|
642 |
||
643 |
text{*Kunen's VI, 1.6 (a)*} |
|
644 |
lemma Transset_Lset: "Transset(Lset(i))" |
|
645 |
apply (rule_tac a=i in eps_induct) |
|
646 |
apply (subst Lset) |
|
647 |
apply (blast intro!: Transset_Union_family Transset_Un Transset_DPow) |
|
648 |
done |
|
649 |
||
13291 | 650 |
lemma mem_Lset_imp_subset_Lset: "a \<in> Lset(i) ==> a \<subseteq> Lset(i)" |
651 |
apply (insert Transset_Lset) |
|
652 |
apply (simp add: Transset_def) |
|
653 |
done |
|
654 |
||
13223 | 655 |
subsubsection{* Monotonicity *} |
656 |
||
657 |
text{*Kunen's VI, 1.6 (b)*} |
|
658 |
lemma Lset_mono [rule_format]: |
|
659 |
"ALL j. i<=j --> Lset(i) <= Lset(j)" |
|
660 |
apply (rule_tac a=i in eps_induct) |
|
661 |
apply (rule impI [THEN allI]) |
|
662 |
apply (subst Lset) |
|
663 |
apply (subst Lset, blast) |
|
664 |
done |
|
665 |
||
666 |
text{*This version lets us remove the premise @{term "Ord(i)"} sometimes.*} |
|
667 |
lemma Lset_mono_mem [rule_format]: |
|
668 |
"ALL j. i:j --> Lset(i) <= Lset(j)" |
|
669 |
apply (rule_tac a=i in eps_induct) |
|
670 |
apply (rule impI [THEN allI]) |
|
671 |
apply (subst Lset, auto) |
|
672 |
apply (rule rev_bexI, assumption) |
|
673 |
apply (blast intro: elem_subset_in_DPow dest: LsetD DPowD) |
|
674 |
done |
|
675 |
||
13291 | 676 |
text{*Useful with Reflection to bump up the ordinal*} |
677 |
lemma subset_Lset_ltD: "[|A \<subseteq> Lset(i); i < j|] ==> A \<subseteq> Lset(j)" |
|
678 |
by (blast dest: ltD [THEN Lset_mono_mem]) |
|
679 |
||
13223 | 680 |
subsubsection{* 0, successor and limit equations fof Lset *} |
681 |
||
682 |
lemma Lset_0 [simp]: "Lset(0) = 0" |
|
683 |
by (subst Lset, blast) |
|
684 |
||
685 |
lemma Lset_succ_subset1: "DPow(Lset(i)) <= Lset(succ(i))" |
|
686 |
by (subst Lset, rule succI1 [THEN RepFunI, THEN Union_upper]) |
|
687 |
||
688 |
lemma Lset_succ_subset2: "Lset(succ(i)) <= DPow(Lset(i))" |
|
689 |
apply (subst Lset, rule UN_least) |
|
690 |
apply (erule succE) |
|
691 |
apply blast |
|
692 |
apply clarify |
|
693 |
apply (rule elem_subset_in_DPow) |
|
694 |
apply (subst Lset) |
|
695 |
apply blast |
|
696 |
apply (blast intro: dest: DPowD Lset_mono_mem) |
|
697 |
done |
|
698 |
||
699 |
lemma Lset_succ: "Lset(succ(i)) = DPow(Lset(i))" |
|
700 |
by (intro equalityI Lset_succ_subset1 Lset_succ_subset2) |
|
701 |
||
702 |
lemma Lset_Union [simp]: "Lset(\<Union>(X)) = (\<Union>y\<in>X. Lset(y))" |
|
703 |
apply (subst Lset) |
|
704 |
apply (rule equalityI) |
|
705 |
txt{*first inclusion*} |
|
706 |
apply (rule UN_least) |
|
707 |
apply (erule UnionE) |
|
708 |
apply (rule subset_trans) |
|
709 |
apply (erule_tac [2] UN_upper, subst Lset, erule UN_upper) |
|
710 |
txt{*opposite inclusion*} |
|
711 |
apply (rule UN_least) |
|
712 |
apply (subst Lset, blast) |
|
713 |
done |
|
714 |
||
715 |
subsubsection{* Lset applied to Limit ordinals *} |
|
716 |
||
717 |
lemma Limit_Lset_eq: |
|
718 |
"Limit(i) ==> Lset(i) = (\<Union>y\<in>i. Lset(y))" |
|
719 |
by (simp add: Lset_Union [symmetric] Limit_Union_eq) |
|
720 |
||
721 |
lemma lt_LsetI: "[| a: Lset(j); j<i |] ==> a : Lset(i)" |
|
722 |
by (blast dest: Lset_mono [OF le_imp_subset [OF leI]]) |
|
723 |
||
724 |
lemma Limit_LsetE: |
|
725 |
"[| a: Lset(i); ~R ==> Limit(i); |
|
726 |
!!x. [| x<i; a: Lset(x) |] ==> R |
|
727 |
|] ==> R" |
|
728 |
apply (rule classical) |
|
729 |
apply (rule Limit_Lset_eq [THEN equalityD1, THEN subsetD, THEN UN_E]) |
|
730 |
prefer 2 apply assumption |
|
731 |
apply blast |
|
732 |
apply (blast intro: ltI Limit_is_Ord) |
|
733 |
done |
|
734 |
||
735 |
subsubsection{* Basic closure properties *} |
|
736 |
||
737 |
lemma zero_in_Lset: "y:x ==> 0 : Lset(x)" |
|
738 |
by (subst Lset, blast intro: empty_in_DPow) |
|
739 |
||
740 |
lemma notin_Lset: "x \<notin> Lset(x)" |
|
741 |
apply (rule_tac a=x in eps_induct) |
|
742 |
apply (subst Lset) |
|
743 |
apply (blast dest: DPowD) |
|
744 |
done |
|
745 |
||
746 |
||
13298 | 747 |
subsection{*Constructible Ordinals: Kunen's VI, 1.9 (b)*} |
13223 | 748 |
|
749 |
text{*The subset consisting of the ordinals is definable.*} |
|
750 |
lemma Ords_in_DPow: "Transset(A) ==> {x \<in> A. Ord(x)} \<in> DPow(A)" |
|
751 |
apply (simp add: DPow_def Collect_subset) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13328
diff
changeset
|
752 |
apply (rule_tac x=Nil in bexI) |
13223 | 753 |
apply (rule_tac x="ordinal_fm(0)" in bexI) |
754 |
apply (simp_all add: sats_ordinal_fm) |
|
755 |
done |
|
756 |
||
757 |
lemma Ords_of_Lset_eq: "Ord(i) ==> {x\<in>Lset(i). Ord(x)} = i" |
|
758 |
apply (erule trans_induct3) |
|
759 |
apply (simp_all add: Lset_succ Limit_Lset_eq Limit_Union_eq) |
|
760 |
txt{*The successor case remains.*} |
|
761 |
apply (rule equalityI) |
|
762 |
txt{*First inclusion*} |
|
763 |
apply clarify |
|
764 |
apply (erule Ord_linear_lt, assumption) |
|
765 |
apply (blast dest: DPow_imp_subset ltD notE [OF notin_Lset]) |
|
766 |
apply blast |
|
767 |
apply (blast dest: ltD) |
|
768 |
txt{*Opposite inclusion, @{term "succ(x) \<subseteq> DPow(Lset(x)) \<inter> ON"}*} |
|
769 |
apply auto |
|
770 |
txt{*Key case: *} |
|
771 |
apply (erule subst, rule Ords_in_DPow [OF Transset_Lset]) |
|
772 |
apply (blast intro: elem_subset_in_DPow dest: OrdmemD elim: equalityE) |
|
773 |
apply (blast intro: Ord_in_Ord) |
|
774 |
done |
|
775 |
||
776 |
||
777 |
lemma Ord_subset_Lset: "Ord(i) ==> i \<subseteq> Lset(i)" |
|
778 |
by (subst Ords_of_Lset_eq [symmetric], assumption, fast) |
|
779 |
||
780 |
lemma Ord_in_Lset: "Ord(i) ==> i \<in> Lset(succ(i))" |
|
781 |
apply (simp add: Lset_succ) |
|
782 |
apply (subst Ords_of_Lset_eq [symmetric], assumption, |
|
783 |
rule Ords_in_DPow [OF Transset_Lset]) |
|
784 |
done |
|
785 |
||
786 |
subsubsection{* Unions *} |
|
787 |
||
788 |
lemma Union_in_Lset: |
|
789 |
"X \<in> Lset(j) ==> Union(X) \<in> Lset(succ(j))" |
|
790 |
apply (insert Transset_Lset) |
|
791 |
apply (rule LsetI [OF succI1]) |
|
792 |
apply (simp add: Transset_def DPow_def) |
|
793 |
apply (intro conjI, blast) |
|
794 |
txt{*Now to create the formula @{term "\<exists>y. y \<in> X \<and> x \<in> y"} *} |
|
795 |
apply (rule_tac x="Cons(X,Nil)" in bexI) |
|
796 |
apply (rule_tac x="Exists(And(Member(0,2), Member(1,0)))" in bexI) |
|
797 |
apply typecheck |
|
798 |
apply (simp add: succ_Un_distrib [symmetric], blast) |
|
799 |
done |
|
800 |
||
801 |
lemma Union_in_LLimit: |
|
802 |
"[| X: Lset(i); Limit(i) |] ==> Union(X) : Lset(i)" |
|
803 |
apply (rule Limit_LsetE, assumption+) |
|
804 |
apply (blast intro: Limit_has_succ lt_LsetI Union_in_Lset) |
|
805 |
done |
|
806 |
||
807 |
subsubsection{* Finite sets and ordered pairs *} |
|
808 |
||
809 |
lemma singleton_in_Lset: "a: Lset(i) ==> {a} : Lset(succ(i))" |
|
810 |
by (simp add: Lset_succ singleton_in_DPow) |
|
811 |
||
812 |
lemma doubleton_in_Lset: |
|
813 |
"[| a: Lset(i); b: Lset(i) |] ==> {a,b} : Lset(succ(i))" |
|
814 |
by (simp add: Lset_succ empty_in_DPow cons_in_DPow) |
|
815 |
||
816 |
lemma Pair_in_Lset: |
|
817 |
"[| a: Lset(i); b: Lset(i); Ord(i) |] ==> <a,b> : Lset(succ(succ(i)))" |
|
818 |
apply (unfold Pair_def) |
|
819 |
apply (blast intro: doubleton_in_Lset) |
|
820 |
done |
|
821 |
||
822 |
lemmas zero_in_LLimit = Limit_has_0 [THEN ltD, THEN zero_in_Lset, standard] |
|
823 |
||
824 |
lemma singleton_in_LLimit: |
|
825 |
"[| a: Lset(i); Limit(i) |] ==> {a} : Lset(i)" |
|
826 |
apply (erule Limit_LsetE, assumption) |
|
827 |
apply (erule singleton_in_Lset [THEN lt_LsetI]) |
|
828 |
apply (blast intro: Limit_has_succ) |
|
829 |
done |
|
830 |
||
831 |
lemmas Lset_UnI1 = Un_upper1 [THEN Lset_mono [THEN subsetD], standard] |
|
832 |
lemmas Lset_UnI2 = Un_upper2 [THEN Lset_mono [THEN subsetD], standard] |
|
833 |
||
834 |
text{*Hard work is finding a single j:i such that {a,b}<=Lset(j)*} |
|
835 |
lemma doubleton_in_LLimit: |
|
836 |
"[| a: Lset(i); b: Lset(i); Limit(i) |] ==> {a,b} : Lset(i)" |
|
837 |
apply (erule Limit_LsetE, assumption) |
|
838 |
apply (erule Limit_LsetE, assumption) |
|
13269 | 839 |
apply (blast intro: lt_LsetI [OF doubleton_in_Lset] |
840 |
Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt) |
|
13223 | 841 |
done |
842 |
||
843 |
lemma Pair_in_LLimit: |
|
844 |
"[| a: Lset(i); b: Lset(i); Limit(i) |] ==> <a,b> : Lset(i)" |
|
845 |
txt{*Infer that a, b occur at ordinals x,xa < i.*} |
|
846 |
apply (erule Limit_LsetE, assumption) |
|
847 |
apply (erule Limit_LsetE, assumption) |
|
848 |
txt{*Infer that succ(succ(x Un xa)) < i *} |
|
849 |
apply (blast intro: lt_Ord lt_LsetI [OF Pair_in_Lset] |
|
850 |
Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt) |
|
851 |
done |
|
852 |
||
853 |
lemma product_LLimit: "Limit(i) ==> Lset(i) * Lset(i) <= Lset(i)" |
|
854 |
by (blast intro: Pair_in_LLimit) |
|
855 |
||
856 |
lemmas Sigma_subset_LLimit = subset_trans [OF Sigma_mono product_LLimit] |
|
857 |
||
858 |
lemma nat_subset_LLimit: "Limit(i) ==> nat \<subseteq> Lset(i)" |
|
859 |
by (blast dest: Ord_subset_Lset nat_le_Limit le_imp_subset Limit_is_Ord) |
|
860 |
||
861 |
lemma nat_into_LLimit: "[| n: nat; Limit(i) |] ==> n : Lset(i)" |
|
862 |
by (blast intro: nat_subset_LLimit [THEN subsetD]) |
|
863 |
||
864 |
||
865 |
subsubsection{* Closure under disjoint union *} |
|
866 |
||
867 |
lemmas zero_in_LLimit = Limit_has_0 [THEN ltD, THEN zero_in_Lset, standard] |
|
868 |
||
869 |
lemma one_in_LLimit: "Limit(i) ==> 1 : Lset(i)" |
|
870 |
by (blast intro: nat_into_LLimit) |
|
871 |
||
872 |
lemma Inl_in_LLimit: |
|
873 |
"[| a: Lset(i); Limit(i) |] ==> Inl(a) : Lset(i)" |
|
874 |
apply (unfold Inl_def) |
|
875 |
apply (blast intro: zero_in_LLimit Pair_in_LLimit) |
|
876 |
done |
|
877 |
||
878 |
lemma Inr_in_LLimit: |
|
879 |
"[| b: Lset(i); Limit(i) |] ==> Inr(b) : Lset(i)" |
|
880 |
apply (unfold Inr_def) |
|
881 |
apply (blast intro: one_in_LLimit Pair_in_LLimit) |
|
882 |
done |
|
883 |
||
884 |
lemma sum_LLimit: "Limit(i) ==> Lset(i) + Lset(i) <= Lset(i)" |
|
885 |
by (blast intro!: Inl_in_LLimit Inr_in_LLimit) |
|
886 |
||
887 |
lemmas sum_subset_LLimit = subset_trans [OF sum_mono sum_LLimit] |
|
888 |
||
889 |
||
890 |
text{*The constructible universe and its rank function*} |
|
891 |
constdefs |
|
892 |
L :: "i=>o" --{*Kunen's definition VI, 1.5, page 167*} |
|
893 |
"L(x) == \<exists>i. Ord(i) & x \<in> Lset(i)" |
|
894 |
||
895 |
lrank :: "i=>i" --{*Kunen's definition VI, 1.7*} |
|
896 |
"lrank(x) == \<mu>i. x \<in> Lset(succ(i))" |
|
897 |
||
898 |
lemma L_I: "[|x \<in> Lset(i); Ord(i)|] ==> L(x)" |
|
899 |
by (simp add: L_def, blast) |
|
900 |
||
901 |
lemma L_D: "L(x) ==> \<exists>i. Ord(i) & x \<in> Lset(i)" |
|
902 |
by (simp add: L_def) |
|
903 |
||
904 |
lemma Ord_lrank [simp]: "Ord(lrank(a))" |
|
905 |
by (simp add: lrank_def) |
|
906 |
||
907 |
lemma Lset_lrank_lt [rule_format]: "Ord(i) ==> x \<in> Lset(i) --> lrank(x) < i" |
|
908 |
apply (erule trans_induct3) |
|
909 |
apply simp |
|
910 |
apply (simp only: lrank_def) |
|
911 |
apply (blast intro: Least_le) |
|
912 |
apply (simp_all add: Limit_Lset_eq) |
|
913 |
apply (blast intro: ltI Limit_is_Ord lt_trans) |
|
914 |
done |
|
915 |
||
916 |
text{*Kunen's VI, 1.8, and the proof is much less trivial than the text |
|
917 |
would suggest. For a start it need the previous lemma, proved by induction.*} |
|
918 |
lemma Lset_iff_lrank_lt: "Ord(i) ==> x \<in> Lset(i) <-> L(x) & lrank(x) < i" |
|
919 |
apply (simp add: L_def, auto) |
|
920 |
apply (blast intro: Lset_lrank_lt) |
|
921 |
apply (unfold lrank_def) |
|
922 |
apply (drule succI1 [THEN Lset_mono_mem, THEN subsetD]) |
|
923 |
apply (drule_tac P="\<lambda>i. x \<in> Lset(succ(i))" in LeastI, assumption) |
|
924 |
apply (blast intro!: le_imp_subset Lset_mono [THEN subsetD]) |
|
925 |
done |
|
926 |
||
927 |
lemma Lset_succ_lrank_iff [simp]: "x \<in> Lset(succ(lrank(x))) <-> L(x)" |
|
928 |
by (simp add: Lset_iff_lrank_lt) |
|
929 |
||
930 |
text{*Kunen's VI, 1.9 (a)*} |
|
931 |
lemma lrank_of_Ord: "Ord(i) ==> lrank(i) = i" |
|
932 |
apply (unfold lrank_def) |
|
933 |
apply (rule Least_equality) |
|
934 |
apply (erule Ord_in_Lset) |
|
935 |
apply assumption |
|
936 |
apply (insert notin_Lset [of i]) |
|
937 |
apply (blast intro!: le_imp_subset Lset_mono [THEN subsetD]) |
|
938 |
done |
|
939 |
||
13245 | 940 |
|
941 |
lemma Ord_in_L: "Ord(i) ==> L(i)" |
|
942 |
by (blast intro: Ord_in_Lset L_I) |
|
943 |
||
13223 | 944 |
text{*This is lrank(lrank(a)) = lrank(a) *} |
945 |
declare Ord_lrank [THEN lrank_of_Ord, simp] |
|
946 |
||
947 |
text{*Kunen's VI, 1.10 *} |
|
948 |
lemma Lset_in_Lset_succ: "Lset(i) \<in> Lset(succ(i))"; |
|
949 |
apply (simp add: Lset_succ DPow_def) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13328
diff
changeset
|
950 |
apply (rule_tac x=Nil in bexI) |
13223 | 951 |
apply (rule_tac x="Equal(0,0)" in bexI) |
952 |
apply auto |
|
953 |
done |
|
954 |
||
955 |
lemma lrank_Lset: "Ord(i) ==> lrank(Lset(i)) = i" |
|
956 |
apply (unfold lrank_def) |
|
957 |
apply (rule Least_equality) |
|
958 |
apply (rule Lset_in_Lset_succ) |
|
959 |
apply assumption |
|
960 |
apply clarify |
|
961 |
apply (subgoal_tac "Lset(succ(ia)) <= Lset(i)") |
|
962 |
apply (blast dest: mem_irrefl) |
|
963 |
apply (blast intro!: le_imp_subset Lset_mono) |
|
964 |
done |
|
965 |
||
966 |
text{*Kunen's VI, 1.11 *} |
|
967 |
lemma Lset_subset_Vset: "Ord(i) ==> Lset(i) <= Vset(i)"; |
|
968 |
apply (erule trans_induct) |
|
969 |
apply (subst Lset) |
|
970 |
apply (subst Vset) |
|
971 |
apply (rule UN_mono [OF subset_refl]) |
|
972 |
apply (rule subset_trans [OF DPow_subset_Pow]) |
|
973 |
apply (rule Pow_mono, blast) |
|
974 |
done |
|
975 |
||
976 |
text{*Kunen's VI, 1.12 *} |
|
977 |
lemma Lset_subset_Vset: "i \<in> nat ==> Lset(i) = Vset(i)"; |
|
978 |
apply (erule nat_induct) |
|
979 |
apply (simp add: Vfrom_0) |
|
980 |
apply (simp add: Lset_succ Vset_succ Finite_Vset Finite_DPow_eq_Pow) |
|
981 |
done |
|
982 |
||
13291 | 983 |
text{*Every set of constructible sets is included in some @{term Lset}*} |
984 |
lemma subset_Lset: |
|
985 |
"(\<forall>x\<in>A. L(x)) ==> \<exists>i. Ord(i) & A \<subseteq> Lset(i)" |
|
986 |
by (rule_tac x = "\<Union>x\<in>A. succ(lrank(x))" in exI, force) |
|
987 |
||
988 |
lemma subset_LsetE: |
|
989 |
"[|\<forall>x\<in>A. L(x); |
|
990 |
!!i. [|Ord(i); A \<subseteq> Lset(i)|] ==> P|] |
|
991 |
==> P" |
|
992 |
by (blast dest: subset_Lset) |
|
993 |
||
13223 | 994 |
subsection{*For L to satisfy the ZF axioms*} |
995 |
||
13245 | 996 |
theorem Union_in_L: "L(X) ==> L(Union(X))" |
13223 | 997 |
apply (simp add: L_def, clarify) |
998 |
apply (drule Ord_imp_greater_Limit) |
|
999 |
apply (blast intro: lt_LsetI Union_in_LLimit Limit_is_Ord) |
|
1000 |
done |
|
1001 |
||
13245 | 1002 |
theorem doubleton_in_L: "[| L(a); L(b) |] ==> L({a, b})" |
13223 | 1003 |
apply (simp add: L_def, clarify) |
1004 |
apply (drule Ord2_imp_greater_Limit, assumption) |
|
1005 |
apply (blast intro: lt_LsetI doubleton_in_LLimit Limit_is_Ord) |
|
1006 |
done |
|
1007 |
||
1008 |
subsubsection{*For L to satisfy Powerset *} |
|
1009 |
||
1010 |
lemma LPow_env_typing: |
|
13511 | 1011 |
"[| y : Lset(i); Ord(i); y \<subseteq> X |] |
1012 |
==> \<exists>z \<in> Pow(X). y \<in> Lset(succ(lrank(z)))" |
|
13223 | 1013 |
by (auto intro: L_I iff: Lset_succ_lrank_iff) |
1014 |
||
1015 |
lemma LPow_in_Lset: |
|
1016 |
"[|X \<in> Lset(i); Ord(i)|] ==> \<exists>j. Ord(j) & {y \<in> Pow(X). L(y)} \<in> Lset(j)" |
|
1017 |
apply (rule_tac x="succ(\<Union>y \<in> Pow(X). succ(lrank(y)))" in exI) |
|
1018 |
apply simp |
|
1019 |
apply (rule LsetI [OF succI1]) |
|
1020 |
apply (simp add: DPow_def) |
|
1021 |
apply (intro conjI, clarify) |
|
13511 | 1022 |
apply (rule_tac a=x in UN_I, simp+) |
13223 | 1023 |
txt{*Now to create the formula @{term "y \<subseteq> X"} *} |
1024 |
apply (rule_tac x="Cons(X,Nil)" in bexI) |
|
1025 |
apply (rule_tac x="subset_fm(0,1)" in bexI) |
|
1026 |
apply typecheck |
|
13511 | 1027 |
apply (rule conjI) |
13223 | 1028 |
apply (simp add: succ_Un_distrib [symmetric]) |
1029 |
apply (rule equality_iffI) |
|
13511 | 1030 |
apply (simp add: Transset_UN [OF Transset_Lset] LPow_env_typing) |
13223 | 1031 |
apply (auto intro: L_I iff: Lset_succ_lrank_iff) |
1032 |
done |
|
1033 |
||
13245 | 1034 |
theorem LPow_in_L: "L(X) ==> L({y \<in> Pow(X). L(y)})" |
13223 | 1035 |
by (blast intro: L_I dest: L_D LPow_in_Lset) |
1036 |
||
13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1037 |
|
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1038 |
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
|
1039 |
|
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1040 |
|
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1041 |
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
|
1042 |
by (induct_tac n, auto) |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1043 |
|
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1044 |
lemma sats_app_0_iff [rule_format]: |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1045 |
"[| p \<in> formula; 0 \<in> A |] |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1046 |
==> \<forall>env \<in> list(A). sats(A,p, env@[0]) <-> sats(A,p,env)" |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1047 |
apply (induct_tac p) |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1048 |
apply (simp_all del: app_Cons add: app_Cons [symmetric] |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1049 |
add: nth_zero_eq_0 nth_append not_lt_iff_le nth_eq_0) |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1050 |
done |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1051 |
|
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1052 |
lemma sats_app_zeroes_iff: |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1053 |
"[| p \<in> formula; 0 \<in> A; env \<in> list(A); n \<in> nat |] |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1054 |
==> sats(A,p,env @ repeat(0,n)) <-> sats(A,p,env)" |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1055 |
apply (induct_tac n, simp) |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1056 |
apply (simp del: repeat.simps |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1057 |
add: repeat_succ_app sats_app_0_iff app_assoc [symmetric]) |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1058 |
done |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1059 |
|
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1060 |
lemma exists_bigger_env: |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1061 |
"[| p \<in> formula; 0 \<in> A; env \<in> list(A) |] |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1062 |
==> \<exists>env' \<in> list(A). arity(p) \<le> succ(length(env')) & |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1063 |
(\<forall>a\<in>A. sats(A,p,Cons(a,env')) <-> sats(A,p,Cons(a,env)))" |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1064 |
apply (rule_tac x="env @ repeat(0,arity(p))" in bexI) |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1065 |
apply (simp del: app_Cons add: app_Cons [symmetric] |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1066 |
add: length_repeat sats_app_zeroes_iff, typecheck) |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1067 |
done |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1068 |
|
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1069 |
|
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1070 |
text{*A simpler version of @{term DPow}: no arity check!*} |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1071 |
constdefs DPow' :: "i => i" |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1072 |
"DPow'(A) == {X \<in> Pow(A). |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1073 |
\<exists>env \<in> list(A). \<exists>p \<in> formula. |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1074 |
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
|
1075 |
|
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1076 |
lemma DPow_subset_DPow': "DPow(A) <= DPow'(A)"; |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1077 |
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
|
1078 |
|
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1079 |
lemma DPow'_0: "DPow'(0) = {0}" |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1080 |
by (auto simp add: DPow'_def) |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1081 |
|
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1082 |
lemma DPow'_subset_DPow: "0 \<in> A ==> DPow'(A) \<subseteq> DPow(A)" |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1083 |
apply (auto simp add: DPow'_def DPow_def) |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1084 |
apply (frule exists_bigger_env, assumption+, force) |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1085 |
done |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1086 |
|
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1087 |
lemma DPow_eq_DPow': "Transset(A) ==> DPow(A) = DPow'(A)" |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1088 |
apply (drule Transset_0_disj) |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1089 |
apply (erule disjE) |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1090 |
apply (simp add: DPow'_0 DPow_0) |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1091 |
apply (rule equalityI) |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1092 |
apply (rule DPow_subset_DPow') |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1093 |
apply (erule DPow'_subset_DPow) |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1094 |
done |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1095 |
|
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1096 |
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
|
1097 |
@{term arity} and @{term length}*} |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1098 |
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
|
1099 |
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
|
1100 |
apply (subst Lset) |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1101 |
apply (subst transrec) |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1102 |
apply (simp only: DPow_eq_DPow' [OF Transset_Lset], simp) |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1103 |
done |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1104 |
|
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1105 |
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
|
1106 |
arities at all!*} |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1107 |
lemma DPow_LsetI [rule_format]: |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1108 |
"[|\<forall>x\<in>Lset(i). P(x) <-> sats(Lset(i), p, Cons(x,env)); |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1109 |
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
|
1110 |
==> {x\<in>Lset(i). P(x)} \<in> DPow(Lset(i))" |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1111 |
by (simp add: DPow_eq_DPow' [OF Transset_Lset] DPow'_def, blast) |
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13339
diff
changeset
|
1112 |
|
13223 | 1113 |
end |