Re: [isabelle] apply proof method to all subgoals

On Sun, 17 Apr 2011, Alexander Katovsky wrote:

How about

  lemma "\<forall> z . ((A (n :: nat) z) \<and> (B n z)) \<longrightarrow> C z"
  proof(induct n, intro allI conjI impI)

It seems `intro` is not attacking the second induction goal. `safe` works here, but in other cases (with particular forms for A B and C) it does more than I want it to.

The proof methods "intro" and "elim" stem from a very ancient phase of Isar (around 1998/1999) when certain key points about structured proofs where not yet undestood.

Instead of iterative decomposition of standard connectives, proofs can be done more directly by stating propositions in the intended way. The "induct" method can work with such rule structure directly. For example:

  fix z :: 'a and n :: nat
  have "A n z ==> B n z ==> C z"
  proof (induct n)

No "intro" boilerplate is needed here.


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