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)
qed

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
qed

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
qed

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.

cheers

chris




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