author | wenzelm |
Wed, 08 Apr 2015 21:24:27 +0200 | |
changeset 59975 | da10875adf8e |
parent 58310 | 91ea607a34d8 |
child 60500 | 903bb1495239 |
permissions | -rw-r--r-- |
57998
8b7508f848ef
rename Quickcheck_Types to Lattice_Constructions and remove quickcheck setup
Andreas Lochbihler
parents:
57997
diff
changeset
|
1 |
(* Title: HOL/Library/Lattice_Constructions.thy |
37915
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 |
|
57998
8b7508f848ef
rename Quickcheck_Types to Lattice_Constructions and remove quickcheck setup
Andreas Lochbihler
parents:
57997
diff
changeset
|
6 |
theory Lattice_Constructions |
57645 | 7 |
imports Main |
37915
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 |
subsection {* Values extended by a bottom element *} |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
11 |
|
58310 | 12 |
datatype 'a bot = Value 'a | Bot |
37915
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
13 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
14 |
instantiation bot :: (preorder) preorder |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
15 |
begin |
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 |
definition less_eq_bot where |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
18 |
"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
|
19 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
20 |
definition less_bot where |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
21 |
"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
|
22 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
23 |
lemma less_eq_bot_Bot [simp]: "Bot \<le> x" |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
24 |
by (simp add: less_eq_bot_def) |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
25 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
26 |
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
|
27 |
by simp |
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 |
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
|
30 |
by (cases x) (simp_all add: less_eq_bot_def) |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
31 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
32 |
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
|
33 |
by (simp add: less_eq_bot_def) |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
34 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
35 |
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
|
36 |
by (simp add: less_eq_bot_def) |
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 |
lemma less_bot_Bot [simp, code]: "x < Bot \<longleftrightarrow> False" |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
39 |
by (simp add: less_bot_def) |
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 |
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
|
42 |
by (cases x) (simp_all add: less_bot_def) |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
43 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
44 |
lemma less_bot_Bot_Value [simp]: "Bot < Value x" |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
45 |
by (simp add: less_bot_def) |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
46 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
47 |
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
|
48 |
by simp |
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 |
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
|
51 |
by (simp add: less_bot_def) |
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 |
instance proof |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
54 |
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
|
55 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
56 |
end |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
57 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
58 |
instance bot :: (order) order proof |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
59 |
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
|
60 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
61 |
instance bot :: (linorder) linorder proof |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
62 |
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
|
63 |
|
43815
4f6e2965d821
adjusted to tightened specification of classes bot and top
haftmann
parents:
40654
diff
changeset
|
64 |
instantiation bot :: (order) bot |
37915
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
65 |
begin |
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 "bot = Bot" |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
68 |
|
57543
36041934e429
adapt and reactivate Quickcheck_Types and add two test cases
Andreas Lochbihler
parents:
44890
diff
changeset
|
69 |
instance .. |
37915
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 |
end |
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 |
instantiation bot :: (top) top |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
74 |
begin |
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 |
definition "top = Value top" |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
77 |
|
57543
36041934e429
adapt and reactivate Quickcheck_Types and add two test cases
Andreas Lochbihler
parents:
44890
diff
changeset
|
78 |
instance .. |
37915
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 |
end |
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 |
instantiation bot :: (semilattice_inf) semilattice_inf |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
83 |
begin |
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 |
definition inf_bot |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
86 |
where |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
87 |
"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
|
88 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
89 |
instance proof |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
90 |
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
|
91 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
92 |
end |
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 |
instantiation bot :: (semilattice_sup) semilattice_sup |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
95 |
begin |
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 |
definition sup_bot |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
98 |
where |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
99 |
"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
|
100 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
101 |
instance proof |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
102 |
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
|
103 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
104 |
end |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
105 |
|
57543
36041934e429
adapt and reactivate Quickcheck_Types and add two test cases
Andreas Lochbihler
parents:
44890
diff
changeset
|
106 |
instance bot :: (lattice) bounded_lattice_bot |
36041934e429
adapt and reactivate Quickcheck_Types and add two test cases
Andreas Lochbihler
parents:
44890
diff
changeset
|
107 |
by(intro_classes)(simp add: bot_bot_def) |
37915
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 |
section {* Values extended by a top element *} |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
110 |
|
58310 | 111 |
datatype 'a top = Value 'a | Top |
37915
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
112 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
113 |
instantiation top :: (preorder) preorder |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
114 |
begin |
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 |
definition less_eq_top where |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
117 |
"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
|
118 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
119 |
definition less_top where |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
120 |
"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
|
121 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
122 |
lemma less_eq_top_Top [simp]: "x <= Top" |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
123 |
by (simp add: less_eq_top_def) |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
124 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
125 |
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
|
126 |
by simp |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
127 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
128 |
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
|
129 |
by (cases x) (simp_all add: less_eq_top_def) |
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 |
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
|
132 |
by (simp add: less_eq_top_def) |
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 |
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
|
135 |
by (simp add: less_eq_top_def) |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
136 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
137 |
lemma less_top_Top [simp, code]: "Top < x \<longleftrightarrow> False" |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
138 |
by (simp add: less_top_def) |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
139 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
140 |
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
|
141 |
by (cases x) (simp_all add: less_top_def) |
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 |
lemma less_top_Value_Top [simp]: "Value x < Top" |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
144 |
by (simp add: less_top_def) |
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 |
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
|
147 |
by simp |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
148 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
149 |
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
|
150 |
by (simp add: less_top_def) |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
151 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
152 |
instance proof |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
153 |
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
|
154 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
155 |
end |
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 |
instance top :: (order) order proof |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
158 |
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
|
159 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
160 |
instance top :: (linorder) linorder proof |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
161 |
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
|
162 |
|
43815
4f6e2965d821
adjusted to tightened specification of classes bot and top
haftmann
parents:
40654
diff
changeset
|
163 |
instantiation top :: (order) top |
37915
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
164 |
begin |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
165 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
166 |
definition "top = Top" |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
167 |
|
57543
36041934e429
adapt and reactivate Quickcheck_Types and add two test cases
Andreas Lochbihler
parents:
44890
diff
changeset
|
168 |
instance .. |
37915
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 |
end |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
171 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
172 |
instantiation top :: (bot) bot |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
173 |
begin |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
174 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
175 |
definition "bot = Value bot" |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
176 |
|
57543
36041934e429
adapt and reactivate Quickcheck_Types and add two test cases
Andreas Lochbihler
parents:
44890
diff
changeset
|
177 |
instance .. |
37915
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 |
end |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
180 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
181 |
instantiation top :: (semilattice_inf) semilattice_inf |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
182 |
begin |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
183 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
184 |
definition inf_top |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
185 |
where |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
186 |
"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
|
187 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
188 |
instance proof |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
189 |
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
|
190 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
191 |
end |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
192 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
193 |
instantiation top :: (semilattice_sup) semilattice_sup |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
194 |
begin |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
195 |
|
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
196 |
definition sup_top |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
197 |
where |
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
198 |
"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
|
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: sup_top_def less_eq_top_def 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 |
|
57543
36041934e429
adapt and reactivate Quickcheck_Types and add two test cases
Andreas Lochbihler
parents:
44890
diff
changeset
|
205 |
instance top :: (lattice) bounded_lattice_top |
36041934e429
adapt and reactivate Quickcheck_Types and add two test cases
Andreas Lochbihler
parents:
44890
diff
changeset
|
206 |
by(intro_classes)(simp add: top_top_def) |
37915
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
207 |
|
57998
8b7508f848ef
rename Quickcheck_Types to Lattice_Constructions and remove quickcheck setup
Andreas Lochbihler
parents:
57997
diff
changeset
|
208 |
subsection {* Values extended by a top and a bottom element *} |
37918
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
209 |
|
58310 | 210 |
datatype 'a flat_complete_lattice = Value 'a | Bot | Top |
37918
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
211 |
|
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
212 |
instantiation flat_complete_lattice :: (type) order |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
213 |
begin |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
214 |
|
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
215 |
definition less_eq_flat_complete_lattice where |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
216 |
"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
|
217 |
|
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
218 |
definition less_flat_complete_lattice where |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
219 |
"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
|
220 |
|
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
221 |
lemma [simp]: "Bot <= y" |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
222 |
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
|
223 |
|
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
224 |
lemma [simp]: "y <= Top" |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
225 |
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
|
226 |
|
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
227 |
lemma greater_than_two_values: |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
228 |
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
|
229 |
shows "z = Top" |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
230 |
using assms |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
231 |
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
|
232 |
|
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
233 |
lemma lesser_than_two_values: |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
234 |
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
|
235 |
shows "z = Bot" |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
236 |
using assms |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
237 |
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
|
238 |
|
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
239 |
instance proof |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
240 |
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
|
241 |
|
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
242 |
end |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
243 |
|
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
244 |
instantiation flat_complete_lattice :: (type) bot |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
245 |
begin |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
246 |
|
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
247 |
definition "bot = Bot" |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
248 |
|
57543
36041934e429
adapt and reactivate Quickcheck_Types and add two test cases
Andreas Lochbihler
parents:
44890
diff
changeset
|
249 |
instance .. |
37918
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
250 |
|
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
251 |
end |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
252 |
|
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
253 |
instantiation flat_complete_lattice :: (type) top |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
254 |
begin |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
255 |
|
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
256 |
definition "top = Top" |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
257 |
|
57543
36041934e429
adapt and reactivate Quickcheck_Types and add two test cases
Andreas Lochbihler
parents:
44890
diff
changeset
|
258 |
instance .. |
37918
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 |
end |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
261 |
|
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
262 |
instantiation flat_complete_lattice :: (type) lattice |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
263 |
begin |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
264 |
|
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
265 |
definition inf_flat_complete_lattice |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
266 |
where |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
267 |
"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
|
268 |
|
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
269 |
definition sup_flat_complete_lattice |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
270 |
where |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
271 |
"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
|
272 |
|
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
273 |
instance proof |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
274 |
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
|
275 |
|
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
276 |
end |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
277 |
|
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
278 |
instantiation flat_complete_lattice :: (type) complete_lattice |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
279 |
begin |
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 |
definition Sup_flat_complete_lattice |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
282 |
where |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
283 |
"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
|
284 |
|
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
285 |
definition Inf_flat_complete_lattice |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
286 |
where |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
287 |
"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
|
288 |
|
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
289 |
instance |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
290 |
proof |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
291 |
fix x A |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
292 |
assume "(x :: 'a flat_complete_lattice) : A" |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
293 |
{ |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
294 |
fix v |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
295 |
assume "A - {Top} = {Value v}" |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
296 |
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
|
297 |
by (auto intro!: the1_equality) |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
298 |
moreover |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
299 |
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
|
300 |
by auto |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
301 |
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
|
302 |
by auto |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
303 |
} |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
304 |
from `x : A` this show "Inf A <= x" |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
305 |
unfolding Inf_flat_complete_lattice_def |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
43815
diff
changeset
|
306 |
by fastforce |
37918
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
307 |
next |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
308 |
fix z A |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
309 |
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
|
310 |
{ |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
311 |
fix v |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
312 |
assume "A - {Top} = {Value v}" |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
313 |
moreover |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
314 |
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
|
315 |
by (auto intro!: the1_equality) |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
316 |
moreover |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
317 |
note z |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
318 |
moreover |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
319 |
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
|
320 |
by auto |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
321 |
} moreover |
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 |
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
|
324 |
have "z <= Bot" |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
325 |
proof (cases "A - {Top} = {Bot}") |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
326 |
case True |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
327 |
from this z show ?thesis |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
328 |
by auto |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
329 |
next |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
330 |
case False |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
331 |
from not_one_value |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
332 |
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
|
333 |
from not_one_value False a1 |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
334 |
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
|
335 |
by (cases a1) auto |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
336 |
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
|
337 |
apply (cases a1) |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
338 |
apply auto |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
339 |
apply (cases a2) |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
340 |
apply auto |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
341 |
apply (auto dest!: lesser_than_two_values) |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
342 |
done |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
343 |
qed |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
344 |
} moreover |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
345 |
note z moreover |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
346 |
ultimately show "z <= Inf A" |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
347 |
unfolding Inf_flat_complete_lattice_def |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
348 |
by auto |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
349 |
next |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
350 |
fix x A |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
351 |
assume "(x :: 'a flat_complete_lattice) : A" |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
352 |
{ |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
353 |
fix v |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
354 |
assume "A - {Bot} = {Value v}" |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
355 |
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
|
356 |
by (auto intro!: the1_equality) |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
357 |
moreover |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
358 |
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
|
359 |
by auto |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
360 |
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
|
361 |
by auto |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
362 |
} |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
363 |
from `x : A` this show "x <= Sup A" |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
364 |
unfolding Sup_flat_complete_lattice_def |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
43815
diff
changeset
|
365 |
by fastforce |
37918
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
366 |
next |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
367 |
fix z A |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
368 |
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
|
369 |
{ |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
370 |
fix v |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
371 |
assume "A - {Bot} = {Value v}" |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
372 |
moreover |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
373 |
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
|
374 |
by (auto intro!: the1_equality) |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
375 |
moreover |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
376 |
note z |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
377 |
moreover |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
378 |
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
|
379 |
by auto |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
380 |
} moreover |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
381 |
{ |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
382 |
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
|
383 |
have "Top <= z" |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
384 |
proof (cases "A - {Bot} = {Top}") |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
385 |
case True |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
386 |
from this z show ?thesis |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
387 |
by auto |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
388 |
next |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
389 |
case False |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
390 |
from not_one_value |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
391 |
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
|
392 |
from not_one_value False a1 |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
393 |
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
|
394 |
by (cases a1) auto |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
395 |
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
|
396 |
apply (cases a1) |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
397 |
apply auto |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
398 |
apply (cases a2) |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
399 |
apply (auto dest!: greater_than_two_values) |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
400 |
done |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
401 |
qed |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
402 |
} moreover |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
403 |
note z moreover |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
404 |
ultimately show "Sup A <= z" |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
405 |
unfolding Sup_flat_complete_lattice_def |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
406 |
by auto |
57543
36041934e429
adapt and reactivate Quickcheck_Types and add two test cases
Andreas Lochbihler
parents:
44890
diff
changeset
|
407 |
next |
36041934e429
adapt and reactivate Quickcheck_Types and add two test cases
Andreas Lochbihler
parents:
44890
diff
changeset
|
408 |
show "Inf {} = (top :: 'a flat_complete_lattice)" |
36041934e429
adapt and reactivate Quickcheck_Types and add two test cases
Andreas Lochbihler
parents:
44890
diff
changeset
|
409 |
by(simp add: Inf_flat_complete_lattice_def top_flat_complete_lattice_def) |
36041934e429
adapt and reactivate Quickcheck_Types and add two test cases
Andreas Lochbihler
parents:
44890
diff
changeset
|
410 |
next |
36041934e429
adapt and reactivate Quickcheck_Types and add two test cases
Andreas Lochbihler
parents:
44890
diff
changeset
|
411 |
show "Sup {} = (bot :: 'a flat_complete_lattice)" |
36041934e429
adapt and reactivate Quickcheck_Types and add two test cases
Andreas Lochbihler
parents:
44890
diff
changeset
|
412 |
by(simp add: Sup_flat_complete_lattice_def bot_flat_complete_lattice_def) |
37918
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
413 |
qed |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
414 |
|
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
415 |
end |
eda5faaca9e2
adding a type for flat complete lattice to Quickcheck_Types
bulwahn
parents:
37915
diff
changeset
|
416 |
|
37915
e709e764f20c
adding Library theory for other quickcheck default types
bulwahn
parents:
diff
changeset
|
417 |
end |