28 fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) & |
28 fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) & |
29 (\<forall>j[M]. j\<in>n --> |
29 (\<forall>j[M]. j\<in>n --> |
30 (\<exists>fj[M]. \<exists>sj[M]. \<exists>fsj[M]. \<exists>ffp[M]. |
30 (\<exists>fj[M]. \<exists>sj[M]. \<exists>fsj[M]. \<exists>ffp[M]. |
31 fun_apply(M,f,j,fj) & successor(M,j,sj) & |
31 fun_apply(M,f,j,fj) & successor(M,j,sj) & |
32 fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \<in> r)))"*) |
32 fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \<in> r)))"*) |
33 constdefs rtran_closure_mem_fm :: "[i,i,i]=>i" |
33 definition rtran_closure_mem_fm :: "[i,i,i]=>i" |
34 "rtran_closure_mem_fm(A,r,p) == |
34 "rtran_closure_mem_fm(A,r,p) == |
35 Exists(Exists(Exists( |
35 Exists(Exists(Exists( |
36 And(omega_fm(2), |
36 And(omega_fm(2), |
37 And(Member(1,2), |
37 And(Member(1,2), |
38 And(succ_fm(1,0), |
38 And(succ_fm(1,0), |
85 subsubsection{*Reflexive/Transitive Closure, Internalized*} |
85 subsubsection{*Reflexive/Transitive Closure, Internalized*} |
86 |
86 |
87 (* "rtran_closure(M,r,s) == |
87 (* "rtran_closure(M,r,s) == |
88 \<forall>A[M]. is_field(M,r,A) --> |
88 \<forall>A[M]. is_field(M,r,A) --> |
89 (\<forall>p[M]. p \<in> s <-> rtran_closure_mem(M,A,r,p))" *) |
89 (\<forall>p[M]. p \<in> s <-> rtran_closure_mem(M,A,r,p))" *) |
90 constdefs rtran_closure_fm :: "[i,i]=>i" |
90 definition rtran_closure_fm :: "[i,i]=>i" |
91 "rtran_closure_fm(r,s) == |
91 "rtran_closure_fm(r,s) == |
92 Forall(Implies(field_fm(succ(r),0), |
92 Forall(Implies(field_fm(succ(r),0), |
93 Forall(Iff(Member(0,succ(succ(s))), |
93 Forall(Iff(Member(0,succ(succ(s))), |
94 rtran_closure_mem_fm(1,succ(succ(r)),0)))))" |
94 rtran_closure_mem_fm(1,succ(succ(r)),0)))))" |
95 |
95 |
119 |
119 |
120 subsubsection{*Transitive Closure of a Relation, Internalized*} |
120 subsubsection{*Transitive Closure of a Relation, Internalized*} |
121 |
121 |
122 (* "tran_closure(M,r,t) == |
122 (* "tran_closure(M,r,t) == |
123 \<exists>s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)" *) |
123 \<exists>s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)" *) |
124 constdefs tran_closure_fm :: "[i,i]=>i" |
124 definition tran_closure_fm :: "[i,i]=>i" |
125 "tran_closure_fm(r,s) == |
125 "tran_closure_fm(r,s) == |
126 Exists(And(rtran_closure_fm(succ(r),0), composition_fm(succ(r),0,succ(s))))" |
126 Exists(And(rtran_closure_fm(succ(r),0), composition_fm(succ(r),0,succ(s))))" |
127 |
127 |
128 lemma tran_closure_type [TC]: |
128 lemma tran_closure_type [TC]: |
129 "[| x \<in> nat; y \<in> nat |] ==> tran_closure_fm(x,y) \<in> formula" |
129 "[| x \<in> nat; y \<in> nat |] ==> tran_closure_fm(x,y) \<in> formula" |
291 |
291 |
292 subsubsection{*The Formula @{term is_nth}, Internalized*} |
292 subsubsection{*The Formula @{term is_nth}, Internalized*} |
293 |
293 |
294 (* "is_nth(M,n,l,Z) == |
294 (* "is_nth(M,n,l,Z) == |
295 \<exists>X[M]. is_iterates(M, is_tl(M), l, n, X) & is_hd(M,X,Z)" *) |
295 \<exists>X[M]. is_iterates(M, is_tl(M), l, n, X) & is_hd(M,X,Z)" *) |
296 constdefs nth_fm :: "[i,i,i]=>i" |
296 definition nth_fm :: "[i,i,i]=>i" |
297 "nth_fm(n,l,Z) == |
297 "nth_fm(n,l,Z) == |
298 Exists(And(is_iterates_fm(tl_fm(1,0), succ(l), succ(n), 0), |
298 Exists(And(is_iterates_fm(tl_fm(1,0), succ(l), succ(n), 0), |
299 hd_fm(0,succ(Z))))" |
299 hd_fm(0,succ(Z))))" |
300 |
300 |
301 lemma nth_fm_type [TC]: |
301 lemma nth_fm_type [TC]: |