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:

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

No "intro" boilerplate is needed here.


	Makarius





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