1.1 --- a/src/ZF/Constructible/WFrec.thy Tue Sep 10 16:47:17 2002 +0200
1.2 +++ b/src/ZF/Constructible/WFrec.thy Tue Sep 10 16:51:31 2002 +0200
1.3 @@ -74,7 +74,7 @@
1.4
1.5 subsection{*Reworking of the Recursion Theory Within @{term M}*}
1.6
1.7 -lemma (in M_axioms) is_recfun_separation':
1.8 +lemma (in M_basic) is_recfun_separation':
1.9 "[| f \<in> r -`` {a} \<rightarrow> range(f); g \<in> r -`` {b} \<rightarrow> range(g);
1.10 M(r); M(f); M(g); M(a); M(b) |]
1.11 ==> separation(M, \<lambda>x. \<not> (\<langle>x, a\<rangle> \<in> r \<longrightarrow> \<langle>x, b\<rangle> \<in> r \<longrightarrow> f ` x = g ` x))"
1.12 @@ -89,7 +89,7 @@
1.13 The last three M-premises are redundant because of @{term "M(r)"},
1.14 but without them we'd have to undertake
1.15 more work to set up the induction formula.*}
1.16 -lemma (in M_axioms) is_recfun_equal [rule_format]:
1.17 +lemma (in M_basic) is_recfun_equal [rule_format]:
1.18 "[|is_recfun(r,a,H,f); is_recfun(r,b,H,g);
1.19 wellfounded(M,r); trans(r);
1.20 M(f); M(g); M(r); M(x); M(a); M(b) |]
1.21 @@ -112,7 +112,7 @@
1.22 apply (blast intro: transD sym)
1.23 done
1.24
1.25 -lemma (in M_axioms) is_recfun_cut:
1.26 +lemma (in M_basic) is_recfun_cut:
1.27 "[|is_recfun(r,a,H,f); is_recfun(r,b,H,g);
1.28 wellfounded(M,r); trans(r);
1.29 M(f); M(g); M(r); <b,a> \<in> r |]
1.30 @@ -124,7 +124,7 @@
1.31 apply (blast intro: is_recfun_equal transD dest: transM)
1.32 done
1.33
1.34 -lemma (in M_axioms) is_recfun_functional:
1.35 +lemma (in M_basic) is_recfun_functional:
1.36 "[|is_recfun(r,a,H,f); is_recfun(r,a,H,g);
1.37 wellfounded(M,r); trans(r); M(f); M(g); M(r) |] ==> f=g"
1.38 apply (rule fun_extension)
1.39 @@ -133,7 +133,7 @@
1.40 done
1.41
1.42 text{*Tells us that @{text is_recfun} can (in principle) be relativized.*}
1.43 -lemma (in M_axioms) is_recfun_relativize:
1.44 +lemma (in M_basic) is_recfun_relativize:
1.45 "[| M(r); M(f); \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |]
1.46 ==> is_recfun(r,a,H,f) <->
1.47 (\<forall>z[M]. z \<in> f <->
1.48 @@ -154,7 +154,7 @@
1.49 apply (simp add: is_recfun_imp_function function_restrictI)
1.50 done
1.51
1.52 -lemma (in M_axioms) is_recfun_restrict:
1.53 +lemma (in M_basic) is_recfun_restrict:
1.54 "[| wellfounded(M,r); trans(r); is_recfun(r,x,H,f); \<langle>y,x\<rangle> \<in> r;
1.55 M(r); M(f);
1.56 \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |]
1.57 @@ -171,7 +171,7 @@
1.58 apply (blast intro: apply_recfun dest: transD)
1.59 done
1.60
1.61 -lemma (in M_axioms) restrict_Y_lemma:
1.62 +lemma (in M_basic) restrict_Y_lemma:
1.63 "[| wellfounded(M,r); trans(r); M(r);
1.64 \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)); M(Y);
1.65 \<forall>b[M].
1.66 @@ -201,7 +201,7 @@
1.67 done
1.68
1.69 text{*For typical applications of Replacement for recursive definitions*}
1.70 -lemma (in M_axioms) univalent_is_recfun:
1.71 +lemma (in M_basic) univalent_is_recfun:
1.72 "[|wellfounded(M,r); trans(r); M(r)|]
1.73 ==> univalent (M, A, \<lambda>x p.
1.74 \<exists>y[M]. p = \<langle>x,y\<rangle> & (\<exists>f[M]. is_recfun(r,x,H,f) & y = H(x,f)))"
1.75 @@ -212,7 +212,7 @@
1.76
1.77 text{*Proof of the inductive step for @{text exists_is_recfun}, since
1.78 we must prove two versions.*}
1.79 -lemma (in M_axioms) exists_is_recfun_indstep:
1.80 +lemma (in M_basic) exists_is_recfun_indstep:
1.81 "[|\<forall>y. \<langle>y, a1\<rangle> \<in> r --> (\<exists>f[M]. is_recfun(r, y, H, f));
1.82 wellfounded(M,r); trans(r); M(r); M(a1);
1.83 strong_replacement(M, \<lambda>x z.
1.84 @@ -245,7 +245,7 @@
1.85
1.86 text{*Relativized version, when we have the (currently weaker) premise
1.87 @{term "wellfounded(M,r)"}*}
1.88 -lemma (in M_axioms) wellfounded_exists_is_recfun:
1.89 +lemma (in M_basic) wellfounded_exists_is_recfun:
1.90 "[|wellfounded(M,r); trans(r);
1.91 separation(M, \<lambda>x. ~ (\<exists>f[M]. is_recfun(r, x, H, f)));
1.92 strong_replacement(M, \<lambda>x z.
1.93 @@ -257,7 +257,7 @@
1.94 apply (rule exists_is_recfun_indstep, assumption+)
1.95 done
1.96
1.97 -lemma (in M_axioms) wf_exists_is_recfun [rule_format]:
1.98 +lemma (in M_basic) wf_exists_is_recfun [rule_format]:
1.99 "[|wf(r); trans(r); M(r);
1.100 strong_replacement(M, \<lambda>x z.
1.101 \<exists>y[M]. \<exists>g[M]. pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g));
1.102 @@ -291,7 +291,7 @@
1.103 strong_replacement(M,
1.104 \<lambda>x z. \<exists>y[M]. pair(M,x,y,z) & is_wfrec(M,MH,r,x,y))"
1.105
1.106 -lemma (in M_axioms) is_recfun_abs:
1.107 +lemma (in M_basic) is_recfun_abs:
1.108 "[| \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)); M(r); M(a); M(f);
1.109 relativize2(M,MH,H) |]
1.110 ==> M_is_recfun(M,MH,r,a,f) <-> is_recfun(r,a,H,f)"
1.111 @@ -306,7 +306,7 @@
1.112 ==> M_is_recfun(M,MH,r,a,f) <-> M_is_recfun(M,MH',r',a',f')"
1.113 by (simp add: M_is_recfun_def)
1.114
1.115 -lemma (in M_axioms) is_wfrec_abs:
1.116 +lemma (in M_basic) is_wfrec_abs:
1.117 "[| \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g));
1.118 relativize2(M,MH,H); M(r); M(a); M(z) |]
1.119 ==> is_wfrec(M,MH,r,a,z) <->
1.120 @@ -314,7 +314,7 @@
1.121 by (simp add: is_wfrec_def relativize2_def is_recfun_abs)
1.122
1.123 text{*Relating @{term wfrec_replacement} to native constructs*}
1.124 -lemma (in M_axioms) wfrec_replacement':
1.125 +lemma (in M_basic) wfrec_replacement':
1.126 "[|wfrec_replacement(M,MH,r);
1.127 \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g));
1.128 relativize2(M,MH,H); M(r)|]
1.129 @@ -381,7 +381,7 @@
1.130 fun_apply(M,f,j,fj) & fj = k"
1.131
1.132
1.133 -locale M_ord_arith = M_axioms +
1.134 +locale M_ord_arith = M_basic +
1.135 assumes oadd_strong_replacement:
1.136 "[| M(i); M(j) |] ==>
1.137 strong_replacement(M,