# HG changeset patch
# User paulson
# Date 1027078162 -7200
# Node ID 6e5f4d911435877a75f5c9afd528db32568c4265
# Parent  11219ca224ab093a448591b8a5925848ecbcea31
Absoluteness of the function "nth"

diff -r 11219ca224ab -r 6e5f4d911435 src/ZF/Constructible/Datatype_absolute.thy
--- a/src/ZF/Constructible/Datatype_absolute.thy	Fri Jul 19 13:28:19 2002 +0200
+++ b/src/ZF/Constructible/Datatype_absolute.thy	Fri Jul 19 13:29:22 2002 +0200
@@ -270,8 +270,69 @@
 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) &
@@ -280,7 +341,7 @@
   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)"
@@ -336,18 +397,26 @@
 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
 
@@ -399,6 +468,8 @@
 done
 
 
+subsection{*Absoluteness for Some List Operators*}
+
 subsection{*Absoluteness for @{text \<epsilon>}-Closure: the @{term eclose} Operator*}
 
 text{*Re-expresses eclose using "iterates"*}
@@ -494,11 +565,6 @@
        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. *}
@@ -521,5 +587,78 @@
 
 
 
+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
diff -r 11219ca224ab -r 6e5f4d911435 src/ZF/Constructible/Relative.thy
--- a/src/ZF/Constructible/Relative.thy	Fri Jul 19 13:28:19 2002 +0200
+++ b/src/ZF/Constructible/Relative.thy	Fri Jul 19 13:29:22 2002 +0200
@@ -64,6 +64,12 @@
        number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) &
        cartprod(M,s1,B,B1) & union(M,A0,B1,Z)"
 
+  is_Inl :: "[i=>o,i,i] => o"
+    "is_Inl(M,a,z) == \<exists>zero[M]. empty(M,zero) & pair(M,zero,a,z)"
+
+  is_Inr :: "[i=>o,i,i] => o"
+    "is_Inr(M,a,z) == \<exists>n1[M]. number1(M,n1) & pair(M,n1,a,z)"
+
   is_converse :: "[i=>o,i,i] => o"
     "is_converse(M,r,z) == 
 	\<forall>x[M]. x \<in> z <-> 
@@ -899,6 +905,22 @@
      "[| M(A); M(B); M(Z) |] ==> is_sum(M,A,B,Z) <-> (Z = A+B)"
 by (simp add: is_sum_def sum_def singleton_0 nat_into_M)
 
+lemma (in M_triv_axioms) Inl_in_M_iff [iff]:
+     "M(Inl(a)) <-> M(a)"
+by (simp add: Inl_def) 
+
+lemma (in M_triv_axioms) Inl_abs [simp]:
+     "M(Z) ==> is_Inl(M,a,Z) <-> (Z = Inl(a))"
+by (simp add: is_Inl_def Inl_def)
+
+lemma (in M_triv_axioms) Inr_in_M_iff [iff]:
+     "M(Inr(a)) <-> M(a)"
+by (simp add: Inr_def) 
+
+lemma (in M_triv_axioms) Inr_abs [simp]:
+     "M(Z) ==> is_Inr(M,a,Z) <-> (Z = Inr(a))"
+by (simp add: is_Inr_def Inr_def)
+
 
 subsubsection {*converse of a relation*}
 
@@ -1158,4 +1180,184 @@
 done
 
 
+subsection{*Relativization and Absoluteness for List Operators*}
+
+constdefs
+
+  is_Nil :: "[i=>o, i] => o"
+     --{* because @{term "[] \<equiv> Inl(0)"}*}
+    "is_Nil(M,xs) == \<exists>zero[M]. empty(M,zero) & is_Inl(M,zero,xs)"
+
+  is_Cons :: "[i=>o,i,i,i] => o"
+     --{* because @{term "Cons(a, l) \<equiv> Inr(\<langle>a,l\<rangle>)"}*}
+    "is_Cons(M,a,l,Z) == \<exists>p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)"
+
+
+lemma (in M_triv_axioms) Nil_in_M [intro,simp]: "M(Nil)"
+by (simp add: Nil_def)
+
+lemma (in M_triv_axioms) Nil_abs [simp]: "M(Z) ==> is_Nil(M,Z) <-> (Z = Nil)"
+by (simp add: is_Nil_def Nil_def)
+
+lemma (in M_triv_axioms) Cons_in_M_iff [iff]: "M(Cons(a,l)) <-> M(a) & M(l)"
+by (simp add: Cons_def) 
+
+lemma (in M_triv_axioms) Cons_abs [simp]:
+     "[|M(a); M(l); M(Z)|] ==> is_Cons(M,a,l,Z) <-> (Z = Cons(a,l))"
+by (simp add: is_Cons_def Cons_def)
+
+
+constdefs
+
+  quasilist :: "i => o"
+    "quasilist(xs) == xs=Nil | (\<exists>x l. xs = Cons(x,l))"
+
+  is_quasilist :: "[i=>o,i] => o"
+    "is_quasilist(M,z) == is_Nil(M,z) | (\<exists>x[M]. \<exists>l[M]. is_Cons(M,x,l,z))"
+
+  list_case' :: "[i, [i,i]=>i, i] => i"
+    --{*A version of @{term list_case} that's always defined.*}
+    "list_case'(a,b,xs) == 
+       if quasilist(xs) then list_case(a,b,xs) else 0"  
+
+  is_list_case :: "[i=>o, i, [i,i,i]=>o, i, i] => o"
+    --{*Returns 0 for non-lists*}
+    "is_list_case(M, a, is_b, xs, z) == 
+       (is_Nil(M,xs) --> z=a) &
+       (\<forall>x[M]. \<forall>l[M]. is_Cons(M,x,l,xs) --> is_b(x,l,z)) &
+       (is_quasilist(M,xs) | empty(M,z))"
+
+  hd' :: "i => i"
+    --{*A version of @{term hd} that's always defined.*}
+    "hd'(xs) == if quasilist(xs) then hd(xs) else 0"  
+
+  tl' :: "i => i"
+    --{*A version of @{term tl} that's always defined.*}
+    "tl'(xs) == if quasilist(xs) then tl(xs) else 0"  
+
+  is_hd :: "[i=>o,i,i] => o"
+     --{* @{term "hd([]) = 0"} no constraints if not a list.
+          Avoiding implication prevents the simplifier's looping.*}
+    "is_hd(M,xs,H) == 
+       (is_Nil(M,xs) --> empty(M,H)) &
+       (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | H=x) &
+       (is_quasilist(M,xs) | empty(M,H))"
+
+  is_tl :: "[i=>o,i,i] => o"
+     --{* @{term "tl([]) = []"}; see comments about @{term is_hd}*}
+    "is_tl(M,xs,T) == 
+       (is_Nil(M,xs) --> T=xs) &
+       (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | T=l) &
+       (is_quasilist(M,xs) | empty(M,T))"
+
+subsubsection{*@{term quasilist}: For Case-Splitting with @{term list_case'}*}
+
+lemma [iff]: "quasilist(Nil)"
+by (simp add: quasilist_def)
+
+lemma [iff]: "quasilist(Cons(x,l))"
+by (simp add: quasilist_def)
+
+lemma list_imp_quasilist: "l \<in> list(A) ==> quasilist(l)"
+by (erule list.cases, simp_all)
+
+subsubsection{*@{term list_case'}, the Modified Version of @{term list_case}*}
+
+lemma list_case'_Nil [simp]: "list_case'(a,b,Nil) = a"
+by (simp add: list_case'_def quasilist_def)
+
+lemma list_case'_Cons [simp]: "list_case'(a,b,Cons(x,l)) = b(x,l)"
+by (simp add: list_case'_def quasilist_def)
+
+lemma non_list_case: "~ quasilist(x) ==> list_case'(a,b,x) = 0" 
+by (simp add: quasilist_def list_case'_def) 
+
+lemma list_case'_eq_list_case [simp]:
+     "xs \<in> list(A) ==>list_case'(a,b,xs) = list_case(a,b,xs)"
+by (erule list.cases, simp_all)
+
+lemma (in M_axioms) list_case'_closed [intro,simp]:
+  "[|M(k); M(a); \<forall>x[M]. \<forall>y[M]. M(b(x,y))|] ==> M(list_case'(a,b,k))"
+apply (case_tac "quasilist(k)") 
+ apply (simp add: quasilist_def, force) 
+apply (simp add: non_list_case) 
+done
+
+lemma (in M_triv_axioms) quasilist_abs [simp]: 
+     "M(z) ==> is_quasilist(M,z) <-> quasilist(z)"
+by (auto simp add: is_quasilist_def quasilist_def)
+
+lemma (in M_triv_axioms) list_case_abs [simp]: 
+     "[| relativize2(M,is_b,b); M(k); M(z) |] 
+      ==> is_list_case(M,a,is_b,k,z) <-> z = list_case'(a,b,k)"
+apply (case_tac "quasilist(k)") 
+ prefer 2 
+ apply (simp add: is_list_case_def non_list_case) 
+ apply (force simp add: quasilist_def) 
+apply (simp add: quasilist_def is_list_case_def)
+apply (elim disjE exE) 
+ apply (simp_all add: relativize2_def) 
+done
+
+
+subsubsection{*The Modified Operators @{term hd'} and @{term tl'}*}
+
+lemma (in M_triv_axioms) is_hd_Nil: "is_hd(M,[],Z) <-> empty(M,Z)"
+by (simp add: is_hd_def )
+
+lemma (in M_triv_axioms) is_hd_Cons:
+     "[|M(a); M(l)|] ==> is_hd(M,Cons(a,l),Z) <-> Z = a"
+by (force simp add: is_hd_def ) 
+
+lemma (in M_triv_axioms) hd_abs [simp]:
+     "[|M(x); M(y)|] ==> is_hd(M,x,y) <-> y = hd'(x)"
+apply (simp add: hd'_def)
+apply (intro impI conjI)
+ prefer 2 apply (force simp add: is_hd_def) 
+apply (simp add: quasilist_def is_hd_def )
+apply (elim disjE exE, auto)
+done 
+
+lemma (in M_triv_axioms) is_tl_Nil: "is_tl(M,[],Z) <-> Z = []"
+by (simp add: is_tl_def )
+
+lemma (in M_triv_axioms) is_tl_Cons:
+     "[|M(a); M(l)|] ==> is_tl(M,Cons(a,l),Z) <-> Z = l"
+by (force simp add: is_tl_def ) 
+
+lemma (in M_triv_axioms) tl_abs [simp]:
+     "[|M(x); M(y)|] ==> is_tl(M,x,y) <-> y = tl'(x)"
+apply (simp add: tl'_def)
+apply (intro impI conjI)
+ prefer 2 apply (force simp add: is_tl_def) 
+apply (simp add: quasilist_def is_tl_def )
+apply (elim disjE exE, auto)
+done 
+
+lemma (in M_triv_axioms) relativize1_tl: "relativize1(M, is_tl(M), tl')"  
+by (simp add: relativize1_def)
+
+lemma hd'_Nil: "hd'([]) = 0"
+by (simp add: hd'_def)
+
+lemma hd'_Cons: "hd'(Cons(a,l)) = a"
+by (simp add: hd'_def)
+
+lemma tl'_Nil: "tl'([]) = []"
+by (simp add: tl'_def)
+
+lemma tl'_Cons: "tl'(Cons(a,l)) = l"
+by (simp add: tl'_def)
+
+lemma iterates_tl_Nil: "n \<in> nat ==> tl'^n ([]) = []"
+apply (induct_tac n) 
+apply (simp_all add: tl'_Nil) 
+done
+
+lemma (in M_axioms) tl'_closed: "M(x) ==> M(tl'(x))"
+apply (simp add: tl'_def)
+apply (force simp add: quasilist_def)
+done
+
+
 end