[isabelle] Questions about . method
Just out of curiosity:
1) Why does the method assumption restrict the given facts to 0 or 1?
2) Why does 'by this' seem to do the same thing? Example: Since I am
using exclusively Isar for proves, I accustomed myself to state lemmas as
assumes "A" and "B" shows "C"
rather than as
lemma "A ==> B ==> C"
lemma "A ==> B ==> A" .
lemma "A ==> B ==> A" by assumption
both works. When 'Isarfying' the lemma a bit more, like
lemma assumes "A" shows "B ==> A"
using assms .
lemma ssumes "A" shows "B ==> A"
using assms by assumption
it is still working. But with
lemma assumes "A" and "B" shows "A"
it doesn't work any longer. Wouldn't it be nice, to have a short way of
proving such simple statements (where one of the current facts solves
the goal). E.g.,
lemma assumes "A" and "B" shows "A' using assms .
And indeed, isn't that, what the documentation claims? In isar-ref.pdf
on page 88, I read "this applies all of the current facts directly as
This archive was generated by a fusion of
Pipermail (Mailman edition) and