author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46823  57bf0cecb366 
child 58871  c399ae4b836f 
permissions  rwrr 
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset

1 
(* Title: ZF/Constructible/Rec_Separation.thy 
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset

2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset

3 
*) 
13429  4 

5 
header {*Separation for Facts About Recursion*} 

13348  6 

16417  7 
theory Rec_Separation imports Separation Internalize begin 
13348  8 

9 
text{*This theory proves all instances needed for locales @{text 

13634  10 
"M_trancl"} and @{text "M_datatypes"}*} 
13348  11 

13363  12 
lemma eq_succ_imp_lt: "[i = succ(j); Ord(i)] ==> j<i" 
13428  13 
by simp 
13363  14 

13493
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset

15 

13348  16 
subsection{*The Locale @{text "M_trancl"}*} 
17 

18 
subsubsection{*Separation for Reflexive/Transitive Closure*} 

19 

20 
text{*First, The Defining Formula*} 

21 

22 
(* "rtran_closure_mem(M,A,r,p) == 

13428  23 
\<exists>nnat[M]. \<exists>n[M]. \<exists>n'[M]. 
13348  24 
omega(M,nnat) & n\<in>nnat & successor(M,n,n') & 
25 
(\<exists>f[M]. typed_function(M,n',A,f) & 

13428  26 
(\<exists>x[M]. \<exists>y[M]. \<exists>zero[M]. pair(M,x,y,p) & empty(M,zero) & 
27 
fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) & 

46823  28 
(\<forall>j[M]. j\<in>n \<longrightarrow> 
13428  29 
(\<exists>fj[M]. \<exists>sj[M]. \<exists>fsj[M]. \<exists>ffp[M]. 
30 
fun_apply(M,f,j,fj) & successor(M,j,sj) & 

31 
fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \<in> r)))"*) 

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

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

33 
rtran_closure_mem_fm :: "[i,i,i]=>i" where 
13428  34 
"rtran_closure_mem_fm(A,r,p) == 
13348  35 
Exists(Exists(Exists( 
36 
And(omega_fm(2), 

37 
And(Member(1,2), 

38 
And(succ_fm(1,0), 

39 
Exists(And(typed_function_fm(1, A#+4, 0), 

13428  40 
And(Exists(Exists(Exists( 
41 
And(pair_fm(2,1,p#+7), 

42 
And(empty_fm(0), 

43 
And(fun_apply_fm(3,0,2), fun_apply_fm(3,5,1))))))), 

44 
Forall(Implies(Member(0,3), 

45 
Exists(Exists(Exists(Exists( 

46 
And(fun_apply_fm(5,4,3), 

47 
And(succ_fm(4,2), 

48 
And(fun_apply_fm(5,2,1), 

49 
And(pair_fm(3,1,0), Member(0,r#+9))))))))))))))))))))" 

13348  50 

51 

52 
lemma rtran_closure_mem_type [TC]: 

53 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] ==> rtran_closure_mem_fm(x,y,z) \<in> formula" 

13428  54 
by (simp add: rtran_closure_mem_fm_def) 
13348  55 

56 
lemma sats_rtran_closure_mem_fm [simp]: 

57 
"[ x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 

46823  58 
==> sats(A, rtran_closure_mem_fm(x,y,z), env) \<longleftrightarrow> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset

59 
rtran_closure_mem(##A, nth(x,env), nth(y,env), nth(z,env))" 
13348  60 
by (simp add: rtran_closure_mem_fm_def rtran_closure_mem_def) 
61 

62 
lemma rtran_closure_mem_iff_sats: 

13428  63 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13348  64 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
46823  65 
==> rtran_closure_mem(##A, x, y, z) \<longleftrightarrow> sats(A, rtran_closure_mem_fm(i,j,k), env)" 
13348  66 
by (simp add: sats_rtran_closure_mem_fm) 
67 

13566  68 
lemma rtran_closure_mem_reflection: 
13428  69 
"REFLECTS[\<lambda>x. rtran_closure_mem(L,f(x),g(x),h(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset

70 
\<lambda>i x. rtran_closure_mem(##Lset(i),f(x),g(x),h(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

71 
apply (simp only: rtran_closure_mem_def) 
13428  72 
apply (intro FOL_reflections function_reflections fun_plus_reflections) 
13348  73 
done 
74 

75 
text{*Separation for @{term "rtrancl(r)"}.*} 

76 
lemma rtrancl_separation: 

77 
"[ L(r); L(A) ] ==> separation (L, rtran_closure_mem(L,A,r))" 

13687  78 
apply (rule gen_separation_multi [OF rtran_closure_mem_reflection, of "{r,A}"], 
79 
auto) 

80 
apply (rule_tac env="[r,A]" in DPow_LsetI) 

81 
apply (rule rtran_closure_mem_iff_sats sep_rules  simp)+ 

13348  82 
done 
83 

84 

85 
subsubsection{*Reflexive/Transitive Closure, Internalized*} 

86 

13428  87 
(* "rtran_closure(M,r,s) == 
46823  88 
\<forall>A[M]. is_field(M,r,A) \<longrightarrow> 
89 
(\<forall>p[M]. p \<in> s \<longleftrightarrow> rtran_closure_mem(M,A,r,p))" *) 

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

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

91 
rtran_closure_fm :: "[i,i]=>i" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

92 
"rtran_closure_fm(r,s) == 
13348  93 
Forall(Implies(field_fm(succ(r),0), 
94 
Forall(Iff(Member(0,succ(succ(s))), 

95 
rtran_closure_mem_fm(1,succ(succ(r)),0)))))" 

96 

97 
lemma rtran_closure_type [TC]: 

98 
"[ x \<in> nat; y \<in> nat ] ==> rtran_closure_fm(x,y) \<in> formula" 

13428  99 
by (simp add: rtran_closure_fm_def) 
13348  100 

101 
lemma sats_rtran_closure_fm [simp]: 

102 
"[ x \<in> nat; y \<in> nat; env \<in> list(A)] 

46823  103 
==> sats(A, rtran_closure_fm(x,y), env) \<longleftrightarrow> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset

104 
rtran_closure(##A, nth(x,env), nth(y,env))" 
13348  105 
by (simp add: rtran_closure_fm_def rtran_closure_def) 
106 

107 
lemma rtran_closure_iff_sats: 

13428  108 
"[ nth(i,env) = x; nth(j,env) = y; 
13348  109 
i \<in> nat; j \<in> nat; env \<in> list(A)] 
46823  110 
==> rtran_closure(##A, x, y) \<longleftrightarrow> sats(A, rtran_closure_fm(i,j), env)" 
13348  111 
by simp 
112 

113 
theorem rtran_closure_reflection: 

13428  114 
"REFLECTS[\<lambda>x. rtran_closure(L,f(x),g(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset

115 
\<lambda>i x. rtran_closure(##Lset(i),f(x),g(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

116 
apply (simp only: rtran_closure_def) 
13348  117 
apply (intro FOL_reflections function_reflections rtran_closure_mem_reflection) 
118 
done 

119 

120 

121 
subsubsection{*Transitive Closure of a Relation, Internalized*} 

122 

123 
(* "tran_closure(M,r,t) == 

124 
\<exists>s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)" *) 

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

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

126 
tran_closure_fm :: "[i,i]=>i" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

127 
"tran_closure_fm(r,s) == 
13348  128 
Exists(And(rtran_closure_fm(succ(r),0), composition_fm(succ(r),0,succ(s))))" 
129 

130 
lemma tran_closure_type [TC]: 

131 
"[ x \<in> nat; y \<in> nat ] ==> tran_closure_fm(x,y) \<in> formula" 

13428  132 
by (simp add: tran_closure_fm_def) 
13348  133 

134 
lemma sats_tran_closure_fm [simp]: 

135 
"[ x \<in> nat; y \<in> nat; env \<in> list(A)] 

46823  136 
==> sats(A, tran_closure_fm(x,y), env) \<longleftrightarrow> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset

137 
tran_closure(##A, nth(x,env), nth(y,env))" 
13348  138 
by (simp add: tran_closure_fm_def tran_closure_def) 
139 

140 
lemma tran_closure_iff_sats: 

13428  141 
"[ nth(i,env) = x; nth(j,env) = y; 
13348  142 
i \<in> nat; j \<in> nat; env \<in> list(A)] 
46823  143 
==> tran_closure(##A, x, y) \<longleftrightarrow> sats(A, tran_closure_fm(i,j), env)" 
13348  144 
by simp 
145 

146 
theorem tran_closure_reflection: 

13428  147 
"REFLECTS[\<lambda>x. tran_closure(L,f(x),g(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset

148 
\<lambda>i x. tran_closure(##Lset(i),f(x),g(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

149 
apply (simp only: tran_closure_def) 
13428  150 
apply (intro FOL_reflections function_reflections 
13348  151 
rtran_closure_reflection composition_reflection) 
152 
done 

153 

154 

13506  155 
subsubsection{*Separation for the Proof of @{text "wellfounded_on_trancl"}*} 
13348  156 

157 
lemma wellfounded_trancl_reflects: 

13428  158 
"REFLECTS[\<lambda>x. \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L]. 
159 
w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp, 

160 
\<lambda>i x. \<exists>w \<in> Lset(i). \<exists>wx \<in> Lset(i). \<exists>rp \<in> Lset(i). 

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset

161 
w \<in> Z & pair(##Lset(i),w,x,wx) & tran_closure(##Lset(i),r,rp) & 
13348  162 
wx \<in> rp]" 
13428  163 
by (intro FOL_reflections function_reflections fun_plus_reflections 
13348  164 
tran_closure_reflection) 
165 

166 
lemma wellfounded_trancl_separation: 

13428  167 
"[ L(r); L(Z) ] ==> 
168 
separation (L, \<lambda>x. 

169 
\<exists>w[L]. \<exists>wx[L]. \<exists>rp[L]. 

170 
w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp)" 

13687  171 
apply (rule gen_separation_multi [OF wellfounded_trancl_reflects, of "{r,Z}"], 
172 
auto) 

173 
apply (rule_tac env="[r,Z]" in DPow_LsetI) 

13348  174 
apply (rule sep_rules tran_closure_iff_sats  simp)+ 
175 
done 

176 

13363  177 

178 
subsubsection{*Instantiating the locale @{text M_trancl}*} 

13428  179 

13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset

180 
lemma M_trancl_axioms_L: "M_trancl_axioms(L)" 
13428  181 
apply (rule M_trancl_axioms.intro) 
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset

182 
apply (assumption  rule rtrancl_separation wellfounded_trancl_separation)+ 
13428  183 
done 
13363  184 

13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset

185 
theorem M_trancl_L: "PROP M_trancl(L)" 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset

186 
by (rule M_trancl.intro [OF M_basic_L M_trancl_axioms_L]) 
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset

187 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29223
diff
changeset

188 
interpretation L?: M_trancl L by (rule M_trancl_L) 
13363  189 

190 

13428  191 
subsection{*@{term L} is Closed Under the Operator @{term list}*} 
13363  192 

13386  193 
subsubsection{*Instances of Replacement for Lists*} 
194 

13363  195 
lemma list_replacement1_Reflects: 
196 
"REFLECTS 

197 
[\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and> 

198 
is_wfrec(L, iterates_MH(L, is_list_functor(L,A), 0), memsn, u, y)), 

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset

199 
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) \<and> 
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset

200 
is_wfrec(##Lset(i), 
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset

201 
iterates_MH(##Lset(i), 
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset

202 
is_list_functor(##Lset(i), A), 0), memsn, u, y))]" 
13428  203 
by (intro FOL_reflections function_reflections is_wfrec_reflection 
204 
iterates_MH_reflection list_functor_reflection) 

13363  205 

13441  206 

13428  207 
lemma list_replacement1: 
13363  208 
"L(A) ==> iterates_replacement(L, is_list_functor(L,A), 0)" 
209 
apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) 

13428  210 
apply (rule strong_replacementI) 
13566  211 
apply (rule_tac u="{B,A,n,0,Memrel(succ(n))}" 
13687  212 
in gen_separation_multi [OF list_replacement1_Reflects], 
213 
auto simp add: nonempty) 

214 
apply (rule_tac env="[B,A,n,0,Memrel(succ(n))]" in DPow_LsetI) 

13434  215 
apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats 
13441  216 
is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats  simp)+ 
13363  217 
done 
218 

13441  219 

13363  220 
lemma list_replacement2_Reflects: 
221 
"REFLECTS 

13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

222 
[\<lambda>x. \<exists>u[L]. u \<in> B & u \<in> nat & 
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

223 
is_iterates(L, is_list_functor(L, A), 0, u, x), 
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

224 
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & u \<in> nat & 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset

225 
is_iterates(##Lset(i), is_list_functor(##Lset(i), A), 0, u, x)]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

226 
by (intro FOL_reflections 
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

227 
is_iterates_reflection list_functor_reflection) 
13363  228 

13428  229 
lemma list_replacement2: 
230 
"L(A) ==> strong_replacement(L, 

13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

231 
\<lambda>n y. n\<in>nat & is_iterates(L, is_list_functor(L,A), 0, n, y))" 
13428  232 
apply (rule strong_replacementI) 
13566  233 
apply (rule_tac u="{A,B,0,nat}" 
13687  234 
in gen_separation_multi [OF list_replacement2_Reflects], 
235 
auto simp add: L_nat nonempty) 

236 
apply (rule_tac env="[A,B,0,nat]" in DPow_LsetI) 

13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

237 
apply (rule sep_rules list_functor_iff_sats is_iterates_iff_sats  simp)+ 
13363  238 
done 
239 

13386  240 

13428  241 
subsection{*@{term L} is Closed Under the Operator @{term formula}*} 
13386  242 

243 
subsubsection{*Instances of Replacement for Formulas*} 

244 

13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

245 
(*FIXME: could prove a lemma iterates_replacementI to eliminate the 
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

246 
need to expand iterates_replacement and wfrec_replacement*) 
13386  247 
lemma formula_replacement1_Reflects: 
248 
"REFLECTS 

13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

249 
[\<lambda>x. \<exists>u[L]. u \<in> B & (\<exists>y[L]. pair(L,u,y,x) & 
13386  250 
is_wfrec(L, iterates_MH(L, is_formula_functor(L), 0), memsn, u, y)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset

251 
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) & 
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset

252 
is_wfrec(##Lset(i), 
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset

253 
iterates_MH(##Lset(i), 
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset

254 
is_formula_functor(##Lset(i)), 0), memsn, u, y))]" 
13428  255 
by (intro FOL_reflections function_reflections is_wfrec_reflection 
256 
iterates_MH_reflection formula_functor_reflection) 

13386  257 

13428  258 
lemma formula_replacement1: 
13386  259 
"iterates_replacement(L, is_formula_functor(L), 0)" 
260 
apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) 

13428  261 
apply (rule strong_replacementI) 
13566  262 
apply (rule_tac u="{B,n,0,Memrel(succ(n))}" 
13687  263 
in gen_separation_multi [OF formula_replacement1_Reflects], 
264 
auto simp add: nonempty) 

265 
apply (rule_tac env="[n,B,0,Memrel(succ(n))]" in DPow_LsetI) 

13434  266 
apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats 
13441  267 
is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats  simp)+ 
13386  268 
done 
269 

270 
lemma formula_replacement2_Reflects: 

271 
"REFLECTS 

13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

272 
[\<lambda>x. \<exists>u[L]. u \<in> B & u \<in> nat & 
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

273 
is_iterates(L, is_formula_functor(L), 0, u, x), 
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

274 
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & u \<in> nat & 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset

275 
is_iterates(##Lset(i), is_formula_functor(##Lset(i)), 0, u, x)]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

276 
by (intro FOL_reflections 
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

277 
is_iterates_reflection formula_functor_reflection) 
13386  278 

13428  279 
lemma formula_replacement2: 
280 
"strong_replacement(L, 

13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

281 
\<lambda>n y. n\<in>nat & is_iterates(L, is_formula_functor(L), 0, n, y))" 
13428  282 
apply (rule strong_replacementI) 
13566  283 
apply (rule_tac u="{B,0,nat}" 
13687  284 
in gen_separation_multi [OF formula_replacement2_Reflects], 
285 
auto simp add: nonempty L_nat) 

286 
apply (rule_tac env="[B,0,nat]" in DPow_LsetI) 

13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

287 
apply (rule sep_rules formula_functor_iff_sats is_iterates_iff_sats  simp)+ 
13386  288 
done 
289 

290 
text{*NB The proofs for type @{term formula} are virtually identical to those 

291 
for @{term "list(A)"}. It was a cutandpaste job! *} 

292 

13387  293 

13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset

294 
subsubsection{*The Formula @{term is_nth}, Internalized*} 
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset

295 

13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

296 
(* "is_nth(M,n,l,Z) == 
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

297 
\<exists>X[M]. is_iterates(M, is_tl(M), l, n, X) & is_hd(M,X,Z)" *) 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

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

299 
nth_fm :: "[i,i,i]=>i" where 
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset

300 
"nth_fm(n,l,Z) == 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

301 
Exists(And(is_iterates_fm(tl_fm(1,0), succ(l), succ(n), 0), 
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

302 
hd_fm(0,succ(Z))))" 
13493
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset

303 

5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset

304 
lemma nth_fm_type [TC]: 
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset

305 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] ==> nth_fm(x,y,z) \<in> formula" 
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset

306 
by (simp add: nth_fm_def) 
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset

307 

5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset

308 
lemma sats_nth_fm [simp]: 
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset

309 
"[ x < length(env); y \<in> nat; z \<in> nat; env \<in> list(A)] 
46823  310 
==> sats(A, nth_fm(x,y,z), env) \<longleftrightarrow> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset

311 
is_nth(##A, nth(x,env), nth(y,env), nth(z,env))" 
13493
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset

312 
apply (frule lt_length_in_nat, assumption) 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

313 
apply (simp add: nth_fm_def is_nth_def sats_is_iterates_fm) 
13493
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset

314 
done 
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset

315 

5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset

316 
lemma nth_iff_sats: 
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset

317 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset

318 
i < length(env); j \<in> nat; k \<in> nat; env \<in> list(A)] 
46823  319 
==> is_nth(##A, x, y, z) \<longleftrightarrow> sats(A, nth_fm(i,j,k), env)" 
13493
5aa68c051725
Lots of new results concerning recursive datatypes, towards absoluteness of
paulson
parents:
13441
diff
changeset

320 
by (simp add: sats_nth_fm) 
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset

321 

01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset

322 
theorem nth_reflection: 
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset

323 
"REFLECTS[\<lambda>x. is_nth(L, f(x), g(x), h(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset

324 
\<lambda>i x. is_nth(##Lset(i), f(x), g(x), h(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

325 
apply (simp only: is_nth_def) 
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

326 
apply (intro FOL_reflections is_iterates_reflection 
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

327 
hd_reflection tl_reflection) 
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset

328 
done 
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset

329 

01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset

330 

13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset

331 
subsubsection{*An Instance of Replacement for @{term nth}*} 
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset

332 

13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

333 
(*FIXME: could prove a lemma iterates_replacementI to eliminate the 
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

334 
need to expand iterates_replacement and wfrec_replacement*) 
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset

335 
lemma nth_replacement_Reflects: 
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset

336 
"REFLECTS 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

337 
[\<lambda>x. \<exists>u[L]. u \<in> B & (\<exists>y[L]. pair(L,u,y,x) & 
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset

338 
is_wfrec(L, iterates_MH(L, is_tl(L), z), memsn, u, y)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset

339 
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) & 
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset

340 
is_wfrec(##Lset(i), 
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset

341 
iterates_MH(##Lset(i), 
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset

342 
is_tl(##Lset(i)), z), memsn, u, y))]" 
13428  343 
by (intro FOL_reflections function_reflections is_wfrec_reflection 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

344 
iterates_MH_reflection tl_reflection) 
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset

345 

13428  346 
lemma nth_replacement: 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

347 
"L(w) ==> iterates_replacement(L, is_tl(L), w)" 
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset

348 
apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) 
13428  349 
apply (rule strong_replacementI) 
13687  350 
apply (rule_tac u="{B,w,Memrel(succ(n))}" 
351 
in gen_separation_multi [OF nth_replacement_Reflects], 

352 
auto) 

353 
apply (rule_tac env="[B,w,Memrel(succ(n))]" in DPow_LsetI) 

13434  354 
apply (rule sep_rules is_nat_case_iff_sats tl_iff_sats 
13441  355 
is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats  simp)+ 
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset

356 
done 
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset

357 

13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset

358 

af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset

359 
subsubsection{*Instantiating the locale @{text M_datatypes}*} 
13428  360 

13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset

361 
lemma M_datatypes_axioms_L: "M_datatypes_axioms(L)" 
13428  362 
apply (rule M_datatypes_axioms.intro) 
363 
apply (assumption  rule 

364 
list_replacement1 list_replacement2 

365 
formula_replacement1 formula_replacement2 

366 
nth_replacement)+ 

367 
done 

13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset

368 

13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset

369 
theorem M_datatypes_L: "PROP M_datatypes(L)" 
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset

370 
apply (rule M_datatypes.intro) 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset

371 
apply (rule M_trancl_L) 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset

372 
apply (rule M_datatypes_axioms_L) 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset

373 
done 
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset

374 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29223
diff
changeset

375 
interpretation L?: M_datatypes L by (rule M_datatypes_L) 
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset

376 

af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset

377 

13428  378 
subsection{*@{term L} is Closed Under the Operator @{term eclose}*} 
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset

379 

af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset

380 
subsubsection{*Instances of Replacement for @{term eclose}*} 
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset

381 

af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset

382 
lemma eclose_replacement1_Reflects: 
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset

383 
"REFLECTS 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

384 
[\<lambda>x. \<exists>u[L]. u \<in> B & (\<exists>y[L]. pair(L,u,y,x) & 
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset

385 
is_wfrec(L, iterates_MH(L, big_union(L), A), memsn, u, y)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset

386 
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) & 
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset

387 
is_wfrec(##Lset(i), 
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset

388 
iterates_MH(##Lset(i), big_union(##Lset(i)), A), 
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset

389 
memsn, u, y))]" 
13428  390 
by (intro FOL_reflections function_reflections is_wfrec_reflection 
391 
iterates_MH_reflection) 

13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset

392 

13428  393 
lemma eclose_replacement1: 
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset

394 
"L(A) ==> iterates_replacement(L, big_union(L), A)" 
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset

395 
apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) 
13428  396 
apply (rule strong_replacementI) 
13566  397 
apply (rule_tac u="{B,A,n,Memrel(succ(n))}" 
13687  398 
in gen_separation_multi [OF eclose_replacement1_Reflects], auto) 
399 
apply (rule_tac env="[B,A,n,Memrel(succ(n))]" in DPow_LsetI) 

13434  400 
apply (rule sep_rules iterates_MH_iff_sats is_nat_case_iff_sats 
13441  401 
is_wfrec_iff_sats big_union_iff_sats quasinat_iff_sats  simp)+ 
13409
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset

402 
done 
d4ea094c650e
Relativization and Separation for the function "nth"
paulson
parents:
13398
diff
changeset

403 

13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset

404 

af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset

405 
lemma eclose_replacement2_Reflects: 
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset

406 
"REFLECTS 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

407 
[\<lambda>x. \<exists>u[L]. u \<in> B & u \<in> nat & 
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

408 
is_iterates(L, big_union(L), A, u, x), 
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

409 
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & u \<in> nat & 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset

410 
is_iterates(##Lset(i), big_union(##Lset(i)), A, u, x)]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

411 
by (intro FOL_reflections function_reflections is_iterates_reflection) 
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset

412 

13428  413 
lemma eclose_replacement2: 
414 
"L(A) ==> strong_replacement(L, 

13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

415 
\<lambda>n y. n\<in>nat & is_iterates(L, big_union(L), A, n, y))" 
13428  416 
apply (rule strong_replacementI) 
13566  417 
apply (rule_tac u="{A,B,nat}" 
13687  418 
in gen_separation_multi [OF eclose_replacement2_Reflects], 
419 
auto simp add: L_nat) 

420 
apply (rule_tac env="[A,B,nat]" in DPow_LsetI) 

13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13651
diff
changeset

421 
apply (rule sep_rules is_iterates_iff_sats big_union_iff_sats  simp)+ 
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset

422 
done 
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset

423 

af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset

424 

af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset

425 
subsubsection{*Instantiating the locale @{text M_eclose}*} 
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset

426 

13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset

427 
lemma M_eclose_axioms_L: "M_eclose_axioms(L)" 
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset

428 
apply (rule M_eclose_axioms.intro) 
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset

429 
apply (assumption  rule eclose_replacement1 eclose_replacement2)+ 
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset

430 
done 
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset

431 

13428  432 
theorem M_eclose_L: "PROP M_eclose(L)" 
433 
apply (rule M_eclose.intro) 

19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset

434 
apply (rule M_datatypes_L) 
13437
01b3fc0cc1b8
separate "axioms" proofs: more flexible for locale reasoning
paulson
parents:
13434
diff
changeset

435 
apply (rule M_eclose_axioms_L) 
13428  436 
done 
13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset

437 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29223
diff
changeset

438 
interpretation L?: M_eclose L by (rule M_eclose_L) 
15766  439 

13422
af9bc8d87a75
Added the assumption nth_replacement to locale M_datatypes.
paulson
parents:
13418
diff
changeset

440 

13348  441 
end 