src/HOL/Library/Lattice_Constructions.thy
author blanchet
Thu Sep 11 19:32:36 2014 +0200 (2014-09-11)
changeset 58310 91ea607a34d8
parent 58249 180f1b3508ed
child 60500 903bb1495239
permissions -rw-r--r--
updated news
     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 {* Values extended by a bottom element *}
    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 proof
    54 qed (auto simp add: less_eq_bot_def less_bot_def less_le_not_le elim: order_trans split: bot.splits)
    55 
    56 end 
    57 
    58 instance bot :: (order) order proof
    59 qed (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
    60 
    61 instance bot :: (linorder) linorder proof
    62 qed (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
    63 
    64 instantiation bot :: (order) bot
    65 begin
    66 
    67 definition "bot = Bot"
    68 
    69 instance ..
    70 
    71 end
    72 
    73 instantiation bot :: (top) top
    74 begin
    75 
    76 definition "top = Value top"
    77 
    78 instance ..
    79 
    80 end
    81 
    82 instantiation bot :: (semilattice_inf) semilattice_inf
    83 begin
    84 
    85 definition inf_bot
    86 where
    87   "inf x y = (case x of Bot => Bot | Value v => (case y of Bot => Bot | Value v' => Value (inf v v')))"
    88 
    89 instance proof
    90 qed (auto simp add: inf_bot_def less_eq_bot_def split: bot.splits)
    91 
    92 end
    93 
    94 instantiation bot :: (semilattice_sup) semilattice_sup
    95 begin
    96 
    97 definition sup_bot
    98 where
    99   "sup x y = (case x of Bot => y | Value v => (case y of Bot => x | Value v' => Value (sup v v')))"
   100 
   101 instance proof
   102 qed (auto simp add: sup_bot_def less_eq_bot_def split: bot.splits)
   103 
   104 end
   105 
   106 instance bot :: (lattice) bounded_lattice_bot
   107 by(intro_classes)(simp add: bot_bot_def)
   108 
   109 section {* Values extended by a top element *}
   110 
   111 datatype 'a top = Value 'a | Top
   112 
   113 instantiation top :: (preorder) preorder
   114 begin
   115 
   116 definition less_eq_top where
   117   "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))"
   118 
   119 definition less_top where
   120   "x < y \<longleftrightarrow> (case x of Top \<Rightarrow> False | Value x \<Rightarrow> (case y of Top \<Rightarrow> True | Value y \<Rightarrow> x < y))"
   121 
   122 lemma less_eq_top_Top [simp]: "x <= Top"
   123   by (simp add: less_eq_top_def)
   124 
   125 lemma less_eq_top_Top_code [code]: "x \<le> Top \<longleftrightarrow> True"
   126   by simp
   127 
   128 lemma less_eq_top_is_Top: "Top \<le> x \<Longrightarrow> x = Top"
   129   by (cases x) (simp_all add: less_eq_top_def)
   130 
   131 lemma less_eq_top_Top_Value [simp, code]: "Top \<le> Value x \<longleftrightarrow> False"
   132   by (simp add: less_eq_top_def)
   133 
   134 lemma less_eq_top_Value_Value [simp, code]: "Value x \<le> Value y \<longleftrightarrow> x \<le> y"
   135   by (simp add: less_eq_top_def)
   136 
   137 lemma less_top_Top [simp, code]: "Top < x \<longleftrightarrow> False"
   138   by (simp add: less_top_def)
   139 
   140 lemma less_top_Top_is_Value: "x < Top \<Longrightarrow> \<exists>z. x = Value z"
   141   by (cases x) (simp_all add: less_top_def)
   142 
   143 lemma less_top_Value_Top [simp]: "Value x < Top"
   144   by (simp add: less_top_def)
   145 
   146 lemma less_top_Value_Top_code [code]: "Value x < Top \<longleftrightarrow> True"
   147   by simp
   148 
   149 lemma less_top_Value [simp, code]: "Value x < Value y \<longleftrightarrow> x < y"
   150   by (simp add: less_top_def)
   151 
   152 instance proof
   153 qed (auto simp add: less_eq_top_def less_top_def less_le_not_le elim: order_trans split: top.splits)
   154 
   155 end 
   156 
   157 instance top :: (order) order proof
   158 qed (auto simp add: less_eq_top_def less_top_def split: top.splits)
   159 
   160 instance top :: (linorder) linorder proof
   161 qed (auto simp add: less_eq_top_def less_top_def split: top.splits)
   162 
   163 instantiation top :: (order) top
   164 begin
   165 
   166 definition "top = Top"
   167 
   168 instance ..
   169 
   170 end
   171 
   172 instantiation top :: (bot) bot
   173 begin
   174 
   175 definition "bot = Value bot"
   176 
   177 instance ..
   178 
   179 end
   180 
   181 instantiation top :: (semilattice_inf) semilattice_inf
   182 begin
   183 
   184 definition inf_top
   185 where
   186   "inf x y = (case x of Top => y | Value v => (case y of Top => x | Value v' => Value (inf v v')))"
   187 
   188 instance proof
   189 qed (auto simp add: inf_top_def less_eq_top_def split: top.splits)
   190 
   191 end
   192 
   193 instantiation top :: (semilattice_sup) semilattice_sup
   194 begin
   195 
   196 definition sup_top
   197 where
   198   "sup x y = (case x of Top => Top | Value v => (case y of Top => Top | Value v' => Value (sup v v')))"
   199 
   200 instance proof
   201 qed (auto simp add: sup_top_def less_eq_top_def split: top.splits)
   202 
   203 end
   204 
   205 instance top :: (lattice) bounded_lattice_top
   206 by(intro_classes)(simp add: top_top_def)
   207 
   208 subsection {* Values extended by a top and a bottom element *}
   209 
   210 datatype 'a flat_complete_lattice = Value 'a | Bot | Top
   211 
   212 instantiation flat_complete_lattice :: (type) order
   213 begin
   214 
   215 definition less_eq_flat_complete_lattice where
   216   "x \<le> y == (case x of Bot => True | Value v1 => (case y of Bot => False | Value v2 => (v1 = v2) | Top => True) | Top => (y = Top))"
   217 
   218 definition less_flat_complete_lattice where
   219   "x < y = (case x of Bot => \<not> (y = Bot) | Value v1 => (y = Top) | Top => False)"
   220 
   221 lemma [simp]: "Bot <= y"
   222 unfolding less_eq_flat_complete_lattice_def by auto
   223 
   224 lemma [simp]: "y <= Top"
   225 unfolding less_eq_flat_complete_lattice_def by (auto split: flat_complete_lattice.splits)
   226 
   227 lemma greater_than_two_values:
   228   assumes "a ~= aa" "Value a <= z" "Value aa <= z"
   229   shows "z = Top"
   230 using assms
   231 by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
   232 
   233 lemma lesser_than_two_values:
   234   assumes "a ~= aa" "z <= Value a" "z <= Value aa"
   235   shows "z = Bot"
   236 using assms
   237 by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
   238 
   239 instance proof
   240 qed (auto simp add: less_eq_flat_complete_lattice_def less_flat_complete_lattice_def split: flat_complete_lattice.splits)
   241 
   242 end
   243 
   244 instantiation flat_complete_lattice :: (type) bot
   245 begin
   246 
   247 definition "bot = Bot"
   248 
   249 instance ..
   250 
   251 end
   252 
   253 instantiation flat_complete_lattice :: (type) top
   254 begin
   255 
   256 definition "top = Top"
   257 
   258 instance ..
   259 
   260 end
   261 
   262 instantiation flat_complete_lattice :: (type) lattice
   263 begin
   264 
   265 definition inf_flat_complete_lattice
   266 where
   267   "inf x y = (case x of Bot => Bot | Value v1 => (case y of Bot => Bot | Value v2 => if (v1 = v2) then x else Bot | Top => x) | Top => y)"
   268 
   269 definition sup_flat_complete_lattice
   270 where
   271   "sup x y = (case x of Bot => y | Value v1 => (case y of Bot => x | Value v2 => if v1 = v2 then x else Top | Top => Top) | Top => Top)"
   272 
   273 instance proof
   274 qed (auto simp add: inf_flat_complete_lattice_def sup_flat_complete_lattice_def less_eq_flat_complete_lattice_def split: flat_complete_lattice.splits)
   275 
   276 end
   277 
   278 instantiation flat_complete_lattice :: (type) complete_lattice
   279 begin
   280 
   281 definition Sup_flat_complete_lattice
   282 where
   283   "Sup A = (if (A = {} \<or> A = {Bot}) then Bot else (if (\<exists> v. A - {Bot} = {Value v}) then Value (THE v. A - {Bot} = {Value v}) else Top))"
   284 
   285 definition Inf_flat_complete_lattice
   286 where
   287   "Inf A = (if (A = {} \<or> A = {Top}) then Top else (if (\<exists> v. A - {Top} = {Value v}) then Value (THE v. A - {Top} = {Value v}) else Bot))"
   288  
   289 instance
   290 proof
   291   fix x A
   292   assume "(x :: 'a flat_complete_lattice) : A"
   293   {
   294     fix v
   295     assume "A - {Top} = {Value v}"
   296     from this have "(THE v. A - {Top} = {Value v}) = v"
   297       by (auto intro!: the1_equality)
   298     moreover
   299     from `x : A` `A - {Top} = {Value v}` have "x = Top \<or> x = Value v"
   300       by auto
   301     ultimately have "Value (THE v. A - {Top} = {Value v}) <= x"
   302       by auto
   303   }
   304   from `x : A` this show "Inf A <= x"
   305     unfolding Inf_flat_complete_lattice_def
   306     by fastforce
   307 next
   308   fix z A
   309   assume z: "\<And>x. x : A ==> z <= (x :: 'a flat_complete_lattice)"
   310   {
   311     fix v
   312     assume "A - {Top} = {Value v}"
   313     moreover
   314     from this have "(THE v. A - {Top} = {Value v}) = v"
   315       by (auto intro!: the1_equality)
   316     moreover
   317     note z
   318     moreover
   319     ultimately have "z <= Value (THE v::'a. A - {Top} = {Value v})"
   320       by auto
   321   } moreover
   322   {
   323     assume not_one_value: "A ~= {}" "A ~= {Top}" "~ (EX v::'a. A - {Top} = {Value v})"
   324     have "z <= Bot"
   325     proof (cases "A - {Top} = {Bot}")
   326       case True
   327       from this z show ?thesis
   328         by auto
   329     next
   330       case False
   331       from not_one_value
   332       obtain a1 where a1: "a1 : A - {Top}" by auto
   333       from not_one_value False a1
   334       obtain a2 where "a2 : A - {Top} \<and> a1 \<noteq> a2"
   335         by (cases a1) auto
   336       from this a1 z[of "a1"] z[of "a2"] show ?thesis
   337         apply (cases a1)
   338         apply auto
   339         apply (cases a2)
   340         apply auto
   341         apply (auto dest!: lesser_than_two_values)
   342         done
   343     qed
   344   } moreover
   345   note z moreover
   346   ultimately show "z <= Inf A"
   347     unfolding Inf_flat_complete_lattice_def
   348     by auto
   349 next
   350   fix x A
   351   assume "(x :: 'a flat_complete_lattice) : A"
   352   {
   353     fix v
   354     assume "A - {Bot} = {Value v}"
   355     from this have "(THE v. A - {Bot} = {Value v}) = v"
   356       by (auto intro!: the1_equality)
   357     moreover
   358     from `x : A` `A - {Bot} = {Value v}` have "x = Bot \<or> x = Value v"
   359       by auto
   360     ultimately have "x <= Value (THE v. A - {Bot} = {Value v})"
   361       by auto
   362   }
   363   from `x : A` this show "x <= Sup A"
   364     unfolding Sup_flat_complete_lattice_def
   365     by fastforce
   366 next
   367   fix z A
   368   assume z: "\<And>x. x : A ==> x <= (z :: 'a flat_complete_lattice)"
   369   {
   370     fix v
   371     assume "A - {Bot} = {Value v}"
   372     moreover
   373     from this have "(THE v. A - {Bot} = {Value v}) = v"
   374       by (auto intro!: the1_equality)
   375     moreover
   376     note z
   377     moreover
   378     ultimately have "Value (THE v::'a. A - {Bot} = {Value v}) <= z"
   379       by auto
   380   } moreover
   381   {
   382     assume not_one_value: "A ~= {}" "A ~= {Bot}" "~ (EX v::'a. A - {Bot} = {Value v})"
   383     have "Top <= z"
   384     proof (cases "A - {Bot} = {Top}")
   385       case True
   386       from this z show ?thesis
   387         by auto
   388     next
   389       case False
   390       from not_one_value
   391       obtain a1 where a1: "a1 : A - {Bot}" by auto
   392       from not_one_value False a1
   393       obtain a2 where "a2 : A - {Bot} \<and> a1 \<noteq> a2"
   394         by (cases a1) auto
   395       from this a1 z[of "a1"] z[of "a2"] show ?thesis
   396         apply (cases a1)
   397         apply auto
   398         apply (cases a2)
   399         apply (auto dest!: greater_than_two_values)
   400         done
   401     qed
   402   } moreover
   403   note z moreover
   404   ultimately show "Sup A <= z"
   405     unfolding Sup_flat_complete_lattice_def
   406     by auto
   407 next
   408   show "Inf {} = (top :: 'a flat_complete_lattice)"
   409     by(simp add: Inf_flat_complete_lattice_def top_flat_complete_lattice_def)
   410 next
   411   show "Sup {} = (bot :: 'a flat_complete_lattice)"
   412     by(simp add: Sup_flat_complete_lattice_def bot_flat_complete_lattice_def)
   413 qed
   414 
   415 end
   416 
   417 end