Email Gateway (Aug 18 2022 at 13:15): Email Gateway (Aug 18 2022 at 13:15):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Gentlemen,
While trying to figure out a way to do a step of a more complex tactic,
I came across subst doing something unexpected to me.
Given a right-associative operator and an associativity property about it:
consts
foo :: "('a => bool) => ('a => bool) => 'a => bool" (infixr "**" 35)
lemma assoc_state:
"((P Q) R) s = (P Q R) s"
sorry
When I try to use it for a specific rewrite:
lemma "((C B A) ** D) s"
apply (subst assoc_state[where P=C and Q="B ** A" and R=D])
I get: "(C (B A) ** D) s"
whereas I expect "(C B A ** D) s"
Does anyone know why this is the case?
Sincerely,
Rafal Kolanski.
Email Gateway (Aug 18 2022 at 13:20):From: Lawrence Paulson <lp15@cam.ac.uk>
The problem is that your expectations are incorrect. If we show the
full bracketing, you are starting with the expression
((C (B A)) ** D)
and the result of applying your substitution should be
(C ((B A) ** D)).
Isabelle gives you precisely this. You were expecting to see
(C (B (A ** D))),
which requires a further application of your equality.
This sort of thing is not trivial to work out in your head. I had to
write it down. That is why we prefer to leave it to computers :-)
Larry Paulson
Last updated: May 03 2024 at 08:18 UTC