lattice instances for option type
authorhaftmann
Fri Sep 07 08:20:18 2012 +0200 (2012-09-07)
changeset 49190e1e1d427747d
parent 49189 3f85cd15a0cc
child 49192 d383fd5dbd3c
lattice instances for option type
CONTRIBUTORS
NEWS
src/HOL/Library/Option_ord.thy
     1.1 --- a/CONTRIBUTORS	Fri Sep 07 08:20:18 2012 +0200
     1.2 +++ b/CONTRIBUTORS	Fri Sep 07 08:20:18 2012 +0200
     1.3 @@ -6,6 +6,9 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* September 2012: Florian Haftmann, TUM
     1.8 +  Lattice instances for type option.
     1.9 +
    1.10  * September 2012: Christian Sternagel, JAIST
    1.11    Consolidated HOL/Library (theories: Prefix_Order, Sublist, and
    1.12    Sublist_Order) w.r.t. prefixes, suffixes, and embedding on lists.
     2.1 --- a/NEWS	Fri Sep 07 08:20:18 2012 +0200
     2.2 +++ b/NEWS	Fri Sep 07 08:20:18 2012 +0200
     2.3 @@ -41,6 +41,9 @@
     2.4  
     2.5  *** HOL ***
     2.6  
     2.7 +* Theory "Library/Option_ord" provides instantiation of option type
     2.8 +to lattice type classes.
     2.9 +
    2.10  * New combinator "Option.these" with type "'a option set => 'a option".
    2.11  
    2.12  * Renamed theory Library/List_Prefix to Library/Sublist.
     3.1 --- a/src/HOL/Library/Option_ord.thy	Fri Sep 07 08:20:18 2012 +0200
     3.2 +++ b/src/HOL/Library/Option_ord.thy	Fri Sep 07 08:20:18 2012 +0200
     3.3 @@ -8,6 +8,21 @@
     3.4  imports Option Main
     3.5  begin
     3.6  
     3.7 +notation
     3.8 +  bot ("\<bottom>") and
     3.9 +  top ("\<top>") and
    3.10 +  inf  (infixl "\<sqinter>" 70) and
    3.11 +  sup  (infixl "\<squnion>" 65) and
    3.12 +  Inf  ("\<Sqinter>_" [900] 900) and
    3.13 +  Sup  ("\<Squnion>_" [900] 900)
    3.14 +
    3.15 +syntax (xsymbols)
    3.16 +  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
    3.17 +  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
    3.18 +  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
    3.19 +  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
    3.20 +
    3.21 +
    3.22  instantiation option :: (preorder) preorder
    3.23  begin
    3.24  
    3.25 @@ -61,7 +76,8 @@
    3.26  instantiation option :: (order) bot
    3.27  begin
    3.28  
    3.29 -definition "bot = None"
    3.30 +definition bot_option where
    3.31 +  "\<bottom> = None"
    3.32  
    3.33  instance proof
    3.34  qed (simp add: bot_option_def)
    3.35 @@ -71,7 +87,8 @@
    3.36  instantiation option :: (top) top
    3.37  begin
    3.38  
    3.39 -definition "top = Some top"
    3.40 +definition top_option where
    3.41 +  "\<top> = Some \<top>"
    3.42  
    3.43  instance proof
    3.44  qed (simp add: top_option_def less_eq_option_def split: option.split)
    3.45 @@ -106,4 +123,254 @@
    3.46    qed
    3.47  qed
    3.48  
    3.49 +instantiation option :: (inf) inf
    3.50 +begin
    3.51 +
    3.52 +definition inf_option where
    3.53 +  "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)))"
    3.54 +
    3.55 +lemma inf_None_1 [simp, code]:
    3.56 +  "None \<sqinter> y = None"
    3.57 +  by (simp add: inf_option_def)
    3.58 +
    3.59 +lemma inf_None_2 [simp, code]:
    3.60 +  "x \<sqinter> None = None"
    3.61 +  by (cases x) (simp_all add: inf_option_def)
    3.62 +
    3.63 +lemma inf_Some [simp, code]:
    3.64 +  "Some x \<sqinter> Some y = Some (x \<sqinter> y)"
    3.65 +  by (simp add: inf_option_def)
    3.66 +
    3.67 +instance ..
    3.68 +
    3.69  end
    3.70 +
    3.71 +instantiation option :: (sup) sup
    3.72 +begin
    3.73 +
    3.74 +definition sup_option where
    3.75 +  "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)))"
    3.76 +
    3.77 +lemma sup_None_1 [simp, code]:
    3.78 +  "None \<squnion> y = y"
    3.79 +  by (simp add: sup_option_def)
    3.80 +
    3.81 +lemma sup_None_2 [simp, code]:
    3.82 +  "x \<squnion> None = x"
    3.83 +  by (cases x) (simp_all add: sup_option_def)
    3.84 +
    3.85 +lemma sup_Some [simp, code]:
    3.86 +  "Some x \<squnion> Some y = Some (x \<squnion> y)"
    3.87 +  by (simp add: sup_option_def)
    3.88 +
    3.89 +instance ..
    3.90 +
    3.91 +end
    3.92 +
    3.93 +instantiation option :: (semilattice_inf) semilattice_inf
    3.94 +begin
    3.95 +
    3.96 +instance proof
    3.97 +  fix x y z :: "'a option"
    3.98 +  show "x \<sqinter> y \<le> x"
    3.99 +    by - (cases x, simp_all, cases y, simp_all)
   3.100 +  show "x \<sqinter> y \<le> y"
   3.101 +    by - (cases x, simp_all, cases y, simp_all)
   3.102 +  show "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<sqinter> z"
   3.103 +    by - (cases x, simp_all, cases y, simp_all, cases z, simp_all)
   3.104 +qed
   3.105 +  
   3.106 +end
   3.107 +
   3.108 +instantiation option :: (semilattice_sup) semilattice_sup
   3.109 +begin
   3.110 +
   3.111 +instance proof
   3.112 +  fix x y z :: "'a option"
   3.113 +  show "x \<le> x \<squnion> y"
   3.114 +    by - (cases x, simp_all, cases y, simp_all)
   3.115 +  show "y \<le> x \<squnion> y"
   3.116 +    by - (cases x, simp_all, cases y, simp_all)
   3.117 +  fix x y z :: "'a option"
   3.118 +  show "y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<squnion> z \<le> x"
   3.119 +    by - (cases y, simp_all, cases z, simp_all, cases x, simp_all)
   3.120 +qed
   3.121 +
   3.122 +end
   3.123 +
   3.124 +instance option :: (lattice) lattice ..
   3.125 +
   3.126 +instance option :: (lattice) bounded_lattice_bot ..
   3.127 +
   3.128 +instance option :: (bounded_lattice_top) bounded_lattice_top ..
   3.129 +
   3.130 +instance option :: (bounded_lattice_top) bounded_lattice ..
   3.131 +
   3.132 +instance option :: (distrib_lattice) distrib_lattice
   3.133 +proof
   3.134 +  fix x y z :: "'a option"
   3.135 +  show "x \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   3.136 +    by - (cases x, simp_all, cases y, simp_all, cases z, simp_all add: sup_inf_distrib1 inf_commute)
   3.137 +qed 
   3.138 +
   3.139 +instantiation option :: (complete_lattice) complete_lattice
   3.140 +begin
   3.141 +
   3.142 +definition Inf_option :: "'a option set \<Rightarrow> 'a option" where
   3.143 +  "\<Sqinter>A = (if None \<in> A then None else Some (\<Sqinter>Option.these A))"
   3.144 +
   3.145 +lemma None_in_Inf [simp]:
   3.146 +  "None \<in> A \<Longrightarrow> \<Sqinter>A = None"
   3.147 +  by (simp add: Inf_option_def)
   3.148 +
   3.149 +definition Sup_option :: "'a option set \<Rightarrow> 'a option" where
   3.150 +  "\<Squnion>A = (if A = {} \<or> A = {None} then None else Some (\<Squnion>Option.these A))"
   3.151 +
   3.152 +lemma empty_Sup [simp]:
   3.153 +  "\<Squnion>{} = None"
   3.154 +  by (simp add: Sup_option_def)
   3.155 +
   3.156 +lemma singleton_None_Sup [simp]:
   3.157 +  "\<Squnion>{None} = None"
   3.158 +  by (simp add: Sup_option_def)
   3.159 +
   3.160 +instance proof
   3.161 +  fix x :: "'a option" and A
   3.162 +  assume "x \<in> A"
   3.163 +  then show "\<Sqinter>A \<le> x"
   3.164 +    by (cases x) (auto simp add: Inf_option_def in_these_eq intro: Inf_lower)
   3.165 +next
   3.166 +  fix z :: "'a option" and A
   3.167 +  assume *: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
   3.168 +  show "z \<le> \<Sqinter>A"
   3.169 +  proof (cases z)
   3.170 +    case None then show ?thesis by simp
   3.171 +  next
   3.172 +    case (Some y)
   3.173 +    show ?thesis
   3.174 +      by (auto simp add: Inf_option_def in_these_eq Some intro!: Inf_greatest dest!: *)
   3.175 +  qed
   3.176 +next
   3.177 +  fix x :: "'a option" and A
   3.178 +  assume "x \<in> A"
   3.179 +  then show "x \<le> \<Squnion>A"
   3.180 +    by (cases x) (auto simp add: Sup_option_def in_these_eq intro: Sup_upper)
   3.181 +next
   3.182 +  fix z :: "'a option" and A
   3.183 +  assume *: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
   3.184 +  show "\<Squnion>A \<le> z "
   3.185 +  proof (cases z)
   3.186 +    case None
   3.187 +    with * have "\<And>x. x \<in> A \<Longrightarrow> x = None" by (auto dest: less_eq_option_None_is_None)
   3.188 +    then have "A = {} \<or> A = {None}" by blast
   3.189 +    then show ?thesis by (simp add: Sup_option_def)
   3.190 +  next
   3.191 +    case (Some y)
   3.192 +    from * have "\<And>w. Some w \<in> A \<Longrightarrow> Some w \<le> z" .
   3.193 +    with Some have "\<And>w. w \<in> Option.these A \<Longrightarrow> w \<le> y"
   3.194 +      by (simp add: in_these_eq)
   3.195 +    then have "\<Squnion>Option.these A \<le> y" by (rule Sup_least)
   3.196 +    with Some show ?thesis by (simp add: Sup_option_def)
   3.197 +  qed
   3.198 +qed
   3.199 +
   3.200 +end
   3.201 +
   3.202 +lemma Some_Inf:
   3.203 +  "Some (\<Sqinter>A) = \<Sqinter>(Some ` A)"
   3.204 +  by (auto simp add: Inf_option_def)
   3.205 +
   3.206 +lemma Some_Sup:
   3.207 +  "A \<noteq> {} \<Longrightarrow> Some (\<Squnion>A) = \<Squnion>(Some ` A)"
   3.208 +  by (auto simp add: Sup_option_def)
   3.209 +
   3.210 +lemma Some_INF:
   3.211 +  "Some (\<Sqinter>x\<in>A. f x) = (\<Sqinter>x\<in>A. Some (f x))"
   3.212 +  by (simp add: INF_def Some_Inf image_image)
   3.213 +
   3.214 +lemma Some_SUP:
   3.215 +  "A \<noteq> {} \<Longrightarrow> Some (\<Squnion>x\<in>A. f x) = (\<Squnion>x\<in>A. Some (f x))"
   3.216 +  by (simp add: SUP_def Some_Sup image_image)
   3.217 +
   3.218 +instantiation option :: (complete_distrib_lattice) complete_distrib_lattice
   3.219 +begin
   3.220 +
   3.221 +instance proof
   3.222 +  fix a :: "'a option" and B
   3.223 +  show "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
   3.224 +  proof (cases a)
   3.225 +    case None
   3.226 +    then show ?thesis by (simp add: INF_def)
   3.227 +  next
   3.228 +    case (Some c)
   3.229 +    show ?thesis
   3.230 +    proof (cases "None \<in> B")
   3.231 +      case True
   3.232 +      then have "Some c = (\<Sqinter>b\<in>B. Some c \<squnion> b)"
   3.233 +        by (auto intro!: antisym INF_lower2 INF_greatest)
   3.234 +      with True Some show ?thesis by simp
   3.235 +    next
   3.236 +      case False then have B: "{x \<in> B. \<exists>y. x = Some y} = B" by auto (metis not_Some_eq)
   3.237 +      from sup_Inf have "Some c \<squnion> Some (\<Sqinter>Option.these B) = Some (\<Sqinter>b\<in>Option.these B. c \<squnion> b)" by simp
   3.238 +      then have "Some c \<squnion> \<Sqinter>(Some ` Option.these B) = (\<Sqinter>x\<in>Some ` Option.these B. Some c \<squnion> x)"
   3.239 +        by (simp add: Some_INF Some_Inf)
   3.240 +      with Some B show ?thesis by (simp add: Some_image_these_eq)
   3.241 +    qed
   3.242 +  qed
   3.243 +  show "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
   3.244 +  proof (cases a)
   3.245 +    case None
   3.246 +    then show ?thesis by (simp add: SUP_def image_constant_conv bot_option_def)
   3.247 +  next
   3.248 +    case (Some c)
   3.249 +    show ?thesis
   3.250 +    proof (cases "B = {} \<or> B = {None}")
   3.251 +      case True
   3.252 +      then show ?thesis by (auto simp add: SUP_def)
   3.253 +    next
   3.254 +      have B: "B = {x \<in> B. \<exists>y. x = Some y} \<union> {x \<in> B. x = None}"
   3.255 +        by auto
   3.256 +      then have Sup_B: "\<Squnion>B = \<Squnion>({x \<in> B. \<exists>y. x = Some y} \<union> {x \<in> B. x = None})"
   3.257 +        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)"
   3.258 +        by simp_all
   3.259 +      have Sup_None: "\<Squnion>{x. x = None \<and> x \<in> B} = None"
   3.260 +        by (simp add: bot_option_def [symmetric])
   3.261 +      have SUP_None: "(\<Squnion>x\<in>{x. x = None \<and> x \<in> B}. Some c \<sqinter> x) = None"
   3.262 +        by (simp add: bot_option_def [symmetric])
   3.263 +      case False then have "Option.these B \<noteq> {}" by (simp add: these_not_empty_eq)
   3.264 +      moreover from inf_Sup have "Some c \<sqinter> Some (\<Squnion>Option.these B) = Some (\<Squnion>b\<in>Option.these B. c \<sqinter> b)"
   3.265 +        by simp
   3.266 +      ultimately have "Some c \<sqinter> \<Squnion>(Some ` Option.these B) = (\<Squnion>x\<in>Some ` Option.these B. Some c \<sqinter> x)"
   3.267 +        by (simp add: Some_SUP Some_Sup)
   3.268 +      with Some show ?thesis
   3.269 +        by (simp add: Some_image_these_eq Sup_B SUP_B Sup_None SUP_None SUP_union Sup_union_distrib)
   3.270 +    qed
   3.271 +  qed
   3.272 +qed
   3.273 +
   3.274 +end
   3.275 +
   3.276 +instantiation option :: (complete_linorder) complete_linorder
   3.277 +begin
   3.278 +
   3.279 +instance ..
   3.280 +
   3.281 +end
   3.282 +
   3.283 +
   3.284 +no_notation
   3.285 +  bot ("\<bottom>") and
   3.286 +  top ("\<top>") and
   3.287 +  inf  (infixl "\<sqinter>" 70) and
   3.288 +  sup  (infixl "\<squnion>" 65) and
   3.289 +  Inf  ("\<Sqinter>_" [900] 900) and
   3.290 +  Sup  ("\<Squnion>_" [900] 900)
   3.291 +
   3.292 +no_syntax (xsymbols)
   3.293 +  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
   3.294 +  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
   3.295 +  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
   3.296 +  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
   3.297 +
   3.298 +end
   3.299 +