# HG changeset patch
# User paulson
# Date 1026400708 -7200
# Node ID 626b79677dfa0017e802b5b4c5b447df55ee3067
# Parent  7d4441c8c46a1cbf9d1e731f7a45cbeedefd35ba
tidied

diff -r 7d4441c8c46a -r 626b79677dfa src/ZF/Constructible/Datatype_absolute.thy
--- a/src/ZF/Constructible/Datatype_absolute.thy	Thu Jul 11 16:57:14 2002 +0200
+++ b/src/ZF/Constructible/Datatype_absolute.thy	Thu Jul 11 17:18:28 2002 +0200
@@ -105,8 +105,7 @@
             z = nat_case(v, \<lambda>m. F(g`m), n))"
 by (simp add: iterates_nat_def recursor_def transrec_def 
               eclose_sing_Ord_eq trans_wfrec_relativize nat_into_M
-              wf_Memrel trans_Memrel relation_Memrel nat_case_closed)
-
+              wf_Memrel trans_Memrel relation_Memrel)
 
 lemma (in M_wfrank) iterates_closed [intro,simp]:
   "[|n \<in> nat; M(v); \<forall>x[M]. M(F(x));
@@ -121,32 +120,54 @@
               wf_Memrel trans_Memrel relation_Memrel nat_case_closed)
 
 
+constdefs
+  is_list_functor :: "[i=>o,i,i,i] => o"
+    "is_list_functor(M,A,X,Z) == 
+        \<exists>n1[M]. \<exists>AX[M]. 
+         number1(M,n1) & cartprod(M,A,X,AX) & is_sum(M,n1,AX,Z)"
+
+  is_list_case :: "[i=>o,i,i,i,i] => o"
+    "is_list_case(M,A,g,x,y) == 
+        is_nat_case(M, 0, 
+             \<lambda>m u. \<exists>gm[M]. fun_apply(M,g,m,gm) & is_list_functor(M,A,gm,u),
+             x, y)"
+
+lemma (in M_axioms) list_functor_abs [simp]: 
+     "[| M(A); M(X); M(Z) |] ==> is_list_functor(M,A,X,Z) <-> (Z = {0} + A*X)"
+by (simp add: is_list_functor_def singleton_0 nat_into_M)
+
+
 locale M_datatypes = M_wfrank +
-(*THEY NEED RELATIVIZATION*)
   assumes list_replacement1: 
-	   "[|M(A); n \<in> nat|] ==> 
-	    strong_replacement(M, 
-	      \<lambda>x z. \<exists>y[M]. \<exists>g[M]. \<exists>sucn[M]. \<exists>memr[M]. 
-                     pair(M,x,y,z) & successor(M,n,sucn) & 
-                     membership(M,sucn,memr) &
-		     is_recfun (memr, x,
-				\<lambda>n f. nat_case(0, \<lambda>m. {0} + A \<times> f`m, n), g) &
-		     y = nat_case(0, \<lambda>m. {0} + A \<times> g`m, x))"
+       "[|M(A); n \<in> nat|] ==> 
+	strong_replacement(M, 
+	  \<lambda>x z. \<exists>y[M]. \<exists>g[M]. \<exists>sucn[M]. \<exists>memr[M]. 
+		 pair(M,x,y,z) & successor(M,n,sucn) & 
+		 membership(M,sucn,memr) &
+		 M_is_recfun (M, memr, x,
+	              \<lambda>n f z. z = nat_case(0, \<lambda>m. {0} + A * f`m, n), g) &
+		 is_nat_case(M, 0, 
+                      \<lambda>m u. is_list_functor(M,A,g`m,u), x, y))"
+(*THEY NEED RELATIVIZATION*)
       and list_replacement2: 
-           "M(A) ==> strong_replacement(M, \<lambda>x y. y = (\<lambda>X. {0} + A \<times> X)^x (0))"
+           "M(A) ==> strong_replacement(M, \<lambda>x y. y = (\<lambda>X. {0} + A * X)^x (0))"
+
 
 
 lemma (in M_datatypes) list_replacement1':
   "[|M(A); n \<in> nat|]
    ==> strong_replacement
-	  (M, \<lambda>x y. \<exists>z[M]. y = \<langle>x,z\<rangle> &
+	  (M, \<lambda>x z. \<exists>y[M]. z = \<langle>x,y\<rangle> &
                (\<exists>g[M]. is_recfun (Memrel(succ(n)), x,
-		          \<lambda>n f. nat_case(0, \<lambda>m. {0} + A \<times> f`m, n), g) &
- 	       z = nat_case(0, \<lambda>m. {0} + A \<times> g ` m, x)))"
-by (insert list_replacement1, simp add: nat_into_M) 
+		          \<lambda>n f. nat_case(0, \<lambda>m. {0} + A * f`m, n), g) &
+ 	       y = nat_case(0, \<lambda>m. {0} + A * g ` m, x)))"
+apply (insert list_replacement1 [of A n], simp add: nat_into_M)
+apply (simp add: nat_into_M apply_abs
+                 is_recfun_abs [of "\<lambda>n f. nat_case(0, \<lambda>m. {0} + A * f`m, n)"])
+done
 
 lemma (in M_datatypes) list_replacement2': 
-  "M(A) ==> strong_replacement(M, \<lambda>x y. y = (\<lambda>X. {0} + A \<times> X)^x (0))"
+  "M(A) ==> strong_replacement(M, \<lambda>x y. y = (\<lambda>X. {0} + A * X)^x (0))"
 by (insert list_replacement2, simp add: nat_into_M) 
 
 
diff -r 7d4441c8c46a -r 626b79677dfa src/ZF/Constructible/Relative.thy
--- a/src/ZF/Constructible/Relative.thy	Thu Jul 11 16:57:14 2002 +0200
+++ b/src/ZF/Constructible/Relative.thy	Thu Jul 11 17:18:28 2002 +0200
@@ -49,6 +49,12 @@
     "cartprod(M,A,B,z) == 
 	\<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,u)))"
 
+  is_sum :: "[i=>o,i,i,i] => o"
+    "is_sum(M,A,B,Z) == 
+       \<exists>A0[M]. \<exists>n1[M]. \<exists>s1[M]. \<exists>B1[M]. 
+       number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) &
+       cartprod(M,s1,B,B1) & union(M,A0,B1,Z)"
+
   is_converse :: "[i=>o,i,i] => o"
     "is_converse(M,r,z) == 
 	\<forall>x[M]. x \<in> z <-> 
@@ -163,6 +169,15 @@
   number3 :: "[i=>o,i] => o"
     "number3(M,a) == (\<exists>x[M]. number2(M,x) & successor(M,x,a))"
 
+  is_quasinat :: "[i=>o,i] => o"
+    "is_quasinat(M,z) == empty(M,z) | (\<exists>m[M]. successor(M,m,z))"
+
+  is_nat_case :: "[i=>o, i, [i,i]=>o, i, i] => o"
+    "is_nat_case(M, a, is_b, k, z) == 
+       (empty(M,k) --> z=a) &
+       (\<forall>m[M]. successor(M,m,k) --> is_b(m,z)) &
+       (is_quasinat(M,k) | z=0)"
+
 
 subsection {*The relativized ZF axioms*}
 constdefs
@@ -607,13 +622,30 @@
      "n \<in> nat ==> M(n)"
 by (induct n rule: nat_induct, simp_all)
 
-lemma (in M_triv_axioms) nat_case_closed:
+lemma (in M_triv_axioms) nat_case_closed [intro,simp]:
   "[|M(k); M(a); \<forall>m[M]. M(b(m))|] ==> M(nat_case(a,b,k))"
 apply (case_tac "k=0", simp) 
 apply (case_tac "\<exists>m. k = succ(m)", force)
 apply (simp add: nat_case_def) 
 done
 
+lemma (in M_triv_axioms) quasinat_abs [simp]: 
+     "M(z) ==> is_quasinat(M,z) <-> quasinat(z)"
+by (auto simp add: is_quasinat_def quasinat_def)
+
+lemma (in M_triv_axioms) nat_case_abs [simp]: 
+  assumes b_abs: "!!x y. M(x) --> M(y) --> (is_b(x,y) <-> y = b(x))"
+  shows
+     "[| M(k); M(z) |] ==> is_nat_case(M,a,is_b,k,z) <-> z = nat_case(a,b,k)"
+apply (case_tac "quasinat(k)") 
+ prefer 2 
+ apply (simp add: is_nat_case_def non_nat_case) 
+ apply (force simp add: quasinat_def) 
+apply (simp add: quasinat_def is_nat_case_def)
+apply (elim disjE exE) 
+ apply (simp_all add: b_abs) 
+done
+
 lemma (in M_triv_axioms) Inl_in_M_iff [iff]:
      "M(Inl(a)) <-> M(a)"
 by (simp add: Inl_def) 
@@ -831,6 +863,10 @@
      "[| M(A); M(B) |] ==> M(A+B)"
 by (simp add: sum_def)
 
+lemma (in M_axioms) sum_abs [simp]:
+     "[| 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)
+
 
 subsubsection {*converse of a relation*}
 
@@ -1096,4 +1132,5 @@
 apply (simp add: funspace_succ nat_into_M) 
 done
 
+
 end
diff -r 7d4441c8c46a -r 626b79677dfa src/ZF/Constructible/Separation.thy
--- a/src/ZF/Constructible/Separation.thy	Thu Jul 11 16:57:14 2002 +0200
+++ b/src/ZF/Constructible/Separation.thy	Thu Jul 11 17:18:28 2002 +0200
@@ -536,7 +536,7 @@
 bind_thm ("exists_is_recfun_indstep", axiomsL (thm "M_axioms.exists_is_recfun_indstep"));
 bind_thm ("wellfounded_exists_is_recfun", axiomsL (thm "M_axioms.wellfounded_exists_is_recfun"));
 bind_thm ("wf_exists_is_recfun", axiomsL (thm "M_axioms.wf_exists_is_recfun")); 
-bind_thm ("is_recfun_iff_M", axiomsL (thm "M_axioms.is_recfun_iff_M"));
+bind_thm ("is_recfun_abs", axiomsL (thm "M_axioms.is_recfun_abs"));
 bind_thm ("irreflexive_abs", axiomsL (thm "M_axioms.irreflexive_abs"));  
 bind_thm ("transitive_rel_abs", axiomsL (thm "M_axioms.transitive_rel_abs"));  
 bind_thm ("linear_rel_abs", axiomsL (thm "M_axioms.linear_rel_abs"));  
diff -r 7d4441c8c46a -r 626b79677dfa src/ZF/Constructible/WF_absolute.thy
--- a/src/ZF/Constructible/WF_absolute.thy	Thu Jul 11 16:57:14 2002 +0200
+++ b/src/ZF/Constructible/WF_absolute.thy	Thu Jul 11 17:18:28 2002 +0200
@@ -262,7 +262,7 @@
       separation
 	   (M, \<lambda>x. ~ (\<exists>f[M]. is_recfun(r^+, x, %x f. range(f), f)))"
 apply (insert wfrank_separation [of r])
-apply (simp add: is_recfun_iff_M [of concl: _ _ "%x. range", THEN iff_sym])
+apply (simp add: is_recfun_abs [of "%x. range"])
 done
 
 lemma (in M_wfrank) wfrank_strong_replacement':
@@ -271,7 +271,7 @@
 		  pair(M,x,y,z) & is_recfun(r^+, x, %x f. range(f), f) &
 		  y = range(f))"
 apply (insert wfrank_strong_replacement [of r])
-apply (simp add: is_recfun_iff_M [of concl: _ _ "%x. range", THEN iff_sym])
+apply (simp add: is_recfun_abs [of "%x. range"])
 done
 
 lemma (in M_wfrank) Ord_wfrank_separation':
@@ -279,7 +279,7 @@
       separation (M, \<lambda>x. 
          ~ (\<forall>f[M]. is_recfun(r^+, x, \<lambda>x. range, f) --> Ord(range(f))))" 
 apply (insert Ord_wfrank_separation [of r])
-apply (simp add: is_recfun_iff_M [of concl: _ _ "%x. range", THEN iff_sym])
+apply (simp add: is_recfun_abs [of "%x. range"])
 done
 
 text{*This function, defined using replacement, is a rank function for
diff -r 7d4441c8c46a -r 626b79677dfa src/ZF/Constructible/WFrec.thy
--- a/src/ZF/Constructible/WFrec.thy	Thu Jul 11 16:57:14 2002 +0200
+++ b/src/ZF/Constructible/WFrec.thy	Thu Jul 11 17:18:28 2002 +0200
@@ -283,10 +283,10 @@
                pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) &
                xa \<in> r & MH(x, f_r_sx, y))"
 
-lemma (in M_axioms) is_recfun_iff_M:
-     "[| M(r); M(a); M(f); \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g));
-       \<forall>x g y. M(x) --> M(g) --> M(y) --> MH(x,g,y) <-> y = H(x,g) |] ==>
-       is_recfun(r,a,H,f) <-> M_is_recfun(M,r,a,MH,f)"
+lemma (in M_axioms) is_recfun_abs:
+     "[| \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g));  M(r); M(a); M(f); 
+         \<forall>x g y. M(x) --> M(g) --> M(y) --> MH(x,g,y) <-> y = H(x,g) |] 
+      ==> M_is_recfun(M,r,a,MH,f) <-> is_recfun(r,a,H,f)"
 apply (simp add: M_is_recfun_def is_recfun_relativize)
 apply (rule rall_cong)
 apply (blast dest: transM)
@@ -300,7 +300,7 @@
 
 
 constdefs
- (*This expresses ordinal addition as a formula in the LAST.  It also 
+ (*This expresses ordinal addition in the language of ZF.  It also 
    provides an abbreviation that can be used in the instance of strong
    replacement below.  Here j is used to define the relation, namely
    Memrel(succ(j)), while x determines the domain of f.*)
@@ -367,7 +367,7 @@
 	f \<in> a \<rightarrow> range(f) & (\<forall>x. M(x) --> x < a --> f`x = i Un f``x)"
 apply (frule lt_Ord) 
 apply (simp add: is_oadd_fun_def Memrel_closed Un_closed 
-             is_recfun_iff_M [of concl: _ _ "%x g. i Un g``x", THEN iff_sym]
+             is_recfun_abs [of "%x g. i Un g``x"]
              image_closed is_recfun_iff_equation  
              Ball_def lt_trans [OF ltI, of _ a] lt_Memrel)
 apply (simp add: lt_def) 
@@ -382,8 +382,7 @@
 		  (\<exists>g[M]. is_recfun(Memrel(succ(j)),x,%x g. i Un g``x,g) & 
 		  y = i Un g``x))" 
 apply (insert oadd_strong_replacement [of i j]) 
-apply (simp add: Memrel_closed Un_closed image_closed is_oadd_fun_def
-                 is_recfun_iff_M)  
+apply (simp add: is_oadd_fun_def is_recfun_abs [of "%x g. i Un g``x"])  
 done