On Thu, Jul 19, 2012 at 8:32 AM, Christian Sternagel <[email protected]> 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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
