author | paulson |
Fri, 28 Jun 2002 11:25:46 +0200 | |
changeset 13254 | 5146ccaedf42 |
parent 13251 | 74cb2af8811e |
child 13268 | 240509babf00 |
permissions | -rw-r--r-- |
13223 | 1 |
theory WFrec = Wellorderings: |
2 |
||
3 |
||
13254 | 4 |
(*Many of these might be useful in WF.thy*) |
13223 | 5 |
|
6 |
lemma is_recfunI: |
|
7 |
"f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))) ==> is_recfun(r,a,H,f)" |
|
8 |
by (simp add: is_recfun_def) |
|
9 |
||
10 |
lemma is_recfun_imp_function: "is_recfun(r,a,H,f) ==> function(f)" |
|
11 |
apply (simp add: is_recfun_def) |
|
12 |
apply (erule ssubst) |
|
13 |
apply (rule function_lam) |
|
14 |
done |
|
15 |
||
16 |
text{*Expresses @{text is_recfun} as a recursion equation*} |
|
17 |
lemma is_recfun_iff_equation: |
|
18 |
"is_recfun(r,a,H,f) <-> |
|
19 |
f \<in> r -`` {a} \<rightarrow> range(f) & |
|
20 |
(\<forall>x \<in> r-``{a}. f`x = H(x, restrict(f, r-``{x})))" |
|
21 |
apply (rule iffI) |
|
22 |
apply (simp add: is_recfun_type apply_recfun Ball_def vimage_singleton_iff, |
|
23 |
clarify) |
|
24 |
apply (simp add: is_recfun_def) |
|
25 |
apply (rule fun_extension) |
|
26 |
apply assumption |
|
27 |
apply (fast intro: lam_type, simp) |
|
28 |
done |
|
29 |
||
13245 | 30 |
lemma is_recfun_imp_in_r: "[|is_recfun(r,a,H,f); \<langle>x,i\<rangle> \<in> f|] ==> \<langle>x, a\<rangle> \<in> r" |
31 |
by (blast dest: is_recfun_type fun_is_rel) |
|
32 |
||
33 |
lemma apply_recfun2: |
|
34 |
"[| is_recfun(r,a,H,f); <x,i>:f |] ==> i = H(x, restrict(f,r-``{x}))" |
|
35 |
apply (frule apply_recfun) |
|
36 |
apply (blast dest: is_recfun_type fun_is_rel) |
|
37 |
apply (simp add: function_apply_equality [OF _ is_recfun_imp_function]) |
|
38 |
done |
|
39 |
||
13254 | 40 |
lemma trans_Int_eq: |
41 |
"[| trans(r); <y,x> \<in> r |] ==> r -`` {x} \<inter> r -`` {y} = r -`` {y}" |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
42 |
by (blast intro: transD) |
13223 | 43 |
|
13254 | 44 |
lemma is_recfun_restrict_idem: |
45 |
"is_recfun(r,a,H,f) ==> restrict(f, r -`` {a}) = f" |
|
46 |
apply (drule is_recfun_type) |
|
47 |
apply (auto simp add: Pi_iff subset_Sigma_imp_relation restrict_idem) |
|
48 |
done |
|
49 |
||
50 |
lemma is_recfun_cong_lemma: |
|
51 |
"[| is_recfun(r,a,H,f); r = r'; a = a'; f = f'; |
|
52 |
!!x g. [| <x,a'> \<in> r'; relation(g); domain(g) <= r' -``{x} |] |
|
53 |
==> H(x,g) = H'(x,g) |] |
|
54 |
==> is_recfun(r',a',H',f')" |
|
55 |
apply (simp add: is_recfun_def) |
|
56 |
apply (erule trans) |
|
57 |
apply (rule lam_cong) |
|
58 |
apply (simp_all add: vimage_singleton_iff Int_lower2) |
|
59 |
done |
|
60 |
||
61 |
text{*For @{text is_recfun} we need only pay attention to functions |
|
62 |
whose domains are initial segments of @{term r}.*} |
|
63 |
lemma is_recfun_cong: |
|
64 |
"[| r = r'; a = a'; f = f'; |
|
65 |
!!x g. [| <x,a'> \<in> r'; relation(g); domain(g) <= r' -``{x} |] |
|
66 |
==> H(x,g) = H'(x,g) |] |
|
67 |
==> is_recfun(r,a,H,f) <-> is_recfun(r',a',H',f')" |
|
68 |
apply (rule iffI) |
|
69 |
txt{*Messy: fast and blast don't work for some reason*} |
|
70 |
apply (erule is_recfun_cong_lemma, auto) |
|
71 |
apply (erule is_recfun_cong_lemma) |
|
72 |
apply (blast intro: sym)+ |
|
73 |
done |
|
13223 | 74 |
|
75 |
||
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
76 |
text{*Stated using @{term "trans(r)"} rather than |
13223 | 77 |
@{term "transitive_rel(M,A,r)"} because the latter rewrites to |
78 |
the former anyway, by @{text transitive_rel_abs}. |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
79 |
As always, theorems should be expressed in simplified form. |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
80 |
The last three M-premises are redundant because of @{term "M(r)"}, |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
81 |
but without them we'd have to undertake |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
82 |
more work to set up the induction formula.*} |
13223 | 83 |
lemma (in M_axioms) is_recfun_equal [rule_format]: |
84 |
"[|is_recfun(r,a,H,f); is_recfun(r,b,H,g); |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
85 |
wellfounded(M,r); trans(r); |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
86 |
M(f); M(g); M(r); M(x); M(a); M(b) |] |
13223 | 87 |
==> <x,a> \<in> r --> <x,b> \<in> r --> f`x=g`x" |
88 |
apply (frule_tac f="f" in is_recfun_type) |
|
89 |
apply (frule_tac f="g" in is_recfun_type) |
|
90 |
apply (simp add: is_recfun_def) |
|
13254 | 91 |
apply (erule_tac a=x in wellfounded_induct, assumption+) |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
92 |
txt{*Separation to justify the induction*} |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
93 |
apply (force intro: is_recfun_separation) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
94 |
txt{*Now the inductive argument itself*} |
13254 | 95 |
apply clarify |
13223 | 96 |
apply (erule ssubst)+ |
97 |
apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def) |
|
98 |
apply (rename_tac x1) |
|
99 |
apply (rule_tac t="%z. H(x1,z)" in subst_context) |
|
100 |
apply (subgoal_tac "ALL y : r-``{x1}. ALL z. <y,z>:f <-> <y,z>:g") |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
101 |
apply (blast intro: transD) |
13223 | 102 |
apply (simp add: apply_iff) |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
103 |
apply (blast intro: transD sym) |
13223 | 104 |
done |
105 |
||
106 |
lemma (in M_axioms) is_recfun_cut: |
|
107 |
"[|is_recfun(r,a,H,f); is_recfun(r,b,H,g); |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
108 |
wellfounded(M,r); trans(r); |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
109 |
M(f); M(g); M(r); <b,a> \<in> r |] |
13223 | 110 |
==> restrict(f, r-``{b}) = g" |
111 |
apply (frule_tac f="f" in is_recfun_type) |
|
112 |
apply (rule fun_extension) |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
113 |
apply (blast intro: transD restrict_type2) |
13223 | 114 |
apply (erule is_recfun_type, simp) |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
115 |
apply (blast intro: is_recfun_equal transD dest: transM) |
13223 | 116 |
done |
117 |
||
118 |
lemma (in M_axioms) is_recfun_functional: |
|
119 |
"[|is_recfun(r,a,H,f); is_recfun(r,a,H,g); |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
120 |
wellfounded(M,r); trans(r); |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
121 |
M(f); M(g); M(r) |] |
13223 | 122 |
==> f=g" |
123 |
apply (rule fun_extension) |
|
124 |
apply (erule is_recfun_type)+ |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
125 |
apply (blast intro!: is_recfun_equal dest: transM) |
13254 | 126 |
done |
13223 | 127 |
|
128 |
text{*Tells us that is_recfun can (in principle) be relativized.*} |
|
129 |
lemma (in M_axioms) is_recfun_relativize: |
|
13254 | 130 |
"[| M(r); M(f); \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
131 |
==> is_recfun(r,a,H,f) <-> |
13254 | 132 |
(\<forall>z[M]. z \<in> f <-> |
133 |
(\<exists>x[M]. <x,a> \<in> r & z = <x, H(x, restrict(f, r-``{x}))>))"; |
|
134 |
apply (simp add: is_recfun_def lam_def) |
|
13223 | 135 |
apply (safe intro!: equalityI) |
13254 | 136 |
apply (drule equalityD1 [THEN subsetD], assumption) |
137 |
apply (blast dest: pair_components_in_M) |
|
138 |
apply (blast elim!: equalityE dest: pair_components_in_M) |
|
139 |
apply (frule transM, assumption, rotate_tac -1) |
|
13223 | 140 |
apply simp |
141 |
apply blast |
|
13254 | 142 |
apply (subgoal_tac "is_function(M,f)") |
143 |
txt{*We use @{term "is_function"} rather than @{term "function"} because |
|
144 |
the subgoal's easier to prove with relativized quantifiers!*} |
|
145 |
prefer 2 apply (simp add: is_function_def) |
|
13223 | 146 |
apply (frule pair_components_in_M, assumption) |
13254 | 147 |
apply (simp add: is_recfun_imp_function function_restrictI) |
13223 | 148 |
done |
149 |
||
150 |
(* ideas for further weaking the H-closure premise: |
|
151 |
apply (drule spec [THEN spec]) |
|
152 |
apply (erule mp) |
|
153 |
apply (intro conjI) |
|
154 |
apply (blast dest!: pair_components_in_M) |
|
155 |
apply (blast intro!: function_restrictI dest!: pair_components_in_M) |
|
156 |
apply (blast intro!: function_restrictI dest!: pair_components_in_M) |
|
157 |
apply (simp only: subset_iff domain_iff restrict_iff vimage_iff) |
|
158 |
apply (simp add: vimage_singleton_iff) |
|
159 |
apply (intro allI impI conjI) |
|
160 |
apply (blast intro: transM dest!: pair_components_in_M) |
|
161 |
prefer 4;apply blast |
|
162 |
*) |
|
163 |
||
164 |
lemma (in M_axioms) is_recfun_restrict: |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
165 |
"[| wellfounded(M,r); trans(r); is_recfun(r,x,H,f); \<langle>y,x\<rangle> \<in> r; |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
166 |
M(r); M(f); |
13254 | 167 |
\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] |
13223 | 168 |
==> is_recfun(r, y, H, restrict(f, r -`` {y}))" |
169 |
apply (frule pair_components_in_M, assumption, clarify) |
|
13254 | 170 |
apply (simp (no_asm_simp) add: is_recfun_relativize restrict_iff |
171 |
trans_Int_eq) |
|
13223 | 172 |
apply safe |
173 |
apply (simp_all add: vimage_singleton_iff is_recfun_type [THEN apply_iff]) |
|
174 |
apply (frule_tac x=xa in pair_components_in_M, assumption) |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
175 |
apply (frule_tac x=xa in apply_recfun, blast intro: transD) |
13247 | 176 |
apply (simp add: is_recfun_type [THEN apply_iff] |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
177 |
is_recfun_imp_function function_restrictI) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
178 |
apply (blast intro: apply_recfun dest: transD) |
13223 | 179 |
done |
180 |
||
181 |
lemma (in M_axioms) restrict_Y_lemma: |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
182 |
"[| wellfounded(M,r); trans(r); M(r); |
13254 | 183 |
\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)); M(Y); |
13223 | 184 |
\<forall>b. M(b) --> |
185 |
b \<in> Y <-> |
|
186 |
(\<exists>x\<in>r -`` {a1}. |
|
187 |
\<exists>y. M(y) \<and> |
|
188 |
(\<exists>g. M(g) \<and> b = \<langle>x,y\<rangle> \<and> is_recfun(r,x,H,g) \<and> y = H(x,g))); |
|
189 |
\<langle>x,a1\<rangle> \<in> r; M(f); is_recfun(r,x,H,f) |] |
|
190 |
==> restrict(Y, r -`` {x}) = f" |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
191 |
apply (subgoal_tac "\<forall>y \<in> r-``{x}. \<forall>z. <y,z>:Y <-> <y,z>:f") |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
192 |
apply (simp (no_asm_simp) add: restrict_def) |
13254 | 193 |
apply (thin_tac "rall(M,?P)")+ --{*essential for efficiency*} |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
194 |
apply (thin_tac "All(?P)")+ --{*essential for efficiency*} |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
195 |
apply (frule is_recfun_type [THEN fun_is_rel], blast) |
13223 | 196 |
apply (frule pair_components_in_M, assumption, clarify) |
197 |
apply (rule iffI) |
|
198 |
apply (frule_tac y="<y,z>" in transM, assumption ) |
|
199 |
apply (rotate_tac -1) |
|
200 |
apply (clarsimp simp add: vimage_singleton_iff is_recfun_type [THEN apply_iff] |
|
201 |
apply_recfun is_recfun_cut) |
|
202 |
txt{*Opposite inclusion: something in f, show in Y*} |
|
203 |
apply (frule_tac y="<y,z>" in transM, assumption, simp) |
|
204 |
apply (rule_tac x=y in bexI) |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
205 |
prefer 2 apply (blast dest: transD) |
13223 | 206 |
apply (rule_tac x=z in exI, simp) |
207 |
apply (rule_tac x="restrict(f, r -`` {y})" in exI) |
|
208 |
apply (simp add: vimage_closed restrict_closed is_recfun_restrict |
|
209 |
apply_recfun is_recfun_type [THEN apply_iff]) |
|
210 |
done |
|
211 |
||
13245 | 212 |
text{*For typical applications of Replacement for recursive definitions*} |
213 |
lemma (in M_axioms) univalent_is_recfun: |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
214 |
"[|wellfounded(M,r); trans(r); M(r)|] |
13245 | 215 |
==> univalent (M, A, \<lambda>x p. \<exists>y. M(y) & |
216 |
(\<exists>f. M(f) & p = \<langle>x, y\<rangle> & is_recfun(r,x,H,f) & y = H(x,f)))" |
|
217 |
apply (simp add: univalent_def) |
|
218 |
apply (blast dest: is_recfun_functional) |
|
219 |
done |
|
220 |
||
13223 | 221 |
text{*Proof of the inductive step for @{text exists_is_recfun}, since |
222 |
we must prove two versions.*} |
|
223 |
lemma (in M_axioms) exists_is_recfun_indstep: |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
224 |
"[|\<forall>y. \<langle>y, a1\<rangle> \<in> r --> (\<exists>f. M(f) & is_recfun(r, y, H, f)); |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
225 |
wellfounded(M,r); trans(r); M(r); M(a1); |
13223 | 226 |
strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) & |
227 |
pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); |
|
13254 | 228 |
\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] |
13223 | 229 |
==> \<exists>f. M(f) & is_recfun(r,a1,H,f)" |
230 |
apply (drule_tac A="r-``{a1}" in strong_replacementD) |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
231 |
apply blast |
13223 | 232 |
txt{*Discharge the "univalent" obligation of Replacement*} |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
233 |
apply (simp add: univalent_is_recfun) |
13223 | 234 |
txt{*Show that the constructed object satisfies @{text is_recfun}*} |
235 |
apply clarify |
|
236 |
apply (rule_tac x=Y in exI) |
|
13254 | 237 |
txt{*Unfold only the top-level occurrence of @{term is_recfun}*} |
238 |
apply (simp (no_asm_simp) add: is_recfun_relativize [of concl: _ a1]) |
|
239 |
txt{*The big iff-formula defininng @{term Y} is now redundant*} |
|
240 |
apply safe |
|
241 |
apply (simp add: vimage_singleton_iff restrict_Y_lemma [of r H]) |
|
13223 | 242 |
txt{*one more case*} |
13254 | 243 |
apply (simp (no_asm_simp) add: Bex_def vimage_singleton_iff) |
244 |
apply (rename_tac x) |
|
245 |
apply (rule_tac x=x in exI, simp) |
|
13223 | 246 |
apply (rule_tac x="H(x, restrict(Y, r -`` {x}))" in exI) |
247 |
apply (drule_tac x1=x in spec [THEN mp], assumption, clarify) |
|
248 |
apply (rule_tac x=f in exI) |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
249 |
apply (simp add: restrict_Y_lemma [of r H]) |
13223 | 250 |
done |
251 |
||
252 |
text{*Relativized version, when we have the (currently weaker) premise |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
253 |
@{term "wellfounded(M,r)"}*} |
13223 | 254 |
lemma (in M_axioms) wellfounded_exists_is_recfun: |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
255 |
"[|wellfounded(M,r); trans(r); |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
256 |
separation(M, \<lambda>x. ~ (\<exists>f. M(f) \<and> is_recfun(r, x, H, f))); |
13223 | 257 |
strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) & |
258 |
pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
259 |
M(r); M(a); |
13254 | 260 |
\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] |
13223 | 261 |
==> \<exists>f. M(f) & is_recfun(r,a,H,f)" |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
262 |
apply (rule wellfounded_induct, assumption+, clarify) |
13223 | 263 |
apply (rule exists_is_recfun_indstep, assumption+) |
264 |
done |
|
265 |
||
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
266 |
lemma (in M_axioms) wf_exists_is_recfun [rule_format]: |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
267 |
"[|wf(r); trans(r); |
13223 | 268 |
strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) & |
269 |
pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
270 |
M(r); |
13254 | 271 |
\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
272 |
==> M(a) --> (\<exists>f. M(f) & is_recfun(r,a,H,f))" |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
273 |
apply (rule wf_induct, assumption+) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
274 |
apply (frule wf_imp_relativized) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
275 |
apply (intro impI) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
276 |
apply (rule exists_is_recfun_indstep) |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
277 |
apply (blast dest: pair_components_in_M)+ |
13223 | 278 |
done |
279 |
||
280 |
constdefs |
|
13254 | 281 |
M_is_recfun :: "[i=>o, i, i, [i=>o,i,i,i]=>o, i] => o" |
282 |
"M_is_recfun(M,r,a,MH,f) == |
|
283 |
\<forall>z[M]. z \<in> f <-> |
|
284 |
(\<exists>x[M]. \<exists>y[M]. \<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M]. \<exists>f_r_sx[M]. |
|
285 |
pair(M,x,y,z) & pair(M,x,a,xa) & upair(M,x,x,sx) & |
|
286 |
pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) & |
|
287 |
xa \<in> r & MH(M, x, f_r_sx, y))" |
|
13223 | 288 |
|
289 |
lemma (in M_axioms) is_recfun_iff_M: |
|
13254 | 290 |
"[| M(r); M(a); M(f); \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)); |
13223 | 291 |
\<forall>x g y. M(x) --> M(g) --> M(y) --> MH(M,x,g,y) <-> y = H(x,g) |] ==> |
292 |
is_recfun(r,a,H,f) <-> M_is_recfun(M,r,a,MH,f)" |
|
13254 | 293 |
apply (simp add: M_is_recfun_def is_recfun_relativize) |
294 |
apply (rule rall_cong) |
|
295 |
apply (blast dest: transM) |
|
13223 | 296 |
done |
297 |
||
298 |
lemma M_is_recfun_cong [cong]: |
|
299 |
"[| r = r'; a = a'; f = f'; |
|
300 |
!!x g y. [| M(x); M(g); M(y) |] ==> MH(M,x,g,y) <-> MH'(M,x,g,y) |] |
|
301 |
==> M_is_recfun(M,r,a,MH,f) <-> M_is_recfun(M,r',a',MH',f')" |
|
302 |
by (simp add: M_is_recfun_def) |
|
303 |
||
304 |
||
305 |
constdefs |
|
306 |
(*This expresses ordinal addition as a formula in the LAST. It also |
|
307 |
provides an abbreviation that can be used in the instance of strong |
|
308 |
replacement below. Here j is used to define the relation, namely |
|
309 |
Memrel(succ(j)), while x determines the domain of f.*) |
|
310 |
is_oadd_fun :: "[i=>o,i,i,i,i] => o" |
|
311 |
"is_oadd_fun(M,i,j,x,f) == |
|
312 |
(\<forall>sj msj. M(sj) --> M(msj) --> |
|
313 |
successor(M,j,sj) --> membership(M,sj,msj) --> |
|
314 |
M_is_recfun(M, msj, x, |
|
315 |
%M x g y. \<exists>gx. M(gx) & image(M,g,x,gx) & union(M,i,gx,y), |
|
316 |
f))" |
|
317 |
||
318 |
is_oadd :: "[i=>o,i,i,i] => o" |
|
319 |
"is_oadd(M,i,j,k) == |
|
320 |
(~ ordinal(M,i) & ~ ordinal(M,j) & k=0) | |
|
321 |
(~ ordinal(M,i) & ordinal(M,j) & k=j) | |
|
322 |
(ordinal(M,i) & ~ ordinal(M,j) & k=i) | |
|
323 |
(ordinal(M,i) & ordinal(M,j) & |
|
324 |
(\<exists>f fj sj. M(f) & M(fj) & M(sj) & |
|
325 |
successor(M,j,sj) & is_oadd_fun(M,i,sj,sj,f) & |
|
326 |
fun_apply(M,f,j,fj) & fj = k))" |
|
327 |
||
328 |
(*NEEDS RELATIVIZATION*) |
|
329 |
omult_eqns :: "[i,i,i,i] => o" |
|
330 |
"omult_eqns(i,x,g,z) == |
|
331 |
Ord(x) & |
|
332 |
(x=0 --> z=0) & |
|
333 |
(\<forall>j. x = succ(j) --> z = g`j ++ i) & |
|
334 |
(Limit(x) --> z = \<Union>(g``x))" |
|
335 |
||
336 |
is_omult_fun :: "[i=>o,i,i,i] => o" |
|
337 |
"is_omult_fun(M,i,j,f) == |
|
338 |
(\<exists>df. M(df) & is_function(M,f) & |
|
339 |
is_domain(M,f,df) & subset(M, j, df)) & |
|
340 |
(\<forall>x\<in>j. omult_eqns(i,x,f,f`x))" |
|
341 |
||
342 |
is_omult :: "[i=>o,i,i,i] => o" |
|
343 |
"is_omult(M,i,j,k) == |
|
344 |
\<exists>f fj sj. M(f) & M(fj) & M(sj) & |
|
345 |
successor(M,j,sj) & is_omult_fun(M,i,sj,f) & |
|
346 |
fun_apply(M,f,j,fj) & fj = k" |
|
347 |
||
348 |
||
349 |
locale M_recursion = M_axioms + |
|
350 |
assumes oadd_strong_replacement: |
|
351 |
"[| M(i); M(j) |] ==> |
|
352 |
strong_replacement(M, |
|
353 |
\<lambda>x z. \<exists>y f fx. M(y) & M(f) & M(fx) & |
|
354 |
pair(M,x,y,z) & is_oadd_fun(M,i,j,x,f) & |
|
355 |
image(M,f,x,fx) & y = i Un fx)" |
|
356 |
and omult_strong_replacement': |
|
357 |
"[| M(i); M(j) |] ==> |
|
358 |
strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) & |
|
359 |
pair(M,x,y,z) & |
|
360 |
is_recfun(Memrel(succ(j)),x,%x g. THE z. omult_eqns(i,x,g,z),g) & |
|
361 |
y = (THE z. omult_eqns(i, x, g, z)))" |
|
362 |
||
363 |
||
364 |
||
365 |
text{*is_oadd_fun: Relating the pure "language of set theory" to Isabelle/ZF*} |
|
366 |
lemma (in M_recursion) is_oadd_fun_iff: |
|
367 |
"[| a\<le>j; M(i); M(j); M(a); M(f) |] |
|
368 |
==> is_oadd_fun(M,i,j,a,f) <-> |
|
369 |
f \<in> a \<rightarrow> range(f) & (\<forall>x. M(x) --> x < a --> f`x = i Un f``x)" |
|
370 |
apply (frule lt_Ord) |
|
371 |
apply (simp add: is_oadd_fun_def Memrel_closed Un_closed |
|
372 |
is_recfun_iff_M [of concl: _ _ "%x g. i Un g``x", THEN iff_sym] |
|
373 |
image_closed is_recfun_iff_equation |
|
374 |
Ball_def lt_trans [OF ltI, of _ a] lt_Memrel) |
|
375 |
apply (simp add: lt_def) |
|
376 |
apply (blast dest: transM) |
|
377 |
done |
|
378 |
||
379 |
||
380 |
lemma (in M_recursion) oadd_strong_replacement': |
|
381 |
"[| M(i); M(j) |] ==> |
|
382 |
strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) & |
|
383 |
pair(M,x,y,z) & |
|
384 |
is_recfun(Memrel(succ(j)),x,%x g. i Un g``x,g) & |
|
385 |
y = i Un g``x)" |
|
386 |
apply (insert oadd_strong_replacement [of i j]) |
|
387 |
apply (simp add: Memrel_closed Un_closed image_closed is_oadd_fun_def |
|
388 |
is_recfun_iff_M) |
|
389 |
done |
|
390 |
||
391 |
||
392 |
lemma (in M_recursion) exists_oadd: |
|
393 |
"[| Ord(j); M(i); M(j) |] |
|
394 |
==> \<exists>f. M(f) & is_recfun(Memrel(succ(j)), j, %x g. i Un g``x, f)" |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
395 |
apply (rule wf_exists_is_recfun [OF wf_Memrel trans_Memrel]) |
13254 | 396 |
apply simp |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
397 |
apply (blast intro: oadd_strong_replacement') |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
398 |
apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed) |
13223 | 399 |
done |
400 |
||
401 |
lemma (in M_recursion) exists_oadd_fun: |
|
402 |
"[| Ord(j); M(i); M(j) |] |
|
403 |
==> \<exists>f. M(f) & is_oadd_fun(M,i,succ(j),succ(j),f)" |
|
404 |
apply (rule exists_oadd [THEN exE]) |
|
405 |
apply (erule Ord_succ, assumption, simp) |
|
406 |
apply (rename_tac f, clarify) |
|
407 |
apply (frule is_recfun_type) |
|
408 |
apply (rule_tac x=f in exI) |
|
409 |
apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def |
|
410 |
is_oadd_fun_iff Ord_trans [OF _ succI1]) |
|
411 |
done |
|
412 |
||
413 |
lemma (in M_recursion) is_oadd_fun_apply: |
|
414 |
"[| x < j; M(i); M(j); M(f); is_oadd_fun(M,i,j,j,f) |] |
|
415 |
==> f`x = i Un (\<Union>k\<in>x. {f ` k})" |
|
416 |
apply (simp add: is_oadd_fun_iff lt_Ord2, clarify) |
|
417 |
apply (frule lt_closed, simp) |
|
418 |
apply (frule leI [THEN le_imp_subset]) |
|
419 |
apply (simp add: image_fun, blast) |
|
420 |
done |
|
421 |
||
422 |
lemma (in M_recursion) is_oadd_fun_iff_oadd [rule_format]: |
|
423 |
"[| is_oadd_fun(M,i,J,J,f); M(i); M(J); M(f); Ord(i); Ord(j) |] |
|
424 |
==> j<J --> f`j = i++j" |
|
425 |
apply (erule_tac i=j in trans_induct, clarify) |
|
426 |
apply (subgoal_tac "\<forall>k\<in>x. k<J") |
|
427 |
apply (simp (no_asm_simp) add: is_oadd_def oadd_unfold is_oadd_fun_apply) |
|
428 |
apply (blast intro: lt_trans ltI lt_Ord) |
|
429 |
done |
|
430 |
||
431 |
lemma (in M_recursion) oadd_abs_fun_apply_iff: |
|
432 |
"[| M(i); M(J); M(f); M(k); j<J; is_oadd_fun(M,i,J,J,f) |] |
|
433 |
==> fun_apply(M,f,j,k) <-> f`j = k" |
|
434 |
by (force simp add: lt_def is_oadd_fun_iff subsetD typed_apply_abs) |
|
435 |
||
436 |
lemma (in M_recursion) Ord_oadd_abs: |
|
437 |
"[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_oadd(M,i,j,k) <-> k = i++j" |
|
438 |
apply (simp add: is_oadd_def oadd_abs_fun_apply_iff is_oadd_fun_iff_oadd) |
|
439 |
apply (frule exists_oadd_fun [of j i], blast+) |
|
440 |
done |
|
441 |
||
442 |
lemma (in M_recursion) oadd_abs: |
|
443 |
"[| M(i); M(j); M(k) |] ==> is_oadd(M,i,j,k) <-> k = i++j" |
|
444 |
apply (case_tac "Ord(i) & Ord(j)") |
|
445 |
apply (simp add: Ord_oadd_abs) |
|
446 |
apply (auto simp add: is_oadd_def oadd_eq_if_raw_oadd) |
|
447 |
done |
|
448 |
||
13245 | 449 |
lemma (in M_recursion) oadd_closed [intro,simp]: |
13223 | 450 |
"[| M(i); M(j) |] ==> M(i++j)" |
451 |
apply (simp add: oadd_eq_if_raw_oadd, clarify) |
|
452 |
apply (simp add: raw_oadd_eq_oadd) |
|
453 |
apply (frule exists_oadd_fun [of j i], auto) |
|
454 |
apply (simp add: apply_closed is_oadd_fun_iff_oadd [symmetric]) |
|
455 |
done |
|
456 |
||
457 |
||
458 |
text{*Ordinal Multiplication*} |
|
459 |
||
460 |
lemma omult_eqns_unique: |
|
461 |
"[| omult_eqns(i,x,g,z); omult_eqns(i,x,g,z') |] ==> z=z'"; |
|
462 |
apply (simp add: omult_eqns_def, clarify) |
|
463 |
apply (erule Ord_cases, simp_all) |
|
464 |
done |
|
465 |
||
466 |
lemma omult_eqns_0: "omult_eqns(i,0,g,z) <-> z=0" |
|
467 |
by (simp add: omult_eqns_def) |
|
468 |
||
469 |
lemma the_omult_eqns_0: "(THE z. omult_eqns(i,0,g,z)) = 0" |
|
470 |
by (simp add: omult_eqns_0) |
|
471 |
||
472 |
lemma omult_eqns_succ: "omult_eqns(i,succ(j),g,z) <-> Ord(j) & z = g`j ++ i" |
|
473 |
by (simp add: omult_eqns_def) |
|
474 |
||
475 |
lemma the_omult_eqns_succ: |
|
476 |
"Ord(j) ==> (THE z. omult_eqns(i,succ(j),g,z)) = g`j ++ i" |
|
477 |
by (simp add: omult_eqns_succ) |
|
478 |
||
479 |
lemma omult_eqns_Limit: |
|
480 |
"Limit(x) ==> omult_eqns(i,x,g,z) <-> z = \<Union>(g``x)" |
|
481 |
apply (simp add: omult_eqns_def) |
|
482 |
apply (blast intro: Limit_is_Ord) |
|
483 |
done |
|
484 |
||
485 |
lemma the_omult_eqns_Limit: |
|
486 |
"Limit(x) ==> (THE z. omult_eqns(i,x,g,z)) = \<Union>(g``x)" |
|
487 |
by (simp add: omult_eqns_Limit) |
|
488 |
||
489 |
lemma omult_eqns_Not: "~ Ord(x) ==> ~ omult_eqns(i,x,g,z)" |
|
490 |
by (simp add: omult_eqns_def) |
|
491 |
||
492 |
||
493 |
lemma (in M_recursion) the_omult_eqns_closed: |
|
494 |
"[| M(i); M(x); M(g); function(g) |] |
|
495 |
==> M(THE z. omult_eqns(i, x, g, z))" |
|
496 |
apply (case_tac "Ord(x)") |
|
497 |
prefer 2 apply (simp add: omult_eqns_Not) --{*trivial, non-Ord case*} |
|
498 |
apply (erule Ord_cases) |
|
499 |
apply (simp add: omult_eqns_0) |
|
500 |
apply (simp add: omult_eqns_succ apply_closed oadd_closed) |
|
501 |
apply (simp add: omult_eqns_Limit) |
|
502 |
done |
|
503 |
||
504 |
lemma (in M_recursion) exists_omult: |
|
505 |
"[| Ord(j); M(i); M(j) |] |
|
506 |
==> \<exists>f. M(f) & is_recfun(Memrel(succ(j)), j, %x g. THE z. omult_eqns(i,x,g,z), f)" |
|
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
507 |
apply (rule wf_exists_is_recfun [OF wf_Memrel trans_Memrel]) |
13254 | 508 |
apply simp |
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
509 |
apply (blast intro: omult_strong_replacement') |
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset
|
510 |
apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed) |
13223 | 511 |
apply (blast intro: the_omult_eqns_closed) |
512 |
done |
|
513 |
||
514 |
lemma (in M_recursion) exists_omult_fun: |
|
515 |
"[| Ord(j); M(i); M(j) |] ==> \<exists>f. M(f) & is_omult_fun(M,i,succ(j),f)" |
|
516 |
apply (rule exists_omult [THEN exE]) |
|
517 |
apply (erule Ord_succ, assumption, simp) |
|
518 |
apply (rename_tac f, clarify) |
|
519 |
apply (frule is_recfun_type) |
|
520 |
apply (rule_tac x=f in exI) |
|
521 |
apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def |
|
522 |
is_omult_fun_def Ord_trans [OF _ succI1]) |
|
523 |
apply (force dest: Ord_in_Ord' |
|
524 |
simp add: omult_eqns_def the_omult_eqns_0 the_omult_eqns_succ |
|
525 |
the_omult_eqns_Limit) |
|
526 |
done |
|
527 |
||
528 |
lemma (in M_recursion) is_omult_fun_apply_0: |
|
529 |
"[| 0 < j; is_omult_fun(M,i,j,f) |] ==> f`0 = 0" |
|
530 |
by (simp add: is_omult_fun_def omult_eqns_def lt_def ball_conj_distrib) |
|
531 |
||
532 |
lemma (in M_recursion) is_omult_fun_apply_succ: |
|
533 |
"[| succ(x) < j; is_omult_fun(M,i,j,f) |] ==> f`succ(x) = f`x ++ i" |
|
534 |
by (simp add: is_omult_fun_def omult_eqns_def lt_def, blast) |
|
535 |
||
536 |
lemma (in M_recursion) is_omult_fun_apply_Limit: |
|
537 |
"[| x < j; Limit(x); M(j); M(f); is_omult_fun(M,i,j,f) |] |
|
538 |
==> f ` x = (\<Union>y\<in>x. f`y)" |
|
539 |
apply (simp add: is_omult_fun_def omult_eqns_def domain_closed lt_def, clarify) |
|
540 |
apply (drule subset_trans [OF OrdmemD], assumption+) |
|
541 |
apply (simp add: ball_conj_distrib omult_Limit image_function) |
|
542 |
done |
|
543 |
||
544 |
lemma (in M_recursion) is_omult_fun_eq_omult: |
|
545 |
"[| is_omult_fun(M,i,J,f); M(J); M(f); Ord(i); Ord(j) |] |
|
546 |
==> j<J --> f`j = i**j" |
|
547 |
apply (erule_tac i=j in trans_induct3) |
|
548 |
apply (safe del: impCE) |
|
549 |
apply (simp add: is_omult_fun_apply_0) |
|
550 |
apply (subgoal_tac "x<J") |
|
551 |
apply (simp add: is_omult_fun_apply_succ omult_succ) |
|
552 |
apply (blast intro: lt_trans) |
|
553 |
apply (subgoal_tac "\<forall>k\<in>x. k<J") |
|
554 |
apply (simp add: is_omult_fun_apply_Limit omult_Limit) |
|
555 |
apply (blast intro: lt_trans ltI lt_Ord) |
|
556 |
done |
|
557 |
||
558 |
lemma (in M_recursion) omult_abs_fun_apply_iff: |
|
559 |
"[| M(i); M(J); M(f); M(k); j<J; is_omult_fun(M,i,J,f) |] |
|
560 |
==> fun_apply(M,f,j,k) <-> f`j = k" |
|
561 |
by (auto simp add: lt_def is_omult_fun_def subsetD apply_abs) |
|
562 |
||
563 |
lemma (in M_recursion) omult_abs: |
|
564 |
"[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_omult(M,i,j,k) <-> k = i**j" |
|
565 |
apply (simp add: is_omult_def omult_abs_fun_apply_iff is_omult_fun_eq_omult) |
|
566 |
apply (frule exists_omult_fun [of j i], blast+) |
|
567 |
done |
|
568 |
||
569 |
end |
|
570 |