# HG changeset patch
# User paulson
# Date 1027429632 -7200
# Node ID d4ea094c650ed7e2cfe81ffbbd3c5f58ecc4847e
# Parent  024af54a625c9fea2fd57b84a4ddc645396c7f6e
Relativization and Separation for the function "nth"

diff -r 024af54a625c -r d4ea094c650e src/ZF/Constructible/Datatype_absolute.thy
--- a/src/ZF/Constructible/Datatype_absolute.thy	Mon Jul 22 13:55:44 2002 +0200
+++ b/src/ZF/Constructible/Datatype_absolute.thy	Tue Jul 23 15:07:12 2002 +0200
@@ -321,9 +321,9 @@
   "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"
+      \<lambda>x h. Lambda (list(A),
+                    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) 
@@ -629,10 +629,6 @@
 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))" 
@@ -649,20 +645,18 @@
        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)|] 
+lemma (in M_datatypes) nth_abs [simp]:
+     "[|iterates_replacement(M, %l t. is_tl(M,l,t), l);
+        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
 
 
-
-
 subsection{*Relativization and Absoluteness for the @{term formula} Constructors*}
 
 constdefs
@@ -912,35 +906,29 @@
                      le_imp_subset formula_N_mono)
 done
 
-lemma Nand_in_formula_N:
-    "[|p \<in> formula; q \<in> formula|]
-     ==> Nand(p,q) \<in> formula_N(succ(succ(depth(p))) \<union> succ(succ(depth(q))))"
-by (simp add: succ_Un_distrib [symmetric] formula_imp_formula_N le_Un_iff) 
-
-
 text{*Express @{term formula_rec} without using @{term rank} or @{term Vset},
 neither of which is absolute.*}
 lemma (in M_triv_axioms) formula_rec_eq:
   "p \<in> formula ==>
    formula_rec(a,b,c,d,p) = 
    transrec (succ(depth(p)),
-      \<lambda>x h. Lambda (formula_N(x),
+      \<lambda>x h. Lambda (formula,
              formula_case' (a, b,
                 \<lambda>u v. c(u, v, h ` succ(depth(u)) ` u, 
                               h ` succ(depth(v)) ` v),
                 \<lambda>u. d(u, h ` succ(depth(u)) ` u)))) 
    ` p"
 apply (induct_tac p)
-txt{*Base case for @{term Member}*}
-apply (subst transrec, simp) 
-txt{*Base case for @{term Equal}*}
-apply (subst transrec, simp)
-txt{*Inductive step for @{term Nand}*}
-apply (subst transrec)
-apply (simp add: succ_Un_distrib Nand_in_formula_N)
+   txt{*Base case for @{term Member}*}
+   apply (subst transrec, simp add: formula.intros) 
+  txt{*Base case for @{term Equal}*}
+  apply (subst transrec, simp add: formula.intros)
+ txt{*Inductive step for @{term Nand}*}
+ apply (subst transrec) 
+ apply (simp add: succ_Un_distrib formula.intros)
 txt{*Inductive step for @{term Forall}*}
 apply (subst transrec) 
-apply (simp add: formula_imp_formula_N) 
+apply (simp add: formula_imp_formula_N formula.intros) 
 done
 
 
diff -r 024af54a625c -r d4ea094c650e src/ZF/Constructible/Rec_Separation.thy
--- a/src/ZF/Constructible/Rec_Separation.thy	Mon Jul 22 13:55:44 2002 +0200
+++ b/src/ZF/Constructible/Rec_Separation.thy	Tue Jul 23 15:07:12 2002 +0200
@@ -1124,6 +1124,239 @@
 declare eclose_abs [intro,simp]
 
 
+subsection{*Internalized Forms of Data Structuring Operators*}
+
+subsubsection{*The Formula @{term is_Inl}, Internalized*}
+
+(*  is_Inl(M,a,z) == \<exists>zero[M]. empty(M,zero) & pair(M,zero,a,z) *)
+constdefs Inl_fm :: "[i,i]=>i"
+    "Inl_fm(a,z) == Exists(And(empty_fm(0), pair_fm(0,succ(a),succ(z))))"
+
+lemma Inl_type [TC]:
+     "[| x \<in> nat; z \<in> nat |] ==> Inl_fm(x,z) \<in> formula"
+by (simp add: Inl_fm_def) 
+
+lemma sats_Inl_fm [simp]:
+   "[| x \<in> nat; z \<in> nat; env \<in> list(A)|]
+    ==> sats(A, Inl_fm(x,z), env) <-> is_Inl(**A, nth(x,env), nth(z,env))"
+by (simp add: Inl_fm_def is_Inl_def)
+
+lemma Inl_iff_sats:
+      "[| nth(i,env) = x; nth(k,env) = z; 
+          i \<in> nat; k \<in> nat; env \<in> list(A)|]
+       ==> is_Inl(**A, x, z) <-> sats(A, Inl_fm(i,k), env)"
+by simp
+
+theorem Inl_reflection:
+     "REFLECTS[\<lambda>x. is_Inl(L,f(x),h(x)), 
+               \<lambda>i x. is_Inl(**Lset(i),f(x),h(x))]"
+apply (simp only: is_Inl_def setclass_simps)
+apply (intro FOL_reflections function_reflections)  
+done
+
+
+subsubsection{*The Formula @{term is_Inr}, Internalized*}
+
+(*  is_Inr(M,a,z) == \<exists>n1[M]. number1(M,n1) & pair(M,n1,a,z) *)
+constdefs Inr_fm :: "[i,i]=>i"
+    "Inr_fm(a,z) == Exists(And(number1_fm(0), pair_fm(0,succ(a),succ(z))))"
+
+lemma Inr_type [TC]:
+     "[| x \<in> nat; z \<in> nat |] ==> Inr_fm(x,z) \<in> formula"
+by (simp add: Inr_fm_def) 
+
+lemma sats_Inr_fm [simp]:
+   "[| x \<in> nat; z \<in> nat; env \<in> list(A)|]
+    ==> sats(A, Inr_fm(x,z), env) <-> is_Inr(**A, nth(x,env), nth(z,env))"
+by (simp add: Inr_fm_def is_Inr_def)
+
+lemma Inr_iff_sats:
+      "[| nth(i,env) = x; nth(k,env) = z; 
+          i \<in> nat; k \<in> nat; env \<in> list(A)|]
+       ==> is_Inr(**A, x, z) <-> sats(A, Inr_fm(i,k), env)"
+by simp
+
+theorem Inr_reflection:
+     "REFLECTS[\<lambda>x. is_Inr(L,f(x),h(x)), 
+               \<lambda>i x. is_Inr(**Lset(i),f(x),h(x))]"
+apply (simp only: is_Inr_def setclass_simps)
+apply (intro FOL_reflections function_reflections)  
+done
+
+
+subsubsection{*The Formula @{term is_Nil}, Internalized*}
+
+(* is_Nil(M,xs) == \<exists>zero[M]. empty(M,zero) & is_Inl(M,zero,xs) *)
+
+constdefs Nil_fm :: "i=>i"
+    "Nil_fm(x) == Exists(And(empty_fm(0), Inl_fm(0,succ(x))))"
+ 
+lemma Nil_type [TC]: "x \<in> nat ==> Nil_fm(x) \<in> formula"
+by (simp add: Nil_fm_def) 
+
+lemma sats_Nil_fm [simp]:
+   "[| x \<in> nat; env \<in> list(A)|]
+    ==> sats(A, Nil_fm(x), env) <-> is_Nil(**A, nth(x,env))"
+by (simp add: Nil_fm_def is_Nil_def)
+
+lemma Nil_iff_sats:
+      "[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
+       ==> is_Nil(**A, x) <-> sats(A, Nil_fm(i), env)"
+by simp
+
+theorem Nil_reflection:
+     "REFLECTS[\<lambda>x. is_Nil(L,f(x)), 
+               \<lambda>i x. is_Nil(**Lset(i),f(x))]"
+apply (simp only: is_Nil_def setclass_simps)
+apply (intro FOL_reflections function_reflections Inl_reflection)  
+done
+
+
+subsubsection{*The Formula @{term is_Nil}, Internalized*}
 
 
+(*  "is_Cons(M,a,l,Z) == \<exists>p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)" *)
+constdefs Cons_fm :: "[i,i,i]=>i"
+    "Cons_fm(a,l,Z) == 
+       Exists(And(pair_fm(succ(a),succ(l),0), Inr_fm(0,succ(Z))))"
+
+lemma Cons_type [TC]:
+     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> Cons_fm(x,y,z) \<in> formula"
+by (simp add: Cons_fm_def) 
+
+lemma sats_Cons_fm [simp]:
+   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
+    ==> sats(A, Cons_fm(x,y,z), env) <-> 
+       is_Cons(**A, nth(x,env), nth(y,env), nth(z,env))"
+by (simp add: Cons_fm_def is_Cons_def)
+
+lemma Cons_iff_sats:
+      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
+          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
+       ==>is_Cons(**A, x, y, z) <-> sats(A, Cons_fm(i,j,k), env)"
+by simp
+
+theorem Cons_reflection:
+     "REFLECTS[\<lambda>x. is_Cons(L,f(x),g(x),h(x)), 
+               \<lambda>i x. is_Cons(**Lset(i),f(x),g(x),h(x))]"
+apply (simp only: is_Cons_def setclass_simps)
+apply (intro FOL_reflections pair_reflection Inr_reflection)  
+done
+
+subsubsection{*The Formula @{term is_quasilist}, Internalized*}
+
+(* is_quasilist(M,xs) == is_Nil(M,z) | (\<exists>x[M]. \<exists>l[M]. is_Cons(M,x,l,z))" *)
+
+constdefs quasilist_fm :: "i=>i"
+    "quasilist_fm(x) == 
+       Or(Nil_fm(x), Exists(Exists(Cons_fm(1,0,succ(succ(x))))))"
+ 
+lemma quasilist_type [TC]: "x \<in> nat ==> quasilist_fm(x) \<in> formula"
+by (simp add: quasilist_fm_def) 
+
+lemma sats_quasilist_fm [simp]:
+   "[| x \<in> nat; env \<in> list(A)|]
+    ==> sats(A, quasilist_fm(x), env) <-> is_quasilist(**A, nth(x,env))"
+by (simp add: quasilist_fm_def is_quasilist_def)
+
+lemma quasilist_iff_sats:
+      "[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
+       ==> is_quasilist(**A, x) <-> sats(A, quasilist_fm(i), env)"
+by simp
+
+theorem quasilist_reflection:
+     "REFLECTS[\<lambda>x. is_quasilist(L,f(x)), 
+               \<lambda>i x. is_quasilist(**Lset(i),f(x))]"
+apply (simp only: is_quasilist_def setclass_simps)
+apply (intro FOL_reflections Nil_reflection Cons_reflection)  
+done
+
+
+subsection{*Absoluteness for the Function @{term nth}*}
+
+
+subsubsection{*The Formula @{term is_tl}, Internalized*}
+
+(*     "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))" *)
+constdefs tl_fm :: "[i,i]=>i"
+    "tl_fm(xs,T) == 
+       And(Implies(Nil_fm(xs), Equal(T,xs)),
+           And(Forall(Forall(Or(Neg(Cons_fm(1,0,xs#+2)), Equal(T#+2,0)))),
+               Or(quasilist_fm(xs), empty_fm(T))))"
+
+lemma tl_type [TC]:
+     "[| x \<in> nat; y \<in> nat |] ==> tl_fm(x,y) \<in> formula"
+by (simp add: tl_fm_def) 
+
+lemma sats_tl_fm [simp]:
+   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
+    ==> sats(A, tl_fm(x,y), env) <-> is_tl(**A, nth(x,env), nth(y,env))"
+by (simp add: tl_fm_def is_tl_def)
+
+lemma tl_iff_sats:
+      "[| nth(i,env) = x; nth(j,env) = y;
+          i \<in> nat; j \<in> nat; env \<in> list(A)|]
+       ==> is_tl(**A, x, y) <-> sats(A, tl_fm(i,j), env)"
+by simp
+
+theorem tl_reflection:
+     "REFLECTS[\<lambda>x. is_tl(L,f(x),g(x)), 
+               \<lambda>i x. is_tl(**Lset(i),f(x),g(x))]"
+apply (simp only: is_tl_def setclass_simps)
+apply (intro FOL_reflections Nil_reflection Cons_reflection
+             quasilist_reflection empty_reflection)  
+done
+
+
+subsubsection{*An Instance of Replacement for @{term nth}*}
+
+lemma nth_replacement_Reflects:
+ "REFLECTS
+   [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
+         is_wfrec(L, iterates_MH(L, is_tl(L), z), memsn, u, y)),
+    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and>
+         is_wfrec(**Lset(i), 
+                  iterates_MH(**Lset(i), 
+                          is_tl(**Lset(i)), z), memsn, u, y))]"
+by (intro FOL_reflections function_reflections is_wfrec_reflection 
+          iterates_MH_reflection list_functor_reflection tl_reflection) 
+
+lemma nth_replacement: 
+   "L(w) ==> iterates_replacement(L, %l t. is_tl(L,l,t), w)"
+apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
+apply (rule strong_replacementI) 
+apply (rule rallI)   
+apply (rule separation_CollectI) 
+apply (subgoal_tac "L(Memrel(succ(n)))") 
+apply (rule_tac A="{A,n,w,z,Memrel(succ(n))}" in subset_LsetE, blast ) 
+apply (rule ReflectsE [OF nth_replacement_Reflects], assumption)
+apply (drule subset_Lset_ltD, assumption) 
+apply (erule reflection_imp_L_separation)
+  apply (simp_all add: lt_Ord2 Memrel_closed)
+apply (elim conjE) 
+apply (rule DPow_LsetI)
+apply (rename_tac v) 
+apply (rule bex_iff_sats conj_iff_sats)+
+apply (rule_tac env = "[u,v,A,z,w,Memrel(succ(n))]" in mem_iff_sats)
+apply (rule sep_rules | simp)+
+apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
+apply (rule sep_rules quasinat_iff_sats tl_iff_sats | simp)+
+done
+
+ML
+{*
+bind_thm ("nth_abs_lemma", datatypes_L (thm "M_datatypes.nth_abs"));
+*}
+
+text{*Instantiating theorem @{text nth_abs} for @{term L}*}
+lemma nth_abs [simp]:
+     "[|L(A); n \<in> nat; l \<in> list(A); L(Z)|] 
+      ==> is_nth(L,n,l,Z) <-> Z = nth(n,l)"
+apply (rule nth_abs_lemma)
+apply (blast intro: nth_replacement transL list_closed, assumption+)
+done
+
 end