src/ZF/Constructible/Datatype_absolute.thy
changeset 13385 31df66ca0780
parent 13382 b37764a46b16
child 13386 f3e9e8b21aba
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Tue Jul 16 20:25:21 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Wed Jul 17 15:48:54 2002 +0200
     1.3 @@ -6,21 +6,43 @@
     1.4  subsection{*The lfp of a continuous function can be expressed as a union*}
     1.5  
     1.6  constdefs
     1.7 -  contin :: "[i=>i]=>o"
     1.8 -   "contin(h) == (\<forall>A. A\<noteq>0 --> h(\<Union>A) = (\<Union>X\<in>A. h(X)))"
     1.9 +  directed :: "i=>o"
    1.10 +   "directed(A) == A\<noteq>0 & (\<forall>x\<in>A. \<forall>y\<in>A. x \<union> y \<in> A)"
    1.11 +
    1.12 +  contin :: "(i=>i) => o"
    1.13 +   "contin(h) == (\<forall>A. directed(A) --> h(\<Union>A) = (\<Union>X\<in>A. h(X)))"
    1.14  
    1.15  lemma bnd_mono_iterates_subset: "[|bnd_mono(D, h); n \<in> nat|] ==> h^n (0) <= D"
    1.16  apply (induct_tac n) 
    1.17   apply (simp_all add: bnd_mono_def, blast) 
    1.18  done
    1.19  
    1.20 +lemma bnd_mono_increasing [rule_format]:
    1.21 +     "[|i \<in> nat; j \<in> nat; bnd_mono(D,h)|] ==> i \<le> j --> h^i(0) \<subseteq> h^j(0)"
    1.22 +apply (rule_tac m=i and n=j in diff_induct, simp_all)
    1.23 +apply (blast del: subsetI
    1.24 +	     intro: bnd_mono_iterates_subset bnd_monoD2 [of concl: h] ) 
    1.25 +done
    1.26 +
    1.27 +lemma directed_iterates: "bnd_mono(D,h) ==> directed({h^n (0). n\<in>nat})"
    1.28 +apply (simp add: directed_def, clarify) 
    1.29 +apply (rename_tac i j)
    1.30 +apply (rule_tac x="i \<union> j" in bexI) 
    1.31 +apply (rule_tac i = i and j = j in Ord_linear_le)
    1.32 +apply (simp_all add: subset_Un_iff [THEN iffD1] le_imp_subset
    1.33 +                     subset_Un_iff2 [THEN iffD1])
    1.34 +apply (simp_all add: subset_Un_iff [THEN iff_sym] bnd_mono_increasing
    1.35 +                     subset_Un_iff2 [THEN iff_sym])
    1.36 +done
    1.37 +
    1.38  
    1.39  lemma contin_iterates_eq: 
    1.40 -    "contin(h) \<Longrightarrow> h(\<Union>n\<in>nat. h^n (0)) = (\<Union>n\<in>nat. h^n (0))"
    1.41 -apply (simp add: contin_def) 
    1.42 +    "[|bnd_mono(D, h); contin(h)|] 
    1.43 +     ==> h(\<Union>n\<in>nat. h^n (0)) = (\<Union>n\<in>nat. h^n (0))"
    1.44 +apply (simp add: contin_def directed_iterates) 
    1.45  apply (rule trans) 
    1.46  apply (rule equalityI) 
    1.47 - apply (simp_all add: UN_subset_iff) 
    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 @@ -51,20 +73,53 @@
    1.53            intro: lfp_subset_Union Union_subset_lfp)
    1.54  
    1.55  
    1.56 +subsubsection{*Some Standard Datatype Constructions Preserve Continuity*}
    1.57 +
    1.58 +lemma contin_imp_mono: "[|X\<subseteq>Y; contin(F)|] ==> F(X) \<subseteq> F(Y)"
    1.59 +apply (simp add: contin_def) 
    1.60 +apply (drule_tac x="{X,Y}" in spec) 
    1.61 +apply (simp add: directed_def subset_Un_iff2 Un_commute) 
    1.62 +done
    1.63 +
    1.64 +lemma sum_contin: "[|contin(F); contin(G)|] ==> contin(\<lambda>X. F(X) + G(X))"
    1.65 +by (simp add: contin_def, blast)
    1.66 +
    1.67 +lemma prod_contin: "[|contin(F); contin(G)|] ==> contin(\<lambda>X. F(X) * G(X))" 
    1.68 +apply (subgoal_tac "\<forall>B C. F(B) \<subseteq> F(B \<union> C)")
    1.69 + prefer 2 apply (simp add: Un_upper1 contin_imp_mono) 
    1.70 +apply (subgoal_tac "\<forall>B C. G(C) \<subseteq> G(B \<union> C)")
    1.71 + prefer 2 apply (simp add: Un_upper2 contin_imp_mono) 
    1.72 +apply (simp add: contin_def, clarify) 
    1.73 +apply (rule equalityI) 
    1.74 + prefer 2 apply blast 
    1.75 +apply clarify 
    1.76 +apply (rename_tac B C) 
    1.77 +apply (rule_tac a="B \<union> C" in UN_I) 
    1.78 + apply (simp add: directed_def, blast)  
    1.79 +done
    1.80 +
    1.81 +lemma const_contin: "contin(\<lambda>X. A)"
    1.82 +by (simp add: contin_def directed_def)
    1.83 +
    1.84 +lemma id_contin: "contin(\<lambda>X. X)"
    1.85 +by (simp add: contin_def)
    1.86 +
    1.87 +
    1.88 +
    1.89  subsection {*lists without univ*}
    1.90  
    1.91 -lemmas datatype_univs = A_into_univ Inl_in_univ Inr_in_univ 
    1.92 -                        Pair_in_univ zero_in_univ
    1.93 +lemmas datatype_univs = Inl_in_univ Inr_in_univ 
    1.94 +                        Pair_in_univ nat_into_univ A_into_univ 
    1.95  
    1.96  lemma list_fun_bnd_mono: "bnd_mono(univ(A), \<lambda>X. {0} + A*X)"
    1.97  apply (rule bnd_monoI)
    1.98   apply (intro subset_refl zero_subset_univ A_subset_univ 
    1.99  	      sum_subset_univ Sigma_subset_univ) 
   1.100 - apply (blast intro!: subset_refl sum_mono Sigma_mono del: subsetI)
   1.101 +apply (rule subset_refl sum_mono Sigma_mono | assumption)+
   1.102  done
   1.103  
   1.104  lemma list_fun_contin: "contin(\<lambda>X. {0} + A*X)"
   1.105 -by (simp add: contin_def, blast)
   1.106 +by (intro sum_contin prod_contin id_contin const_contin) 
   1.107  
   1.108  text{*Re-expresses lists using sum and product*}
   1.109  lemma list_eq_lfp2: "list(A) = lfp(univ(A), \<lambda>X. {0} + A*X)"