[isabelle] assumptions format in isar



Hi All,

In isar proofs I am chaining facts with moreover like this
from hyp1 have foo1 .
moreover
from hyp2 have foo2 .
...
ultimately have main ...

Then, I have a goal and a bunch of facts in "using this".

For technical reasons I need to have the same behavior as if I would type:
main
apply (insert foo1)
apply (insert foo2)
...

That is, to move the facts from "using this" to the goal.

My current "trick" is to add "apply (simp)" or "apply clarsimp" after "ultimately have main". This puts the hypotheses within the goal (at least this is my understanding). But, if there is nothing to simplify, the trick does not work. I can use the "apply insert" within isar proofs, but it's not so nice :-)

Does anyone have an idea how I can put the hypotheses within the goal (another trick like "apply simp" that would work even if there is nothing to simplify would work :-) ?

Thanks,

Julien

--
Julien Schmaltz                Saarland University
Computer Science Department    Institute for Computer Architecture
Phone: +49 (0)681 302 2419     Fax: +49 (0)681 302 4290
Email: julien at cs.uni-sb.de     WWW: http://www-wjp.cs.uni-sb.de/







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