[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

  lemma
    assumes "A" and "B" shows "C"

rather than as

  lemma "A ==> B ==> C"

Now, e.g.,

  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 rules."

cheers

chris






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