src/ZF/Constructible/Datatype_absolute.thy
changeset 13634 99a593b49b04
parent 13615 449a70d88b38
child 13647 7f6f0ffc45c3
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Tue Oct 08 14:09:18 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Wed Oct 09 11:07:13 2002 +0200
     1.3 @@ -1,7 +1,6 @@
     1.4  (*  Title:      ZF/Constructible/Datatype_absolute.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 {*Absoluteness Properties for Recursive Datatypes*}
    1.11 @@ -127,38 +126,38 @@
    1.12           wfrec_replacement(M, iterates_MH(M,isF,v), Memrel(succ(n)))"
    1.13  
    1.14  lemma (in M_basic) iterates_MH_abs:
    1.15 -  "[| relativize1(M,isF,F); M(n); M(g); M(z) |] 
    1.16 +  "[| relation1(M,isF,F); M(n); M(g); M(z) |] 
    1.17     ==> iterates_MH(M,isF,v,n,g,z) <-> z = nat_case(v, \<lambda>m. F(g`m), n)"
    1.18  by (simp add: nat_case_abs [of _ "\<lambda>m. F(g ` m)"]
    1.19 -              relativize1_def iterates_MH_def)  
    1.20 +              relation1_def iterates_MH_def)  
    1.21  
    1.22  lemma (in M_basic) iterates_imp_wfrec_replacement:
    1.23 -  "[|relativize1(M,isF,F); n \<in> nat; iterates_replacement(M,isF,v)|] 
    1.24 +  "[|relation1(M,isF,F); n \<in> nat; iterates_replacement(M,isF,v)|] 
    1.25     ==> wfrec_replacement(M, \<lambda>n f z. z = nat_case(v, \<lambda>m. F(f`m), n), 
    1.26                         Memrel(succ(n)))" 
    1.27  by (simp add: iterates_replacement_def iterates_MH_abs)
    1.28  
    1.29  theorem (in M_trancl) iterates_abs:
    1.30 -  "[| iterates_replacement(M,isF,v); relativize1(M,isF,F);
    1.31 +  "[| iterates_replacement(M,isF,v); relation1(M,isF,F);
    1.32        n \<in> nat; M(v); M(z); \<forall>x[M]. M(F(x)) |] 
    1.33     ==> is_wfrec(M, iterates_MH(M,isF,v), Memrel(succ(n)), n, z) <->
    1.34         z = iterates(F,n,v)" 
    1.35  apply (frule iterates_imp_wfrec_replacement, assumption+)
    1.36  apply (simp add: wf_Memrel trans_Memrel relation_Memrel nat_into_M
    1.37 -                 relativize2_def iterates_MH_abs 
    1.38 +                 relation2_def iterates_MH_abs 
    1.39                   iterates_nat_def recursor_def transrec_def 
    1.40                   eclose_sing_Ord_eq nat_into_M
    1.41           trans_wfrec_abs [of _ _ _ _ "\<lambda>n g. nat_case(v, \<lambda>m. F(g`m), n)"])
    1.42  done
    1.43  
    1.44  
    1.45 -lemma (in M_wfrank) iterates_closed [intro,simp]:
    1.46 -  "[| iterates_replacement(M,isF,v); relativize1(M,isF,F);
    1.47 +lemma (in M_trancl) iterates_closed [intro,simp]:
    1.48 +  "[| iterates_replacement(M,isF,v); relation1(M,isF,F);
    1.49        n \<in> nat; M(v); \<forall>x[M]. M(F(x)) |] 
    1.50     ==> M(iterates(F,n,v))"
    1.51  apply (frule iterates_imp_wfrec_replacement, assumption+)
    1.52  apply (simp add: wf_Memrel trans_Memrel relation_Memrel nat_into_M
    1.53 -                 relativize2_def iterates_MH_abs 
    1.54 +                 relation2_def iterates_MH_abs 
    1.55                   iterates_nat_def recursor_def transrec_def 
    1.56                   eclose_sing_Ord_eq nat_into_M
    1.57           trans_wfrec_closed [of _ _ _ "\<lambda>n g. nat_case(v, \<lambda>m. F(g`m), n)"])
    1.58 @@ -459,7 +458,7 @@
    1.59    is_formula :: "[i=>o,i] => o"
    1.60      "is_formula(M,Z) == \<forall>p[M]. p \<in> Z <-> mem_formula(M,p)"
    1.61  
    1.62 -locale M_datatypes = M_wfrank +
    1.63 +locale M_datatypes = M_trancl +
    1.64   assumes list_replacement1: 
    1.65     "M(A) ==> iterates_replacement(M, is_list_functor(M,A), 0)"
    1.66    and list_replacement2: 
    1.67 @@ -487,14 +486,14 @@
    1.68  apply (insert list_replacement2 [of A]) 
    1.69  apply (rule strong_replacement_cong [THEN iffD1])  
    1.70  apply (rule conj_cong [OF iff_refl iterates_abs [of "is_list_functor(M,A)"]]) 
    1.71 -apply (simp_all add: list_replacement1 relativize1_def) 
    1.72 +apply (simp_all add: list_replacement1 relation1_def) 
    1.73  done
    1.74  
    1.75  lemma (in M_datatypes) list_closed [intro,simp]:
    1.76       "M(A) ==> M(list(A))"
    1.77  apply (insert list_replacement1)
    1.78  by  (simp add: RepFun_closed2 list_eq_Union 
    1.79 -               list_replacement2' relativize1_def
    1.80 +               list_replacement2' relation1_def
    1.81                 iterates_closed [of "is_list_functor(M,A)"])
    1.82  
    1.83  text{*WARNING: use only with @{text "dest:"} or with variables fixed!*}
    1.84 @@ -504,21 +503,21 @@
    1.85       "[|M(A); n\<in>nat; M(Z)|] 
    1.86        ==> is_list_N(M,A,n,Z) <-> Z = list_N(A,n)"
    1.87  apply (insert list_replacement1)
    1.88 -apply (simp add: is_list_N_def list_N_def relativize1_def nat_into_M
    1.89 +apply (simp add: is_list_N_def list_N_def relation1_def nat_into_M
    1.90                   iterates_abs [of "is_list_functor(M,A)" _ "\<lambda>X. {0} + A*X"])
    1.91  done
    1.92  
    1.93  lemma (in M_datatypes) list_N_closed [intro,simp]:
    1.94       "[|M(A); n\<in>nat|] ==> M(list_N(A,n))"
    1.95  apply (insert list_replacement1)
    1.96 -apply (simp add: is_list_N_def list_N_def relativize1_def nat_into_M
    1.97 +apply (simp add: is_list_N_def list_N_def relation1_def nat_into_M
    1.98                   iterates_closed [of "is_list_functor(M,A)"])
    1.99  done
   1.100  
   1.101  lemma (in M_datatypes) mem_list_abs [simp]:
   1.102       "M(A) ==> mem_list(M,A,l) <-> l \<in> list(A)"
   1.103  apply (insert list_replacement1)
   1.104 -apply (simp add: mem_list_def list_N_def relativize1_def list_eq_Union
   1.105 +apply (simp add: mem_list_def list_N_def relation1_def list_eq_Union
   1.106                   iterates_closed [of "is_list_functor(M,A)"]) 
   1.107  done
   1.108  
   1.109 @@ -535,14 +534,14 @@
   1.110  apply (insert formula_replacement2) 
   1.111  apply (rule strong_replacement_cong [THEN iffD1])  
   1.112  apply (rule conj_cong [OF iff_refl iterates_abs [of "is_formula_functor(M)"]]) 
   1.113 -apply (simp_all add: formula_replacement1 relativize1_def) 
   1.114 +apply (simp_all add: formula_replacement1 relation1_def) 
   1.115  done
   1.116  
   1.117  lemma (in M_datatypes) formula_closed [intro,simp]:
   1.118       "M(formula)"
   1.119  apply (insert formula_replacement1)
   1.120  apply  (simp add: RepFun_closed2 formula_eq_Union 
   1.121 -                  formula_replacement2' relativize1_def
   1.122 +                  formula_replacement2' relation1_def
   1.123                    iterates_closed [of "is_formula_functor(M)"])
   1.124  done
   1.125  
   1.126 @@ -552,7 +551,7 @@
   1.127       "[|n\<in>nat; M(Z)|] 
   1.128        ==> is_formula_N(M,n,Z) <-> Z = formula_N(n)"
   1.129  apply (insert formula_replacement1)
   1.130 -apply (simp add: is_formula_N_def formula_N_def relativize1_def nat_into_M
   1.131 +apply (simp add: is_formula_N_def formula_N_def relation1_def nat_into_M
   1.132                   iterates_abs [of "is_formula_functor(M)" _ 
   1.133                                    "\<lambda>X. ((nat*nat) + (nat*nat)) + (X*X + X)"])
   1.134  done
   1.135 @@ -560,14 +559,14 @@
   1.136  lemma (in M_datatypes) formula_N_closed [intro,simp]:
   1.137       "n\<in>nat ==> M(formula_N(n))"
   1.138  apply (insert formula_replacement1)
   1.139 -apply (simp add: is_formula_N_def formula_N_def relativize1_def nat_into_M
   1.140 +apply (simp add: is_formula_N_def formula_N_def relation1_def nat_into_M
   1.141                   iterates_closed [of "is_formula_functor(M)"])
   1.142  done
   1.143  
   1.144  lemma (in M_datatypes) mem_formula_abs [simp]:
   1.145       "mem_formula(M,l) <-> l \<in> formula"
   1.146  apply (insert formula_replacement1)
   1.147 -apply (simp add: mem_formula_def relativize1_def formula_eq_Union formula_N_def
   1.148 +apply (simp add: mem_formula_def relation1_def formula_eq_Union formula_N_def
   1.149                   iterates_closed [of "is_formula_functor(M)"]) 
   1.150  done
   1.151  
   1.152 @@ -624,27 +623,27 @@
   1.153  apply (insert eclose_replacement2 [of A]) 
   1.154  apply (rule strong_replacement_cong [THEN iffD1])  
   1.155  apply (rule conj_cong [OF iff_refl iterates_abs [of "big_union(M)"]]) 
   1.156 -apply (simp_all add: eclose_replacement1 relativize1_def) 
   1.157 +apply (simp_all add: eclose_replacement1 relation1_def) 
   1.158  done
   1.159  
   1.160  lemma (in M_eclose) eclose_closed [intro,simp]:
   1.161       "M(A) ==> M(eclose(A))"
   1.162  apply (insert eclose_replacement1)
   1.163  by  (simp add: RepFun_closed2 eclose_eq_Union 
   1.164 -               eclose_replacement2' relativize1_def
   1.165 +               eclose_replacement2' relation1_def
   1.166                 iterates_closed [of "big_union(M)"])
   1.167  
   1.168  lemma (in M_eclose) is_eclose_n_abs [simp]:
   1.169       "[|M(A); n\<in>nat; M(Z)|] ==> is_eclose_n(M,A,n,Z) <-> Z = Union^n (A)"
   1.170  apply (insert eclose_replacement1)
   1.171 -apply (simp add: is_eclose_n_def relativize1_def nat_into_M
   1.172 +apply (simp add: is_eclose_n_def relation1_def nat_into_M
   1.173                   iterates_abs [of "big_union(M)" _ "Union"])
   1.174  done
   1.175  
   1.176  lemma (in M_eclose) mem_eclose_abs [simp]:
   1.177       "M(A) ==> mem_eclose(M,A,l) <-> l \<in> eclose(A)"
   1.178  apply (insert eclose_replacement1)
   1.179 -apply (simp add: mem_eclose_def relativize1_def eclose_eq_Union
   1.180 +apply (simp add: mem_eclose_def relation1_def eclose_eq_Union
   1.181                   iterates_closed [of "big_union(M)"]) 
   1.182  done
   1.183  
   1.184 @@ -679,7 +678,7 @@
   1.185    @{text "trans_wfrec_abs"} rather than @{text "trans_wfrec_abs"},
   1.186    which I haven't even proved yet. *}
   1.187  theorem (in M_eclose) transrec_abs:
   1.188 -  "[|transrec_replacement(M,MH,i);  relativize2(M,MH,H);
   1.189 +  "[|transrec_replacement(M,MH,i);  relation2(M,MH,H);
   1.190       Ord(i);  M(i);  M(z);
   1.191       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
   1.192     ==> is_transrec(M,MH,i,z) <-> z = transrec(i,H)" 
   1.193 @@ -688,7 +687,7 @@
   1.194  
   1.195  
   1.196  theorem (in M_eclose) transrec_closed:
   1.197 -     "[|transrec_replacement(M,MH,i);  relativize2(M,MH,H);
   1.198 +     "[|transrec_replacement(M,MH,i);  relation2(M,MH,H);
   1.199  	Ord(i);  M(i);  
   1.200  	\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
   1.201        ==> M(transrec(i,H))"
   1.202 @@ -770,7 +769,7 @@
   1.203   prefer 2 apply (blast intro: transM)
   1.204  apply (simp add: is_nth_def nth_eq_hd_iterates_tl nat_into_M
   1.205                   tl'_closed iterates_tl'_closed 
   1.206 -                 iterates_abs [OF _ relativize1_tl] nth_replacement)
   1.207 +                 iterates_abs [OF _ relation1_tl] nth_replacement)
   1.208  done
   1.209  
   1.210  
   1.211 @@ -848,14 +847,14 @@
   1.212        (\<forall>x[M]. mem_formula(M,x) --> is_Forall(M,x,p) --> is_d(x,z))"
   1.213  
   1.214  lemma (in M_datatypes) formula_case_abs [simp]: 
   1.215 -     "[| Relativize2(M,nat,nat,is_a,a); Relativize2(M,nat,nat,is_b,b); 
   1.216 -         Relativize2(M,formula,formula,is_c,c); Relativize1(M,formula,is_d,d); 
   1.217 +     "[| Relation2(M,nat,nat,is_a,a); Relation2(M,nat,nat,is_b,b); 
   1.218 +         Relation2(M,formula,formula,is_c,c); Relation1(M,formula,is_d,d); 
   1.219           p \<in> formula; M(z) |] 
   1.220        ==> is_formula_case(M,is_a,is_b,is_c,is_d,p,z) <-> 
   1.221            z = formula_case(a,b,c,d,p)"
   1.222  apply (simp add: formula_into_M is_formula_case_def)
   1.223  apply (erule formula.cases) 
   1.224 -   apply (simp_all add: Relativize1_def Relativize2_def) 
   1.225 +   apply (simp_all add: Relation1_def Relation2_def) 
   1.226  done
   1.227  
   1.228  lemma (in M_datatypes) formula_case_closed [intro,simp]:
   1.229 @@ -935,18 +934,18 @@
   1.230  
   1.231  text{*Sufficient conditions to relative the instance of @{term formula_case}
   1.232        in @{term formula_rec}*}
   1.233 -lemma (in M_datatypes) Relativize1_formula_rec_case:
   1.234 -     "[|Relativize2(M, nat, nat, is_a, a);
   1.235 -        Relativize2(M, nat, nat, is_b, b);
   1.236 -        Relativize2 (M, formula, formula, 
   1.237 +lemma (in M_datatypes) Relation1_formula_rec_case:
   1.238 +     "[|Relation2(M, nat, nat, is_a, a);
   1.239 +        Relation2(M, nat, nat, is_b, b);
   1.240 +        Relation2 (M, formula, formula, 
   1.241             is_c, \<lambda>u v. c(u, v, h`succ(depth(u))`u, h`succ(depth(v))`v));
   1.242 -        Relativize1(M, formula, 
   1.243 +        Relation1(M, formula, 
   1.244             is_d, \<lambda>u. d(u, h ` succ(depth(u)) ` u));
   1.245   	M(h) |] 
   1.246 -      ==> Relativize1(M, formula,
   1.247 +      ==> Relation1(M, formula,
   1.248                           is_formula_case (M, is_a, is_b, is_c, is_d),
   1.249                           formula_rec_case(a, b, c, d, h))"
   1.250 -apply (simp (no_asm) add: formula_rec_case_def Relativize1_def) 
   1.251 +apply (simp (no_asm) add: formula_rec_case_def Relation1_def) 
   1.252  apply (simp add: formula_case_abs) 
   1.253  done
   1.254  
   1.255 @@ -963,19 +962,19 @@
   1.256  	 (M, fml, is_formula_case (M, is_a, is_b, is_c(f), is_d(f)), z)"
   1.257  
   1.258    assumes a_closed: "[|x\<in>nat; y\<in>nat|] ==> M(a(x,y))"
   1.259 -      and a_rel:    "Relativize2(M, nat, nat, is_a, a)"
   1.260 +      and a_rel:    "Relation2(M, nat, nat, is_a, a)"
   1.261        and b_closed: "[|x\<in>nat; y\<in>nat|] ==> M(b(x,y))"
   1.262 -      and b_rel:    "Relativize2(M, nat, nat, is_b, b)"
   1.263 +      and b_rel:    "Relation2(M, nat, nat, is_b, b)"
   1.264        and c_closed: "[|x \<in> formula; y \<in> formula; M(gx); M(gy)|]
   1.265                       ==> M(c(x, y, gx, gy))"
   1.266        and c_rel:
   1.267           "M(f) ==> 
   1.268 -          Relativize2 (M, formula, formula, is_c(f),
   1.269 +          Relation2 (M, formula, formula, is_c(f),
   1.270               \<lambda>u v. c(u, v, f ` succ(depth(u)) ` u, f ` succ(depth(v)) ` v))"
   1.271        and d_closed: "[|x \<in> formula; M(gx)|] ==> M(d(x, gx))"
   1.272        and d_rel:
   1.273           "M(f) ==> 
   1.274 -          Relativize1(M, formula, is_d(f), \<lambda>u. d(u, f ` succ(depth(u)) ` u))"
   1.275 +          Relation1(M, formula, is_d(f), \<lambda>u. d(u, f ` succ(depth(u)) ` u))"
   1.276        and fr_replace: "n \<in> nat ==> transrec_replacement(M,MH,n)"
   1.277        and fr_lam_replace:
   1.278             "M(g) ==>
   1.279 @@ -992,12 +991,12 @@
   1.280  by (simp add: lam_closed2 fr_lam_replace formula_rec_case_closed)
   1.281  
   1.282  lemma (in Formula_Rec) MH_rel2:
   1.283 -     "relativize2 (M, MH,
   1.284 +     "relation2 (M, MH,
   1.285               \<lambda>x h. Lambda (formula, formula_rec_case(a,b,c,d,h)))"
   1.286 -apply (simp add: relativize2_def MH_def, clarify) 
   1.287 +apply (simp add: relation2_def MH_def, clarify) 
   1.288  apply (rule lambda_abs2) 
   1.289  apply (rule fr_lam_replace, assumption)
   1.290 -apply (rule Relativize1_formula_rec_case)  
   1.291 +apply (rule Relation1_formula_rec_case)  
   1.292  apply (simp_all add: a_rel b_rel c_rel d_rel formula_rec_case_closed) 
   1.293  done
   1.294