src/ZF/Constructible/Datatype_absolute.thy
changeset 13397 6e5f4d911435
parent 13395 4eb948d1eb4e
child 13398 1cadd412da48
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Fri Jul 19 13:28:19 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Fri Jul 19 13:29:22 2002 +0200
     1.3 @@ -270,8 +270,69 @@
     1.4  subsection{*@{term M} Contains the List and Formula Datatypes*}
     1.5  
     1.6  constdefs
     1.7 -  is_list_n :: "[i=>o,i,i,i] => o"
     1.8 -    "is_list_n(M,A,n,Z) == 
     1.9 +  list_N :: "[i,i] => i"
    1.10 +    "list_N(A,n) == (\<lambda>X. {0} + A * X)^n (0)"
    1.11 +
    1.12 +lemma Nil_in_list_N [simp]: "[] \<in> list_N(A,succ(n))"
    1.13 +by (simp add: list_N_def Nil_def)
    1.14 +
    1.15 +lemma Cons_in_list_N [simp]:
    1.16 +     "Cons(a,l) \<in> list_N(A,succ(n)) <-> a\<in>A & l \<in> list_N(A,n)"
    1.17 +by (simp add: list_N_def Cons_def) 
    1.18 +
    1.19 +text{*These two aren't simprules because they reveal the underlying
    1.20 +list representation.*}
    1.21 +lemma list_N_0: "list_N(A,0) = 0"
    1.22 +by (simp add: list_N_def)
    1.23 +
    1.24 +lemma list_N_succ: "list_N(A,succ(n)) = {0} + A * (list_N(A,n))"
    1.25 +by (simp add: list_N_def)
    1.26 +
    1.27 +lemma list_N_imp_list:
    1.28 +  "[| l \<in> list_N(A,n); n \<in> nat |] ==> l \<in> list(A)"
    1.29 +by (force simp add: list_eq_Union list_N_def)
    1.30 +
    1.31 +lemma list_N_imp_length_lt [rule_format]:
    1.32 +     "n \<in> nat ==> \<forall>l \<in> list_N(A,n). length(l) < n"
    1.33 +apply (induct_tac n)  
    1.34 +apply (auto simp add: list_N_0 list_N_succ 
    1.35 +                      Nil_def [symmetric] Cons_def [symmetric]) 
    1.36 +done
    1.37 +
    1.38 +lemma list_imp_list_N [rule_format]:
    1.39 +     "l \<in> list(A) ==> \<forall>n\<in>nat. length(l) < n --> l \<in> list_N(A, n)"
    1.40 +apply (induct_tac l)
    1.41 +apply (force elim: natE)+
    1.42 +done
    1.43 +
    1.44 +lemma list_N_imp_eq_length:
    1.45 +      "[|n \<in> nat; l \<notin> list_N(A, n); l \<in> list_N(A, succ(n))|] 
    1.46 +       ==> n = length(l)"
    1.47 +apply (rule le_anti_sym) 
    1.48 + prefer 2 apply (simp add: list_N_imp_length_lt) 
    1.49 +apply (frule list_N_imp_list, simp)
    1.50 +apply (simp add: not_lt_iff_le [symmetric]) 
    1.51 +apply (blast intro: list_imp_list_N) 
    1.52 +done
    1.53 +  
    1.54 +text{*Express @{term list_rec} without using @{term rank} or @{term Vset},
    1.55 +neither of which is absolute.*}
    1.56 +lemma (in M_triv_axioms) list_rec_eq:
    1.57 +  "l \<in> list(A) ==>
    1.58 +   list_rec(a,g,l) = 
    1.59 +   transrec (succ(length(l)),
    1.60 +      \<lambda>x h. Lambda (list_N(A,x),
    1.61 +             list_case' (a, 
    1.62 +                \<lambda>a l. g(a, l, h ` succ(length(l)) ` l)))) ` l"
    1.63 +apply (induct_tac l) 
    1.64 +apply (subst transrec, simp) 
    1.65 +apply (subst transrec) 
    1.66 +apply (simp add: list_imp_list_N) 
    1.67 +done
    1.68 +
    1.69 +constdefs
    1.70 +  is_list_N :: "[i=>o,i,i,i] => o"
    1.71 +    "is_list_N(M,A,n,Z) == 
    1.72        \<exists>zero[M]. \<exists>sn[M]. \<exists>msn[M]. 
    1.73         empty(M,zero) & 
    1.74         successor(M,n,sn) & membership(M,sn,msn) &
    1.75 @@ -280,7 +341,7 @@
    1.76    mem_list :: "[i=>o,i,i] => o"
    1.77      "mem_list(M,A,l) == 
    1.78        \<exists>n[M]. \<exists>listn[M]. 
    1.79 -       finite_ordinal(M,n) & is_list_n(M,A,n,listn) & l \<in> listn"
    1.80 +       finite_ordinal(M,n) & is_list_N(M,A,n,listn) & l \<in> listn"
    1.81  
    1.82    is_list :: "[i=>o,i,i] => o"
    1.83      "is_list(M,A,Z) == \<forall>l[M]. l \<in> Z <-> mem_list(M,A,l)"
    1.84 @@ -336,18 +397,26 @@
    1.85  by  (simp add: RepFun_closed2 list_eq_Union 
    1.86                 list_replacement2' relativize1_def
    1.87                 iterates_closed [of "is_list_functor(M,A)"])
    1.88 -lemma (in M_datatypes) is_list_n_abs [simp]:
    1.89 +
    1.90 +lemma (in M_datatypes) list_N_abs [simp]:
    1.91       "[|M(A); n\<in>nat; M(Z)|] 
    1.92 -      ==> is_list_n(M,A,n,Z) <-> Z = (\<lambda>X. {0} + A * X)^n (0)"
    1.93 +      ==> is_list_N(M,A,n,Z) <-> Z = list_N(A,n)"
    1.94  apply (insert list_replacement1)
    1.95 -apply (simp add: is_list_n_def relativize1_def nat_into_M
    1.96 +apply (simp add: is_list_N_def list_N_def relativize1_def nat_into_M
    1.97                   iterates_abs [of "is_list_functor(M,A)" _ "\<lambda>X. {0} + A*X"])
    1.98  done
    1.99  
   1.100 +lemma (in M_datatypes) list_N_closed [intro,simp]:
   1.101 +     "[|M(A); n\<in>nat|] ==> M(list_N(A,n))"
   1.102 +apply (insert list_replacement1)
   1.103 +apply (simp add: is_list_N_def list_N_def relativize1_def nat_into_M
   1.104 +                 iterates_closed [of "is_list_functor(M,A)"])
   1.105 +done
   1.106 +
   1.107  lemma (in M_datatypes) mem_list_abs [simp]:
   1.108       "M(A) ==> mem_list(M,A,l) <-> l \<in> list(A)"
   1.109  apply (insert list_replacement1)
   1.110 -apply (simp add: mem_list_def relativize1_def list_eq_Union
   1.111 +apply (simp add: mem_list_def list_N_def relativize1_def list_eq_Union
   1.112                   iterates_closed [of "is_list_functor(M,A)"]) 
   1.113  done
   1.114  
   1.115 @@ -399,6 +468,8 @@
   1.116  done
   1.117  
   1.118  
   1.119 +subsection{*Absoluteness for Some List Operators*}
   1.120 +
   1.121  subsection{*Absoluteness for @{text \<epsilon>}-Closure: the @{term eclose} Operator*}
   1.122  
   1.123  text{*Re-expresses eclose using "iterates"*}
   1.124 @@ -494,11 +565,6 @@
   1.125         upair(M,a,a,sa) & is_eclose(M,sa,esa) & membership(M,esa,mesa) &
   1.126         wfrec_replacement(M,MH,mesa)"
   1.127  
   1.128 -(*????????????????Ordinal.thy*)
   1.129 -lemma Transset_trans_Memrel: 
   1.130 -    "\<forall>j\<in>i. Transset(j) ==> trans(Memrel(i))"
   1.131 -by (unfold Transset_def trans_def, blast)
   1.132 -
   1.133  text{*The condition @{term "Ord(i)"} lets us use the simpler 
   1.134    @{text "trans_wfrec_abs"} rather than @{text "trans_wfrec_abs"},
   1.135    which I haven't even proved yet. *}
   1.136 @@ -521,5 +587,78 @@
   1.137  
   1.138  
   1.139  
   1.140 +subsection{*Absoluteness for the List Operator @{term length}*}
   1.141 +constdefs
   1.142 +
   1.143 +  is_length :: "[i=>o,i,i,i] => o"
   1.144 +    "is_length(M,A,l,n) == 
   1.145 +       \<exists>sn[M]. \<exists>list_n[M]. \<exists>list_sn[M]. 
   1.146 +        is_list_N(M,A,n,list_n) & l \<notin> list_n &
   1.147 +        successor(M,n,sn) & is_list_N(M,A,sn,list_sn) & l \<in> list_sn"
   1.148 +
   1.149 +
   1.150 +lemma (in M_datatypes) length_abs [simp]:
   1.151 +     "[|M(A); l \<in> list(A); n \<in> nat|] ==> is_length(M,A,l,n) <-> n = length(l)"
   1.152 +apply (subgoal_tac "M(l) & M(n)")
   1.153 + prefer 2 apply (blast dest: transM)  
   1.154 +apply (simp add: is_length_def)
   1.155 +apply (blast intro: list_imp_list_N nat_into_Ord list_N_imp_eq_length
   1.156 +             dest: list_N_imp_length_lt)
   1.157 +done
   1.158 +
   1.159 +text{*Proof is trivial since @{term length} returns natural numbers.*}
   1.160 +lemma (in M_triv_axioms) length_closed [intro,simp]:
   1.161 +     "l \<in> list(A) ==> M(length(l))"
   1.162 +by (simp add: nat_into_M ) 
   1.163 +
   1.164 +
   1.165 +subsection {*Absoluteness for @{term nth}*}
   1.166 +
   1.167 +lemma nth_eq_hd_iterates_tl [rule_format]:
   1.168 +     "xs \<in> list(A) ==> \<forall>n \<in> nat. nth(n,xs) = hd' (tl'^n (xs))"
   1.169 +apply (induct_tac xs) 
   1.170 +apply (simp add: iterates_tl_Nil hd'_Nil, clarify) 
   1.171 +apply (erule natE)
   1.172 +apply (simp add: hd'_Cons) 
   1.173 +apply (simp add: tl'_Cons iterates_commute) 
   1.174 +done
   1.175 +
   1.176 +lemma (in M_axioms) iterates_tl'_closed:
   1.177 +     "[|n \<in> nat; M(x)|] ==> M(tl'^n (x))"
   1.178 +apply (induct_tac n, simp) 
   1.179 +apply (simp add: tl'_Cons tl'_closed) 
   1.180 +done
   1.181 +
   1.182 +locale (open) M_nth = M_datatypes +
   1.183 + assumes nth_replacement1: 
   1.184 +   "M(xs) ==> iterates_replacement(M, %l t. is_tl(M,l,t), xs)"
   1.185 +
   1.186 +text{*Immediate by type-checking*}
   1.187 +lemma (in M_datatypes) nth_closed [intro,simp]:
   1.188 +     "[|xs \<in> list(A); n \<in> nat; M(A)|] ==> M(nth(n,xs))" 
   1.189 +apply (case_tac "n < length(xs)")
   1.190 + apply (blast intro: nth_type transM)
   1.191 +apply (simp add: not_lt_iff_le nth_eq_0)
   1.192 +done
   1.193 +
   1.194 +constdefs
   1.195 +  is_nth :: "[i=>o,i,i,i] => o"
   1.196 +    "is_nth(M,n,l,Z) == 
   1.197 +      \<exists>X[M]. \<exists>sn[M]. \<exists>msn[M]. 
   1.198 +       successor(M,n,sn) & membership(M,sn,msn) &
   1.199 +       is_wfrec(M, iterates_MH(M, is_tl(M), l), msn, n, X) &
   1.200 +       is_hd(M,X,Z)"
   1.201 + 
   1.202 +lemma (in M_nth) nth_abs [simp]:
   1.203 +     "[|M(A); n \<in> nat; l \<in> list(A); M(Z)|] 
   1.204 +      ==> is_nth(M,n,l,Z) <-> Z = nth(n,l)"
   1.205 +apply (subgoal_tac "M(l)") 
   1.206 + prefer 2 apply (blast intro: transM)
   1.207 +apply (insert nth_replacement1)
   1.208 +apply (simp add: is_nth_def nth_eq_hd_iterates_tl nat_into_M
   1.209 +                 tl'_closed iterates_tl'_closed 
   1.210 +                 iterates_abs [OF _ relativize1_tl])
   1.211 +done
   1.212 +
   1.213  
   1.214  end