src/ZF/Constructible/Datatype_absolute.thy
changeset 13418 7c0ba9dba978
parent 13409 d4ea094c650e
child 13422 af9bc8d87a75
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Wed Jul 24 16:16:44 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Wed Jul 24 17:59:12 2002 +0200
     1.3 @@ -499,7 +499,7 @@
     1.4      "is_eclose(M,A,Z) == \<forall>u[M]. u \<in> Z <-> mem_eclose(M,A,u)"
     1.5  
     1.6  
     1.7 -locale (open) M_eclose = M_wfrank +
     1.8 +locale (open) M_eclose = M_datatypes +
     1.9   assumes eclose_replacement1: 
    1.10     "M(A) ==> iterates_replacement(M, big_union(M), A)"
    1.11    and eclose_replacement2: 
    1.12 @@ -569,22 +569,25 @@
    1.13    @{text "trans_wfrec_abs"} rather than @{text "trans_wfrec_abs"},
    1.14    which I haven't even proved yet. *}
    1.15  theorem (in M_eclose) transrec_abs:
    1.16 -  "[|Ord(i);  M(i);  M(z);
    1.17 -     transrec_replacement(M,MH,i);  relativize2(M,MH,H);
    1.18 +  "[|transrec_replacement(M,MH,i);  relativize2(M,MH,H);
    1.19 +     Ord(i);  M(i);  M(z);
    1.20       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
    1.21     ==> is_transrec(M,MH,i,z) <-> z = transrec(i,H)" 
    1.22 -by (simp add: trans_wfrec_abs transrec_replacement_def is_transrec_def
    1.23 +apply (rotate_tac 2) 
    1.24 +apply (simp add: trans_wfrec_abs transrec_replacement_def is_transrec_def
    1.25         transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
    1.26 +done
    1.27  
    1.28  
    1.29  theorem (in M_eclose) transrec_closed:
    1.30 -     "[|Ord(i);  M(i);  M(z);
    1.31 -	transrec_replacement(M,MH,i);  relativize2(M,MH,H);
    1.32 +     "[|transrec_replacement(M,MH,i);  relativize2(M,MH,H);
    1.33 +	Ord(i);  M(i);  
    1.34  	\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
    1.35        ==> M(transrec(i,H))"
    1.36 -by (simp add: trans_wfrec_closed transrec_replacement_def is_transrec_def
    1.37 +apply (rotate_tac 2) 
    1.38 +apply (simp add: trans_wfrec_closed transrec_replacement_def is_transrec_def
    1.39         transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
    1.40 -
    1.41 +done
    1.42  
    1.43  
    1.44  subsection{*Absoluteness for the List Operator @{term length}*}
    1.45 @@ -803,6 +806,17 @@
    1.46  apply (simp add: non_formula_case) 
    1.47  done
    1.48  
    1.49 +text{*Compared with @{text formula_case_closed'}, the premise on @{term p} is
    1.50 +      stronger while the other premises are weaker, incorporating typing 
    1.51 +      information.*}
    1.52 +lemma (in M_datatypes) formula_case_closed [intro,simp]:
    1.53 +  "[|p \<in> formula; 
    1.54 +     \<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> M(a(x,y)); 
    1.55 +     \<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> M(b(x,y)); 
    1.56 +     \<forall>x[M]. \<forall>y[M]. x\<in>formula --> y\<in>formula --> M(c(x,y)); 
    1.57 +     \<forall>x[M]. x\<in>formula --> M(d(x))|] ==> M(formula_case(a,b,c,d,p))"
    1.58 +by (erule formula.cases, simp_all) 
    1.59 +
    1.60  lemma (in M_triv_axioms) formula_case_abs [simp]: 
    1.61       "[| relativize2(M,is_a,a); relativize2(M,is_b,b); 
    1.62           relativize2(M,is_c,c); relativize1(M,is_d,d); M(p); M(z) |]