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--
```     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`