Re: [isabelle] Induction starting from 1 and beyond



Maybe this is a good point to remind us all of the very nice "induction_schema" method that comes with the function package by Alex Krauss (and the automatic "termination" methods that also come with it, like "lexicographic_order").

lemma ind_from_2 [case_names 0 1 2 many]:
  fixes P :: "nat â bool"
  assumes "P 0"
    and "P 1"
    and "P 2"
    and "âk. k â 2 â P k â P (Suc k)"
  shows "P n"
  using assms
  apply (induction_schema)
  apply (case_tac n, force, force)
  apply (lexicographic_order)
done

the 2nd line of the proof script is a bit awkward in this case, but can often be replaced by "apply (pat_completeness)" (which raises an exception on this specific example).

cheers

chris

On 03/24/2015 11:02 PM, Joachim Breitner wrote:
Dear Douglas,

Am Dienstag, den 24.03.2015, 15:37 -0500 schrieb W. Douglas Maurer:
P. S. While I was still in graduate school I co-wrote a paper
containing an inductive proof in which the inductive step, P(k-1)
implies P(k), depended on the fact that k >= 3. Therefore I needed
two basis steps, one for k = 1, which was trivial, and one for k = 2,
which my co-author supplied. How would you do something like that in
Isar?

remember that inductions schemes are just regular lemmas, so you can
always define precisely the induction rule that you need, and use that:

lemma ind_from_2[case_names 0 1 2 many]:
   assumes "P 0"
   assumes "P 1"
   assumes "P 2"
   assumes "â k. k â 2 â P k â P (Suc k)"
   shows "P n"
proof(induction n)
   case 0 thus ?case by fact
next
   case (Suc k)
   have "k = 0 â k = 1 â k â 2" by auto
   with Suc.IH assms
   show ?case by (auto simp add: numeral_eq_Suc)
qed


And later

lemma "foo n"
proof(induction n rule: ind_from_2)
case 0 show ?case...
next
case 1 show ?case...
next
case 2 show ?case...
next
case many show ?case...
qed

I find this separation of concerns makes your proofs much easier to read
and understand.


Greetings,
Joachim





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