src/HOL/Complete_Partial_Order.thy

     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: ccpo_Sup_least)
 qed
 
+end
 
 subsection {* Fixpoint induction *}
 
-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 (Sup A))"
+setup {* Sign.map_naming (Name_Space.mandatory_path "ccpo") *}
+
+definition admissible :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
+where "admissible lub ord P = (\<forall>A. chain ord A \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (lub A))"
 
 lemma admissibleI:
-  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
+  assumes "\<And>A. chain ord A \<Longrightarrow> \<forall>x\<in>A. P x \<Longrightarrow> P (lub A)"
+  shows "ccpo.admissible lub ord P"
+using assms unfolding ccpo.admissible_def by fast
 
 lemma admissibleD:
-  assumes "admissible P"
-  assumes "chain (op \<le>) A"
+  assumes "ccpo.admissible lub ord P"
+  assumes "chain ord A"
   assumes "\<And>x. x \<in> A \<Longrightarrow> P x"
-  shows "P (Sup A)"
-using assms by (auto simp: admissible_def)
-
-lemma fixp_induct:
-  assumes adm: "admissible P"
+  shows "P (lub A)"
+using assms by (auto simp: ccpo.admissible_def)
+
+setup {* Sign.map_naming Name_Space.parent_path *}
+
+lemma (in ccpo) fixp_induct:
+  assumes adm: "ccpo.admissible Sup (op \<le>) P"
   assumes mono: "monotone (op \<le>) (op \<le>) f"
   assumes step: "\<And>x. P x \<Longrightarrow> P (f x)"
   shows "P (fixp f)"
 unfolding fixp_def using adm chain_iterates[OF mono]
-proof (rule admissibleD)
+proof (rule ccpo.admissibleD)
   fix x assume "x \<in> iterates f"
   thus "P x"
     by (induct rule: iterates.induct)
-      (auto intro: step admissibleD adm)
-qed
-
-lemma admissible_True: "admissible (\<lambda>x. True)"
-unfolding admissible_def by simp
-
-lemma admissible_False: "\<not> admissible (\<lambda>x. False)"
-unfolding admissible_def chain_def by simp
-
-lemma admissible_const: "admissible (\<lambda>x. t) = t"
+      (auto intro: step ccpo.admissibleD adm)
+qed
+
+lemma admissible_True: "ccpo.admissible lub ord (\<lambda>x. True)"
+unfolding ccpo.admissible_def by simp
+
+lemma admissible_False: "\<not> ccpo.admissible lub ord (\<lambda>x. False)"
+unfolding ccpo.admissible_def chain_def by simp
+
+lemma admissible_const: "ccpo.admissible lub ord (\<lambda>x. t) = t"
 by (cases t, simp_all add: admissible_True admissible_False)
 
 lemma admissible_conj:
-  assumes "admissible (\<lambda>x. P x)"
-  assumes "admissible (\<lambda>x. Q x)"
-  shows "admissible (\<lambda>x. P x \<and> Q x)"
-using assms unfolding admissible_def by simp
+  assumes "ccpo.admissible lub ord (\<lambda>x. P x)"
+  assumes "ccpo.admissible lub ord (\<lambda>x. Q x)"
+  shows "ccpo.admissible lub ord (\<lambda>x. P x \<and> Q x)"
+using assms unfolding ccpo.admissible_def by simp
 
 lemma admissible_all:
-  assumes "\<And>y. admissible (\<lambda>x. P x y)"
-  shows "admissible (\<lambda>x. \<forall>y. P x y)"
-using assms unfolding admissible_def by fast
+  assumes "\<And>y. ccpo.admissible lub ord (\<lambda>x. P x y)"
+  shows "ccpo.admissible lub ord (\<lambda>x. \<forall>y. P x y)"
+using assms unfolding ccpo.admissible_def by fast
 
 lemma admissible_ball:
-  assumes "\<And>y. y \<in> A \<Longrightarrow> admissible (\<lambda>x. P x y)"
-  shows "admissible (\<lambda>x. \<forall>y\<in>A. P x y)"
-using assms unfolding admissible_def by fast
-
-lemma chain_compr: "chain (op \<le>) A \<Longrightarrow> chain (op \<le>) {x \<in> A. P x}"
+  assumes "\<And>y. y \<in> A \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x y)"
+  shows "ccpo.admissible lub ord (\<lambda>x. \<forall>y\<in>A. P x y)"
+using assms unfolding ccpo.admissible_def by fast
+
+lemma chain_compr: "chain ord A \<Longrightarrow> chain ord {x \<in> A. P x}"
 unfolding chain_def by fast
+
+context ccpo begin
 
 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 "Sup A = Sup {x \<in> A. P x}"

     done
 qed
 
 lemma admissible_disj:
   fixes P Q :: "'a \<Rightarrow> bool"
-  assumes P: "admissible (\<lambda>x. P x)"
-  assumes Q: "admissible (\<lambda>x. Q x)"
-  shows "admissible (\<lambda>x. P x \<or> Q x)"
-proof (rule admissibleI)
+  assumes P: "ccpo.admissible Sup (op \<le>) (\<lambda>x. P x)"
+  assumes Q: "ccpo.admissible Sup (op \<le>) (\<lambda>x. Q x)"
+  shows "ccpo.admissible Sup (op \<le>) (\<lambda>x. P x \<or> Q x)"
+proof (rule ccpo.admissibleI)
   fix A :: "'a set" assume A: "chain (op \<le>) A"
   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 "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 (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)
+    apply (rule disjI1, rule ccpo.admissibleD [OF P chain_compr [OF A]], simp)
+    apply (rule disjI2, rule ccpo.admissibleD [OF Q chain_compr [OF A]], simp)
     done
 qed
 
 end
 

     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
+hide_const (open) iterates fixp
 
 end