[isabelle] simplification at the ML level



Hello,

  I woud like to simplify goals having the following pattern : "X ==> False" .
Like for example simplifying
¬ ( (a /= b) \/ (f a = b)) ==> False
to
(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 to get
"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,
Clément






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.