Email Gateway (Aug 18 2022 at 14:14): Email Gateway (Aug 18 2022 at 14:14):From: Peter Lammich <peter.lammich@uni-muenster.de>
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
Email Gateway (Aug 18 2022 at 14:14):From: Brian Huffman <brianh@cs.pdx.edu>
Hi Peter,
I managed to get the simplifier to do what you want. First, you will
need to prove a simp rule for rewriting list_case when both branches
are the same:
lemma list_case_const: "(case xs of [] => k | b # bs => k) = k"
by (induct xs) simp_all
You are also correct in thinking that the congruence rules are causing
problems. You will need to disable the default cong rule for
list_case, which you can do with "cong del". The following command
does what you want:
apply (simp add: list_case_const cong del: list.case_cong)
Email Gateway (Aug 18 2022 at 14:15):From: Peter Lammich <peter.lammich@uni-muenster.de>
Nice!
I'll soon try it out, it should make some of my proofs definitely more
elegant.
Peter
Brian Huffman wrote:
Last updated: Nov 21 2024 at 12:39 UTC