# HG changeset patch
# User Andreas Lochbihler
# Date 1499077189 -7200
# Node ID 4c999b5d78e24137b6f4ea71a750ff4ef0358ebb
# Parent  453f9cabddb5a13f9151de350dd53e39cb953f22
qualify Complete_Partial_Order2.compact

diff -r 453f9cabddb5 -r 4c999b5d78e2 src/HOL/Library/Complete_Partial_Order2.thy
--- a/src/HOL/Library/Complete_Partial_Order2.thy	Sat Jul 01 16:39:56 2017 +0200
+++ b/src/HOL/Library/Complete_Partial_Order2.thy	Mon Jul 03 12:19:49 2017 +0200
@@ -904,6 +904,7 @@
 
 end
 
+setup \<open>Sign.map_naming (Name_Space.mandatory_path "ccpo")\<close>
 
 inductive compact :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
   for lub ord x 
@@ -912,15 +913,15 @@
      ccpo.admissible lub ord (\<lambda>y. x \<noteq> y) \<rbrakk>
   \<Longrightarrow> compact lub ord x"
 
-hide_fact (open) compact
+setup \<open>Sign.map_naming Name_Space.parent_path\<close>
 
 context ccpo begin
 
 lemma compactI:
   assumes "ccpo.admissible Sup op \<le> (\<lambda>y. \<not> x \<le> y)"
-  shows "compact Sup op \<le> x"
+  shows "ccpo.compact Sup op \<le> x"
 using assms
-proof(rule compact.intros)
+proof(rule ccpo.compact.intros)
   have neq: "(\<lambda>y. x \<noteq> y) = (\<lambda>y. \<not> x \<le> y \<or> \<not> y \<le> x)" by(auto)
   show "ccpo.admissible Sup op \<le> (\<lambda>y. x \<noteq> y)"
     by(subst neq)(rule admissible_disj admissible_not_below assms)+
@@ -928,7 +929,7 @@
 
 lemma compact_bot:
   assumes "x = Sup {}"
-  shows "compact Sup op \<le> x"
+  shows "ccpo.compact Sup op \<le> x"
 proof(rule compactI)
   show "ccpo.admissible Sup op \<le> (\<lambda>y. \<not> x \<le> y)" using assms
     by(auto intro!: ccpo.admissibleI intro: ccpo_Sup_least chain_empty)
@@ -937,11 +938,11 @@
 end
 
 lemma admissible_compact_neq' [THEN admissible_subst, cont_intro, simp]:
-  shows admissible_compact_neq: "compact lub ord k \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. k \<noteq> x)"
-by(simp add: compact.simps)
+  shows admissible_compact_neq: "ccpo.compact lub ord k \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. k \<noteq> x)"
+by(simp add: ccpo.compact.simps)
 
 lemma admissible_neq_compact' [THEN admissible_subst, cont_intro, simp]:
-  shows admissible_neq_compact: "compact lub ord k \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. x \<noteq> k)"
+  shows admissible_neq_compact: "ccpo.compact lub ord k \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. x \<noteq> k)"
 by(subst eq_commute)(rule admissible_compact_neq)
 
 context partial_function_definitions begin
@@ -1728,7 +1729,7 @@
   "mono_option B \<Longrightarrow> mono_option (\<lambda>f. map_option g (B f))"
 unfolding map_conv_bind_option by(rule bind_mono) simp_all
 
-lemma compact_flat_lub [cont_intro]: "compact (flat_lub x) (flat_ord x) y"
+lemma compact_flat_lub [cont_intro]: "ccpo.compact (flat_lub x) (flat_ord x) y"
 using flat_interpretation[THEN ccpo]
 proof(rule ccpo.compactI[OF _ ccpo.admissibleI])
   fix A