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.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.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.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)"
```