Email Gateway (Aug 18 2022 at 09:56): Email Gateway (Aug 18 2022 at 09:56):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hello all,
I have the following lemma:
consts f:: "'a set => 'a set"
lemma fin: "f X = \<Union> { f {x} | x . x : X }" sorry
And in a proof, I have to solve the following subgoal:
"f X = \<Union> { f {(a,b)} | a b . (a,b) : X }"
How to do this elegantly using lemma fin ?? Things like (simp add: fin)
or (auto iff add: fin) do not work ?
Greetings and thanks in advance
Peter Lammich
Email Gateway (Aug 18 2022 at 09:56):From: Brian Huffman <brianh@csee.ogi.edu>
The reason fin does not work as a simplification rule is because it loops:
Notice that the right-hand side mentions "f {x}", which is an instance of the
pattern on the left-hand side.
I can think of two workarounds. First, you can use (subst fin); the subst
tactic only applies the rewrite once, not repeatedly like simp does.
Alternatively, you can use (simp add: fin [of X]) or (simp add: fin [where
X=X]). This prevents the simplifier from looping, since the instantiated rule
will not match terms like "f {x}".
Email Gateway (Aug 18 2022 at 09:56):From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
Peter Lammich wrote:
Peter,
If all else fails, try using the following lemma:
Goal "{ f {x} | x . x : X } = { f {(a,b)} | a b . (a,b) : X }";
Level 0 (1 subgoal)
{f {x} |x. x : X} = {f {(a, b)} |a b. (a, b) : X}
1. {f {x} |x. x : X} = {f {(a, b)} |a b. (a, b) : X}
val it = [] : Thm.thm list
auto();
Level 1
{f {x} |x. x : X} = {f {(a, b)} |a b. (a, b) : X}
No subgoals!
val it = () : unit
Jeremy
Last updated: May 03 2024 at 04:19 UTC