(* ID: $Id$
Author: Florian Haftmann, TU Muenchen
*)
header {* Collection classes as examples for code generation *}
theory CodeCollections
imports Main
begin
section {* Collection classes as examples for code generation *}
class ordered = eq +
constrains eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^loc><<=" 65)
fixes lt :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^loc><<" 65)
assumes order_refl: "x \<^loc><<= x"
assumes order_trans: "x \<^loc><<= y ==> y \<^loc><<= z ==> x \<^loc><<= z"
assumes order_antisym: "x \<^loc><<= y ==> y \<^loc><<= x ==> x = y"
declare order_refl [simp, intro]
defs
lt_def: "x << y == (x <<= y \<and> x \<noteq> y)"
lemma lt_intro [intro]:
assumes "x <<= y" and "x \<noteq> y"
shows "x << y"
unfolding lt_def ..
lemma lt_elim [elim]:
assumes "(x::'a::ordered) << y"
and Q: "!!x y::'a::ordered. x <<= y \<Longrightarrow> x \<noteq> y \<Longrightarrow> P"
shows P
proof -
from prems have R1: "x <<= y" and R2: "x \<noteq> y" by (simp_all add: lt_def)
show P by (rule Q [OF R1 R2])
qed
lemma lt_trans:
assumes "x << y" and "y << z"
shows "x << z"
proof
from prems lt_def have prems': "x <<= y" "y <<= z" by auto
show "x <<= z" by (rule order_trans, auto intro: prems')
next
show "x \<noteq> z"
proof
from prems lt_def have prems': "x <<= y" "y <<= z" "x \<noteq> y" by auto
assume "x = z"
with prems' have "x <<= y" and "y <<= x" by auto
with order_antisym have "x = y" .
with prems' show False by auto
qed
qed
definition (in ordered)
min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
"min x y = (if x \<^loc><<= y then x else y)"
max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
"max x y = (if x \<^loc><<= y then y else x)"
definition
min :: "'a::ordered \<Rightarrow> 'a \<Rightarrow> 'a"
"min x y = (if x <<= y then x else y)"
max :: "'a::ordered \<Rightarrow> 'a \<Rightarrow> 'a"
"max x y = (if x <<= y then y else x)"
fun abs_sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
where
"abs_sorted cmp [] = True"
| "abs_sorted cmp [x] = True"
| "abs_sorted cmp (x#y#xs) = (cmp x y \<and> abs_sorted cmp (y#xs))"
termination by (auto_term "measure (length o snd)")
thm abs_sorted.simps
abbreviation (in ordered)
"sorted \<equiv> abs_sorted le"
abbreviation
"sorted \<equiv> abs_sorted le"
lemma (in ordered) sorted_weakening:
assumes "sorted (x # xs)"
shows "sorted xs"
using prems proof (induct xs)
case Nil show ?case by simp
next
case (Cons x' xs)
from this(5) have "sorted (x # x' # xs)" .
then show "sorted (x' # xs)"
by auto
qed
instance bool :: ordered
"p <<= q == (p --> q)"
by default (unfold ordered_bool_def, blast+)
instance nat :: ordered
"m <<= n == m <= n"
by default (simp_all add: ordered_nat_def)
instance int :: ordered
"k <<= l == k <= l"
by default (simp_all add: ordered_int_def)
instance unit :: ordered
"u <<= v == True"
by default (simp_all add: ordered_unit_def)
fun le_option' :: "'a::ordered option \<Rightarrow> 'a option \<Rightarrow> bool"
where
"le_option' None y = True"
| "le_option' (Some x) None = False"
| "le_option' (Some x) (Some y) = x <<= y"
termination by (auto_term "{}")
instance option :: (ordered) ordered
"x <<= y == le_option' x y"
proof (default, unfold ordered_option_def)
fix x
show "le_option' x x" by (cases x) simp_all
next
fix x y z
assume "le_option' x y" "le_option' y z"
then show "le_option' x z"
by (cases x, simp_all, cases y, simp_all, cases z, simp_all)
(erule order_trans, assumption)
next
fix x y
assume "le_option' x y" "le_option' y x"
then show "x = y"
by (cases x, simp_all, cases y, simp_all, cases y, simp_all)
(erule order_antisym, assumption)
qed
lemma [simp, code]:
"None <<= y = True"
"Some x <<= None = False"
"Some v <<= Some w = v <<= w"
unfolding ordered_option_def le_option'.simps by rule+
fun le_pair' :: "'a::ordered \<times> 'b::ordered \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
where
"le_pair' (x1, y1) (x2, y2) = (x1 << x2 \<or> x1 = x2 \<and> y1 <<= y2)"
termination by (auto_term "{}")
instance * :: (ordered, ordered) ordered
"x <<= y == le_pair' x y"
apply (default, unfold "ordered_*_def", unfold split_paired_all)
apply simp_all
apply (auto intro: lt_trans order_trans)[1]
unfolding lt_def apply (auto intro: order_antisym)[1]
done
lemma [simp, code]:
"(x1, y1) <<= (x2, y2) = (x1 << x2 \<or> x1 = x2 \<and> y1 <<= y2)"
unfolding "ordered_*_def" le_pair'.simps ..
(*
fun le_list' :: "'a::ordered list \<Rightarrow> 'a list \<Rightarrow> bool"
where
"le_list' [] ys = True"
| "le_list' (x#xs) [] = False"
| "le_list' (x#xs) (y#ys) = (x << y \<or> x = y \<and> le_list' xs ys)"
termination by (auto_term "measure (length o fst)")
instance (ordered) list :: ordered
"xs <<= ys == le_list' xs ys"
proof (default, unfold "ordered_list_def")
fix xs
show "le_list' xs xs" by (induct xs) simp_all
next
fix xs ys zs
assume "le_list' xs ys" and "le_list' ys zs"
then show "le_list' xs zs"
apply (induct xs zs rule: le_list'.induct)
apply simp_all
apply (cases ys) apply simp_all
apply (induct ys) apply simp_all
apply (induct ys)
apply simp_all
apply (induct zs)
apply simp_all
next
fix xs ys
assume "le_list' xs ys" and "le_list' ys xs"
show "xs = ys" sorry
qed
lemma [simp, code]:
"[] <<= ys = True"
"(x#xs) <<= [] = False"
"(x#xs) <<= (y#ys) = (x << y \<or> x = y \<and> xs <<= ys)"
unfolding "ordered_list_def" le_list'.simps by rule+*)
class infimum = ordered +
fixes inf
assumes inf: "inf \<^loc><<= x"
lemma (in infimum)
assumes prem: "a \<^loc><<= inf"
shows no_smaller: "a = inf"
using prem inf by (rule order_antisym)
ML {* set quick_and_dirty *}
function abs_max_of :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a"
where
"abs_max_of cmp inff [] = inff"
| "abs_max_of cmp inff [x] = x"
| "abs_max_of cmp inff (x#xs) =
ordered.max cmp x (abs_max_of cmp inff xs)"
apply pat_completeness sorry
abbreviation (in infimum)
"max_of xs \<equiv> abs_max_of le inf"
abbreviation
"max_of xs \<equiv> abs_max_of le inf"
instance bool :: infimum
"inf == False"
by default (simp add: infimum_bool_def)
instance nat :: infimum
"inf == 0"
by default (simp add: infimum_nat_def)
instance unit :: infimum
"inf == ()"
by default (simp add: infimum_unit_def)
instance option :: (ordered) infimum
"inf == None"
by default (simp add: infimum_option_def)
instance * :: (infimum, infimum) infimum
"inf == (inf, inf)"
by default (unfold "infimum_*_def", unfold split_paired_all, auto intro: inf)
class enum = ordered +
fixes enum :: "'a list"
assumes member_enum: "x \<in> set enum"
and ordered_enum: "abs_sorted le enum"
(*
FIXME:
- abbreviations must be propagated before locale introduction
- then also now shadowing may occur
*)
(*abbreviation (in enum)
"local.sorted \<equiv> abs_sorted le"*)
instance bool :: enum
(* FIXME: better name handling of definitions *)
"_1": "enum == [False, True]"
by default (simp_all add: enum_bool_def)
instance unit :: enum
"_2": "enum == [()]"
by default (simp_all add: enum_unit_def)
(*consts
product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a * 'b) list"
primrec
"product [] ys = []"
"product (x#xs) ys = map (Pair x) ys @ product xs ys"
lemma product_all:
assumes "x \<in> set xs" "y \<in> set ys"
shows "(x, y) \<in> set (product xs ys)"
using prems proof (induct xs)
case Nil
then have False by auto
then show ?case ..
next
case (Cons z xs)
then show ?case
proof (cases "x = z")
case True
with Cons have "(x, y) \<in> set (product (x # xs) ys)" by simp
with True show ?thesis by simp
next
case False
with Cons have "x \<in> set xs" by auto
with Cons have "(x, y) \<in> set (product xs ys)" by auto
then show "(x, y) \<in> set (product (z#xs) ys)" by auto
qed
qed
lemma product_sorted:
assumes "sorted xs" "sorted ys"
shows "sorted (product xs ys)"
using prems proof (induct xs)
case Nil
then show ?case by simp
next
case (Cons x xs)
from Cons ordered.sorted_weakening have "sorted xs" by auto
with Cons have "sorted (product xs ys)" by auto
then show ?case apply simp
proof -
assume
apply simp
proof (cases "x = z")
case True
with Cons have "(x, y) \<in> set (product (x # xs) ys)" by simp
with True show ?thesis by simp
next
case False
with Cons have "x \<in> set xs" by auto
with Cons have "(x, y) \<in> set (product xs ys)" by auto
then show "(x, y) \<in> set (product (z#xs) ys)" by auto
qed
qed
instance (enum, enum) * :: enum
"_3": "enum == product enum enum"
apply default
apply (simp_all add: "enum_*_def")
apply (unfold split_paired_all)
apply (rule product_all)
apply (rule member_enum)+
sorry*)
instance option :: (enum) enum
"_4": "enum == None # map Some enum"
proof (default, unfold enum_option_def)
fix x :: "'a::enum option"
show "x \<in> set (None # map Some enum)"
proof (cases x)
case None then show ?thesis by auto
next
case (Some x) then show ?thesis by (auto intro: member_enum)
qed
next
show "sorted (None # map Some (enum :: ('a::enum) list))"
sorry
(*proof (cases "enum :: 'a list")
case Nil then show ?thesis by simp
next
case (Cons x xs)
then have "sorted (None # map Some (x # xs))" sorry
then show ?thesis apply simp
apply simp_all
apply auto*)
qed
ML {* reset quick_and_dirty *}
consts
get_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a option"
primrec
"get_first p [] = None"
"get_first p (x#xs) = (if p x then Some x else get_first p xs)"
consts
get_index :: "('a \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> nat option"
primrec
"get_index p n [] = None"
"get_index p n (x#xs) = (if p x then Some n else get_index p (Suc n) xs)"
definition
between :: "'a::enum \<Rightarrow> 'a \<Rightarrow> 'a option"
"between x y = get_first (\<lambda>z. x << z & z << y) enum"
definition
index :: "'a::enum \<Rightarrow> nat"
"index x = the (get_index (\<lambda>y. y = x) 0 enum)"
definition
add :: "'a::enum \<Rightarrow> 'a \<Rightarrow> 'a"
"add x y =
(let
enm = enum
in enm ! ((index x + index y) mod length enm))"
consts
sum :: "'a::{enum, infimum} list \<Rightarrow> 'a"
primrec
"sum [] = inf"
"sum (x#xs) = add x (sum xs)"
definition
"test1 = sum [None, Some True, None, Some False]"
"test2 = (inf :: nat \<times> unit)"
code_gen "op <<="
code_gen "op <<"
code_gen inf
code_gen between
code_gen index
code_gen test1
code_gen test2
code_gen (SML -)
end