src/ZF/Constructible/Datatype_absolute.thy

--- a/src/ZF/Constructible/Datatype_absolute.thy	Wed Jul 24 16:16:44 2002 +0200
+++ b/src/ZF/Constructible/Datatype_absolute.thy	Wed Jul 24 17:59:12 2002 +0200
@@ -499,7 +499,7 @@
     "is_eclose(M,A,Z) == \<forall>u[M]. u \<in> Z <-> mem_eclose(M,A,u)"
 
 
-locale (open) M_eclose = M_wfrank +
+locale (open) M_eclose = M_datatypes +
  assumes eclose_replacement1: 
    "M(A) ==> iterates_replacement(M, big_union(M), A)"
   and eclose_replacement2: 
@@ -569,22 +569,25 @@
   @{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);
-     transrec_replacement(M,MH,i);  relativize2(M,MH,H);
+  "[|transrec_replacement(M,MH,i);  relativize2(M,MH,H);
+     Ord(i);  M(i);  M(z);
      \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
    ==> is_transrec(M,MH,i,z) <-> z = transrec(i,H)" 
-by (simp add: trans_wfrec_abs transrec_replacement_def is_transrec_def
+apply (rotate_tac 2) 
+apply (simp add: trans_wfrec_abs transrec_replacement_def is_transrec_def
        transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
+done
 
 
 theorem (in M_eclose) transrec_closed:
-     "[|Ord(i);  M(i);  M(z);
-	transrec_replacement(M,MH,i);  relativize2(M,MH,H);
+     "[|transrec_replacement(M,MH,i);  relativize2(M,MH,H);
+	Ord(i);  M(i);  
 	\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
       ==> M(transrec(i,H))"
-by (simp add: trans_wfrec_closed transrec_replacement_def is_transrec_def
+apply (rotate_tac 2) 
+apply (simp add: trans_wfrec_closed transrec_replacement_def is_transrec_def
        transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
-
+done
 
 
 subsection{*Absoluteness for the List Operator @{term length}*}
@@ -803,6 +806,17 @@
 apply (simp add: non_formula_case) 
 done
 
+text{*Compared with @{text formula_case_closed'}, the premise on @{term p} is
+      stronger while the other premises are weaker, incorporating typing 
+      information.*}
+lemma (in M_datatypes) formula_case_closed [intro,simp]:
+  "[|p \<in> formula; 
+     \<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> M(a(x,y)); 
+     \<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> M(b(x,y)); 
+     \<forall>x[M]. \<forall>y[M]. x\<in>formula --> y\<in>formula --> M(c(x,y)); 
+     \<forall>x[M]. x\<in>formula --> M(d(x))|] ==> M(formula_case(a,b,c,d,p))"
+by (erule formula.cases, simp_all) 
+
 lemma (in M_triv_axioms) formula_case_abs [simp]: 
      "[| relativize2(M,is_a,a); relativize2(M,is_b,b); 
          relativize2(M,is_c,c); relativize1(M,is_d,d); M(p); M(z) |]