Dear all,
I put together some functions on lists (that I use in some small proof)
in Data_List.thy. While doing so and thinking about functions and proofs
I would need in the future, I stumbled across the following points:
1) how to name HOLCF functions for which similar functions already exist
in HOL. As you can see from my example thy-file, I tried to be as close
to Haskell as possible and therefore hid existing HOL-names. My thinking
was that when having a HOLCF type of lazy lists one would never want to
use the HOL datatype list again. Maybe this was oversimplified. What do
you think?
2) I think at some point something like "set :: 'a list => 'a set" for
HOLCF lists would be useful... however, I did not manage to define it,
since I was not able to prove continuity for the following specification
"set $ Nil = {}" |
"set $ (Cons$x$xs) = insert$x$(set$xs)"
Maybe such a function is not a good idea at all in the HOLCF setting and
we should find something different.
3) also if properties only hold for "defined" instances of lists (there
are some differences in how defined they have to be... only xs not
bottom, or additional no element of xs is bottom, ...), I am currently
missing a convenient way of expressing this... (first I was thinking
about "set" from above... but then again, if "set" is a continuous
function also "set$xs" can be undefined... so maybe there is a nicer way?)
4) How to nicely integrate natural numbers? I don't really want to mix
=> and ->, e.g., the "list"-function "take" should have type "nat lift
-> 'a list -> 'a list" (or something similar), rather than "nat => 'a
list -> 'a list" I guess.
I am sure some of you have already considered the above points ;), so
please let me know your conclusions.
cheers
chris
theory Type_Classes
imports HOLCF
begin
class eq =
fixes eq :: "'a::pcpo \<rightarrow> 'a \<rightarrow> tr"
assumes equals_strict [simp]:
"eq\<cdot>x\<cdot>\<bottom> = \<bottom>" "eq\<cdot>\<bottom>\<cdot>y =
\<bottom>"
and eq_simps [dest]:
"eq\<cdot>x\<cdot>y = TT \<Longrightarrow> x = y"
"eq\<cdot>x\<cdot>y = FF \<Longrightarrow> x \<noteq> y"
instantiation lift :: (type) eq
begin
definition eq_lift where
"eq_lift \<equiv> \<Lambda> x y.
(case x of Def x' \<Rightarrow>
(case y of Def y' \<Rightarrow>
Def (x' = y')
| \<bottom> \<Rightarrow> \<bottom>)
| \<bottom> \<Rightarrow> \<bottom>)"
lemma 1: "eq\<cdot>(x::'a lift)\<cdot>\<bottom> = \<bottom>"
by (cases x) (simp add: eq_lift_def)+
lemma 2: "eq\<cdot>\<bottom>\<cdot>(y::'a lift) = \<bottom>"
by (cases y) (simp add: eq_lift_def)+
lemma 3: "eq\<cdot>(x::'a lift)\<cdot>y = TT \<Longrightarrow> x = y"
by (cases x) (cases y, simp_all add: eq_lift_def)+
lemma 4: "eq\<cdot>(x::'a lift)\<cdot>y = FF \<Longrightarrow> x \<noteq> y"
by (cases x) (cases y, simp_all add: eq_lift_def)+
instance
by (intro_classes) (fact 1 2 3 4)+
end
end
theory Data_List
imports Type_Classes
begin
subsection {* Setup *}
hide_type (open) list
hide_const (open) List.append List.Cons List.filter List.foldr List.map
List.Nil List.take
no_notation Map.map_add (infixl "++" 100)
domain 'a list =
Nil |
Cons (lazy head :: 'a) (lazy tail :: "'a list")
abbreviation null :: "'a list \<rightarrow> tr" where "null \<equiv> is_Nil"
subsection {* Definitions *}
fixrec map :: "('a \<rightarrow> 'b) \<rightarrow> 'a list \<rightarrow> 'b
list" where
"map\<cdot>f\<cdot>Nil = Nil" |
"map\<cdot>f\<cdot>(Cons\<cdot>x\<cdot>xs) =
Cons\<cdot>(f\<cdot>x)\<cdot>(map\<cdot>f\<cdot>xs)"
fixrec filter :: "('a \<rightarrow> tr) \<rightarrow> 'a list \<rightarrow> 'a
list" where
"filter\<cdot>P\<cdot>Nil = Nil" |
"filter\<cdot>P\<cdot>(Cons\<cdot>x\<cdot>xs) =
If (P\<cdot>x) then Cons\<cdot>x\<cdot>(filter\<cdot>P\<cdot>xs) else
filter\<cdot>P\<cdot>xs"
fixrec iterate :: "('a \<rightarrow> 'a) \<rightarrow> 'a \<rightarrow> 'a
list" where
"iterate\<cdot>f\<cdot>x =
Cons\<cdot>x\<cdot>(iterate\<cdot>f\<cdot>(f\<cdot>x))"
fixrec foldr :: "('a \<rightarrow> 'b \<rightarrow> 'b) \<rightarrow> 'b
\<rightarrow> 'a list \<rightarrow> 'b" where
"foldr\<cdot>f\<cdot>d\<cdot>Nil = d" |
"foldr\<cdot>f\<cdot>d\<cdot>(Cons\<cdot>x\<cdot>xs) =
f\<cdot>x\<cdot>(foldr\<cdot>f\<cdot>d\<cdot>xs)"
fixrec elem :: "'a::{domain, eq} \<rightarrow> 'a list \<rightarrow> tr" where
"elem\<cdot>x\<cdot>Nil = FF" |
"elem\<cdot>x\<cdot>(Cons\<cdot>y\<cdot>ys) = (eq\<cdot>x\<cdot>y orelse
elem\<cdot>x\<cdot>ys)"
fixrec append :: "'a list \<rightarrow> 'a list \<rightarrow> 'a list" where
"append\<cdot>Nil\<cdot>ys = ys" |
"append\<cdot>(Cons\<cdot>x\<cdot>xs)\<cdot>ys =
Cons\<cdot>x\<cdot>(append\<cdot>xs\<cdot>ys)"
fixrec all :: "('a \<rightarrow> tr) \<rightarrow> 'a list \<rightarrow> tr"
where
"all\<cdot>P\<cdot>Nil = TT" |
"all\<cdot>P\<cdot>(Cons\<cdot>x\<cdot>xs) = (P\<cdot>x andalso
all\<cdot>P\<cdot>xs)"
abbreviation append_syn :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a
list" (infixr "++" 65) where
"xs ++ ys \<equiv> append\<cdot>xs\<cdot>ys"
lemma filter_strict [simp]:
"filter\<cdot>P\<cdot>\<bottom> = \<bottom>"
by fixrec_simp
lemma map_strict [simp]:
"map\<cdot>f\<cdot>\<bottom> = \<bottom>"
by fixrec_simp
lemma map_ID [simp]:
"map\<cdot>ID\<cdot>xs = xs"
by (induct xs) simp_all
lemma strict_foldr_strict2 [simp]:
"(\<And>x. f\<cdot>x\<cdot>\<bottom> = \<bottom>) \<Longrightarrow>
foldr\<cdot>f\<cdot>\<bottom>\<cdot>xs = \<bottom>"
by (induct xs, auto) fixrec_simp
lemma foldr_strict [simp]:
"foldr\<cdot>f\<cdot>d\<cdot>\<bottom> = \<bottom>"
"foldr\<cdot>f\<cdot>\<bottom>\<cdot>Nil = \<bottom>"
"foldr\<cdot>\<bottom>\<cdot>d\<cdot>(Cons\<cdot>x\<cdot>xs) = \<bottom>"
by fixrec_simp+
lemma elem_strict [simp]:
"elem\<cdot>x\<cdot>\<bottom> = \<bottom>"
"elem\<cdot>\<bottom>\<cdot>(Cons\<cdot>y\<cdot>ys) = \<bottom>"
by fixrec_simp+
lemma append_strict1 [simp]:
"\<bottom> ++ ys = \<bottom>"
by fixrec_simp
lemma append_Nil2 [simp]:
"xs ++ Nil = xs"
by (induct xs) simp_all
lemma append_assoc [simp]:
"(xs ++ ys) ++ zs = xs ++ ys ++ zs"
by (induct xs) simp_all
lemma filter_append [simp]:
"filter\<cdot>P\<cdot>(xs ++ ys) = filter\<cdot>P\<cdot>xs ++
filter\<cdot>P\<cdot>ys"
proof (induct xs)
case (Cons x xs) thus ?case by (cases "P\<cdot>x") (auto simp: If_and_if)
qed simp_all
(*FIXME: move*)
lemma orelse_assoc [simp]:
"((x orelse y) orelse z) = (x orelse y orelse z)"
by (cases x rule: trE) auto
lemma elem_append [simp]:
"elem\<cdot>x\<cdot>(xs ++ ys) = (elem\<cdot>x\<cdot>xs orelse
elem\<cdot>x\<cdot>ys)"
by (induct xs) auto
lemma filter_filter [simp]:
"filter\<cdot>P\<cdot>(filter\<cdot>Q\<cdot>xs) = filter\<cdot>(\<Lambda> x.
Q\<cdot>x andalso P\<cdot>x)\<cdot>xs"
by (induct xs) (auto simp: If2_def [symmetric] split: split_If2)
(*FIXME: move*)
lemma neg_orelse [simp]: "neg\<cdot>(x orelse y) = (neg\<cdot>x andalso
neg\<cdot>y)"
by (cases x rule: trE) auto
(*FIXME: move*)
lemma neg_andalso [simp]: "neg\<cdot>(x andalso y) = (neg\<cdot>x orelse
neg\<cdot>y)"
by (cases x rule: trE) auto
lemma head_append [simp]:
"head\<cdot>(xs ++ ys) = If null\<cdot>xs then head\<cdot>ys else
head\<cdot>xs"
by (cases xs) simp_all
end
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
