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

3 
*) 

4 

13306  5 
header{*Relativized WellFounded Recursion*} 
6 

16417  7 
theory WFrec imports Wellorderings begin 
13223  8 

9 

13506  10 
subsection{*General Lemmas*} 
11 

13254  12 
(*Many of these might be useful in WF.thy*) 
13223  13 

13269  14 
lemma apply_recfun2: 
15 
"[ is_recfun(r,a,H,f); <x,i>:f ] ==> i = H(x, restrict(f,r``{x}))" 

16 
apply (frule apply_recfun) 

17 
apply (blast dest: is_recfun_type fun_is_rel) 

18 
apply (simp add: function_apply_equality [OF _ is_recfun_imp_function]) 

13223  19 
done 
20 

21 
text{*Expresses @{text is_recfun} as a recursion equation*} 

22 
lemma is_recfun_iff_equation: 

46823  23 
"is_recfun(r,a,H,f) \<longleftrightarrow> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

24 
f \<in> r `` {a} \<rightarrow> range(f) & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

25 
(\<forall>x \<in> r``{a}. f`x = H(x, restrict(f, r``{x})))" 
13223  26 
apply (rule iffI) 
27 
apply (simp add: is_recfun_type apply_recfun Ball_def vimage_singleton_iff, 

28 
clarify) 

29 
apply (simp add: is_recfun_def) 

30 
apply (rule fun_extension) 

31 
apply assumption 

32 
apply (fast intro: lam_type, simp) 

33 
done 

34 

13245  35 
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  36 
by (blast dest: is_recfun_type fun_is_rel) 
13245  37 

13254  38 
lemma trans_Int_eq: 
39 
"[ 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

40 
by (blast intro: transD) 
13223  41 

13254  42 
lemma is_recfun_restrict_idem: 
43 
"is_recfun(r,a,H,f) ==> restrict(f, r `` {a}) = f" 

44 
apply (drule is_recfun_type) 

45 
apply (auto simp add: Pi_iff subset_Sigma_imp_relation restrict_idem) 

46 
done 

47 

48 
lemma is_recfun_cong_lemma: 

49 
"[ is_recfun(r,a,H,f); r = r'; a = a'; f = f'; 

46823  50 
!!x g. [ <x,a'> \<in> r'; relation(g); domain(g) \<subseteq> r' ``{x} ] 
13254  51 
==> H(x,g) = H'(x,g) ] 
52 
==> is_recfun(r',a',H',f')" 

53 
apply (simp add: is_recfun_def) 

54 
apply (erule trans) 

55 
apply (rule lam_cong) 

56 
apply (simp_all add: vimage_singleton_iff Int_lower2) 

57 
done 

58 

59 
text{*For @{text is_recfun} we need only pay attention to functions 

60 
whose domains are initial segments of @{term r}.*} 

61 
lemma is_recfun_cong: 

62 
"[ r = r'; a = a'; f = f'; 

46823  63 
!!x g. [ <x,a'> \<in> r'; relation(g); domain(g) \<subseteq> r' ``{x} ] 
13254  64 
==> H(x,g) = H'(x,g) ] 
46823  65 
==> is_recfun(r,a,H,f) \<longleftrightarrow> is_recfun(r',a',H',f')" 
13254  66 
apply (rule iffI) 
67 
txt{*Messy: fast and blast don't work for some reason*} 

68 
apply (erule is_recfun_cong_lemma, auto) 

69 
apply (erule is_recfun_cong_lemma) 

70 
apply (blast intro: sym)+ 

71 
done 

13223  72 

13506  73 
subsection{*Reworking of the Recursion Theory Within @{term M}*} 
74 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13506
diff
changeset

75 
lemma (in M_basic) is_recfun_separation': 
13319  76 
"[ f \<in> r `` {a} \<rightarrow> range(f); g \<in> r `` {b} \<rightarrow> range(g); 
77 
M(r); M(f); M(g); M(a); M(b) ] 

78 
==> separation(M, \<lambda>x. \<not> (\<langle>x, a\<rangle> \<in> r \<longrightarrow> \<langle>x, b\<rangle> \<in> r \<longrightarrow> f ` x = g ` x))" 

79 
apply (insert is_recfun_separation [of r f g a b]) 

13352  80 
apply (simp add: vimage_singleton_iff) 
13319  81 
done 
13223  82 

13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset

83 
text{*Stated using @{term "trans(r)"} rather than 
13223  84 
@{term "transitive_rel(M,A,r)"} because the latter rewrites to 
85 
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

86 
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

87 
The last three Mpremises are redundant because of @{term "M(r)"}, 
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset

88 
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

89 
more work to set up the induction formula.*} 
13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13506
diff
changeset

90 
lemma (in M_basic) is_recfun_equal [rule_format]: 
13223  91 
"[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

92 
wellfounded(M,r); trans(r); 
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset

93 
M(f); M(g); M(r); M(x); M(a); M(b) ] 
46823  94 
==> <x,a> \<in> r \<longrightarrow> <x,b> \<in> r \<longrightarrow> f`x=g`x" 
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13319
diff
changeset

95 
apply (frule_tac f=f in is_recfun_type) 
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13319
diff
changeset

96 
apply (frule_tac f=g in is_recfun_type) 
13223  97 
apply (simp add: is_recfun_def) 
13254  98 
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

99 
txt{*Separation to justify the induction*} 
13319  100 
apply (blast intro: is_recfun_separation') 
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset

101 
txt{*Now the inductive argument itself*} 
13254  102 
apply clarify 
13223  103 
apply (erule ssubst)+ 
104 
apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def) 

105 
apply (rename_tac x1) 

106 
apply (rule_tac t="%z. H(x1,z)" in subst_context) 

46823  107 
apply (subgoal_tac "\<forall>y \<in> r``{x1}. \<forall>z. <y,z>\<in>f \<longleftrightarrow> <y,z>\<in>g") 
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset

108 
apply (blast intro: transD) 
13223  109 
apply (simp add: apply_iff) 
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset

110 
apply (blast intro: transD sym) 
13223  111 
done 
112 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13506
diff
changeset

113 
lemma (in M_basic) is_recfun_cut: 
13223  114 
"[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

115 
wellfounded(M,r); trans(r); 
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset

116 
M(f); M(g); M(r); <b,a> \<in> r ] 
13223  117 
==> restrict(f, r``{b}) = g" 
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13319
diff
changeset

118 
apply (frule_tac f=f in is_recfun_type) 
13223  119 
apply (rule fun_extension) 
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset

120 
apply (blast intro: transD restrict_type2) 
13223  121 
apply (erule is_recfun_type, simp) 
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset

122 
apply (blast intro: is_recfun_equal transD dest: transM) 
13223  123 
done 
124 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13506
diff
changeset

125 
lemma (in M_basic) is_recfun_functional: 
13223  126 
"[is_recfun(r,a,H,f); is_recfun(r,a,H,g); 
13268  127 
wellfounded(M,r); trans(r); M(f); M(g); M(r) ] ==> f=g" 
13223  128 
apply (rule fun_extension) 
129 
apply (erule is_recfun_type)+ 

13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset

130 
apply (blast intro!: is_recfun_equal dest: transM) 
13254  131 
done 
13223  132 

13295  133 
text{*Tells us that @{text is_recfun} can (in principle) be relativized.*} 
13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13506
diff
changeset

134 
lemma (in M_basic) is_recfun_relativize: 
46823  135 
"[ M(r); M(f); \<forall>x[M]. \<forall>g[M]. function(g) \<longrightarrow> M(H(x,g)) ] 
136 
==> is_recfun(r,a,H,f) \<longleftrightarrow> 

137 
(\<forall>z[M]. z \<in> f \<longleftrightarrow> 

13254  138 
(\<exists>x[M]. <x,a> \<in> r & z = <x, H(x, restrict(f, r``{x}))>))"; 
139 
apply (simp add: is_recfun_def lam_def) 

13223  140 
apply (safe intro!: equalityI) 
13254  141 
apply (drule equalityD1 [THEN subsetD], assumption) 
142 
apply (blast dest: pair_components_in_M) 

143 
apply (blast elim!: equalityE dest: pair_components_in_M) 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13564
diff
changeset

144 
apply (frule transM, assumption) 
13223  145 
apply simp 
146 
apply blast 

13254  147 
apply (subgoal_tac "is_function(M,f)") 
148 
txt{*We use @{term "is_function"} rather than @{term "function"} because 

149 
the subgoal's easier to prove with relativized quantifiers!*} 

150 
prefer 2 apply (simp add: is_function_def) 

13223  151 
apply (frule pair_components_in_M, assumption) 
13254  152 
apply (simp add: is_recfun_imp_function function_restrictI) 
13223  153 
done 
154 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13506
diff
changeset

155 
lemma (in M_basic) is_recfun_restrict: 
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset

156 
"[ 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

157 
M(r); M(f); 
46823  158 
\<forall>x[M]. \<forall>g[M]. function(g) \<longrightarrow> M(H(x,g)) ] 
13223  159 
==> is_recfun(r, y, H, restrict(f, r `` {y}))" 
160 
apply (frule pair_components_in_M, assumption, clarify) 

13254  161 
apply (simp (no_asm_simp) add: is_recfun_relativize restrict_iff 
162 
trans_Int_eq) 

13223  163 
apply safe 
164 
apply (simp_all add: vimage_singleton_iff is_recfun_type [THEN apply_iff]) 

165 
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

166 
apply (frule_tac x=xa in apply_recfun, blast intro: transD) 
13247  167 
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

168 
is_recfun_imp_function function_restrictI) 
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset

169 
apply (blast intro: apply_recfun dest: transD) 
13223  170 
done 
171 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13506
diff
changeset

172 
lemma (in M_basic) restrict_Y_lemma: 
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset

173 
"[ wellfounded(M,r); trans(r); M(r); 
46823  174 
\<forall>x[M]. \<forall>g[M]. function(g) \<longrightarrow> M(H(x,g)); M(Y); 
13299  175 
\<forall>b[M]. 
46823  176 
b \<in> Y \<longleftrightarrow> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

177 
(\<exists>x[M]. <x,a1> \<in> r & 
13299  178 
(\<exists>y[M]. b = \<langle>x,y\<rangle> & (\<exists>g[M]. is_recfun(r,x,H,g) \<and> y = H(x,g)))); 
179 
\<langle>x,a1\<rangle> \<in> r; is_recfun(r,x,H,f); M(f) ] 

13223  180 
==> restrict(Y, r `` {x}) = f" 
46823  181 
apply (subgoal_tac "\<forall>y \<in> r``{x}. \<forall>z. <y,z>:Y \<longleftrightarrow> <y,z>:f") 
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset

182 
apply (simp (no_asm_simp) add: restrict_def) 
13254  183 
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

184 
apply (frule is_recfun_type [THEN fun_is_rel], blast) 
13223  185 
apply (frule pair_components_in_M, assumption, clarify) 
186 
apply (rule iffI) 

13505  187 
apply (frule_tac y="<y,z>" in transM, assumption) 
13223  188 
apply (clarsimp simp add: vimage_singleton_iff is_recfun_type [THEN apply_iff] 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

189 
apply_recfun is_recfun_cut) 
13223  190 
txt{*Opposite inclusion: something in f, show in Y*} 
13293  191 
apply (frule_tac y="<y,z>" in transM, assumption) 
192 
apply (simp add: vimage_singleton_iff) 

193 
apply (rule conjI) 

194 
apply (blast dest: transD) 

13268  195 
apply (rule_tac x="restrict(f, r `` {y})" in rexI) 
196 
apply (simp_all add: is_recfun_restrict 

197 
apply_recfun is_recfun_type [THEN apply_iff]) 

13223  198 
done 
199 

13245  200 
text{*For typical applications of Replacement for recursive definitions*} 
13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13506
diff
changeset

201 
lemma (in M_basic) univalent_is_recfun: 
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset

202 
"[wellfounded(M,r); trans(r); M(r)] 
13268  203 
==> univalent (M, A, \<lambda>x p. 
13293  204 
\<exists>y[M]. p = \<langle>x,y\<rangle> & (\<exists>f[M]. is_recfun(r,x,H,f) & y = H(x,f)))" 
13245  205 
apply (simp add: univalent_def) 
206 
apply (blast dest: is_recfun_functional) 

207 
done 

208 

13299  209 

13223  210 
text{*Proof of the inductive step for @{text exists_is_recfun}, since 
211 
we must prove two versions.*} 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13506
diff
changeset

212 
lemma (in M_basic) exists_is_recfun_indstep: 
46823  213 
"[\<forall>y. \<langle>y, a1\<rangle> \<in> r \<longrightarrow> (\<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

214 
wellfounded(M,r); trans(r); M(r); M(a1); 
13268  215 
strong_replacement(M, \<lambda>x z. 
216 
\<exists>y[M]. \<exists>g[M]. pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 

46823  217 
\<forall>x[M]. \<forall>g[M]. function(g) \<longrightarrow> M(H(x,g))] 
13268  218 
==> \<exists>f[M]. is_recfun(r,a1,H,f)" 
13223  219 
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

220 
apply blast 
13223  221 
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

222 
apply (simp add: univalent_is_recfun) 
13223  223 
txt{*Show that the constructed object satisfies @{text is_recfun}*} 
224 
apply clarify 

13268  225 
apply (rule_tac x=Y in rexI) 
13254  226 
txt{*Unfold only the toplevel occurrence of @{term is_recfun}*} 
227 
apply (simp (no_asm_simp) add: is_recfun_relativize [of concl: _ a1]) 

13268  228 
txt{*The big iffformula defining @{term Y} is now redundant*} 
13254  229 
apply safe 
13299  230 
apply (simp add: vimage_singleton_iff restrict_Y_lemma [of r H _ a1]) 
13223  231 
txt{*one more case*} 
13254  232 
apply (simp (no_asm_simp) add: Bex_def vimage_singleton_iff) 
13223  233 
apply (drule_tac x1=x in spec [THEN mp], assumption, clarify) 
13268  234 
apply (rename_tac f) 
235 
apply (rule_tac x=f in rexI) 

13293  236 
apply (simp_all add: restrict_Y_lemma [of r H]) 
13299  237 
txt{*FIXME: should not be needed!*} 
238 
apply (subst restrict_Y_lemma [of r H]) 

239 
apply (simp add: vimage_singleton_iff)+ 

240 
apply blast+ 

13223  241 
done 
242 

243 
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

244 
@{term "wellfounded(M,r)"}*} 
13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13506
diff
changeset

245 
lemma (in M_basic) wellfounded_exists_is_recfun: 
13251
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset

246 
"[wellfounded(M,r); trans(r); 
13268  247 
separation(M, \<lambda>x. ~ (\<exists>f[M]. is_recfun(r, x, H, f))); 
248 
strong_replacement(M, \<lambda>x z. 

249 
\<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

250 
M(r); M(a); 
46823  251 
\<forall>x[M]. \<forall>g[M]. function(g) \<longrightarrow> M(H(x,g)) ] 
13268  252 
==> \<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

253 
apply (rule wellfounded_induct, assumption+, clarify) 
13223  254 
apply (rule exists_is_recfun_indstep, assumption+) 
255 
done 

256 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13506
diff
changeset

257 
lemma (in M_basic) wf_exists_is_recfun [rule_format]: 
13268  258 
"[wf(r); trans(r); M(r); 
259 
strong_replacement(M, \<lambda>x z. 

260 
\<exists>y[M]. \<exists>g[M]. pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 

46823  261 
\<forall>x[M]. \<forall>g[M]. function(g) \<longrightarrow> M(H(x,g)) ] 
262 
==> M(a) \<longrightarrow> (\<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

263 
apply (rule wf_induct, assumption+) 
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset

264 
apply (frule wf_imp_relativized) 
74cb2af8811e
new treatment of wfrec, replacing wf[A](r) by wf(r)
paulson
parents:
13247
diff
changeset

265 
apply (intro impI) 
13268  266 
apply (rule exists_is_recfun_indstep) 
267 
apply (blast dest: transM del: rev_rallE, assumption+) 

13223  268 
done 
269 

13506  270 

271 
subsection{*Relativization of the ZF Predicate @{term is_recfun}*} 

272 

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

274 
M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o" where 
13352  275 
"M_is_recfun(M,MH,r,a,f) == 
46823  276 
\<forall>z[M]. z \<in> f \<longleftrightarrow> 
13254  277 
(\<exists>x[M]. \<exists>y[M]. \<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M]. \<exists>f_r_sx[M]. 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

278 
pair(M,x,y,z) & pair(M,x,a,xa) & upair(M,x,x,sx) & 
13254  279 
pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) & 
13348  280 
xa \<in> r & MH(x, f_r_sx, y))" 
13223  281 

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

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

283 
is_wfrec :: "[i=>o, [i,i,i]=>o, i, i, i] => o" where 
13353  284 
"is_wfrec(M,MH,r,a,z) == 
285 
\<exists>f[M]. M_is_recfun(M,MH,r,a,f) & MH(a,f,z)" 

286 

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

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

288 
wfrec_replacement :: "[i=>o, [i,i,i]=>o, i] => o" where 
13353  289 
"wfrec_replacement(M,MH,r) == 
290 
strong_replacement(M, 

291 
\<lambda>x z. \<exists>y[M]. pair(M,x,y,z) & is_wfrec(M,MH,r,x,y))" 

292 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13506
diff
changeset

293 
lemma (in M_basic) is_recfun_abs: 
46823  294 
"[ \<forall>x[M]. \<forall>g[M]. function(g) \<longrightarrow> M(H(x,g)); M(r); M(a); M(f); 
13634  295 
relation2(M,MH,H) ] 
46823  296 
==> M_is_recfun(M,MH,r,a,f) \<longleftrightarrow> is_recfun(r,a,H,f)" 
13634  297 
apply (simp add: M_is_recfun_def relation2_def is_recfun_relativize) 
13254  298 
apply (rule rall_cong) 
299 
apply (blast dest: transM) 

13223  300 
done 
301 

302 
lemma M_is_recfun_cong [cong]: 

303 
"[ r = r'; a = a'; f = f'; 

46823  304 
!!x g y. [ M(x); M(g); M(y) ] ==> MH(x,g,y) \<longleftrightarrow> MH'(x,g,y) ] 
305 
==> M_is_recfun(M,MH,r,a,f) \<longleftrightarrow> M_is_recfun(M,MH',r',a',f')" 

13223  306 
by (simp add: M_is_recfun_def) 
307 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13506
diff
changeset

308 
lemma (in M_basic) is_wfrec_abs: 
46823  309 
"[ \<forall>x[M]. \<forall>g[M]. function(g) \<longrightarrow> M(H(x,g)); 
13634  310 
relation2(M,MH,H); M(r); M(a); M(z) ] 
46823  311 
==> is_wfrec(M,MH,r,a,z) \<longleftrightarrow> 
13353  312 
(\<exists>g[M]. is_recfun(r,a,H,g) & z = H(a,g))" 
13634  313 
by (simp add: is_wfrec_def relation2_def is_recfun_abs) 
13223  314 

13353  315 
text{*Relating @{term wfrec_replacement} to native constructs*} 
13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13506
diff
changeset

316 
lemma (in M_basic) wfrec_replacement': 
13353  317 
"[wfrec_replacement(M,MH,r); 
46823  318 
\<forall>x[M]. \<forall>g[M]. function(g) \<longrightarrow> M(H(x,g)); 
13634  319 
relation2(M,MH,H); M(r)] 
13353  320 
==> strong_replacement(M, \<lambda>x z. \<exists>y[M]. 
321 
pair(M,x,y,z) & (\<exists>g[M]. is_recfun(r,x,H,g) & y = H(x,g)))" 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13564
diff
changeset

322 
by (simp add: wfrec_replacement_def is_wfrec_abs) 
13353  323 

324 
lemma wfrec_replacement_cong [cong]: 

46823  325 
"[ !!x y z. [ M(x); M(y); M(z) ] ==> MH(x,y,z) \<longleftrightarrow> MH'(x,y,z); 
13353  326 
r=r' ] 
46823  327 
==> wfrec_replacement(M, %x y. MH(x,y), r) \<longleftrightarrow> 
13353  328 
wfrec_replacement(M, %x y. MH'(x,y), r')" 
329 
by (simp add: is_wfrec_def wfrec_replacement_def) 

330 

331 

13223  332 
end 
333 