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