src/ZF/Constructible/Datatype_absolute.thy
 changeset 13647 7f6f0ffc45c3 parent 13634 99a593b49b04 child 13655 95b95cdb4704
```     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Mon Oct 14 10:44:32 2002 +0200
1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Mon Oct 14 11:32:00 2002 +0200
1.3 @@ -425,7 +425,7 @@
1.4  done
1.5
1.6
1.7 -
1.8 +text{*This result and the next are unused.*}
1.9  lemma formula_N_mono [rule_format]:
1.10    "[| m \<in> nat; n \<in> nat |] ==> m\<le>n --> formula_N(m) \<subseteq> formula_N(n)"
1.11  apply (rule_tac m = m and n = n in diff_induct)
1.12 @@ -577,8 +577,6 @@
1.13  done
1.14
1.15
1.16 -subsection{*Absoluteness for Some List Operators*}
1.17 -
1.18  subsection{*Absoluteness for @{text \<epsilon>}-Closure: the @{term eclose} Operator*}
1.19
1.20  text{*Re-expresses eclose using "iterates"*}
1.21 @@ -705,8 +703,9 @@
1.22
1.23
1.24  subsection{*Absoluteness for the List Operator @{term length}*}
1.25 +text{*But it is never used.*}
1.26 +
1.27  constdefs
1.28 -
1.29    is_length :: "[i=>o,i,i,i] => o"
1.30      "is_length(M,A,l,n) ==
1.31         \<exists>sn[M]. \<exists>list_n[M]. \<exists>list_sn[M].
1.32 @@ -729,7 +728,7 @@
1.34
1.35
1.36 -subsection {*Absoluteness for @{term nth}*}
1.37 +subsection {*Absoluteness for the List Operator @{term nth}*}
1.38
1.39  lemma nth_eq_hd_iterates_tl [rule_format]:
1.40       "xs \<in> list(A) ==> \<forall>n \<in> nat. nth(n,xs) = hd' (tl'^n (xs))"
1.41 @@ -828,8 +827,67 @@
1.43
1.44
1.45 +
1.46  subsection {*Absoluteness for @{term formula_rec}*}
1.47
1.48 +constdefs
1.49 +
1.50 +  formula_rec_case :: "[[i,i]=>i, [i,i]=>i, [i,i,i,i]=>i, [i,i]=>i, i, i] => i"
1.51 +    --{* the instance of @{term formula_case} in @{term formula_rec}*}
1.52 +   "formula_rec_case(a,b,c,d,h) ==
1.53 +        formula_case (a, b,
1.54 +                \<lambda>u v. c(u, v, h ` succ(depth(u)) ` u,
1.55 +                              h ` succ(depth(v)) ` v),
1.56 +                \<lambda>u. d(u, h ` succ(depth(u)) ` u))"
1.57 +
1.58 +text{*Unfold @{term formula_rec} to @{term formula_rec_case}.
1.59 +     Express @{term formula_rec} without using @{term rank} or @{term Vset},
1.60 +neither of which is absolute.*}
1.61 +lemma (in M_trivial) formula_rec_eq:
1.62 +  "p \<in> formula ==>
1.63 +   formula_rec(a,b,c,d,p) =
1.64 +   transrec (succ(depth(p)),
1.65 +             \<lambda>x h. Lambda (formula, formula_rec_case(a,b,c,d,h))) ` p"
1.67 +apply (induct_tac p)
1.68 +   txt{*Base case for @{term Member}*}
1.69 +   apply (subst transrec, simp add: formula.intros)
1.70 +  txt{*Base case for @{term Equal}*}
1.71 +  apply (subst transrec, simp add: formula.intros)
1.72 + txt{*Inductive step for @{term Nand}*}
1.73 + apply (subst transrec)
1.74 + apply (simp add: succ_Un_distrib formula.intros)
1.75 +txt{*Inductive step for @{term Forall}*}
1.76 +apply (subst transrec)
1.77 +apply (simp add: formula_imp_formula_N formula.intros)
1.78 +done
1.79 +
1.80 +
1.81 +subsubsection{*Absoluteness for the Formula Operator @{term depth}*}
1.82 +constdefs
1.83 +
1.84 +  is_depth :: "[i=>o,i,i] => o"
1.85 +    "is_depth(M,p,n) ==
1.86 +       \<exists>sn[M]. \<exists>formula_n[M]. \<exists>formula_sn[M].
1.87 +        is_formula_N(M,n,formula_n) & p \<notin> formula_n &
1.88 +        successor(M,n,sn) & is_formula_N(M,sn,formula_sn) & p \<in> formula_sn"
1.89 +
1.90 +
1.91 +lemma (in M_datatypes) depth_abs [simp]:
1.92 +     "[|p \<in> formula; n \<in> nat|] ==> is_depth(M,p,n) <-> n = depth(p)"
1.93 +apply (subgoal_tac "M(p) & M(n)")
1.94 + prefer 2 apply (blast dest: transM)
1.96 +apply (blast intro: formula_imp_formula_N nat_into_Ord formula_N_imp_eq_depth
1.97 +             dest: formula_N_imp_depth_lt)
1.98 +done
1.99 +
1.100 +text{*Proof is trivial since @{term depth} returns natural numbers.*}
1.101 +lemma (in M_trivial) depth_closed [intro,simp]:
1.102 +     "p \<in> formula ==> M(depth(p))"
1.104 +
1.105 +
1.106  subsubsection{*@{term is_formula_case}: relativization of @{term formula_case}*}
1.107
1.108  constdefs
1.109 @@ -866,73 +924,17 @@
1.110  by (erule formula.cases, simp_all)
1.111
1.112
1.113 -subsection{*Absoluteness for the Formula Operator @{term depth}*}
1.114 -constdefs
1.115 -
1.116 -  is_depth :: "[i=>o,i,i] => o"
1.117 -    "is_depth(M,p,n) ==
1.118 -       \<exists>sn[M]. \<exists>formula_n[M]. \<exists>formula_sn[M].
1.119 -        is_formula_N(M,n,formula_n) & p \<notin> formula_n &
1.120 -        successor(M,n,sn) & is_formula_N(M,sn,formula_sn) & p \<in> formula_sn"
1.121 -
1.122 -
1.123 -lemma (in M_datatypes) depth_abs [simp]:
1.124 -     "[|p \<in> formula; n \<in> nat|] ==> is_depth(M,p,n) <-> n = depth(p)"
1.125 -apply (subgoal_tac "M(p) & M(n)")
1.126 - prefer 2 apply (blast dest: transM)
1.128 -apply (blast intro: formula_imp_formula_N nat_into_Ord formula_N_imp_eq_depth
1.129 -             dest: formula_N_imp_depth_lt)
1.130 -done
1.131 -
1.132 -text{*Proof is trivial since @{term depth} returns natural numbers.*}
1.133 -lemma (in M_trivial) depth_closed [intro,simp]:
1.134 -     "p \<in> formula ==> M(depth(p))"
1.136 -
1.137 -
1.138 -subsection {*Absoluteness for @{term formula_rec}*}
1.139 +subsubsection {*Absoluteness for @{term formula_rec}: Final Results*}
1.140
1.141  constdefs
1.142 -
1.143 -  formula_rec_case :: "[[i,i]=>i, [i,i]=>i, [i,i,i,i]=>i, [i,i]=>i, i, i] => i"
1.144 -    --{* the instance of @{term formula_case} in @{term formula_rec}*}
1.145 -   "formula_rec_case(a,b,c,d,h) ==
1.146 -        formula_case (a, b,
1.147 -                \<lambda>u v. c(u, v, h ` succ(depth(u)) ` u,
1.148 -                              h ` succ(depth(v)) ` v),
1.149 -                \<lambda>u. d(u, h ` succ(depth(u)) ` u))"
1.150 -
1.151    is_formula_rec :: "[i=>o, [i,i,i]=>o, i, i] => o"
1.152      --{* predicate to relativize the functional @{term formula_rec}*}
1.153     "is_formula_rec(M,MH,p,z)  ==
1.154        \<exists>dp[M]. \<exists>i[M]. \<exists>f[M]. finite_ordinal(M,dp) & is_depth(M,p,dp) &
1.155               successor(M,dp,i) & fun_apply(M,f,p,z) & is_transrec(M,MH,i,f)"
1.156
1.157 -text{*Unfold @{term formula_rec} to @{term formula_rec_case}.
1.158 -     Express @{term formula_rec} without using @{term rank} or @{term Vset},
1.159 -neither of which is absolute.*}
1.160 -lemma (in M_trivial) formula_rec_eq:
1.161 -  "p \<in> formula ==>
1.162 -   formula_rec(a,b,c,d,p) =
1.163 -   transrec (succ(depth(p)),
1.164 -             \<lambda>x h. Lambda (formula, formula_rec_case(a,b,c,d,h))) ` p"
1.166 -apply (induct_tac p)
1.167 -   txt{*Base case for @{term Member}*}
1.168 -   apply (subst transrec, simp add: formula.intros)
1.169 -  txt{*Base case for @{term Equal}*}
1.170 -  apply (subst transrec, simp add: formula.intros)
1.171 - txt{*Inductive step for @{term Nand}*}
1.172 - apply (subst transrec)
1.173 - apply (simp add: succ_Un_distrib formula.intros)
1.174 -txt{*Inductive step for @{term Forall}*}
1.175 -apply (subst transrec)
1.176 -apply (simp add: formula_imp_formula_N formula.intros)
1.177 -done
1.178
1.179 -
1.180 -text{*Sufficient conditions to relative the instance of @{term formula_case}
1.181 +text{*Sufficient conditions to relativize the instance of @{term formula_case}
1.182        in @{term formula_rec}*}
1.183  lemma (in M_datatypes) Relation1_formula_rec_case:
1.184       "[|Relation2(M, nat, nat, is_a, a);
```