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