[isabelle] assumptions format in isar
In isar proofs I am chaining facts with moreover like this
from hyp1 have foo1 .
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:
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
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 :-) ?
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