src/HOL/Library/Lattice_Constructions.thy
changeset 60508 2127bee2069a
parent 60500 903bb1495239
child 60509 0928cf63920f
     1.1 --- a/src/HOL/Library/Lattice_Constructions.thy	Wed Jun 17 18:58:46 2015 +0200
     1.2 +++ b/src/HOL/Library/Lattice_Constructions.thy	Wed Jun 17 20:05:21 2015 +0200
     1.3 @@ -50,33 +50,28 @@
     1.4  lemma less_bot_Value [simp, code]: "Value x < Value y \<longleftrightarrow> x < y"
     1.5    by (simp add: less_bot_def)
     1.6  
     1.7 -instance proof
     1.8 -qed (auto simp add: less_eq_bot_def less_bot_def less_le_not_le elim: order_trans split: bot.splits)
     1.9 +instance
    1.10 +  by default
    1.11 +    (auto simp add: less_eq_bot_def less_bot_def less_le_not_le elim: order_trans split: bot.splits)
    1.12  
    1.13 -end 
    1.14 +end
    1.15  
    1.16 -instance bot :: (order) order proof
    1.17 -qed (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
    1.18 +instance bot :: (order) order
    1.19 +  by default (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
    1.20  
    1.21 -instance bot :: (linorder) linorder proof
    1.22 -qed (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
    1.23 +instance bot :: (linorder) linorder
    1.24 +  by default (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
    1.25  
    1.26  instantiation bot :: (order) bot
    1.27  begin
    1.28 -
    1.29 -definition "bot = Bot"
    1.30 -
    1.31 -instance ..
    1.32 -
    1.33 +  definition "bot = Bot"
    1.34 +  instance ..
    1.35  end
    1.36  
    1.37  instantiation bot :: (top) top
    1.38  begin
    1.39 -
    1.40 -definition "top = Value top"
    1.41 -
    1.42 -instance ..
    1.43 -
    1.44 +  definition "top = Value top"
    1.45 +  instance ..
    1.46  end
    1.47  
    1.48  instantiation bot :: (semilattice_inf) semilattice_inf
    1.49 @@ -84,10 +79,16 @@
    1.50  
    1.51  definition inf_bot
    1.52  where
    1.53 -  "inf x y = (case x of Bot => Bot | Value v => (case y of Bot => Bot | Value v' => Value (inf v v')))"
    1.54 +  "inf x y =
    1.55 +    (case x of
    1.56 +      Bot \<Rightarrow> Bot
    1.57 +    | Value v \<Rightarrow>
    1.58 +        (case y of
    1.59 +          Bot \<Rightarrow> Bot
    1.60 +        | Value v' \<Rightarrow> Value (inf v v')))"
    1.61  
    1.62 -instance proof
    1.63 -qed (auto simp add: inf_bot_def less_eq_bot_def split: bot.splits)
    1.64 +instance
    1.65 +  by default (auto simp add: inf_bot_def less_eq_bot_def split: bot.splits)
    1.66  
    1.67  end
    1.68  
    1.69 @@ -96,17 +97,24 @@
    1.70  
    1.71  definition sup_bot
    1.72  where
    1.73 -  "sup x y = (case x of Bot => y | Value v => (case y of Bot => x | Value v' => Value (sup v v')))"
    1.74 +  "sup x y =
    1.75 +    (case x of
    1.76 +      Bot \<Rightarrow> y
    1.77 +    | Value v \<Rightarrow>
    1.78 +        (case y of
    1.79 +          Bot \<Rightarrow> x
    1.80 +        | Value v' \<Rightarrow> Value (sup v v')))"
    1.81  
    1.82 -instance proof
    1.83 -qed (auto simp add: sup_bot_def less_eq_bot_def split: bot.splits)
    1.84 +instance
    1.85 +  by default (auto simp add: sup_bot_def less_eq_bot_def split: bot.splits)
    1.86  
    1.87  end
    1.88  
    1.89  instance bot :: (lattice) bounded_lattice_bot
    1.90 -by(intro_classes)(simp add: bot_bot_def)
    1.91 +  by intro_classes (simp add: bot_bot_def)
    1.92  
    1.93 -section \<open>Values extended by a top element\<close>
    1.94 +
    1.95 +subsection \<open>Values extended by a top element\<close>
    1.96  
    1.97  datatype 'a top = Value 'a | Top
    1.98  
    1.99 @@ -119,7 +127,7 @@
   1.100  definition less_top where
   1.101    "x < y \<longleftrightarrow> (case x of Top \<Rightarrow> False | Value x \<Rightarrow> (case y of Top \<Rightarrow> True | Value y \<Rightarrow> x < y))"
   1.102  
   1.103 -lemma less_eq_top_Top [simp]: "x <= Top"
   1.104 +lemma less_eq_top_Top [simp]: "x \<le> Top"
   1.105    by (simp add: less_eq_top_def)
   1.106  
   1.107  lemma less_eq_top_Top_code [code]: "x \<le> Top \<longleftrightarrow> True"
   1.108 @@ -149,33 +157,28 @@
   1.109  lemma less_top_Value [simp, code]: "Value x < Value y \<longleftrightarrow> x < y"
   1.110    by (simp add: less_top_def)
   1.111  
   1.112 -instance proof
   1.113 -qed (auto simp add: less_eq_top_def less_top_def less_le_not_le elim: order_trans split: top.splits)
   1.114 +instance
   1.115 +  by default
   1.116 +    (auto simp add: less_eq_top_def less_top_def less_le_not_le elim: order_trans split: top.splits)
   1.117  
   1.118 -end 
   1.119 +end
   1.120  
   1.121 -instance top :: (order) order proof
   1.122 -qed (auto simp add: less_eq_top_def less_top_def split: top.splits)
   1.123 +instance top :: (order) order
   1.124 +  by default (auto simp add: less_eq_top_def less_top_def split: top.splits)
   1.125  
   1.126 -instance top :: (linorder) linorder proof
   1.127 -qed (auto simp add: less_eq_top_def less_top_def split: top.splits)
   1.128 +instance top :: (linorder) linorder
   1.129 +  by default (auto simp add: less_eq_top_def less_top_def split: top.splits)
   1.130  
   1.131  instantiation top :: (order) top
   1.132  begin
   1.133 -
   1.134 -definition "top = Top"
   1.135 -
   1.136 -instance ..
   1.137 -
   1.138 +  definition "top = Top"
   1.139 +  instance ..
   1.140  end
   1.141  
   1.142  instantiation top :: (bot) bot
   1.143  begin
   1.144 -
   1.145 -definition "bot = Value bot"
   1.146 -
   1.147 -instance ..
   1.148 -
   1.149 +  definition "bot = Value bot"
   1.150 +  instance ..
   1.151  end
   1.152  
   1.153  instantiation top :: (semilattice_inf) semilattice_inf
   1.154 @@ -183,10 +186,16 @@
   1.155  
   1.156  definition inf_top
   1.157  where
   1.158 -  "inf x y = (case x of Top => y | Value v => (case y of Top => x | Value v' => Value (inf v v')))"
   1.159 +  "inf x y =
   1.160 +    (case x of
   1.161 +      Top \<Rightarrow> y
   1.162 +    | Value v \<Rightarrow>
   1.163 +        (case y of
   1.164 +          Top \<Rightarrow> x
   1.165 +        | Value v' \<Rightarrow> Value (inf v v')))"
   1.166  
   1.167 -instance proof
   1.168 -qed (auto simp add: inf_top_def less_eq_top_def split: top.splits)
   1.169 +instance
   1.170 +  by default (auto simp add: inf_top_def less_eq_top_def split: top.splits)
   1.171  
   1.172  end
   1.173  
   1.174 @@ -195,15 +204,22 @@
   1.175  
   1.176  definition sup_top
   1.177  where
   1.178 -  "sup x y = (case x of Top => Top | Value v => (case y of Top => Top | Value v' => Value (sup v v')))"
   1.179 +  "sup x y =
   1.180 +    (case x of
   1.181 +      Top \<Rightarrow> Top
   1.182 +    | Value v \<Rightarrow>
   1.183 +        (case y of
   1.184 +          Top \<Rightarrow> Top
   1.185 +        | Value v' \<Rightarrow> Value (sup v v')))"
   1.186  
   1.187 -instance proof
   1.188 -qed (auto simp add: sup_top_def less_eq_top_def split: top.splits)
   1.189 +instance
   1.190 +  by default (auto simp add: sup_top_def less_eq_top_def split: top.splits)
   1.191  
   1.192  end
   1.193  
   1.194  instance top :: (lattice) bounded_lattice_top
   1.195 -by(intro_classes)(simp add: top_top_def)
   1.196 +  by default (simp add: top_top_def)
   1.197 +
   1.198  
   1.199  subsection \<open>Values extended by a top and a bottom element\<close>
   1.200  
   1.201 @@ -212,51 +228,61 @@
   1.202  instantiation flat_complete_lattice :: (type) order
   1.203  begin
   1.204  
   1.205 -definition less_eq_flat_complete_lattice where
   1.206 -  "x \<le> y == (case x of Bot => True | Value v1 => (case y of Bot => False | Value v2 => (v1 = v2) | Top => True) | Top => (y = Top))"
   1.207 -
   1.208 -definition less_flat_complete_lattice where
   1.209 -  "x < y = (case x of Bot => \<not> (y = Bot) | Value v1 => (y = Top) | Top => False)"
   1.210 +definition less_eq_flat_complete_lattice
   1.211 +where
   1.212 +  "x \<le> y \<equiv>
   1.213 +    (case x of
   1.214 +      Bot \<Rightarrow> True
   1.215 +    | Value v1 \<Rightarrow>
   1.216 +        (case y of
   1.217 +          Bot \<Rightarrow> False
   1.218 +        | Value v2 \<Rightarrow> v1 = v2
   1.219 +        | Top \<Rightarrow> True)
   1.220 +    | Top \<Rightarrow> y = Top)"
   1.221  
   1.222 -lemma [simp]: "Bot <= y"
   1.223 -unfolding less_eq_flat_complete_lattice_def by auto
   1.224 +definition less_flat_complete_lattice
   1.225 +where
   1.226 +  "x < y =
   1.227 +    (case x of
   1.228 +      Bot \<Rightarrow> y \<noteq> Bot
   1.229 +    | Value v1 \<Rightarrow> y = Top
   1.230 +    | Top \<Rightarrow> False)"
   1.231  
   1.232 -lemma [simp]: "y <= Top"
   1.233 -unfolding less_eq_flat_complete_lattice_def by (auto split: flat_complete_lattice.splits)
   1.234 +lemma [simp]: "Bot \<le> y"
   1.235 +  unfolding less_eq_flat_complete_lattice_def by auto
   1.236 +
   1.237 +lemma [simp]: "y \<le> Top"
   1.238 +  unfolding less_eq_flat_complete_lattice_def by (auto split: flat_complete_lattice.splits)
   1.239  
   1.240  lemma greater_than_two_values:
   1.241 -  assumes "a ~= aa" "Value a <= z" "Value aa <= z"
   1.242 +  assumes "a \<noteq> aa" "Value a \<le> z" "Value aa \<le> z"
   1.243    shows "z = Top"
   1.244 -using assms
   1.245 -by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
   1.246 +  using assms
   1.247 +  by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
   1.248  
   1.249  lemma lesser_than_two_values:
   1.250 -  assumes "a ~= aa" "z <= Value a" "z <= Value aa"
   1.251 +  assumes "a \<noteq> aa" "z \<le> Value a" "z \<le> Value aa"
   1.252    shows "z = Bot"
   1.253 -using assms
   1.254 -by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
   1.255 +  using assms
   1.256 +  by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
   1.257  
   1.258 -instance proof
   1.259 -qed (auto simp add: less_eq_flat_complete_lattice_def less_flat_complete_lattice_def split: flat_complete_lattice.splits)
   1.260 +instance
   1.261 +  by default
   1.262 +    (auto simp add: less_eq_flat_complete_lattice_def less_flat_complete_lattice_def
   1.263 +      split: flat_complete_lattice.splits)
   1.264  
   1.265  end
   1.266  
   1.267  instantiation flat_complete_lattice :: (type) bot
   1.268  begin
   1.269 -
   1.270 -definition "bot = Bot"
   1.271 -
   1.272 -instance ..
   1.273 -
   1.274 +  definition "bot = Bot"
   1.275 +  instance ..
   1.276  end
   1.277  
   1.278  instantiation flat_complete_lattice :: (type) top
   1.279  begin
   1.280 -
   1.281 -definition "top = Top"
   1.282 -
   1.283 -instance ..
   1.284 -
   1.285 +  definition "top = Top"
   1.286 +  instance ..
   1.287  end
   1.288  
   1.289  instantiation flat_complete_lattice :: (type) lattice
   1.290 @@ -264,14 +290,32 @@
   1.291  
   1.292  definition inf_flat_complete_lattice
   1.293  where
   1.294 -  "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)"
   1.295 +  "inf x y =
   1.296 +    (case x of
   1.297 +      Bot \<Rightarrow> Bot
   1.298 +    | Value v1 \<Rightarrow>
   1.299 +        (case y of
   1.300 +          Bot \<Rightarrow> Bot
   1.301 +        | Value v2 \<Rightarrow> if v1 = v2 then x else Bot
   1.302 +        | Top \<Rightarrow> x)
   1.303 +    | Top \<Rightarrow> y)"
   1.304  
   1.305  definition sup_flat_complete_lattice
   1.306  where
   1.307 -  "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)"
   1.308 +  "sup x y =
   1.309 +    (case x of
   1.310 +      Bot \<Rightarrow> y
   1.311 +    | Value v1 \<Rightarrow>
   1.312 +        (case y of
   1.313 +          Bot \<Rightarrow> x
   1.314 +        | Value v2 \<Rightarrow> if v1 = v2 then x else Top
   1.315 +        | Top \<Rightarrow> Top)
   1.316 +    | Top \<Rightarrow> Top)"
   1.317  
   1.318 -instance proof
   1.319 -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)
   1.320 +instance
   1.321 +  by default
   1.322 +    (auto simp add: inf_flat_complete_lattice_def sup_flat_complete_lattice_def
   1.323 +      less_eq_flat_complete_lattice_def split: flat_complete_lattice.splits)
   1.324  
   1.325  end
   1.326  
   1.327 @@ -280,60 +324,65 @@
   1.328  
   1.329  definition Sup_flat_complete_lattice
   1.330  where
   1.331 -  "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))"
   1.332 +  "Sup A =
   1.333 +    (if A = {} \<or> A = {Bot} then Bot
   1.334 +     else if \<exists>v. A - {Bot} = {Value v} then Value (THE v. A - {Bot} = {Value v})
   1.335 +     else Top)"
   1.336  
   1.337  definition Inf_flat_complete_lattice
   1.338  where
   1.339 -  "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))"
   1.340 - 
   1.341 +  "Inf A =
   1.342 +    (if A = {} \<or> A = {Top} then Top
   1.343 +     else if \<exists>v. A - {Top} = {Value v} then Value (THE v. A - {Top} = {Value v})
   1.344 +     else Bot)"
   1.345 +
   1.346  instance
   1.347  proof
   1.348 -  fix x A
   1.349 -  assume "(x :: 'a flat_complete_lattice) : A"
   1.350 +  fix x :: "'a flat_complete_lattice"
   1.351 +  fix A
   1.352 +  assume "x \<in> A"
   1.353    {
   1.354      fix v
   1.355      assume "A - {Top} = {Value v}"
   1.356 -    from this have "(THE v. A - {Top} = {Value v}) = v"
   1.357 +    then have "(THE v. A - {Top} = {Value v}) = v"
   1.358        by (auto intro!: the1_equality)
   1.359      moreover
   1.360 -    from \<open>x : A\<close> \<open>A - {Top} = {Value v}\<close> have "x = Top \<or> x = Value v"
   1.361 +    from \<open>x \<in> A\<close> \<open>A - {Top} = {Value v}\<close> have "x = Top \<or> x = Value v"
   1.362        by auto
   1.363 -    ultimately have "Value (THE v. A - {Top} = {Value v}) <= x"
   1.364 +    ultimately have "Value (THE v. A - {Top} = {Value v}) \<le> x"
   1.365        by auto
   1.366    }
   1.367 -  from \<open>x : A\<close> this show "Inf A <= x"
   1.368 +  with \<open>x \<in> A\<close> show "Inf A \<le> x"
   1.369      unfolding Inf_flat_complete_lattice_def
   1.370      by fastforce
   1.371  next
   1.372 -  fix z A
   1.373 -  assume z: "\<And>x. x : A ==> z <= (x :: 'a flat_complete_lattice)"
   1.374 +  fix z :: "'a flat_complete_lattice"
   1.375 +  fix A
   1.376 +  assume z: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
   1.377    {
   1.378      fix v
   1.379 -    assume "A - {Top} = {Value v}"
   1.380 -    moreover
   1.381 -    from this have "(THE v. A - {Top} = {Value v}) = v"
   1.382 +    assume *: "A - {Top} = {Value v}"
   1.383 +    then have "(THE v. A - {Top} = {Value v}) = v"
   1.384        by (auto intro!: the1_equality)
   1.385 -    moreover
   1.386 -    note z
   1.387 -    moreover
   1.388 -    ultimately have "z <= Value (THE v::'a. A - {Top} = {Value v})"
   1.389 -      by auto
   1.390 -  } moreover
   1.391 +    with * have "z \<le> Value (THE v::'a. A - {Top} = {Value v})"
   1.392 +      using z by auto
   1.393 +  }
   1.394 +  moreover
   1.395    {
   1.396 -    assume not_one_value: "A ~= {}" "A ~= {Top}" "~ (EX v::'a. A - {Top} = {Value v})"
   1.397 -    have "z <= Bot"
   1.398 +    assume not_one_value: "A \<noteq> {}" "A \<noteq> {Top}" "\<not> (\<exists>v::'a. A - {Top} = {Value v})"
   1.399 +    have "z \<le> Bot"
   1.400      proof (cases "A - {Top} = {Bot}")
   1.401        case True
   1.402 -      from this z show ?thesis
   1.403 +      with z show ?thesis
   1.404          by auto
   1.405      next
   1.406        case False
   1.407        from not_one_value
   1.408 -      obtain a1 where a1: "a1 : A - {Top}" by auto
   1.409 +      obtain a1 where a1: "a1 \<in> A - {Top}" by auto
   1.410        from not_one_value False a1
   1.411 -      obtain a2 where "a2 : A - {Top} \<and> a1 \<noteq> a2"
   1.412 +      obtain a2 where "a2 \<in> A - {Top} \<and> a1 \<noteq> a2"
   1.413          by (cases a1) auto
   1.414 -      from this a1 z[of "a1"] z[of "a2"] show ?thesis
   1.415 +      with a1 z[of "a1"] z[of "a2"] show ?thesis
   1.416          apply (cases a1)
   1.417          apply auto
   1.418          apply (cases a2)
   1.419 @@ -341,75 +390,69 @@
   1.420          apply (auto dest!: lesser_than_two_values)
   1.421          done
   1.422      qed
   1.423 -  } moreover
   1.424 -  note z moreover
   1.425 -  ultimately show "z <= Inf A"
   1.426 -    unfolding Inf_flat_complete_lattice_def
   1.427 -    by auto
   1.428 +  }
   1.429 +  ultimately show "z \<le> Inf A"
   1.430 +    using z unfolding Inf_flat_complete_lattice_def by auto  -- slow
   1.431  next
   1.432 -  fix x A
   1.433 -  assume "(x :: 'a flat_complete_lattice) : A"
   1.434 +  fix x :: "'a flat_complete_lattice"
   1.435 +  fix A
   1.436 +  assume "x \<in> A"
   1.437    {
   1.438      fix v
   1.439      assume "A - {Bot} = {Value v}"
   1.440 -    from this have "(THE v. A - {Bot} = {Value v}) = v"
   1.441 +    then have "(THE v. A - {Bot} = {Value v}) = v"
   1.442        by (auto intro!: the1_equality)
   1.443      moreover
   1.444 -    from \<open>x : A\<close> \<open>A - {Bot} = {Value v}\<close> have "x = Bot \<or> x = Value v"
   1.445 +    from \<open>x \<in> A\<close> \<open>A - {Bot} = {Value v}\<close> have "x = Bot \<or> x = Value v"
   1.446        by auto
   1.447 -    ultimately have "x <= Value (THE v. A - {Bot} = {Value v})"
   1.448 +    ultimately have "x \<le> Value (THE v. A - {Bot} = {Value v})"
   1.449        by auto
   1.450    }
   1.451 -  from \<open>x : A\<close> this show "x <= Sup A"
   1.452 +  with \<open>x \<in> A\<close> show "x \<le> Sup A"
   1.453      unfolding Sup_flat_complete_lattice_def
   1.454      by fastforce
   1.455  next
   1.456 -  fix z A
   1.457 -  assume z: "\<And>x. x : A ==> x <= (z :: 'a flat_complete_lattice)"
   1.458 +  fix z :: "'a flat_complete_lattice"
   1.459 +  fix A
   1.460 +  assume z: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
   1.461    {
   1.462      fix v
   1.463      assume "A - {Bot} = {Value v}"
   1.464      moreover
   1.465 -    from this have "(THE v. A - {Bot} = {Value v}) = v"
   1.466 +    then have "(THE v. A - {Bot} = {Value v}) = v"
   1.467        by (auto intro!: the1_equality)
   1.468 -    moreover
   1.469 -    note z
   1.470 -    moreover
   1.471 -    ultimately have "Value (THE v::'a. A - {Bot} = {Value v}) <= z"
   1.472 -      by auto
   1.473 -  } moreover
   1.474 +    ultimately have "Value (THE v::'a. A - {Bot} = {Value v}) \<le> z"
   1.475 +      using z by auto
   1.476 +  }
   1.477 +  moreover
   1.478    {
   1.479 -    assume not_one_value: "A ~= {}" "A ~= {Bot}" "~ (EX v::'a. A - {Bot} = {Value v})"
   1.480 -    have "Top <= z"
   1.481 +    assume not_one_value: "A \<noteq> {}" "A \<noteq> {Bot}" "\<not> (\<exists>v::'a. A - {Bot} = {Value v})"
   1.482 +    have "Top \<le> z"
   1.483      proof (cases "A - {Bot} = {Top}")
   1.484        case True
   1.485 -      from this z show ?thesis
   1.486 +      with z show ?thesis
   1.487          by auto
   1.488      next
   1.489        case False
   1.490 -      from not_one_value
   1.491 -      obtain a1 where a1: "a1 : A - {Bot}" by auto
   1.492 -      from not_one_value False a1
   1.493 -      obtain a2 where "a2 : A - {Bot} \<and> a1 \<noteq> a2"
   1.494 +      from not_one_value obtain a1 where a1: "a1 \<in> A - {Bot}"
   1.495 +        by auto
   1.496 +      from not_one_value False a1 obtain a2 where "a2 \<in> A - {Bot} \<and> a1 \<noteq> a2"
   1.497          by (cases a1) auto
   1.498 -      from this a1 z[of "a1"] z[of "a2"] show ?thesis
   1.499 +      with a1 z[of "a1"] z[of "a2"] show ?thesis
   1.500          apply (cases a1)
   1.501          apply auto
   1.502          apply (cases a2)
   1.503          apply (auto dest!: greater_than_two_values)
   1.504          done
   1.505      qed
   1.506 -  } moreover
   1.507 -  note z moreover
   1.508 -  ultimately show "Sup A <= z"
   1.509 -    unfolding Sup_flat_complete_lattice_def
   1.510 -    by auto
   1.511 +  }
   1.512 +  ultimately show "Sup A \<le> z"
   1.513 +    using z unfolding Sup_flat_complete_lattice_def by auto  -- slow
   1.514  next
   1.515    show "Inf {} = (top :: 'a flat_complete_lattice)"
   1.516 -    by(simp add: Inf_flat_complete_lattice_def top_flat_complete_lattice_def)
   1.517 -next
   1.518 +    by (simp add: Inf_flat_complete_lattice_def top_flat_complete_lattice_def)
   1.519    show "Sup {} = (bot :: 'a flat_complete_lattice)"
   1.520 -    by(simp add: Sup_flat_complete_lattice_def bot_flat_complete_lattice_def)
   1.521 +    by (simp add: Sup_flat_complete_lattice_def bot_flat_complete_lattice_def)
   1.522  qed
   1.523  
   1.524  end