src/ZF/Constructible/Datatype_absolute.thy
 changeset 13655 95b95cdb4704 parent 13647 7f6f0ffc45c3 child 13687 22dce9134953
```     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Fri Oct 18 09:53:18 2002 +0200
1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Fri Oct 18 17:50:13 2002 +0200
1.3 @@ -125,6 +125,11 @@
1.4        \<forall>n[M]. n\<in>nat -->
1.5           wfrec_replacement(M, iterates_MH(M,isF,v), Memrel(succ(n)))"
1.6
1.7 +  is_iterates :: "[i=>o, [i,i]=>o, i, i, i] => o"
1.8 +    "is_iterates(M,isF,v,n,Z) ==
1.9 +      \<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
1.10 +                       is_wfrec(M, iterates_MH(M,isF,v), msn, n, Z)"
1.11 +
1.12  lemma (in M_basic) iterates_MH_abs:
1.13    "[| relation1(M,isF,F); M(n); M(g); M(z) |]
1.14     ==> iterates_MH(M,isF,v,n,g,z) <-> z = nat_case(v, \<lambda>m. F(g`m), n)"
1.15 @@ -140,11 +145,10 @@
1.16  theorem (in M_trancl) iterates_abs:
1.17    "[| iterates_replacement(M,isF,v); relation1(M,isF,F);
1.18        n \<in> nat; M(v); M(z); \<forall>x[M]. M(F(x)) |]
1.19 -   ==> is_wfrec(M, iterates_MH(M,isF,v), Memrel(succ(n)), n, z) <->
1.20 -       z = iterates(F,n,v)"
1.21 +   ==> is_iterates(M,isF,v,n,z) <-> z = iterates(F,n,v)"
1.22  apply (frule iterates_imp_wfrec_replacement, assumption+)
1.23  apply (simp add: wf_Memrel trans_Memrel relation_Memrel nat_into_M
1.24 -                 relation2_def iterates_MH_abs
1.25 +                 is_iterates_def relation2_def iterates_MH_abs
1.26                   iterates_nat_def recursor_def transrec_def
1.27                   eclose_sing_Ord_eq nat_into_M
1.28           trans_wfrec_abs [of _ _ _ _ "\<lambda>n g. nat_case(v, \<lambda>m. F(g`m), n)"])
1.29 @@ -338,10 +342,8 @@
1.30  constdefs
1.31    is_list_N :: "[i=>o,i,i,i] => o"
1.32      "is_list_N(M,A,n,Z) ==
1.33 -      \<exists>zero[M]. \<exists>sn[M]. \<exists>msn[M].
1.34 -       empty(M,zero) &
1.35 -       successor(M,n,sn) & membership(M,sn,msn) &
1.36 -       is_wfrec(M, iterates_MH(M, is_list_functor(M,A),zero), msn, n, Z)"
1.37 +      \<exists>zero[M]. empty(M,zero) &
1.38 +                is_iterates(M, is_list_functor(M,A), zero, n, Z)"
1.39
1.40    mem_list :: "[i=>o,i,i] => o"
1.41      "mem_list(M,A,l) ==
1.42 @@ -442,11 +444,9 @@
1.43  constdefs
1.44    is_formula_N :: "[i=>o,i,i] => o"
1.45      "is_formula_N(M,n,Z) ==
1.46 -      \<exists>zero[M]. \<exists>sn[M]. \<exists>msn[M].
1.47 -       empty(M,zero) &
1.48 -       successor(M,n,sn) & membership(M,sn,msn) &
1.49 -       is_wfrec(M, iterates_MH(M, is_formula_functor(M),zero), msn, n, Z)"
1.50 -
1.51 +      \<exists>zero[M]. empty(M,zero) &
1.52 +                is_iterates(M, is_formula_functor(M), zero, n, Z)"
1.53 +
1.54
1.55  constdefs
1.56
1.57 @@ -459,40 +459,34 @@
1.58      "is_formula(M,Z) == \<forall>p[M]. p \<in> Z <-> mem_formula(M,p)"
1.59
1.60  locale M_datatypes = M_trancl +
1.61 - assumes list_replacement1:
1.62 + assumes list_replacement1:
1.63     "M(A) ==> iterates_replacement(M, is_list_functor(M,A), 0)"
1.64 -  and list_replacement2:
1.65 -   "M(A) ==> strong_replacement(M,
1.66 -         \<lambda>n y. n\<in>nat &
1.67 -               (\<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
1.68 -               is_wfrec(M, iterates_MH(M,is_list_functor(M,A), 0),
1.69 -                        msn, n, y)))"
1.70 -  and formula_replacement1:
1.71 +  and list_replacement2:
1.72 +   "M(A) ==> strong_replacement(M,
1.73 +         \<lambda>n y. n\<in>nat & is_iterates(M, is_list_functor(M,A), 0, n, y))"
1.74 +  and formula_replacement1:
1.75     "iterates_replacement(M, is_formula_functor(M), 0)"
1.76 -  and formula_replacement2:
1.77 -   "strong_replacement(M,
1.78 -         \<lambda>n y. n\<in>nat &
1.79 -               (\<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
1.80 -               is_wfrec(M, iterates_MH(M,is_formula_functor(M), 0),
1.81 -                        msn, n, y)))"
1.82 +  and formula_replacement2:
1.83 +   "strong_replacement(M,
1.84 +         \<lambda>n y. n\<in>nat & is_iterates(M, is_formula_functor(M), 0, n, y))"
1.85    and nth_replacement:
1.86     "M(l) ==> iterates_replacement(M, %l t. is_tl(M,l,t), l)"
1.87 -
1.88 +
1.89
1.90  subsubsection{*Absoluteness of the List Construction*}
1.91
1.92 -lemma (in M_datatypes) list_replacement2':
1.93 +lemma (in M_datatypes) list_replacement2':
1.94    "M(A) ==> strong_replacement(M, \<lambda>n y. n\<in>nat & y = (\<lambda>X. {0} + A * X)^n (0))"
1.95 -apply (insert list_replacement2 [of A])
1.96 -apply (rule strong_replacement_cong [THEN iffD1])
1.97 -apply (rule conj_cong [OF iff_refl iterates_abs [of "is_list_functor(M,A)"]])
1.98 -apply (simp_all add: list_replacement1 relation1_def)
1.99 +apply (insert list_replacement2 [of A])
1.100 +apply (rule strong_replacement_cong [THEN iffD1])
1.101 +apply (rule conj_cong [OF iff_refl iterates_abs [of "is_list_functor(M,A)"]])
1.102 +apply (simp_all add: list_replacement1 relation1_def)
1.103  done
1.104
1.105  lemma (in M_datatypes) list_closed [intro,simp]:
1.106       "M(A) ==> M(list(A))"
1.107  apply (insert list_replacement1)
1.108 -by  (simp add: RepFun_closed2 list_eq_Union
1.109 +by  (simp add: RepFun_closed2 list_eq_Union
1.110                 list_replacement2' relation1_def
1.111                 iterates_closed [of "is_list_functor(M,A)"])
1.112
1.113 @@ -500,7 +494,7 @@
1.114  lemmas (in M_datatypes) list_into_M = transM [OF _ list_closed]
1.115
1.116  lemma (in M_datatypes) list_N_abs [simp]:
1.117 -     "[|M(A); n\<in>nat; M(Z)|]
1.118 +     "[|M(A); n\<in>nat; M(Z)|]
1.119        ==> is_list_N(M,A,n,Z) <-> Z = list_N(A,n)"
1.120  apply (insert list_replacement1)
1.121  apply (simp add: is_list_N_def list_N_def relation1_def nat_into_M
1.122 @@ -518,7 +512,7 @@
1.123       "M(A) ==> mem_list(M,A,l) <-> l \<in> list(A)"
1.124  apply (insert list_replacement1)
1.125  apply (simp add: mem_list_def list_N_def relation1_def list_eq_Union
1.126 -                 iterates_closed [of "is_list_functor(M,A)"])
1.127 +                 iterates_closed [of "is_list_functor(M,A)"])
1.128  done
1.129
1.130  lemma (in M_datatypes) list_abs [simp]:
1.131 @@ -529,18 +523,18 @@
1.132
1.133  subsubsection{*Absoluteness of Formulas*}
1.134
1.135 -lemma (in M_datatypes) formula_replacement2':
1.136 +lemma (in M_datatypes) formula_replacement2':
1.137    "strong_replacement(M, \<lambda>n y. n\<in>nat & y = (\<lambda>X. ((nat*nat) + (nat*nat)) + (X*X + X))^n (0))"
1.138 -apply (insert formula_replacement2)
1.139 -apply (rule strong_replacement_cong [THEN iffD1])
1.140 -apply (rule conj_cong [OF iff_refl iterates_abs [of "is_formula_functor(M)"]])
1.141 -apply (simp_all add: formula_replacement1 relation1_def)
1.142 +apply (insert formula_replacement2)
1.143 +apply (rule strong_replacement_cong [THEN iffD1])
1.144 +apply (rule conj_cong [OF iff_refl iterates_abs [of "is_formula_functor(M)"]])
1.145 +apply (simp_all add: formula_replacement1 relation1_def)
1.146  done
1.147
1.148  lemma (in M_datatypes) formula_closed [intro,simp]:
1.149       "M(formula)"
1.150  apply (insert formula_replacement1)
1.151 -apply  (simp add: RepFun_closed2 formula_eq_Union
1.152 +apply  (simp add: RepFun_closed2 formula_eq_Union
1.153                    formula_replacement2' relation1_def
1.154                    iterates_closed [of "is_formula_functor(M)"])
1.155  done
1.156 @@ -548,11 +542,11 @@
1.157  lemmas (in M_datatypes) formula_into_M = transM [OF _ formula_closed]
1.158
1.159  lemma (in M_datatypes) formula_N_abs [simp]:
1.160 -     "[|n\<in>nat; M(Z)|]
1.161 +     "[|n\<in>nat; M(Z)|]
1.162        ==> is_formula_N(M,n,Z) <-> Z = formula_N(n)"
1.163  apply (insert formula_replacement1)
1.164  apply (simp add: is_formula_N_def formula_N_def relation1_def nat_into_M
1.165 -                 iterates_abs [of "is_formula_functor(M)" _
1.166 +                 iterates_abs [of "is_formula_functor(M)" _
1.167                                    "\<lambda>X. ((nat*nat) + (nat*nat)) + (X*X + X)"])
1.168  done
1.169
1.170 @@ -567,7 +561,7 @@
1.171       "mem_formula(M,l) <-> l \<in> formula"
1.172  apply (insert formula_replacement1)
1.173  apply (simp add: mem_formula_def relation1_def formula_eq_Union formula_N_def
1.174 -                 iterates_closed [of "is_formula_functor(M)"])
1.175 +                 iterates_closed [of "is_formula_functor(M)"])
1.176  done
1.177
1.178  lemma (in M_datatypes) formula_abs [simp]:
1.179 @@ -582,24 +576,21 @@
1.180  text{*Re-expresses eclose using "iterates"*}
1.181  lemma eclose_eq_Union:
1.182       "eclose(A) = (\<Union>n\<in>nat. Union^n (A))"
1.184 -apply (rule UN_cong)
1.186 +apply (rule UN_cong)
1.187  apply (rule refl)
1.188  apply (induct_tac n)
1.193  done
1.194
1.195  constdefs
1.196    is_eclose_n :: "[i=>o,i,i,i] => o"
1.197 -    "is_eclose_n(M,A,n,Z) ==
1.198 -      \<exists>sn[M]. \<exists>msn[M].
1.199 -       successor(M,n,sn) & membership(M,sn,msn) &
1.200 -       is_wfrec(M, iterates_MH(M, big_union(M), A), msn, n, Z)"
1.201 -
1.202 +    "is_eclose_n(M,A,n,Z) == is_iterates(M, big_union(M), A, n, Z)"
1.203 +
1.204    mem_eclose :: "[i=>o,i,i] => o"
1.205 -    "mem_eclose(M,A,l) ==
1.206 -      \<exists>n[M]. \<exists>eclosen[M].
1.207 +    "mem_eclose(M,A,l) ==
1.208 +      \<exists>n[M]. \<exists>eclosen[M].
1.209         finite_ordinal(M,n) & is_eclose_n(M,A,n,eclosen) & l \<in> eclosen"
1.210
1.211    is_eclose :: "[i=>o,i,i] => o"
1.212 @@ -607,27 +598,24 @@
1.213
1.214
1.215  locale M_eclose = M_datatypes +
1.216 - assumes eclose_replacement1:
1.217 + assumes eclose_replacement1:
1.218     "M(A) ==> iterates_replacement(M, big_union(M), A)"
1.219 -  and eclose_replacement2:
1.220 -   "M(A) ==> strong_replacement(M,
1.221 -         \<lambda>n y. n\<in>nat &
1.222 -               (\<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
1.223 -               is_wfrec(M, iterates_MH(M,big_union(M), A),
1.224 -                        msn, n, y)))"
1.225 +  and eclose_replacement2:
1.226 +   "M(A) ==> strong_replacement(M,
1.227 +         \<lambda>n y. n\<in>nat & is_iterates(M, big_union(M), A, n, y))"
1.228
1.229 -lemma (in M_eclose) eclose_replacement2':
1.230 +lemma (in M_eclose) eclose_replacement2':
1.231    "M(A) ==> strong_replacement(M, \<lambda>n y. n\<in>nat & y = Union^n (A))"
1.232 -apply (insert eclose_replacement2 [of A])
1.233 -apply (rule strong_replacement_cong [THEN iffD1])
1.234 -apply (rule conj_cong [OF iff_refl iterates_abs [of "big_union(M)"]])
1.235 -apply (simp_all add: eclose_replacement1 relation1_def)
1.236 +apply (insert eclose_replacement2 [of A])
1.237 +apply (rule strong_replacement_cong [THEN iffD1])
1.238 +apply (rule conj_cong [OF iff_refl iterates_abs [of "big_union(M)"]])
1.239 +apply (simp_all add: eclose_replacement1 relation1_def)
1.240  done
1.241
1.242  lemma (in M_eclose) eclose_closed [intro,simp]:
1.243       "M(A) ==> M(eclose(A))"
1.244  apply (insert eclose_replacement1)
1.245 -by  (simp add: RepFun_closed2 eclose_eq_Union
1.246 +by  (simp add: RepFun_closed2 eclose_eq_Union
1.247                 eclose_replacement2' relation1_def
1.248                 iterates_closed [of "big_union(M)"])
1.249
1.250 @@ -642,7 +630,7 @@
1.251       "M(A) ==> mem_eclose(M,A,l) <-> l \<in> eclose(A)"
1.252  apply (insert eclose_replacement1)
1.253  apply (simp add: mem_eclose_def relation1_def eclose_eq_Union
1.254 -                 iterates_closed [of "big_union(M)"])
1.255 +                 iterates_closed [of "big_union(M)"])
1.256  done
1.257
1.258  lemma (in M_eclose) eclose_abs [simp]:
1.259 @@ -652,54 +640,52 @@
1.260  done
1.261
1.262
1.263 -
1.264 -
1.265  subsection {*Absoluteness for @{term transrec}*}
1.266
1.267 -
1.268  text{* @{term "transrec(a,H) \<equiv> wfrec(Memrel(eclose({a})), a, H)"} *}
1.269  constdefs
1.270
1.271    is_transrec :: "[i=>o, [i,i,i]=>o, i, i] => o"
1.272 -   "is_transrec(M,MH,a,z) ==
1.273 -      \<exists>sa[M]. \<exists>esa[M]. \<exists>mesa[M].
1.274 +   "is_transrec(M,MH,a,z) ==
1.275 +      \<exists>sa[M]. \<exists>esa[M]. \<exists>mesa[M].
1.276         upair(M,a,a,sa) & is_eclose(M,sa,esa) & membership(M,esa,mesa) &
1.277         is_wfrec(M,MH,mesa,a,z)"
1.278
1.279    transrec_replacement :: "[i=>o, [i,i,i]=>o, i] => o"
1.280     "transrec_replacement(M,MH,a) ==
1.281 -      \<exists>sa[M]. \<exists>esa[M]. \<exists>mesa[M].
1.282 +      \<exists>sa[M]. \<exists>esa[M]. \<exists>mesa[M].
1.283         upair(M,a,a,sa) & is_eclose(M,sa,esa) & membership(M,esa,mesa) &
1.284         wfrec_replacement(M,MH,mesa)"
1.285
1.286 -text{*The condition @{term "Ord(i)"} lets us use the simpler
1.287 +text{*The condition @{term "Ord(i)"} lets us use the simpler
1.288    @{text "trans_wfrec_abs"} rather than @{text "trans_wfrec_abs"},
1.289    which I haven't even proved yet. *}
1.290  theorem (in M_eclose) transrec_abs:
1.291    "[|transrec_replacement(M,MH,i);  relation2(M,MH,H);
1.292       Ord(i);  M(i);  M(z);
1.293 -     \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|]
1.294 -   ==> is_transrec(M,MH,i,z) <-> z = transrec(i,H)"
1.295 +     \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|]
1.296 +   ==> is_transrec(M,MH,i,z) <-> z = transrec(i,H)"
1.297  by (simp add: trans_wfrec_abs transrec_replacement_def is_transrec_def
1.298         transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
1.299
1.300
1.301  theorem (in M_eclose) transrec_closed:
1.302       "[|transrec_replacement(M,MH,i);  relation2(M,MH,H);
1.303 -	Ord(i);  M(i);
1.304 -	\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|]
1.305 +	Ord(i);  M(i);
1.306 +	\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|]
1.307        ==> M(transrec(i,H))"
1.308  by (simp add: trans_wfrec_closed transrec_replacement_def is_transrec_def
1.309          transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
1.310
1.311
1.312  text{*Helps to prove instances of @{term transrec_replacement}*}
1.313 -lemma (in M_eclose) transrec_replacementI:
1.314 +lemma (in M_eclose) transrec_replacementI:
1.315     "[|M(a);
1.316 -    strong_replacement (M,
1.317 -                  \<lambda>x z. \<exists>y[M]. pair(M, x, y, z) \<and> is_wfrec(M,MH,Memrel(eclose({a})),x,y))|]
1.318 +      strong_replacement (M,
1.319 +                  \<lambda>x z. \<exists>y[M]. pair(M, x, y, z) &
1.320 +                               is_wfrec(M,MH,Memrel(eclose({a})),x,y))|]
1.321      ==> transrec_replacement(M,MH,a)"
1.322 -by (simp add: transrec_replacement_def wfrec_replacement_def)
1.323 +by (simp add: transrec_replacement_def wfrec_replacement_def)
1.324
1.325
1.326  subsection{*Absoluteness for the List Operator @{term length}*}
1.327 @@ -707,8 +693,8 @@
1.328
1.329  constdefs
1.330    is_length :: "[i=>o,i,i,i] => o"
1.331 -    "is_length(M,A,l,n) ==
1.332 -       \<exists>sn[M]. \<exists>list_n[M]. \<exists>list_sn[M].
1.333 +    "is_length(M,A,l,n) ==
1.334 +       \<exists>sn[M]. \<exists>list_n[M]. \<exists>list_sn[M].
1.335          is_list_N(M,A,n,list_n) & l \<notin> list_n &
1.336          successor(M,n,sn) & is_list_N(M,A,sn,list_sn) & l \<in> list_sn"
1.337
1.338 @@ -716,7 +702,7 @@
1.339  lemma (in M_datatypes) length_abs [simp]:
1.340       "[|M(A); l \<in> list(A); n \<in> nat|] ==> is_length(M,A,l,n) <-> n = length(l)"
1.341  apply (subgoal_tac "M(l) & M(n)")
1.342 - prefer 2 apply (blast dest: transM)
1.343 + prefer 2 apply (blast dest: transM)
1.345  apply (blast intro: list_imp_list_N nat_into_Ord list_N_imp_eq_length
1.346               dest: list_N_imp_length_lt)
1.347 @@ -725,29 +711,29 @@
1.348  text{*Proof is trivial since @{term length} returns natural numbers.*}
1.349  lemma (in M_trivial) length_closed [intro,simp]:
1.350       "l \<in> list(A) ==> M(length(l))"
1.353
1.354
1.355  subsection {*Absoluteness for the List Operator @{term nth}*}
1.356
1.357  lemma nth_eq_hd_iterates_tl [rule_format]:
1.358       "xs \<in> list(A) ==> \<forall>n \<in> nat. nth(n,xs) = hd' (tl'^n (xs))"
1.359 -apply (induct_tac xs)
1.360 -apply (simp add: iterates_tl_Nil hd'_Nil, clarify)
1.361 +apply (induct_tac xs)
1.362 +apply (simp add: iterates_tl_Nil hd'_Nil, clarify)
1.363  apply (erule natE)
1.365 -apply (simp add: tl'_Cons iterates_commute)
1.367 +apply (simp add: tl'_Cons iterates_commute)
1.368  done
1.369
1.370  lemma (in M_basic) iterates_tl'_closed:
1.371       "[|n \<in> nat; M(x)|] ==> M(tl'^n (x))"
1.372 -apply (induct_tac n, simp)
1.373 -apply (simp add: tl'_Cons tl'_closed)
1.374 +apply (induct_tac n, simp)
1.375 +apply (simp add: tl'_Cons tl'_closed)
1.376  done
1.377
1.378  text{*Immediate by type-checking*}
1.379  lemma (in M_datatypes) nth_closed [intro,simp]:
1.380 -     "[|xs \<in> list(A); n \<in> nat; M(A)|] ==> M(nth(n,xs))"
1.381 +     "[|xs \<in> list(A); n \<in> nat; M(A)|] ==> M(nth(n,xs))"
1.382  apply (case_tac "n < length(xs)")
1.383   apply (blast intro: nth_type transM)
1.384  apply (simp add: not_lt_iff_le nth_eq_0)
1.385 @@ -755,19 +741,16 @@
1.386
1.387  constdefs
1.388    is_nth :: "[i=>o,i,i,i] => o"
1.389 -    "is_nth(M,n,l,Z) ==
1.390 -      \<exists>X[M]. \<exists>sn[M]. \<exists>msn[M].
1.391 -       successor(M,n,sn) & membership(M,sn,msn) &
1.392 -       is_wfrec(M, iterates_MH(M, is_tl(M), l), msn, n, X) &
1.393 -       is_hd(M,X,Z)"
1.394 -
1.395 +    "is_nth(M,n,l,Z) ==
1.396 +      \<exists>X[M]. is_iterates(M, is_tl(M), l, n, X) & is_hd(M,X,Z)"
1.397 +
1.398  lemma (in M_datatypes) nth_abs [simp]:
1.399 -     "[|M(A); n \<in> nat; l \<in> list(A); M(Z)|]
1.400 +     "[|M(A); n \<in> nat; l \<in> list(A); M(Z)|]
1.401        ==> is_nth(M,n,l,Z) <-> Z = nth(n,l)"
1.402 -apply (subgoal_tac "M(l)")
1.403 +apply (subgoal_tac "M(l)")
1.404   prefer 2 apply (blast intro: transM)
1.405  apply (simp add: is_nth_def nth_eq_hd_iterates_tl nat_into_M
1.406 -                 tl'_closed iterates_tl'_closed
1.407 +                 tl'_closed iterates_tl'_closed
1.408                   iterates_abs [OF _ relation1_tl] nth_replacement)
1.409  done
1.410
1.411 @@ -786,7 +769,7 @@
1.412
1.413  lemma (in M_trivial) Member_in_M_iff [iff]:
1.414       "M(Member(x,y)) <-> M(x) & M(y)"
1.417
1.418  constdefs
1.419    is_Equal :: "[i=>o,i,i,i] => o"
1.420 @@ -799,7 +782,7 @@
1.421  by (simp add: is_Equal_def Equal_def)
1.422
1.423  lemma (in M_trivial) Equal_in_M_iff [iff]: "M(Equal(x,y)) <-> M(x) & M(y)"
1.426
1.427  constdefs
1.428    is_Nand :: "[i=>o,i,i,i] => o"
1.429 @@ -812,7 +795,7 @@
1.430  by (simp add: is_Nand_def Nand_def)
1.431
1.432  lemma (in M_trivial) Nand_in_M_iff [iff]: "M(Nand(x,y)) <-> M(x) & M(y)"
1.435
1.436  constdefs
1.437    is_Forall :: "[i=>o,i,i] => o"
1.438 @@ -836,7 +819,7 @@
1.439      --{* the instance of @{term formula_case} in @{term formula_rec}*}
1.440     "formula_rec_case(a,b,c,d,h) ==
1.441          formula_case (a, b,
1.442 -                \<lambda>u v. c(u, v, h ` succ(depth(u)) ` u,
1.443 +                \<lambda>u v. c(u, v, h ` succ(depth(u)) ` u,
1.444                                h ` succ(depth(v)) ` v),
1.445                  \<lambda>u. d(u, h ` succ(depth(u)) ` u))"
1.446
1.447 @@ -845,21 +828,21 @@
1.448  neither of which is absolute.*}
1.449  lemma (in M_trivial) formula_rec_eq:
1.450    "p \<in> formula ==>
1.451 -   formula_rec(a,b,c,d,p) =
1.452 +   formula_rec(a,b,c,d,p) =
1.453     transrec (succ(depth(p)),
1.454               \<lambda>x h. Lambda (formula, formula_rec_case(a,b,c,d,h))) ` p"
1.456  apply (induct_tac p)
1.457     txt{*Base case for @{term Member}*}
1.458 -   apply (subst transrec, simp add: formula.intros)
1.459 +   apply (subst transrec, simp add: formula.intros)
1.460    txt{*Base case for @{term Equal}*}
1.461    apply (subst transrec, simp add: formula.intros)
1.462   txt{*Inductive step for @{term Nand}*}
1.463 - apply (subst transrec)
1.464 + apply (subst transrec)
1.465   apply (simp add: succ_Un_distrib formula.intros)
1.466  txt{*Inductive step for @{term Forall}*}
1.467 -apply (subst transrec)
1.468 -apply (simp add: formula_imp_formula_N formula.intros)
1.469 +apply (subst transrec)
1.470 +apply (simp add: formula_imp_formula_N formula.intros)
1.471  done
1.472
1.473
1.474 @@ -867,8 +850,8 @@
1.475  constdefs
1.476
1.477    is_depth :: "[i=>o,i,i] => o"
1.478 -    "is_depth(M,p,n) ==
1.479 -       \<exists>sn[M]. \<exists>formula_n[M]. \<exists>formula_sn[M].
1.480 +    "is_depth(M,p,n) ==
1.481 +       \<exists>sn[M]. \<exists>formula_n[M]. \<exists>formula_sn[M].
1.482          is_formula_N(M,n,formula_n) & p \<notin> formula_n &
1.483          successor(M,n,sn) & is_formula_N(M,sn,formula_sn) & p \<in> formula_sn"
1.484
1.485 @@ -876,7 +859,7 @@
1.486  lemma (in M_datatypes) depth_abs [simp]:
1.487       "[|p \<in> formula; n \<in> nat|] ==> is_depth(M,p,n) <-> n = depth(p)"
1.488  apply (subgoal_tac "M(p) & M(n)")
1.489 - prefer 2 apply (blast dest: transM)
1.490 + prefer 2 apply (blast dest: transM)
1.492  apply (blast intro: formula_imp_formula_N nat_into_Ord formula_N_imp_eq_depth
1.493               dest: formula_N_imp_depth_lt)
1.494 @@ -885,43 +868,43 @@
1.495  text{*Proof is trivial since @{term depth} returns natural numbers.*}
1.496  lemma (in M_trivial) depth_closed [intro,simp]:
1.497       "p \<in> formula ==> M(depth(p))"
1.500
1.501
1.502  subsubsection{*@{term is_formula_case}: relativization of @{term formula_case}*}
1.503
1.504  constdefs
1.505
1.506 - is_formula_case ::
1.507 + is_formula_case ::
1.508      "[i=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i]=>o, i, i] => o"
1.509    --{*no constraint on non-formulas*}
1.510 -  "is_formula_case(M, is_a, is_b, is_c, is_d, p, z) ==
1.511 -      (\<forall>x[M]. \<forall>y[M]. finite_ordinal(M,x) --> finite_ordinal(M,y) -->
1.512 +  "is_formula_case(M, is_a, is_b, is_c, is_d, p, z) ==
1.513 +      (\<forall>x[M]. \<forall>y[M]. finite_ordinal(M,x) --> finite_ordinal(M,y) -->
1.514                        is_Member(M,x,y,p) --> is_a(x,y,z)) &
1.515 -      (\<forall>x[M]. \<forall>y[M]. finite_ordinal(M,x) --> finite_ordinal(M,y) -->
1.516 +      (\<forall>x[M]. \<forall>y[M]. finite_ordinal(M,x) --> finite_ordinal(M,y) -->
1.517                        is_Equal(M,x,y,p) --> is_b(x,y,z)) &
1.518 -      (\<forall>x[M]. \<forall>y[M]. mem_formula(M,x) --> mem_formula(M,y) -->
1.519 +      (\<forall>x[M]. \<forall>y[M]. mem_formula(M,x) --> mem_formula(M,y) -->
1.520                       is_Nand(M,x,y,p) --> is_c(x,y,z)) &
1.521        (\<forall>x[M]. mem_formula(M,x) --> is_Forall(M,x,p) --> is_d(x,z))"
1.522
1.523 -lemma (in M_datatypes) formula_case_abs [simp]:
1.524 -     "[| Relation2(M,nat,nat,is_a,a); Relation2(M,nat,nat,is_b,b);
1.525 -         Relation2(M,formula,formula,is_c,c); Relation1(M,formula,is_d,d);
1.526 -         p \<in> formula; M(z) |]
1.527 -      ==> is_formula_case(M,is_a,is_b,is_c,is_d,p,z) <->
1.528 +lemma (in M_datatypes) formula_case_abs [simp]:
1.529 +     "[| Relation2(M,nat,nat,is_a,a); Relation2(M,nat,nat,is_b,b);
1.530 +         Relation2(M,formula,formula,is_c,c); Relation1(M,formula,is_d,d);
1.531 +         p \<in> formula; M(z) |]
1.532 +      ==> is_formula_case(M,is_a,is_b,is_c,is_d,p,z) <->
1.533            z = formula_case(a,b,c,d,p)"
1.534  apply (simp add: formula_into_M is_formula_case_def)
1.535 -apply (erule formula.cases)
1.536 -   apply (simp_all add: Relation1_def Relation2_def)
1.537 +apply (erule formula.cases)
1.538 +   apply (simp_all add: Relation1_def Relation2_def)
1.539  done
1.540
1.541  lemma (in M_datatypes) formula_case_closed [intro,simp]:
1.542 -  "[|p \<in> formula;
1.543 -     \<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> M(a(x,y));
1.544 -     \<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> M(b(x,y));
1.545 -     \<forall>x[M]. \<forall>y[M]. x\<in>formula --> y\<in>formula --> M(c(x,y));
1.546 +  "[|p \<in> formula;
1.547 +     \<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> M(a(x,y));
1.548 +     \<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> M(b(x,y));
1.549 +     \<forall>x[M]. \<forall>y[M]. x\<in>formula --> y\<in>formula --> M(c(x,y));
1.550       \<forall>x[M]. x\<in>formula --> M(d(x))|] ==> M(formula_case(a,b,c,d,p))"
1.551 -by (erule formula.cases, simp_all)
1.552 +by (erule formula.cases, simp_all)
1.553
1.554
1.555  subsubsection {*Absoluteness for @{term formula_rec}: Final Results*}
1.556 @@ -930,7 +913,7 @@
1.557    is_formula_rec :: "[i=>o, [i,i,i]=>o, i, i] => o"
1.558      --{* predicate to relativize the functional @{term formula_rec}*}
1.559     "is_formula_rec(M,MH,p,z)  ==
1.560 -      \<exists>dp[M]. \<exists>i[M]. \<exists>f[M]. finite_ordinal(M,dp) & is_depth(M,p,dp) &
1.561 +      \<exists>dp[M]. \<exists>i[M]. \<exists>f[M]. finite_ordinal(M,dp) & is_depth(M,p,dp) &
1.562               successor(M,dp,i) & fun_apply(M,f,p,z) & is_transrec(M,MH,i,f)"
1.563
1.564
1.565 @@ -939,16 +922,16 @@
1.566  lemma (in M_datatypes) Relation1_formula_rec_case:
1.567       "[|Relation2(M, nat, nat, is_a, a);
1.568          Relation2(M, nat, nat, is_b, b);
1.569 -        Relation2 (M, formula, formula,
1.570 +        Relation2 (M, formula, formula,
1.571             is_c, \<lambda>u v. c(u, v, h`succ(depth(u))`u, h`succ(depth(v))`v));
1.572 -        Relation1(M, formula,
1.573 +        Relation1(M, formula,
1.574             is_d, \<lambda>u. d(u, h ` succ(depth(u)) ` u));
1.575 - 	M(h) |]
1.576 + 	M(h) |]
1.577        ==> Relation1(M, formula,
1.578                           is_formula_case (M, is_a, is_b, is_c, is_d),
1.579                           formula_rec_case(a, b, c, d, h))"
1.580 -apply (simp (no_asm) add: formula_rec_case_def Relation1_def)
1.582 +apply (simp (no_asm) add: formula_rec_case_def Relation1_def)
1.584  done
1.585
1.586
1.587 @@ -970,12 +953,12 @@
1.588        and c_closed: "[|x \<in> formula; y \<in> formula; M(gx); M(gy)|]
1.589                       ==> M(c(x, y, gx, gy))"
1.590        and c_rel:
1.591 -         "M(f) ==>
1.592 +         "M(f) ==>
1.593            Relation2 (M, formula, formula, is_c(f),
1.594               \<lambda>u v. c(u, v, f ` succ(depth(u)) ` u, f ` succ(depth(v)) ` v))"
1.595        and d_closed: "[|x \<in> formula; M(gx)|] ==> M(d(x, gx))"
1.596        and d_rel:
1.597 -         "M(f) ==>
1.598 +         "M(f) ==>
1.599            Relation1(M, formula, is_d(f), \<lambda>u. d(u, f ` succ(depth(u)) ` u))"
1.600        and fr_replace: "n \<in> nat ==> transrec_replacement(M,MH,n)"
1.601        and fr_lam_replace:
1.602 @@ -986,7 +969,7 @@
1.603
1.604  lemma (in Formula_Rec) formula_rec_case_closed:
1.605      "[|M(g); p \<in> formula|] ==> M(formula_rec_case(a, b, c, d, g, p))"
1.606 -by (simp add: formula_rec_case_def a_closed b_closed c_closed d_closed)
1.607 +by (simp add: formula_rec_case_def a_closed b_closed c_closed d_closed)
1.608
1.609  lemma (in Formula_Rec) formula_rec_lam_closed:
1.610      "M(g) ==> M(Lambda (formula, formula_rec_case(a,b,c,d,g)))"
1.611 @@ -995,29 +978,29 @@
1.612  lemma (in Formula_Rec) MH_rel2:
1.613       "relation2 (M, MH,
1.614               \<lambda>x h. Lambda (formula, formula_rec_case(a,b,c,d,h)))"
1.615 -apply (simp add: relation2_def MH_def, clarify)
1.616 -apply (rule lambda_abs2)
1.617 +apply (simp add: relation2_def MH_def, clarify)
1.618 +apply (rule lambda_abs2)
1.619  apply (rule fr_lam_replace, assumption)
1.620 -apply (rule Relation1_formula_rec_case)
1.621 -apply (simp_all add: a_rel b_rel c_rel d_rel formula_rec_case_closed)
1.622 +apply (rule Relation1_formula_rec_case)
1.623 +apply (simp_all add: a_rel b_rel c_rel d_rel formula_rec_case_closed)
1.624  done
1.625
1.626  lemma (in Formula_Rec) fr_transrec_closed:
1.627      "n \<in> nat
1.628       ==> M(transrec
1.629            (n, \<lambda>x h. Lambda(formula, formula_rec_case(a, b, c, d, h))))"
1.630 -by (simp add: transrec_closed [OF fr_replace MH_rel2]
1.631 -              nat_into_M formula_rec_lam_closed)
1.632 +by (simp add: transrec_closed [OF fr_replace MH_rel2]
1.633 +              nat_into_M formula_rec_lam_closed)
1.634
1.635  text{*The main two results: @{term formula_rec} is absolute for @{term M}.*}
1.636  theorem (in Formula_Rec) formula_rec_closed:
1.637      "p \<in> formula ==> M(formula_rec(a,b,c,d,p))"
1.638 -by (simp add: formula_rec_eq fr_transrec_closed
1.639 +by (simp add: formula_rec_eq fr_transrec_closed
1.640                transM [OF _ formula_closed])
1.641
1.642  theorem (in Formula_Rec) formula_rec_abs:
1.643 -  "[| p \<in> formula; M(z)|]
1.644 -   ==> is_formula_rec(M,MH,p,z) <-> z = formula_rec(a,b,c,d,p)"
1.645 +  "[| p \<in> formula; M(z)|]
1.646 +   ==> is_formula_rec(M,MH,p,z) <-> z = formula_rec(a,b,c,d,p)"
1.647  by (simp add: is_formula_rec_def formula_rec_eq transM [OF _ formula_closed]
1.648                transrec_abs [OF fr_replace MH_rel2] depth_type
1.649                fr_transrec_closed formula_rec_lam_closed eq_commute)
```