# HG changeset patch
# User nipkow
# Date 1346999764 -7200
# Node ID d383fd5dbd3c5b89b534b5f91f510f46ca896520
# Parent  e1e1d427747d3738a20619d045a3885dbb50876a# Parent  3601bf546775afebe84b282d92e8f7eba3a124d3
merged

diff -r 3601bf546775 -r d383fd5dbd3c CONTRIBUTORS
--- a/CONTRIBUTORS	Fri Sep 07 08:35:35 2012 +0200
+++ b/CONTRIBUTORS	Fri Sep 07 08:36:04 2012 +0200
@@ -6,6 +6,9 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* September 2012: Florian Haftmann, TUM
+  Lattice instances for type option.
+
 * September 2012: Christian Sternagel, JAIST
   Consolidated HOL/Library (theories: Prefix_Order, Sublist, and
   Sublist_Order) w.r.t. prefixes, suffixes, and embedding on lists.
diff -r 3601bf546775 -r d383fd5dbd3c NEWS
--- a/NEWS	Fri Sep 07 08:35:35 2012 +0200
+++ b/NEWS	Fri Sep 07 08:36:04 2012 +0200
@@ -41,6 +41,11 @@
 
 *** HOL ***
 
+* Theory "Library/Option_ord" provides instantiation of option type
+to lattice type classes.
+
+* New combinator "Option.these" with type "'a option set => 'a option".
+
 * Renamed theory Library/List_Prefix to Library/Sublist.
 INCOMPATIBILITY.  Related changes are:
 
diff -r 3601bf546775 -r d383fd5dbd3c src/HOL/Library/Option_ord.thy
--- a/src/HOL/Library/Option_ord.thy	Fri Sep 07 08:35:35 2012 +0200
+++ b/src/HOL/Library/Option_ord.thy	Fri Sep 07 08:36:04 2012 +0200
@@ -8,6 +8,21 @@
 imports Option Main
 begin
 
+notation
+  bot ("\<bottom>") and
+  top ("\<top>") and
+  inf  (infixl "\<sqinter>" 70) and
+  sup  (infixl "\<squnion>" 65) and
+  Inf  ("\<Sqinter>_" [900] 900) and
+  Sup  ("\<Squnion>_" [900] 900)
+
+syntax (xsymbols)
+  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
+  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
+  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
+  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
+
+
 instantiation option :: (preorder) preorder
 begin
 
@@ -61,7 +76,8 @@
 instantiation option :: (order) bot
 begin
 
-definition "bot = None"
+definition bot_option where
+  "\<bottom> = None"
 
 instance proof
 qed (simp add: bot_option_def)
@@ -71,7 +87,8 @@
 instantiation option :: (top) top
 begin
 
-definition "top = Some top"
+definition top_option where
+  "\<top> = Some \<top>"
 
 instance proof
 qed (simp add: top_option_def less_eq_option_def split: option.split)
@@ -106,4 +123,254 @@
   qed
 qed
 
+instantiation option :: (inf) inf
+begin
+
+definition inf_option where
+  "x \<sqinter> y = (case x of None \<Rightarrow> None | Some x \<Rightarrow> (case y of None \<Rightarrow> None | Some y \<Rightarrow> Some (x \<sqinter> y)))"
+
+lemma inf_None_1 [simp, code]:
+  "None \<sqinter> y = None"
+  by (simp add: inf_option_def)
+
+lemma inf_None_2 [simp, code]:
+  "x \<sqinter> None = None"
+  by (cases x) (simp_all add: inf_option_def)
+
+lemma inf_Some [simp, code]:
+  "Some x \<sqinter> Some y = Some (x \<sqinter> y)"
+  by (simp add: inf_option_def)
+
+instance ..
+
 end
+
+instantiation option :: (sup) sup
+begin
+
+definition sup_option where
+  "x \<squnion> y = (case x of None \<Rightarrow> y | Some x' \<Rightarrow> (case y of None \<Rightarrow> x | Some y \<Rightarrow> Some (x' \<squnion> y)))"
+
+lemma sup_None_1 [simp, code]:
+  "None \<squnion> y = y"
+  by (simp add: sup_option_def)
+
+lemma sup_None_2 [simp, code]:
+  "x \<squnion> None = x"
+  by (cases x) (simp_all add: sup_option_def)
+
+lemma sup_Some [simp, code]:
+  "Some x \<squnion> Some y = Some (x \<squnion> y)"
+  by (simp add: sup_option_def)
+
+instance ..
+
+end
+
+instantiation option :: (semilattice_inf) semilattice_inf
+begin
+
+instance proof
+  fix x y z :: "'a option"
+  show "x \<sqinter> y \<le> x"
+    by - (cases x, simp_all, cases y, simp_all)
+  show "x \<sqinter> y \<le> y"
+    by - (cases x, simp_all, cases y, simp_all)
+  show "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<sqinter> z"
+    by - (cases x, simp_all, cases y, simp_all, cases z, simp_all)
+qed
+  
+end
+
+instantiation option :: (semilattice_sup) semilattice_sup
+begin
+
+instance proof
+  fix x y z :: "'a option"
+  show "x \<le> x \<squnion> y"
+    by - (cases x, simp_all, cases y, simp_all)
+  show "y \<le> x \<squnion> y"
+    by - (cases x, simp_all, cases y, simp_all)
+  fix x y z :: "'a option"
+  show "y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<squnion> z \<le> x"
+    by - (cases y, simp_all, cases z, simp_all, cases x, simp_all)
+qed
+
+end
+
+instance option :: (lattice) lattice ..
+
+instance option :: (lattice) bounded_lattice_bot ..
+
+instance option :: (bounded_lattice_top) bounded_lattice_top ..
+
+instance option :: (bounded_lattice_top) bounded_lattice ..
+
+instance option :: (distrib_lattice) distrib_lattice
+proof
+  fix x y z :: "'a option"
+  show "x \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
+    by - (cases x, simp_all, cases y, simp_all, cases z, simp_all add: sup_inf_distrib1 inf_commute)
+qed 
+
+instantiation option :: (complete_lattice) complete_lattice
+begin
+
+definition Inf_option :: "'a option set \<Rightarrow> 'a option" where
+  "\<Sqinter>A = (if None \<in> A then None else Some (\<Sqinter>Option.these A))"
+
+lemma None_in_Inf [simp]:
+  "None \<in> A \<Longrightarrow> \<Sqinter>A = None"
+  by (simp add: Inf_option_def)
+
+definition Sup_option :: "'a option set \<Rightarrow> 'a option" where
+  "\<Squnion>A = (if A = {} \<or> A = {None} then None else Some (\<Squnion>Option.these A))"
+
+lemma empty_Sup [simp]:
+  "\<Squnion>{} = None"
+  by (simp add: Sup_option_def)
+
+lemma singleton_None_Sup [simp]:
+  "\<Squnion>{None} = None"
+  by (simp add: Sup_option_def)
+
+instance proof
+  fix x :: "'a option" and A
+  assume "x \<in> A"
+  then show "\<Sqinter>A \<le> x"
+    by (cases x) (auto simp add: Inf_option_def in_these_eq intro: Inf_lower)
+next
+  fix z :: "'a option" and A
+  assume *: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
+  show "z \<le> \<Sqinter>A"
+  proof (cases z)
+    case None then show ?thesis by simp
+  next
+    case (Some y)
+    show ?thesis
+      by (auto simp add: Inf_option_def in_these_eq Some intro!: Inf_greatest dest!: *)
+  qed
+next
+  fix x :: "'a option" and A
+  assume "x \<in> A"
+  then show "x \<le> \<Squnion>A"
+    by (cases x) (auto simp add: Sup_option_def in_these_eq intro: Sup_upper)
+next
+  fix z :: "'a option" and A
+  assume *: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
+  show "\<Squnion>A \<le> z "
+  proof (cases z)
+    case None
+    with * have "\<And>x. x \<in> A \<Longrightarrow> x = None" by (auto dest: less_eq_option_None_is_None)
+    then have "A = {} \<or> A = {None}" by blast
+    then show ?thesis by (simp add: Sup_option_def)
+  next
+    case (Some y)
+    from * have "\<And>w. Some w \<in> A \<Longrightarrow> Some w \<le> z" .
+    with Some have "\<And>w. w \<in> Option.these A \<Longrightarrow> w \<le> y"
+      by (simp add: in_these_eq)
+    then have "\<Squnion>Option.these A \<le> y" by (rule Sup_least)
+    with Some show ?thesis by (simp add: Sup_option_def)
+  qed
+qed
+
+end
+
+lemma Some_Inf:
+  "Some (\<Sqinter>A) = \<Sqinter>(Some ` A)"
+  by (auto simp add: Inf_option_def)
+
+lemma Some_Sup:
+  "A \<noteq> {} \<Longrightarrow> Some (\<Squnion>A) = \<Squnion>(Some ` A)"
+  by (auto simp add: Sup_option_def)
+
+lemma Some_INF:
+  "Some (\<Sqinter>x\<in>A. f x) = (\<Sqinter>x\<in>A. Some (f x))"
+  by (simp add: INF_def Some_Inf image_image)
+
+lemma Some_SUP:
+  "A \<noteq> {} \<Longrightarrow> Some (\<Squnion>x\<in>A. f x) = (\<Squnion>x\<in>A. Some (f x))"
+  by (simp add: SUP_def Some_Sup image_image)
+
+instantiation option :: (complete_distrib_lattice) complete_distrib_lattice
+begin
+
+instance proof
+  fix a :: "'a option" and B
+  show "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
+  proof (cases a)
+    case None
+    then show ?thesis by (simp add: INF_def)
+  next
+    case (Some c)
+    show ?thesis
+    proof (cases "None \<in> B")
+      case True
+      then have "Some c = (\<Sqinter>b\<in>B. Some c \<squnion> b)"
+        by (auto intro!: antisym INF_lower2 INF_greatest)
+      with True Some show ?thesis by simp
+    next
+      case False then have B: "{x \<in> B. \<exists>y. x = Some y} = B" by auto (metis not_Some_eq)
+      from sup_Inf have "Some c \<squnion> Some (\<Sqinter>Option.these B) = Some (\<Sqinter>b\<in>Option.these B. c \<squnion> b)" by simp
+      then have "Some c \<squnion> \<Sqinter>(Some ` Option.these B) = (\<Sqinter>x\<in>Some ` Option.these B. Some c \<squnion> x)"
+        by (simp add: Some_INF Some_Inf)
+      with Some B show ?thesis by (simp add: Some_image_these_eq)
+    qed
+  qed
+  show "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
+  proof (cases a)
+    case None
+    then show ?thesis by (simp add: SUP_def image_constant_conv bot_option_def)
+  next
+    case (Some c)
+    show ?thesis
+    proof (cases "B = {} \<or> B = {None}")
+      case True
+      then show ?thesis by (auto simp add: SUP_def)
+    next
+      have B: "B = {x \<in> B. \<exists>y. x = Some y} \<union> {x \<in> B. x = None}"
+        by auto
+      then have Sup_B: "\<Squnion>B = \<Squnion>({x \<in> B. \<exists>y. x = Some y} \<union> {x \<in> B. x = None})"
+        and SUP_B: "\<And>f. (\<Squnion>x \<in> B. f x) = (\<Squnion>x \<in> {x \<in> B. \<exists>y. x = Some y} \<union> {x \<in> B. x = None}. f x)"
+        by simp_all
+      have Sup_None: "\<Squnion>{x. x = None \<and> x \<in> B} = None"
+        by (simp add: bot_option_def [symmetric])
+      have SUP_None: "(\<Squnion>x\<in>{x. x = None \<and> x \<in> B}. Some c \<sqinter> x) = None"
+        by (simp add: bot_option_def [symmetric])
+      case False then have "Option.these B \<noteq> {}" by (simp add: these_not_empty_eq)
+      moreover from inf_Sup have "Some c \<sqinter> Some (\<Squnion>Option.these B) = Some (\<Squnion>b\<in>Option.these B. c \<sqinter> b)"
+        by simp
+      ultimately have "Some c \<sqinter> \<Squnion>(Some ` Option.these B) = (\<Squnion>x\<in>Some ` Option.these B. Some c \<sqinter> x)"
+        by (simp add: Some_SUP Some_Sup)
+      with Some show ?thesis
+        by (simp add: Some_image_these_eq Sup_B SUP_B Sup_None SUP_None SUP_union Sup_union_distrib)
+    qed
+  qed
+qed
+
+end
+
+instantiation option :: (complete_linorder) complete_linorder
+begin
+
+instance ..
+
+end
+
+
+no_notation
+  bot ("\<bottom>") and
+  top ("\<top>") and
+  inf  (infixl "\<sqinter>" 70) and
+  sup  (infixl "\<squnion>" 65) and
+  Inf  ("\<Sqinter>_" [900] 900) and
+  Sup  ("\<Squnion>_" [900] 900)
+
+no_syntax (xsymbols)
+  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
+  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
+  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
+  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
+
+end
+
diff -r 3601bf546775 -r d383fd5dbd3c src/HOL/Option.thy
--- a/src/HOL/Option.thy	Fri Sep 07 08:35:35 2012 +0200
+++ b/src/HOL/Option.thy	Fri Sep 07 08:36:04 2012 +0200
@@ -117,9 +117,57 @@
 lemma bind_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> bind x f = bind y g"
 by (cases x) auto
 
-hide_const (open) set map bind
+definition these :: "'a option set \<Rightarrow> 'a set"
+where
+  "these A = the ` {x \<in> A. x \<noteq> None}"
+
+lemma these_empty [simp]:
+  "these {} = {}"
+  by (simp add: these_def)
+
+lemma these_insert_None [simp]:
+  "these (insert None A) = these A"
+  by (auto simp add: these_def)
+
+lemma these_insert_Some [simp]:
+  "these (insert (Some x) A) = insert x (these A)"
+proof -
+  have "{y \<in> insert (Some x) A. y \<noteq> None} = insert (Some x) {y \<in> A. y \<noteq> None}"
+    by auto
+  then show ?thesis by (simp add: these_def)
+qed
+
+lemma in_these_eq:
+  "x \<in> these A \<longleftrightarrow> Some x \<in> A"
+proof
+  assume "Some x \<in> A"
+  then obtain B where "A = insert (Some x) B" by auto
+  then show "x \<in> these A" by (auto simp add: these_def intro!: image_eqI)
+next
+  assume "x \<in> these A"
+  then show "Some x \<in> A" by (auto simp add: these_def)
+qed
+
+lemma these_image_Some_eq [simp]:
+  "these (Some ` A) = A"
+  by (auto simp add: these_def intro!: image_eqI)
+
+lemma Some_image_these_eq:
+  "Some ` these A = {x\<in>A. x \<noteq> None}"
+  by (auto simp add: these_def image_image intro!: image_eqI)
+
+lemma these_empty_eq:
+  "these B = {} \<longleftrightarrow> B = {} \<or> B = {None}"
+  by (auto simp add: these_def)
+
+lemma these_not_empty_eq:
+  "these B \<noteq> {} \<longleftrightarrow> B \<noteq> {} \<and> B \<noteq> {None}"
+  by (auto simp add: these_empty_eq)
+
+hide_const (open) set map bind these
 hide_fact (open) map_cong bind_cong
 
+
 subsubsection {* Code generator setup *}
 
 definition is_none :: "'a option \<Rightarrow> bool" where
@@ -164,3 +212,4 @@
   Option None Some
 
 end
+