rename Quickcheck_Types to Lattice_Constructions and remove quickcheck setup
authorAndreas Lochbihler
Tue Aug 19 15:19:16 2014 +0200 (2014-08-19)
changeset 579988b7508f848ef
parent 57997 4f93afabcdd2
child 57999 412ec967e3b3
rename Quickcheck_Types to Lattice_Constructions and remove quickcheck setup
src/HOL/Library/Lattice_Constructions.thy
src/HOL/Library/Library.thy
src/HOL/Library/Quickcheck_Types.thy
src/HOL/ROOT
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Lattice_Constructions.thy	Tue Aug 19 15:19:16 2014 +0200
     1.3 @@ -0,0 +1,417 @@
     1.4 +(*  Title:      HOL/Library/Lattice_Constructions.thy
     1.5 +    Author:     Lukas Bulwahn
     1.6 +    Copyright   2010 TU Muenchen
     1.7 +*)
     1.8 +
     1.9 +theory Lattice_Constructions
    1.10 +imports Main
    1.11 +begin
    1.12 +
    1.13 +subsection {* Values extended by a bottom element *}
    1.14 +
    1.15 +datatype 'a bot = Value 'a | Bot
    1.16 +
    1.17 +instantiation bot :: (preorder) preorder
    1.18 +begin
    1.19 +
    1.20 +definition less_eq_bot where
    1.21 +  "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))"
    1.22 +
    1.23 +definition less_bot where
    1.24 +  "x < y \<longleftrightarrow> (case y of Bot \<Rightarrow> False | Value y \<Rightarrow> (case x of Bot \<Rightarrow> True | Value x \<Rightarrow> x < y))"
    1.25 +
    1.26 +lemma less_eq_bot_Bot [simp]: "Bot \<le> x"
    1.27 +  by (simp add: less_eq_bot_def)
    1.28 +
    1.29 +lemma less_eq_bot_Bot_code [code]: "Bot \<le> x \<longleftrightarrow> True"
    1.30 +  by simp
    1.31 +
    1.32 +lemma less_eq_bot_Bot_is_Bot: "x \<le> Bot \<Longrightarrow> x = Bot"
    1.33 +  by (cases x) (simp_all add: less_eq_bot_def)
    1.34 +
    1.35 +lemma less_eq_bot_Value_Bot [simp, code]: "Value x \<le> Bot \<longleftrightarrow> False"
    1.36 +  by (simp add: less_eq_bot_def)
    1.37 +
    1.38 +lemma less_eq_bot_Value [simp, code]: "Value x \<le> Value y \<longleftrightarrow> x \<le> y"
    1.39 +  by (simp add: less_eq_bot_def)
    1.40 +
    1.41 +lemma less_bot_Bot [simp, code]: "x < Bot \<longleftrightarrow> False"
    1.42 +  by (simp add: less_bot_def)
    1.43 +
    1.44 +lemma less_bot_Bot_is_Value: "Bot < x \<Longrightarrow> \<exists>z. x = Value z"
    1.45 +  by (cases x) (simp_all add: less_bot_def)
    1.46 +
    1.47 +lemma less_bot_Bot_Value [simp]: "Bot < Value x"
    1.48 +  by (simp add: less_bot_def)
    1.49 +
    1.50 +lemma less_bot_Bot_Value_code [code]: "Bot < Value x \<longleftrightarrow> True"
    1.51 +  by simp
    1.52 +
    1.53 +lemma less_bot_Value [simp, code]: "Value x < Value y \<longleftrightarrow> x < y"
    1.54 +  by (simp add: less_bot_def)
    1.55 +
    1.56 +instance proof
    1.57 +qed (auto simp add: less_eq_bot_def less_bot_def less_le_not_le elim: order_trans split: bot.splits)
    1.58 +
    1.59 +end 
    1.60 +
    1.61 +instance bot :: (order) order proof
    1.62 +qed (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
    1.63 +
    1.64 +instance bot :: (linorder) linorder proof
    1.65 +qed (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
    1.66 +
    1.67 +instantiation bot :: (order) bot
    1.68 +begin
    1.69 +
    1.70 +definition "bot = Bot"
    1.71 +
    1.72 +instance ..
    1.73 +
    1.74 +end
    1.75 +
    1.76 +instantiation bot :: (top) top
    1.77 +begin
    1.78 +
    1.79 +definition "top = Value top"
    1.80 +
    1.81 +instance ..
    1.82 +
    1.83 +end
    1.84 +
    1.85 +instantiation bot :: (semilattice_inf) semilattice_inf
    1.86 +begin
    1.87 +
    1.88 +definition inf_bot
    1.89 +where
    1.90 +  "inf x y = (case x of Bot => Bot | Value v => (case y of Bot => Bot | Value v' => Value (inf v v')))"
    1.91 +
    1.92 +instance proof
    1.93 +qed (auto simp add: inf_bot_def less_eq_bot_def split: bot.splits)
    1.94 +
    1.95 +end
    1.96 +
    1.97 +instantiation bot :: (semilattice_sup) semilattice_sup
    1.98 +begin
    1.99 +
   1.100 +definition sup_bot
   1.101 +where
   1.102 +  "sup x y = (case x of Bot => y | Value v => (case y of Bot => x | Value v' => Value (sup v v')))"
   1.103 +
   1.104 +instance proof
   1.105 +qed (auto simp add: sup_bot_def less_eq_bot_def split: bot.splits)
   1.106 +
   1.107 +end
   1.108 +
   1.109 +instance bot :: (lattice) bounded_lattice_bot
   1.110 +by(intro_classes)(simp add: bot_bot_def)
   1.111 +
   1.112 +section {* Values extended by a top element *}
   1.113 +
   1.114 +datatype 'a top = Value 'a | Top
   1.115 +
   1.116 +instantiation top :: (preorder) preorder
   1.117 +begin
   1.118 +
   1.119 +definition less_eq_top where
   1.120 +  "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))"
   1.121 +
   1.122 +definition less_top where
   1.123 +  "x < y \<longleftrightarrow> (case x of Top \<Rightarrow> False | Value x \<Rightarrow> (case y of Top \<Rightarrow> True | Value y \<Rightarrow> x < y))"
   1.124 +
   1.125 +lemma less_eq_top_Top [simp]: "x <= Top"
   1.126 +  by (simp add: less_eq_top_def)
   1.127 +
   1.128 +lemma less_eq_top_Top_code [code]: "x \<le> Top \<longleftrightarrow> True"
   1.129 +  by simp
   1.130 +
   1.131 +lemma less_eq_top_is_Top: "Top \<le> x \<Longrightarrow> x = Top"
   1.132 +  by (cases x) (simp_all add: less_eq_top_def)
   1.133 +
   1.134 +lemma less_eq_top_Top_Value [simp, code]: "Top \<le> Value x \<longleftrightarrow> False"
   1.135 +  by (simp add: less_eq_top_def)
   1.136 +
   1.137 +lemma less_eq_top_Value_Value [simp, code]: "Value x \<le> Value y \<longleftrightarrow> x \<le> y"
   1.138 +  by (simp add: less_eq_top_def)
   1.139 +
   1.140 +lemma less_top_Top [simp, code]: "Top < x \<longleftrightarrow> False"
   1.141 +  by (simp add: less_top_def)
   1.142 +
   1.143 +lemma less_top_Top_is_Value: "x < Top \<Longrightarrow> \<exists>z. x = Value z"
   1.144 +  by (cases x) (simp_all add: less_top_def)
   1.145 +
   1.146 +lemma less_top_Value_Top [simp]: "Value x < Top"
   1.147 +  by (simp add: less_top_def)
   1.148 +
   1.149 +lemma less_top_Value_Top_code [code]: "Value x < Top \<longleftrightarrow> True"
   1.150 +  by simp
   1.151 +
   1.152 +lemma less_top_Value [simp, code]: "Value x < Value y \<longleftrightarrow> x < y"
   1.153 +  by (simp add: less_top_def)
   1.154 +
   1.155 +instance proof
   1.156 +qed (auto simp add: less_eq_top_def less_top_def less_le_not_le elim: order_trans split: top.splits)
   1.157 +
   1.158 +end 
   1.159 +
   1.160 +instance top :: (order) order proof
   1.161 +qed (auto simp add: less_eq_top_def less_top_def split: top.splits)
   1.162 +
   1.163 +instance top :: (linorder) linorder proof
   1.164 +qed (auto simp add: less_eq_top_def less_top_def split: top.splits)
   1.165 +
   1.166 +instantiation top :: (order) top
   1.167 +begin
   1.168 +
   1.169 +definition "top = Top"
   1.170 +
   1.171 +instance ..
   1.172 +
   1.173 +end
   1.174 +
   1.175 +instantiation top :: (bot) bot
   1.176 +begin
   1.177 +
   1.178 +definition "bot = Value bot"
   1.179 +
   1.180 +instance ..
   1.181 +
   1.182 +end
   1.183 +
   1.184 +instantiation top :: (semilattice_inf) semilattice_inf
   1.185 +begin
   1.186 +
   1.187 +definition inf_top
   1.188 +where
   1.189 +  "inf x y = (case x of Top => y | Value v => (case y of Top => x | Value v' => Value (inf v v')))"
   1.190 +
   1.191 +instance proof
   1.192 +qed (auto simp add: inf_top_def less_eq_top_def split: top.splits)
   1.193 +
   1.194 +end
   1.195 +
   1.196 +instantiation top :: (semilattice_sup) semilattice_sup
   1.197 +begin
   1.198 +
   1.199 +definition sup_top
   1.200 +where
   1.201 +  "sup x y = (case x of Top => Top | Value v => (case y of Top => Top | Value v' => Value (sup v v')))"
   1.202 +
   1.203 +instance proof
   1.204 +qed (auto simp add: sup_top_def less_eq_top_def split: top.splits)
   1.205 +
   1.206 +end
   1.207 +
   1.208 +instance top :: (lattice) bounded_lattice_top
   1.209 +by(intro_classes)(simp add: top_top_def)
   1.210 +
   1.211 +subsection {* Values extended by a top and a bottom element *}
   1.212 +
   1.213 +datatype 'a flat_complete_lattice = Value 'a | Bot | Top
   1.214 +
   1.215 +instantiation flat_complete_lattice :: (type) order
   1.216 +begin
   1.217 +
   1.218 +definition less_eq_flat_complete_lattice where
   1.219 +  "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.220 +
   1.221 +definition less_flat_complete_lattice where
   1.222 +  "x < y = (case x of Bot => \<not> (y = Bot) | Value v1 => (y = Top) | Top => False)"
   1.223 +
   1.224 +lemma [simp]: "Bot <= y"
   1.225 +unfolding less_eq_flat_complete_lattice_def by auto
   1.226 +
   1.227 +lemma [simp]: "y <= Top"
   1.228 +unfolding less_eq_flat_complete_lattice_def by (auto split: flat_complete_lattice.splits)
   1.229 +
   1.230 +lemma greater_than_two_values:
   1.231 +  assumes "a ~= aa" "Value a <= z" "Value aa <= z"
   1.232 +  shows "z = Top"
   1.233 +using assms
   1.234 +by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
   1.235 +
   1.236 +lemma lesser_than_two_values:
   1.237 +  assumes "a ~= aa" "z <= Value a" "z <= Value aa"
   1.238 +  shows "z = Bot"
   1.239 +using assms
   1.240 +by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
   1.241 +
   1.242 +instance proof
   1.243 +qed (auto simp add: less_eq_flat_complete_lattice_def less_flat_complete_lattice_def split: flat_complete_lattice.splits)
   1.244 +
   1.245 +end
   1.246 +
   1.247 +instantiation flat_complete_lattice :: (type) bot
   1.248 +begin
   1.249 +
   1.250 +definition "bot = Bot"
   1.251 +
   1.252 +instance ..
   1.253 +
   1.254 +end
   1.255 +
   1.256 +instantiation flat_complete_lattice :: (type) top
   1.257 +begin
   1.258 +
   1.259 +definition "top = Top"
   1.260 +
   1.261 +instance ..
   1.262 +
   1.263 +end
   1.264 +
   1.265 +instantiation flat_complete_lattice :: (type) lattice
   1.266 +begin
   1.267 +
   1.268 +definition inf_flat_complete_lattice
   1.269 +where
   1.270 +  "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.271 +
   1.272 +definition sup_flat_complete_lattice
   1.273 +where
   1.274 +  "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.275 +
   1.276 +instance proof
   1.277 +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.278 +
   1.279 +end
   1.280 +
   1.281 +instantiation flat_complete_lattice :: (type) complete_lattice
   1.282 +begin
   1.283 +
   1.284 +definition Sup_flat_complete_lattice
   1.285 +where
   1.286 +  "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.287 +
   1.288 +definition Inf_flat_complete_lattice
   1.289 +where
   1.290 +  "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.291 + 
   1.292 +instance
   1.293 +proof
   1.294 +  fix x A
   1.295 +  assume "(x :: 'a flat_complete_lattice) : A"
   1.296 +  {
   1.297 +    fix v
   1.298 +    assume "A - {Top} = {Value v}"
   1.299 +    from this have "(THE v. A - {Top} = {Value v}) = v"
   1.300 +      by (auto intro!: the1_equality)
   1.301 +    moreover
   1.302 +    from `x : A` `A - {Top} = {Value v}` have "x = Top \<or> x = Value v"
   1.303 +      by auto
   1.304 +    ultimately have "Value (THE v. A - {Top} = {Value v}) <= x"
   1.305 +      by auto
   1.306 +  }
   1.307 +  from `x : A` this show "Inf A <= x"
   1.308 +    unfolding Inf_flat_complete_lattice_def
   1.309 +    by fastforce
   1.310 +next
   1.311 +  fix z A
   1.312 +  assume z: "\<And>x. x : A ==> z <= (x :: 'a flat_complete_lattice)"
   1.313 +  {
   1.314 +    fix v
   1.315 +    assume "A - {Top} = {Value v}"
   1.316 +    moreover
   1.317 +    from this have "(THE v. A - {Top} = {Value v}) = v"
   1.318 +      by (auto intro!: the1_equality)
   1.319 +    moreover
   1.320 +    note z
   1.321 +    moreover
   1.322 +    ultimately have "z <= Value (THE v::'a. A - {Top} = {Value v})"
   1.323 +      by auto
   1.324 +  } moreover
   1.325 +  {
   1.326 +    assume not_one_value: "A ~= {}" "A ~= {Top}" "~ (EX v::'a. A - {Top} = {Value v})"
   1.327 +    have "z <= Bot"
   1.328 +    proof (cases "A - {Top} = {Bot}")
   1.329 +      case True
   1.330 +      from this z show ?thesis
   1.331 +        by auto
   1.332 +    next
   1.333 +      case False
   1.334 +      from not_one_value
   1.335 +      obtain a1 where a1: "a1 : A - {Top}" by auto
   1.336 +      from not_one_value False a1
   1.337 +      obtain a2 where "a2 : A - {Top} \<and> a1 \<noteq> a2"
   1.338 +        by (cases a1) auto
   1.339 +      from this a1 z[of "a1"] z[of "a2"] show ?thesis
   1.340 +        apply (cases a1)
   1.341 +        apply auto
   1.342 +        apply (cases a2)
   1.343 +        apply auto
   1.344 +        apply (auto dest!: lesser_than_two_values)
   1.345 +        done
   1.346 +    qed
   1.347 +  } moreover
   1.348 +  note z moreover
   1.349 +  ultimately show "z <= Inf A"
   1.350 +    unfolding Inf_flat_complete_lattice_def
   1.351 +    by auto
   1.352 +next
   1.353 +  fix x A
   1.354 +  assume "(x :: 'a flat_complete_lattice) : A"
   1.355 +  {
   1.356 +    fix v
   1.357 +    assume "A - {Bot} = {Value v}"
   1.358 +    from this have "(THE v. A - {Bot} = {Value v}) = v"
   1.359 +      by (auto intro!: the1_equality)
   1.360 +    moreover
   1.361 +    from `x : A` `A - {Bot} = {Value v}` have "x = Bot \<or> x = Value v"
   1.362 +      by auto
   1.363 +    ultimately have "x <= Value (THE v. A - {Bot} = {Value v})"
   1.364 +      by auto
   1.365 +  }
   1.366 +  from `x : A` this show "x <= Sup A"
   1.367 +    unfolding Sup_flat_complete_lattice_def
   1.368 +    by fastforce
   1.369 +next
   1.370 +  fix z A
   1.371 +  assume z: "\<And>x. x : A ==> x <= (z :: 'a flat_complete_lattice)"
   1.372 +  {
   1.373 +    fix v
   1.374 +    assume "A - {Bot} = {Value v}"
   1.375 +    moreover
   1.376 +    from this have "(THE v. A - {Bot} = {Value v}) = v"
   1.377 +      by (auto intro!: the1_equality)
   1.378 +    moreover
   1.379 +    note z
   1.380 +    moreover
   1.381 +    ultimately have "Value (THE v::'a. A - {Bot} = {Value v}) <= z"
   1.382 +      by auto
   1.383 +  } moreover
   1.384 +  {
   1.385 +    assume not_one_value: "A ~= {}" "A ~= {Bot}" "~ (EX v::'a. A - {Bot} = {Value v})"
   1.386 +    have "Top <= z"
   1.387 +    proof (cases "A - {Bot} = {Top}")
   1.388 +      case True
   1.389 +      from this z show ?thesis
   1.390 +        by auto
   1.391 +    next
   1.392 +      case False
   1.393 +      from not_one_value
   1.394 +      obtain a1 where a1: "a1 : A - {Bot}" by auto
   1.395 +      from not_one_value False a1
   1.396 +      obtain a2 where "a2 : A - {Bot} \<and> a1 \<noteq> a2"
   1.397 +        by (cases a1) auto
   1.398 +      from this a1 z[of "a1"] z[of "a2"] show ?thesis
   1.399 +        apply (cases a1)
   1.400 +        apply auto
   1.401 +        apply (cases a2)
   1.402 +        apply (auto dest!: greater_than_two_values)
   1.403 +        done
   1.404 +    qed
   1.405 +  } moreover
   1.406 +  note z moreover
   1.407 +  ultimately show "Sup A <= z"
   1.408 +    unfolding Sup_flat_complete_lattice_def
   1.409 +    by auto
   1.410 +next
   1.411 +  show "Inf {} = (top :: 'a flat_complete_lattice)"
   1.412 +    by(simp add: Inf_flat_complete_lattice_def top_flat_complete_lattice_def)
   1.413 +next
   1.414 +  show "Sup {} = (bot :: 'a flat_complete_lattice)"
   1.415 +    by(simp add: Sup_flat_complete_lattice_def bot_flat_complete_lattice_def)
   1.416 +qed
   1.417 +
   1.418 +end
   1.419 +
   1.420 +end
   1.421 \ No newline at end of file
     2.1 --- a/src/HOL/Library/Library.thy	Tue Aug 19 14:58:38 2014 +0200
     2.2 +++ b/src/HOL/Library/Library.thy	Tue Aug 19 15:19:16 2014 +0200
     2.3 @@ -32,6 +32,7 @@
     2.4    IArray
     2.5    Lattice_Algebras
     2.6    Lattice_Syntax
     2.7 +  Lattice_Constructions
     2.8    ListVector
     2.9    Lubs_Glbs
    2.10    Mapping
     3.1 --- a/src/HOL/Library/Quickcheck_Types.thy	Tue Aug 19 14:58:38 2014 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,430 +0,0 @@
     3.4 -(*  Title:      HOL/Library/Quickcheck_Types.thy
     3.5 -    Author:     Lukas Bulwahn
     3.6 -    Copyright   2010 TU Muenchen
     3.7 -*)
     3.8 -
     3.9 -theory Quickcheck_Types
    3.10 -imports Main
    3.11 -begin
    3.12 -
    3.13 -text {*
    3.14 -This theory provides some default types for the quickcheck execution.
    3.15 -In most cases, the default type @{typ "int"} meets the sort constraints
    3.16 -of the proposition.
    3.17 -But for the type classes bot and top, the type @{typ "int"} is insufficient.
    3.18 -Hence, we provide other types than @{typ "int"} as further default types.  
    3.19 -*}
    3.20 -
    3.21 -subsection {* Values extended by a bottom element *}
    3.22 -
    3.23 -datatype 'a bot = Value 'a | Bot
    3.24 -
    3.25 -instantiation bot :: (preorder) preorder
    3.26 -begin
    3.27 -
    3.28 -definition less_eq_bot where
    3.29 -  "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))"
    3.30 -
    3.31 -definition less_bot where
    3.32 -  "x < y \<longleftrightarrow> (case y of Bot \<Rightarrow> False | Value y \<Rightarrow> (case x of Bot \<Rightarrow> True | Value x \<Rightarrow> x < y))"
    3.33 -
    3.34 -lemma less_eq_bot_Bot [simp]: "Bot \<le> x"
    3.35 -  by (simp add: less_eq_bot_def)
    3.36 -
    3.37 -lemma less_eq_bot_Bot_code [code]: "Bot \<le> x \<longleftrightarrow> True"
    3.38 -  by simp
    3.39 -
    3.40 -lemma less_eq_bot_Bot_is_Bot: "x \<le> Bot \<Longrightarrow> x = Bot"
    3.41 -  by (cases x) (simp_all add: less_eq_bot_def)
    3.42 -
    3.43 -lemma less_eq_bot_Value_Bot [simp, code]: "Value x \<le> Bot \<longleftrightarrow> False"
    3.44 -  by (simp add: less_eq_bot_def)
    3.45 -
    3.46 -lemma less_eq_bot_Value [simp, code]: "Value x \<le> Value y \<longleftrightarrow> x \<le> y"
    3.47 -  by (simp add: less_eq_bot_def)
    3.48 -
    3.49 -lemma less_bot_Bot [simp, code]: "x < Bot \<longleftrightarrow> False"
    3.50 -  by (simp add: less_bot_def)
    3.51 -
    3.52 -lemma less_bot_Bot_is_Value: "Bot < x \<Longrightarrow> \<exists>z. x = Value z"
    3.53 -  by (cases x) (simp_all add: less_bot_def)
    3.54 -
    3.55 -lemma less_bot_Bot_Value [simp]: "Bot < Value x"
    3.56 -  by (simp add: less_bot_def)
    3.57 -
    3.58 -lemma less_bot_Bot_Value_code [code]: "Bot < Value x \<longleftrightarrow> True"
    3.59 -  by simp
    3.60 -
    3.61 -lemma less_bot_Value [simp, code]: "Value x < Value y \<longleftrightarrow> x < y"
    3.62 -  by (simp add: less_bot_def)
    3.63 -
    3.64 -instance proof
    3.65 -qed (auto simp add: less_eq_bot_def less_bot_def less_le_not_le elim: order_trans split: bot.splits)
    3.66 -
    3.67 -end 
    3.68 -
    3.69 -instance bot :: (order) order proof
    3.70 -qed (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
    3.71 -
    3.72 -instance bot :: (linorder) linorder proof
    3.73 -qed (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
    3.74 -
    3.75 -instantiation bot :: (order) bot
    3.76 -begin
    3.77 -
    3.78 -definition "bot = Bot"
    3.79 -
    3.80 -instance ..
    3.81 -
    3.82 -end
    3.83 -
    3.84 -instantiation bot :: (top) top
    3.85 -begin
    3.86 -
    3.87 -definition "top = Value top"
    3.88 -
    3.89 -instance ..
    3.90 -
    3.91 -end
    3.92 -
    3.93 -instantiation bot :: (semilattice_inf) semilattice_inf
    3.94 -begin
    3.95 -
    3.96 -definition inf_bot
    3.97 -where
    3.98 -  "inf x y = (case x of Bot => Bot | Value v => (case y of Bot => Bot | Value v' => Value (inf v v')))"
    3.99 -
   3.100 -instance proof
   3.101 -qed (auto simp add: inf_bot_def less_eq_bot_def split: bot.splits)
   3.102 -
   3.103 -end
   3.104 -
   3.105 -instantiation bot :: (semilattice_sup) semilattice_sup
   3.106 -begin
   3.107 -
   3.108 -definition sup_bot
   3.109 -where
   3.110 -  "sup x y = (case x of Bot => y | Value v => (case y of Bot => x | Value v' => Value (sup v v')))"
   3.111 -
   3.112 -instance proof
   3.113 -qed (auto simp add: sup_bot_def less_eq_bot_def split: bot.splits)
   3.114 -
   3.115 -end
   3.116 -
   3.117 -instance bot :: (lattice) bounded_lattice_bot
   3.118 -by(intro_classes)(simp add: bot_bot_def)
   3.119 -
   3.120 -section {* Values extended by a top element *}
   3.121 -
   3.122 -datatype 'a top = Value 'a | Top
   3.123 -
   3.124 -instantiation top :: (preorder) preorder
   3.125 -begin
   3.126 -
   3.127 -definition less_eq_top where
   3.128 -  "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))"
   3.129 -
   3.130 -definition less_top where
   3.131 -  "x < y \<longleftrightarrow> (case x of Top \<Rightarrow> False | Value x \<Rightarrow> (case y of Top \<Rightarrow> True | Value y \<Rightarrow> x < y))"
   3.132 -
   3.133 -lemma less_eq_top_Top [simp]: "x <= Top"
   3.134 -  by (simp add: less_eq_top_def)
   3.135 -
   3.136 -lemma less_eq_top_Top_code [code]: "x \<le> Top \<longleftrightarrow> True"
   3.137 -  by simp
   3.138 -
   3.139 -lemma less_eq_top_is_Top: "Top \<le> x \<Longrightarrow> x = Top"
   3.140 -  by (cases x) (simp_all add: less_eq_top_def)
   3.141 -
   3.142 -lemma less_eq_top_Top_Value [simp, code]: "Top \<le> Value x \<longleftrightarrow> False"
   3.143 -  by (simp add: less_eq_top_def)
   3.144 -
   3.145 -lemma less_eq_top_Value_Value [simp, code]: "Value x \<le> Value y \<longleftrightarrow> x \<le> y"
   3.146 -  by (simp add: less_eq_top_def)
   3.147 -
   3.148 -lemma less_top_Top [simp, code]: "Top < x \<longleftrightarrow> False"
   3.149 -  by (simp add: less_top_def)
   3.150 -
   3.151 -lemma less_top_Top_is_Value: "x < Top \<Longrightarrow> \<exists>z. x = Value z"
   3.152 -  by (cases x) (simp_all add: less_top_def)
   3.153 -
   3.154 -lemma less_top_Value_Top [simp]: "Value x < Top"
   3.155 -  by (simp add: less_top_def)
   3.156 -
   3.157 -lemma less_top_Value_Top_code [code]: "Value x < Top \<longleftrightarrow> True"
   3.158 -  by simp
   3.159 -
   3.160 -lemma less_top_Value [simp, code]: "Value x < Value y \<longleftrightarrow> x < y"
   3.161 -  by (simp add: less_top_def)
   3.162 -
   3.163 -instance proof
   3.164 -qed (auto simp add: less_eq_top_def less_top_def less_le_not_le elim: order_trans split: top.splits)
   3.165 -
   3.166 -end 
   3.167 -
   3.168 -instance top :: (order) order proof
   3.169 -qed (auto simp add: less_eq_top_def less_top_def split: top.splits)
   3.170 -
   3.171 -instance top :: (linorder) linorder proof
   3.172 -qed (auto simp add: less_eq_top_def less_top_def split: top.splits)
   3.173 -
   3.174 -instantiation top :: (order) top
   3.175 -begin
   3.176 -
   3.177 -definition "top = Top"
   3.178 -
   3.179 -instance ..
   3.180 -
   3.181 -end
   3.182 -
   3.183 -instantiation top :: (bot) bot
   3.184 -begin
   3.185 -
   3.186 -definition "bot = Value bot"
   3.187 -
   3.188 -instance ..
   3.189 -
   3.190 -end
   3.191 -
   3.192 -instantiation top :: (semilattice_inf) semilattice_inf
   3.193 -begin
   3.194 -
   3.195 -definition inf_top
   3.196 -where
   3.197 -  "inf x y = (case x of Top => y | Value v => (case y of Top => x | Value v' => Value (inf v v')))"
   3.198 -
   3.199 -instance proof
   3.200 -qed (auto simp add: inf_top_def less_eq_top_def split: top.splits)
   3.201 -
   3.202 -end
   3.203 -
   3.204 -instantiation top :: (semilattice_sup) semilattice_sup
   3.205 -begin
   3.206 -
   3.207 -definition sup_top
   3.208 -where
   3.209 -  "sup x y = (case x of Top => Top | Value v => (case y of Top => Top | Value v' => Value (sup v v')))"
   3.210 -
   3.211 -instance proof
   3.212 -qed (auto simp add: sup_top_def less_eq_top_def split: top.splits)
   3.213 -
   3.214 -end
   3.215 -
   3.216 -instance top :: (lattice) bounded_lattice_top
   3.217 -by(intro_classes)(simp add: top_top_def)
   3.218 -
   3.219 -
   3.220 -datatype 'a flat_complete_lattice = Value 'a | Bot | Top
   3.221 -
   3.222 -instantiation flat_complete_lattice :: (type) order
   3.223 -begin
   3.224 -
   3.225 -definition less_eq_flat_complete_lattice where
   3.226 -  "x \<le> y == (case x of Bot => True | Value v1 => (case y of Bot => False | Value v2 => (v1 = v2) | Top => True) | Top => (y = Top))"
   3.227 -
   3.228 -definition less_flat_complete_lattice where
   3.229 -  "x < y = (case x of Bot => \<not> (y = Bot) | Value v1 => (y = Top) | Top => False)"
   3.230 -
   3.231 -lemma [simp]: "Bot <= y"
   3.232 -unfolding less_eq_flat_complete_lattice_def by auto
   3.233 -
   3.234 -lemma [simp]: "y <= Top"
   3.235 -unfolding less_eq_flat_complete_lattice_def by (auto split: flat_complete_lattice.splits)
   3.236 -
   3.237 -lemma greater_than_two_values:
   3.238 -  assumes "a ~= aa" "Value a <= z" "Value aa <= z"
   3.239 -  shows "z = Top"
   3.240 -using assms
   3.241 -by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
   3.242 -
   3.243 -lemma lesser_than_two_values:
   3.244 -  assumes "a ~= aa" "z <= Value a" "z <= Value aa"
   3.245 -  shows "z = Bot"
   3.246 -using assms
   3.247 -by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
   3.248 -
   3.249 -instance proof
   3.250 -qed (auto simp add: less_eq_flat_complete_lattice_def less_flat_complete_lattice_def split: flat_complete_lattice.splits)
   3.251 -
   3.252 -end
   3.253 -
   3.254 -instantiation flat_complete_lattice :: (type) bot
   3.255 -begin
   3.256 -
   3.257 -definition "bot = Bot"
   3.258 -
   3.259 -instance ..
   3.260 -
   3.261 -end
   3.262 -
   3.263 -instantiation flat_complete_lattice :: (type) top
   3.264 -begin
   3.265 -
   3.266 -definition "top = Top"
   3.267 -
   3.268 -instance ..
   3.269 -
   3.270 -end
   3.271 -
   3.272 -instantiation flat_complete_lattice :: (type) lattice
   3.273 -begin
   3.274 -
   3.275 -definition inf_flat_complete_lattice
   3.276 -where
   3.277 -  "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)"
   3.278 -
   3.279 -definition sup_flat_complete_lattice
   3.280 -where
   3.281 -  "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)"
   3.282 -
   3.283 -instance proof
   3.284 -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)
   3.285 -
   3.286 -end
   3.287 -
   3.288 -instantiation flat_complete_lattice :: (type) complete_lattice
   3.289 -begin
   3.290 -
   3.291 -definition Sup_flat_complete_lattice
   3.292 -where
   3.293 -  "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))"
   3.294 -
   3.295 -definition Inf_flat_complete_lattice
   3.296 -where
   3.297 -  "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))"
   3.298 - 
   3.299 -instance
   3.300 -proof
   3.301 -  fix x A
   3.302 -  assume "(x :: 'a flat_complete_lattice) : A"
   3.303 -  {
   3.304 -    fix v
   3.305 -    assume "A - {Top} = {Value v}"
   3.306 -    from this have "(THE v. A - {Top} = {Value v}) = v"
   3.307 -      by (auto intro!: the1_equality)
   3.308 -    moreover
   3.309 -    from `x : A` `A - {Top} = {Value v}` have "x = Top \<or> x = Value v"
   3.310 -      by auto
   3.311 -    ultimately have "Value (THE v. A - {Top} = {Value v}) <= x"
   3.312 -      by auto
   3.313 -  }
   3.314 -  from `x : A` this show "Inf A <= x"
   3.315 -    unfolding Inf_flat_complete_lattice_def
   3.316 -    by fastforce
   3.317 -next
   3.318 -  fix z A
   3.319 -  assume z: "\<And>x. x : A ==> z <= (x :: 'a flat_complete_lattice)"
   3.320 -  {
   3.321 -    fix v
   3.322 -    assume "A - {Top} = {Value v}"
   3.323 -    moreover
   3.324 -    from this have "(THE v. A - {Top} = {Value v}) = v"
   3.325 -      by (auto intro!: the1_equality)
   3.326 -    moreover
   3.327 -    note z
   3.328 -    moreover
   3.329 -    ultimately have "z <= Value (THE v::'a. A - {Top} = {Value v})"
   3.330 -      by auto
   3.331 -  } moreover
   3.332 -  {
   3.333 -    assume not_one_value: "A ~= {}" "A ~= {Top}" "~ (EX v::'a. A - {Top} = {Value v})"
   3.334 -    have "z <= Bot"
   3.335 -    proof (cases "A - {Top} = {Bot}")
   3.336 -      case True
   3.337 -      from this z show ?thesis
   3.338 -        by auto
   3.339 -    next
   3.340 -      case False
   3.341 -      from not_one_value
   3.342 -      obtain a1 where a1: "a1 : A - {Top}" by auto
   3.343 -      from not_one_value False a1
   3.344 -      obtain a2 where "a2 : A - {Top} \<and> a1 \<noteq> a2"
   3.345 -        by (cases a1) auto
   3.346 -      from this a1 z[of "a1"] z[of "a2"] show ?thesis
   3.347 -        apply (cases a1)
   3.348 -        apply auto
   3.349 -        apply (cases a2)
   3.350 -        apply auto
   3.351 -        apply (auto dest!: lesser_than_two_values)
   3.352 -        done
   3.353 -    qed
   3.354 -  } moreover
   3.355 -  note z moreover
   3.356 -  ultimately show "z <= Inf A"
   3.357 -    unfolding Inf_flat_complete_lattice_def
   3.358 -    by auto
   3.359 -next
   3.360 -  fix x A
   3.361 -  assume "(x :: 'a flat_complete_lattice) : A"
   3.362 -  {
   3.363 -    fix v
   3.364 -    assume "A - {Bot} = {Value v}"
   3.365 -    from this have "(THE v. A - {Bot} = {Value v}) = v"
   3.366 -      by (auto intro!: the1_equality)
   3.367 -    moreover
   3.368 -    from `x : A` `A - {Bot} = {Value v}` have "x = Bot \<or> x = Value v"
   3.369 -      by auto
   3.370 -    ultimately have "x <= Value (THE v. A - {Bot} = {Value v})"
   3.371 -      by auto
   3.372 -  }
   3.373 -  from `x : A` this show "x <= Sup A"
   3.374 -    unfolding Sup_flat_complete_lattice_def
   3.375 -    by fastforce
   3.376 -next
   3.377 -  fix z A
   3.378 -  assume z: "\<And>x. x : A ==> x <= (z :: 'a flat_complete_lattice)"
   3.379 -  {
   3.380 -    fix v
   3.381 -    assume "A - {Bot} = {Value v}"
   3.382 -    moreover
   3.383 -    from this have "(THE v. A - {Bot} = {Value v}) = v"
   3.384 -      by (auto intro!: the1_equality)
   3.385 -    moreover
   3.386 -    note z
   3.387 -    moreover
   3.388 -    ultimately have "Value (THE v::'a. A - {Bot} = {Value v}) <= z"
   3.389 -      by auto
   3.390 -  } moreover
   3.391 -  {
   3.392 -    assume not_one_value: "A ~= {}" "A ~= {Bot}" "~ (EX v::'a. A - {Bot} = {Value v})"
   3.393 -    have "Top <= z"
   3.394 -    proof (cases "A - {Bot} = {Top}")
   3.395 -      case True
   3.396 -      from this z show ?thesis
   3.397 -        by auto
   3.398 -    next
   3.399 -      case False
   3.400 -      from not_one_value
   3.401 -      obtain a1 where a1: "a1 : A - {Bot}" by auto
   3.402 -      from not_one_value False a1
   3.403 -      obtain a2 where "a2 : A - {Bot} \<and> a1 \<noteq> a2"
   3.404 -        by (cases a1) auto
   3.405 -      from this a1 z[of "a1"] z[of "a2"] show ?thesis
   3.406 -        apply (cases a1)
   3.407 -        apply auto
   3.408 -        apply (cases a2)
   3.409 -        apply (auto dest!: greater_than_two_values)
   3.410 -        done
   3.411 -    qed
   3.412 -  } moreover
   3.413 -  note z moreover
   3.414 -  ultimately show "Sup A <= z"
   3.415 -    unfolding Sup_flat_complete_lattice_def
   3.416 -    by auto
   3.417 -next
   3.418 -  show "Inf {} = (top :: 'a flat_complete_lattice)"
   3.419 -    by(simp add: Inf_flat_complete_lattice_def top_flat_complete_lattice_def)
   3.420 -next
   3.421 -  show "Sup {} = (bot :: 'a flat_complete_lattice)"
   3.422 -    by(simp add: Sup_flat_complete_lattice_def bot_flat_complete_lattice_def)
   3.423 -qed
   3.424 -
   3.425 -end
   3.426 -
   3.427 -section {* Quickcheck configuration *}
   3.428 -
   3.429 -quickcheck_params[finite_types = false, default_type = ["int", "int bot", "int top", "Enum.finite_4 flat_complete_lattice"]]
   3.430 -
   3.431 -hide_type flat_complete_lattice bot top
   3.432 -
   3.433 -end
   3.434 \ No newline at end of file
     4.1 --- a/src/HOL/ROOT	Tue Aug 19 14:58:38 2014 +0200
     4.2 +++ b/src/HOL/ROOT	Tue Aug 19 15:19:16 2014 +0200
     4.3 @@ -38,7 +38,6 @@
     4.4      Product_Lexorder
     4.5      Product_Order
     4.6      Finite_Lattice
     4.7 -    Quickcheck_Types
     4.8      (*data refinements and dependent applications*)
     4.9      AList_Mapping
    4.10      Code_Binary_Nat