author | bulwahn |
Wed, 21 Jul 2010 18:11:51 +0200 | |
changeset 37915 | e709e764f20c |
child 37918 | eda5faaca9e2 |
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 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
55 |
subsection {* Values extended by a bottom element *} |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
56 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
57 |
datatype 'a bot = Value 'a | Bot |
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 |
instantiation bot :: (preorder) preorder |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
60 |
begin |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
61 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
62 |
definition less_eq_bot where |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
63 |
"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
|
64 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
65 |
definition less_bot where |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
66 |
"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
|
67 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
68 |
lemma less_eq_bot_Bot [simp]: "Bot \<le> x" |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
69 |
by (simp add: less_eq_bot_def) |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
70 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
71 |
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
|
72 |
by simp |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
73 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
74 |
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
|
75 |
by (cases x) (simp_all add: less_eq_bot_def) |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
76 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
77 |
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
|
78 |
by (simp add: less_eq_bot_def) |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
79 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
80 |
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
|
81 |
by (simp add: less_eq_bot_def) |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
82 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
83 |
lemma less_bot_Bot [simp, code]: "x < Bot \<longleftrightarrow> False" |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
84 |
by (simp add: less_bot_def) |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
85 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
86 |
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
|
87 |
by (cases x) (simp_all add: less_bot_def) |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
88 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
89 |
lemma less_bot_Bot_Value [simp]: "Bot < Value x" |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
90 |
by (simp add: less_bot_def) |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
91 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
92 |
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
|
93 |
by simp |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
94 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
95 |
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
|
96 |
by (simp add: less_bot_def) |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
97 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
98 |
instance proof |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
99 |
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
|
100 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
101 |
end |
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 |
instance bot :: (order) order proof |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
104 |
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
|
105 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
106 |
instance bot :: (linorder) linorder proof |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
107 |
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
|
108 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
109 |
instantiation bot :: (preorder) bot |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
110 |
begin |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
111 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
112 |
definition "bot = Bot" |
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 |
instance proof |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
115 |
qed (simp add: bot_bot_def) |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
116 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
117 |
end |
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 |
instantiation bot :: (top) top |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
120 |
begin |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
121 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
122 |
definition "top = Value top" |
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 |
instance proof |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
125 |
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
|
126 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
127 |
end |
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 |
instantiation bot :: (semilattice_inf) semilattice_inf |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
130 |
begin |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
131 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
132 |
definition inf_bot |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
133 |
where |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
134 |
"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
|
135 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
136 |
instance proof |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
137 |
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
|
138 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
139 |
end |
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 |
instantiation bot :: (semilattice_sup) semilattice_sup |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
142 |
begin |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
143 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
144 |
definition sup_bot |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
145 |
where |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
146 |
"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
|
147 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
148 |
instance proof |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
149 |
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
|
150 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
151 |
end |
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 |
instance bot :: (lattice) bounded_lattice_bot .. |
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 |
section {* Values extended by a top element *} |
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 |
datatype 'a top = Value 'a | Top |
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 |
instantiation top :: (preorder) preorder |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
160 |
begin |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
161 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
162 |
definition less_eq_top where |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
163 |
"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
|
164 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
165 |
definition less_top where |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
166 |
"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
|
167 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
168 |
lemma less_eq_top_Top [simp]: "x <= Top" |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
169 |
by (simp add: less_eq_top_def) |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
170 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
171 |
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
|
172 |
by simp |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
173 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
174 |
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
|
175 |
by (cases x) (simp_all add: less_eq_top_def) |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
176 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
177 |
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
|
178 |
by (simp add: less_eq_top_def) |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
179 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
180 |
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
|
181 |
by (simp add: less_eq_top_def) |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
182 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
183 |
lemma less_top_Top [simp, code]: "Top < x \<longleftrightarrow> False" |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
184 |
by (simp add: less_top_def) |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
185 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
186 |
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
|
187 |
by (cases x) (simp_all add: less_top_def) |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
188 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
189 |
lemma less_top_Value_Top [simp]: "Value x < Top" |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
190 |
by (simp add: less_top_def) |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
191 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
192 |
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
|
193 |
by simp |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
194 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
195 |
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
|
196 |
by (simp add: less_top_def) |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
197 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
198 |
instance proof |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
199 |
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
|
200 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
201 |
end |
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 |
instance top :: (order) order proof |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
204 |
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
|
205 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
206 |
instance top :: (linorder) linorder proof |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
207 |
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
|
208 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
209 |
instantiation top :: (preorder) top |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
210 |
begin |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
211 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
212 |
definition "top = Top" |
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 |
instance proof |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
215 |
qed (simp add: top_top_def) |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
216 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
217 |
end |
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 |
instantiation top :: (bot) bot |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
220 |
begin |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
221 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
222 |
definition "bot = Value bot" |
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 |
instance proof |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
225 |
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
|
226 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
227 |
end |
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 |
instantiation top :: (semilattice_inf) semilattice_inf |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
230 |
begin |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
231 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
232 |
definition inf_top |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
233 |
where |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
234 |
"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
|
235 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
236 |
instance proof |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
237 |
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
|
238 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
239 |
end |
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 |
instantiation top :: (semilattice_sup) semilattice_sup |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
242 |
begin |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
243 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
244 |
definition sup_top |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
245 |
where |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
246 |
"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
|
247 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
248 |
instance proof |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
249 |
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
|
250 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
251 |
end |
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 |
instance top :: (lattice) bounded_lattice_top .. |
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 |
section {* Quickcheck configuration *} |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
256 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
257 |
quickcheck_params[default_type = ["int", "non_distrib_lattice", "int bot", "int top"]] |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
258 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
259 |
hide_type non_distrib_lattice bot top |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
260 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
261 |
end |