src/ZF/Constructible/Datatype_absolute.thy
changeset 13386 f3e9e8b21aba
parent 13385 31df66ca0780
child 13395 4eb948d1eb4e
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Wed Jul 17 15:48:54 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Wed Jul 17 16:41:32 2002 +0200
     1.3 @@ -106,45 +106,6 @@
     1.4  
     1.5  
     1.6  
     1.7 -subsection {*lists without univ*}
     1.8 -
     1.9 -lemmas datatype_univs = Inl_in_univ Inr_in_univ 
    1.10 -                        Pair_in_univ nat_into_univ A_into_univ 
    1.11 -
    1.12 -lemma list_fun_bnd_mono: "bnd_mono(univ(A), \<lambda>X. {0} + A*X)"
    1.13 -apply (rule bnd_monoI)
    1.14 - apply (intro subset_refl zero_subset_univ A_subset_univ 
    1.15 -	      sum_subset_univ Sigma_subset_univ) 
    1.16 -apply (rule subset_refl sum_mono Sigma_mono | assumption)+
    1.17 -done
    1.18 -
    1.19 -lemma list_fun_contin: "contin(\<lambda>X. {0} + A*X)"
    1.20 -by (intro sum_contin prod_contin id_contin const_contin) 
    1.21 -
    1.22 -text{*Re-expresses lists using sum and product*}
    1.23 -lemma list_eq_lfp2: "list(A) = lfp(univ(A), \<lambda>X. {0} + A*X)"
    1.24 -apply (simp add: list_def) 
    1.25 -apply (rule equalityI) 
    1.26 - apply (rule lfp_lowerbound) 
    1.27 -  prefer 2 apply (rule lfp_subset)
    1.28 - apply (clarify, subst lfp_unfold [OF list_fun_bnd_mono])
    1.29 - apply (simp add: Nil_def Cons_def)
    1.30 - apply blast 
    1.31 -txt{*Opposite inclusion*}
    1.32 -apply (rule lfp_lowerbound) 
    1.33 - prefer 2 apply (rule lfp_subset) 
    1.34 -apply (clarify, subst lfp_unfold [OF list.bnd_mono]) 
    1.35 -apply (simp add: Nil_def Cons_def)
    1.36 -apply (blast intro: datatype_univs
    1.37 -             dest: lfp_subset [THEN subsetD])
    1.38 -done
    1.39 -
    1.40 -text{*Re-expresses lists using "iterates", no univ.*}
    1.41 -lemma list_eq_Union:
    1.42 -     "list(A) = (\<Union>n\<in>nat. (\<lambda>X. {0} + A*X) ^ n (0))"
    1.43 -by (simp add: list_eq_lfp2 lfp_eq_Union list_fun_bnd_mono list_fun_contin)
    1.44 -
    1.45 -
    1.46  subsection {*Absoluteness for "Iterates"*}
    1.47  
    1.48  constdefs
    1.49 @@ -198,6 +159,45 @@
    1.50  done
    1.51  
    1.52  
    1.53 +subsection {*lists without univ*}
    1.54 +
    1.55 +lemmas datatype_univs = Inl_in_univ Inr_in_univ 
    1.56 +                        Pair_in_univ nat_into_univ A_into_univ 
    1.57 +
    1.58 +lemma list_fun_bnd_mono: "bnd_mono(univ(A), \<lambda>X. {0} + A*X)"
    1.59 +apply (rule bnd_monoI)
    1.60 + apply (intro subset_refl zero_subset_univ A_subset_univ 
    1.61 +	      sum_subset_univ Sigma_subset_univ) 
    1.62 +apply (rule subset_refl sum_mono Sigma_mono | assumption)+
    1.63 +done
    1.64 +
    1.65 +lemma list_fun_contin: "contin(\<lambda>X. {0} + A*X)"
    1.66 +by (intro sum_contin prod_contin id_contin const_contin) 
    1.67 +
    1.68 +text{*Re-expresses lists using sum and product*}
    1.69 +lemma list_eq_lfp2: "list(A) = lfp(univ(A), \<lambda>X. {0} + A*X)"
    1.70 +apply (simp add: list_def) 
    1.71 +apply (rule equalityI) 
    1.72 + apply (rule lfp_lowerbound) 
    1.73 +  prefer 2 apply (rule lfp_subset)
    1.74 + apply (clarify, subst lfp_unfold [OF list_fun_bnd_mono])
    1.75 + apply (simp add: Nil_def Cons_def)
    1.76 + apply blast 
    1.77 +txt{*Opposite inclusion*}
    1.78 +apply (rule lfp_lowerbound) 
    1.79 + prefer 2 apply (rule lfp_subset) 
    1.80 +apply (clarify, subst lfp_unfold [OF list.bnd_mono]) 
    1.81 +apply (simp add: Nil_def Cons_def)
    1.82 +apply (blast intro: datatype_univs
    1.83 +             dest: lfp_subset [THEN subsetD])
    1.84 +done
    1.85 +
    1.86 +text{*Re-expresses lists using "iterates", no univ.*}
    1.87 +lemma list_eq_Union:
    1.88 +     "list(A) = (\<Union>n\<in>nat. (\<lambda>X. {0} + A*X) ^ n (0))"
    1.89 +by (simp add: list_eq_lfp2 lfp_eq_Union list_fun_bnd_mono list_fun_contin)
    1.90 +
    1.91 +
    1.92  constdefs
    1.93    is_list_functor :: "[i=>o,i,i,i] => o"
    1.94      "is_list_functor(M,A,X,Z) == 
    1.95 @@ -209,6 +209,65 @@
    1.96  by (simp add: is_list_functor_def singleton_0 nat_into_M)
    1.97  
    1.98  
    1.99 +subsection {*formulas without univ*}
   1.100 +
   1.101 +lemma formula_fun_bnd_mono:
   1.102 +     "bnd_mono(univ(0), \<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X)))"
   1.103 +apply (rule bnd_monoI)
   1.104 + apply (intro subset_refl zero_subset_univ A_subset_univ 
   1.105 +	      sum_subset_univ Sigma_subset_univ nat_subset_univ) 
   1.106 +apply (rule subset_refl sum_mono Sigma_mono | assumption)+
   1.107 +done
   1.108 +
   1.109 +lemma formula_fun_contin:
   1.110 +     "contin(\<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X)))"
   1.111 +by (intro sum_contin prod_contin id_contin const_contin) 
   1.112 +
   1.113 +
   1.114 +text{*Re-expresses formulas using sum and product*}
   1.115 +lemma formula_eq_lfp2:
   1.116 +    "formula = lfp(univ(0), \<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X)))"
   1.117 +apply (simp add: formula_def) 
   1.118 +apply (rule equalityI) 
   1.119 + apply (rule lfp_lowerbound) 
   1.120 +  prefer 2 apply (rule lfp_subset)
   1.121 + apply (clarify, subst lfp_unfold [OF formula_fun_bnd_mono])
   1.122 + apply (simp add: Member_def Equal_def Neg_def And_def Forall_def)
   1.123 + apply blast 
   1.124 +txt{*Opposite inclusion*}
   1.125 +apply (rule lfp_lowerbound) 
   1.126 + prefer 2 apply (rule lfp_subset, clarify) 
   1.127 +apply (subst lfp_unfold [OF formula.bnd_mono, simplified]) 
   1.128 +apply (simp add: Member_def Equal_def Neg_def And_def Forall_def)  
   1.129 +apply (elim sumE SigmaE, simp_all) 
   1.130 +apply (blast intro: datatype_univs dest: lfp_subset [THEN subsetD])+  
   1.131 +done
   1.132 +
   1.133 +text{*Re-expresses formulas using "iterates", no univ.*}
   1.134 +lemma formula_eq_Union:
   1.135 +     "formula = 
   1.136 +      (\<Union>n\<in>nat. (\<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X))) ^ n (0))"
   1.137 +by (simp add: formula_eq_lfp2 lfp_eq_Union formula_fun_bnd_mono 
   1.138 +              formula_fun_contin)
   1.139 +
   1.140 +
   1.141 +constdefs
   1.142 +  is_formula_functor :: "[i=>o,i,i] => o"
   1.143 +    "is_formula_functor(M,X,Z) == 
   1.144 +        \<exists>nat'[M]. \<exists>natnat[M]. \<exists>natnatsum[M]. \<exists>XX[M]. \<exists>X3[M]. \<exists>X4[M]. 
   1.145 +          omega(M,nat') & cartprod(M,nat',nat',natnat) & 
   1.146 +          is_sum(M,natnat,natnat,natnatsum) &
   1.147 +          cartprod(M,X,X,XX) & is_sum(M,XX,X,X3) & is_sum(M,X,X3,X4) &
   1.148 +          is_sum(M,natnatsum,X4,Z)"
   1.149 +
   1.150 +lemma (in M_axioms) formula_functor_abs [simp]: 
   1.151 +     "[| M(X); M(Z) |] 
   1.152 +      ==> is_formula_functor(M,X,Z) <-> 
   1.153 +          Z = ((nat*nat) + (nat*nat)) + (X + (X*X + X))"
   1.154 +by (simp add: is_formula_functor_def) 
   1.155 +
   1.156 +
   1.157 +subsection{*@{term M} Contains the List and Formula Datatypes*}
   1.158  locale (open) M_datatypes = M_wfrank +
   1.159   assumes list_replacement1: 
   1.160     "M(A) ==> iterates_replacement(M, is_list_functor(M,A), 0)"
   1.161 @@ -218,6 +277,14 @@
   1.162                 (\<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
   1.163                 is_wfrec(M, iterates_MH(M,is_list_functor(M,A), 0), 
   1.164                          msn, n, y)))"
   1.165 +  and formula_replacement1: 
   1.166 +   "iterates_replacement(M, is_formula_functor(M), 0)"
   1.167 +  and formula_replacement2: 
   1.168 +   "strong_replacement(M, 
   1.169 +         \<lambda>n y. n\<in>nat & 
   1.170 +               (\<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
   1.171 +               is_wfrec(M, iterates_MH(M,is_formula_functor(M), 0), 
   1.172 +                        msn, n, y)))"
   1.173  
   1.174  lemma (in M_datatypes) list_replacement2': 
   1.175    "M(A) ==> strong_replacement(M, \<lambda>n y. n\<in>nat & y = (\<lambda>X. {0} + A * X)^n (0))"
   1.176 @@ -235,4 +302,20 @@
   1.177                 iterates_closed [of "is_list_functor(M,A)"])
   1.178  
   1.179  
   1.180 +lemma (in M_datatypes) formula_replacement2': 
   1.181 +  "strong_replacement(M, \<lambda>n y. n\<in>nat & y = (\<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X)))^n (0))"
   1.182 +apply (insert formula_replacement2) 
   1.183 +apply (rule strong_replacement_cong [THEN iffD1])  
   1.184 +apply (rule conj_cong [OF iff_refl iterates_abs [of "is_formula_functor(M)"]]) 
   1.185 +apply (simp_all add: formula_replacement1 relativize1_def) 
   1.186 +done
   1.187 +
   1.188 +lemma (in M_datatypes) formula_closed [intro,simp]:
   1.189 +     "M(formula)"
   1.190 +apply (insert formula_replacement1)
   1.191 +apply  (simp add: RepFun_closed2 formula_eq_Union 
   1.192 +                  formula_replacement2' relativize1_def
   1.193 +                  iterates_closed [of "is_formula_functor(M)"])
   1.194 +done
   1.195 +
   1.196  end