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)

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



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

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

And later

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

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


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