src/HOL/Library/Quickcheck_Types.thy
author Andreas Lochbihler
Fri Jul 11 15:35:11 2014 +0200 (2014-07-11)
changeset 57543 36041934e429
parent 44890 22f665a2e91c
child 57544 8840fa17e17c
permissions -rw-r--r--
adapt and reactivate Quickcheck_Types and add two test cases
     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 ..
   117 
   118 end
   119 
   120 instantiation bot :: (top) top
   121 begin
   122 
   123 definition "top = Value top"
   124 
   125 instance ..
   126 
   127 end
   128 
   129 instantiation bot :: (semilattice_inf) semilattice_inf
   130 begin
   131 
   132 definition inf_bot
   133 where
   134   "inf x y = (case x of Bot => Bot | Value v => (case y of Bot => Bot | Value v' => Value (inf v v')))"
   135 
   136 instance proof
   137 qed (auto simp add: inf_bot_def less_eq_bot_def split: bot.splits)
   138 
   139 end
   140 
   141 instantiation bot :: (semilattice_sup) semilattice_sup
   142 begin
   143 
   144 definition sup_bot
   145 where
   146   "sup x y = (case x of Bot => y | Value v => (case y of Bot => x | Value v' => Value (sup v v')))"
   147 
   148 instance proof
   149 qed (auto simp add: sup_bot_def less_eq_bot_def split: bot.splits)
   150 
   151 end
   152 
   153 instance bot :: (lattice) bounded_lattice_bot
   154 by(intro_classes)(simp add: bot_bot_def)
   155 
   156 section {* Values extended by a top element *}
   157 
   158 datatype 'a top = Value 'a | Top
   159 
   160 instantiation top :: (preorder) preorder
   161 begin
   162 
   163 definition less_eq_top where
   164   "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))"
   165 
   166 definition less_top where
   167   "x < y \<longleftrightarrow> (case x of Top \<Rightarrow> False | Value x \<Rightarrow> (case y of Top \<Rightarrow> True | Value y \<Rightarrow> x < y))"
   168 
   169 lemma less_eq_top_Top [simp]: "x <= Top"
   170   by (simp add: less_eq_top_def)
   171 
   172 lemma less_eq_top_Top_code [code]: "x \<le> Top \<longleftrightarrow> True"
   173   by simp
   174 
   175 lemma less_eq_top_is_Top: "Top \<le> x \<Longrightarrow> x = Top"
   176   by (cases x) (simp_all add: less_eq_top_def)
   177 
   178 lemma less_eq_top_Top_Value [simp, code]: "Top \<le> Value x \<longleftrightarrow> False"
   179   by (simp add: less_eq_top_def)
   180 
   181 lemma less_eq_top_Value_Value [simp, code]: "Value x \<le> Value y \<longleftrightarrow> x \<le> y"
   182   by (simp add: less_eq_top_def)
   183 
   184 lemma less_top_Top [simp, code]: "Top < x \<longleftrightarrow> False"
   185   by (simp add: less_top_def)
   186 
   187 lemma less_top_Top_is_Value: "x < Top \<Longrightarrow> \<exists>z. x = Value z"
   188   by (cases x) (simp_all add: less_top_def)
   189 
   190 lemma less_top_Value_Top [simp]: "Value x < Top"
   191   by (simp add: less_top_def)
   192 
   193 lemma less_top_Value_Top_code [code]: "Value x < Top \<longleftrightarrow> True"
   194   by simp
   195 
   196 lemma less_top_Value [simp, code]: "Value x < Value y \<longleftrightarrow> x < y"
   197   by (simp add: less_top_def)
   198 
   199 instance proof
   200 qed (auto simp add: less_eq_top_def less_top_def less_le_not_le elim: order_trans split: top.splits)
   201 
   202 end 
   203 
   204 instance top :: (order) order proof
   205 qed (auto simp add: less_eq_top_def less_top_def split: top.splits)
   206 
   207 instance top :: (linorder) linorder proof
   208 qed (auto simp add: less_eq_top_def less_top_def split: top.splits)
   209 
   210 instantiation top :: (order) top
   211 begin
   212 
   213 definition "top = Top"
   214 
   215 instance ..
   216 
   217 end
   218 
   219 instantiation top :: (bot) bot
   220 begin
   221 
   222 definition "bot = Value bot"
   223 
   224 instance ..
   225 
   226 end
   227 
   228 instantiation top :: (semilattice_inf) semilattice_inf
   229 begin
   230 
   231 definition inf_top
   232 where
   233   "inf x y = (case x of Top => y | Value v => (case y of Top => x | Value v' => Value (inf v v')))"
   234 
   235 instance proof
   236 qed (auto simp add: inf_top_def less_eq_top_def split: top.splits)
   237 
   238 end
   239 
   240 instantiation top :: (semilattice_sup) semilattice_sup
   241 begin
   242 
   243 definition sup_top
   244 where
   245   "sup x y = (case x of Top => Top | Value v => (case y of Top => Top | Value v' => Value (sup v v')))"
   246 
   247 instance proof
   248 qed (auto simp add: sup_top_def less_eq_top_def split: top.splits)
   249 
   250 end
   251 
   252 instance top :: (lattice) bounded_lattice_top
   253 by(intro_classes)(simp add: top_top_def)
   254 
   255 
   256 datatype 'a flat_complete_lattice = Value 'a | Bot | Top
   257 
   258 instantiation flat_complete_lattice :: (type) order
   259 begin
   260 
   261 definition less_eq_flat_complete_lattice where
   262   "x \<le> y == (case x of Bot => True | Value v1 => (case y of Bot => False | Value v2 => (v1 = v2) | Top => True) | Top => (y = Top))"
   263 
   264 definition less_flat_complete_lattice where
   265   "x < y = (case x of Bot => \<not> (y = Bot) | Value v1 => (y = Top) | Top => False)"
   266 
   267 lemma [simp]: "Bot <= y"
   268 unfolding less_eq_flat_complete_lattice_def by auto
   269 
   270 lemma [simp]: "y <= Top"
   271 unfolding less_eq_flat_complete_lattice_def by (auto split: flat_complete_lattice.splits)
   272 
   273 lemma greater_than_two_values:
   274   assumes "a ~= aa" "Value a <= z" "Value aa <= z"
   275   shows "z = Top"
   276 using assms
   277 by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
   278 
   279 lemma lesser_than_two_values:
   280   assumes "a ~= aa" "z <= Value a" "z <= Value aa"
   281   shows "z = Bot"
   282 using assms
   283 by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
   284 
   285 instance proof
   286 qed (auto simp add: less_eq_flat_complete_lattice_def less_flat_complete_lattice_def split: flat_complete_lattice.splits)
   287 
   288 end
   289 
   290 instantiation flat_complete_lattice :: (type) bot
   291 begin
   292 
   293 definition "bot = Bot"
   294 
   295 instance ..
   296 
   297 end
   298 
   299 instantiation flat_complete_lattice :: (type) top
   300 begin
   301 
   302 definition "top = Top"
   303 
   304 instance ..
   305 
   306 end
   307 
   308 instantiation flat_complete_lattice :: (type) lattice
   309 begin
   310 
   311 definition inf_flat_complete_lattice
   312 where
   313   "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)"
   314 
   315 definition sup_flat_complete_lattice
   316 where
   317   "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)"
   318 
   319 instance proof
   320 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)
   321 
   322 end
   323 
   324 instantiation flat_complete_lattice :: (type) complete_lattice
   325 begin
   326 
   327 definition Sup_flat_complete_lattice
   328 where
   329   "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))"
   330 
   331 definition Inf_flat_complete_lattice
   332 where
   333   "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))"
   334  
   335 instance
   336 proof
   337   fix x A
   338   assume "(x :: 'a flat_complete_lattice) : A"
   339   {
   340     fix v
   341     assume "A - {Top} = {Value v}"
   342     from this have "(THE v. A - {Top} = {Value v}) = v"
   343       by (auto intro!: the1_equality)
   344     moreover
   345     from `x : A` `A - {Top} = {Value v}` have "x = Top \<or> x = Value v"
   346       by auto
   347     ultimately have "Value (THE v. A - {Top} = {Value v}) <= x"
   348       by auto
   349   }
   350   from `x : A` this show "Inf A <= x"
   351     unfolding Inf_flat_complete_lattice_def
   352     by fastforce
   353 next
   354   fix z A
   355   assume z: "\<And>x. x : A ==> z <= (x :: 'a flat_complete_lattice)"
   356   {
   357     fix v
   358     assume "A - {Top} = {Value v}"
   359     moreover
   360     from this have "(THE v. A - {Top} = {Value v}) = v"
   361       by (auto intro!: the1_equality)
   362     moreover
   363     note z
   364     moreover
   365     ultimately have "z <= Value (THE v::'a. A - {Top} = {Value v})"
   366       by auto
   367   } moreover
   368   {
   369     assume not_one_value: "A ~= {}" "A ~= {Top}" "~ (EX v::'a. A - {Top} = {Value v})"
   370     have "z <= Bot"
   371     proof (cases "A - {Top} = {Bot}")
   372       case True
   373       from this z show ?thesis
   374         by auto
   375     next
   376       case False
   377       from not_one_value
   378       obtain a1 where a1: "a1 : A - {Top}" by auto
   379       from not_one_value False a1
   380       obtain a2 where "a2 : A - {Top} \<and> a1 \<noteq> a2"
   381         by (cases a1) auto
   382       from this a1 z[of "a1"] z[of "a2"] show ?thesis
   383         apply (cases a1)
   384         apply auto
   385         apply (cases a2)
   386         apply auto
   387         apply (auto dest!: lesser_than_two_values)
   388         done
   389     qed
   390   } moreover
   391   note z moreover
   392   ultimately show "z <= Inf A"
   393     unfolding Inf_flat_complete_lattice_def
   394     by auto
   395 next
   396   fix x A
   397   assume "(x :: 'a flat_complete_lattice) : A"
   398   {
   399     fix v
   400     assume "A - {Bot} = {Value v}"
   401     from this have "(THE v. A - {Bot} = {Value v}) = v"
   402       by (auto intro!: the1_equality)
   403     moreover
   404     from `x : A` `A - {Bot} = {Value v}` have "x = Bot \<or> x = Value v"
   405       by auto
   406     ultimately have "x <= Value (THE v. A - {Bot} = {Value v})"
   407       by auto
   408   }
   409   from `x : A` this show "x <= Sup A"
   410     unfolding Sup_flat_complete_lattice_def
   411     by fastforce
   412 next
   413   fix z A
   414   assume z: "\<And>x. x : A ==> x <= (z :: 'a flat_complete_lattice)"
   415   {
   416     fix v
   417     assume "A - {Bot} = {Value v}"
   418     moreover
   419     from this have "(THE v. A - {Bot} = {Value v}) = v"
   420       by (auto intro!: the1_equality)
   421     moreover
   422     note z
   423     moreover
   424     ultimately have "Value (THE v::'a. A - {Bot} = {Value v}) <= z"
   425       by auto
   426   } moreover
   427   {
   428     assume not_one_value: "A ~= {}" "A ~= {Bot}" "~ (EX v::'a. A - {Bot} = {Value v})"
   429     have "Top <= z"
   430     proof (cases "A - {Bot} = {Top}")
   431       case True
   432       from this z show ?thesis
   433         by auto
   434     next
   435       case False
   436       from not_one_value
   437       obtain a1 where a1: "a1 : A - {Bot}" by auto
   438       from not_one_value False a1
   439       obtain a2 where "a2 : A - {Bot} \<and> a1 \<noteq> a2"
   440         by (cases a1) auto
   441       from this a1 z[of "a1"] z[of "a2"] show ?thesis
   442         apply (cases a1)
   443         apply auto
   444         apply (cases a2)
   445         apply (auto dest!: greater_than_two_values)
   446         done
   447     qed
   448   } moreover
   449   note z moreover
   450   ultimately show "Sup A <= z"
   451     unfolding Sup_flat_complete_lattice_def
   452     by auto
   453 next
   454   show "Inf {} = (top :: 'a flat_complete_lattice)"
   455     by(simp add: Inf_flat_complete_lattice_def top_flat_complete_lattice_def)
   456 next
   457   show "Sup {} = (bot :: 'a flat_complete_lattice)"
   458     by(simp add: Sup_flat_complete_lattice_def bot_flat_complete_lattice_def)
   459 qed
   460 
   461 end
   462 
   463 section {* Quickcheck configuration *}
   464 
   465 quickcheck_params[finite_types = false, default_type = ["int", "non_distrib_lattice", "int bot", "int top", "Enum.finite_4 flat_complete_lattice"]]
   466 
   467 hide_type non_distrib_lattice flat_complete_lattice bot top
   468 
   469 lemma "\<lbrakk> inf x z = inf y z; sup x z = sup y z \<rbrakk> \<Longrightarrow> x = y" 
   470 quickcheck[exhaustive, expect=counterexample]
   471 oops
   472 
   473 lemma "Inf {} = bot"
   474 quickcheck[exhaustive, expect=counterexample]
   475 oops
   476 
   477 end