admissibility on option type

--- a/src/HOL/Partial_Function.thy	Mon May 23 21:34:37 2011 +0200
+++ b/src/HOL/Partial_Function.thy	Tue May 31 11:11:17 2011 +0200
@@ -23,6 +23,17 @@
 definition "img_ord f ord = (\<lambda>x y. ord (f x) (f y))"
 definition "img_lub f g Lub = (\<lambda>A. g (Lub (f ` A)))"
 
+lemma chain_fun: 
+  assumes A: "chain (fun_ord ord) A"
+  shows "chain ord {y. \<exists>f\<in>A. y = f a}" (is "chain ord ?C")
+proof (rule chainI)
+  fix x y assume "x \<in> ?C" "y \<in> ?C"
+  then obtain f g where fg: "f \<in> A" "g \<in> A" 
+    and [simp]: "x = f a" "y = g a" by blast
+  from chainD[OF A fg]
+  show "ord x y \<or> ord y x" unfolding fun_ord_def by auto
+qed
+
 lemma call_mono[partial_function_mono]: "monotone (fun_ord ord) ord (\<lambda>f. f t)"
 by (rule monotoneI) (auto simp: fun_ord_def)
 
@@ -53,17 +64,6 @@
 proof -
   interpret partial_function_definitions ord lb by fact
 
-  { fix A a assume A: "chain ?ordf A"
-    have "chain ord {y. \<exists>f\<in>A. y = f a}" (is "chain ord ?C")
-    proof (rule chainI)
-      fix x y assume "x \<in> ?C" "y \<in> ?C"
-      then obtain f g where fg: "f \<in> A" "g \<in> A" 
-        and [simp]: "x = f a" "y = g a" by blast
-      from chainD[OF A fg]
-      show "ord x y \<or> ord y x" unfolding fun_ord_def by auto
-    qed }
-  note chain_fun = this
-
   show ?thesis
   proof
     fix x show "?ordf x x"
@@ -75,7 +75,7 @@
   next
     fix x y assume "?ordf x y" "?ordf y x"
     thus "x = y" unfolding fun_ord_def
-      by (force intro!: ext dest: leq_antisym)
+      by (force intro!: dest: leq_antisym)
   next
     fix A f assume f: "f \<in> A" and A: "chain ?ordf A"
     thus "?ordf f (?lubf A)"
@@ -129,6 +129,7 @@
 abbreviation "lub_fun \<equiv> fun_lub lub"
 abbreviation "fixp_fun == ccpo.fixp le_fun lub_fun"
 abbreviation "mono_body \<equiv> monotone le_fun leq"
+abbreviation "admissible \<equiv> ccpo.admissible le_fun lub_fun"
 
 text {* Interpret manually, to avoid flooding everything with facts about
   orders *}
@@ -251,6 +252,43 @@
   show "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y'. C y' g))" .
 qed
 
+lemma flat_lub_in_chain:
+  assumes ch: "chain (flat_ord b) A "
+  assumes lub: "flat_lub b A = a"
+  shows "a = b \<or> a \<in> A"
+proof (cases "A \<subseteq> {b}")
+  case True
+  then have "flat_lub b A = b" unfolding flat_lub_def by simp
+  with lub show ?thesis by simp
+next
+  case False
+  then obtain c where "c \<in> A" and "c \<noteq> b" by auto
+  { fix z assume "z \<in> A"
+    from chainD[OF ch `c \<in> A` this] have "z = c \<or> z = b"
+      unfolding flat_ord_def using `c \<noteq> b` by auto }
+  with False have "A - {b} = {c}" by auto
+  with False have "flat_lub b A = c" by (auto simp: flat_lub_def)
+  with `c \<in> A` lub show ?thesis by simp
+qed
+
+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])
+  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"
+  from ch have ch': "\<And>x. chain option_ord {y. \<exists>f\<in>A. y = f x}" by (rule chain_fun)
+  show "\<forall>x y. option.lub_fun A x = Some y \<longrightarrow> P x y"
+  proof (intro allI impI)
+    fix x y assume "option.lub_fun A x = Some y"
+    from flat_lub_in_chain[OF ch' this[unfolded fun_lub_def]]
+    have "Some y \<in> {y. \<exists>f\<in>A. y = f x}" by simp
+    then have "\<exists>f\<in>A. f x = Some y" by auto
+    with IH show "P x y" by auto
+  qed
+qed
+
+
 hide_const (open) chain
 
 end