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.125  lemma admissibleI:
   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.128    shows "admissible P"
   1.129  using assms unfolding admissible_def by fast
   1.130  
   1.131 @@ -173,7 +172,7 @@
   1.132    assumes "admissible P"
   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.141  lemma admissible_disj_lemma:
   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