# HG changeset patch
# User Andreas Lochbihler
# Date 1378134891 -7200
# Node ID f6629734dd2b5c36b697d2c608b869aafbb3f7d1
# Parent  735e078a64e74fec1171c074868af59e6f08a5ca# Parent  7ffc4a746a73791e4f6993be0ca0e764d5ac4e98
merged

diff -r 7ffc4a746a73 -r f6629734dd2b NEWS
--- a/NEWS	Mon Sep 02 15:13:00 2013 +0200
+++ b/NEWS	Mon Sep 02 17:14:51 2013 +0200
@@ -265,6 +265,11 @@
 Code_Target_Nat and Code_Target_Numeral.  See the tutorial on code
 generation for details.  INCOMPATIBILITY.
 
+* Complete_Partial_Order.admissible is defined outside the type 
+class ccpo, but with mandatory prefix ccpo. Admissibility theorems
+lose the class predicate assumption or sort constraint when possible.
+INCOMPATIBILITY.
+
 * Introduce type class "conditionally_complete_lattice": Like a
 complete lattice but does not assume the existence of the top and
 bottom elements.  Allows to generalize some lemmas about reals and
diff -r 7ffc4a746a73 -r f6629734dd2b src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Mon Sep 02 15:13:00 2013 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Mon Sep 02 17:14:51 2013 +0200
@@ -53,13 +53,6 @@
 (* If the compilation fails with an error "ambiguous implicit values",
    read \<section>7.1 in the Code Generation Manual *)
 
-class ccpo_linorder = ccpo + linorder
-
-lemma [code]:
-  "(Complete_Partial_Order.admissible :: ('a :: ccpo_linorder \<Rightarrow> bool) \<Rightarrow> bool) P = 
-    (\<forall>A. Complete_Partial_Order.chain (op \<le>) A \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (Sup A))"
-unfolding admissible_def by blast
-
 lemma [code]:
   "(gfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Sup {u. u \<le> f u}"
 unfolding gfp_def by blast
diff -r 7ffc4a746a73 -r f6629734dd2b src/HOL/Complete_Partial_Order.thy
--- a/src/HOL/Complete_Partial_Order.thy	Mon Sep 02 15:13:00 2013 +0200
+++ b/src/HOL/Complete_Partial_Order.thy	Mon Sep 02 17:14:51 2013 +0200
@@ -155,67 +155,72 @@
   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)
+  shows "P (lub A)"
+using assms by (auto simp: ccpo.admissible_def)
 
-lemma fixp_induct:
-  assumes adm: "admissible P"
+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)
+      (auto intro: step ccpo.admissibleD adm)
 qed
 
-lemma admissible_True: "admissible (\<lambda>x. True)"
-unfolding admissible_def by simp
+lemma admissible_True: "ccpo.admissible lub ord (\<lambda>x. True)"
+unfolding ccpo.admissible_def by simp
 
-lemma admissible_False: "\<not> admissible (\<lambda>x. False)"
-unfolding admissible_def chain_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: "admissible (\<lambda>x. t) = t"
+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
+  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 (op \<le>) A \<Longrightarrow> chain (op \<le>) {x \<in> A. P x}"
+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"
@@ -238,10 +243,10 @@
 
 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)"
@@ -250,8 +255,8 @@
     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
 
@@ -271,6 +276,6 @@
     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
diff -r 7ffc4a746a73 -r f6629734dd2b src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Sep 02 15:13:00 2013 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Sep 02 17:14:51 2013 +0200
@@ -432,7 +432,7 @@
 lemma heap_step_admissible: 
   "option.admissible
       (\<lambda>f:: 'a => ('b * 'c) option. \<forall>h h' r. f h = Some (r, h') \<longrightarrow> P x h h' r)"
-proof (rule ccpo.admissibleI[OF option.ccpo])
+proof (rule ccpo.admissibleI)
   fix A :: "('a \<Rightarrow> ('b * 'c) option) set"
   assume ch: "Complete_Partial_Order.chain option.le_fun A"
     and IH: "\<forall>f\<in>A. \<forall>h h' r. f h = Some (r, h') \<longrightarrow> P x h h' r"
diff -r 7ffc4a746a73 -r f6629734dd2b src/HOL/Partial_Function.thy
--- a/src/HOL/Partial_Function.thy	Mon Sep 02 15:13:00 2013 +0200
+++ b/src/HOL/Partial_Function.thy	Mon Sep 02 17:14:51 2013 +0200
@@ -250,7 +250,7 @@
 lemma tailrec_admissible:
   "ccpo.admissible (fun_lub (flat_lub undefined)) (fun_ord tailrec_ord)
      (\<lambda>a. \<forall>x. a x \<noteq> undefined \<longrightarrow> P x (a x))"
-proof(intro ccpo.admissibleI[OF tailrec.ccpo] strip)
+proof(intro ccpo.admissibleI strip)
   fix A x
   assume chain: "Complete_Partial_Order.chain (fun_ord tailrec_ord) A"
     and P [rule_format]: "\<forall>f\<in>A. \<forall>x. f x \<noteq> undefined \<longrightarrow> P x (f x)"
@@ -290,13 +290,13 @@
   assumes inj: "\<And>x y. f x = f y \<Longrightarrow> x = y"
   assumes inv: "\<And>x. f (g x) = x"
   shows "ccpo.admissible (img_lub f g lub) (img_ord f le) P"
-proof (rule ccpo.admissibleI, rule ccpo, rule partial_function_image, fact pfun, fact inj, fact inv)
+proof (rule ccpo.admissibleI)
   fix A assume "chain (img_ord f le) A"
    then have ch': "chain le (f ` A)"
       by (auto simp: img_ord_def intro: chainI dest: chainD)
   assume P_A: "\<forall>x\<in>A. P x"
-  have "(P o g) (lub (f ` A))"
-  proof (rule ccpo.admissibleD[OF ccpo, OF pfun adm ch'])
+  have "(P o g) (lub (f ` A))" using adm ch'
+  proof (rule ccpo.admissibleD)
     fix x assume "x \<in> f ` A"
     with P_A show "(P o g) x" by (auto simp: inj[OF inv])
   qed
@@ -307,13 +307,13 @@
   assumes pfun: "partial_function_definitions le lub"
   assumes adm: "\<And>x. ccpo.admissible lub le (Q x)"
   shows "ccpo.admissible  (fun_lub lub) (fun_ord le) (\<lambda>f. \<forall>x. Q x (f x))"
-proof (rule ccpo.admissibleI, rule ccpo, rule partial_function_lift, rule pfun)
+proof (rule ccpo.admissibleI)
   fix A :: "('b \<Rightarrow> 'a) set"
   assume Q: "\<forall>f\<in>A. \<forall>x. Q x (f x)"
   assume ch: "chain (fun_ord le) A"
   show "\<forall>x. Q x (fun_lub lub A x)"
     unfolding fun_lub_def
-    by (rule allI, rule ccpo.admissibleD[OF ccpo, OF pfun adm chain_fun[OF ch]])
+    by (rule allI, rule ccpo.admissibleD[OF adm chain_fun[OF ch]])
       (auto simp: Q)
 qed
 
@@ -360,7 +360,7 @@
 
 lemma option_admissible: "option.admissible (%(f::'a \<Rightarrow> 'b option).
   (\<forall>x y. f x = Some y \<longrightarrow> P x y))"
-proof (rule ccpo.admissibleI[OF option.ccpo])
+proof (rule ccpo.admissibleI)
   fix A :: "('a \<Rightarrow> 'b option) set"
   assume ch: "chain option.le_fun A"
     and IH: "\<forall>f\<in>A. \<forall>x y. f x = Some y \<longrightarrow> P x y"