*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Simplifier problem (Congruence rules?)*From*: Peter Lammich <peter.lammich at uni-muenster.de>*Date*: Tue, 27 Oct 2009 20:59:16 +0100*User-agent*: Thunderbird 2.0.0.23 (X11/20090817)

Hi all, I have some problem with the simplifier, probably with congruence rule setup: Consider the goal: "P (\<Union>x\<in>S. case x of [] \<Rightarrow> f True | (a#as) \<Rightarrow> f (case c x of [] \<Rightarrow> True | (b#bs) \<Rightarrow> True) )" is there any way to set up the simplifier such that it will rewrite this goal to: "P (\<Union>x\<in>S. f True)" ? Regards & thanks for any help in advance, Peter

**Follow-Ups**:**Re: [isabelle] Simplifier problem (Congruence rules?)***From:*Brian Huffman

- Previous by Date: Re: [isabelle] Lattices with explicit carrier set vs. lattices with implicit carrier set
- Next by Date: Re: [isabelle] Lattices with explicit carrier set vs. lattices with implicit carrier set
- Previous by Thread: Re: [isabelle] Lattices with explicit carrier set vs. lattices with implicit carrier set[SEC=UNCLASSIFIED]
- Next by Thread: Re: [isabelle] Simplifier problem (Congruence rules?)
- Cl-isabelle-users October 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list