# HG changeset patch
# User huffman
# Date 1325181247 -3600
# Node ID 1e3ff542e83ead6cdea05af9f5de081ba62d0ae3
# Parent  67e1dcc0b8429ac052e9d93bad1df87fc36cf41e
remove constant 'ccpo.lub', re-use constant 'Sup' instead

diff -r 67e1dcc0b842 -r 1e3ff542e83e src/HOL/Complete_Partial_Order.thy
--- a/src/HOL/Complete_Partial_Order.thy	Thu Dec 29 17:43:54 2011 +0100
+++ b/src/HOL/Complete_Partial_Order.thy	Thu Dec 29 18:54:07 2011 +0100
@@ -57,10 +57,9 @@
   empty set is a chain, so every ccpo must have a bottom element.
 *}
 
-class ccpo = order +
-  fixes lub :: "'a set \<Rightarrow> 'a"
-  assumes lub_upper: "chain (op \<le>) A \<Longrightarrow> x \<in> A \<Longrightarrow> x \<le> lub A"
-  assumes lub_least: "chain (op \<le>) A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> lub A \<le> z"
+class ccpo = order + Sup +
+  assumes ccpo_Sup_upper: "\<lbrakk>chain (op \<le>) A; x \<in> A\<rbrakk> \<Longrightarrow> x \<le> Sup A"
+  assumes ccpo_Sup_least: "\<lbrakk>chain (op \<le>) A; \<And>x. x \<in> A \<Longrightarrow> x \<le> z\<rbrakk> \<Longrightarrow> Sup A \<le> z"
 begin
 
 subsection {* Transfinite iteration of a function *}
@@ -69,12 +68,12 @@
 for f :: "'a \<Rightarrow> 'a"
 where
   step: "x \<in> iterates f \<Longrightarrow> f x \<in> iterates f"
-| lub: "chain (op \<le>) M \<Longrightarrow> \<forall>x\<in>M. x \<in> iterates f \<Longrightarrow> lub M \<in> iterates f"
+| Sup: "chain (op \<le>) M \<Longrightarrow> \<forall>x\<in>M. x \<in> iterates f \<Longrightarrow> Sup M \<in> iterates f"
 
 lemma iterates_le_f:
   "x \<in> iterates f \<Longrightarrow> monotone (op \<le>) (op \<le>) f \<Longrightarrow> x \<le> f x"
 by (induct x rule: iterates.induct)
-  (force dest: monotoneD intro!: lub_upper lub_least)+
+  (force dest: monotoneD intro!: ccpo_Sup_upper ccpo_Sup_least)+
 
 lemma chain_iterates:
   assumes f: "monotone (op \<le>) (op \<le>) f"
@@ -89,33 +88,33 @@
     proof (induct y rule: iterates.induct)
       case (step y) with IH f show ?case by (auto dest: monotoneD)
     next
-      case (lub M)
+      case (Sup M)
       then have chM: "chain (op \<le>) M"
         and IH': "\<And>z. z \<in> M \<Longrightarrow> f x \<le> z \<or> z \<le> f x" by auto
-      show "f x \<le> lub M \<or> lub M \<le> f x"
+      show "f x \<le> Sup M \<or> Sup M \<le> f x"
       proof (cases "\<exists>z\<in>M. f x \<le> z")
-        case True then have "f x \<le> lub M"
+        case True then have "f x \<le> Sup M"
           apply rule
           apply (erule order_trans)
-          by (rule lub_upper[OF chM])
+          by (rule ccpo_Sup_upper[OF chM])
         thus ?thesis ..
       next
         case False with IH'
-        show ?thesis by (auto intro: lub_least[OF chM])
+        show ?thesis by (auto intro: ccpo_Sup_least[OF chM])
       qed
     qed
   next
-    case (lub M y)
+    case (Sup M y)
     show ?case
     proof (cases "\<exists>x\<in>M. y \<le> x")
-      case True then have "y \<le> lub M"
+      case True then have "y \<le> Sup M"
         apply rule
         apply (erule order_trans)
-        by (rule lub_upper[OF lub(1)])
+        by (rule ccpo_Sup_upper[OF Sup(1)])
       thus ?thesis ..
     next
-      case False with lub
-      show ?thesis by (auto intro: lub_least)
+      case False with Sup
+      show ?thesis by (auto intro: ccpo_Sup_least)
     qed
   qed
 qed
@@ -125,12 +124,12 @@
 definition
   fixp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"
 where
-  "fixp f = lub (iterates f)"
+  "fixp f = Sup (iterates f)"
 
 lemma iterates_fixp:
   assumes f: "monotone (op \<le>) (op \<le>) f" shows "fixp f \<in> iterates f"
 unfolding fixp_def
-by (simp add: iterates.lub chain_iterates f)
+by (simp add: iterates.Sup chain_iterates f)
 
 lemma fixp_unfold:
   assumes f: "monotone (op \<le>) (op \<le>) f"
@@ -138,8 +137,8 @@
 proof (rule antisym)
   show "fixp f \<le> f (fixp f)"
     by (intro iterates_le_f iterates_fixp f)
-  have "f (fixp f) \<le> lub (iterates f)"
-    by (intro lub_upper chain_iterates f iterates.step iterates_fixp)
+  have "f (fixp f) \<le> Sup (iterates f)"
+    by (intro ccpo_Sup_upper chain_iterates f iterates.step iterates_fixp)
   thus "f (fixp f) \<le> fixp f"
     unfolding fixp_def .
 qed
@@ -147,13 +146,13 @@
 lemma fixp_lowerbound:
   assumes f: "monotone (op \<le>) (op \<le>) f" and z: "f z \<le> z" shows "fixp f \<le> z"
 unfolding fixp_def
-proof (rule lub_least[OF chain_iterates[OF f]])
+proof (rule ccpo_Sup_least[OF chain_iterates[OF f]])
   fix x assume "x \<in> iterates f"
   thus "x \<le> z"
   proof (induct x rule: iterates.induct)
     fix x assume "x \<le> z" with f have "f x \<le> f z" by (rule monotoneD)
     also note z finally show "f x \<le> z" .
-  qed (auto intro: lub_least)
+  qed (auto intro: ccpo_Sup_least)
 qed
 
 
@@ -162,10 +161,10 @@
 definition
   admissible :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
 where
-  "admissible P = (\<forall>A. chain (op \<le>) A \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (lub A))"
+  "admissible P = (\<forall>A. chain (op \<le>) A \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (Sup A))"
 
 lemma admissibleI:
-  assumes "\<And>A. chain (op \<le>) A \<Longrightarrow> \<forall>x\<in>A. P x \<Longrightarrow> P (lub A)"
+  assumes "\<And>A. chain (op \<le>) A \<Longrightarrow> \<forall>x\<in>A. P x \<Longrightarrow> P (Sup A)"
   shows "admissible P"
 using assms unfolding admissible_def by fast
 
@@ -173,7 +172,7 @@
   assumes "admissible P"
   assumes "chain (op \<le>) A"
   assumes "\<And>x. x \<in> A \<Longrightarrow> P x"
-  shows "P (lub A)"
+  shows "P (Sup A)"
 using assms by (auto simp: admissible_def)
 
 lemma fixp_induct:
@@ -220,20 +219,20 @@
 lemma admissible_disj_lemma:
   assumes A: "chain (op \<le>)A"
   assumes P: "\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> P y"
-  shows "lub A = lub {x \<in> A. P x}"
+  shows "Sup A = Sup {x \<in> A. P x}"
 proof (rule antisym)
   have *: "chain (op \<le>) {x \<in> A. P x}"
     by (rule chain_compr [OF A])
-  show "lub A \<le> lub {x \<in> A. P x}"
-    apply (rule lub_least [OF A])
+  show "Sup A \<le> Sup {x \<in> A. P x}"
+    apply (rule ccpo_Sup_least [OF A])
     apply (drule P [rule_format], clarify)
     apply (erule order_trans)
-    apply (simp add: lub_upper [OF *])
+    apply (simp add: ccpo_Sup_upper [OF *])
     done
-  show "lub {x \<in> A. P x} \<le> lub A"
-    apply (rule lub_least [OF *])
+  show "Sup {x \<in> A. P x} \<le> Sup A"
+    apply (rule ccpo_Sup_least [OF *])
     apply clarify
-    apply (simp add: lub_upper [OF A])
+    apply (simp add: ccpo_Sup_upper [OF A])
     done
 qed
 
@@ -247,9 +246,9 @@
   assume "\<forall>x\<in>A. P x \<or> Q x"
   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)"
     using chainD[OF A] by blast
-  hence "lub A = lub {x \<in> A. P x} \<or> lub A = lub {x \<in> A. Q x}"
+  hence "Sup A = Sup {x \<in> A. P x} \<or> Sup A = Sup {x \<in> A. Q x}"
     using admissible_disj_lemma [OF A] by fast
-  thus "P (lub A) \<or> Q (lub A)"
+  thus "P (Sup A) \<or> Q (Sup A)"
     apply (rule disjE, simp_all)
     apply (rule disjI1, rule admissibleD [OF P chain_compr [OF A]], simp)
     apply (rule disjI2, rule admissibleD [OF Q chain_compr [OF A]], simp)
@@ -258,6 +257,20 @@
 
 end
 
-hide_const (open) lub iterates fixp admissible
+instance complete_lattice \<subseteq> ccpo
+  by default (fast intro: Sup_upper Sup_least)+
+
+lemma lfp_eq_fixp:
+  assumes f: "mono f" shows "lfp f = fixp f"
+proof (rule antisym)
+  from f have f': "monotone (op \<le>) (op \<le>) f"
+    unfolding mono_def monotone_def .
+  show "lfp f \<le> fixp f"
+    by (rule lfp_lowerbound, subst fixp_unfold [OF f'], rule order_refl)
+  show "fixp f \<le> lfp f"
+    by (rule fixp_lowerbound [OF f'], subst lfp_unfold [OF f], rule order_refl)
+qed
+
+hide_const (open) iterates fixp admissible
 
 end
diff -r 67e1dcc0b842 -r 1e3ff542e83e src/HOL/Partial_Function.thy
--- a/src/HOL/Partial_Function.thy	Thu Dec 29 17:43:54 2011 +0100
+++ b/src/HOL/Partial_Function.thy	Thu Dec 29 18:54:07 2011 +0100
@@ -90,7 +90,7 @@
 qed
 
 lemma ccpo: assumes "partial_function_definitions ord lb"
-  shows "class.ccpo ord (mk_less ord) lb"
+  shows "class.ccpo lb ord (mk_less ord)"
 using assms unfolding partial_function_definitions_def mk_less_def
 by unfold_locales blast+
 
@@ -127,14 +127,14 @@
 
 abbreviation "le_fun \<equiv> fun_ord leq"
 abbreviation "lub_fun \<equiv> fun_lub lub"
-abbreviation "fixp_fun \<equiv> ccpo.fixp le_fun lub_fun"
+abbreviation "fixp_fun \<equiv> ccpo.fixp lub_fun le_fun"
 abbreviation "mono_body \<equiv> monotone le_fun leq"
-abbreviation "admissible \<equiv> ccpo.admissible le_fun lub_fun"
+abbreviation "admissible \<equiv> ccpo.admissible lub_fun le_fun"
 
 text {* Interpret manually, to avoid flooding everything with facts about
   orders *}
 
-lemma ccpo: "class.ccpo le_fun (mk_less le_fun) lub_fun"
+lemma ccpo: "class.ccpo lub_fun le_fun (mk_less le_fun)"
 apply (rule ccpo)
 apply (rule partial_function_lift)
 apply (rule partial_function_definitions_axioms)
@@ -175,7 +175,7 @@
   assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)"
   assumes eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))"
   assumes inverse: "\<And>f. U (C f) = f"
-  assumes adm: "ccpo.admissible le_fun lub_fun P"
+  assumes adm: "ccpo.admissible lub_fun le_fun P"
   assumes step: "\<And>f. P (U f) \<Longrightarrow> P (U (F f))"
   shows "P (U f)"
 unfolding eq inverse
@@ -307,7 +307,7 @@
     C :: "('b \<Rightarrow> 'a option) \<Rightarrow> 'c" and
     P :: "'b \<Rightarrow> 'a \<Rightarrow> bool"
   assumes mono: "\<And>x. mono_option (\<lambda>f. U (F (C f)) x)"
-  assumes eq: "f \<equiv> C (ccpo.fixp (fun_ord option_ord) (fun_lub (flat_lub None)) (\<lambda>f. U (F (C f))))"
+  assumes eq: "f \<equiv> C (ccpo.fixp (fun_lub (flat_lub None)) (fun_ord option_ord) (\<lambda>f. U (F (C f))))"
   assumes inverse2: "\<And>f. U (C f) = f"
   assumes step: "\<And>f x y. (\<And>x y. U f x = Some y \<Longrightarrow> P x y) \<Longrightarrow> U (F f) x = Some y \<Longrightarrow> P x y"
   assumes defined: "U f x = Some y"
@@ -326,4 +326,3 @@
 hide_const (open) chain
 
 end
-