Re-organization of Constructible theories
authorpaulson
Wed Oct 09 11:07:13 2002 +0200 (2002-10-09 ago)
changeset 1363499a593b49b04
parent 13633 b03a36b8d528
child 13635 c41e88151b54
Re-organization of Constructible theories
src/ZF/Constructible/AC_in_L.thy
src/ZF/Constructible/DPow_absolute.thy
src/ZF/Constructible/Datatype_absolute.thy
src/ZF/Constructible/Formula.thy
src/ZF/Constructible/Internalize.thy
src/ZF/Constructible/L_axioms.thy
src/ZF/Constructible/MetaExists.thy
src/ZF/Constructible/Normal.thy
src/ZF/Constructible/ROOT.ML
src/ZF/Constructible/Rank.thy
src/ZF/Constructible/Rank_Separation.thy
src/ZF/Constructible/Rec_Separation.thy
src/ZF/Constructible/Reflection.thy
src/ZF/Constructible/Relative.thy
src/ZF/Constructible/Satisfies_absolute.thy
src/ZF/Constructible/Separation.thy
src/ZF/Constructible/WF_absolute.thy
src/ZF/Constructible/WFrec.thy
src/ZF/Constructible/Wellorderings.thy
src/ZF/IsaMakefile
src/ZF/OrderArith.thy
src/ZF/WF.thy
     1.1 --- a/src/ZF/Constructible/AC_in_L.thy	Tue Oct 08 14:09:18 2002 +0200
     1.2 +++ b/src/ZF/Constructible/AC_in_L.thy	Wed Oct 09 11:07:13 2002 +0200
     1.3 @@ -1,7 +1,6 @@
     1.4  (*  Title:      ZF/Constructible/AC_in_L.thy
     1.5      ID: $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   2002  University of Cambridge
     1.8  *)
     1.9  
    1.10  header {* The Axiom of Choice Holds in L! *}
     2.1 --- a/src/ZF/Constructible/DPow_absolute.thy	Tue Oct 08 14:09:18 2002 +0200
     2.2 +++ b/src/ZF/Constructible/DPow_absolute.thy	Wed Oct 09 11:07:13 2002 +0200
     2.3 @@ -1,7 +1,6 @@
     2.4  (*  Title:      ZF/Constructible/DPow_absolute.thy
     2.5      ID:         $Id$
     2.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 -    Copyright   2002  University of Cambridge
     2.8  *)
     2.9  
    2.10  header {*Absoluteness for the Definable Powerset Function*}
    2.11 @@ -522,14 +521,14 @@
    2.12     ==> is_Lset(M,i,z) <-> z = Lset(i)"
    2.13  apply (simp add: is_Lset_def Lset_eq_transrec_DPow') 
    2.14  apply (rule transrec_abs)  
    2.15 -apply (simp_all add: transrec_rep' relativize2_def RepFun_DPow_apply_closed)
    2.16 +apply (simp_all add: transrec_rep' relation2_def RepFun_DPow_apply_closed)
    2.17  done
    2.18  
    2.19  lemma (in M_Lset) Lset_closed:
    2.20    "[|Ord(i);  M(i)|] ==> M(Lset(i))"
    2.21  apply (simp add: Lset_eq_transrec_DPow') 
    2.22  apply (rule transrec_closed [OF transrec_rep']) 
    2.23 -apply (simp_all add: relativize2_def RepFun_DPow_apply_closed)
    2.24 +apply (simp_all add: relation2_def RepFun_DPow_apply_closed)
    2.25  done
    2.26  
    2.27  
    2.28 @@ -629,7 +628,6 @@
    2.29      "constructible(M,x) ==
    2.30         \<exists>i[M]. \<exists>Li[M]. ordinal(M,i) & is_Lset(M,i,Li) & x \<in> Li"
    2.31  
    2.32 -
    2.33  theorem V_equals_L_in_L:
    2.34    "L(x) ==> constructible(L,x)"
    2.35  apply (simp add: constructible_def Lset_abs Lset_closed) 
    2.36 @@ -637,5 +635,4 @@
    2.37  apply (blast intro: Ord_in_L) 
    2.38  done
    2.39  
    2.40 -
    2.41  end
     3.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Tue Oct 08 14:09:18 2002 +0200
     3.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Wed Oct 09 11:07:13 2002 +0200
     3.3 @@ -1,7 +1,6 @@
     3.4  (*  Title:      ZF/Constructible/Datatype_absolute.thy
     3.5      ID: $Id$
     3.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 -    Copyright   2002  University of Cambridge
     3.8  *)
     3.9  
    3.10  header {*Absoluteness Properties for Recursive Datatypes*}
    3.11 @@ -127,38 +126,38 @@
    3.12           wfrec_replacement(M, iterates_MH(M,isF,v), Memrel(succ(n)))"
    3.13  
    3.14  lemma (in M_basic) iterates_MH_abs:
    3.15 -  "[| relativize1(M,isF,F); M(n); M(g); M(z) |] 
    3.16 +  "[| relation1(M,isF,F); M(n); M(g); M(z) |] 
    3.17     ==> iterates_MH(M,isF,v,n,g,z) <-> z = nat_case(v, \<lambda>m. F(g`m), n)"
    3.18  by (simp add: nat_case_abs [of _ "\<lambda>m. F(g ` m)"]
    3.19 -              relativize1_def iterates_MH_def)  
    3.20 +              relation1_def iterates_MH_def)  
    3.21  
    3.22  lemma (in M_basic) iterates_imp_wfrec_replacement:
    3.23 -  "[|relativize1(M,isF,F); n \<in> nat; iterates_replacement(M,isF,v)|] 
    3.24 +  "[|relation1(M,isF,F); n \<in> nat; iterates_replacement(M,isF,v)|] 
    3.25     ==> wfrec_replacement(M, \<lambda>n f z. z = nat_case(v, \<lambda>m. F(f`m), n), 
    3.26                         Memrel(succ(n)))" 
    3.27  by (simp add: iterates_replacement_def iterates_MH_abs)
    3.28  
    3.29  theorem (in M_trancl) iterates_abs:
    3.30 -  "[| iterates_replacement(M,isF,v); relativize1(M,isF,F);
    3.31 +  "[| iterates_replacement(M,isF,v); relation1(M,isF,F);
    3.32        n \<in> nat; M(v); M(z); \<forall>x[M]. M(F(x)) |] 
    3.33     ==> is_wfrec(M, iterates_MH(M,isF,v), Memrel(succ(n)), n, z) <->
    3.34         z = iterates(F,n,v)" 
    3.35  apply (frule iterates_imp_wfrec_replacement, assumption+)
    3.36  apply (simp add: wf_Memrel trans_Memrel relation_Memrel nat_into_M
    3.37 -                 relativize2_def iterates_MH_abs 
    3.38 +                 relation2_def iterates_MH_abs 
    3.39                   iterates_nat_def recursor_def transrec_def 
    3.40                   eclose_sing_Ord_eq nat_into_M
    3.41           trans_wfrec_abs [of _ _ _ _ "\<lambda>n g. nat_case(v, \<lambda>m. F(g`m), n)"])
    3.42  done
    3.43  
    3.44  
    3.45 -lemma (in M_wfrank) iterates_closed [intro,simp]:
    3.46 -  "[| iterates_replacement(M,isF,v); relativize1(M,isF,F);
    3.47 +lemma (in M_trancl) iterates_closed [intro,simp]:
    3.48 +  "[| iterates_replacement(M,isF,v); relation1(M,isF,F);
    3.49        n \<in> nat; M(v); \<forall>x[M]. M(F(x)) |] 
    3.50     ==> M(iterates(F,n,v))"
    3.51  apply (frule iterates_imp_wfrec_replacement, assumption+)
    3.52  apply (simp add: wf_Memrel trans_Memrel relation_Memrel nat_into_M
    3.53 -                 relativize2_def iterates_MH_abs 
    3.54 +                 relation2_def iterates_MH_abs 
    3.55                   iterates_nat_def recursor_def transrec_def 
    3.56                   eclose_sing_Ord_eq nat_into_M
    3.57           trans_wfrec_closed [of _ _ _ "\<lambda>n g. nat_case(v, \<lambda>m. F(g`m), n)"])
    3.58 @@ -459,7 +458,7 @@
    3.59    is_formula :: "[i=>o,i] => o"
    3.60      "is_formula(M,Z) == \<forall>p[M]. p \<in> Z <-> mem_formula(M,p)"
    3.61  
    3.62 -locale M_datatypes = M_wfrank +
    3.63 +locale M_datatypes = M_trancl +
    3.64   assumes list_replacement1: 
    3.65     "M(A) ==> iterates_replacement(M, is_list_functor(M,A), 0)"
    3.66    and list_replacement2: 
    3.67 @@ -487,14 +486,14 @@
    3.68  apply (insert list_replacement2 [of A]) 
    3.69  apply (rule strong_replacement_cong [THEN iffD1])  
    3.70  apply (rule conj_cong [OF iff_refl iterates_abs [of "is_list_functor(M,A)"]]) 
    3.71 -apply (simp_all add: list_replacement1 relativize1_def) 
    3.72 +apply (simp_all add: list_replacement1 relation1_def) 
    3.73  done
    3.74  
    3.75  lemma (in M_datatypes) list_closed [intro,simp]:
    3.76       "M(A) ==> M(list(A))"
    3.77  apply (insert list_replacement1)
    3.78  by  (simp add: RepFun_closed2 list_eq_Union 
    3.79 -               list_replacement2' relativize1_def
    3.80 +               list_replacement2' relation1_def
    3.81                 iterates_closed [of "is_list_functor(M,A)"])
    3.82  
    3.83  text{*WARNING: use only with @{text "dest:"} or with variables fixed!*}
    3.84 @@ -504,21 +503,21 @@
    3.85       "[|M(A); n\<in>nat; M(Z)|] 
    3.86        ==> is_list_N(M,A,n,Z) <-> Z = list_N(A,n)"
    3.87  apply (insert list_replacement1)
    3.88 -apply (simp add: is_list_N_def list_N_def relativize1_def nat_into_M
    3.89 +apply (simp add: is_list_N_def list_N_def relation1_def nat_into_M
    3.90                   iterates_abs [of "is_list_functor(M,A)" _ "\<lambda>X. {0} + A*X"])
    3.91  done
    3.92  
    3.93  lemma (in M_datatypes) list_N_closed [intro,simp]:
    3.94       "[|M(A); n\<in>nat|] ==> M(list_N(A,n))"
    3.95  apply (insert list_replacement1)
    3.96 -apply (simp add: is_list_N_def list_N_def relativize1_def nat_into_M
    3.97 +apply (simp add: is_list_N_def list_N_def relation1_def nat_into_M
    3.98                   iterates_closed [of "is_list_functor(M,A)"])
    3.99  done
   3.100  
   3.101  lemma (in M_datatypes) mem_list_abs [simp]:
   3.102       "M(A) ==> mem_list(M,A,l) <-> l \<in> list(A)"
   3.103  apply (insert list_replacement1)
   3.104 -apply (simp add: mem_list_def list_N_def relativize1_def list_eq_Union
   3.105 +apply (simp add: mem_list_def list_N_def relation1_def list_eq_Union
   3.106                   iterates_closed [of "is_list_functor(M,A)"]) 
   3.107  done
   3.108  
   3.109 @@ -535,14 +534,14 @@
   3.110  apply (insert formula_replacement2) 
   3.111  apply (rule strong_replacement_cong [THEN iffD1])  
   3.112  apply (rule conj_cong [OF iff_refl iterates_abs [of "is_formula_functor(M)"]]) 
   3.113 -apply (simp_all add: formula_replacement1 relativize1_def) 
   3.114 +apply (simp_all add: formula_replacement1 relation1_def) 
   3.115  done
   3.116  
   3.117  lemma (in M_datatypes) formula_closed [intro,simp]:
   3.118       "M(formula)"
   3.119  apply (insert formula_replacement1)
   3.120  apply  (simp add: RepFun_closed2 formula_eq_Union 
   3.121 -                  formula_replacement2' relativize1_def
   3.122 +                  formula_replacement2' relation1_def
   3.123                    iterates_closed [of "is_formula_functor(M)"])
   3.124  done
   3.125  
   3.126 @@ -552,7 +551,7 @@
   3.127       "[|n\<in>nat; M(Z)|] 
   3.128        ==> is_formula_N(M,n,Z) <-> Z = formula_N(n)"
   3.129  apply (insert formula_replacement1)
   3.130 -apply (simp add: is_formula_N_def formula_N_def relativize1_def nat_into_M
   3.131 +apply (simp add: is_formula_N_def formula_N_def relation1_def nat_into_M
   3.132                   iterates_abs [of "is_formula_functor(M)" _ 
   3.133                                    "\<lambda>X. ((nat*nat) + (nat*nat)) + (X*X + X)"])
   3.134  done
   3.135 @@ -560,14 +559,14 @@
   3.136  lemma (in M_datatypes) formula_N_closed [intro,simp]:
   3.137       "n\<in>nat ==> M(formula_N(n))"
   3.138  apply (insert formula_replacement1)
   3.139 -apply (simp add: is_formula_N_def formula_N_def relativize1_def nat_into_M
   3.140 +apply (simp add: is_formula_N_def formula_N_def relation1_def nat_into_M
   3.141                   iterates_closed [of "is_formula_functor(M)"])
   3.142  done
   3.143  
   3.144  lemma (in M_datatypes) mem_formula_abs [simp]:
   3.145       "mem_formula(M,l) <-> l \<in> formula"
   3.146  apply (insert formula_replacement1)
   3.147 -apply (simp add: mem_formula_def relativize1_def formula_eq_Union formula_N_def
   3.148 +apply (simp add: mem_formula_def relation1_def formula_eq_Union formula_N_def
   3.149                   iterates_closed [of "is_formula_functor(M)"]) 
   3.150  done
   3.151  
   3.152 @@ -624,27 +623,27 @@
   3.153  apply (insert eclose_replacement2 [of A]) 
   3.154  apply (rule strong_replacement_cong [THEN iffD1])  
   3.155  apply (rule conj_cong [OF iff_refl iterates_abs [of "big_union(M)"]]) 
   3.156 -apply (simp_all add: eclose_replacement1 relativize1_def) 
   3.157 +apply (simp_all add: eclose_replacement1 relation1_def) 
   3.158  done
   3.159  
   3.160  lemma (in M_eclose) eclose_closed [intro,simp]:
   3.161       "M(A) ==> M(eclose(A))"
   3.162  apply (insert eclose_replacement1)
   3.163  by  (simp add: RepFun_closed2 eclose_eq_Union 
   3.164 -               eclose_replacement2' relativize1_def
   3.165 +               eclose_replacement2' relation1_def
   3.166                 iterates_closed [of "big_union(M)"])
   3.167  
   3.168  lemma (in M_eclose) is_eclose_n_abs [simp]:
   3.169       "[|M(A); n\<in>nat; M(Z)|] ==> is_eclose_n(M,A,n,Z) <-> Z = Union^n (A)"
   3.170  apply (insert eclose_replacement1)
   3.171 -apply (simp add: is_eclose_n_def relativize1_def nat_into_M
   3.172 +apply (simp add: is_eclose_n_def relation1_def nat_into_M
   3.173                   iterates_abs [of "big_union(M)" _ "Union"])
   3.174  done
   3.175  
   3.176  lemma (in M_eclose) mem_eclose_abs [simp]:
   3.177       "M(A) ==> mem_eclose(M,A,l) <-> l \<in> eclose(A)"
   3.178  apply (insert eclose_replacement1)
   3.179 -apply (simp add: mem_eclose_def relativize1_def eclose_eq_Union
   3.180 +apply (simp add: mem_eclose_def relation1_def eclose_eq_Union
   3.181                   iterates_closed [of "big_union(M)"]) 
   3.182  done
   3.183  
   3.184 @@ -679,7 +678,7 @@
   3.185    @{text "trans_wfrec_abs"} rather than @{text "trans_wfrec_abs"},
   3.186    which I haven't even proved yet. *}
   3.187  theorem (in M_eclose) transrec_abs:
   3.188 -  "[|transrec_replacement(M,MH,i);  relativize2(M,MH,H);
   3.189 +  "[|transrec_replacement(M,MH,i);  relation2(M,MH,H);
   3.190       Ord(i);  M(i);  M(z);
   3.191       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
   3.192     ==> is_transrec(M,MH,i,z) <-> z = transrec(i,H)" 
   3.193 @@ -688,7 +687,7 @@
   3.194  
   3.195  
   3.196  theorem (in M_eclose) transrec_closed:
   3.197 -     "[|transrec_replacement(M,MH,i);  relativize2(M,MH,H);
   3.198 +     "[|transrec_replacement(M,MH,i);  relation2(M,MH,H);
   3.199  	Ord(i);  M(i);  
   3.200  	\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
   3.201        ==> M(transrec(i,H))"
   3.202 @@ -770,7 +769,7 @@
   3.203   prefer 2 apply (blast intro: transM)
   3.204  apply (simp add: is_nth_def nth_eq_hd_iterates_tl nat_into_M
   3.205                   tl'_closed iterates_tl'_closed 
   3.206 -                 iterates_abs [OF _ relativize1_tl] nth_replacement)
   3.207 +                 iterates_abs [OF _ relation1_tl] nth_replacement)
   3.208  done
   3.209  
   3.210  
   3.211 @@ -848,14 +847,14 @@
   3.212        (\<forall>x[M]. mem_formula(M,x) --> is_Forall(M,x,p) --> is_d(x,z))"
   3.213  
   3.214  lemma (in M_datatypes) formula_case_abs [simp]: 
   3.215 -     "[| Relativize2(M,nat,nat,is_a,a); Relativize2(M,nat,nat,is_b,b); 
   3.216 -         Relativize2(M,formula,formula,is_c,c); Relativize1(M,formula,is_d,d); 
   3.217 +     "[| Relation2(M,nat,nat,is_a,a); Relation2(M,nat,nat,is_b,b); 
   3.218 +         Relation2(M,formula,formula,is_c,c); Relation1(M,formula,is_d,d); 
   3.219           p \<in> formula; M(z) |] 
   3.220        ==> is_formula_case(M,is_a,is_b,is_c,is_d,p,z) <-> 
   3.221            z = formula_case(a,b,c,d,p)"
   3.222  apply (simp add: formula_into_M is_formula_case_def)
   3.223  apply (erule formula.cases) 
   3.224 -   apply (simp_all add: Relativize1_def Relativize2_def) 
   3.225 +   apply (simp_all add: Relation1_def Relation2_def) 
   3.226  done
   3.227  
   3.228  lemma (in M_datatypes) formula_case_closed [intro,simp]:
   3.229 @@ -935,18 +934,18 @@
   3.230  
   3.231  text{*Sufficient conditions to relative the instance of @{term formula_case}
   3.232        in @{term formula_rec}*}
   3.233 -lemma (in M_datatypes) Relativize1_formula_rec_case:
   3.234 -     "[|Relativize2(M, nat, nat, is_a, a);
   3.235 -        Relativize2(M, nat, nat, is_b, b);
   3.236 -        Relativize2 (M, formula, formula, 
   3.237 +lemma (in M_datatypes) Relation1_formula_rec_case:
   3.238 +     "[|Relation2(M, nat, nat, is_a, a);
   3.239 +        Relation2(M, nat, nat, is_b, b);
   3.240 +        Relation2 (M, formula, formula, 
   3.241             is_c, \<lambda>u v. c(u, v, h`succ(depth(u))`u, h`succ(depth(v))`v));
   3.242 -        Relativize1(M, formula, 
   3.243 +        Relation1(M, formula, 
   3.244             is_d, \<lambda>u. d(u, h ` succ(depth(u)) ` u));
   3.245   	M(h) |] 
   3.246 -      ==> Relativize1(M, formula,
   3.247 +      ==> Relation1(M, formula,
   3.248                           is_formula_case (M, is_a, is_b, is_c, is_d),
   3.249                           formula_rec_case(a, b, c, d, h))"
   3.250 -apply (simp (no_asm) add: formula_rec_case_def Relativize1_def) 
   3.251 +apply (simp (no_asm) add: formula_rec_case_def Relation1_def) 
   3.252  apply (simp add: formula_case_abs) 
   3.253  done
   3.254  
   3.255 @@ -963,19 +962,19 @@
   3.256  	 (M, fml, is_formula_case (M, is_a, is_b, is_c(f), is_d(f)), z)"
   3.257  
   3.258    assumes a_closed: "[|x\<in>nat; y\<in>nat|] ==> M(a(x,y))"
   3.259 -      and a_rel:    "Relativize2(M, nat, nat, is_a, a)"
   3.260 +      and a_rel:    "Relation2(M, nat, nat, is_a, a)"
   3.261        and b_closed: "[|x\<in>nat; y\<in>nat|] ==> M(b(x,y))"
   3.262 -      and b_rel:    "Relativize2(M, nat, nat, is_b, b)"
   3.263 +      and b_rel:    "Relation2(M, nat, nat, is_b, b)"
   3.264        and c_closed: "[|x \<in> formula; y \<in> formula; M(gx); M(gy)|]
   3.265                       ==> M(c(x, y, gx, gy))"
   3.266        and c_rel:
   3.267           "M(f) ==> 
   3.268 -          Relativize2 (M, formula, formula, is_c(f),
   3.269 +          Relation2 (M, formula, formula, is_c(f),
   3.270               \<lambda>u v. c(u, v, f ` succ(depth(u)) ` u, f ` succ(depth(v)) ` v))"
   3.271        and d_closed: "[|x \<in> formula; M(gx)|] ==> M(d(x, gx))"
   3.272        and d_rel:
   3.273           "M(f) ==> 
   3.274 -          Relativize1(M, formula, is_d(f), \<lambda>u. d(u, f ` succ(depth(u)) ` u))"
   3.275 +          Relation1(M, formula, is_d(f), \<lambda>u. d(u, f ` succ(depth(u)) ` u))"
   3.276        and fr_replace: "n \<in> nat ==> transrec_replacement(M,MH,n)"
   3.277        and fr_lam_replace:
   3.278             "M(g) ==>
   3.279 @@ -992,12 +991,12 @@
   3.280  by (simp add: lam_closed2 fr_lam_replace formula_rec_case_closed)
   3.281  
   3.282  lemma (in Formula_Rec) MH_rel2:
   3.283 -     "relativize2 (M, MH,
   3.284 +     "relation2 (M, MH,
   3.285               \<lambda>x h. Lambda (formula, formula_rec_case(a,b,c,d,h)))"
   3.286 -apply (simp add: relativize2_def MH_def, clarify) 
   3.287 +apply (simp add: relation2_def MH_def, clarify) 
   3.288  apply (rule lambda_abs2) 
   3.289  apply (rule fr_lam_replace, assumption)
   3.290 -apply (rule Relativize1_formula_rec_case)  
   3.291 +apply (rule Relation1_formula_rec_case)  
   3.292  apply (simp_all add: a_rel b_rel c_rel d_rel formula_rec_case_closed) 
   3.293  done
   3.294  
     4.1 --- a/src/ZF/Constructible/Formula.thy	Tue Oct 08 14:09:18 2002 +0200
     4.2 +++ b/src/ZF/Constructible/Formula.thy	Wed Oct 09 11:07:13 2002 +0200
     4.3 @@ -1,7 +1,6 @@
     4.4  (*  Title:      ZF/Constructible/Formula.thy
     4.5      ID: $Id$
     4.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7 -    Copyright   2002  University of Cambridge
     4.8  *)
     4.9  
    4.10  header {* First-Order Formulas and the Definition of the Class L *}
     5.1 --- a/src/ZF/Constructible/Internalize.thy	Tue Oct 08 14:09:18 2002 +0200
     5.2 +++ b/src/ZF/Constructible/Internalize.thy	Wed Oct 09 11:07:13 2002 +0200
     5.3 @@ -1,7 +1,6 @@
     5.4  (*  Title:      ZF/Constructible/Internalize.thy
     5.5      ID: $Id$
     5.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7 -    Copyright   2002  University of Cambridge
     5.8  *)
     5.9  
    5.10  theory Internalize = L_axioms + Datatype_absolute:
     6.1 --- a/src/ZF/Constructible/L_axioms.thy	Tue Oct 08 14:09:18 2002 +0200
     6.2 +++ b/src/ZF/Constructible/L_axioms.thy	Wed Oct 09 11:07:13 2002 +0200
     6.3 @@ -1,7 +1,6 @@
     6.4  (*  Title:      ZF/Constructible/L_axioms.thy
     6.5      ID:         $Id$
     6.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.7 -    Copyright   2002  University of Cambridge
     6.8  *)
     6.9  
    6.10  header {* The ZF Axioms (Except Separation) in L *}
     7.1 --- a/src/ZF/Constructible/MetaExists.thy	Tue Oct 08 14:09:18 2002 +0200
     7.2 +++ b/src/ZF/Constructible/MetaExists.thy	Wed Oct 09 11:07:13 2002 +0200
     7.3 @@ -1,7 +1,6 @@
     7.4  (*  Title:      ZF/Constructible/MetaExists.thy
     7.5      ID:         $Id$
     7.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.7 -    Copyright   2002  University of Cambridge
     7.8  *)
     7.9  
    7.10  header{*The meta-existential quantifier*}
     8.1 --- a/src/ZF/Constructible/Normal.thy	Tue Oct 08 14:09:18 2002 +0200
     8.2 +++ b/src/ZF/Constructible/Normal.thy	Wed Oct 09 11:07:13 2002 +0200
     8.3 @@ -1,7 +1,6 @@
     8.4  (*  Title:      ZF/Constructible/Normal.thy
     8.5      ID:         $Id$
     8.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.7 -    Copyright   2002  University of Cambridge
     8.8  *)
     8.9  
    8.10  header {*Closed Unbounded Classes and Normal Functions*}
     9.1 --- a/src/ZF/Constructible/ROOT.ML	Tue Oct 08 14:09:18 2002 +0200
     9.2 +++ b/src/ZF/Constructible/ROOT.ML	Wed Oct 09 11:07:13 2002 +0200
     9.3 @@ -8,3 +8,4 @@
     9.4  
     9.5  use_thy "DPow_absolute";
     9.6  use_thy "AC_in_L";
     9.7 +use_thy "Rank_Separation";
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/ZF/Constructible/Rank.thy	Wed Oct 09 11:07:13 2002 +0200
    10.3 @@ -0,0 +1,935 @@
    10.4 +(*  Title:      ZF/Constructible/Rank.thy
    10.5 +    ID:   $Id$
    10.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    10.7 +*)
    10.8 +
    10.9 +header {*Absoluteness for Order Types, Rank Functions and Well-Founded 
   10.10 +         Relations*}
   10.11 +
   10.12 +theory Rank = WF_absolute:
   10.13 +
   10.14 +subsection {*Order Types: A Direct Construction by Replacement*}
   10.15 +
   10.16 +locale M_ordertype = M_basic +
   10.17 +assumes well_ord_iso_separation:
   10.18 +     "[| M(A); M(f); M(r) |]
   10.19 +      ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y[M]. (\<exists>p[M].
   10.20 +		     fun_apply(M,f,x,y) & pair(M,y,x,p) & p \<in> r)))"
   10.21 +  and obase_separation:
   10.22 +     --{*part of the order type formalization*}
   10.23 +     "[| M(A); M(r) |]
   10.24 +      ==> separation(M, \<lambda>a. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M].
   10.25 +	     ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
   10.26 +	     order_isomorphism(M,par,r,x,mx,g))"
   10.27 +  and obase_equals_separation:
   10.28 +     "[| M(A); M(r) |]
   10.29 +      ==> separation (M, \<lambda>x. x\<in>A --> ~(\<exists>y[M]. \<exists>g[M].
   10.30 +			      ordinal(M,y) & (\<exists>my[M]. \<exists>pxr[M].
   10.31 +			      membership(M,y,my) & pred_set(M,A,x,r,pxr) &
   10.32 +			      order_isomorphism(M,pxr,r,y,my,g))))"
   10.33 +  and omap_replacement:
   10.34 +     "[| M(A); M(r) |]
   10.35 +      ==> strong_replacement(M,
   10.36 +             \<lambda>a z. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M].
   10.37 +	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) &
   10.38 +	     pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
   10.39 +
   10.40 +
   10.41 +text{*Inductive argument for Kunen's Lemma I 6.1, etc.
   10.42 +      Simple proof from Halmos, page 72*}
   10.43 +lemma  (in M_ordertype) wellordered_iso_subset_lemma: 
   10.44 +     "[| wellordered(M,A,r);  f \<in> ord_iso(A,r, A',r);  A'<= A;  y \<in> A;  
   10.45 +       M(A);  M(f);  M(r) |] ==> ~ <f`y, y> \<in> r"
   10.46 +apply (unfold wellordered_def ord_iso_def)
   10.47 +apply (elim conjE CollectE) 
   10.48 +apply (erule wellfounded_on_induct, assumption+)
   10.49 + apply (insert well_ord_iso_separation [of A f r])
   10.50 + apply (simp, clarify) 
   10.51 +apply (drule_tac a = x in bij_is_fun [THEN apply_type], assumption, blast)
   10.52 +done
   10.53 +
   10.54 +
   10.55 +text{*Kunen's Lemma I 6.1, page 14: 
   10.56 +      there's no order-isomorphism to an initial segment of a well-ordering*}
   10.57 +lemma (in M_ordertype) wellordered_iso_predD:
   10.58 +     "[| wellordered(M,A,r);  f \<in> ord_iso(A, r, Order.pred(A,x,r), r);  
   10.59 +       M(A);  M(f);  M(r) |] ==> x \<notin> A"
   10.60 +apply (rule notI) 
   10.61 +apply (frule wellordered_iso_subset_lemma, assumption)
   10.62 +apply (auto elim: predE)  
   10.63 +(*Now we know  ~ (f`x < x) *)
   10.64 +apply (drule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption)
   10.65 +(*Now we also know f`x  \<in> pred(A,x,r);  contradiction! *)
   10.66 +apply (simp add: Order.pred_def)
   10.67 +done
   10.68 +
   10.69 +
   10.70 +lemma (in M_ordertype) wellordered_iso_pred_eq_lemma:
   10.71 +     "[| f \<in> \<langle>Order.pred(A,y,r), r\<rangle> \<cong> \<langle>Order.pred(A,x,r), r\<rangle>;
   10.72 +       wellordered(M,A,r); x\<in>A; y\<in>A; M(A); M(f); M(r) |] ==> <x,y> \<notin> r"
   10.73 +apply (frule wellordered_is_trans_on, assumption)
   10.74 +apply (rule notI) 
   10.75 +apply (drule_tac x2=y and x=x and r2=r in 
   10.76 +         wellordered_subset [OF _ pred_subset, THEN wellordered_iso_predD]) 
   10.77 +apply (simp add: trans_pred_pred_eq) 
   10.78 +apply (blast intro: predI dest: transM)+
   10.79 +done
   10.80 +
   10.81 +
   10.82 +text{*Simple consequence of Lemma 6.1*}
   10.83 +lemma (in M_ordertype) wellordered_iso_pred_eq:
   10.84 +     "[| wellordered(M,A,r);
   10.85 +       f \<in> ord_iso(Order.pred(A,a,r), r, Order.pred(A,c,r), r);   
   10.86 +       M(A);  M(f);  M(r);  a\<in>A;  c\<in>A |] ==> a=c"
   10.87 +apply (frule wellordered_is_trans_on, assumption)
   10.88 +apply (frule wellordered_is_linear, assumption)
   10.89 +apply (erule_tac x=a and y=c in linearE, auto) 
   10.90 +apply (drule ord_iso_sym)
   10.91 +(*two symmetric cases*)
   10.92 +apply (blast dest: wellordered_iso_pred_eq_lemma)+ 
   10.93 +done
   10.94 +
   10.95 +
   10.96 +text{*Following Kunen's Theorem I 7.6, page 17.  Note that this material is
   10.97 +not required elsewhere.*}
   10.98 +
   10.99 +text{*Can't use @{text well_ord_iso_preserving} because it needs the
  10.100 +strong premise @{term "well_ord(A,r)"}*}
  10.101 +lemma (in M_ordertype) ord_iso_pred_imp_lt:
  10.102 +     "[| f \<in> ord_iso(Order.pred(A,x,r), r, i, Memrel(i));
  10.103 +         g \<in> ord_iso(Order.pred(A,y,r), r, j, Memrel(j));
  10.104 +         wellordered(M,A,r);  x \<in> A;  y \<in> A; M(A); M(r); M(f); M(g); M(j);
  10.105 +         Ord(i); Ord(j); \<langle>x,y\<rangle> \<in> r |]
  10.106 +      ==> i < j"
  10.107 +apply (frule wellordered_is_trans_on, assumption)
  10.108 +apply (frule_tac y=y in transM, assumption) 
  10.109 +apply (rule_tac i=i and j=j in Ord_linear_lt, auto)  
  10.110 +txt{*case @{term "i=j"} yields a contradiction*}
  10.111 + apply (rule_tac x1=x and A1="Order.pred(A,y,r)" in 
  10.112 +          wellordered_iso_predD [THEN notE]) 
  10.113 +   apply (blast intro: wellordered_subset [OF _ pred_subset]) 
  10.114 +  apply (simp add: trans_pred_pred_eq)
  10.115 +  apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans) 
  10.116 + apply (simp_all add: pred_iff pred_closed converse_closed comp_closed)
  10.117 +txt{*case @{term "j<i"} also yields a contradiction*}
  10.118 +apply (frule restrict_ord_iso2, assumption+) 
  10.119 +apply (frule ord_iso_sym [THEN ord_iso_is_bij, THEN bij_is_fun]) 
  10.120 +apply (frule apply_type, blast intro: ltD) 
  10.121 +  --{*thus @{term "converse(f)`j \<in> Order.pred(A,x,r)"}*}
  10.122 +apply (simp add: pred_iff) 
  10.123 +apply (subgoal_tac
  10.124 +       "\<exists>h[M]. h \<in> ord_iso(Order.pred(A,y,r), r, 
  10.125 +                               Order.pred(A, converse(f)`j, r), r)")
  10.126 + apply (clarify, frule wellordered_iso_pred_eq, assumption+)
  10.127 + apply (blast dest: wellordered_asym)  
  10.128 +apply (intro rexI)
  10.129 + apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans)+
  10.130 +done
  10.131 +
  10.132 +
  10.133 +lemma ord_iso_converse1:
  10.134 +     "[| f: ord_iso(A,r,B,s);  <b, f`a>: s;  a:A;  b:B |] 
  10.135 +      ==> <converse(f) ` b, a> : r"
  10.136 +apply (frule ord_iso_converse, assumption+) 
  10.137 +apply (blast intro: ord_iso_is_bij [THEN bij_is_fun, THEN apply_funtype]) 
  10.138 +apply (simp add: left_inverse_bij [OF ord_iso_is_bij])
  10.139 +done
  10.140 +
  10.141 +
  10.142 +constdefs
  10.143 +  
  10.144 +  obase :: "[i=>o,i,i] => i"
  10.145 +       --{*the domain of @{text om}, eventually shown to equal @{text A}*}
  10.146 +   "obase(M,A,r) == {a\<in>A. \<exists>x[M]. \<exists>g[M]. Ord(x) & 
  10.147 +                          g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x))}"
  10.148 +
  10.149 +  omap :: "[i=>o,i,i,i] => o"  
  10.150 +    --{*the function that maps wosets to order types*}
  10.151 +   "omap(M,A,r,f) == 
  10.152 +	\<forall>z[M].
  10.153 +         z \<in> f <-> (\<exists>a\<in>A. \<exists>x[M]. \<exists>g[M]. z = <a,x> & Ord(x) & 
  10.154 +                        g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))"
  10.155 +
  10.156 +
  10.157 +  otype :: "[i=>o,i,i,i] => o"  --{*the order types themselves*}
  10.158 +   "otype(M,A,r,i) == \<exists>f[M]. omap(M,A,r,f) & is_range(M,f,i)"
  10.159 +
  10.160 +
  10.161 +text{*Can also be proved with the premise @{term "M(z)"} instead of
  10.162 +      @{term "M(f)"}, but that version is less useful.  This lemma
  10.163 +      is also more useful than the definition, @{text omap_def}.*}
  10.164 +lemma (in M_ordertype) omap_iff:
  10.165 +     "[| omap(M,A,r,f); M(A); M(f) |] 
  10.166 +      ==> z \<in> f <->
  10.167 +          (\<exists>a\<in>A. \<exists>x[M]. \<exists>g[M]. z = <a,x> & Ord(x) & 
  10.168 +                                g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))"
  10.169 +apply (simp add: omap_def Memrel_closed pred_closed) 
  10.170 +apply (rule iffI)
  10.171 + apply (drule_tac [2] x=z in rspec)
  10.172 + apply (drule_tac x=z in rspec)
  10.173 + apply (blast dest: transM)+
  10.174 +done
  10.175 +
  10.176 +lemma (in M_ordertype) omap_unique:
  10.177 +     "[| omap(M,A,r,f); omap(M,A,r,f'); M(A); M(r); M(f); M(f') |] ==> f' = f" 
  10.178 +apply (rule equality_iffI) 
  10.179 +apply (simp add: omap_iff) 
  10.180 +done
  10.181 +
  10.182 +lemma (in M_ordertype) omap_yields_Ord:
  10.183 +     "[| omap(M,A,r,f); \<langle>a,x\<rangle> \<in> f; M(a); M(x) |]  ==> Ord(x)"
  10.184 +  by (simp add: omap_def)
  10.185 +
  10.186 +lemma (in M_ordertype) otype_iff:
  10.187 +     "[| otype(M,A,r,i); M(A); M(r); M(i) |] 
  10.188 +      ==> x \<in> i <-> 
  10.189 +          (M(x) & Ord(x) & 
  10.190 +           (\<exists>a\<in>A. \<exists>g[M]. g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x))))"
  10.191 +apply (auto simp add: omap_iff otype_def)
  10.192 + apply (blast intro: transM) 
  10.193 +apply (rule rangeI) 
  10.194 +apply (frule transM, assumption)
  10.195 +apply (simp add: omap_iff, blast)
  10.196 +done
  10.197 +
  10.198 +lemma (in M_ordertype) otype_eq_range:
  10.199 +     "[| omap(M,A,r,f); otype(M,A,r,i); M(A); M(r); M(f); M(i) |] 
  10.200 +      ==> i = range(f)"
  10.201 +apply (auto simp add: otype_def omap_iff)
  10.202 +apply (blast dest: omap_unique) 
  10.203 +done
  10.204 +
  10.205 +
  10.206 +lemma (in M_ordertype) Ord_otype:
  10.207 +     "[| otype(M,A,r,i); trans[A](r); M(A); M(r); M(i) |] ==> Ord(i)"
  10.208 +apply (rule OrdI) 
  10.209 +prefer 2 
  10.210 +    apply (simp add: Ord_def otype_def omap_def) 
  10.211 +    apply clarify 
  10.212 +    apply (frule pair_components_in_M, assumption) 
  10.213 +    apply blast 
  10.214 +apply (auto simp add: Transset_def otype_iff) 
  10.215 +  apply (blast intro: transM)
  10.216 + apply (blast intro: Ord_in_Ord) 
  10.217 +apply (rename_tac y a g)
  10.218 +apply (frule ord_iso_sym [THEN ord_iso_is_bij, THEN bij_is_fun, 
  10.219 +			  THEN apply_funtype],  assumption)  
  10.220 +apply (rule_tac x="converse(g)`y" in bexI)
  10.221 + apply (frule_tac a="converse(g) ` y" in ord_iso_restrict_pred, assumption) 
  10.222 +apply (safe elim!: predE) 
  10.223 +apply (blast intro: restrict_ord_iso ord_iso_sym ltI dest: transM)
  10.224 +done
  10.225 +
  10.226 +lemma (in M_ordertype) domain_omap:
  10.227 +     "[| omap(M,A,r,f);  M(A); M(r); M(B); M(f) |] 
  10.228 +      ==> domain(f) = obase(M,A,r)"
  10.229 +apply (simp add: domain_closed obase_def) 
  10.230 +apply (rule equality_iffI) 
  10.231 +apply (simp add: domain_iff omap_iff, blast) 
  10.232 +done
  10.233 +
  10.234 +lemma (in M_ordertype) omap_subset: 
  10.235 +     "[| omap(M,A,r,f); otype(M,A,r,i); 
  10.236 +       M(A); M(r); M(f); M(B); M(i) |] ==> f \<subseteq> obase(M,A,r) * i"
  10.237 +apply clarify 
  10.238 +apply (simp add: omap_iff obase_def) 
  10.239 +apply (force simp add: otype_iff) 
  10.240 +done
  10.241 +
  10.242 +lemma (in M_ordertype) omap_funtype: 
  10.243 +     "[| omap(M,A,r,f); otype(M,A,r,i); 
  10.244 +         M(A); M(r); M(f); M(i) |] ==> f \<in> obase(M,A,r) -> i"
  10.245 +apply (simp add: domain_omap omap_subset Pi_iff function_def omap_iff) 
  10.246 +apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans) 
  10.247 +done
  10.248 +
  10.249 +
  10.250 +lemma (in M_ordertype) wellordered_omap_bij:
  10.251 +     "[| wellordered(M,A,r); omap(M,A,r,f); otype(M,A,r,i); 
  10.252 +       M(A); M(r); M(f); M(i) |] ==> f \<in> bij(obase(M,A,r),i)"
  10.253 +apply (insert omap_funtype [of A r f i]) 
  10.254 +apply (auto simp add: bij_def inj_def) 
  10.255 +prefer 2  apply (blast intro: fun_is_surj dest: otype_eq_range) 
  10.256 +apply (frule_tac a=w in apply_Pair, assumption) 
  10.257 +apply (frule_tac a=x in apply_Pair, assumption) 
  10.258 +apply (simp add: omap_iff) 
  10.259 +apply (blast intro: wellordered_iso_pred_eq ord_iso_sym ord_iso_trans) 
  10.260 +done
  10.261 +
  10.262 +
  10.263 +text{*This is not the final result: we must show @{term "oB(A,r) = A"}*}
  10.264 +lemma (in M_ordertype) omap_ord_iso:
  10.265 +     "[| wellordered(M,A,r); omap(M,A,r,f); otype(M,A,r,i); 
  10.266 +       M(A); M(r); M(f); M(i) |] ==> f \<in> ord_iso(obase(M,A,r),r,i,Memrel(i))"
  10.267 +apply (rule ord_isoI)
  10.268 + apply (erule wellordered_omap_bij, assumption+) 
  10.269 +apply (insert omap_funtype [of A r f i], simp) 
  10.270 +apply (frule_tac a=x in apply_Pair, assumption) 
  10.271 +apply (frule_tac a=y in apply_Pair, assumption) 
  10.272 +apply (auto simp add: omap_iff)
  10.273 + txt{*direction 1: assuming @{term "\<langle>x,y\<rangle> \<in> r"}*}
  10.274 + apply (blast intro: ltD ord_iso_pred_imp_lt)
  10.275 + txt{*direction 2: proving @{term "\<langle>x,y\<rangle> \<in> r"} using linearity of @{term r}*}
  10.276 +apply (rename_tac x y g ga) 
  10.277 +apply (frule wellordered_is_linear, assumption, 
  10.278 +       erule_tac x=x and y=y in linearE, assumption+) 
  10.279 +txt{*the case @{term "x=y"} leads to immediate contradiction*} 
  10.280 +apply (blast elim: mem_irrefl) 
  10.281 +txt{*the case @{term "\<langle>y,x\<rangle> \<in> r"}: handle like the opposite direction*}
  10.282 +apply (blast dest: ord_iso_pred_imp_lt ltD elim: mem_asym) 
  10.283 +done
  10.284 +
  10.285 +lemma (in M_ordertype) Ord_omap_image_pred:
  10.286 +     "[| wellordered(M,A,r); omap(M,A,r,f); otype(M,A,r,i); 
  10.287 +       M(A); M(r); M(f); M(i); b \<in> A |] ==> Ord(f `` Order.pred(A,b,r))"
  10.288 +apply (frule wellordered_is_trans_on, assumption)
  10.289 +apply (rule OrdI) 
  10.290 +	prefer 2 apply (simp add: image_iff omap_iff Ord_def, blast) 
  10.291 +txt{*Hard part is to show that the image is a transitive set.*}
  10.292 +apply (simp add: Transset_def, clarify) 
  10.293 +apply (simp add: image_iff pred_iff apply_iff [OF omap_funtype [of A r f i]])
  10.294 +apply (rename_tac c j, clarify)
  10.295 +apply (frule omap_funtype [of A r f, THEN apply_funtype], assumption+)
  10.296 +apply (subgoal_tac "j : i") 
  10.297 +	prefer 2 apply (blast intro: Ord_trans Ord_otype)
  10.298 +apply (subgoal_tac "converse(f) ` j : obase(M,A,r)") 
  10.299 +	prefer 2 
  10.300 +	apply (blast dest: wellordered_omap_bij [THEN bij_converse_bij, 
  10.301 +                                      THEN bij_is_fun, THEN apply_funtype])
  10.302 +apply (rule_tac x="converse(f) ` j" in bexI) 
  10.303 + apply (simp add: right_inverse_bij [OF wellordered_omap_bij]) 
  10.304 +apply (intro predI conjI)
  10.305 + apply (erule_tac b=c in trans_onD) 
  10.306 + apply (rule ord_iso_converse1 [OF omap_ord_iso [of A r f i]])
  10.307 +apply (auto simp add: obase_def)
  10.308 +done
  10.309 +
  10.310 +lemma (in M_ordertype) restrict_omap_ord_iso:
  10.311 +     "[| wellordered(M,A,r); omap(M,A,r,f); otype(M,A,r,i); 
  10.312 +       D \<subseteq> obase(M,A,r); M(A); M(r); M(f); M(i) |] 
  10.313 +      ==> restrict(f,D) \<in> (\<langle>D,r\<rangle> \<cong> \<langle>f``D, Memrel(f``D)\<rangle>)"
  10.314 +apply (frule ord_iso_restrict_image [OF omap_ord_iso [of A r f i]], 
  10.315 +       assumption+)
  10.316 +apply (drule ord_iso_sym [THEN subset_ord_iso_Memrel]) 
  10.317 +apply (blast dest: subsetD [OF omap_subset]) 
  10.318 +apply (drule ord_iso_sym, simp) 
  10.319 +done
  10.320 +
  10.321 +lemma (in M_ordertype) obase_equals: 
  10.322 +     "[| wellordered(M,A,r); omap(M,A,r,f); otype(M,A,r,i);
  10.323 +       M(A); M(r); M(f); M(i) |] ==> obase(M,A,r) = A"
  10.324 +apply (rule equalityI, force simp add: obase_def, clarify) 
  10.325 +apply (unfold obase_def, simp) 
  10.326 +apply (frule wellordered_is_wellfounded_on, assumption)
  10.327 +apply (erule wellfounded_on_induct, assumption+)
  10.328 + apply (frule obase_equals_separation [of A r], assumption) 
  10.329 + apply (simp, clarify) 
  10.330 +apply (rename_tac b) 
  10.331 +apply (subgoal_tac "Order.pred(A,b,r) <= obase(M,A,r)") 
  10.332 + apply (blast intro!: restrict_omap_ord_iso Ord_omap_image_pred)
  10.333 +apply (force simp add: pred_iff obase_def)  
  10.334 +done
  10.335 +
  10.336 +
  10.337 +
  10.338 +text{*Main result: @{term om} gives the order-isomorphism 
  10.339 +      @{term "\<langle>A,r\<rangle> \<cong> \<langle>i, Memrel(i)\<rangle>"} *}
  10.340 +theorem (in M_ordertype) omap_ord_iso_otype:
  10.341 +     "[| wellordered(M,A,r); omap(M,A,r,f); otype(M,A,r,i);
  10.342 +       M(A); M(r); M(f); M(i) |] ==> f \<in> ord_iso(A, r, i, Memrel(i))"
  10.343 +apply (frule omap_ord_iso, assumption+)
  10.344 +apply (simp add: obase_equals)  
  10.345 +done 
  10.346 +
  10.347 +lemma (in M_ordertype) obase_exists:
  10.348 +     "[| M(A); M(r) |] ==> M(obase(M,A,r))"
  10.349 +apply (simp add: obase_def) 
  10.350 +apply (insert obase_separation [of A r])
  10.351 +apply (simp add: separation_def)  
  10.352 +done
  10.353 +
  10.354 +lemma (in M_ordertype) omap_exists:
  10.355 +     "[| M(A); M(r) |] ==> \<exists>z[M]. omap(M,A,r,z)"
  10.356 +apply (simp add: omap_def) 
  10.357 +apply (insert omap_replacement [of A r])
  10.358 +apply (simp add: strong_replacement_def) 
  10.359 +apply (drule_tac x="obase(M,A,r)" in rspec) 
  10.360 + apply (simp add: obase_exists) 
  10.361 +apply (simp add: Memrel_closed pred_closed obase_def)
  10.362 +apply (erule impE) 
  10.363 + apply (clarsimp simp add: univalent_def)
  10.364 + apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans, clarify)  
  10.365 +apply (rule_tac x=Y in rexI) 
  10.366 +apply (simp add: Memrel_closed pred_closed obase_def, blast, assumption)
  10.367 +done
  10.368 +
  10.369 +declare rall_simps [simp] rex_simps [simp]
  10.370 +
  10.371 +lemma (in M_ordertype) otype_exists:
  10.372 +     "[| wellordered(M,A,r); M(A); M(r) |] ==> \<exists>i[M]. otype(M,A,r,i)"
  10.373 +apply (insert omap_exists [of A r])  
  10.374 +apply (simp add: otype_def, safe)
  10.375 +apply (rule_tac x="range(x)" in rexI) 
  10.376 +apply blast+
  10.377 +done
  10.378 +
  10.379 +lemma (in M_ordertype) ordertype_exists:
  10.380 +     "[| wellordered(M,A,r); M(A); M(r) |]
  10.381 +      ==> \<exists>f[M]. (\<exists>i[M]. Ord(i) & f \<in> ord_iso(A, r, i, Memrel(i)))"
  10.382 +apply (insert obase_exists [of A r] omap_exists [of A r] otype_exists [of A r], simp, clarify)
  10.383 +apply (rename_tac i) 
  10.384 +apply (subgoal_tac "Ord(i)", blast intro: omap_ord_iso_otype)
  10.385 +apply (rule Ord_otype) 
  10.386 +    apply (force simp add: otype_def range_closed) 
  10.387 +   apply (simp_all add: wellordered_is_trans_on) 
  10.388 +done
  10.389 +
  10.390 +
  10.391 +lemma (in M_ordertype) relativized_imp_well_ord: 
  10.392 +     "[| wellordered(M,A,r); M(A); M(r) |] ==> well_ord(A,r)" 
  10.393 +apply (insert ordertype_exists [of A r], simp)
  10.394 +apply (blast intro: well_ord_ord_iso well_ord_Memrel)  
  10.395 +done
  10.396 +
  10.397 +subsection {*Kunen's theorem 5.4, page 127*}
  10.398 +
  10.399 +text{*(a) The notion of Wellordering is absolute*}
  10.400 +theorem (in M_ordertype) well_ord_abs [simp]: 
  10.401 +     "[| M(A); M(r) |] ==> wellordered(M,A,r) <-> well_ord(A,r)" 
  10.402 +by (blast intro: well_ord_imp_relativized relativized_imp_well_ord)  
  10.403 +
  10.404 +
  10.405 +text{*(b) Order types are absolute*}
  10.406 +theorem (in M_ordertype) 
  10.407 +     "[| wellordered(M,A,r); f \<in> ord_iso(A, r, i, Memrel(i));
  10.408 +       M(A); M(r); M(f); M(i); Ord(i) |] ==> i = ordertype(A,r)"
  10.409 +by (blast intro: Ord_ordertype relativized_imp_well_ord ordertype_ord_iso
  10.410 +                 Ord_iso_implies_eq ord_iso_sym ord_iso_trans)
  10.411 +
  10.412 +
  10.413 +subsection{*Ordinal Arithmetic: Two Examples of Recursion*}
  10.414 +
  10.415 +text{*Note: the remainder of this theory is not needed elsewhere.*}
  10.416 +
  10.417 +subsubsection{*Ordinal Addition*}
  10.418 +
  10.419 +(*FIXME: update to use new techniques!!*)
  10.420 +constdefs
  10.421 + (*This expresses ordinal addition in the language of ZF.  It also 
  10.422 +   provides an abbreviation that can be used in the instance of strong
  10.423 +   replacement below.  Here j is used to define the relation, namely
  10.424 +   Memrel(succ(j)), while x determines the domain of f.*)
  10.425 + is_oadd_fun :: "[i=>o,i,i,i,i] => o"
  10.426 +    "is_oadd_fun(M,i,j,x,f) == 
  10.427 +       (\<forall>sj msj. M(sj) --> M(msj) --> 
  10.428 +                 successor(M,j,sj) --> membership(M,sj,msj) --> 
  10.429 +	         M_is_recfun(M, 
  10.430 +		     %x g y. \<exists>gx[M]. image(M,g,x,gx) & union(M,i,gx,y),
  10.431 +		     msj, x, f))"
  10.432 +
  10.433 + is_oadd :: "[i=>o,i,i,i] => o"
  10.434 +    "is_oadd(M,i,j,k) == 
  10.435 +        (~ ordinal(M,i) & ~ ordinal(M,j) & k=0) |
  10.436 +        (~ ordinal(M,i) & ordinal(M,j) & k=j) |
  10.437 +        (ordinal(M,i) & ~ ordinal(M,j) & k=i) |
  10.438 +        (ordinal(M,i) & ordinal(M,j) & 
  10.439 +	 (\<exists>f fj sj. M(f) & M(fj) & M(sj) & 
  10.440 +		    successor(M,j,sj) & is_oadd_fun(M,i,sj,sj,f) & 
  10.441 +		    fun_apply(M,f,j,fj) & fj = k))"
  10.442 +
  10.443 + (*NEEDS RELATIVIZATION*)
  10.444 + omult_eqns :: "[i,i,i,i] => o"
  10.445 +    "omult_eqns(i,x,g,z) ==
  10.446 +            Ord(x) & 
  10.447 +	    (x=0 --> z=0) &
  10.448 +            (\<forall>j. x = succ(j) --> z = g`j ++ i) &
  10.449 +            (Limit(x) --> z = \<Union>(g``x))"
  10.450 +
  10.451 + is_omult_fun :: "[i=>o,i,i,i] => o"
  10.452 +    "is_omult_fun(M,i,j,f) == 
  10.453 +	    (\<exists>df. M(df) & is_function(M,f) & 
  10.454 +                  is_domain(M,f,df) & subset(M, j, df)) & 
  10.455 +            (\<forall>x\<in>j. omult_eqns(i,x,f,f`x))"
  10.456 +
  10.457 + is_omult :: "[i=>o,i,i,i] => o"
  10.458 +    "is_omult(M,i,j,k) == 
  10.459 +	\<exists>f fj sj. M(f) & M(fj) & M(sj) & 
  10.460 +                  successor(M,j,sj) & is_omult_fun(M,i,sj,f) & 
  10.461 +                  fun_apply(M,f,j,fj) & fj = k"
  10.462 +
  10.463 +
  10.464 +locale M_ord_arith = M_ordertype +
  10.465 +  assumes oadd_strong_replacement:
  10.466 +   "[| M(i); M(j) |] ==>
  10.467 +    strong_replacement(M, 
  10.468 +         \<lambda>x z. \<exists>y[M]. pair(M,x,y,z) & 
  10.469 +                  (\<exists>f[M]. \<exists>fx[M]. is_oadd_fun(M,i,j,x,f) & 
  10.470 +		           image(M,f,x,fx) & y = i Un fx))"
  10.471 +
  10.472 + and omult_strong_replacement':
  10.473 +   "[| M(i); M(j) |] ==>
  10.474 +    strong_replacement(M, 
  10.475 +         \<lambda>x z. \<exists>y[M]. z = <x,y> &
  10.476 +	     (\<exists>g[M]. is_recfun(Memrel(succ(j)),x,%x g. THE z. omult_eqns(i,x,g,z),g) & 
  10.477 +	     y = (THE z. omult_eqns(i, x, g, z))))" 
  10.478 +
  10.479 +
  10.480 +
  10.481 +text{*@{text is_oadd_fun}: Relating the pure "language of set theory" to Isabelle/ZF*}
  10.482 +lemma (in M_ord_arith) is_oadd_fun_iff:
  10.483 +   "[| a\<le>j; M(i); M(j); M(a); M(f) |] 
  10.484 +    ==> is_oadd_fun(M,i,j,a,f) <->
  10.485 +	f \<in> a \<rightarrow> range(f) & (\<forall>x. M(x) --> x < a --> f`x = i Un f``x)"
  10.486 +apply (frule lt_Ord) 
  10.487 +apply (simp add: is_oadd_fun_def Memrel_closed Un_closed 
  10.488 +             relation2_def is_recfun_abs [of "%x g. i Un g``x"]
  10.489 +             image_closed is_recfun_iff_equation  
  10.490 +             Ball_def lt_trans [OF ltI, of _ a] lt_Memrel)
  10.491 +apply (simp add: lt_def) 
  10.492 +apply (blast dest: transM) 
  10.493 +done
  10.494 +
  10.495 +
  10.496 +lemma (in M_ord_arith) oadd_strong_replacement':
  10.497 +    "[| M(i); M(j) |] ==>
  10.498 +     strong_replacement(M, 
  10.499 +            \<lambda>x z. \<exists>y[M]. z = <x,y> &
  10.500 +		  (\<exists>g[M]. is_recfun(Memrel(succ(j)),x,%x g. i Un g``x,g) & 
  10.501 +		  y = i Un g``x))" 
  10.502 +apply (insert oadd_strong_replacement [of i j]) 
  10.503 +apply (simp add: is_oadd_fun_def relation2_def
  10.504 +                 is_recfun_abs [of "%x g. i Un g``x"])  
  10.505 +done
  10.506 +
  10.507 +
  10.508 +lemma (in M_ord_arith) exists_oadd:
  10.509 +    "[| Ord(j);  M(i);  M(j) |]
  10.510 +     ==> \<exists>f[M]. is_recfun(Memrel(succ(j)), j, %x g. i Un g``x, f)"
  10.511 +apply (rule wf_exists_is_recfun [OF wf_Memrel trans_Memrel])
  10.512 +    apply (simp_all add: Memrel_type oadd_strong_replacement') 
  10.513 +done 
  10.514 +
  10.515 +lemma (in M_ord_arith) exists_oadd_fun:
  10.516 +    "[| Ord(j);  M(i);  M(j) |] ==> \<exists>f[M]. is_oadd_fun(M,i,succ(j),succ(j),f)"
  10.517 +apply (rule exists_oadd [THEN rexE])
  10.518 +apply (erule Ord_succ, assumption, simp) 
  10.519 +apply (rename_tac f) 
  10.520 +apply (frule is_recfun_type)
  10.521 +apply (rule_tac x=f in rexI) 
  10.522 + apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def
  10.523 +                  is_oadd_fun_iff Ord_trans [OF _ succI1], assumption)
  10.524 +done
  10.525 +
  10.526 +lemma (in M_ord_arith) is_oadd_fun_apply:
  10.527 +    "[| x < j; M(i); M(j); M(f); is_oadd_fun(M,i,j,j,f) |] 
  10.528 +     ==> f`x = i Un (\<Union>k\<in>x. {f ` k})"
  10.529 +apply (simp add: is_oadd_fun_iff lt_Ord2, clarify) 
  10.530 +apply (frule lt_closed, simp)
  10.531 +apply (frule leI [THEN le_imp_subset])  
  10.532 +apply (simp add: image_fun, blast) 
  10.533 +done
  10.534 +
  10.535 +lemma (in M_ord_arith) is_oadd_fun_iff_oadd [rule_format]:
  10.536 +    "[| is_oadd_fun(M,i,J,J,f); M(i); M(J); M(f); Ord(i); Ord(j) |] 
  10.537 +     ==> j<J --> f`j = i++j"
  10.538 +apply (erule_tac i=j in trans_induct, clarify) 
  10.539 +apply (subgoal_tac "\<forall>k\<in>x. k<J")
  10.540 + apply (simp (no_asm_simp) add: is_oadd_def oadd_unfold is_oadd_fun_apply)
  10.541 +apply (blast intro: lt_trans ltI lt_Ord) 
  10.542 +done
  10.543 +
  10.544 +lemma (in M_ord_arith) Ord_oadd_abs:
  10.545 +    "[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_oadd(M,i,j,k) <-> k = i++j"
  10.546 +apply (simp add: is_oadd_def is_oadd_fun_iff_oadd)
  10.547 +apply (frule exists_oadd_fun [of j i], blast+)
  10.548 +done
  10.549 +
  10.550 +lemma (in M_ord_arith) oadd_abs:
  10.551 +    "[| M(i); M(j); M(k) |] ==> is_oadd(M,i,j,k) <-> k = i++j"
  10.552 +apply (case_tac "Ord(i) & Ord(j)")
  10.553 + apply (simp add: Ord_oadd_abs)
  10.554 +apply (auto simp add: is_oadd_def oadd_eq_if_raw_oadd)
  10.555 +done
  10.556 +
  10.557 +lemma (in M_ord_arith) oadd_closed [intro,simp]:
  10.558 +    "[| M(i); M(j) |] ==> M(i++j)"
  10.559 +apply (simp add: oadd_eq_if_raw_oadd, clarify) 
  10.560 +apply (simp add: raw_oadd_eq_oadd) 
  10.561 +apply (frule exists_oadd_fun [of j i], auto)
  10.562 +apply (simp add: apply_closed is_oadd_fun_iff_oadd [symmetric]) 
  10.563 +done
  10.564 +
  10.565 +
  10.566 +subsubsection{*Ordinal Multiplication*}
  10.567 +
  10.568 +lemma omult_eqns_unique:
  10.569 +     "[| omult_eqns(i,x,g,z); omult_eqns(i,x,g,z') |] ==> z=z'";
  10.570 +apply (simp add: omult_eqns_def, clarify) 
  10.571 +apply (erule Ord_cases, simp_all) 
  10.572 +done
  10.573 +
  10.574 +lemma omult_eqns_0: "omult_eqns(i,0,g,z) <-> z=0"
  10.575 +by (simp add: omult_eqns_def)
  10.576 +
  10.577 +lemma the_omult_eqns_0: "(THE z. omult_eqns(i,0,g,z)) = 0"
  10.578 +by (simp add: omult_eqns_0)
  10.579 +
  10.580 +lemma omult_eqns_succ: "omult_eqns(i,succ(j),g,z) <-> Ord(j) & z = g`j ++ i"
  10.581 +by (simp add: omult_eqns_def)
  10.582 +
  10.583 +lemma the_omult_eqns_succ:
  10.584 +     "Ord(j) ==> (THE z. omult_eqns(i,succ(j),g,z)) = g`j ++ i"
  10.585 +by (simp add: omult_eqns_succ) 
  10.586 +
  10.587 +lemma omult_eqns_Limit:
  10.588 +     "Limit(x) ==> omult_eqns(i,x,g,z) <-> z = \<Union>(g``x)"
  10.589 +apply (simp add: omult_eqns_def) 
  10.590 +apply (blast intro: Limit_is_Ord) 
  10.591 +done
  10.592 +
  10.593 +lemma the_omult_eqns_Limit:
  10.594 +     "Limit(x) ==> (THE z. omult_eqns(i,x,g,z)) = \<Union>(g``x)"
  10.595 +by (simp add: omult_eqns_Limit)
  10.596 +
  10.597 +lemma omult_eqns_Not: "~ Ord(x) ==> ~ omult_eqns(i,x,g,z)"
  10.598 +by (simp add: omult_eqns_def)
  10.599 +
  10.600 +
  10.601 +lemma (in M_ord_arith) the_omult_eqns_closed:
  10.602 +    "[| M(i); M(x); M(g); function(g) |] 
  10.603 +     ==> M(THE z. omult_eqns(i, x, g, z))"
  10.604 +apply (case_tac "Ord(x)")
  10.605 + prefer 2 apply (simp add: omult_eqns_Not) --{*trivial, non-Ord case*}
  10.606 +apply (erule Ord_cases) 
  10.607 +  apply (simp add: omult_eqns_0)
  10.608 + apply (simp add: omult_eqns_succ apply_closed oadd_closed) 
  10.609 +apply (simp add: omult_eqns_Limit) 
  10.610 +done
  10.611 +
  10.612 +lemma (in M_ord_arith) exists_omult:
  10.613 +    "[| Ord(j);  M(i);  M(j) |]
  10.614 +     ==> \<exists>f[M]. is_recfun(Memrel(succ(j)), j, %x g. THE z. omult_eqns(i,x,g,z), f)"
  10.615 +apply (rule wf_exists_is_recfun [OF wf_Memrel trans_Memrel])
  10.616 +    apply (simp_all add: Memrel_type omult_strong_replacement') 
  10.617 +apply (blast intro: the_omult_eqns_closed) 
  10.618 +done
  10.619 +
  10.620 +lemma (in M_ord_arith) exists_omult_fun:
  10.621 +    "[| Ord(j);  M(i);  M(j) |] ==> \<exists>f[M]. is_omult_fun(M,i,succ(j),f)"
  10.622 +apply (rule exists_omult [THEN rexE])
  10.623 +apply (erule Ord_succ, assumption, simp) 
  10.624 +apply (rename_tac f) 
  10.625 +apply (frule is_recfun_type)
  10.626 +apply (rule_tac x=f in rexI) 
  10.627 +apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def
  10.628 +                 is_omult_fun_def Ord_trans [OF _ succI1])
  10.629 + apply (force dest: Ord_in_Ord' 
  10.630 +              simp add: omult_eqns_def the_omult_eqns_0 the_omult_eqns_succ
  10.631 +                        the_omult_eqns_Limit, assumption)
  10.632 +done
  10.633 +
  10.634 +lemma (in M_ord_arith) is_omult_fun_apply_0:
  10.635 +    "[| 0 < j; is_omult_fun(M,i,j,f) |] ==> f`0 = 0"
  10.636 +by (simp add: is_omult_fun_def omult_eqns_def lt_def ball_conj_distrib)
  10.637 +
  10.638 +lemma (in M_ord_arith) is_omult_fun_apply_succ:
  10.639 +    "[| succ(x) < j; is_omult_fun(M,i,j,f) |] ==> f`succ(x) = f`x ++ i"
  10.640 +by (simp add: is_omult_fun_def omult_eqns_def lt_def, blast) 
  10.641 +
  10.642 +lemma (in M_ord_arith) is_omult_fun_apply_Limit:
  10.643 +    "[| x < j; Limit(x); M(j); M(f); is_omult_fun(M,i,j,f) |] 
  10.644 +     ==> f ` x = (\<Union>y\<in>x. f`y)"
  10.645 +apply (simp add: is_omult_fun_def omult_eqns_def domain_closed lt_def, clarify)
  10.646 +apply (drule subset_trans [OF OrdmemD], assumption+)  
  10.647 +apply (simp add: ball_conj_distrib omult_Limit image_function)
  10.648 +done
  10.649 +
  10.650 +lemma (in M_ord_arith) is_omult_fun_eq_omult:
  10.651 +    "[| is_omult_fun(M,i,J,f); M(J); M(f); Ord(i); Ord(j) |] 
  10.652 +     ==> j<J --> f`j = i**j"
  10.653 +apply (erule_tac i=j in trans_induct3)
  10.654 +apply (safe del: impCE)
  10.655 +  apply (simp add: is_omult_fun_apply_0) 
  10.656 + apply (subgoal_tac "x<J") 
  10.657 +  apply (simp add: is_omult_fun_apply_succ omult_succ)  
  10.658 + apply (blast intro: lt_trans) 
  10.659 +apply (subgoal_tac "\<forall>k\<in>x. k<J")
  10.660 + apply (simp add: is_omult_fun_apply_Limit omult_Limit) 
  10.661 +apply (blast intro: lt_trans ltI lt_Ord) 
  10.662 +done
  10.663 +
  10.664 +lemma (in M_ord_arith) omult_abs:
  10.665 +    "[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_omult(M,i,j,k) <-> k = i**j"
  10.666 +apply (simp add: is_omult_def is_omult_fun_eq_omult)
  10.667 +apply (frule exists_omult_fun [of j i], blast+)
  10.668 +done
  10.669 +
  10.670 +
  10.671 +
  10.672 +locale M_wfrank = M_trancl +
  10.673 +  assumes wfrank_separation:
  10.674 +     "M(r) ==>
  10.675 +      separation (M, \<lambda>x. 
  10.676 +         \<forall>rplus[M]. tran_closure(M,r,rplus) -->
  10.677 +         ~ (\<exists>f[M]. M_is_recfun(M, %x f y. is_range(M,f,y), rplus, x, f)))"
  10.678 + and wfrank_strong_replacement:
  10.679 +     "M(r) ==>
  10.680 +      strong_replacement(M, \<lambda>x z. 
  10.681 +         \<forall>rplus[M]. tran_closure(M,r,rplus) -->
  10.682 +         (\<exists>y[M]. \<exists>f[M]. pair(M,x,y,z)  & 
  10.683 +                        M_is_recfun(M, %x f y. is_range(M,f,y), rplus, x, f) &
  10.684 +                        is_range(M,f,y)))"
  10.685 + and Ord_wfrank_separation:
  10.686 +     "M(r) ==>
  10.687 +      separation (M, \<lambda>x.
  10.688 +         \<forall>rplus[M]. tran_closure(M,r,rplus) --> 
  10.689 +          ~ (\<forall>f[M]. \<forall>rangef[M]. 
  10.690 +             is_range(M,f,rangef) -->
  10.691 +             M_is_recfun(M, \<lambda>x f y. is_range(M,f,y), rplus, x, f) -->
  10.692 +             ordinal(M,rangef)))" 
  10.693 +
  10.694 +
  10.695 +text{*Proving that the relativized instances of Separation or Replacement
  10.696 +agree with the "real" ones.*}
  10.697 +
  10.698 +lemma (in M_wfrank) wfrank_separation':
  10.699 +     "M(r) ==>
  10.700 +      separation
  10.701 +	   (M, \<lambda>x. ~ (\<exists>f[M]. is_recfun(r^+, x, %x f. range(f), f)))"
  10.702 +apply (insert wfrank_separation [of r])
  10.703 +apply (simp add: relation2_def is_recfun_abs [of "%x. range"])
  10.704 +done
  10.705 +
  10.706 +lemma (in M_wfrank) wfrank_strong_replacement':
  10.707 +     "M(r) ==>
  10.708 +      strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>f[M]. 
  10.709 +		  pair(M,x,y,z) & is_recfun(r^+, x, %x f. range(f), f) &
  10.710 +		  y = range(f))"
  10.711 +apply (insert wfrank_strong_replacement [of r])
  10.712 +apply (simp add: relation2_def is_recfun_abs [of "%x. range"])
  10.713 +done
  10.714 +
  10.715 +lemma (in M_wfrank) Ord_wfrank_separation':
  10.716 +     "M(r) ==>
  10.717 +      separation (M, \<lambda>x. 
  10.718 +         ~ (\<forall>f[M]. is_recfun(r^+, x, \<lambda>x. range, f) --> Ord(range(f))))" 
  10.719 +apply (insert Ord_wfrank_separation [of r])
  10.720 +apply (simp add: relation2_def is_recfun_abs [of "%x. range"])
  10.721 +done
  10.722 +
  10.723 +text{*This function, defined using replacement, is a rank function for
  10.724 +well-founded relations within the class M.*}
  10.725 +constdefs
  10.726 + wellfoundedrank :: "[i=>o,i,i] => i"
  10.727 +    "wellfoundedrank(M,r,A) ==
  10.728 +        {p. x\<in>A, \<exists>y[M]. \<exists>f[M]. 
  10.729 +                       p = <x,y> & is_recfun(r^+, x, %x f. range(f), f) &
  10.730 +                       y = range(f)}"
  10.731 +
  10.732 +lemma (in M_wfrank) exists_wfrank:
  10.733 +    "[| wellfounded(M,r); M(a); M(r) |]
  10.734 +     ==> \<exists>f[M]. is_recfun(r^+, a, %x f. range(f), f)"
  10.735 +apply (rule wellfounded_exists_is_recfun)
  10.736 +      apply (blast intro: wellfounded_trancl)
  10.737 +     apply (rule trans_trancl)
  10.738 +    apply (erule wfrank_separation')
  10.739 +   apply (erule wfrank_strong_replacement')
  10.740 +apply (simp_all add: trancl_subset_times)
  10.741 +done
  10.742 +
  10.743 +lemma (in M_wfrank) M_wellfoundedrank:
  10.744 +    "[| wellfounded(M,r); M(r); M(A) |] ==> M(wellfoundedrank(M,r,A))"
  10.745 +apply (insert wfrank_strong_replacement' [of r])
  10.746 +apply (simp add: wellfoundedrank_def)
  10.747 +apply (rule strong_replacement_closed)
  10.748 +   apply assumption+
  10.749 + apply (rule univalent_is_recfun)
  10.750 +   apply (blast intro: wellfounded_trancl)
  10.751 +  apply (rule trans_trancl)
  10.752 + apply (simp add: trancl_subset_times) 
  10.753 +apply (blast dest: transM) 
  10.754 +done
  10.755 +
  10.756 +lemma (in M_wfrank) Ord_wfrank_range [rule_format]:
  10.757 +    "[| wellfounded(M,r); a\<in>A; M(r); M(A) |]
  10.758 +     ==> \<forall>f[M]. is_recfun(r^+, a, %x f. range(f), f) --> Ord(range(f))"
  10.759 +apply (drule wellfounded_trancl, assumption)
  10.760 +apply (rule wellfounded_induct, assumption, erule (1) transM)
  10.761 +  apply simp
  10.762 + apply (blast intro: Ord_wfrank_separation', clarify)
  10.763 +txt{*The reasoning in both cases is that we get @{term y} such that
  10.764 +   @{term "\<langle>y, x\<rangle> \<in> r^+"}.  We find that
  10.765 +   @{term "f`y = restrict(f, r^+ -`` {y})"}. *}
  10.766 +apply (rule OrdI [OF _ Ord_is_Transset])
  10.767 + txt{*An ordinal is a transitive set...*}
  10.768 + apply (simp add: Transset_def)
  10.769 + apply clarify
  10.770 + apply (frule apply_recfun2, assumption)
  10.771 + apply (force simp add: restrict_iff)
  10.772 +txt{*...of ordinals.  This second case requires the induction hyp.*}
  10.773 +apply clarify
  10.774 +apply (rename_tac i y)
  10.775 +apply (frule apply_recfun2, assumption)
  10.776 +apply (frule is_recfun_imp_in_r, assumption)
  10.777 +apply (frule is_recfun_restrict)
  10.778 +    (*simp_all won't work*)
  10.779 +    apply (simp add: trans_trancl trancl_subset_times)+
  10.780 +apply (drule spec [THEN mp], assumption)
  10.781 +apply (subgoal_tac "M(restrict(f, r^+ -`` {y}))")
  10.782 + apply (drule_tac x="restrict(f, r^+ -`` {y})" in rspec)
  10.783 +apply assumption
  10.784 + apply (simp add: function_apply_equality [OF _ is_recfun_imp_function])
  10.785 +apply (blast dest: pair_components_in_M)
  10.786 +done
  10.787 +
  10.788 +lemma (in M_wfrank) Ord_range_wellfoundedrank:
  10.789 +    "[| wellfounded(M,r); r \<subseteq> A*A;  M(r); M(A) |]
  10.790 +     ==> Ord (range(wellfoundedrank(M,r,A)))"
  10.791 +apply (frule wellfounded_trancl, assumption)
  10.792 +apply (frule trancl_subset_times)
  10.793 +apply (simp add: wellfoundedrank_def)
  10.794 +apply (rule OrdI [OF _ Ord_is_Transset])
  10.795 + prefer 2
  10.796 + txt{*by our previous result the range consists of ordinals.*}
  10.797 + apply (blast intro: Ord_wfrank_range)
  10.798 +txt{*We still must show that the range is a transitive set.*}
  10.799 +apply (simp add: Transset_def, clarify, simp)
  10.800 +apply (rename_tac x i f u)
  10.801 +apply (frule is_recfun_imp_in_r, assumption)
  10.802 +apply (subgoal_tac "M(u) & M(i) & M(x)")
  10.803 + prefer 2 apply (blast dest: transM, clarify)
  10.804 +apply (rule_tac a=u in rangeI)
  10.805 +apply (rule_tac x=u in ReplaceI)
  10.806 +  apply simp 
  10.807 +  apply (rule_tac x="restrict(f, r^+ -`` {u})" in rexI)
  10.808 +   apply (blast intro: is_recfun_restrict trans_trancl dest: apply_recfun2)
  10.809 +  apply simp 
  10.810 +apply blast 
  10.811 +txt{*Unicity requirement of Replacement*}
  10.812 +apply clarify
  10.813 +apply (frule apply_recfun2, assumption)
  10.814 +apply (simp add: trans_trancl is_recfun_cut)
  10.815 +done
  10.816 +
  10.817 +lemma (in M_wfrank) function_wellfoundedrank:
  10.818 +    "[| wellfounded(M,r); M(r); M(A)|]
  10.819 +     ==> function(wellfoundedrank(M,r,A))"
  10.820 +apply (simp add: wellfoundedrank_def function_def, clarify)
  10.821 +txt{*Uniqueness: repeated below!*}
  10.822 +apply (drule is_recfun_functional, assumption)
  10.823 +     apply (blast intro: wellfounded_trancl)
  10.824 +    apply (simp_all add: trancl_subset_times trans_trancl)
  10.825 +done
  10.826 +
  10.827 +lemma (in M_wfrank) domain_wellfoundedrank:
  10.828 +    "[| wellfounded(M,r); M(r); M(A)|]
  10.829 +     ==> domain(wellfoundedrank(M,r,A)) = A"
  10.830 +apply (simp add: wellfoundedrank_def function_def)
  10.831 +apply (rule equalityI, auto)
  10.832 +apply (frule transM, assumption)
  10.833 +apply (frule_tac a=x in exists_wfrank, assumption+, clarify)
  10.834 +apply (rule_tac b="range(f)" in domainI)
  10.835 +apply (rule_tac x=x in ReplaceI)
  10.836 +  apply simp 
  10.837 +  apply (rule_tac x=f in rexI, blast, simp_all)
  10.838 +txt{*Uniqueness (for Replacement): repeated above!*}
  10.839 +apply clarify
  10.840 +apply (drule is_recfun_functional, assumption)
  10.841 +    apply (blast intro: wellfounded_trancl)
  10.842 +    apply (simp_all add: trancl_subset_times trans_trancl)
  10.843 +done
  10.844 +
  10.845 +lemma (in M_wfrank) wellfoundedrank_type:
  10.846 +    "[| wellfounded(M,r);  M(r); M(A)|]
  10.847 +     ==> wellfoundedrank(M,r,A) \<in> A -> range(wellfoundedrank(M,r,A))"
  10.848 +apply (frule function_wellfoundedrank [of r A], assumption+)
  10.849 +apply (frule function_imp_Pi)
  10.850 + apply (simp add: wellfoundedrank_def relation_def)
  10.851 + apply blast
  10.852 +apply (simp add: domain_wellfoundedrank)
  10.853 +done
  10.854 +
  10.855 +lemma (in M_wfrank) Ord_wellfoundedrank:
  10.856 +    "[| wellfounded(M,r); a \<in> A; r \<subseteq> A*A;  M(r); M(A) |]
  10.857 +     ==> Ord(wellfoundedrank(M,r,A) ` a)"
  10.858 +by (blast intro: apply_funtype [OF wellfoundedrank_type]
  10.859 +                 Ord_in_Ord [OF Ord_range_wellfoundedrank])
  10.860 +
  10.861 +lemma (in M_wfrank) wellfoundedrank_eq:
  10.862 +     "[| is_recfun(r^+, a, %x. range, f);
  10.863 +         wellfounded(M,r);  a \<in> A; M(f); M(r); M(A)|]
  10.864 +      ==> wellfoundedrank(M,r,A) ` a = range(f)"
  10.865 +apply (rule apply_equality)
  10.866 + prefer 2 apply (blast intro: wellfoundedrank_type)
  10.867 +apply (simp add: wellfoundedrank_def)
  10.868 +apply (rule ReplaceI)
  10.869 +  apply (rule_tac x="range(f)" in rexI) 
  10.870 +  apply blast
  10.871 + apply simp_all
  10.872 +txt{*Unicity requirement of Replacement*}
  10.873 +apply clarify
  10.874 +apply (drule is_recfun_functional, assumption)
  10.875 +    apply (blast intro: wellfounded_trancl)
  10.876 +    apply (simp_all add: trancl_subset_times trans_trancl)
  10.877 +done
  10.878 +
  10.879 +
  10.880 +lemma (in M_wfrank) wellfoundedrank_lt:
  10.881 +     "[| <a,b> \<in> r;
  10.882 +         wellfounded(M,r); r \<subseteq> A*A;  M(r); M(A)|]
  10.883 +      ==> wellfoundedrank(M,r,A) ` a < wellfoundedrank(M,r,A) ` b"
  10.884 +apply (frule wellfounded_trancl, assumption)
  10.885 +apply (subgoal_tac "a\<in>A & b\<in>A")
  10.886 + prefer 2 apply blast
  10.887 +apply (simp add: lt_def Ord_wellfoundedrank, clarify)
  10.888 +apply (frule exists_wfrank [of concl: _ b], erule (1) transM, assumption)
  10.889 +apply clarify
  10.890 +apply (rename_tac fb)
  10.891 +apply (frule is_recfun_restrict [of concl: "r^+" a])
  10.892 +    apply (rule trans_trancl, assumption)
  10.893 +   apply (simp_all add: r_into_trancl trancl_subset_times)
  10.894 +txt{*Still the same goal, but with new @{text is_recfun} assumptions.*}
  10.895 +apply (simp add: wellfoundedrank_eq)
  10.896 +apply (frule_tac a=a in wellfoundedrank_eq, assumption+)
  10.897 +   apply (simp_all add: transM [of a])
  10.898 +txt{*We have used equations for wellfoundedrank and now must use some
  10.899 +    for  @{text is_recfun}. *}
  10.900 +apply (rule_tac a=a in rangeI)
  10.901 +apply (simp add: is_recfun_type [THEN apply_iff] vimage_singleton_iff
  10.902 +                 r_into_trancl apply_recfun r_into_trancl)
  10.903 +done
  10.904 +
  10.905 +
  10.906 +lemma (in M_wfrank) wellfounded_imp_subset_rvimage:
  10.907 +     "[|wellfounded(M,r); r \<subseteq> A*A; M(r); M(A)|]
  10.908 +      ==> \<exists>i f. Ord(i) & r <= rvimage(A, f, Memrel(i))"
  10.909 +apply (rule_tac x="range(wellfoundedrank(M,r,A))" in exI)
  10.910 +apply (rule_tac x="wellfoundedrank(M,r,A)" in exI)
  10.911 +apply (simp add: Ord_range_wellfoundedrank, clarify)
  10.912 +apply (frule subsetD, assumption, clarify)
  10.913 +apply (simp add: rvimage_iff wellfoundedrank_lt [THEN ltD])
  10.914 +apply (blast intro: apply_rangeI wellfoundedrank_type)
  10.915 +done
  10.916 +
  10.917 +lemma (in M_wfrank) wellfounded_imp_wf:
  10.918 +     "[|wellfounded(M,r); relation(r); M(r)|] ==> wf(r)"
  10.919 +by (blast dest!: relation_field_times_field wellfounded_imp_subset_rvimage
  10.920 +          intro: wf_rvimage_Ord [THEN wf_subset])
  10.921 +
  10.922 +lemma (in M_wfrank) wellfounded_on_imp_wf_on:
  10.923 +     "[|wellfounded_on(M,A,r); relation(r); M(r); M(A)|] ==> wf[A](r)"
  10.924 +apply (simp add: wellfounded_on_iff_wellfounded wf_on_def)
  10.925 +apply (rule wellfounded_imp_wf)
  10.926 +apply (simp_all add: relation_def)
  10.927 +done
  10.928 +
  10.929 +
  10.930 +theorem (in M_wfrank) wf_abs:
  10.931 +     "[|relation(r); M(r)|] ==> wellfounded(M,r) <-> wf(r)"
  10.932 +by (blast intro: wellfounded_imp_wf wf_imp_relativized)
  10.933 +
  10.934 +theorem (in M_wfrank) wf_on_abs:
  10.935 +     "[|relation(r); M(r); M(A)|] ==> wellfounded_on(M,A,r) <-> wf[A](r)"
  10.936 +by (blast intro: wellfounded_on_imp_wf_on wf_on_imp_relativized)
  10.937 +
  10.938 +end
  10.939 \ No newline at end of file
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/ZF/Constructible/Rank_Separation.thy	Wed Oct 09 11:07:13 2002 +0200
    11.3 @@ -0,0 +1,265 @@
    11.4 +(*  Title:      ZF/Constructible/Rank_Separation.thy
    11.5 +    ID:   $Id$
    11.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    11.7 +*)
    11.8 +
    11.9 +header {*Separation for Facts About Order Types, Rank Functions and 
   11.10 +      Well-Founded Relations*}
   11.11 +
   11.12 +theory Rank_Separation = Rank + Rec_Separation:
   11.13 +
   11.14 +
   11.15 +text{*This theory proves all instances needed for locales
   11.16 +       @{text "M_ordertype"} and  @{text "M_wfrank"}*}
   11.17 +
   11.18 +subsection{*The Locale @{text "M_ordertype"}*}
   11.19 +
   11.20 +subsubsection{*Separation for Order-Isomorphisms*}
   11.21 +
   11.22 +lemma well_ord_iso_Reflects:
   11.23 +  "REFLECTS[\<lambda>x. x\<in>A -->
   11.24 +                (\<exists>y[L]. \<exists>p[L]. fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r),
   11.25 +        \<lambda>i x. x\<in>A --> (\<exists>y \<in> Lset(i). \<exists>p \<in> Lset(i).
   11.26 +                fun_apply(**Lset(i),f,x,y) & pair(**Lset(i),y,x,p) & p \<in> r)]"
   11.27 +by (intro FOL_reflections function_reflections)
   11.28 +
   11.29 +lemma well_ord_iso_separation:
   11.30 +     "[| L(A); L(f); L(r) |]
   11.31 +      ==> separation (L, \<lambda>x. x\<in>A --> (\<exists>y[L]. (\<exists>p[L].
   11.32 +                     fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r)))"
   11.33 +apply (rule gen_separation [OF well_ord_iso_Reflects, of "{A,f,r}"], simp)
   11.34 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   11.35 +apply (rule DPow_LsetI)
   11.36 +apply (rule imp_iff_sats)
   11.37 +apply (rule_tac env = "[x,A,f,r]" in mem_iff_sats)
   11.38 +apply (rule sep_rules | simp)+
   11.39 +done
   11.40 +
   11.41 +
   11.42 +subsubsection{*Separation for @{term "obase"}*}
   11.43 +
   11.44 +lemma obase_reflects:
   11.45 +  "REFLECTS[\<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
   11.46 +             ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
   11.47 +             order_isomorphism(L,par,r,x,mx,g),
   11.48 +        \<lambda>i a. \<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i). \<exists>par \<in> Lset(i).
   11.49 +             ordinal(**Lset(i),x) & membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) &
   11.50 +             order_isomorphism(**Lset(i),par,r,x,mx,g)]"
   11.51 +by (intro FOL_reflections function_reflections fun_plus_reflections)
   11.52 +
   11.53 +lemma obase_separation:
   11.54 +     --{*part of the order type formalization*}
   11.55 +     "[| L(A); L(r) |]
   11.56 +      ==> separation(L, \<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
   11.57 +             ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
   11.58 +             order_isomorphism(L,par,r,x,mx,g))"
   11.59 +apply (rule gen_separation [OF obase_reflects, of "{A,r}"], simp)
   11.60 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   11.61 +apply (rule DPow_LsetI)
   11.62 +apply (rule bex_iff_sats conj_iff_sats)+
   11.63 +apply (rule_tac env = "[x,a,A,r]" in ordinal_iff_sats)
   11.64 +apply (rule sep_rules | simp)+
   11.65 +done
   11.66 +
   11.67 +
   11.68 +subsubsection{*Separation for a Theorem about @{term "obase"}*}
   11.69 +
   11.70 +lemma obase_equals_reflects:
   11.71 +  "REFLECTS[\<lambda>x. x\<in>A --> ~(\<exists>y[L]. \<exists>g[L].
   11.72 +                ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L].
   11.73 +                membership(L,y,my) & pred_set(L,A,x,r,pxr) &
   11.74 +                order_isomorphism(L,pxr,r,y,my,g))),
   11.75 +        \<lambda>i x. x\<in>A --> ~(\<exists>y \<in> Lset(i). \<exists>g \<in> Lset(i).
   11.76 +                ordinal(**Lset(i),y) & (\<exists>my \<in> Lset(i). \<exists>pxr \<in> Lset(i).
   11.77 +                membership(**Lset(i),y,my) & pred_set(**Lset(i),A,x,r,pxr) &
   11.78 +                order_isomorphism(**Lset(i),pxr,r,y,my,g)))]"
   11.79 +by (intro FOL_reflections function_reflections fun_plus_reflections)
   11.80 +
   11.81 +lemma obase_equals_separation:
   11.82 +     "[| L(A); L(r) |]
   11.83 +      ==> separation (L, \<lambda>x. x\<in>A --> ~(\<exists>y[L]. \<exists>g[L].
   11.84 +                              ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L].
   11.85 +                              membership(L,y,my) & pred_set(L,A,x,r,pxr) &
   11.86 +                              order_isomorphism(L,pxr,r,y,my,g))))"
   11.87 +apply (rule gen_separation [OF obase_equals_reflects, of "{A,r}"], simp)
   11.88 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   11.89 +apply (rule DPow_LsetI)
   11.90 +apply (rule imp_iff_sats ball_iff_sats disj_iff_sats not_iff_sats)+
   11.91 +apply (rule_tac env = "[x,A,r]" in mem_iff_sats)
   11.92 +apply (rule sep_rules | simp)+
   11.93 +done
   11.94 +
   11.95 +
   11.96 +subsubsection{*Replacement for @{term "omap"}*}
   11.97 +
   11.98 +lemma omap_reflects:
   11.99 + "REFLECTS[\<lambda>z. \<exists>a[L]. a\<in>B & (\<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
  11.100 +     ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) &
  11.101 +     pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g)),
  11.102 + \<lambda>i z. \<exists>a \<in> Lset(i). a\<in>B & (\<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i).
  11.103 +        \<exists>par \<in> Lset(i).
  11.104 +         ordinal(**Lset(i),x) & pair(**Lset(i),a,x,z) &
  11.105 +         membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) &
  11.106 +         order_isomorphism(**Lset(i),par,r,x,mx,g))]"
  11.107 +by (intro FOL_reflections function_reflections fun_plus_reflections)
  11.108 +
  11.109 +lemma omap_replacement:
  11.110 +     "[| L(A); L(r) |]
  11.111 +      ==> strong_replacement(L,
  11.112 +             \<lambda>a z. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
  11.113 +             ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) &
  11.114 +             pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g))"
  11.115 +apply (rule strong_replacementI)
  11.116 +apply (rename_tac B)
  11.117 +apply (rule_tac u="{A,r,B}" in gen_separation [OF omap_reflects], simp)
  11.118 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
  11.119 +apply (rule DPow_LsetI)
  11.120 +apply (rule bex_iff_sats conj_iff_sats)+
  11.121 +apply (rule_tac env = "[a,z,A,B,r]" in mem_iff_sats)
  11.122 +apply (rule sep_rules | simp)+
  11.123 +done
  11.124 +
  11.125 +
  11.126 +
  11.127 +subsection{*Instantiating the locale @{text M_ordertype}*}
  11.128 +text{*Separation (and Strong Replacement) for basic set-theoretic constructions
  11.129 +such as intersection, Cartesian Product and image.*}
  11.130 +
  11.131 +lemma M_ordertype_axioms_L: "M_ordertype_axioms(L)"
  11.132 +  apply (rule M_ordertype_axioms.intro)
  11.133 +       apply (assumption | rule well_ord_iso_separation
  11.134 +	 obase_separation obase_equals_separation
  11.135 +	 omap_replacement)+
  11.136 +  done
  11.137 +
  11.138 +theorem M_ordertype_L: "PROP M_ordertype(L)"
  11.139 +apply (rule M_ordertype.intro)
  11.140 +     apply (rule M_basic.axioms [OF M_basic_L])+
  11.141 +apply (rule M_ordertype_axioms_L) 
  11.142 +done
  11.143 +
  11.144 +
  11.145 +subsection{*The Locale @{text "M_wfrank"}*}
  11.146 +
  11.147 +subsubsection{*Separation for @{term "wfrank"}*}
  11.148 +
  11.149 +lemma wfrank_Reflects:
  11.150 + "REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
  11.151 +              ~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)),
  11.152 +      \<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
  11.153 +         ~ (\<exists>f \<in> Lset(i).
  11.154 +            M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y),
  11.155 +                        rplus, x, f))]"
  11.156 +by (intro FOL_reflections function_reflections is_recfun_reflection tran_closure_reflection)
  11.157 +
  11.158 +lemma wfrank_separation:
  11.159 +     "L(r) ==>
  11.160 +      separation (L, \<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
  11.161 +         ~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)))"
  11.162 +apply (rule gen_separation [OF wfrank_Reflects], simp)
  11.163 +apply (rule DPow_LsetI)
  11.164 +apply (rule ball_iff_sats imp_iff_sats)+
  11.165 +apply (rule_tac env="[rplus,x,r]" in tran_closure_iff_sats)
  11.166 +apply (rule sep_rules is_recfun_iff_sats | simp)+
  11.167 +done
  11.168 +
  11.169 +
  11.170 +subsubsection{*Replacement for @{term "wfrank"}*}
  11.171 +
  11.172 +lemma wfrank_replacement_Reflects:
  11.173 + "REFLECTS[\<lambda>z. \<exists>x[L]. x \<in> A &
  11.174 +        (\<forall>rplus[L]. tran_closure(L,r,rplus) -->
  11.175 +         (\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z)  &
  11.176 +                        M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) &
  11.177 +                        is_range(L,f,y))),
  11.178 + \<lambda>i z. \<exists>x \<in> Lset(i). x \<in> A &
  11.179 +      (\<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
  11.180 +       (\<exists>y \<in> Lset(i). \<exists>f \<in> Lset(i). pair(**Lset(i),x,y,z)  &
  11.181 +         M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y), rplus, x, f) &
  11.182 +         is_range(**Lset(i),f,y)))]"
  11.183 +by (intro FOL_reflections function_reflections fun_plus_reflections
  11.184 +             is_recfun_reflection tran_closure_reflection)
  11.185 +
  11.186 +lemma wfrank_strong_replacement:
  11.187 +     "L(r) ==>
  11.188 +      strong_replacement(L, \<lambda>x z.
  11.189 +         \<forall>rplus[L]. tran_closure(L,r,rplus) -->
  11.190 +         (\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z)  &
  11.191 +                        M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) &
  11.192 +                        is_range(L,f,y)))"
  11.193 +apply (rule strong_replacementI)
  11.194 +apply (rule_tac u="{r,A}" in gen_separation [OF wfrank_replacement_Reflects], 
  11.195 +       simp)
  11.196 +apply (drule mem_Lset_imp_subset_Lset, clarsimp)
  11.197 +apply (rule DPow_LsetI)
  11.198 +apply (rule bex_iff_sats ball_iff_sats conj_iff_sats)+
  11.199 +apply (rule_tac env = "[x,z,A,r]" in mem_iff_sats)
  11.200 +apply (rule sep_rules list.intros app_type tran_closure_iff_sats 
  11.201 +            is_recfun_iff_sats | simp)+
  11.202 +done
  11.203 +
  11.204 +
  11.205 +subsubsection{*Separation for Proving @{text Ord_wfrank_range}*}
  11.206 +
  11.207 +lemma Ord_wfrank_Reflects:
  11.208 + "REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
  11.209 +          ~ (\<forall>f[L]. \<forall>rangef[L].
  11.210 +             is_range(L,f,rangef) -->
  11.211 +             M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) -->
  11.212 +             ordinal(L,rangef)),
  11.213 +      \<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
  11.214 +          ~ (\<forall>f \<in> Lset(i). \<forall>rangef \<in> Lset(i).
  11.215 +             is_range(**Lset(i),f,rangef) -->
  11.216 +             M_is_recfun(**Lset(i), \<lambda>x f y. is_range(**Lset(i),f,y),
  11.217 +                         rplus, x, f) -->
  11.218 +             ordinal(**Lset(i),rangef))]"
  11.219 +by (intro FOL_reflections function_reflections is_recfun_reflection
  11.220 +          tran_closure_reflection ordinal_reflection)
  11.221 +
  11.222 +lemma  Ord_wfrank_separation:
  11.223 +     "L(r) ==>
  11.224 +      separation (L, \<lambda>x.
  11.225 +         \<forall>rplus[L]. tran_closure(L,r,rplus) -->
  11.226 +          ~ (\<forall>f[L]. \<forall>rangef[L].
  11.227 +             is_range(L,f,rangef) -->
  11.228 +             M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) -->
  11.229 +             ordinal(L,rangef)))"
  11.230 +apply (rule gen_separation [OF Ord_wfrank_Reflects], simp)
  11.231 +apply (rule DPow_LsetI)
  11.232 +apply (rule ball_iff_sats imp_iff_sats)+
  11.233 +apply (rule_tac env="[rplus,x,r]" in tran_closure_iff_sats)
  11.234 +apply (rule sep_rules is_recfun_iff_sats | simp)+
  11.235 +done
  11.236 +
  11.237 +
  11.238 +subsubsection{*Instantiating the locale @{text M_wfrank}*}
  11.239 +
  11.240 +lemma M_wfrank_axioms_L: "M_wfrank_axioms(L)"
  11.241 +  apply (rule M_wfrank_axioms.intro)
  11.242 +   apply (assumption | rule
  11.243 +     wfrank_separation wfrank_strong_replacement Ord_wfrank_separation)+
  11.244 +  done
  11.245 +
  11.246 +theorem M_wfrank_L: "PROP M_wfrank(L)"
  11.247 +  apply (rule M_wfrank.intro)
  11.248 +     apply (rule M_trancl.axioms [OF M_trancl_L])+
  11.249 +  apply (rule M_wfrank_axioms_L) 
  11.250 +  done
  11.251 +
  11.252 +lemmas exists_wfrank = M_wfrank.exists_wfrank [OF M_wfrank_L]
  11.253 +  and M_wellfoundedrank = M_wfrank.M_wellfoundedrank [OF M_wfrank_L]
  11.254 +  and Ord_wfrank_range = M_wfrank.Ord_wfrank_range [OF M_wfrank_L]
  11.255 +  and Ord_range_wellfoundedrank = M_wfrank.Ord_range_wellfoundedrank [OF M_wfrank_L]
  11.256 +  and function_wellfoundedrank = M_wfrank.function_wellfoundedrank [OF M_wfrank_L]
  11.257 +  and domain_wellfoundedrank = M_wfrank.domain_wellfoundedrank [OF M_wfrank_L]
  11.258 +  and wellfoundedrank_type = M_wfrank.wellfoundedrank_type [OF M_wfrank_L]
  11.259 +  and Ord_wellfoundedrank = M_wfrank.Ord_wellfoundedrank [OF M_wfrank_L]
  11.260 +  and wellfoundedrank_eq = M_wfrank.wellfoundedrank_eq [OF M_wfrank_L]
  11.261 +  and wellfoundedrank_lt = M_wfrank.wellfoundedrank_lt [OF M_wfrank_L]
  11.262 +  and wellfounded_imp_subset_rvimage = M_wfrank.wellfounded_imp_subset_rvimage [OF M_wfrank_L]
  11.263 +  and wellfounded_imp_wf = M_wfrank.wellfounded_imp_wf [OF M_wfrank_L]
  11.264 +  and wellfounded_on_imp_wf_on = M_wfrank.wellfounded_on_imp_wf_on [OF M_wfrank_L]
  11.265 +  and wf_abs = M_wfrank.wf_abs [OF M_wfrank_L]
  11.266 +  and wf_on_abs = M_wfrank.wf_on_abs [OF M_wfrank_L]
  11.267 +
  11.268 +end
  11.269 \ No newline at end of file
    12.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Tue Oct 08 14:09:18 2002 +0200
    12.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Wed Oct 09 11:07:13 2002 +0200
    12.3 @@ -1,7 +1,6 @@
    12.4  (*  Title:      ZF/Constructible/Rec_Separation.thy
    12.5 -    ID:         $Id$
    12.6 +    ID:   $Id$
    12.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    12.8 -    Copyright   2002  University of Cambridge
    12.9  *)
   12.10  
   12.11  header {*Separation for Facts About Recursion*}
   12.12 @@ -9,7 +8,7 @@
   12.13  theory Rec_Separation = Separation + Internalize:
   12.14  
   12.15  text{*This theory proves all instances needed for locales @{text
   12.16 -"M_trancl"}, @{text "M_wfrank"} and @{text "M_datatypes"}*}
   12.17 +"M_trancl"} and @{text "M_datatypes"}*}
   12.18  
   12.19  lemma eq_succ_imp_lt: "[|i = succ(j); Ord(i)|] ==> j<i"
   12.20  by simp
   12.21 @@ -223,139 +222,6 @@
   12.22  declare trancl_abs [simp]
   12.23  
   12.24  
   12.25 -subsection{*The Locale @{text "M_wfrank"}*}
   12.26 -
   12.27 -subsubsection{*Separation for @{term "wfrank"}*}
   12.28 -
   12.29 -lemma wfrank_Reflects:
   12.30 - "REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
   12.31 -              ~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)),
   12.32 -      \<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
   12.33 -         ~ (\<exists>f \<in> Lset(i).
   12.34 -            M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y),
   12.35 -                        rplus, x, f))]"
   12.36 -by (intro FOL_reflections function_reflections is_recfun_reflection tran_closure_reflection)
   12.37 -
   12.38 -lemma wfrank_separation:
   12.39 -     "L(r) ==>
   12.40 -      separation (L, \<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
   12.41 -         ~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)))"
   12.42 -apply (rule gen_separation [OF wfrank_Reflects], simp)
   12.43 -apply (rule DPow_LsetI)
   12.44 -apply (rule ball_iff_sats imp_iff_sats)+
   12.45 -apply (rule_tac env="[rplus,x,r]" in tran_closure_iff_sats)
   12.46 -apply (rule sep_rules is_recfun_iff_sats | simp)+
   12.47 -done
   12.48 -
   12.49 -
   12.50 -subsubsection{*Replacement for @{term "wfrank"}*}
   12.51 -
   12.52 -lemma wfrank_replacement_Reflects:
   12.53 - "REFLECTS[\<lambda>z. \<exists>x[L]. x \<in> A &
   12.54 -        (\<forall>rplus[L]. tran_closure(L,r,rplus) -->
   12.55 -         (\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z)  &
   12.56 -                        M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) &
   12.57 -                        is_range(L,f,y))),
   12.58 - \<lambda>i z. \<exists>x \<in> Lset(i). x \<in> A &
   12.59 -      (\<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
   12.60 -       (\<exists>y \<in> Lset(i). \<exists>f \<in> Lset(i). pair(**Lset(i),x,y,z)  &
   12.61 -         M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y), rplus, x, f) &
   12.62 -         is_range(**Lset(i),f,y)))]"
   12.63 -by (intro FOL_reflections function_reflections fun_plus_reflections
   12.64 -             is_recfun_reflection tran_closure_reflection)
   12.65 -
   12.66 -lemma wfrank_strong_replacement:
   12.67 -     "L(r) ==>
   12.68 -      strong_replacement(L, \<lambda>x z.
   12.69 -         \<forall>rplus[L]. tran_closure(L,r,rplus) -->
   12.70 -         (\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z)  &
   12.71 -                        M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) &
   12.72 -                        is_range(L,f,y)))"
   12.73 -apply (rule strong_replacementI)
   12.74 -apply (rule_tac u="{r,A}" in gen_separation [OF wfrank_replacement_Reflects], 
   12.75 -       simp)
   12.76 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   12.77 -apply (rule DPow_LsetI)
   12.78 -apply (rule bex_iff_sats ball_iff_sats conj_iff_sats)+
   12.79 -apply (rule_tac env = "[x,z,A,r]" in mem_iff_sats)
   12.80 -apply (rule sep_rules list.intros app_type tran_closure_iff_sats 
   12.81 -            is_recfun_iff_sats | simp)+
   12.82 -done
   12.83 -
   12.84 -
   12.85 -subsubsection{*Separation for Proving @{text Ord_wfrank_range}*}
   12.86 -
   12.87 -lemma Ord_wfrank_Reflects:
   12.88 - "REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
   12.89 -          ~ (\<forall>f[L]. \<forall>rangef[L].
   12.90 -             is_range(L,f,rangef) -->
   12.91 -             M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) -->
   12.92 -             ordinal(L,rangef)),
   12.93 -      \<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
   12.94 -          ~ (\<forall>f \<in> Lset(i). \<forall>rangef \<in> Lset(i).
   12.95 -             is_range(**Lset(i),f,rangef) -->
   12.96 -             M_is_recfun(**Lset(i), \<lambda>x f y. is_range(**Lset(i),f,y),
   12.97 -                         rplus, x, f) -->
   12.98 -             ordinal(**Lset(i),rangef))]"
   12.99 -by (intro FOL_reflections function_reflections is_recfun_reflection
  12.100 -          tran_closure_reflection ordinal_reflection)
  12.101 -
  12.102 -lemma  Ord_wfrank_separation:
  12.103 -     "L(r) ==>
  12.104 -      separation (L, \<lambda>x.
  12.105 -         \<forall>rplus[L]. tran_closure(L,r,rplus) -->
  12.106 -          ~ (\<forall>f[L]. \<forall>rangef[L].
  12.107 -             is_range(L,f,rangef) -->
  12.108 -             M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) -->
  12.109 -             ordinal(L,rangef)))"
  12.110 -apply (rule gen_separation [OF Ord_wfrank_Reflects], simp)
  12.111 -apply (rule DPow_LsetI)
  12.112 -apply (rule ball_iff_sats imp_iff_sats)+
  12.113 -apply (rule_tac env="[rplus,x,r]" in tran_closure_iff_sats)
  12.114 -apply (rule sep_rules is_recfun_iff_sats | simp)+
  12.115 -done
  12.116 -
  12.117 -
  12.118 -subsubsection{*Instantiating the locale @{text M_wfrank}*}
  12.119 -
  12.120 -lemma M_wfrank_axioms_L: "M_wfrank_axioms(L)"
  12.121 -  apply (rule M_wfrank_axioms.intro)
  12.122 -   apply (assumption | rule
  12.123 -     wfrank_separation wfrank_strong_replacement Ord_wfrank_separation)+
  12.124 -  done
  12.125 -
  12.126 -theorem M_wfrank_L: "PROP M_wfrank(L)"
  12.127 -  apply (rule M_wfrank.intro)
  12.128 -     apply (rule M_trancl.axioms [OF M_trancl_L])+
  12.129 -  apply (rule M_wfrank_axioms_L) 
  12.130 -  done
  12.131 -
  12.132 -lemmas iterates_closed = M_wfrank.iterates_closed [OF M_wfrank_L]
  12.133 -  and exists_wfrank = M_wfrank.exists_wfrank [OF M_wfrank_L]
  12.134 -  and M_wellfoundedrank = M_wfrank.M_wellfoundedrank [OF M_wfrank_L]
  12.135 -  and Ord_wfrank_range = M_wfrank.Ord_wfrank_range [OF M_wfrank_L]
  12.136 -  and Ord_range_wellfoundedrank = M_wfrank.Ord_range_wellfoundedrank [OF M_wfrank_L]
  12.137 -  and function_wellfoundedrank = M_wfrank.function_wellfoundedrank [OF M_wfrank_L]
  12.138 -  and domain_wellfoundedrank = M_wfrank.domain_wellfoundedrank [OF M_wfrank_L]
  12.139 -  and wellfoundedrank_type = M_wfrank.wellfoundedrank_type [OF M_wfrank_L]
  12.140 -  and Ord_wellfoundedrank = M_wfrank.Ord_wellfoundedrank [OF M_wfrank_L]
  12.141 -  and wellfoundedrank_eq = M_wfrank.wellfoundedrank_eq [OF M_wfrank_L]
  12.142 -  and wellfoundedrank_lt = M_wfrank.wellfoundedrank_lt [OF M_wfrank_L]
  12.143 -  and wellfounded_imp_subset_rvimage = M_wfrank.wellfounded_imp_subset_rvimage [OF M_wfrank_L]
  12.144 -  and wellfounded_imp_wf = M_wfrank.wellfounded_imp_wf [OF M_wfrank_L]
  12.145 -  and wellfounded_on_imp_wf_on = M_wfrank.wellfounded_on_imp_wf_on [OF M_wfrank_L]
  12.146 -  and wf_abs = M_wfrank.wf_abs [OF M_wfrank_L]
  12.147 -  and wf_on_abs = M_wfrank.wf_on_abs [OF M_wfrank_L]
  12.148 -  and wfrec_replacement_iff = M_wfrank.wfrec_replacement_iff [OF M_wfrank_L]
  12.149 -  and trans_wfrec_closed = M_wfrank.trans_wfrec_closed [OF M_wfrank_L]
  12.150 -  and wfrec_closed = M_wfrank.wfrec_closed [OF M_wfrank_L]
  12.151 -
  12.152 -declare iterates_closed [intro,simp]
  12.153 -declare Ord_wfrank_range [rule_format]
  12.154 -declare wf_abs [simp]
  12.155 -declare wf_on_abs [simp]
  12.156 -
  12.157 -
  12.158  subsection{*@{term L} is Closed Under the Operator @{term list}*}
  12.159  
  12.160  subsubsection{*Instances of Replacement for Lists*}
  12.161 @@ -578,7 +444,7 @@
  12.162  
  12.163  theorem M_datatypes_L: "PROP M_datatypes(L)"
  12.164    apply (rule M_datatypes.intro)
  12.165 -      apply (rule M_wfrank.axioms [OF M_wfrank_L])+
  12.166 +      apply (rule M_trancl.axioms [OF M_trancl_L])+
  12.167   apply (rule M_datatypes_axioms_L) 
  12.168   done
  12.169  
    13.1 --- a/src/ZF/Constructible/Reflection.thy	Tue Oct 08 14:09:18 2002 +0200
    13.2 +++ b/src/ZF/Constructible/Reflection.thy	Wed Oct 09 11:07:13 2002 +0200
    13.3 @@ -1,7 +1,6 @@
    13.4  (*  Title:      ZF/Constructible/Reflection.thy
    13.5      ID:         $Id$
    13.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    13.7 -    Copyright   2002  University of Cambridge
    13.8  *)
    13.9  
   13.10  header {* The Reflection Theorem*}
    14.1 --- a/src/ZF/Constructible/Relative.thy	Tue Oct 08 14:09:18 2002 +0200
    14.2 +++ b/src/ZF/Constructible/Relative.thy	Wed Oct 09 11:07:13 2002 +0200
    14.3 @@ -1,7 +1,6 @@
    14.4  (*  Title:      ZF/Constructible/Relative.thy
    14.5      ID:         $Id$
    14.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    14.7 -    Copyright   2002  University of Cambridge
    14.8  *)
    14.9  
   14.10  header {*Relativization and Absoluteness*}
   14.11 @@ -197,43 +196,43 @@
   14.12         (\<forall>m[M]. successor(M,m,k) --> is_b(m,z)) &
   14.13         (is_quasinat(M,k) | empty(M,z))"
   14.14  
   14.15 -  relativize1 :: "[i=>o, [i,i]=>o, i=>i] => o"
   14.16 -    "relativize1(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. is_f(x,y) <-> y = f(x)"
   14.17 +  relation1 :: "[i=>o, [i,i]=>o, i=>i] => o"
   14.18 +    "relation1(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. is_f(x,y) <-> y = f(x)"
   14.19  
   14.20 -  Relativize1 :: "[i=>o, i, [i,i]=>o, i=>i] => o"
   14.21 +  Relation1 :: "[i=>o, i, [i,i]=>o, i=>i] => o"
   14.22      --{*as above, but typed*}
   14.23 -    "Relativize1(M,A,is_f,f) ==
   14.24 +    "Relation1(M,A,is_f,f) ==
   14.25          \<forall>x[M]. \<forall>y[M]. x\<in>A --> is_f(x,y) <-> y = f(x)"
   14.26  
   14.27 -  relativize2 :: "[i=>o, [i,i,i]=>o, [i,i]=>i] => o"
   14.28 -    "relativize2(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. is_f(x,y,z) <-> z = f(x,y)"
   14.29 +  relation2 :: "[i=>o, [i,i,i]=>o, [i,i]=>i] => o"
   14.30 +    "relation2(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. is_f(x,y,z) <-> z = f(x,y)"
   14.31  
   14.32 -  Relativize2 :: "[i=>o, i, i, [i,i,i]=>o, [i,i]=>i] => o"
   14.33 -    "Relativize2(M,A,B,is_f,f) ==
   14.34 +  Relation2 :: "[i=>o, i, i, [i,i,i]=>o, [i,i]=>i] => o"
   14.35 +    "Relation2(M,A,B,is_f,f) ==
   14.36          \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. x\<in>A --> y\<in>B --> is_f(x,y,z) <-> z = f(x,y)"
   14.37  
   14.38 -  relativize3 :: "[i=>o, [i,i,i,i]=>o, [i,i,i]=>i] => o"
   14.39 -    "relativize3(M,is_f,f) ==
   14.40 +  relation3 :: "[i=>o, [i,i,i,i]=>o, [i,i,i]=>i] => o"
   14.41 +    "relation3(M,is_f,f) ==
   14.42         \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M]. is_f(x,y,z,u) <-> u = f(x,y,z)"
   14.43  
   14.44 -  Relativize3 :: "[i=>o, i, i, i, [i,i,i,i]=>o, [i,i,i]=>i] => o"
   14.45 -    "Relativize3(M,A,B,C,is_f,f) ==
   14.46 +  Relation3 :: "[i=>o, i, i, i, [i,i,i,i]=>o, [i,i,i]=>i] => o"
   14.47 +    "Relation3(M,A,B,C,is_f,f) ==
   14.48         \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M].
   14.49           x\<in>A --> y\<in>B --> z\<in>C --> is_f(x,y,z,u) <-> u = f(x,y,z)"
   14.50  
   14.51 -  relativize4 :: "[i=>o, [i,i,i,i,i]=>o, [i,i,i,i]=>i] => o"
   14.52 -    "relativize4(M,is_f,f) ==
   14.53 +  relation4 :: "[i=>o, [i,i,i,i,i]=>o, [i,i,i,i]=>i] => o"
   14.54 +    "relation4(M,is_f,f) ==
   14.55         \<forall>u[M]. \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>a[M]. is_f(u,x,y,z,a) <-> a = f(u,x,y,z)"
   14.56  
   14.57  
   14.58  text{*Useful when absoluteness reasoning has replaced the predicates by terms*}
   14.59 -lemma triv_Relativize1:
   14.60 -     "Relativize1(M, A, \<lambda>x y. y = f(x), f)"
   14.61 -by (simp add: Relativize1_def)
   14.62 +lemma triv_Relation1:
   14.63 +     "Relation1(M, A, \<lambda>x y. y = f(x), f)"
   14.64 +by (simp add: Relation1_def)
   14.65  
   14.66 -lemma triv_Relativize2:
   14.67 -     "Relativize2(M, A, B, \<lambda>x y a. a = f(x,y), f)"
   14.68 -by (simp add: Relativize2_def)
   14.69 +lemma triv_Relation2:
   14.70 +     "Relation2(M, A, B, \<lambda>x y a. a = f(x,y), f)"
   14.71 +by (simp add: Relation2_def)
   14.72  
   14.73  
   14.74  subsection {*The relativized ZF axioms*}
   14.75 @@ -730,9 +729,9 @@
   14.76  
   14.77  lemma (in M_trivial) lambda_abs2 [simp]:
   14.78       "[| strong_replacement(M, \<lambda>x y. x\<in>A & y = \<langle>x, b(x)\<rangle>);
   14.79 -         Relativize1(M,A,is_b,b); M(A); \<forall>m[M]. m\<in>A --> M(b(m)); M(z) |]
   14.80 +         Relation1(M,A,is_b,b); M(A); \<forall>m[M]. m\<in>A --> M(b(m)); M(z) |]
   14.81        ==> is_lambda(M,A,is_b,z) <-> z = Lambda(A,b)"
   14.82 -apply (simp add: Relativize1_def is_lambda_def)
   14.83 +apply (simp add: Relation1_def is_lambda_def)
   14.84  apply (rule iffI)
   14.85   prefer 2 apply (simp add: lam_def)
   14.86  apply (rule M_equalityI)
   14.87 @@ -787,7 +786,7 @@
   14.88  by (auto simp add: is_quasinat_def quasinat_def)
   14.89  
   14.90  lemma (in M_trivial) nat_case_abs [simp]:
   14.91 -     "[| relativize1(M,is_b,b); M(k); M(z) |]
   14.92 +     "[| relation1(M,is_b,b); M(k); M(z) |]
   14.93        ==> is_nat_case(M,a,is_b,k,z) <-> z = nat_case(a,b,k)"
   14.94  apply (case_tac "quasinat(k)")
   14.95   prefer 2
   14.96 @@ -795,7 +794,7 @@
   14.97   apply (force simp add: quasinat_def)
   14.98  apply (simp add: quasinat_def is_nat_case_def)
   14.99  apply (elim disjE exE)
  14.100 - apply (simp_all add: relativize1_def)
  14.101 + apply (simp_all add: relation1_def)
  14.102  done
  14.103  
  14.104  (*NOT for the simplifier.  The assumption M(z') is apparently necessary, but
  14.105 @@ -929,30 +928,8 @@
  14.106        strong_replacement(M, \<lambda>p z. \<exists>f[M]. \<exists>b[M]. \<exists>nb[M]. \<exists>cnbf[M].
  14.107                  pair(M,f,b,p) & pair(M,n,b,nb) & is_cons(M,nb,f,cnbf) &
  14.108                  upair(M,cnbf,cnbf,z))"
  14.109 -  and well_ord_iso_separation:
  14.110 -     "[| M(A); M(f); M(r) |]
  14.111 -      ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y[M]. (\<exists>p[M].
  14.112 -		     fun_apply(M,f,x,y) & pair(M,y,x,p) & p \<in> r)))"
  14.113 -  and obase_separation:
  14.114 -     --{*part of the order type formalization*}
  14.115 -     "[| M(A); M(r) |]
  14.116 -      ==> separation(M, \<lambda>a. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M].
  14.117 -	     ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
  14.118 -	     order_isomorphism(M,par,r,x,mx,g))"
  14.119 -  and obase_equals_separation:
  14.120 -     "[| M(A); M(r) |]
  14.121 -      ==> separation (M, \<lambda>x. x\<in>A --> ~(\<exists>y[M]. \<exists>g[M].
  14.122 -			      ordinal(M,y) & (\<exists>my[M]. \<exists>pxr[M].
  14.123 -			      membership(M,y,my) & pred_set(M,A,x,r,pxr) &
  14.124 -			      order_isomorphism(M,pxr,r,y,my,g))))"
  14.125 -  and omap_replacement:
  14.126 -     "[| M(A); M(r) |]
  14.127 -      ==> strong_replacement(M,
  14.128 -             \<lambda>a z. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M].
  14.129 -	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) &
  14.130 -	     pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
  14.131    and is_recfun_separation:
  14.132 -     --{*for well-founded recursion*}
  14.133 +     --{*for well-founded recursion: used to prove @{text is_recfun_equal}*}
  14.134       "[| M(r); M(f); M(g); M(a); M(b) |]
  14.135       ==> separation(M,
  14.136              \<lambda>x. \<exists>xa[M]. \<exists>xb[M].
  14.137 @@ -1490,7 +1467,7 @@
  14.138  by (auto simp add: is_quasilist_def quasilist_def)
  14.139  
  14.140  lemma (in M_trivial) list_case_abs [simp]:
  14.141 -     "[| relativize2(M,is_b,b); M(k); M(z) |]
  14.142 +     "[| relation2(M,is_b,b); M(k); M(z) |]
  14.143        ==> is_list_case(M,a,is_b,k,z) <-> z = list_case'(a,b,k)"
  14.144  apply (case_tac "quasilist(k)")
  14.145   prefer 2
  14.146 @@ -1498,7 +1475,7 @@
  14.147   apply (force simp add: quasilist_def)
  14.148  apply (simp add: quasilist_def is_list_case_def)
  14.149  apply (elim disjE exE)
  14.150 - apply (simp_all add: relativize2_def)
  14.151 + apply (simp_all add: relation2_def)
  14.152  done
  14.153  
  14.154  
  14.155 @@ -1536,8 +1513,8 @@
  14.156  apply (elim disjE exE, auto)
  14.157  done
  14.158  
  14.159 -lemma (in M_trivial) relativize1_tl: "relativize1(M, is_tl(M), tl')"
  14.160 -by (simp add: relativize1_def)
  14.161 +lemma (in M_trivial) relation1_tl: "relation1(M, is_tl(M), tl')"
  14.162 +by (simp add: relation1_def)
  14.163  
  14.164  lemma hd'_Nil: "hd'([]) = 0"
  14.165  by (simp add: hd'_def)
    15.1 --- a/src/ZF/Constructible/Satisfies_absolute.thy	Tue Oct 08 14:09:18 2002 +0200
    15.2 +++ b/src/ZF/Constructible/Satisfies_absolute.thy	Wed Oct 09 11:07:13 2002 +0200
    15.3 @@ -1,7 +1,6 @@
    15.4  (*  Title:      ZF/Constructible/Satisfies_absolute.thy
    15.5 -    ID:         $Id$
    15.6 +    ID:  $Id$
    15.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    15.8 -    Copyright   2002  University of Cambridge
    15.9  *)
   15.10  
   15.11  header {*Absoluteness for the Satisfies Relation on Formulas*}
   15.12 @@ -367,9 +366,9 @@
   15.13  done
   15.14  
   15.15  lemma (in M_satisfies) a_rel:
   15.16 -     "M(A) ==> Relativize2(M, nat, nat, satisfies_is_a(M,A), satisfies_a(A))"
   15.17 -apply (simp add: Relativize2_def satisfies_is_a_def satisfies_a_def)
   15.18 -apply (simp add: lambda_abs2 [OF Member_replacement'] Relativize1_def)
   15.19 +     "M(A) ==> Relation2(M, nat, nat, satisfies_is_a(M,A), satisfies_a(A))"
   15.20 +apply (simp add: Relation2_def satisfies_is_a_def satisfies_a_def)
   15.21 +apply (simp add: lambda_abs2 [OF Member_replacement'] Relation1_def)
   15.22  done
   15.23  
   15.24  lemma (in M_satisfies) b_closed:
   15.25 @@ -379,9 +378,9 @@
   15.26  done
   15.27  
   15.28  lemma (in M_satisfies) b_rel:
   15.29 -     "M(A) ==> Relativize2(M, nat, nat, satisfies_is_b(M,A), satisfies_b(A))"
   15.30 -apply (simp add: Relativize2_def satisfies_is_b_def satisfies_b_def)
   15.31 -apply (simp add: lambda_abs2 [OF Equal_replacement'] Relativize1_def)
   15.32 +     "M(A) ==> Relation2(M, nat, nat, satisfies_is_b(M,A), satisfies_b(A))"
   15.33 +apply (simp add: Relation2_def satisfies_is_b_def satisfies_b_def)
   15.34 +apply (simp add: lambda_abs2 [OF Equal_replacement'] Relation1_def)
   15.35  done
   15.36  
   15.37  lemma (in M_satisfies) c_closed:
   15.38 @@ -395,12 +394,12 @@
   15.39  
   15.40  lemma (in M_satisfies) c_rel:
   15.41   "[|M(A); M(f)|] ==> 
   15.42 -  Relativize2 (M, formula, formula, 
   15.43 +  Relation2 (M, formula, formula, 
   15.44                 satisfies_is_c(M,A,f),
   15.45  	       \<lambda>u v. satisfies_c(A, u, v, f ` succ(depth(u)) ` u, 
   15.46  					  f ` succ(depth(v)) ` v))"
   15.47 -apply (simp add: Relativize2_def satisfies_is_c_def satisfies_c_def)
   15.48 -apply (simp add: lambda_abs2 [OF Nand_replacement' triv_Relativize1] 
   15.49 +apply (simp add: Relation2_def satisfies_is_c_def satisfies_c_def)
   15.50 +apply (simp add: lambda_abs2 [OF Nand_replacement' triv_Relation1] 
   15.51                   formula_into_M)
   15.52  done
   15.53  
   15.54 @@ -414,11 +413,11 @@
   15.55  
   15.56  lemma (in M_satisfies) d_rel:
   15.57   "[|M(A); M(f)|] ==> 
   15.58 -  Relativize1(M, formula, satisfies_is_d(M,A,f), 
   15.59 +  Relation1(M, formula, satisfies_is_d(M,A,f), 
   15.60       \<lambda>u. satisfies_d(A, u, f ` succ(depth(u)) ` u))"
   15.61  apply (simp del: rall_abs 
   15.62 -            add: Relativize1_def satisfies_is_d_def satisfies_d_def)
   15.63 -apply (simp add: lambda_abs2 [OF Forall_replacement' triv_Relativize1] 
   15.64 +            add: Relation1_def satisfies_is_d_def satisfies_d_def)
   15.65 +apply (simp add: lambda_abs2 [OF Forall_replacement' triv_Relation1] 
   15.66                   formula_into_M)
   15.67  done
   15.68  
    16.1 --- a/src/ZF/Constructible/Separation.thy	Tue Oct 08 14:09:18 2002 +0200
    16.2 +++ b/src/ZF/Constructible/Separation.thy	Wed Oct 09 11:07:13 2002 +0200
    16.3 @@ -1,7 +1,6 @@
    16.4  (*  Title:      ZF/Constructible/Separation.thy
    16.5      ID:         $Id$
    16.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    16.7 -    Copyright   2002  University of Cambridge
    16.8  *)
    16.9  
   16.10  header{*Early Instances of Separation and Strong Replacement*}
   16.11 @@ -270,113 +269,7 @@
   16.12  done
   16.13  
   16.14  
   16.15 -subsection{*Separation for Order-Isomorphisms*}
   16.16 -
   16.17 -lemma well_ord_iso_Reflects:
   16.18 -  "REFLECTS[\<lambda>x. x\<in>A -->
   16.19 -                (\<exists>y[L]. \<exists>p[L]. fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r),
   16.20 -        \<lambda>i x. x\<in>A --> (\<exists>y \<in> Lset(i). \<exists>p \<in> Lset(i).
   16.21 -                fun_apply(**Lset(i),f,x,y) & pair(**Lset(i),y,x,p) & p \<in> r)]"
   16.22 -by (intro FOL_reflections function_reflections)
   16.23 -
   16.24 -lemma well_ord_iso_separation:
   16.25 -     "[| L(A); L(f); L(r) |]
   16.26 -      ==> separation (L, \<lambda>x. x\<in>A --> (\<exists>y[L]. (\<exists>p[L].
   16.27 -                     fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r)))"
   16.28 -apply (rule gen_separation [OF well_ord_iso_Reflects, of "{A,f,r}"], simp)
   16.29 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   16.30 -apply (rule DPow_LsetI)
   16.31 -apply (rule imp_iff_sats)
   16.32 -apply (rule_tac env = "[x,A,f,r]" in mem_iff_sats)
   16.33 -apply (rule sep_rules | simp)+
   16.34 -done
   16.35 -
   16.36 -
   16.37 -subsection{*Separation for @{term "obase"}*}
   16.38 -
   16.39 -lemma obase_reflects:
   16.40 -  "REFLECTS[\<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
   16.41 -             ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
   16.42 -             order_isomorphism(L,par,r,x,mx,g),
   16.43 -        \<lambda>i a. \<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i). \<exists>par \<in> Lset(i).
   16.44 -             ordinal(**Lset(i),x) & membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) &
   16.45 -             order_isomorphism(**Lset(i),par,r,x,mx,g)]"
   16.46 -by (intro FOL_reflections function_reflections fun_plus_reflections)
   16.47 -
   16.48 -lemma obase_separation:
   16.49 -     --{*part of the order type formalization*}
   16.50 -     "[| L(A); L(r) |]
   16.51 -      ==> separation(L, \<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
   16.52 -             ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
   16.53 -             order_isomorphism(L,par,r,x,mx,g))"
   16.54 -apply (rule gen_separation [OF obase_reflects, of "{A,r}"], simp)
   16.55 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   16.56 -apply (rule DPow_LsetI)
   16.57 -apply (rule bex_iff_sats conj_iff_sats)+
   16.58 -apply (rule_tac env = "[x,a,A,r]" in ordinal_iff_sats)
   16.59 -apply (rule sep_rules | simp)+
   16.60 -done
   16.61 -
   16.62 -
   16.63 -subsection{*Separation for a Theorem about @{term "obase"}*}
   16.64 -
   16.65 -lemma obase_equals_reflects:
   16.66 -  "REFLECTS[\<lambda>x. x\<in>A --> ~(\<exists>y[L]. \<exists>g[L].
   16.67 -                ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L].
   16.68 -                membership(L,y,my) & pred_set(L,A,x,r,pxr) &
   16.69 -                order_isomorphism(L,pxr,r,y,my,g))),
   16.70 -        \<lambda>i x. x\<in>A --> ~(\<exists>y \<in> Lset(i). \<exists>g \<in> Lset(i).
   16.71 -                ordinal(**Lset(i),y) & (\<exists>my \<in> Lset(i). \<exists>pxr \<in> Lset(i).
   16.72 -                membership(**Lset(i),y,my) & pred_set(**Lset(i),A,x,r,pxr) &
   16.73 -                order_isomorphism(**Lset(i),pxr,r,y,my,g)))]"
   16.74 -by (intro FOL_reflections function_reflections fun_plus_reflections)
   16.75 -
   16.76 -lemma obase_equals_separation:
   16.77 -     "[| L(A); L(r) |]
   16.78 -      ==> separation (L, \<lambda>x. x\<in>A --> ~(\<exists>y[L]. \<exists>g[L].
   16.79 -                              ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L].
   16.80 -                              membership(L,y,my) & pred_set(L,A,x,r,pxr) &
   16.81 -                              order_isomorphism(L,pxr,r,y,my,g))))"
   16.82 -apply (rule gen_separation [OF obase_equals_reflects, of "{A,r}"], simp)
   16.83 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
   16.84 -apply (rule DPow_LsetI)
   16.85 -apply (rule imp_iff_sats ball_iff_sats disj_iff_sats not_iff_sats)+
   16.86 -apply (rule_tac env = "[x,A,r]" in mem_iff_sats)
   16.87 -apply (rule sep_rules | simp)+
   16.88 -done
   16.89 -
   16.90 -
   16.91 -subsection{*Replacement for @{term "omap"}*}
   16.92 -
   16.93 -lemma omap_reflects:
   16.94 - "REFLECTS[\<lambda>z. \<exists>a[L]. a\<in>B & (\<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
   16.95 -     ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) &
   16.96 -     pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g)),
   16.97 - \<lambda>i z. \<exists>a \<in> Lset(i). a\<in>B & (\<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i).
   16.98 -        \<exists>par \<in> Lset(i).
   16.99 -         ordinal(**Lset(i),x) & pair(**Lset(i),a,x,z) &
  16.100 -         membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) &
  16.101 -         order_isomorphism(**Lset(i),par,r,x,mx,g))]"
  16.102 -by (intro FOL_reflections function_reflections fun_plus_reflections)
  16.103 -
  16.104 -lemma omap_replacement:
  16.105 -     "[| L(A); L(r) |]
  16.106 -      ==> strong_replacement(L,
  16.107 -             \<lambda>a z. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
  16.108 -             ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) &
  16.109 -             pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g))"
  16.110 -apply (rule strong_replacementI)
  16.111 -apply (rename_tac B)
  16.112 -apply (rule_tac u="{A,r,B}" in gen_separation [OF omap_reflects], simp)
  16.113 -apply (drule mem_Lset_imp_subset_Lset, clarsimp)
  16.114 -apply (rule DPow_LsetI)
  16.115 -apply (rule bex_iff_sats conj_iff_sats)+
  16.116 -apply (rule_tac env = "[a,z,A,B,r]" in mem_iff_sats)
  16.117 -apply (rule sep_rules | simp)+
  16.118 -done
  16.119 -
  16.120 -
  16.121 -subsection{*Separation for a Theorem about @{term "obase"}*}
  16.122 +subsection{*Separation for a Theorem about @{term "is_recfun"}*}
  16.123  
  16.124  lemma is_recfun_reflects:
  16.125    "REFLECTS[\<lambda>x. \<exists>xa[L]. \<exists>xb[L].
  16.126 @@ -416,9 +309,7 @@
  16.127  	 Inter_separation Diff_separation cartprod_separation image_separation
  16.128  	 converse_separation restrict_separation
  16.129  	 comp_separation pred_separation Memrel_separation
  16.130 -	 funspace_succ_replacement well_ord_iso_separation
  16.131 -	 obase_separation obase_equals_separation
  16.132 -	 omap_replacement is_recfun_separation)+
  16.133 +	 funspace_succ_replacement is_recfun_separation)+
  16.134    done
  16.135  
  16.136  theorem M_basic_L: "PROP M_basic(L)"
  16.137 @@ -469,7 +360,6 @@
  16.138    and is_recfun_relativize = M_basic.is_recfun_relativize [OF M_basic_L]
  16.139    and is_recfun_restrict = M_basic.is_recfun_restrict [OF M_basic_L]
  16.140    and univalent_is_recfun = M_basic.univalent_is_recfun [OF M_basic_L]
  16.141 -  and exists_is_recfun_indstep = M_basic.exists_is_recfun_indstep [OF M_basic_L]
  16.142    and wellfounded_exists_is_recfun = M_basic.wellfounded_exists_is_recfun [OF M_basic_L]
  16.143    and wf_exists_is_recfun = M_basic.wf_exists_is_recfun [OF M_basic_L]
  16.144    and is_recfun_abs = M_basic.is_recfun_abs [OF M_basic_L]
  16.145 @@ -499,34 +389,8 @@
  16.146    and membership_abs = M_basic.membership_abs [OF M_basic_L]
  16.147    and M_Memrel_iff = M_basic.M_Memrel_iff [OF M_basic_L]
  16.148    and Memrel_closed = M_basic.Memrel_closed [OF M_basic_L]
  16.149 -  and wellordered_iso_predD = M_basic.wellordered_iso_predD [OF M_basic_L]
  16.150 -  and wellordered_iso_pred_eq = M_basic.wellordered_iso_pred_eq [OF M_basic_L]
  16.151    and wellfounded_on_asym = M_basic.wellfounded_on_asym [OF M_basic_L]
  16.152    and wellordered_asym = M_basic.wellordered_asym [OF M_basic_L]
  16.153 -  and ord_iso_pred_imp_lt = M_basic.ord_iso_pred_imp_lt [OF M_basic_L]
  16.154 -  and obase_iff = M_basic.obase_iff [OF M_basic_L]
  16.155 -  and omap_iff = M_basic.omap_iff [OF M_basic_L]
  16.156 -  and omap_unique = M_basic.omap_unique [OF M_basic_L]
  16.157 -  and omap_yields_Ord = M_basic.omap_yields_Ord [OF M_basic_L]
  16.158 -  and otype_iff = M_basic.otype_iff [OF M_basic_L]
  16.159 -  and otype_eq_range = M_basic.otype_eq_range [OF M_basic_L]
  16.160 -  and Ord_otype = M_basic.Ord_otype [OF M_basic_L]
  16.161 -  and domain_omap = M_basic.domain_omap [OF M_basic_L]
  16.162 -  and omap_subset = M_basic.omap_subset [OF M_basic_L]
  16.163 -  and omap_funtype = M_basic.omap_funtype [OF M_basic_L]
  16.164 -  and wellordered_omap_bij = M_basic.wellordered_omap_bij [OF M_basic_L]
  16.165 -  and omap_ord_iso = M_basic.omap_ord_iso [OF M_basic_L]
  16.166 -  and Ord_omap_image_pred = M_basic.Ord_omap_image_pred [OF M_basic_L]
  16.167 -  and restrict_omap_ord_iso = M_basic.restrict_omap_ord_iso [OF M_basic_L]
  16.168 -  and obase_equals = M_basic.obase_equals [OF M_basic_L]
  16.169 -  and omap_ord_iso_otype = M_basic.omap_ord_iso_otype [OF M_basic_L]
  16.170 -  and obase_exists = M_basic.obase_exists [OF M_basic_L]
  16.171 -  and omap_exists = M_basic.omap_exists [OF M_basic_L]
  16.172 -  and otype_exists = M_basic.otype_exists [OF M_basic_L]
  16.173 -  and omap_ord_iso_otype' = M_basic.omap_ord_iso_otype' [OF M_basic_L]
  16.174 -  and ordertype_exists = M_basic.ordertype_exists [OF M_basic_L]
  16.175 -  and relativized_imp_well_ord = M_basic.relativized_imp_well_ord [OF M_basic_L]
  16.176 -  and well_ord_abs = M_basic.well_ord_abs [OF M_basic_L]
  16.177  
  16.178  declare cartprod_closed [intro, simp]
  16.179  declare sum_closed [intro, simp]
    17.1 --- a/src/ZF/Constructible/WF_absolute.thy	Tue Oct 08 14:09:18 2002 +0200
    17.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Wed Oct 09 11:07:13 2002 +0200
    17.3 @@ -1,68 +1,12 @@
    17.4  (*  Title:      ZF/Constructible/WF_absolute.thy
    17.5      ID:         $Id$
    17.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    17.7 -    Copyright   2002  University of Cambridge
    17.8  *)
    17.9  
   17.10  header {*Absoluteness for Well-Founded Relations and Well-Founded Recursion*}
   17.11  
   17.12  theory WF_absolute = WFrec:
   17.13  
   17.14 -subsection{*Every well-founded relation is a subset of some inverse image of
   17.15 -      an ordinal*}
   17.16 -
   17.17 -lemma wf_rvimage_Ord: "Ord(i) \<Longrightarrow> wf(rvimage(A, f, Memrel(i)))"
   17.18 -by (blast intro: wf_rvimage wf_Memrel)
   17.19 -
   17.20 -
   17.21 -constdefs
   17.22 -  wfrank :: "[i,i]=>i"
   17.23 -    "wfrank(r,a) == wfrec(r, a, %x f. \<Union>y \<in> r-``{x}. succ(f`y))"
   17.24 -
   17.25 -constdefs
   17.26 -  wftype :: "i=>i"
   17.27 -    "wftype(r) == \<Union>y \<in> range(r). succ(wfrank(r,y))"
   17.28 -
   17.29 -lemma wfrank: "wf(r) ==> wfrank(r,a) = (\<Union>y \<in> r-``{a}. succ(wfrank(r,y)))"
   17.30 -by (subst wfrank_def [THEN def_wfrec], simp_all)
   17.31 -
   17.32 -lemma Ord_wfrank: "wf(r) ==> Ord(wfrank(r,a))"
   17.33 -apply (rule_tac a=a in wf_induct, assumption)
   17.34 -apply (subst wfrank, assumption)
   17.35 -apply (rule Ord_succ [THEN Ord_UN], blast)
   17.36 -done
   17.37 -
   17.38 -lemma wfrank_lt: "[|wf(r); <a,b> \<in> r|] ==> wfrank(r,a) < wfrank(r,b)"
   17.39 -apply (rule_tac a1 = b in wfrank [THEN ssubst], assumption)
   17.40 -apply (rule UN_I [THEN ltI])
   17.41 -apply (simp add: Ord_wfrank vimage_iff)+
   17.42 -done
   17.43 -
   17.44 -lemma Ord_wftype: "wf(r) ==> Ord(wftype(r))"
   17.45 -by (simp add: wftype_def Ord_wfrank)
   17.46 -
   17.47 -lemma wftypeI: "\<lbrakk>wf(r);  x \<in> field(r)\<rbrakk> \<Longrightarrow> wfrank(r,x) \<in> wftype(r)"
   17.48 -apply (simp add: wftype_def)
   17.49 -apply (blast intro: wfrank_lt [THEN ltD])
   17.50 -done
   17.51 -
   17.52 -
   17.53 -lemma wf_imp_subset_rvimage:
   17.54 -     "[|wf(r); r \<subseteq> A*A|] ==> \<exists>i f. Ord(i) & r <= rvimage(A, f, Memrel(i))"
   17.55 -apply (rule_tac x="wftype(r)" in exI)
   17.56 -apply (rule_tac x="\<lambda>x\<in>A. wfrank(r,x)" in exI)
   17.57 -apply (simp add: Ord_wftype, clarify)
   17.58 -apply (frule subsetD, assumption, clarify)
   17.59 -apply (simp add: rvimage_iff wfrank_lt [THEN ltD])
   17.60 -apply (blast intro: wftypeI)
   17.61 -done
   17.62 -
   17.63 -theorem wf_iff_subset_rvimage:
   17.64 -  "relation(r) ==> wf(r) <-> (\<exists>i f A. Ord(i) & r <= rvimage(A, f, Memrel(i)))"
   17.65 -by (blast dest!: relation_field_times_field wf_imp_subset_rvimage
   17.66 -          intro: wf_rvimage_Ord [THEN wf_subset])
   17.67 -
   17.68 -
   17.69  subsection{*Transitive closure without fixedpoints*}
   17.70  
   17.71  constdefs
   17.72 @@ -236,271 +180,6 @@
   17.73  rank function.*}
   17.74  
   17.75  
   17.76 -locale M_wfrank = M_trancl +
   17.77 -  assumes wfrank_separation:
   17.78 -     "M(r) ==>
   17.79 -      separation (M, \<lambda>x. 
   17.80 -         \<forall>rplus[M]. tran_closure(M,r,rplus) -->
   17.81 -         ~ (\<exists>f[M]. M_is_recfun(M, %x f y. is_range(M,f,y), rplus, x, f)))"
   17.82 - and wfrank_strong_replacement:
   17.83 -     "M(r) ==>
   17.84 -      strong_replacement(M, \<lambda>x z. 
   17.85 -         \<forall>rplus[M]. tran_closure(M,r,rplus) -->
   17.86 -         (\<exists>y[M]. \<exists>f[M]. pair(M,x,y,z)  & 
   17.87 -                        M_is_recfun(M, %x f y. is_range(M,f,y), rplus, x, f) &
   17.88 -                        is_range(M,f,y)))"
   17.89 - and Ord_wfrank_separation:
   17.90 -     "M(r) ==>
   17.91 -      separation (M, \<lambda>x.
   17.92 -         \<forall>rplus[M]. tran_closure(M,r,rplus) --> 
   17.93 -          ~ (\<forall>f[M]. \<forall>rangef[M]. 
   17.94 -             is_range(M,f,rangef) -->
   17.95 -             M_is_recfun(M, \<lambda>x f y. is_range(M,f,y), rplus, x, f) -->
   17.96 -             ordinal(M,rangef)))" 
   17.97 -
   17.98 -text{*Proving that the relativized instances of Separation or Replacement
   17.99 -agree with the "real" ones.*}
  17.100 -
  17.101 -lemma (in M_wfrank) wfrank_separation':
  17.102 -     "M(r) ==>
  17.103 -      separation
  17.104 -	   (M, \<lambda>x. ~ (\<exists>f[M]. is_recfun(r^+, x, %x f. range(f), f)))"
  17.105 -apply (insert wfrank_separation [of r])
  17.106 -apply (simp add: relativize2_def is_recfun_abs [of "%x. range"])
  17.107 -done
  17.108 -
  17.109 -lemma (in M_wfrank) wfrank_strong_replacement':
  17.110 -     "M(r) ==>
  17.111 -      strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>f[M]. 
  17.112 -		  pair(M,x,y,z) & is_recfun(r^+, x, %x f. range(f), f) &
  17.113 -		  y = range(f))"
  17.114 -apply (insert wfrank_strong_replacement [of r])
  17.115 -apply (simp add: relativize2_def is_recfun_abs [of "%x. range"])
  17.116 -done
  17.117 -
  17.118 -lemma (in M_wfrank) Ord_wfrank_separation':
  17.119 -     "M(r) ==>
  17.120 -      separation (M, \<lambda>x. 
  17.121 -         ~ (\<forall>f[M]. is_recfun(r^+, x, \<lambda>x. range, f) --> Ord(range(f))))" 
  17.122 -apply (insert Ord_wfrank_separation [of r])
  17.123 -apply (simp add: relativize2_def is_recfun_abs [of "%x. range"])
  17.124 -done
  17.125 -
  17.126 -text{*This function, defined using replacement, is a rank function for
  17.127 -well-founded relations within the class M.*}
  17.128 -constdefs
  17.129 - wellfoundedrank :: "[i=>o,i,i] => i"
  17.130 -    "wellfoundedrank(M,r,A) ==
  17.131 -        {p. x\<in>A, \<exists>y[M]. \<exists>f[M]. 
  17.132 -                       p = <x,y> & is_recfun(r^+, x, %x f. range(f), f) &
  17.133 -                       y = range(f)}"
  17.134 -
  17.135 -lemma (in M_wfrank) exists_wfrank:
  17.136 -    "[| wellfounded(M,r); M(a); M(r) |]
  17.137 -     ==> \<exists>f[M]. is_recfun(r^+, a, %x f. range(f), f)"
  17.138 -apply (rule wellfounded_exists_is_recfun)
  17.139 -      apply (blast intro: wellfounded_trancl)
  17.140 -     apply (rule trans_trancl)
  17.141 -    apply (erule wfrank_separation')
  17.142 -   apply (erule wfrank_strong_replacement')
  17.143 -apply (simp_all add: trancl_subset_times)
  17.144 -done
  17.145 -
  17.146 -lemma (in M_wfrank) M_wellfoundedrank:
  17.147 -    "[| wellfounded(M,r); M(r); M(A) |] ==> M(wellfoundedrank(M,r,A))"
  17.148 -apply (insert wfrank_strong_replacement' [of r])
  17.149 -apply (simp add: wellfoundedrank_def)
  17.150 -apply (rule strong_replacement_closed)
  17.151 -   apply assumption+
  17.152 - apply (rule univalent_is_recfun)
  17.153 -   apply (blast intro: wellfounded_trancl)
  17.154 -  apply (rule trans_trancl)
  17.155 - apply (simp add: trancl_subset_times) 
  17.156 -apply (blast dest: transM) 
  17.157 -done
  17.158 -
  17.159 -lemma (in M_wfrank) Ord_wfrank_range [rule_format]:
  17.160 -    "[| wellfounded(M,r); a\<in>A; M(r); M(A) |]
  17.161 -     ==> \<forall>f[M]. is_recfun(r^+, a, %x f. range(f), f) --> Ord(range(f))"
  17.162 -apply (drule wellfounded_trancl, assumption)
  17.163 -apply (rule wellfounded_induct, assumption, erule (1) transM)
  17.164 -  apply simp
  17.165 - apply (blast intro: Ord_wfrank_separation', clarify)
  17.166 -txt{*The reasoning in both cases is that we get @{term y} such that
  17.167 -   @{term "\<langle>y, x\<rangle> \<in> r^+"}.  We find that
  17.168 -   @{term "f`y = restrict(f, r^+ -`` {y})"}. *}
  17.169 -apply (rule OrdI [OF _ Ord_is_Transset])
  17.170 - txt{*An ordinal is a transitive set...*}
  17.171 - apply (simp add: Transset_def)
  17.172 - apply clarify
  17.173 - apply (frule apply_recfun2, assumption)
  17.174 - apply (force simp add: restrict_iff)
  17.175 -txt{*...of ordinals.  This second case requires the induction hyp.*}
  17.176 -apply clarify
  17.177 -apply (rename_tac i y)
  17.178 -apply (frule apply_recfun2, assumption)
  17.179 -apply (frule is_recfun_imp_in_r, assumption)
  17.180 -apply (frule is_recfun_restrict)
  17.181 -    (*simp_all won't work*)
  17.182 -    apply (simp add: trans_trancl trancl_subset_times)+
  17.183 -apply (drule spec [THEN mp], assumption)
  17.184 -apply (subgoal_tac "M(restrict(f, r^+ -`` {y}))")
  17.185 - apply (drule_tac x="restrict(f, r^+ -`` {y})" in rspec)
  17.186 -apply assumption
  17.187 - apply (simp add: function_apply_equality [OF _ is_recfun_imp_function])
  17.188 -apply (blast dest: pair_components_in_M)
  17.189 -done
  17.190 -
  17.191 -lemma (in M_wfrank) Ord_range_wellfoundedrank:
  17.192 -    "[| wellfounded(M,r); r \<subseteq> A*A;  M(r); M(A) |]
  17.193 -     ==> Ord (range(wellfoundedrank(M,r,A)))"
  17.194 -apply (frule wellfounded_trancl, assumption)
  17.195 -apply (frule trancl_subset_times)
  17.196 -apply (simp add: wellfoundedrank_def)
  17.197 -apply (rule OrdI [OF _ Ord_is_Transset])
  17.198 - prefer 2
  17.199 - txt{*by our previous result the range consists of ordinals.*}
  17.200 - apply (blast intro: Ord_wfrank_range)
  17.201 -txt{*We still must show that the range is a transitive set.*}
  17.202 -apply (simp add: Transset_def, clarify, simp)
  17.203 -apply (rename_tac x i f u)
  17.204 -apply (frule is_recfun_imp_in_r, assumption)
  17.205 -apply (subgoal_tac "M(u) & M(i) & M(x)")
  17.206 - prefer 2 apply (blast dest: transM, clarify)
  17.207 -apply (rule_tac a=u in rangeI)
  17.208 -apply (rule_tac x=u in ReplaceI)
  17.209 -  apply simp 
  17.210 -  apply (rule_tac x="restrict(f, r^+ -`` {u})" in rexI)
  17.211 -   apply (blast intro: is_recfun_restrict trans_trancl dest: apply_recfun2)
  17.212 -  apply simp 
  17.213 -apply blast 
  17.214 -txt{*Unicity requirement of Replacement*}
  17.215 -apply clarify
  17.216 -apply (frule apply_recfun2, assumption)
  17.217 -apply (simp add: trans_trancl is_recfun_cut)
  17.218 -done
  17.219 -
  17.220 -lemma (in M_wfrank) function_wellfoundedrank:
  17.221 -    "[| wellfounded(M,r); M(r); M(A)|]
  17.222 -     ==> function(wellfoundedrank(M,r,A))"
  17.223 -apply (simp add: wellfoundedrank_def function_def, clarify)
  17.224 -txt{*Uniqueness: repeated below!*}
  17.225 -apply (drule is_recfun_functional, assumption)
  17.226 -     apply (blast intro: wellfounded_trancl)
  17.227 -    apply (simp_all add: trancl_subset_times trans_trancl)
  17.228 -done
  17.229 -
  17.230 -lemma (in M_wfrank) domain_wellfoundedrank:
  17.231 -    "[| wellfounded(M,r); M(r); M(A)|]
  17.232 -     ==> domain(wellfoundedrank(M,r,A)) = A"
  17.233 -apply (simp add: wellfoundedrank_def function_def)
  17.234 -apply (rule equalityI, auto)
  17.235 -apply (frule transM, assumption)
  17.236 -apply (frule_tac a=x in exists_wfrank, assumption+, clarify)
  17.237 -apply (rule_tac b="range(f)" in domainI)
  17.238 -apply (rule_tac x=x in ReplaceI)
  17.239 -  apply simp 
  17.240 -  apply (rule_tac x=f in rexI, blast, simp_all)
  17.241 -txt{*Uniqueness (for Replacement): repeated above!*}
  17.242 -apply clarify
  17.243 -apply (drule is_recfun_functional, assumption)
  17.244 -    apply (blast intro: wellfounded_trancl)
  17.245 -    apply (simp_all add: trancl_subset_times trans_trancl)
  17.246 -done
  17.247 -
  17.248 -lemma (in M_wfrank) wellfoundedrank_type:
  17.249 -    "[| wellfounded(M,r);  M(r); M(A)|]
  17.250 -     ==> wellfoundedrank(M,r,A) \<in> A -> range(wellfoundedrank(M,r,A))"
  17.251 -apply (frule function_wellfoundedrank [of r A], assumption+)
  17.252 -apply (frule function_imp_Pi)
  17.253 - apply (simp add: wellfoundedrank_def relation_def)
  17.254 - apply blast
  17.255 -apply (simp add: domain_wellfoundedrank)
  17.256 -done
  17.257 -
  17.258 -lemma (in M_wfrank) Ord_wellfoundedrank:
  17.259 -    "[| wellfounded(M,r); a \<in> A; r \<subseteq> A*A;  M(r); M(A) |]
  17.260 -     ==> Ord(wellfoundedrank(M,r,A) ` a)"
  17.261 -by (blast intro: apply_funtype [OF wellfoundedrank_type]
  17.262 -                 Ord_in_Ord [OF Ord_range_wellfoundedrank])
  17.263 -
  17.264 -lemma (in M_wfrank) wellfoundedrank_eq:
  17.265 -     "[| is_recfun(r^+, a, %x. range, f);
  17.266 -         wellfounded(M,r);  a \<in> A; M(f); M(r); M(A)|]
  17.267 -      ==> wellfoundedrank(M,r,A) ` a = range(f)"
  17.268 -apply (rule apply_equality)
  17.269 - prefer 2 apply (blast intro: wellfoundedrank_type)
  17.270 -apply (simp add: wellfoundedrank_def)
  17.271 -apply (rule ReplaceI)
  17.272 -  apply (rule_tac x="range(f)" in rexI) 
  17.273 -  apply blast
  17.274 - apply simp_all
  17.275 -txt{*Unicity requirement of Replacement*}
  17.276 -apply clarify
  17.277 -apply (drule is_recfun_functional, assumption)
  17.278 -    apply (blast intro: wellfounded_trancl)
  17.279 -    apply (simp_all add: trancl_subset_times trans_trancl)
  17.280 -done
  17.281 -
  17.282 -
  17.283 -lemma (in M_wfrank) wellfoundedrank_lt:
  17.284 -     "[| <a,b> \<in> r;
  17.285 -         wellfounded(M,r); r \<subseteq> A*A;  M(r); M(A)|]
  17.286 -      ==> wellfoundedrank(M,r,A) ` a < wellfoundedrank(M,r,A) ` b"
  17.287 -apply (frule wellfounded_trancl, assumption)
  17.288 -apply (subgoal_tac "a\<in>A & b\<in>A")
  17.289 - prefer 2 apply blast
  17.290 -apply (simp add: lt_def Ord_wellfoundedrank, clarify)
  17.291 -apply (frule exists_wfrank [of concl: _ b], erule (1) transM, assumption)
  17.292 -apply clarify
  17.293 -apply (rename_tac fb)
  17.294 -apply (frule is_recfun_restrict [of concl: "r^+" a])
  17.295 -    apply (rule trans_trancl, assumption)
  17.296 -   apply (simp_all add: r_into_trancl trancl_subset_times)
  17.297 -txt{*Still the same goal, but with new @{text is_recfun} assumptions.*}
  17.298 -apply (simp add: wellfoundedrank_eq)
  17.299 -apply (frule_tac a=a in wellfoundedrank_eq, assumption+)
  17.300 -   apply (simp_all add: transM [of a])
  17.301 -txt{*We have used equations for wellfoundedrank and now must use some
  17.302 -    for  @{text is_recfun}. *}
  17.303 -apply (rule_tac a=a in rangeI)
  17.304 -apply (simp add: is_recfun_type [THEN apply_iff] vimage_singleton_iff
  17.305 -                 r_into_trancl apply_recfun r_into_trancl)
  17.306 -done
  17.307 -
  17.308 -
  17.309 -lemma (in M_wfrank) wellfounded_imp_subset_rvimage:
  17.310 -     "[|wellfounded(M,r); r \<subseteq> A*A; M(r); M(A)|]
  17.311 -      ==> \<exists>i f. Ord(i) & r <= rvimage(A, f, Memrel(i))"
  17.312 -apply (rule_tac x="range(wellfoundedrank(M,r,A))" in exI)
  17.313 -apply (rule_tac x="wellfoundedrank(M,r,A)" in exI)
  17.314 -apply (simp add: Ord_range_wellfoundedrank, clarify)
  17.315 -apply (frule subsetD, assumption, clarify)
  17.316 -apply (simp add: rvimage_iff wellfoundedrank_lt [THEN ltD])
  17.317 -apply (blast intro: apply_rangeI wellfoundedrank_type)
  17.318 -done
  17.319 -
  17.320 -lemma (in M_wfrank) wellfounded_imp_wf:
  17.321 -     "[|wellfounded(M,r); relation(r); M(r)|] ==> wf(r)"
  17.322 -by (blast dest!: relation_field_times_field wellfounded_imp_subset_rvimage
  17.323 -          intro: wf_rvimage_Ord [THEN wf_subset])
  17.324 -
  17.325 -lemma (in M_wfrank) wellfounded_on_imp_wf_on:
  17.326 -     "[|wellfounded_on(M,A,r); relation(r); M(r); M(A)|] ==> wf[A](r)"
  17.327 -apply (simp add: wellfounded_on_iff_wellfounded wf_on_def)
  17.328 -apply (rule wellfounded_imp_wf)
  17.329 -apply (simp_all add: relation_def)
  17.330 -done
  17.331 -
  17.332 -
  17.333 -theorem (in M_wfrank) wf_abs [simp]:
  17.334 -     "[|relation(r); M(r)|] ==> wellfounded(M,r) <-> wf(r)"
  17.335 -by (blast intro: wellfounded_imp_wf wf_imp_relativized)
  17.336 -
  17.337 -theorem (in M_wfrank) wf_on_abs [simp]:
  17.338 -     "[|relation(r); M(r); M(A)|] ==> wellfounded_on(M,A,r) <-> wf[A](r)"
  17.339 -by (blast intro: wellfounded_on_imp_wf_on wf_on_imp_relativized)
  17.340 -
  17.341  
  17.342  text{*absoluteness for wfrec-defined functions.*}
  17.343  
  17.344 @@ -531,7 +210,7 @@
  17.345        before we can replace @{term "r^+"} by @{term r}. *}
  17.346  theorem (in M_trancl) trans_wfrec_relativize:
  17.347    "[|wf(r);  trans(r);  relation(r);  M(r);  M(a);
  17.348 -     wfrec_replacement(M,MH,r);  relativize2(M,MH,H);
  17.349 +     wfrec_replacement(M,MH,r);  relation2(M,MH,H);
  17.350       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
  17.351     ==> wfrec(r,a,H) = z <-> (\<exists>f[M]. is_recfun(r,a,H,f) & z = H(a,f))" 
  17.352  apply (frule wfrec_replacement', assumption+) 
  17.353 @@ -542,15 +221,15 @@
  17.354  
  17.355  theorem (in M_trancl) trans_wfrec_abs:
  17.356    "[|wf(r);  trans(r);  relation(r);  M(r);  M(a);  M(z);
  17.357 -     wfrec_replacement(M,MH,r);  relativize2(M,MH,H);
  17.358 +     wfrec_replacement(M,MH,r);  relation2(M,MH,H);
  17.359       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
  17.360     ==> is_wfrec(M,MH,r,a,z) <-> z=wfrec(r,a,H)" 
  17.361 -apply (simp add: trans_wfrec_relativize [THEN iff_sym] is_wfrec_abs, blast) 
  17.362 -done
  17.363 +by (simp add: trans_wfrec_relativize [THEN iff_sym] is_wfrec_abs, blast) 
  17.364 +
  17.365  
  17.366  lemma (in M_trancl) trans_eq_pair_wfrec_iff:
  17.367    "[|wf(r);  trans(r); relation(r); M(r);  M(y); 
  17.368 -     wfrec_replacement(M,MH,r);  relativize2(M,MH,H);
  17.369 +     wfrec_replacement(M,MH,r);  relation2(M,MH,H);
  17.370       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
  17.371     ==> y = <x, wfrec(r, x, H)> <-> 
  17.372         (\<exists>f[M]. is_recfun(r,x,H,f) & y = <x, H(x,f)>)"
  17.373 @@ -565,7 +244,7 @@
  17.374  subsection{*M is closed under well-founded recursion*}
  17.375  
  17.376  text{*Lemma with the awkward premise mentioning @{text wfrec}.*}
  17.377 -lemma (in M_wfrank) wfrec_closed_lemma [rule_format]:
  17.378 +lemma (in M_trancl) wfrec_closed_lemma [rule_format]:
  17.379       "[|wf(r); M(r); 
  17.380          strong_replacement(M, \<lambda>x y. y = \<langle>x, wfrec(r, x, H)\<rangle>);
  17.381          \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
  17.382 @@ -579,7 +258,7 @@
  17.383  done
  17.384  
  17.385  text{*Eliminates one instance of replacement.*}
  17.386 -lemma (in M_wfrank) wfrec_replacement_iff:
  17.387 +lemma (in M_trancl) wfrec_replacement_iff:
  17.388       "strong_replacement(M, \<lambda>x z. 
  17.389            \<exists>y[M]. pair(M,x,y,z) & (\<exists>g[M]. is_recfun(r,x,H,g) & y = H(x,g))) <->
  17.390        strong_replacement(M, 
  17.391 @@ -589,9 +268,9 @@
  17.392  done
  17.393  
  17.394  text{*Useful version for transitive relations*}
  17.395 -theorem (in M_wfrank) trans_wfrec_closed:
  17.396 +theorem (in M_trancl) trans_wfrec_closed:
  17.397       "[|wf(r); trans(r); relation(r); M(r); M(a);
  17.398 -       wfrec_replacement(M,MH,r);  relativize2(M,MH,H);
  17.399 +       wfrec_replacement(M,MH,r);  relation2(M,MH,H);
  17.400          \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
  17.401        ==> M(wfrec(r,a,H))"
  17.402  apply (frule wfrec_replacement', assumption+) 
  17.403 @@ -619,10 +298,10 @@
  17.404  done
  17.405  
  17.406  text{*Full version not assuming transitivity, but maybe not very useful.*}
  17.407 -theorem (in M_wfrank) wfrec_closed:
  17.408 +theorem (in M_trancl) wfrec_closed:
  17.409       "[|wf(r); M(r); M(a);
  17.410          wfrec_replacement(M,MH,r^+);  
  17.411 -        relativize2(M,MH, \<lambda>x f. H(x, restrict(f, r -`` {x})));
  17.412 +        relation2(M,MH, \<lambda>x f. H(x, restrict(f, r -`` {x})));
  17.413          \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
  17.414        ==> M(wfrec(r,a,H))"
  17.415  apply (frule wfrec_replacement' 
    18.1 --- a/src/ZF/Constructible/WFrec.thy	Tue Oct 08 14:09:18 2002 +0200
    18.2 +++ b/src/ZF/Constructible/WFrec.thy	Wed Oct 09 11:07:13 2002 +0200
    18.3 @@ -1,7 +1,6 @@
    18.4  (*  Title:      ZF/Constructible/WFrec.thy
    18.5      ID:         $Id$
    18.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    18.7 -    Copyright   2002  University of Cambridge
    18.8  *)
    18.9  
   18.10  header{*Relativized Well-Founded Recursion*}
   18.11 @@ -292,9 +291,9 @@
   18.12  
   18.13  lemma (in M_basic) is_recfun_abs:
   18.14       "[| \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g));  M(r); M(a); M(f); 
   18.15 -         relativize2(M,MH,H) |] 
   18.16 +         relation2(M,MH,H) |] 
   18.17        ==> M_is_recfun(M,MH,r,a,f) <-> is_recfun(r,a,H,f)"
   18.18 -apply (simp add: M_is_recfun_def relativize2_def is_recfun_relativize)
   18.19 +apply (simp add: M_is_recfun_def relation2_def is_recfun_relativize)
   18.20  apply (rule rall_cong)
   18.21  apply (blast dest: transM)
   18.22  done
   18.23 @@ -307,16 +306,16 @@
   18.24  
   18.25  lemma (in M_basic) is_wfrec_abs:
   18.26       "[| \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)); 
   18.27 -         relativize2(M,MH,H);  M(r); M(a); M(z) |]
   18.28 +         relation2(M,MH,H);  M(r); M(a); M(z) |]
   18.29        ==> is_wfrec(M,MH,r,a,z) <-> 
   18.30            (\<exists>g[M]. is_recfun(r,a,H,g) & z = H(a,g))"
   18.31 -by (simp add: is_wfrec_def relativize2_def is_recfun_abs)
   18.32 +by (simp add: is_wfrec_def relation2_def is_recfun_abs)
   18.33  
   18.34  text{*Relating @{term wfrec_replacement} to native constructs*}
   18.35  lemma (in M_basic) wfrec_replacement':
   18.36    "[|wfrec_replacement(M,MH,r);
   18.37       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)); 
   18.38 -     relativize2(M,MH,H);  M(r)|] 
   18.39 +     relation2(M,MH,H);  M(r)|] 
   18.40     ==> strong_replacement(M, \<lambda>x z. \<exists>y[M]. 
   18.41                  pair(M,x,y,z) & (\<exists>g[M]. is_recfun(r,x,H,g) & y = H(x,g)))"
   18.42  by (simp add: wfrec_replacement_def is_wfrec_abs) 
   18.43 @@ -329,259 +328,5 @@
   18.44  by (simp add: is_wfrec_def wfrec_replacement_def) 
   18.45  
   18.46  
   18.47 -subsection{*Ordinal Arithmetic: Two Examples of Recursion*}
   18.48 -
   18.49 -subsubsection{*Ordinal Addition*}
   18.50 -
   18.51 -(*FIXME: update to use new techniques!!*)
   18.52 -constdefs
   18.53 - (*This expresses ordinal addition in the language of ZF.  It also 
   18.54 -   provides an abbreviation that can be used in the instance of strong
   18.55 -   replacement below.  Here j is used to define the relation, namely
   18.56 -   Memrel(succ(j)), while x determines the domain of f.*)
   18.57 - is_oadd_fun :: "[i=>o,i,i,i,i] => o"
   18.58 -    "is_oadd_fun(M,i,j,x,f) == 
   18.59 -       (\<forall>sj msj. M(sj) --> M(msj) --> 
   18.60 -                 successor(M,j,sj) --> membership(M,sj,msj) --> 
   18.61 -	         M_is_recfun(M, 
   18.62 -		     %x g y. \<exists>gx[M]. image(M,g,x,gx) & union(M,i,gx,y),
   18.63 -		     msj, x, f))"
   18.64 -
   18.65 - is_oadd :: "[i=>o,i,i,i] => o"
   18.66 -    "is_oadd(M,i,j,k) == 
   18.67 -        (~ ordinal(M,i) & ~ ordinal(M,j) & k=0) |
   18.68 -        (~ ordinal(M,i) & ordinal(M,j) & k=j) |
   18.69 -        (ordinal(M,i) & ~ ordinal(M,j) & k=i) |
   18.70 -        (ordinal(M,i) & ordinal(M,j) & 
   18.71 -	 (\<exists>f fj sj. M(f) & M(fj) & M(sj) & 
   18.72 -		    successor(M,j,sj) & is_oadd_fun(M,i,sj,sj,f) & 
   18.73 -		    fun_apply(M,f,j,fj) & fj = k))"
   18.74 -
   18.75 - (*NEEDS RELATIVIZATION*)
   18.76 - omult_eqns :: "[i,i,i,i] => o"
   18.77 -    "omult_eqns(i,x,g,z) ==
   18.78 -            Ord(x) & 
   18.79 -	    (x=0 --> z=0) &
   18.80 -            (\<forall>j. x = succ(j) --> z = g`j ++ i) &
   18.81 -            (Limit(x) --> z = \<Union>(g``x))"
   18.82 -
   18.83 - is_omult_fun :: "[i=>o,i,i,i] => o"
   18.84 -    "is_omult_fun(M,i,j,f) == 
   18.85 -	    (\<exists>df. M(df) & is_function(M,f) & 
   18.86 -                  is_domain(M,f,df) & subset(M, j, df)) & 
   18.87 -            (\<forall>x\<in>j. omult_eqns(i,x,f,f`x))"
   18.88 -
   18.89 - is_omult :: "[i=>o,i,i,i] => o"
   18.90 -    "is_omult(M,i,j,k) == 
   18.91 -	\<exists>f fj sj. M(f) & M(fj) & M(sj) & 
   18.92 -                  successor(M,j,sj) & is_omult_fun(M,i,sj,f) & 
   18.93 -                  fun_apply(M,f,j,fj) & fj = k"
   18.94 -
   18.95 -
   18.96 -locale M_ord_arith = M_basic +
   18.97 -  assumes oadd_strong_replacement:
   18.98 -   "[| M(i); M(j) |] ==>
   18.99 -    strong_replacement(M, 
  18.100 -         \<lambda>x z. \<exists>y[M]. pair(M,x,y,z) & 
  18.101 -                  (\<exists>f[M]. \<exists>fx[M]. is_oadd_fun(M,i,j,x,f) & 
  18.102 -		           image(M,f,x,fx) & y = i Un fx))"
  18.103 -
  18.104 - and omult_strong_replacement':
  18.105 -   "[| M(i); M(j) |] ==>
  18.106 -    strong_replacement(M, 
  18.107 -         \<lambda>x z. \<exists>y[M]. z = <x,y> &
  18.108 -	     (\<exists>g[M]. is_recfun(Memrel(succ(j)),x,%x g. THE z. omult_eqns(i,x,g,z),g) & 
  18.109 -	     y = (THE z. omult_eqns(i, x, g, z))))" 
  18.110 -
  18.111 -
  18.112 -
  18.113 -text{*@{text is_oadd_fun}: Relating the pure "language of set theory" to Isabelle/ZF*}
  18.114 -lemma (in M_ord_arith) is_oadd_fun_iff:
  18.115 -   "[| a\<le>j; M(i); M(j); M(a); M(f) |] 
  18.116 -    ==> is_oadd_fun(M,i,j,a,f) <->
  18.117 -	f \<in> a \<rightarrow> range(f) & (\<forall>x. M(x) --> x < a --> f`x = i Un f``x)"
  18.118 -apply (frule lt_Ord) 
  18.119 -apply (simp add: is_oadd_fun_def Memrel_closed Un_closed 
  18.120 -             relativize2_def is_recfun_abs [of "%x g. i Un g``x"]
  18.121 -             image_closed is_recfun_iff_equation  
  18.122 -             Ball_def lt_trans [OF ltI, of _ a] lt_Memrel)
  18.123 -apply (simp add: lt_def) 
  18.124 -apply (blast dest: transM) 
  18.125 -done
  18.126 -
  18.127 -
  18.128 -lemma (in M_ord_arith) oadd_strong_replacement':
  18.129 -    "[| M(i); M(j) |] ==>
  18.130 -     strong_replacement(M, 
  18.131 -            \<lambda>x z. \<exists>y[M]. z = <x,y> &
  18.132 -		  (\<exists>g[M]. is_recfun(Memrel(succ(j)),x,%x g. i Un g``x,g) & 
  18.133 -		  y = i Un g``x))" 
  18.134 -apply (insert oadd_strong_replacement [of i j]) 
  18.135 -apply (simp add: is_oadd_fun_def relativize2_def is_recfun_abs [of "%x g. i Un g``x"])  
  18.136 -done
  18.137 -
  18.138 -
  18.139 -lemma (in M_ord_arith) exists_oadd:
  18.140 -    "[| Ord(j);  M(i);  M(j) |]
  18.141 -     ==> \<exists>f[M]. is_recfun(Memrel(succ(j)), j, %x g. i Un g``x, f)"
  18.142 -apply (rule wf_exists_is_recfun [OF wf_Memrel trans_Memrel])
  18.143 -    apply (simp_all add: Memrel_type oadd_strong_replacement') 
  18.144 -done 
  18.145 -
  18.146 -lemma (in M_ord_arith) exists_oadd_fun:
  18.147 -    "[| Ord(j);  M(i);  M(j) |] ==> \<exists>f[M]. is_oadd_fun(M,i,succ(j),succ(j),f)"
  18.148 -apply (rule exists_oadd [THEN rexE])
  18.149 -apply (erule Ord_succ, assumption, simp) 
  18.150 -apply (rename_tac f) 
  18.151 -apply (frule is_recfun_type)
  18.152 -apply (rule_tac x=f in rexI) 
  18.153 - apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def
  18.154 -                  is_oadd_fun_iff Ord_trans [OF _ succI1], assumption)
  18.155 -done
  18.156 -
  18.157 -lemma (in M_ord_arith) is_oadd_fun_apply:
  18.158 -    "[| x < j; M(i); M(j); M(f); is_oadd_fun(M,i,j,j,f) |] 
  18.159 -     ==> f`x = i Un (\<Union>k\<in>x. {f ` k})"
  18.160 -apply (simp add: is_oadd_fun_iff lt_Ord2, clarify) 
  18.161 -apply (frule lt_closed, simp)
  18.162 -apply (frule leI [THEN le_imp_subset])  
  18.163 -apply (simp add: image_fun, blast) 
  18.164 -done
  18.165 -
  18.166 -lemma (in M_ord_arith) is_oadd_fun_iff_oadd [rule_format]:
  18.167 -    "[| is_oadd_fun(M,i,J,J,f); M(i); M(J); M(f); Ord(i); Ord(j) |] 
  18.168 -     ==> j<J --> f`j = i++j"
  18.169 -apply (erule_tac i=j in trans_induct, clarify) 
  18.170 -apply (subgoal_tac "\<forall>k\<in>x. k<J")
  18.171 - apply (simp (no_asm_simp) add: is_oadd_def oadd_unfold is_oadd_fun_apply)
  18.172 -apply (blast intro: lt_trans ltI lt_Ord) 
  18.173 -done
  18.174 -
  18.175 -lemma (in M_ord_arith) Ord_oadd_abs:
  18.176 -    "[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_oadd(M,i,j,k) <-> k = i++j"
  18.177 -apply (simp add: is_oadd_def is_oadd_fun_iff_oadd)
  18.178 -apply (frule exists_oadd_fun [of j i], blast+)
  18.179 -done
  18.180 -
  18.181 -lemma (in M_ord_arith) oadd_abs:
  18.182 -    "[| M(i); M(j); M(k) |] ==> is_oadd(M,i,j,k) <-> k = i++j"
  18.183 -apply (case_tac "Ord(i) & Ord(j)")
  18.184 - apply (simp add: Ord_oadd_abs)
  18.185 -apply (auto simp add: is_oadd_def oadd_eq_if_raw_oadd)
  18.186 -done
  18.187 -
  18.188 -lemma (in M_ord_arith) oadd_closed [intro,simp]:
  18.189 -    "[| M(i); M(j) |] ==> M(i++j)"
  18.190 -apply (simp add: oadd_eq_if_raw_oadd, clarify) 
  18.191 -apply (simp add: raw_oadd_eq_oadd) 
  18.192 -apply (frule exists_oadd_fun [of j i], auto)
  18.193 -apply (simp add: apply_closed is_oadd_fun_iff_oadd [symmetric]) 
  18.194 -done
  18.195 -
  18.196 -
  18.197 -subsubsection{*Ordinal Multiplication*}
  18.198 -
  18.199 -lemma omult_eqns_unique:
  18.200 -     "[| omult_eqns(i,x,g,z); omult_eqns(i,x,g,z') |] ==> z=z'";
  18.201 -apply (simp add: omult_eqns_def, clarify) 
  18.202 -apply (erule Ord_cases, simp_all) 
  18.203 -done
  18.204 -
  18.205 -lemma omult_eqns_0: "omult_eqns(i,0,g,z) <-> z=0"
  18.206 -by (simp add: omult_eqns_def)
  18.207 -
  18.208 -lemma the_omult_eqns_0: "(THE z. omult_eqns(i,0,g,z)) = 0"
  18.209 -by (simp add: omult_eqns_0)
  18.210 -
  18.211 -lemma omult_eqns_succ: "omult_eqns(i,succ(j),g,z) <-> Ord(j) & z = g`j ++ i"
  18.212 -by (simp add: omult_eqns_def)
  18.213 -
  18.214 -lemma the_omult_eqns_succ:
  18.215 -     "Ord(j) ==> (THE z. omult_eqns(i,succ(j),g,z)) = g`j ++ i"
  18.216 -by (simp add: omult_eqns_succ) 
  18.217 -
  18.218 -lemma omult_eqns_Limit:
  18.219 -     "Limit(x) ==> omult_eqns(i,x,g,z) <-> z = \<Union>(g``x)"
  18.220 -apply (simp add: omult_eqns_def) 
  18.221 -apply (blast intro: Limit_is_Ord) 
  18.222 -done
  18.223 -
  18.224 -lemma the_omult_eqns_Limit:
  18.225 -     "Limit(x) ==> (THE z. omult_eqns(i,x,g,z)) = \<Union>(g``x)"
  18.226 -by (simp add: omult_eqns_Limit)
  18.227 -
  18.228 -lemma omult_eqns_Not: "~ Ord(x) ==> ~ omult_eqns(i,x,g,z)"
  18.229 -by (simp add: omult_eqns_def)
  18.230 -
  18.231 -
  18.232 -lemma (in M_ord_arith) the_omult_eqns_closed:
  18.233 -    "[| M(i); M(x); M(g); function(g) |] 
  18.234 -     ==> M(THE z. omult_eqns(i, x, g, z))"
  18.235 -apply (case_tac "Ord(x)")
  18.236 - prefer 2 apply (simp add: omult_eqns_Not) --{*trivial, non-Ord case*}
  18.237 -apply (erule Ord_cases) 
  18.238 -  apply (simp add: omult_eqns_0)
  18.239 - apply (simp add: omult_eqns_succ apply_closed oadd_closed) 
  18.240 -apply (simp add: omult_eqns_Limit) 
  18.241 -done
  18.242 -
  18.243 -lemma (in M_ord_arith) exists_omult:
  18.244 -    "[| Ord(j);  M(i);  M(j) |]
  18.245 -     ==> \<exists>f[M]. is_recfun(Memrel(succ(j)), j, %x g. THE z. omult_eqns(i,x,g,z), f)"
  18.246 -apply (rule wf_exists_is_recfun [OF wf_Memrel trans_Memrel])
  18.247 -    apply (simp_all add: Memrel_type omult_strong_replacement') 
  18.248 -apply (blast intro: the_omult_eqns_closed) 
  18.249 -done
  18.250 -
  18.251 -lemma (in M_ord_arith) exists_omult_fun:
  18.252 -    "[| Ord(j);  M(i);  M(j) |] ==> \<exists>f[M]. is_omult_fun(M,i,succ(j),f)"
  18.253 -apply (rule exists_omult [THEN rexE])
  18.254 -apply (erule Ord_succ, assumption, simp) 
  18.255 -apply (rename_tac f) 
  18.256 -apply (frule is_recfun_type)
  18.257 -apply (rule_tac x=f in rexI) 
  18.258 -apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def
  18.259 -                 is_omult_fun_def Ord_trans [OF _ succI1])
  18.260 - apply (force dest: Ord_in_Ord' 
  18.261 -              simp add: omult_eqns_def the_omult_eqns_0 the_omult_eqns_succ
  18.262 -                        the_omult_eqns_Limit, assumption)
  18.263 -done
  18.264 -
  18.265 -lemma (in M_ord_arith) is_omult_fun_apply_0:
  18.266 -    "[| 0 < j; is_omult_fun(M,i,j,f) |] ==> f`0 = 0"
  18.267 -by (simp add: is_omult_fun_def omult_eqns_def lt_def ball_conj_distrib)
  18.268 -
  18.269 -lemma (in M_ord_arith) is_omult_fun_apply_succ:
  18.270 -    "[| succ(x) < j; is_omult_fun(M,i,j,f) |] ==> f`succ(x) = f`x ++ i"
  18.271 -by (simp add: is_omult_fun_def omult_eqns_def lt_def, blast) 
  18.272 -
  18.273 -lemma (in M_ord_arith) is_omult_fun_apply_Limit:
  18.274 -    "[| x < j; Limit(x); M(j); M(f); is_omult_fun(M,i,j,f) |] 
  18.275 -     ==> f ` x = (\<Union>y\<in>x. f`y)"
  18.276 -apply (simp add: is_omult_fun_def omult_eqns_def domain_closed lt_def, clarify)
  18.277 -apply (drule subset_trans [OF OrdmemD], assumption+)  
  18.278 -apply (simp add: ball_conj_distrib omult_Limit image_function)
  18.279 -done
  18.280 -
  18.281 -lemma (in M_ord_arith) is_omult_fun_eq_omult:
  18.282 -    "[| is_omult_fun(M,i,J,f); M(J); M(f); Ord(i); Ord(j) |] 
  18.283 -     ==> j<J --> f`j = i**j"
  18.284 -apply (erule_tac i=j in trans_induct3)
  18.285 -apply (safe del: impCE)
  18.286 -  apply (simp add: is_omult_fun_apply_0) 
  18.287 - apply (subgoal_tac "x<J") 
  18.288 -  apply (simp add: is_omult_fun_apply_succ omult_succ)  
  18.289 - apply (blast intro: lt_trans) 
  18.290 -apply (subgoal_tac "\<forall>k\<in>x. k<J")
  18.291 - apply (simp add: is_omult_fun_apply_Limit omult_Limit) 
  18.292 -apply (blast intro: lt_trans ltI lt_Ord) 
  18.293 -done
  18.294 -
  18.295 -lemma (in M_ord_arith) omult_abs:
  18.296 -    "[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_omult(M,i,j,k) <-> k = i**j"
  18.297 -apply (simp add: is_omult_def is_omult_fun_eq_omult)
  18.298 -apply (frule exists_omult_fun [of j i], blast+)
  18.299 -done
  18.300 -
  18.301  end
  18.302  
    19.1 --- a/src/ZF/Constructible/Wellorderings.thy	Tue Oct 08 14:09:18 2002 +0200
    19.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Wed Oct 09 11:07:13 2002 +0200
    19.3 @@ -1,7 +1,6 @@
    19.4  (*  Title:      ZF/Constructible/Wellorderings.thy
    19.5      ID:         $Id$
    19.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    19.7 -    Copyright   2002  University of Cambridge
    19.8  *)
    19.9  
   19.10  header {*Relativized Wellorderings*}
   19.11 @@ -220,60 +219,6 @@
   19.12  		    wellfounded_on_subset)
   19.13  done
   19.14  
   19.15 -text{*Inductive argument for Kunen's Lemma 6.1, etc.
   19.16 -      Simple proof from Halmos, page 72*}
   19.17 -lemma  (in M_basic) wellordered_iso_subset_lemma: 
   19.18 -     "[| wellordered(M,A,r);  f \<in> ord_iso(A,r, A',r);  A'<= A;  y \<in> A;  
   19.19 -       M(A);  M(f);  M(r) |] ==> ~ <f`y, y> \<in> r"
   19.20 -apply (unfold wellordered_def ord_iso_def)
   19.21 -apply (elim conjE CollectE) 
   19.22 -apply (erule wellfounded_on_induct, assumption+)
   19.23 - apply (insert well_ord_iso_separation [of A f r])
   19.24 - apply (simp, clarify) 
   19.25 -apply (drule_tac a = x in bij_is_fun [THEN apply_type], assumption, blast)
   19.26 -done
   19.27 -
   19.28 -
   19.29 -text{*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment
   19.30 -      of a well-ordering*}
   19.31 -lemma (in M_basic) wellordered_iso_predD:
   19.32 -     "[| wellordered(M,A,r);  f \<in> ord_iso(A, r, Order.pred(A,x,r), r);  
   19.33 -       M(A);  M(f);  M(r) |] ==> x \<notin> A"
   19.34 -apply (rule notI) 
   19.35 -apply (frule wellordered_iso_subset_lemma, assumption)
   19.36 -apply (auto elim: predE)  
   19.37 -(*Now we know  ~ (f`x < x) *)
   19.38 -apply (drule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption)
   19.39 -(*Now we also know f`x  \<in> pred(A,x,r);  contradiction! *)
   19.40 -apply (simp add: Order.pred_def)
   19.41 -done
   19.42 -
   19.43 -
   19.44 -lemma (in M_basic) wellordered_iso_pred_eq_lemma:
   19.45 -     "[| f \<in> \<langle>Order.pred(A,y,r), r\<rangle> \<cong> \<langle>Order.pred(A,x,r), r\<rangle>;
   19.46 -       wellordered(M,A,r); x\<in>A; y\<in>A; M(A); M(f); M(r) |] ==> <x,y> \<notin> r"
   19.47 -apply (frule wellordered_is_trans_on, assumption)
   19.48 -apply (rule notI) 
   19.49 -apply (drule_tac x2=y and x=x and r2=r in 
   19.50 -         wellordered_subset [OF _ pred_subset, THEN wellordered_iso_predD]) 
   19.51 -apply (simp add: trans_pred_pred_eq) 
   19.52 -apply (blast intro: predI dest: transM)+
   19.53 -done
   19.54 -
   19.55 -
   19.56 -text{*Simple consequence of Lemma 6.1*}
   19.57 -lemma (in M_basic) wellordered_iso_pred_eq:
   19.58 -     "[| wellordered(M,A,r);
   19.59 -       f \<in> ord_iso(Order.pred(A,a,r), r, Order.pred(A,c,r), r);   
   19.60 -       M(A);  M(f);  M(r);  a\<in>A;  c\<in>A |] ==> a=c"
   19.61 -apply (frule wellordered_is_trans_on, assumption)
   19.62 -apply (frule wellordered_is_linear, assumption)
   19.63 -apply (erule_tac x=a and y=c in linearE, auto) 
   19.64 -apply (drule ord_iso_sym)
   19.65 -(*two symmetric cases*)
   19.66 -apply (blast dest: wellordered_iso_pred_eq_lemma)+ 
   19.67 -done
   19.68 -
   19.69  lemma (in M_basic) wellfounded_on_asym:
   19.70       "[| wellfounded_on(M,A,r);  <a,x>\<in>r;  a\<in>A; x\<in>A;  M(A) |] ==> <x,a>\<notin>r"
   19.71  apply (simp add: wellfounded_on_def) 
   19.72 @@ -285,353 +230,4 @@
   19.73       "[| wellordered(M,A,r);  <a,x>\<in>r;  a\<in>A; x\<in>A;  M(A) |] ==> <x,a>\<notin>r"
   19.74  by (simp add: wellordered_def, blast dest: wellfounded_on_asym)
   19.75  
   19.76 -
   19.77 -text{*Can't use @{text well_ord_iso_preserving} because it needs the
   19.78 -strong premise @{term "well_ord(A,r)"}*}
   19.79 -lemma (in M_basic) ord_iso_pred_imp_lt:
   19.80 -     "[| f \<in> ord_iso(Order.pred(A,x,r), r, i, Memrel(i));
   19.81 -         g \<in> ord_iso(Order.pred(A,y,r), r, j, Memrel(j));
   19.82 -         wellordered(M,A,r);  x \<in> A;  y \<in> A; M(A); M(r); M(f); M(g); M(j);
   19.83 -         Ord(i); Ord(j); \<langle>x,y\<rangle> \<in> r |]
   19.84 -      ==> i < j"
   19.85 -apply (frule wellordered_is_trans_on, assumption)
   19.86 -apply (frule_tac y=y in transM, assumption) 
   19.87 -apply (rule_tac i=i and j=j in Ord_linear_lt, auto)  
   19.88 -txt{*case @{term "i=j"} yields a contradiction*}
   19.89 - apply (rule_tac x1=x and A1="Order.pred(A,y,r)" in 
   19.90 -          wellordered_iso_predD [THEN notE]) 
   19.91 -   apply (blast intro: wellordered_subset [OF _ pred_subset]) 
   19.92 -  apply (simp add: trans_pred_pred_eq)
   19.93 -  apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans) 
   19.94 - apply (simp_all add: pred_iff pred_closed converse_closed comp_closed)
   19.95 -txt{*case @{term "j<i"} also yields a contradiction*}
   19.96 -apply (frule restrict_ord_iso2, assumption+) 
   19.97 -apply (frule ord_iso_sym [THEN ord_iso_is_bij, THEN bij_is_fun]) 
   19.98 -apply (frule apply_type, blast intro: ltD) 
   19.99 -  --{*thus @{term "converse(f)`j \<in> Order.pred(A,x,r)"}*}
  19.100 -apply (simp add: pred_iff) 
  19.101 -apply (subgoal_tac
  19.102 -       "\<exists>h[M]. h \<in> ord_iso(Order.pred(A,y,r), r, 
  19.103 -                               Order.pred(A, converse(f)`j, r), r)")
  19.104 - apply (clarify, frule wellordered_iso_pred_eq, assumption+)
  19.105 - apply (blast dest: wellordered_asym)  
  19.106 -apply (intro rexI)
  19.107 - apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans)+
  19.108 -done
  19.109 -
  19.110 -
  19.111 -lemma ord_iso_converse1:
  19.112 -     "[| f: ord_iso(A,r,B,s);  <b, f`a>: s;  a:A;  b:B |] 
  19.113 -      ==> <converse(f) ` b, a> : r"
  19.114 -apply (frule ord_iso_converse, assumption+) 
  19.115 -apply (blast intro: ord_iso_is_bij [THEN bij_is_fun, THEN apply_funtype]) 
  19.116 -apply (simp add: left_inverse_bij [OF ord_iso_is_bij])
  19.117 -done
  19.118 -
  19.119 -
  19.120 -subsection {* Order Types: A Direct Construction by Replacement*}
  19.121 -
  19.122 -text{*This follows Kunen's Theorem I 7.6, page 17.*}
  19.123 -
  19.124 -constdefs
  19.125 -  
  19.126 -  obase :: "[i=>o,i,i,i] => o"
  19.127 -       --{*the domain of @{text om}, eventually shown to equal @{text A}*}
  19.128 -   "obase(M,A,r,z) == 
  19.129 -	\<forall>a[M]. 
  19.130 -         a \<in> z <-> 
  19.131 -          (a\<in>A & (\<exists>x[M]. \<exists>g[M]. Ord(x) & 
  19.132 -                   order_isomorphism(M,Order.pred(A,a,r),r,x,Memrel(x),g)))"
  19.133 -
  19.134 -
  19.135 -  omap :: "[i=>o,i,i,i] => o"  
  19.136 -    --{*the function that maps wosets to order types*}
  19.137 -   "omap(M,A,r,f) == 
  19.138 -	\<forall>z[M].
  19.139 -         z \<in> f <-> 
  19.140 -          (\<exists>a[M]. a\<in>A & 
  19.141 -           (\<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M]. 
  19.142 -                ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & 
  19.143 -                pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g)))"
  19.144 -
  19.145 -
  19.146 -  otype :: "[i=>o,i,i,i] => o"  --{*the order types themselves*}
  19.147 -   "otype(M,A,r,i) == \<exists>f[M]. omap(M,A,r,f) & is_range(M,f,i)"
  19.148 -
  19.149 -
  19.150 -
  19.151 -lemma (in M_basic) obase_iff:
  19.152 -     "[| M(A); M(r); M(z) |] 
  19.153 -      ==> obase(M,A,r,z) <-> 
  19.154 -          z = {a\<in>A. \<exists>x[M]. \<exists>g[M]. Ord(x) & 
  19.155 -                          g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x))}"
  19.156 -apply (simp add: obase_def Memrel_closed pred_closed)
  19.157 -apply (rule iffI) 
  19.158 - prefer 2 apply blast 
  19.159 -apply (rule equalityI) 
  19.160 - apply (clarify, frule transM, assumption, simp) 
  19.161 -apply (clarify, frule transM, assumption, force)
  19.162 -done
  19.163 -
  19.164 -text{*Can also be proved with the premise @{term "M(z)"} instead of
  19.165 -      @{term "M(f)"}, but that version is less useful.*}
  19.166 -lemma (in M_basic) omap_iff:
  19.167 -     "[| omap(M,A,r,f); M(A); M(r); M(f) |] 
  19.168 -      ==> z \<in> f <->
  19.169 -      (\<exists>a\<in>A. \<exists>x[M]. \<exists>g[M]. z = <a,x> & Ord(x) & 
  19.170 -                        g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))"
  19.171 -apply (simp add: omap_def Memrel_closed pred_closed) 
  19.172 -apply (rule iffI)
  19.173 - apply (drule_tac [2] x=z in rspec)
  19.174 - apply (drule_tac x=z in rspec)
  19.175 - apply (blast dest: transM)+
  19.176 -done
  19.177 -
  19.178 -lemma (in M_basic) omap_unique:
  19.179 -     "[| omap(M,A,r,f); omap(M,A,r,f'); M(A); M(r); M(f); M(f') |] ==> f' = f" 
  19.180 -apply (rule equality_iffI) 
  19.181 -apply (simp add: omap_iff) 
  19.182 -done
  19.183 -
  19.184 -lemma (in M_basic) omap_yields_Ord:
  19.185 -     "[| omap(M,A,r,f); \<langle>a,x\<rangle> \<in> f; M(a); M(x) |]  ==> Ord(x)"
  19.186 -  by (simp add: omap_def)
  19.187 -
  19.188 -lemma (in M_basic) otype_iff:
  19.189 -     "[| otype(M,A,r,i); M(A); M(r); M(i) |] 
  19.190 -      ==> x \<in> i <-> 
  19.191 -          (M(x) & Ord(x) & 
  19.192 -           (\<exists>a\<in>A. \<exists>g[M]. g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x))))"
  19.193 -apply (auto simp add: omap_iff otype_def)
  19.194 - apply (blast intro: transM) 
  19.195 -apply (rule rangeI) 
  19.196 -apply (frule transM, assumption)
  19.197 -apply (simp add: omap_iff, blast)
  19.198 -done
  19.199 -
  19.200 -lemma (in M_basic) otype_eq_range:
  19.201 -     "[| omap(M,A,r,f); otype(M,A,r,i); M(A); M(r); M(f); M(i) |] 
  19.202 -      ==> i = range(f)"
  19.203 -apply (auto simp add: otype_def omap_iff)
  19.204 -apply (blast dest: omap_unique) 
  19.205 -done
  19.206 -
  19.207 -
  19.208 -lemma (in M_basic) Ord_otype:
  19.209 -     "[| otype(M,A,r,i); trans[A](r); M(A); M(r); M(i) |] ==> Ord(i)"
  19.210 -apply (rule OrdI) 
  19.211 -prefer 2 
  19.212 -    apply (simp add: Ord_def otype_def omap_def) 
  19.213 -    apply clarify 
  19.214 -    apply (frule pair_components_in_M, assumption) 
  19.215 -    apply blast 
  19.216 -apply (auto simp add: Transset_def otype_iff) 
  19.217 -  apply (blast intro: transM)
  19.218 - apply (blast intro: Ord_in_Ord) 
  19.219 -apply (rename_tac y a g)
  19.220 -apply (frule ord_iso_sym [THEN ord_iso_is_bij, THEN bij_is_fun, 
  19.221 -			  THEN apply_funtype],  assumption)  
  19.222 -apply (rule_tac x="converse(g)`y" in bexI)
  19.223 - apply (frule_tac a="converse(g) ` y" in ord_iso_restrict_pred, assumption) 
  19.224 -apply (safe elim!: predE) 
  19.225 -apply (blast intro: restrict_ord_iso ord_iso_sym ltI dest: transM)
  19.226 -done
  19.227 -
  19.228 -lemma (in M_basic) domain_omap:
  19.229 -     "[| omap(M,A,r,f);  obase(M,A,r,B); M(A); M(r); M(B); M(f) |] 
  19.230 -      ==> domain(f) = B"
  19.231 -apply (simp add: domain_closed obase_iff) 
  19.232 -apply (rule equality_iffI) 
  19.233 -apply (simp add: domain_iff omap_iff, blast) 
  19.234 -done
  19.235 -
  19.236 -lemma (in M_basic) omap_subset: 
  19.237 -     "[| omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); 
  19.238 -       M(A); M(r); M(f); M(B); M(i) |] ==> f \<subseteq> B * i"
  19.239 -apply clarify 
  19.240 -apply (simp add: omap_iff obase_iff) 
  19.241 -apply (force simp add: otype_iff) 
  19.242 -done
  19.243 -
  19.244 -lemma (in M_basic) omap_funtype: 
  19.245 -     "[| omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); 
  19.246 -       M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> B -> i"
  19.247 -apply (simp add: domain_omap omap_subset Pi_iff function_def omap_iff) 
  19.248 -apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans) 
  19.249 -done
  19.250 -
  19.251 -
  19.252 -lemma (in M_basic) wellordered_omap_bij:
  19.253 -     "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); 
  19.254 -       M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> bij(B,i)"
  19.255 -apply (insert omap_funtype [of A r f B i]) 
  19.256 -apply (auto simp add: bij_def inj_def) 
  19.257 -prefer 2  apply (blast intro: fun_is_surj dest: otype_eq_range) 
  19.258 -apply (frule_tac a=w in apply_Pair, assumption) 
  19.259 -apply (frule_tac a=x in apply_Pair, assumption) 
  19.260 -apply (simp add: omap_iff) 
  19.261 -apply (blast intro: wellordered_iso_pred_eq ord_iso_sym ord_iso_trans) 
  19.262 -done
  19.263 -
  19.264 -
  19.265 -text{*This is not the final result: we must show @{term "oB(A,r) = A"}*}
  19.266 -lemma (in M_basic) omap_ord_iso:
  19.267 -     "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); 
  19.268 -       M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> ord_iso(B,r,i,Memrel(i))"
  19.269 -apply (rule ord_isoI)
  19.270 - apply (erule wellordered_omap_bij, assumption+) 
  19.271 -apply (insert omap_funtype [of A r f B i], simp) 
  19.272 -apply (frule_tac a=x in apply_Pair, assumption) 
  19.273 -apply (frule_tac a=y in apply_Pair, assumption) 
  19.274 -apply (auto simp add: omap_iff)
  19.275 - txt{*direction 1: assuming @{term "\<langle>x,y\<rangle> \<in> r"}*}
  19.276 - apply (blast intro: ltD ord_iso_pred_imp_lt)
  19.277 - txt{*direction 2: proving @{term "\<langle>x,y\<rangle> \<in> r"} using linearity of @{term r}*}
  19.278 -apply (rename_tac x y g ga) 
  19.279 -apply (frule wellordered_is_linear, assumption, 
  19.280 -       erule_tac x=x and y=y in linearE, assumption+) 
  19.281 -txt{*the case @{term "x=y"} leads to immediate contradiction*} 
  19.282 -apply (blast elim: mem_irrefl) 
  19.283 -txt{*the case @{term "\<langle>y,x\<rangle> \<in> r"}: handle like the opposite direction*}
  19.284 -apply (blast dest: ord_iso_pred_imp_lt ltD elim: mem_asym) 
  19.285 -done
  19.286 -
  19.287 -lemma (in M_basic) Ord_omap_image_pred:
  19.288 -     "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); 
  19.289 -       M(A); M(r); M(f); M(B); M(i); b \<in> A |] ==> Ord(f `` Order.pred(A,b,r))"
  19.290 -apply (frule wellordered_is_trans_on, assumption)
  19.291 -apply (rule OrdI) 
  19.292 -	prefer 2 apply (simp add: image_iff omap_iff Ord_def, blast) 
  19.293 -txt{*Hard part is to show that the image is a transitive set.*}
  19.294 -apply (simp add: Transset_def, clarify) 
  19.295 -apply (simp add: image_iff pred_iff apply_iff [OF omap_funtype [of A r f B i]])
  19.296 -apply (rename_tac c j, clarify)
  19.297 -apply (frule omap_funtype [of A r f B, THEN apply_funtype], assumption+)
  19.298 -apply (subgoal_tac "j : i") 
  19.299 -	prefer 2 apply (blast intro: Ord_trans Ord_otype)
  19.300 -apply (subgoal_tac "converse(f) ` j : B") 
  19.301 -	prefer 2 
  19.302 -	apply (blast dest: wellordered_omap_bij [THEN bij_converse_bij, 
  19.303 -                                      THEN bij_is_fun, THEN apply_funtype])
  19.304 -apply (rule_tac x="converse(f) ` j" in bexI) 
  19.305 - apply (simp add: right_inverse_bij [OF wellordered_omap_bij]) 
  19.306 -apply (intro predI conjI)
  19.307 - apply (erule_tac b=c in trans_onD) 
  19.308 - apply (rule ord_iso_converse1 [OF omap_ord_iso [of A r f B i]])
  19.309 -apply (auto simp add: obase_iff)
  19.310 -done
  19.311 -
  19.312 -lemma (in M_basic) restrict_omap_ord_iso:
  19.313 -     "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); 
  19.314 -       D \<subseteq> B; M(A); M(r); M(f); M(B); M(i) |] 
  19.315 -      ==> restrict(f,D) \<in> (\<langle>D,r\<rangle> \<cong> \<langle>f``D, Memrel(f``D)\<rangle>)"
  19.316 -apply (frule ord_iso_restrict_image [OF omap_ord_iso [of A r f B i]], 
  19.317 -       assumption+)
  19.318 -apply (drule ord_iso_sym [THEN subset_ord_iso_Memrel]) 
  19.319 -apply (blast dest: subsetD [OF omap_subset]) 
  19.320 -apply (drule ord_iso_sym, simp) 
  19.321 -done
  19.322 -
  19.323 -lemma (in M_basic) obase_equals: 
  19.324 -     "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i);
  19.325 -       M(A); M(r); M(f); M(B); M(i) |] ==> B = A"
  19.326 -apply (rule equalityI, force simp add: obase_iff, clarify) 
  19.327 -apply (subst obase_iff [of A r B, THEN iffD1], assumption+, simp) 
  19.328 -apply (frule wellordered_is_wellfounded_on, assumption)
  19.329 -apply (erule wellfounded_on_induct, assumption+)
  19.330 - apply (frule obase_equals_separation [of A r], assumption) 
  19.331 - apply (simp, clarify) 
  19.332 -apply (rename_tac b) 
  19.333 -apply (subgoal_tac "Order.pred(A,b,r) <= B") 
  19.334 - apply (blast intro!: restrict_omap_ord_iso Ord_omap_image_pred)
  19.335 -apply (force simp add: pred_iff obase_iff)  
  19.336 -done
  19.337 -
  19.338 -
  19.339 -
  19.340 -text{*Main result: @{term om} gives the order-isomorphism 
  19.341 -      @{term "\<langle>A,r\<rangle> \<cong> \<langle>i, Memrel(i)\<rangle>"} *}
  19.342 -theorem (in M_basic) omap_ord_iso_otype:
  19.343 -     "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i);
  19.344 -       M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> ord_iso(A, r, i, Memrel(i))"
  19.345 -apply (frule omap_ord_iso, assumption+) 
  19.346 -apply (frule obase_equals, assumption+, blast) 
  19.347 -done 
  19.348 -
  19.349 -lemma (in M_basic) obase_exists:
  19.350 -     "[| M(A); M(r) |] ==> \<exists>z[M]. obase(M,A,r,z)"
  19.351 -apply (simp add: obase_def) 
  19.352 -apply (insert obase_separation [of A r])
  19.353 -apply (simp add: separation_def)  
  19.354 -done
  19.355 -
  19.356 -lemma (in M_basic) omap_exists:
  19.357 -     "[| M(A); M(r) |] ==> \<exists>z[M]. omap(M,A,r,z)"
  19.358 -apply (insert obase_exists [of A r]) 
  19.359 -apply (simp add: omap_def) 
  19.360 -apply (insert omap_replacement [of A r])
  19.361 -apply (simp add: strong_replacement_def, clarify) 
  19.362 -apply (drule_tac x=x in rspec, clarify) 
  19.363 -apply (simp add: Memrel_closed pred_closed obase_iff)
  19.364 -apply (erule impE) 
  19.365 - apply (clarsimp simp add: univalent_def)
  19.366 - apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans, clarify)  
  19.367 -apply (rule_tac x=Y in rexI) 
  19.368 -apply (simp add: Memrel_closed pred_closed obase_iff, blast, assumption)
  19.369 -done
  19.370 -
  19.371 -declare rall_simps [simp] rex_simps [simp]
  19.372 -
  19.373 -lemma (in M_basic) otype_exists:
  19.374 -     "[| wellordered(M,A,r); M(A); M(r) |] ==> \<exists>i[M]. otype(M,A,r,i)"
  19.375 -apply (insert omap_exists [of A r])  
  19.376 -apply (simp add: otype_def, safe)
  19.377 -apply (rule_tac x="range(x)" in rexI) 
  19.378 -apply blast+
  19.379 -done
  19.380 -
  19.381 -theorem (in M_basic) omap_ord_iso_otype':
  19.382 -     "[| wellordered(M,A,r); M(A); M(r) |]
  19.383 -      ==> \<exists>f[M]. (\<exists>i[M]. Ord(i) & f \<in> ord_iso(A, r, i, Memrel(i)))"
  19.384 -apply (insert obase_exists [of A r] omap_exists [of A r] otype_exists [of A r], simp, clarify)
  19.385 -apply (rename_tac i) 
  19.386 -apply (subgoal_tac "Ord(i)", blast intro: omap_ord_iso_otype) 
  19.387 -apply (rule Ord_otype) 
  19.388 -    apply (force simp add: otype_def range_closed) 
  19.389 -   apply (simp_all add: wellordered_is_trans_on) 
  19.390 -done
  19.391 -
  19.392 -lemma (in M_basic) ordertype_exists:
  19.393 -     "[| wellordered(M,A,r); M(A); M(r) |]
  19.394 -      ==> \<exists>f[M]. (\<exists>i[M]. Ord(i) & f \<in> ord_iso(A, r, i, Memrel(i)))"
  19.395 -apply (insert obase_exists [of A r] omap_exists [of A r] otype_exists [of A r], simp, clarify)
  19.396 -apply (rename_tac i) 
  19.397 -apply (subgoal_tac "Ord(i)", blast intro: omap_ord_iso_otype')
  19.398 -apply (rule Ord_otype) 
  19.399 -    apply (force simp add: otype_def range_closed) 
  19.400 -   apply (simp_all add: wellordered_is_trans_on) 
  19.401 -done
  19.402 -
  19.403 -
  19.404 -lemma (in M_basic) relativized_imp_well_ord: 
  19.405 -     "[| wellordered(M,A,r); M(A); M(r) |] ==> well_ord(A,r)" 
  19.406 -apply (insert ordertype_exists [of A r], simp)
  19.407 -apply (blast intro: well_ord_ord_iso well_ord_Memrel)  
  19.408 -done
  19.409 -
  19.410 -subsection {*Kunen's theorem 5.4, poage 127*}
  19.411 -
  19.412 -text{*(a) The notion of Wellordering is absolute*}
  19.413 -theorem (in M_basic) well_ord_abs [simp]: 
  19.414 -     "[| M(A); M(r) |] ==> wellordered(M,A,r) <-> well_ord(A,r)" 
  19.415 -by (blast intro: well_ord_imp_relativized relativized_imp_well_ord)  
  19.416 -
  19.417 -
  19.418 -text{*(b) Order types are absolute*}
  19.419 -lemma (in M_basic) 
  19.420 -     "[| wellordered(M,A,r); f \<in> ord_iso(A, r, i, Memrel(i));
  19.421 -       M(A); M(r); M(f); M(i); Ord(i) |] ==> i = ordertype(A,r)"
  19.422 -by (blast intro: Ord_ordertype relativized_imp_well_ord ordertype_ord_iso
  19.423 -                 Ord_iso_implies_eq ord_iso_sym ord_iso_trans)
  19.424 -
  19.425  end
    20.1 --- a/src/ZF/IsaMakefile	Tue Oct 08 14:09:18 2002 +0200
    20.2 +++ b/src/ZF/IsaMakefile	Wed Oct 09 11:07:13 2002 +0200
    20.3 @@ -83,6 +83,7 @@
    20.4    Constructible/AC_in_L.thy Constructible/Relative.thy \
    20.5    Constructible/L_axioms.thy    Constructible/Wellorderings.thy \
    20.6    Constructible/MetaExists.thy  Constructible/Normal.thy \
    20.7 +  Constructible/Rank.thy Constructible/Rank_Separation.thy \
    20.8    Constructible/Rec_Separation.thy Constructible/Separation.thy \
    20.9    Constructible/Satisfies_absolute.thy Constructible/WF_absolute.thy \
   20.10    Constructible/Reflection.thy  Constructible/WFrec.thy \
    21.1 --- a/src/ZF/OrderArith.thy	Tue Oct 08 14:09:18 2002 +0200
    21.2 +++ b/src/ZF/OrderArith.thy	Wed Oct 09 11:07:13 2002 +0200
    21.3 @@ -398,6 +398,61 @@
    21.4  by (unfold ord_iso_def rvimage_def, blast)
    21.5  
    21.6  
    21.7 +subsection{*Every well-founded relation is a subset of some inverse image of
    21.8 +      an ordinal*}
    21.9 +
   21.10 +lemma wf_rvimage_Ord: "Ord(i) \<Longrightarrow> wf(rvimage(A, f, Memrel(i)))"
   21.11 +by (blast intro: wf_rvimage wf_Memrel)
   21.12 +
   21.13 +
   21.14 +constdefs
   21.15 +  wfrank :: "[i,i]=>i"
   21.16 +    "wfrank(r,a) == wfrec(r, a, %x f. \<Union>y \<in> r-``{x}. succ(f`y))"
   21.17 +
   21.18 +constdefs
   21.19 +  wftype :: "i=>i"
   21.20 +    "wftype(r) == \<Union>y \<in> range(r). succ(wfrank(r,y))"
   21.21 +
   21.22 +lemma wfrank: "wf(r) ==> wfrank(r,a) = (\<Union>y \<in> r-``{a}. succ(wfrank(r,y)))"
   21.23 +by (subst wfrank_def [THEN def_wfrec], simp_all)
   21.24 +
   21.25 +lemma Ord_wfrank: "wf(r) ==> Ord(wfrank(r,a))"
   21.26 +apply (rule_tac a=a in wf_induct, assumption)
   21.27 +apply (subst wfrank, assumption)
   21.28 +apply (rule Ord_succ [THEN Ord_UN], blast)
   21.29 +done
   21.30 +
   21.31 +lemma wfrank_lt: "[|wf(r); <a,b> \<in> r|] ==> wfrank(r,a) < wfrank(r,b)"
   21.32 +apply (rule_tac a1 = b in wfrank [THEN ssubst], assumption)
   21.33 +apply (rule UN_I [THEN ltI])
   21.34 +apply (simp add: Ord_wfrank vimage_iff)+
   21.35 +done
   21.36 +
   21.37 +lemma Ord_wftype: "wf(r) ==> Ord(wftype(r))"
   21.38 +by (simp add: wftype_def Ord_wfrank)
   21.39 +
   21.40 +lemma wftypeI: "\<lbrakk>wf(r);  x \<in> field(r)\<rbrakk> \<Longrightarrow> wfrank(r,x) \<in> wftype(r)"
   21.41 +apply (simp add: wftype_def)
   21.42 +apply (blast intro: wfrank_lt [THEN ltD])
   21.43 +done
   21.44 +
   21.45 +
   21.46 +lemma wf_imp_subset_rvimage:
   21.47 +     "[|wf(r); r \<subseteq> A*A|] ==> \<exists>i f. Ord(i) & r <= rvimage(A, f, Memrel(i))"
   21.48 +apply (rule_tac x="wftype(r)" in exI)
   21.49 +apply (rule_tac x="\<lambda>x\<in>A. wfrank(r,x)" in exI)
   21.50 +apply (simp add: Ord_wftype, clarify)
   21.51 +apply (frule subsetD, assumption, clarify)
   21.52 +apply (simp add: rvimage_iff wfrank_lt [THEN ltD])
   21.53 +apply (blast intro: wftypeI)
   21.54 +done
   21.55 +
   21.56 +theorem wf_iff_subset_rvimage:
   21.57 +  "relation(r) ==> wf(r) <-> (\<exists>i f A. Ord(i) & r <= rvimage(A, f, Memrel(i)))"
   21.58 +by (blast dest!: relation_field_times_field wf_imp_subset_rvimage
   21.59 +          intro: wf_rvimage_Ord [THEN wf_subset])
   21.60 +
   21.61 +
   21.62  subsection{*Other Results*}
   21.63  
   21.64  lemma wf_times: "A Int B = 0 ==> wf(A*B)"
    22.1 --- a/src/ZF/WF.thy	Tue Oct 08 14:09:18 2002 +0200
    22.2 +++ b/src/ZF/WF.thy	Wed Oct 09 11:07:13 2002 +0200
    22.3 @@ -47,7 +47,7 @@
    22.4  
    22.5  subsection{*Well-Founded Relations*}
    22.6  
    22.7 -(** Equivalences between wf and wf_on **)
    22.8 +subsubsection{*Equivalences between @{term wf} and @{term wf_on}*}
    22.9  
   22.10  lemma wf_imp_wf_on: "wf(r) ==> wf[A](r)"
   22.11  apply (unfold wf_def wf_on_def, clarify) (*needed for blast's efficiency*)
   22.12 @@ -72,10 +72,11 @@
   22.13  lemma wf_subset: "[|wf(s); r<=s|] ==> wf(r)"
   22.14  by (simp add: wf_def, fast)
   22.15  
   22.16 -(** Introduction rules for wf_on **)
   22.17 +subsubsection{*Introduction Rules for @{term wf_on}*}
   22.18  
   22.19 +text{*If every non-empty subset of @{term A} has an @{term r}-minimal element
   22.20 +   then we have @{term "wf[A](r)"}.*}
   22.21  lemma wf_onI:
   22.22 -(*If every non-empty subset of A has an r-minimal element then wf[A](r).*)
   22.23   assumes prem: "!!Z u. [| Z<=A;  u:Z;  ALL x:Z. EX y:Z. <y,x>:r |] ==> False"
   22.24   shows         "wf[A](r)"
   22.25  apply (unfold wf_on_def wf_def)
   22.26 @@ -83,9 +84,9 @@
   22.27  apply (rule_tac Z = "Z" in prem, blast+)
   22.28  done
   22.29  
   22.30 -(*If r allows well-founded induction over A then wf[A](r)
   22.31 -  Premise is equivalent to
   22.32 -  !!B. ALL x:A. (ALL y. <y,x>: r --> y:B) --> x:B ==> A<=B  *)
   22.33 +text{*If @{term r} allows well-founded induction over @{term A}
   22.34 +   then we have @{term "wf[A](r)"}.   Premise is equivalent to
   22.35 +  @{term "!!B. ALL x:A. (ALL y. <y,x>: r --> y:B) --> x:B ==> A<=B"} *}
   22.36  lemma wf_onI2:
   22.37   assumes prem: "!!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B;   y:A |]
   22.38                         ==> y:B"
   22.39 @@ -97,13 +98,14 @@
   22.40  done
   22.41  
   22.42  
   22.43 -(** Well-founded Induction **)
   22.44 +subsubsection{*Well-founded Induction*}
   22.45  
   22.46 -(*Consider the least z in domain(r) such that P(z) does not hold...*)
   22.47 +text{*Consider the least @{term z} in @{term "domain(r)"} such that
   22.48 +  @{term "P(z)"} does not hold...*}
   22.49  lemma wf_induct [induct set: wf]:
   22.50      "[| wf(r);
   22.51 -        !!x.[| ALL y. <y,x>: r --> P(y) |] ==> P(x)
   22.52 -     |]  ==>  P(a)"
   22.53 +        !!x.[| ALL y. <y,x>: r --> P(y) |] ==> P(x) |]  
   22.54 +     ==> P(a)"
   22.55  apply (unfold wf_def) 
   22.56  apply (erule_tac x = "{z : domain(r). ~ P(z)}" in allE)
   22.57  apply blast 
   22.58 @@ -111,7 +113,7 @@
   22.59  
   22.60  lemmas wf_induct_rule = wf_induct [rule_format, induct set: wf]
   22.61  
   22.62 -(*The form of this rule is designed to match wfI*)
   22.63 +text{*The form of this rule is designed to match @{text wfI}*}
   22.64  lemma wf_induct2:
   22.65      "[| wf(r);  a:A;  field(r)<=A;
   22.66          !!x.[| x: A;  ALL y. <y,x>: r --> P(y) |] ==> P(x) |]
   22.67 @@ -136,7 +138,8 @@
   22.68    wf_on_induct [rule_format, consumes 2, induct set: wf_on]
   22.69  
   22.70  
   22.71 -(*If r allows well-founded induction then wf(r)*)
   22.72 +text{*If @{term r} allows well-founded induction 
   22.73 +   then we have @{term "wf(r)"}.*}
   22.74  lemma wfI:
   22.75      "[| field(r)<=A;
   22.76          !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B;  y:A|]
   22.77 @@ -185,8 +188,8 @@
   22.78  
   22.79  
   22.80  
   22.81 -
   22.82 -(*transitive closure of a WF relation is WF provided A is downwards closed*)
   22.83 +text{*transitive closure of a WF relation is WF provided 
   22.84 +  @{term A} is downward closed*}
   22.85  lemma wf_on_trancl:
   22.86      "[| wf[A](r);  r-``A <= A |] ==> wf[A](r^+)"
   22.87  apply (rule wf_onI2)
   22.88 @@ -204,13 +207,13 @@
   22.89  done
   22.90  
   22.91  
   22.92 -
   22.93 -(** r-``{a} is the set of everything under a in r **)
   22.94 +text{*@{term "r-``{a}"} is the set of everything under @{term a} in @{term r}*}
   22.95  
   22.96  lemmas underI = vimage_singleton_iff [THEN iffD2, standard]
   22.97  lemmas underD = vimage_singleton_iff [THEN iffD1, standard]
   22.98  
   22.99 -(** is_recfun **)
  22.100 +
  22.101 +subsection{*The Predicate @{term is_recfun}*}
  22.102  
  22.103  lemma is_recfun_type: "is_recfun(r,a,H,f) ==> f: r-``{a} -> range(f)"
  22.104  apply (unfold is_recfun_def)
  22.105 @@ -281,7 +284,7 @@
  22.106  apply (rule_tac f = "lam y: r-``{a1}. wftrec (r,y,H)" in is_the_recfun)
  22.107    apply typecheck
  22.108  apply (unfold is_recfun_def wftrec_def)
  22.109 -(*Applying the substitution: must keep the quantified assumption!!*)
  22.110 +  --{*Applying the substitution: must keep the quantified assumption!*}
  22.111  apply (rule lam_cong [OF refl]) 
  22.112  apply (drule underD) 
  22.113  apply (fold is_recfun_def)
  22.114 @@ -316,7 +319,8 @@
  22.115  apply (simp_all add: vimage_singleton_iff [THEN iff_sym] the_recfun_cut)
  22.116  done
  22.117  
  22.118 -(** Removal of the premise trans(r) **)
  22.119 +
  22.120 +subsubsection{*Removal of the Premise @{term "trans(r)"}*}
  22.121  
  22.122  (*NOT SUITABLE FOR REWRITING: it is recursive!*)
  22.123  lemma wfrec:
  22.124 @@ -355,11 +359,11 @@
  22.125  apply (simp add: vimage_Int_square cons_subset_iff)
  22.126  done
  22.127  
  22.128 -(*Minimal-element characterization of well-foundedness*)
  22.129 +text{*Minimal-element characterization of well-foundedness*}
  22.130  lemma wf_eq_minimal:
  22.131       "wf(r) <-> (ALL Q x. x:Q --> (EX z:Q. ALL y. <y,z>:r --> y~:Q))"
  22.132 -apply (unfold wf_def, blast)
  22.133 -done
  22.134 +by (unfold wf_def, blast)
  22.135 +
  22.136  
  22.137  ML
  22.138  {*