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