Re: [isabelle] An induction rule

On 04/03/2015 06:04 AM, Elsa L. Gunter wrote:
lemma strange_induct[rule_format]: "(P (0::nat)) â (â j > 0. â i < j. P
i â P j) â P n"
proof (induct rule: nat_less_induct, auto)
  fix n
  assume A:" âm<n. P m" and B: "P 0" and C: " âj>0ânat. âi<j. P i â P j"
  from A and B and C
  show "P n"
  by (case_tac "n = 0", auto)

Just for the record, it is bad style to start a proof with an automatic method ("proof (..., auto)" above), since basically the resulting subgoals can change at the whim of whoever is maintaining the theories your own development is based on.

This can often be avoided by phrasing the lemma statement more "Isarish", e.g.,

lemma strange_induct:
  assumes "P (0::nat)"
    and "âj > 0. âi < j. P i â P j"
  shows "P n"
proof (induct rule: nat_less_induct)
  fix n
  assume " âm < n. P m"
  with assms show "P n" by (cases n) auto

Another possibility is to use a combination of raw proof blocks and a final application of an automatic method:

lemma strange_induct' [rule_format]:
  "P (0::nat) â (â j > 0. â i < j. P i â P j) â P n"
proof -
    fix n
    assume "âm < n. P m" and "P 0" and " â j > 0. â i < j. P i â P j"
    then have "P n" by (cases "n = 0") auto
  then show ?thesis
    by (induct rule: nat_less_induct) blast

In that way you can just state what you *want* (as opposed to what you *have* to state according to the current subgoal) and rely on automatic tools to make sure that this corresponds to the current subgoal.



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