Re: [isabelle] apply proof method to all subgoals
On Sun, 17 Apr 2011, Alexander Katovsky wrote:
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