author | haftmann |
Fri, 02 Mar 2007 15:43:15 +0100 | |
changeset 22384 | 33a46e6c7f04 |
parent 22179 | 1a3575de2afc |
child 22473 | 753123c89d72 |
permissions | -rw-r--r-- |
22068 | 1 |
(* ID: $Id$ |
20436 | 2 |
Author: Florian Haftmann, TU Muenchen |
3 |
*) |
|
4 |
||
5 |
header {* Collection classes as examples for code generation *} |
|
6 |
||
7 |
theory CodeCollections |
|
21460 | 8 |
imports Main Product_ord List_lexord |
20436 | 9 |
begin |
10 |
||
21460 | 11 |
fun |
12 |
abs_sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where |
|
13 |
"abs_sorted cmp [] \<longleftrightarrow> True" |
|
14 |
"abs_sorted cmp [x] \<longleftrightarrow> True" |
|
15 |
"abs_sorted cmp (x#y#xs) \<longleftrightarrow> cmp x y \<and> abs_sorted cmp (y#xs)" |
|
20436 | 16 |
|
21460 | 17 |
abbreviation (in ord) |
18 |
"sorted \<equiv> abs_sorted less_eq" |
|
20436 | 19 |
|
22068 | 20 |
lemma (in order) sorted_weakening: |
20436 | 21 |
assumes "sorted (x # xs)" |
22 |
shows "sorted xs" |
|
23 |
using prems proof (induct xs) |
|
24 |
case Nil show ?case by simp |
|
25 |
next |
|
26 |
case (Cons x' xs) |
|
21460 | 27 |
from this have "sorted (x # x' # xs)" by auto |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
28 |
then show "sorted (x' # xs)" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
29 |
by auto |
20436 | 30 |
qed |
31 |
||
21460 | 32 |
instance unit :: order |
33 |
"u \<le> v \<equiv> True" |
|
34 |
"u < v \<equiv> False" |
|
21924 | 35 |
by default (simp_all add: less_eq_unit_def less_unit_def) |
20436 | 36 |
|
21460 | 37 |
fun le_option' :: "'a\<Colon>order option \<Rightarrow> 'a option \<Rightarrow> bool" |
38 |
where "le_option' None y \<longleftrightarrow> True" |
|
39 |
| "le_option' (Some x) None \<longleftrightarrow> False" |
|
40 |
| "le_option' (Some x) (Some y) \<longleftrightarrow> x \<le> y" |
|
20436 | 41 |
|
21460 | 42 |
instance option :: (order) order |
43 |
"x \<le> y \<equiv> le_option' x y" |
|
44 |
"x < y \<equiv> x \<le> y \<and> x \<noteq> y" |
|
21924 | 45 |
proof (default, unfold less_eq_option_def less_option_def) |
20436 | 46 |
fix x |
47 |
show "le_option' x x" by (cases x) simp_all |
|
48 |
next |
|
49 |
fix x y z |
|
50 |
assume "le_option' x y" "le_option' y z" |
|
51 |
then show "le_option' x z" |
|
52 |
by (cases x, simp_all, cases y, simp_all, cases z, simp_all) |
|
53 |
next |
|
54 |
fix x y |
|
55 |
assume "le_option' x y" "le_option' y x" |
|
56 |
then show "x = y" |
|
57 |
by (cases x, simp_all, cases y, simp_all, cases y, simp_all) |
|
58 |
next |
|
21460 | 59 |
fix x y |
60 |
show "le_option' x y \<and> x \<noteq> y \<longleftrightarrow> le_option' x y \<and> x \<noteq> y" .. |
|
20436 | 61 |
qed |
62 |
||
63 |
lemma [simp, code]: |
|
21460 | 64 |
"None \<le> y \<longleftrightarrow> True" |
65 |
"Some x \<le> None \<longleftrightarrow> False" |
|
66 |
"Some v \<le> Some w \<longleftrightarrow> v \<le> w" |
|
21924 | 67 |
unfolding less_eq_option_def less_option_def le_option'.simps by rule+ |
20436 | 68 |
|
21460 | 69 |
lemma forall_all [simp]: |
70 |
"list_all P xs \<longleftrightarrow> (\<forall>x\<in>set xs. P x)" |
|
71 |
by (induct xs) auto |
|
20436 | 72 |
|
21460 | 73 |
lemma exists_ex [simp]: |
74 |
"list_ex P xs \<longleftrightarrow> (\<exists>x\<in>set xs. P x)" |
|
75 |
by (induct xs) auto |
|
20436 | 76 |
|
22179 | 77 |
class finite = |
21460 | 78 |
fixes fin :: "'a list" |
79 |
assumes member_fin: "x \<in> set fin" |
|
80 |
begin |
|
20436 | 81 |
|
21460 | 82 |
lemma set_enum_UNIV: |
83 |
"set fin = UNIV" |
|
84 |
using member_fin by auto |
|
20436 | 85 |
|
21460 | 86 |
lemma all_forall [code func, code inline]: |
87 |
"(\<forall>x. P x) \<longleftrightarrow> list_all P fin" |
|
88 |
using set_enum_UNIV by simp_all |
|
20436 | 89 |
|
21460 | 90 |
lemma ex_exists [code func, code inline]: |
91 |
"(\<exists>x. P x) \<longleftrightarrow> list_ex P fin" |
|
92 |
using set_enum_UNIV by simp_all |
|
20436 | 93 |
|
21460 | 94 |
end |
95 |
||
22179 | 96 |
instance bool :: finite |
21924 | 97 |
"fin == [False, True]" |
21460 | 98 |
by default (simp_all add: fin_bool_def) |
20436 | 99 |
|
22179 | 100 |
instance unit :: finite |
21924 | 101 |
"fin == [()]" |
21460 | 102 |
by default (simp_all add: fin_unit_def) |
20436 | 103 |
|
21460 | 104 |
fun |
20436 | 105 |
product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a * 'b) list" |
21460 | 106 |
where |
20436 | 107 |
"product [] ys = []" |
108 |
"product (x#xs) ys = map (Pair x) ys @ product xs ys" |
|
109 |
||
110 |
lemma product_all: |
|
111 |
assumes "x \<in> set xs" "y \<in> set ys" |
|
112 |
shows "(x, y) \<in> set (product xs ys)" |
|
113 |
using prems proof (induct xs) |
|
114 |
case Nil |
|
115 |
then have False by auto |
|
116 |
then show ?case .. |
|
117 |
next |
|
118 |
case (Cons z xs) |
|
119 |
then show ?case |
|
120 |
proof (cases "x = z") |
|
121 |
case True |
|
122 |
with Cons have "(x, y) \<in> set (product (x # xs) ys)" by simp |
|
123 |
with True show ?thesis by simp |
|
124 |
next |
|
125 |
case False |
|
126 |
with Cons have "x \<in> set xs" by auto |
|
127 |
with Cons have "(x, y) \<in> set (product xs ys)" by auto |
|
128 |
then show "(x, y) \<in> set (product (z#xs) ys)" by auto |
|
129 |
qed |
|
130 |
qed |
|
131 |
||
22179 | 132 |
instance * :: (finite, finite) finite |
21924 | 133 |
"fin == product fin fin" |
20436 | 134 |
apply default |
21460 | 135 |
apply (simp_all add: "fin_*_def") |
20436 | 136 |
apply (unfold split_paired_all) |
137 |
apply (rule product_all) |
|
22384
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22179
diff
changeset
|
138 |
apply (rule member_fin)+ |
21460 | 139 |
done |
20436 | 140 |
|
22179 | 141 |
instance option :: (finite) finite |
21924 | 142 |
"fin == None # map Some fin" |
21460 | 143 |
proof (default, unfold fin_option_def) |
22179 | 144 |
fix x :: "'a::finite option" |
21460 | 145 |
show "x \<in> set (None # map Some fin)" |
20436 | 146 |
proof (cases x) |
147 |
case None then show ?thesis by auto |
|
148 |
next |
|
22384
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22179
diff
changeset
|
149 |
case (Some x) then show ?thesis by (auto intro: member_fin) |
20436 | 150 |
qed |
151 |
qed |
|
152 |
||
153 |
consts |
|
154 |
get_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a option" |
|
155 |
||
156 |
primrec |
|
157 |
"get_first p [] = None" |
|
158 |
"get_first p (x#xs) = (if p x then Some x else get_first p xs)" |
|
159 |
||
160 |
consts |
|
161 |
get_index :: "('a \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> nat option" |
|
162 |
||
163 |
primrec |
|
164 |
"get_index p n [] = None" |
|
165 |
"get_index p n (x#xs) = (if p x then Some n else get_index p (Suc n) xs)" |
|
166 |
||
21460 | 167 |
(*definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21319
diff
changeset
|
168 |
between :: "'a::enum \<Rightarrow> 'a \<Rightarrow> 'a option" where |
20436 | 169 |
"between x y = get_first (\<lambda>z. x << z & z << y) enum" |
170 |
||
171 |
definition |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21319
diff
changeset
|
172 |
index :: "'a::enum \<Rightarrow> nat" where |
20436 | 173 |
"index x = the (get_index (\<lambda>y. y = x) 0 enum)" |
174 |
||
175 |
definition |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21319
diff
changeset
|
176 |
add :: "'a::enum \<Rightarrow> 'a \<Rightarrow> 'a" where |
20436 | 177 |
"add x y = |
178 |
(let |
|
179 |
enm = enum |
|
180 |
in enm ! ((index x + index y) mod length enm))" |
|
181 |
||
182 |
consts |
|
183 |
sum :: "'a::{enum, infimum} list \<Rightarrow> 'a" |
|
184 |
||
185 |
primrec |
|
186 |
"sum [] = inf" |
|
21460 | 187 |
"sum (x#xs) = add x (sum xs)"*) |
20436 | 188 |
|
21460 | 189 |
(*definition "test1 = sum [None, Some True, None, Some False]"*) |
190 |
(*definition "test2 = (inf :: nat \<times> unit)"*) |
|
191 |
definition "test3 \<longleftrightarrow> (\<exists>x \<Colon> bool option. case x of Some P \<Rightarrow> P | None \<Rightarrow> False)" |
|
192 |
||
22179 | 193 |
code_gen test3 (SML #) (OCaml -) (Haskell -) |
20436 | 194 |
|
195 |
end |