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.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) |]
```