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.33  by (simp add: nat_into_M) 
    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.42  by (simp add: Forall_def)
    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.66 +apply (simp add: formula_rec_case_def)
    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.95 +apply (simp add: is_depth_def)
    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.103 +by (simp add: nat_into_M) 
   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.127 -apply (simp add: is_depth_def)
   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.135 -by (simp add: nat_into_M) 
   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.165 -apply (simp add: formula_rec_case_def)
   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);