src/ZF/Constructible/Datatype_absolute.thy

 
 
 subsection{*@{term M} Contains the List and Formula Datatypes*}
 
 constdefs
-  is_list_n :: "[i=>o,i,i,i] => o"
-    "is_list_n(M,A,n,Z) == 
+  list_N :: "[i,i] => i"
+    "list_N(A,n) == (\<lambda>X. {0} + A * X)^n (0)"
+
+lemma Nil_in_list_N [simp]: "[] \<in> list_N(A,succ(n))"
+by (simp add: list_N_def Nil_def)
+
+lemma Cons_in_list_N [simp]:
+     "Cons(a,l) \<in> list_N(A,succ(n)) <-> a\<in>A & l \<in> list_N(A,n)"
+by (simp add: list_N_def Cons_def) 
+
+text{*These two aren't simprules because they reveal the underlying
+list representation.*}
+lemma list_N_0: "list_N(A,0) = 0"
+by (simp add: list_N_def)
+
+lemma list_N_succ: "list_N(A,succ(n)) = {0} + A * (list_N(A,n))"
+by (simp add: list_N_def)
+
+lemma list_N_imp_list:
+  "[| l \<in> list_N(A,n); n \<in> nat |] ==> l \<in> list(A)"
+by (force simp add: list_eq_Union list_N_def)
+
+lemma list_N_imp_length_lt [rule_format]:
+     "n \<in> nat ==> \<forall>l \<in> list_N(A,n). length(l) < n"
+apply (induct_tac n)  
+apply (auto simp add: list_N_0 list_N_succ 
+                      Nil_def [symmetric] Cons_def [symmetric]) 
+done
+
+lemma list_imp_list_N [rule_format]:
+     "l \<in> list(A) ==> \<forall>n\<in>nat. length(l) < n --> l \<in> list_N(A, n)"
+apply (induct_tac l)
+apply (force elim: natE)+
+done
+
+lemma list_N_imp_eq_length:
+      "[|n \<in> nat; l \<notin> list_N(A, n); l \<in> list_N(A, succ(n))|] 
+       ==> n = length(l)"
+apply (rule le_anti_sym) 
+ prefer 2 apply (simp add: list_N_imp_length_lt) 
+apply (frule list_N_imp_list, simp)
+apply (simp add: not_lt_iff_le [symmetric]) 
+apply (blast intro: list_imp_list_N) 
+done
+  
+text{*Express @{term list_rec} without using @{term rank} or @{term Vset},
+neither of which is absolute.*}
+lemma (in M_triv_axioms) list_rec_eq:
+  "l \<in> list(A) ==>
+   list_rec(a,g,l) = 
+   transrec (succ(length(l)),
+      \<lambda>x h. Lambda (list_N(A,x),
+             list_case' (a, 
+                \<lambda>a l. g(a, l, h ` succ(length(l)) ` l)))) ` l"
+apply (induct_tac l) 
+apply (subst transrec, simp) 
+apply (subst transrec) 
+apply (simp add: list_imp_list_N) 
+done
+
+constdefs
+  is_list_N :: "[i=>o,i,i,i] => o"
+    "is_list_N(M,A,n,Z) == 
       \<exists>zero[M]. \<exists>sn[M]. \<exists>msn[M]. 
        empty(M,zero) & 
        successor(M,n,sn) & membership(M,sn,msn) &
        is_wfrec(M, iterates_MH(M, is_list_functor(M,A),zero), msn, n, Z)"
   
   mem_list :: "[i=>o,i,i] => o"
     "mem_list(M,A,l) == 
       \<exists>n[M]. \<exists>listn[M]. 
-       finite_ordinal(M,n) & is_list_n(M,A,n,listn) & l \<in> listn"
+       finite_ordinal(M,n) & is_list_N(M,A,n,listn) & l \<in> listn"
 
   is_list :: "[i=>o,i,i] => o"
     "is_list(M,A,Z) == \<forall>l[M]. l \<in> Z <-> mem_list(M,A,l)"
 
 constdefs

      "M(A) ==> M(list(A))"
 apply (insert list_replacement1)
 by  (simp add: RepFun_closed2 list_eq_Union 
                list_replacement2' relativize1_def
                iterates_closed [of "is_list_functor(M,A)"])
-lemma (in M_datatypes) is_list_n_abs [simp]:
+
+lemma (in M_datatypes) list_N_abs [simp]:
      "[|M(A); n\<in>nat; M(Z)|] 
-      ==> is_list_n(M,A,n,Z) <-> Z = (\<lambda>X. {0} + A * X)^n (0)"
+      ==> is_list_N(M,A,n,Z) <-> Z = list_N(A,n)"
 apply (insert list_replacement1)
-apply (simp add: is_list_n_def relativize1_def nat_into_M
+apply (simp add: is_list_N_def list_N_def relativize1_def nat_into_M
                  iterates_abs [of "is_list_functor(M,A)" _ "\<lambda>X. {0} + A*X"])
+done
+
+lemma (in M_datatypes) list_N_closed [intro,simp]:
+     "[|M(A); n\<in>nat|] ==> M(list_N(A,n))"
+apply (insert list_replacement1)
+apply (simp add: is_list_N_def list_N_def relativize1_def nat_into_M
+                 iterates_closed [of "is_list_functor(M,A)"])
 done
 
 lemma (in M_datatypes) mem_list_abs [simp]:
      "M(A) ==> mem_list(M,A,l) <-> l \<in> list(A)"
 apply (insert list_replacement1)
-apply (simp add: mem_list_def relativize1_def list_eq_Union
+apply (simp add: mem_list_def list_N_def relativize1_def list_eq_Union
                  iterates_closed [of "is_list_functor(M,A)"]) 
 done
 
 lemma (in M_datatypes) list_abs [simp]:
      "[|M(A); M(Z)|] ==> is_list(M,A,Z) <-> Z = list(A)"

      "[|M(Z)|] ==> is_formula(M,Z) <-> Z = formula"
 apply (simp add: is_formula_def, safe)
 apply (rule M_equalityI, simp_all)
 done
 
+
+subsection{*Absoluteness for Some List Operators*}
 
 subsection{*Absoluteness for @{text \<epsilon>}-Closure: the @{term eclose} Operator*}
 
 text{*Re-expresses eclose using "iterates"*}
 lemma eclose_eq_Union:

    "transrec_replacement(M,MH,a) ==
       \<exists>sa[M]. \<exists>esa[M]. \<exists>mesa[M]. 
        upair(M,a,a,sa) & is_eclose(M,sa,esa) & membership(M,esa,mesa) &
        wfrec_replacement(M,MH,mesa)"
 
-(*????????????????Ordinal.thy*)
-lemma Transset_trans_Memrel: 
-    "\<forall>j\<in>i. Transset(j) ==> trans(Memrel(i))"
-by (unfold Transset_def trans_def, blast)
-
 text{*The condition @{term "Ord(i)"} lets us use the simpler 
   @{text "trans_wfrec_abs"} rather than @{text "trans_wfrec_abs"},
   which I haven't even proved yet. *}
 theorem (in M_eclose) transrec_abs:
   "[|Ord(i);  M(i);  M(z);

 by (simp add: trans_wfrec_closed transrec_replacement_def is_transrec_def
        transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
 
 
 
+subsection{*Absoluteness for the List Operator @{term length}*}
+constdefs
+
+  is_length :: "[i=>o,i,i,i] => o"
+    "is_length(M,A,l,n) == 
+       \<exists>sn[M]. \<exists>list_n[M]. \<exists>list_sn[M]. 
+        is_list_N(M,A,n,list_n) & l \<notin> list_n &
+        successor(M,n,sn) & is_list_N(M,A,sn,list_sn) & l \<in> list_sn"
+
+
+lemma (in M_datatypes) length_abs [simp]:
+     "[|M(A); l \<in> list(A); n \<in> nat|] ==> is_length(M,A,l,n) <-> n = length(l)"
+apply (subgoal_tac "M(l) & M(n)")
+ prefer 2 apply (blast dest: transM)  
+apply (simp add: is_length_def)
+apply (blast intro: list_imp_list_N nat_into_Ord list_N_imp_eq_length
+             dest: list_N_imp_length_lt)
+done
+
+text{*Proof is trivial since @{term length} returns natural numbers.*}
+lemma (in M_triv_axioms) length_closed [intro,simp]:
+     "l \<in> list(A) ==> M(length(l))"
+by (simp add: nat_into_M ) 
+
+
+subsection {*Absoluteness for @{term nth}*}
+
+lemma nth_eq_hd_iterates_tl [rule_format]:
+     "xs \<in> list(A) ==> \<forall>n \<in> nat. nth(n,xs) = hd' (tl'^n (xs))"
+apply (induct_tac xs) 
+apply (simp add: iterates_tl_Nil hd'_Nil, clarify) 
+apply (erule natE)
+apply (simp add: hd'_Cons) 
+apply (simp add: tl'_Cons iterates_commute) 
+done
+
+lemma (in M_axioms) iterates_tl'_closed:
+     "[|n \<in> nat; M(x)|] ==> M(tl'^n (x))"
+apply (induct_tac n, simp) 
+apply (simp add: tl'_Cons tl'_closed) 
+done
+
+locale (open) M_nth = M_datatypes +
+ assumes nth_replacement1: 
+   "M(xs) ==> iterates_replacement(M, %l t. is_tl(M,l,t), xs)"
+
+text{*Immediate by type-checking*}
+lemma (in M_datatypes) nth_closed [intro,simp]:
+     "[|xs \<in> list(A); n \<in> nat; M(A)|] ==> M(nth(n,xs))" 
+apply (case_tac "n < length(xs)")
+ apply (blast intro: nth_type transM)
+apply (simp add: not_lt_iff_le nth_eq_0)
+done
+
+constdefs
+  is_nth :: "[i=>o,i,i,i] => o"
+    "is_nth(M,n,l,Z) == 
+      \<exists>X[M]. \<exists>sn[M]. \<exists>msn[M]. 
+       successor(M,n,sn) & membership(M,sn,msn) &
+       is_wfrec(M, iterates_MH(M, is_tl(M), l), msn, n, X) &
+       is_hd(M,X,Z)"
+ 
+lemma (in M_nth) nth_abs [simp]:
+     "[|M(A); n \<in> nat; l \<in> list(A); M(Z)|] 
+      ==> is_nth(M,n,l,Z) <-> Z = nth(n,l)"
+apply (subgoal_tac "M(l)") 
+ prefer 2 apply (blast intro: transM)
+apply (insert nth_replacement1)
+apply (simp add: is_nth_def nth_eq_hd_iterates_tl nat_into_M
+                 tl'_closed iterates_tl'_closed 
+                 iterates_abs [OF _ relativize1_tl])
+done
+
 
 end