[isabelle-dev] HOLCF lists

Christian Sternagel c-sterna at jaist.ac.jp
Tue Jul 17 11:04:43 CEST 2012

```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

cheers

chris
-------------- next part --------------
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
-------------- next part --------------
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

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