[isabelle-dev] HOLCF lists

[Brian Huffman]

On Thu, Jul 19, 2012 at 8:32 AM, Christian Sternagel
<c-sterna at jaist.ac.jp> wrote:
> I created a repository at
>
> http://sourceforge.net/p/holcf-prelude/

Thanks for setting this up!

> PPS: As I mentioned in an earlier mail. I would like to add a constant "set
> :: 'a Data_List.list => 'a set" for specification purposes. I don't see how
> this is possible as inductive_set. Any hints?

I defined "set" in terms of a binary list membership predicate that I
defined with "inductive". It seems that inductive_set is unable to
directly define a constant of type "'a => 'b set" unless the parameter
of type 'a is fixed.

> The reason why I think I need this function is that I want to prove
>
>   filter$P$(filter$Q$xs) = filter$Q$(filter$P$xs)
>
> which is not true unconditionally due to strictness issues. I thought that
> using "set" I could formulate appropriate assumptions, such that the above
> equation holds, e.g., "ALL x : set xs. P x andalso Q x = Q x andalso P x".

I was able to prove a congruence lemma for filter in terms of set,
using fixed-point induction:

lemma filter_cong: "ALL x : set xs. p$x = q$x ==> filter$p$xs = filter$q$xs"

This should be sufficient to prove plenty of other lemmas including
the one you mention.

- Brian