src/HOL/Complete_Partial_Order.thy
 changeset 46041 1e3ff542e83e parent 40252 029400b6c893 child 53361 1cb7d3c0cf31
```     1.1 --- a/src/HOL/Complete_Partial_Order.thy	Thu Dec 29 17:43:54 2011 +0100
1.2 +++ b/src/HOL/Complete_Partial_Order.thy	Thu Dec 29 18:54:07 2011 +0100
1.3 @@ -57,10 +57,9 @@
1.4    empty set is a chain, so every ccpo must have a bottom element.
1.5  *}
1.6
1.7 -class ccpo = order +
1.8 -  fixes lub :: "'a set \<Rightarrow> 'a"
1.9 -  assumes lub_upper: "chain (op \<le>) A \<Longrightarrow> x \<in> A \<Longrightarrow> x \<le> lub A"
1.10 -  assumes lub_least: "chain (op \<le>) A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> lub A \<le> z"
1.11 +class ccpo = order + Sup +
1.12 +  assumes ccpo_Sup_upper: "\<lbrakk>chain (op \<le>) A; x \<in> A\<rbrakk> \<Longrightarrow> x \<le> Sup A"
1.13 +  assumes ccpo_Sup_least: "\<lbrakk>chain (op \<le>) A; \<And>x. x \<in> A \<Longrightarrow> x \<le> z\<rbrakk> \<Longrightarrow> Sup A \<le> z"
1.14  begin
1.15
1.16  subsection {* Transfinite iteration of a function *}
1.17 @@ -69,12 +68,12 @@
1.18  for f :: "'a \<Rightarrow> 'a"
1.19  where
1.20    step: "x \<in> iterates f \<Longrightarrow> f x \<in> iterates f"
1.21 -| lub: "chain (op \<le>) M \<Longrightarrow> \<forall>x\<in>M. x \<in> iterates f \<Longrightarrow> lub M \<in> iterates f"
1.22 +| Sup: "chain (op \<le>) M \<Longrightarrow> \<forall>x\<in>M. x \<in> iterates f \<Longrightarrow> Sup M \<in> iterates f"
1.23
1.24  lemma iterates_le_f:
1.25    "x \<in> iterates f \<Longrightarrow> monotone (op \<le>) (op \<le>) f \<Longrightarrow> x \<le> f x"
1.26  by (induct x rule: iterates.induct)
1.27 -  (force dest: monotoneD intro!: lub_upper lub_least)+
1.28 +  (force dest: monotoneD intro!: ccpo_Sup_upper ccpo_Sup_least)+
1.29
1.30  lemma chain_iterates:
1.31    assumes f: "monotone (op \<le>) (op \<le>) f"
1.32 @@ -89,33 +88,33 @@
1.33      proof (induct y rule: iterates.induct)
1.34        case (step y) with IH f show ?case by (auto dest: monotoneD)
1.35      next
1.36 -      case (lub M)
1.37 +      case (Sup M)
1.38        then have chM: "chain (op \<le>) M"
1.39          and IH': "\<And>z. z \<in> M \<Longrightarrow> f x \<le> z \<or> z \<le> f x" by auto
1.40 -      show "f x \<le> lub M \<or> lub M \<le> f x"
1.41 +      show "f x \<le> Sup M \<or> Sup M \<le> f x"
1.42        proof (cases "\<exists>z\<in>M. f x \<le> z")
1.43 -        case True then have "f x \<le> lub M"
1.44 +        case True then have "f x \<le> Sup M"
1.45            apply rule
1.46            apply (erule order_trans)
1.47 -          by (rule lub_upper[OF chM])
1.48 +          by (rule ccpo_Sup_upper[OF chM])
1.49          thus ?thesis ..
1.50        next
1.51          case False with IH'
1.52 -        show ?thesis by (auto intro: lub_least[OF chM])
1.53 +        show ?thesis by (auto intro: ccpo_Sup_least[OF chM])
1.54        qed
1.55      qed
1.56    next
1.57 -    case (lub M y)
1.58 +    case (Sup M y)
1.59      show ?case
1.60      proof (cases "\<exists>x\<in>M. y \<le> x")
1.61 -      case True then have "y \<le> lub M"
1.62 +      case True then have "y \<le> Sup M"
1.63          apply rule
1.64          apply (erule order_trans)
1.65 -        by (rule lub_upper[OF lub(1)])
1.66 +        by (rule ccpo_Sup_upper[OF Sup(1)])
1.67        thus ?thesis ..
1.68      next
1.69 -      case False with lub
1.70 -      show ?thesis by (auto intro: lub_least)
1.71 +      case False with Sup
1.72 +      show ?thesis by (auto intro: ccpo_Sup_least)
1.73      qed
1.74    qed
1.75  qed
1.76 @@ -125,12 +124,12 @@
1.77  definition
1.78    fixp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"
1.79  where
1.80 -  "fixp f = lub (iterates f)"
1.81 +  "fixp f = Sup (iterates f)"
1.82
1.83  lemma iterates_fixp:
1.84    assumes f: "monotone (op \<le>) (op \<le>) f" shows "fixp f \<in> iterates f"
1.85  unfolding fixp_def
1.86 -by (simp add: iterates.lub chain_iterates f)
1.87 +by (simp add: iterates.Sup chain_iterates f)
1.88
1.89  lemma fixp_unfold:
1.90    assumes f: "monotone (op \<le>) (op \<le>) f"
1.91 @@ -138,8 +137,8 @@
1.92  proof (rule antisym)
1.93    show "fixp f \<le> f (fixp f)"
1.94      by (intro iterates_le_f iterates_fixp f)
1.95 -  have "f (fixp f) \<le> lub (iterates f)"
1.96 -    by (intro lub_upper chain_iterates f iterates.step iterates_fixp)
1.97 +  have "f (fixp f) \<le> Sup (iterates f)"
1.98 +    by (intro ccpo_Sup_upper chain_iterates f iterates.step iterates_fixp)
1.99    thus "f (fixp f) \<le> fixp f"
1.100      unfolding fixp_def .
1.101  qed
1.102 @@ -147,13 +146,13 @@
1.103  lemma fixp_lowerbound:
1.104    assumes f: "monotone (op \<le>) (op \<le>) f" and z: "f z \<le> z" shows "fixp f \<le> z"
1.105  unfolding fixp_def
1.106 -proof (rule lub_least[OF chain_iterates[OF f]])
1.107 +proof (rule ccpo_Sup_least[OF chain_iterates[OF f]])
1.108    fix x assume "x \<in> iterates f"
1.109    thus "x \<le> z"
1.110    proof (induct x rule: iterates.induct)
1.111      fix x assume "x \<le> z" with f have "f x \<le> f z" by (rule monotoneD)
1.112      also note z finally show "f x \<le> z" .
1.113 -  qed (auto intro: lub_least)
1.114 +  qed (auto intro: ccpo_Sup_least)
1.115  qed
1.116
1.117
1.118 @@ -162,10 +161,10 @@
1.119  definition
1.120    admissible :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
1.121  where
1.122 -  "admissible P = (\<forall>A. chain (op \<le>) A \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (lub A))"
1.123 +  "admissible P = (\<forall>A. chain (op \<le>) A \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (Sup A))"
1.124
1.126 -  assumes "\<And>A. chain (op \<le>) A \<Longrightarrow> \<forall>x\<in>A. P x \<Longrightarrow> P (lub A)"
1.127 +  assumes "\<And>A. chain (op \<le>) A \<Longrightarrow> \<forall>x\<in>A. P x \<Longrightarrow> P (Sup A)"
1.129  using assms unfolding admissible_def by fast
1.130
1.131 @@ -173,7 +172,7 @@
1.133    assumes "chain (op \<le>) A"
1.134    assumes "\<And>x. x \<in> A \<Longrightarrow> P x"
1.135 -  shows "P (lub A)"
1.136 +  shows "P (Sup A)"
1.137  using assms by (auto simp: admissible_def)
1.138
1.139  lemma fixp_induct:
1.140 @@ -220,20 +219,20 @@
1.142    assumes A: "chain (op \<le>)A"
1.143    assumes P: "\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> P y"
1.144 -  shows "lub A = lub {x \<in> A. P x}"
1.145 +  shows "Sup A = Sup {x \<in> A. P x}"
1.146  proof (rule antisym)
1.147    have *: "chain (op \<le>) {x \<in> A. P x}"
1.148      by (rule chain_compr [OF A])
1.149 -  show "lub A \<le> lub {x \<in> A. P x}"
1.150 -    apply (rule lub_least [OF A])
1.151 +  show "Sup A \<le> Sup {x \<in> A. P x}"
1.152 +    apply (rule ccpo_Sup_least [OF A])
1.153      apply (drule P [rule_format], clarify)
1.154      apply (erule order_trans)
1.155 -    apply (simp add: lub_upper [OF *])
1.156 +    apply (simp add: ccpo_Sup_upper [OF *])
1.157      done
1.158 -  show "lub {x \<in> A. P x} \<le> lub A"
1.159 -    apply (rule lub_least [OF *])
1.160 +  show "Sup {x \<in> A. P x} \<le> Sup A"
1.161 +    apply (rule ccpo_Sup_least [OF *])
1.162      apply clarify
1.163 -    apply (simp add: lub_upper [OF A])
1.164 +    apply (simp add: ccpo_Sup_upper [OF A])
1.165      done
1.166  qed
1.167
1.168 @@ -247,9 +246,9 @@
1.169    assume "\<forall>x\<in>A. P x \<or> Q x"
1.170    hence "(\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> P y) \<or> (\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> Q y)"
1.171      using chainD[OF A] by blast
1.172 -  hence "lub A = lub {x \<in> A. P x} \<or> lub A = lub {x \<in> A. Q x}"
1.173 +  hence "Sup A = Sup {x \<in> A. P x} \<or> Sup A = Sup {x \<in> A. Q x}"
1.174      using admissible_disj_lemma [OF A] by fast
1.175 -  thus "P (lub A) \<or> Q (lub A)"
1.176 +  thus "P (Sup A) \<or> Q (Sup A)"
1.177      apply (rule disjE, simp_all)
1.178      apply (rule disjI1, rule admissibleD [OF P chain_compr [OF A]], simp)
1.179      apply (rule disjI2, rule admissibleD [OF Q chain_compr [OF A]], simp)
1.180 @@ -258,6 +257,20 @@
1.181
1.182  end
1.183
1.184 -hide_const (open) lub iterates fixp admissible
1.185 +instance complete_lattice \<subseteq> ccpo
1.186 +  by default (fast intro: Sup_upper Sup_least)+
1.187 +
1.188 +lemma lfp_eq_fixp:
1.189 +  assumes f: "mono f" shows "lfp f = fixp f"
1.190 +proof (rule antisym)
1.191 +  from f have f': "monotone (op \<le>) (op \<le>) f"
1.192 +    unfolding mono_def monotone_def .
1.193 +  show "lfp f \<le> fixp f"
1.194 +    by (rule lfp_lowerbound, subst fixp_unfold [OF f'], rule order_refl)
1.195 +  show "fixp f \<le> lfp f"
1.196 +    by (rule fixp_lowerbound [OF f'], subst lfp_unfold [OF f], rule order_refl)
1.197 +qed
1.198 +
1.199 +hide_const (open) iterates fixp admissible
1.200
1.201  end
```