[isabelle-dev] HOLCF lists

[Christian Sternagel]

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