[isabelle] simplification at the ML level
I woud like to simplify goals having the following pattern : "X ==> False" .
Like for example simplifying
¬ ( (a /= b) \/ (f a = b)) ==> False
(a = b /\ f b /= b) ==> False
(at the ML level) But the Simp_tac tactic fails, I guess because it
works from bottom to up.
What should I use ?
Another problem I'm running into is that I want to simplify goal
without implicitly applying assumption too. For example I would like
"X ==> X" from "~~ X ==> ~~X"
At the proof general level, using "simp" is too strong and finishs the
proof in 1 step. Using "simp (no_asm)" only simplifies the right hand
side which is not what I want too. I'm maybe confused by the term
"assumption" sometimes refering to the hypothesis, sometimes refering
to the "assumption" tactic.
And what about that at the ML level ?
Thanks for your help,
This archive was generated by a fusion of
Pipermail (Mailman edition) and