src/HOL/Library/Lattice_Constructions.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (3 months ago)
changeset 69946 494934c30f38
parent 62390 842917225d56
permissions -rw-r--r--
improved code equations taken over from AFP
     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