src/HOL/Library/Lattice_Constructions.thy
 author wenzelm Tue May 15 13:57:39 2018 +0200 (16 months ago) changeset 68189 6163c90694ef parent 62390 842917225d56 permissions -rw-r--r--
```     1 (*  Title:      HOL/Library/Lattice_Constructions.thy
```
```     2     Author:     Lukas Bulwahn
```
```     3     Copyright   2010 TU Muenchen
```
```     4 *)
```
```     5
```
```     6 theory Lattice_Constructions
```
```     7 imports Main
```
```     8 begin
```
```     9
```
```    10 subsection \<open>Values extended by a bottom element\<close>
```
```    11
```
```    12 datatype 'a bot = Value 'a | Bot
```
```    13
```
```    14 instantiation bot :: (preorder) preorder
```
```    15 begin
```
```    16
```
```    17 definition less_eq_bot where
```
```    18   "x \<le> y \<longleftrightarrow> (case x of Bot \<Rightarrow> True | Value x \<Rightarrow> (case y of Bot \<Rightarrow> False | Value y \<Rightarrow> x \<le> y))"
```
```    19
```
```    20 definition less_bot where
```
```    21   "x < y \<longleftrightarrow> (case y of Bot \<Rightarrow> False | Value y \<Rightarrow> (case x of Bot \<Rightarrow> True | Value x \<Rightarrow> x < y))"
```
```    22
```
```    23 lemma less_eq_bot_Bot [simp]: "Bot \<le> x"
```
```    24   by (simp add: less_eq_bot_def)
```
```    25
```
```    26 lemma less_eq_bot_Bot_code [code]: "Bot \<le> x \<longleftrightarrow> True"
```
```    27   by simp
```
```    28
```
```    29 lemma less_eq_bot_Bot_is_Bot: "x \<le> Bot \<Longrightarrow> x = Bot"
```
```    30   by (cases x) (simp_all add: less_eq_bot_def)
```
```    31
```
```    32 lemma less_eq_bot_Value_Bot [simp, code]: "Value x \<le> Bot \<longleftrightarrow> False"
```
```    33   by (simp add: less_eq_bot_def)
```
```    34
```
```    35 lemma less_eq_bot_Value [simp, code]: "Value x \<le> Value y \<longleftrightarrow> x \<le> y"
```
```    36   by (simp add: less_eq_bot_def)
```
```    37
```
```    38 lemma less_bot_Bot [simp, code]: "x < Bot \<longleftrightarrow> False"
```
```    39   by (simp add: less_bot_def)
```
```    40
```
```    41 lemma less_bot_Bot_is_Value: "Bot < x \<Longrightarrow> \<exists>z. x = Value z"
```
```    42   by (cases x) (simp_all add: less_bot_def)
```
```    43
```
```    44 lemma less_bot_Bot_Value [simp]: "Bot < Value x"
```
```    45   by (simp add: less_bot_def)
```
```    46
```
```    47 lemma less_bot_Bot_Value_code [code]: "Bot < Value x \<longleftrightarrow> True"
```
```    48   by simp
```
```    49
```
```    50 lemma less_bot_Value [simp, code]: "Value x < Value y \<longleftrightarrow> x < y"
```
```    51   by (simp add: less_bot_def)
```
```    52
```
```    53 instance
```
```    54   by standard
```
```    55     (auto simp add: less_eq_bot_def less_bot_def less_le_not_le elim: order_trans split: bot.splits)
```
```    56
```
```    57 end
```
```    58
```
```    59 instance bot :: (order) order
```
```    60   by standard (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
```
```    61
```
```    62 instance bot :: (linorder) linorder
```
```    63   by standard (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
```
```    64
```
```    65 instantiation bot :: (order) bot
```
```    66 begin
```
```    67   definition "bot = Bot"
```
```    68   instance ..
```
```    69 end
```
```    70
```
```    71 instantiation bot :: (top) top
```
```    72 begin
```
```    73   definition "top = Value top"
```
```    74   instance ..
```
```    75 end
```
```    76
```
```    77 instantiation bot :: (semilattice_inf) semilattice_inf
```
```    78 begin
```
```    79
```
```    80 definition inf_bot
```
```    81 where
```
```    82   "inf x y =
```
```    83     (case x of
```
```    84       Bot \<Rightarrow> Bot
```
```    85     | Value v \<Rightarrow>
```
```    86         (case y of
```
```    87           Bot \<Rightarrow> Bot
```
```    88         | Value v' \<Rightarrow> Value (inf v v')))"
```
```    89
```
```    90 instance
```
```    91   by standard (auto simp add: inf_bot_def less_eq_bot_def split: bot.splits)
```
```    92
```
```    93 end
```
```    94
```
```    95 instantiation bot :: (semilattice_sup) semilattice_sup
```
```    96 begin
```
```    97
```
```    98 definition sup_bot
```
```    99 where
```
```   100   "sup x y =
```
```   101     (case x of
```
```   102       Bot \<Rightarrow> y
```
```   103     | Value v \<Rightarrow>
```
```   104         (case y of
```
```   105           Bot \<Rightarrow> x
```
```   106         | Value v' \<Rightarrow> Value (sup v v')))"
```
```   107
```
```   108 instance
```
```   109   by standard (auto simp add: sup_bot_def less_eq_bot_def split: bot.splits)
```
```   110
```
```   111 end
```
```   112
```
```   113 instance bot :: (lattice) bounded_lattice_bot
```
```   114   by intro_classes (simp add: bot_bot_def)
```
```   115
```
```   116
```
```   117 subsection \<open>Values extended by a top element\<close>
```
```   118
```
```   119 datatype 'a top = Value 'a | Top
```
```   120
```
```   121 instantiation top :: (preorder) preorder
```
```   122 begin
```
```   123
```
```   124 definition less_eq_top where
```
```   125   "x \<le> y \<longleftrightarrow> (case y of Top \<Rightarrow> True | Value y \<Rightarrow> (case x of Top \<Rightarrow> False | Value x \<Rightarrow> x \<le> y))"
```
```   126
```
```   127 definition less_top where
```
```   128   "x < y \<longleftrightarrow> (case x of Top \<Rightarrow> False | Value x \<Rightarrow> (case y of Top \<Rightarrow> True | Value y \<Rightarrow> x < y))"
```
```   129
```
```   130 lemma less_eq_top_Top [simp]: "x \<le> Top"
```
```   131   by (simp add: less_eq_top_def)
```
```   132
```
```   133 lemma less_eq_top_Top_code [code]: "x \<le> Top \<longleftrightarrow> True"
```
```   134   by simp
```
```   135
```
```   136 lemma less_eq_top_is_Top: "Top \<le> x \<Longrightarrow> x = Top"
```
```   137   by (cases x) (simp_all add: less_eq_top_def)
```
```   138
```
```   139 lemma less_eq_top_Top_Value [simp, code]: "Top \<le> Value x \<longleftrightarrow> False"
```
```   140   by (simp add: less_eq_top_def)
```
```   141
```
```   142 lemma less_eq_top_Value_Value [simp, code]: "Value x \<le> Value y \<longleftrightarrow> x \<le> y"
```
```   143   by (simp add: less_eq_top_def)
```
```   144
```
```   145 lemma less_top_Top [simp, code]: "Top < x \<longleftrightarrow> False"
```
```   146   by (simp add: less_top_def)
```
```   147
```
```   148 lemma less_top_Top_is_Value: "x < Top \<Longrightarrow> \<exists>z. x = Value z"
```
```   149   by (cases x) (simp_all add: less_top_def)
```
```   150
```
```   151 lemma less_top_Value_Top [simp]: "Value x < Top"
```
```   152   by (simp add: less_top_def)
```
```   153
```
```   154 lemma less_top_Value_Top_code [code]: "Value x < Top \<longleftrightarrow> True"
```
```   155   by simp
```
```   156
```
```   157 lemma less_top_Value [simp, code]: "Value x < Value y \<longleftrightarrow> x < y"
```
```   158   by (simp add: less_top_def)
```
```   159
```
```   160 instance
```
```   161   by standard
```
```   162     (auto simp add: less_eq_top_def less_top_def less_le_not_le elim: order_trans split: top.splits)
```
```   163
```
```   164 end
```
```   165
```
```   166 instance top :: (order) order
```
```   167   by standard (auto simp add: less_eq_top_def less_top_def split: top.splits)
```
```   168
```
```   169 instance top :: (linorder) linorder
```
```   170   by standard (auto simp add: less_eq_top_def less_top_def split: top.splits)
```
```   171
```
```   172 instantiation top :: (order) top
```
```   173 begin
```
```   174   definition "top = Top"
```
```   175   instance ..
```
```   176 end
```
```   177
```
```   178 instantiation top :: (bot) bot
```
```   179 begin
```
```   180   definition "bot = Value bot"
```
```   181   instance ..
```
```   182 end
```
```   183
```
```   184 instantiation top :: (semilattice_inf) semilattice_inf
```
```   185 begin
```
```   186
```
```   187 definition inf_top
```
```   188 where
```
```   189   "inf x y =
```
```   190     (case x of
```
```   191       Top \<Rightarrow> y
```
```   192     | Value v \<Rightarrow>
```
```   193         (case y of
```
```   194           Top \<Rightarrow> x
```
```   195         | Value v' \<Rightarrow> Value (inf v v')))"
```
```   196
```
```   197 instance
```
```   198   by standard (auto simp add: inf_top_def less_eq_top_def split: top.splits)
```
```   199
```
```   200 end
```
```   201
```
```   202 instantiation top :: (semilattice_sup) semilattice_sup
```
```   203 begin
```
```   204
```
```   205 definition sup_top
```
```   206 where
```
```   207   "sup x y =
```
```   208     (case x of
```
```   209       Top \<Rightarrow> Top
```
```   210     | Value v \<Rightarrow>
```
```   211         (case y of
```
```   212           Top \<Rightarrow> Top
```
```   213         | Value v' \<Rightarrow> Value (sup v v')))"
```
```   214
```
```   215 instance
```
```   216   by standard (auto simp add: sup_top_def less_eq_top_def split: top.splits)
```
```   217
```
```   218 end
```
```   219
```
```   220 instance top :: (lattice) bounded_lattice_top
```
```   221   by standard (simp add: top_top_def)
```
```   222
```
```   223
```
```   224 subsection \<open>Values extended by a top and a bottom element\<close>
```
```   225
```
```   226 datatype 'a flat_complete_lattice = Value 'a | Bot | Top
```
```   227
```
```   228 instantiation flat_complete_lattice :: (type) order
```
```   229 begin
```
```   230
```
```   231 definition less_eq_flat_complete_lattice
```
```   232 where
```
```   233   "x \<le> y \<equiv>
```
```   234     (case x of
```
```   235       Bot \<Rightarrow> True
```
```   236     | Value v1 \<Rightarrow>
```
```   237         (case y of
```
```   238           Bot \<Rightarrow> False
```
```   239         | Value v2 \<Rightarrow> v1 = v2
```
```   240         | Top \<Rightarrow> True)
```
```   241     | Top \<Rightarrow> y = Top)"
```
```   242
```
```   243 definition less_flat_complete_lattice
```
```   244 where
```
```   245   "x < y =
```
```   246     (case x of
```
```   247       Bot \<Rightarrow> y \<noteq> Bot
```
```   248     | Value v1 \<Rightarrow> y = Top
```
```   249     | Top \<Rightarrow> False)"
```
```   250
```
```   251 lemma [simp]: "Bot \<le> y"
```
```   252   unfolding less_eq_flat_complete_lattice_def by auto
```
```   253
```
```   254 lemma [simp]: "y \<le> Top"
```
```   255   unfolding less_eq_flat_complete_lattice_def by (auto split: flat_complete_lattice.splits)
```
```   256
```
```   257 lemma greater_than_two_values:
```
```   258   assumes "a \<noteq> b" "Value a \<le> z" "Value b \<le> z"
```
```   259   shows "z = Top"
```
```   260   using assms
```
```   261   by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
```
```   262
```
```   263 lemma lesser_than_two_values:
```
```   264   assumes "a \<noteq> b" "z \<le> Value a" "z \<le> Value b"
```
```   265   shows "z = Bot"
```
```   266   using assms
```
```   267   by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
```
```   268
```
```   269 instance
```
```   270   by standard
```
```   271     (auto simp add: less_eq_flat_complete_lattice_def less_flat_complete_lattice_def
```
```   272       split: flat_complete_lattice.splits)
```
```   273
```
```   274 end
```
```   275
```
```   276 instantiation flat_complete_lattice :: (type) bot
```
```   277 begin
```
```   278   definition "bot = Bot"
```
```   279   instance ..
```
```   280 end
```
```   281
```
```   282 instantiation flat_complete_lattice :: (type) top
```
```   283 begin
```
```   284   definition "top = Top"
```
```   285   instance ..
```
```   286 end
```
```   287
```
```   288 instantiation flat_complete_lattice :: (type) lattice
```
```   289 begin
```
```   290
```
```   291 definition inf_flat_complete_lattice
```
```   292 where
```
```   293   "inf x y =
```
```   294     (case x of
```
```   295       Bot \<Rightarrow> Bot
```
```   296     | Value v1 \<Rightarrow>
```
```   297         (case y of
```
```   298           Bot \<Rightarrow> Bot
```
```   299         | Value v2 \<Rightarrow> if v1 = v2 then x else Bot
```
```   300         | Top \<Rightarrow> x)
```
```   301     | Top \<Rightarrow> y)"
```
```   302
```
```   303 definition sup_flat_complete_lattice
```
```   304 where
```
```   305   "sup x y =
```
```   306     (case x of
```
```   307       Bot \<Rightarrow> y
```
```   308     | Value v1 \<Rightarrow>
```
```   309         (case y of
```
```   310           Bot \<Rightarrow> x
```
```   311         | Value v2 \<Rightarrow> if v1 = v2 then x else Top
```
```   312         | Top \<Rightarrow> Top)
```
```   313     | Top \<Rightarrow> Top)"
```
```   314
```
```   315 instance
```
```   316   by standard
```
```   317     (auto simp add: inf_flat_complete_lattice_def sup_flat_complete_lattice_def
```
```   318       less_eq_flat_complete_lattice_def split: flat_complete_lattice.splits)
```
```   319
```
```   320 end
```
```   321
```
```   322 instantiation flat_complete_lattice :: (type) complete_lattice
```
```   323 begin
```
```   324
```
```   325 definition Sup_flat_complete_lattice
```
```   326 where
```
```   327   "Sup A =
```
```   328     (if A = {} \<or> A = {Bot} then Bot
```
```   329      else if \<exists>v. A - {Bot} = {Value v} then Value (THE v. A - {Bot} = {Value v})
```
```   330      else Top)"
```
```   331
```
```   332 definition Inf_flat_complete_lattice
```
```   333 where
```
```   334   "Inf A =
```
```   335     (if A = {} \<or> A = {Top} then Top
```
```   336      else if \<exists>v. A - {Top} = {Value v} then Value (THE v. A - {Top} = {Value v})
```
```   337      else Bot)"
```
```   338
```
```   339 instance
```
```   340 proof
```
```   341   fix x :: "'a flat_complete_lattice"
```
```   342   fix A
```
```   343   assume "x \<in> A"
```
```   344   {
```
```   345     fix v
```
```   346     assume "A - {Top} = {Value v}"
```
```   347     then have "(THE v. A - {Top} = {Value v}) = v"
```
```   348       by (auto intro!: the1_equality)
```
```   349     moreover
```
```   350     from \<open>x \<in> A\<close> \<open>A - {Top} = {Value v}\<close> have "x = Top \<or> x = Value v"
```
```   351       by auto
```
```   352     ultimately have "Value (THE v. A - {Top} = {Value v}) \<le> x"
```
```   353       by auto
```
```   354   }
```
```   355   with \<open>x \<in> A\<close> show "Inf A \<le> x"
```
```   356     unfolding Inf_flat_complete_lattice_def
```
```   357     by fastforce
```
```   358 next
```
```   359   fix z :: "'a flat_complete_lattice"
```
```   360   fix A
```
```   361   show "z \<le> Inf A" if z: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
```
```   362   proof -
```
```   363     consider "A = {} \<or> A = {Top}"
```
```   364       | "A \<noteq> {}" "A \<noteq> {Top}" "\<exists>v. A - {Top} = {Value v}"
```
```   365       | "A \<noteq> {}" "A \<noteq> {Top}" "\<not> (\<exists>v. A - {Top} = {Value v})"
```
```   366       by blast
```
```   367     then show ?thesis
```
```   368     proof cases
```
```   369       case 1
```
```   370       then have "Inf A = Top"
```
```   371         unfolding Inf_flat_complete_lattice_def by auto
```
```   372       then show ?thesis by simp
```
```   373     next
```
```   374       case 2
```
```   375       then obtain v where v1: "A - {Top} = {Value v}"
```
```   376         by auto
```
```   377       then have v2: "(THE v. A - {Top} = {Value v}) = v"
```
```   378         by (auto intro!: the1_equality)
```
```   379       from 2 v2 have Inf: "Inf A = Value v"
```
```   380         unfolding Inf_flat_complete_lattice_def by simp
```
```   381       from v1 have "Value v \<in> A" by blast
```
```   382       then have "z \<le> Value v" by (rule z)
```
```   383       with Inf show ?thesis by simp
```
```   384     next
```
```   385       case 3
```
```   386       then have Inf: "Inf A = Bot"
```
```   387         unfolding Inf_flat_complete_lattice_def by auto
```
```   388       have "z \<le> Bot"
```
```   389       proof (cases "A - {Top} = {Bot}")
```
```   390         case True
```
```   391         then have "Bot \<in> A" by blast
```
```   392         then show ?thesis by (rule z)
```
```   393       next
```
```   394         case False
```
```   395         from 3 obtain a1 where a1: "a1 \<in> A - {Top}"
```
```   396           by auto
```
```   397         from 3 False a1 obtain a2 where "a2 \<in> A - {Top} \<and> a1 \<noteq> a2"
```
```   398           by (cases a1) auto
```
```   399         with a1 z[of "a1"] z[of "a2"] show ?thesis
```
```   400           apply (cases a1)
```
```   401           apply auto
```
```   402           apply (cases a2)
```
```   403           apply auto
```
```   404           apply (auto dest!: lesser_than_two_values)
```
```   405           done
```
```   406       qed
```
```   407       with Inf show ?thesis by simp
```
```   408     qed
```
```   409   qed
```
```   410 next
```
```   411   fix x :: "'a flat_complete_lattice"
```
```   412   fix A
```
```   413   assume "x \<in> A"
```
```   414   {
```
```   415     fix v
```
```   416     assume "A - {Bot} = {Value v}"
```
```   417     then have "(THE v. A - {Bot} = {Value v}) = v"
```
```   418       by (auto intro!: the1_equality)
```
```   419     moreover
```
```   420     from \<open>x \<in> A\<close> \<open>A - {Bot} = {Value v}\<close> have "x = Bot \<or> x = Value v"
```
```   421       by auto
```
```   422     ultimately have "x \<le> Value (THE v. A - {Bot} = {Value v})"
```
```   423       by auto
```
```   424   }
```
```   425   with \<open>x \<in> A\<close> show "x \<le> Sup A"
```
```   426     unfolding Sup_flat_complete_lattice_def
```
```   427     by fastforce
```
```   428 next
```
```   429   fix z :: "'a flat_complete_lattice"
```
```   430   fix A
```
```   431   show "Sup A \<le> z" if z: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
```
```   432   proof -
```
```   433     consider "A = {} \<or> A = {Bot}"
```
```   434       | "A \<noteq> {}" "A \<noteq> {Bot}" "\<exists>v. A - {Bot} = {Value v}"
```
```   435       | "A \<noteq> {}" "A \<noteq> {Bot}" "\<not> (\<exists>v. A - {Bot} = {Value v})"
```
```   436       by blast
```
```   437     then show ?thesis
```
```   438     proof cases
```
```   439       case 1
```
```   440       then have "Sup A = Bot"
```
```   441         unfolding Sup_flat_complete_lattice_def by auto
```
```   442       then show ?thesis by simp
```
```   443     next
```
```   444       case 2
```
```   445       then obtain v where v1: "A - {Bot} = {Value v}"
```
```   446         by auto
```
```   447       then have v2: "(THE v. A - {Bot} = {Value v}) = v"
```
```   448         by (auto intro!: the1_equality)
```
```   449       from 2 v2 have Sup: "Sup A = Value v"
```
```   450         unfolding Sup_flat_complete_lattice_def by simp
```
```   451       from v1 have "Value v \<in> A" by blast
```
```   452       then have "Value v \<le> z" by (rule z)
```
```   453       with Sup show ?thesis by simp
```
```   454     next
```
```   455       case 3
```
```   456       then have Sup: "Sup A = Top"
```
```   457         unfolding Sup_flat_complete_lattice_def by auto
```
```   458       have "Top \<le> z"
```
```   459       proof (cases "A - {Bot} = {Top}")
```
```   460         case True
```
```   461         then have "Top \<in> A" by blast
```
```   462         then show ?thesis by (rule z)
```
```   463       next
```
```   464         case False
```
```   465         from 3 obtain a1 where a1: "a1 \<in> A - {Bot}"
```
```   466           by auto
```
```   467         from 3 False a1 obtain a2 where "a2 \<in> A - {Bot} \<and> a1 \<noteq> a2"
```
```   468           by (cases a1) auto
```
```   469         with a1 z[of "a1"] z[of "a2"] show ?thesis
```
```   470           apply (cases a1)
```
```   471           apply auto
```
```   472           apply (cases a2)
```
```   473           apply (auto dest!: greater_than_two_values)
```
```   474           done
```
```   475       qed
```
```   476       with Sup show ?thesis by simp
```
```   477     qed
```
```   478   qed
```
```   479 next
```
```   480   show "Inf {} = (top :: 'a flat_complete_lattice)"
```
```   481     by (simp add: Inf_flat_complete_lattice_def top_flat_complete_lattice_def)
```
```   482   show "Sup {} = (bot :: 'a flat_complete_lattice)"
```
```   483     by (simp add: Sup_flat_complete_lattice_def bot_flat_complete_lattice_def)
```
```   484 qed
```
```   485
```
```   486 end
```
```   487
```
```   488 end
```