[isabelle-dev] HOLCF lists
Brian Huffman
huffman at in.tum.de
Thu Jul 19 10:10:18 CEST 2012
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
More information about the isabelle-dev
mailing list