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