src/ZF/Constructible/Datatype_absolute.thy
changeset 13268 240509babf00
child 13269 3ba9be497c33
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Mon Jul 01 18:16:18 2002 +0200
     1.3 @@ -0,0 +1,173 @@
     1.4 +theory Datatype_absolute = WF_absolute:
     1.5 +
     1.6 +(*Epsilon.thy*)
     1.7 +lemma succ_subset_eclose_sing: "succ(i) <= eclose({i})"
     1.8 +apply (insert arg_subset_eclose [of "{i}"], simp) 
     1.9 +apply (frule eclose_subset, blast) 
    1.10 +done
    1.11 +
    1.12 +lemma eclose_sing_Ord_eq: "Ord(i) ==> eclose({i}) = succ(i)"
    1.13 +apply (rule equalityI)
    1.14 +apply (erule eclose_sing_Ord)  
    1.15 +apply (rule succ_subset_eclose_sing) 
    1.16 +done
    1.17 +
    1.18 +(*Ordinal.thy*)
    1.19 +lemma relation_Memrel: "relation(Memrel(A))"
    1.20 +by (simp add: relation_def Memrel_def, blast)
    1.21 +
    1.22 +lemma (in M_axioms) nat_case_closed:
    1.23 +  "[|M(k); M(a); \<forall>m[M]. M(b(m))|] ==> M(nat_case(a,b,k))"
    1.24 +apply (case_tac "k=0", simp) 
    1.25 +apply (case_tac "\<exists>m. k = succ(m)")
    1.26 +apply force 
    1.27 +apply (simp add: nat_case_def) 
    1.28 +done
    1.29 +
    1.30 +
    1.31 +subsection{*The lfp of a continuous function can be expressed as a union*}
    1.32 +
    1.33 +constdefs
    1.34 +  contin :: "[i=>i]=>o"
    1.35 +   "contin(h) == (\<forall>A. A\<noteq>0 --> h(\<Union>A) = (\<Union>X\<in>A. h(X)))"
    1.36 +
    1.37 +lemma bnd_mono_iterates_subset: "[|bnd_mono(D, h); n \<in> nat|] ==> h^n (0) <= D"
    1.38 +apply (induct_tac n) 
    1.39 + apply (simp_all add: bnd_mono_def, blast) 
    1.40 +done
    1.41 +
    1.42 +
    1.43 +lemma contin_iterates_eq: 
    1.44 +    "contin(h) \<Longrightarrow> h(\<Union>n\<in>nat. h^n (0)) = (\<Union>n\<in>nat. h^n (0))"
    1.45 +apply (simp add: contin_def) 
    1.46 +apply (rule trans) 
    1.47 +apply (rule equalityI) 
    1.48 + apply (simp_all add: UN_subset_iff) 
    1.49 + apply safe
    1.50 + apply (erule_tac [2] natE) 
    1.51 +  apply (rule_tac a="succ(x)" in UN_I) 
    1.52 +   apply simp_all 
    1.53 +apply blast 
    1.54 +done
    1.55 +
    1.56 +lemma lfp_subset_Union:
    1.57 +     "[|bnd_mono(D, h); contin(h)|] ==> lfp(D,h) <= (\<Union>n\<in>nat. h^n(0))"
    1.58 +apply (rule lfp_lowerbound) 
    1.59 + apply (simp add: contin_iterates_eq) 
    1.60 +apply (simp add: contin_def bnd_mono_iterates_subset UN_subset_iff) 
    1.61 +done
    1.62 +
    1.63 +lemma Union_subset_lfp:
    1.64 +     "bnd_mono(D,h) ==> (\<Union>n\<in>nat. h^n(0)) <= lfp(D,h)"
    1.65 +apply (simp add: UN_subset_iff)
    1.66 +apply (rule ballI)  
    1.67 +apply (induct_tac x, simp_all) 
    1.68 +apply (rule subset_trans [of _ "h(lfp(D,h))"])
    1.69 + apply (blast dest: bnd_monoD2 [OF _ _ lfp_subset] )  
    1.70 +apply (erule lfp_lemma2) 
    1.71 +done
    1.72 +
    1.73 +lemma lfp_eq_Union:
    1.74 +     "[|bnd_mono(D, h); contin(h)|] ==> lfp(D,h) = (\<Union>n\<in>nat. h^n(0))"
    1.75 +by (blast del: subsetI 
    1.76 +          intro: lfp_subset_Union Union_subset_lfp)
    1.77 +
    1.78 +
    1.79 +subsection {*lists without univ*}
    1.80 +
    1.81 +lemmas datatype_univs = A_into_univ Inl_in_univ Inr_in_univ 
    1.82 +                        Pair_in_univ zero_in_univ
    1.83 +
    1.84 +lemma list_fun_bnd_mono: "bnd_mono(univ(A), \<lambda>X. {0} + A*X)"
    1.85 +apply (rule bnd_monoI)
    1.86 + apply (intro subset_refl zero_subset_univ A_subset_univ 
    1.87 +	      sum_subset_univ Sigma_subset_univ) 
    1.88 + apply (blast intro!: subset_refl sum_mono Sigma_mono del: subsetI)
    1.89 +done
    1.90 +
    1.91 +lemma list_fun_contin: "contin(\<lambda>X. {0} + A*X)"
    1.92 +by (simp add: contin_def, blast)
    1.93 +
    1.94 +text{*Re-expresses lists using sum and product*}
    1.95 +lemma list_eq_lfp2: "list(A) = lfp(univ(A), \<lambda>X. {0} + A*X)"
    1.96 +apply (simp add: list_def) 
    1.97 +apply (rule equalityI) 
    1.98 + apply (rule lfp_lowerbound) 
    1.99 +  prefer 2 apply (rule lfp_subset)
   1.100 + apply (clarify, subst lfp_unfold [OF list_fun_bnd_mono])
   1.101 + apply (simp add: Nil_def Cons_def)
   1.102 + apply blast 
   1.103 +txt{*Opposite inclusion*}
   1.104 +apply (rule lfp_lowerbound) 
   1.105 + prefer 2 apply (rule lfp_subset) 
   1.106 +apply (clarify, subst lfp_unfold [OF list.bnd_mono]) 
   1.107 +apply (simp add: Nil_def Cons_def)
   1.108 +apply (blast intro: datatype_univs
   1.109 +             dest: lfp_subset [THEN subsetD])
   1.110 +done
   1.111 +
   1.112 +text{*Re-expresses lists using "iterates", no univ.*}
   1.113 +lemma list_eq_Union:
   1.114 +     "list(A) = (\<Union>n\<in>nat. (\<lambda>X. {0} + A*X) ^ n (0))"
   1.115 +by (simp add: list_eq_lfp2 lfp_eq_Union list_fun_bnd_mono list_fun_contin)
   1.116 +
   1.117 +
   1.118 +subsection {*Absoluteness for "Iterates"*}
   1.119 +
   1.120 +lemma (in M_trancl) iterates_relativize:
   1.121 +  "[|n \<in> nat; M(v); \<forall>x[M]. M(F(x));
   1.122 +     strong_replacement(M, 
   1.123 +       \<lambda>x z. \<exists>y[M]. \<exists>g[M]. pair(M, x, y, z) &
   1.124 +              is_recfun (Memrel(succ(n)), x,
   1.125 +                         \<lambda>n f. nat_case(v, \<lambda>m. F(f`m), n), g) &
   1.126 +              y = nat_case(v, \<lambda>m. F(g`m), x))|] 
   1.127 +   ==> iterates(F,n,v) = z <-> 
   1.128 +       (\<exists>g[M]. is_recfun(Memrel(succ(n)), n, 
   1.129 +                             \<lambda>n g. nat_case(v, \<lambda>m. F(g`m), n), g) &
   1.130 +            z = nat_case(v, \<lambda>m. F(g`m), n))"
   1.131 +by (simp add: iterates_nat_def recursor_def transrec_def 
   1.132 +              eclose_sing_Ord_eq trans_wfrec_relativize nat_into_M
   1.133 +              wf_Memrel trans_Memrel relation_Memrel nat_case_closed)
   1.134 +
   1.135 +
   1.136 +lemma (in M_wfrank) iterates_closed [intro,simp]:
   1.137 +  "[|n \<in> nat; M(v); \<forall>x[M]. M(F(x));
   1.138 +     strong_replacement(M, 
   1.139 +       \<lambda>x z. \<exists>y[M]. \<exists>g[M]. pair(M, x, y, z) &
   1.140 +              is_recfun (Memrel(succ(n)), x,
   1.141 +                         \<lambda>n f. nat_case(v, \<lambda>m. F(f`m), n), g) &
   1.142 +              y = nat_case(v, \<lambda>m. F(g`m), x))|] 
   1.143 +   ==> M(iterates(F,n,v))"
   1.144 +by (simp add: iterates_nat_def recursor_def transrec_def 
   1.145 +              eclose_sing_Ord_eq trans_wfrec_closed nat_into_M
   1.146 +              wf_Memrel trans_Memrel relation_Memrel nat_case_closed)
   1.147 +
   1.148 +
   1.149 +locale M_datatypes = M_wfrank +
   1.150 +(*THEY NEED RELATIVIZATION*)
   1.151 +  assumes list_replacement1: 
   1.152 +	   "[|M(A); n \<in> nat|] ==> 
   1.153 +	    strong_replacement(M, 
   1.154 +	      \<lambda>x z. \<exists>y[M]. \<exists>g[M]. pair(M, x, y, z) &
   1.155 +		     is_recfun (Memrel(succ(n)), x,
   1.156 +				\<lambda>n f. nat_case(0, \<lambda>m. {0} + A \<times> f`m, n), g) &
   1.157 +		     y = nat_case(0, \<lambda>m. {0} + A \<times> g`m, x))"
   1.158 +      and list_replacement2': 
   1.159 +           "M(A) ==> strong_replacement(M, \<lambda>x y. y = (\<lambda>X. {0} + A \<times> X)^x (0))"
   1.160 +
   1.161 +
   1.162 +lemma (in M_datatypes) list_replacement1':
   1.163 +  "[|M(A); n \<in> nat|]
   1.164 +   ==> strong_replacement
   1.165 +	  (M, \<lambda>x y. \<exists>z[M]. \<exists>g[M]. y = \<langle>x, z\<rangle> &
   1.166 +               is_recfun (Memrel(succ(n)), x,
   1.167 +		          \<lambda>n f. nat_case(0, \<lambda>m. {0} + A \<times> f ` m, n), g) &
   1.168 + 	       z = nat_case(0, \<lambda>m. {0} + A \<times> g ` m, x))"
   1.169 +by (insert list_replacement1, simp) 
   1.170 +
   1.171 +
   1.172 +lemma (in M_datatypes) list_closed [intro,simp]:
   1.173 +     "M(A) ==> M(list(A))"
   1.174 +by (simp add: list_eq_Union list_replacement1' list_replacement2')
   1.175 +
   1.176 +end