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