Email Gateway (Aug 19 2022 at 08:45): Email Gateway (Aug 19 2022 at 08:45):From: Felipe Magno de Almeida <felipe.m.almeida@gmail.com>
Hello,
I'm studying the "A Logical Approach To Discrete Math" and am trying to use
Isabelle with solving a few exercises. I am in the Induction chapter, and I'm
trying to prove:
lemma
fixes x y h :: nat
shows "\<exists>x y. 2(x::nat) + 5(y::nat) = (h::nat)+4"
Which would be the equivalent of the first exercise of the chapter which is:
P.n : (\<exists>h,k | 0 <= h /\ 0 <= k: 2h + 5k = n) for n>=4
I've searched the web for isabelle strong induction and cases, etc, I've even
tried to read the src/HOL/Tools/inductive.ML but I'm not very proficient in
ML so I really couldn't understand much. So I really have no idea on how
to proceed.
I wrote a proof in my notebook as:
Proved P.0 and proved P.1, then proved that
P.n => P.n+2
But with Isabelle I have no idea how to transpose this. The induct proof
divides in cases 0 and Suc h. So all I have is until now:
lemma
fixes x y h :: nat
shows "\<exists>x y. 2(x::nat) + 5(y::nat) = (h::nat)+4"
proof (induct h)
case 0
have "\<exists> x y. 2x + 5y = (0::nat) + 4"
apply (rule_tac x = 2 in exI)
by simp
thus ?case .
next
case (Suc n)
and from here I have no idea how to continue.
What I wanted was to:
lemma
fixes x y h :: nat
shows "\<exists>x y. 2(x::nat) + 5(y::nat) = (h::nat)+4"
proof (induct h)
case 0
have "\<exists> x y. 2x + 5y = (0::nat) + 4"
apply (rule_tac x = 2 in exI)
by simp
thus ?case .
next
case (Suc 0)
(* etc *)
thus ?case .
next
case (Suc (Suc n))
(* prove P.n ==> P (Suc (Suc n)) *)
thus ?case .
qed
Any pointers?
Thanks in advance,
Email Gateway (Aug 19 2022 at 08:45):From: Alfio Martini <alfio.martini@acm.org>
Hi Felipe,
I am not with Gries book here, but It seems that you are looking for might
be
what is often called recursion [or computation] induction.
Take a look at section 2.3.4, in the new Isabelle tutorial (here):
http://isabelle.in.tum.de/dist/Isabelle2012/doc/prog-prove.pdf
and also at section 3.5 of the traditional Isabelle tutorial here:
http://isabelle.in.tum.de/dist/Isabelle2012/doc/tutorial.pdf
Best!
Email Gateway (Aug 19 2022 at 08:45):From: René Neumann <rene.neumann@in.tum.de>
Hi,
If you don't find an induction rule that suits your needs, write one :)
lemma nat_plus2_induct [case_names Zero One SucSuc]:
assumes "P 0"
and "P (Suc 0)"
and "\<And>n. P n \<Longrightarrow> P (Suc (Suc n))"
shows "P (n::nat)"
proof (induct n rule: less_induct)
case (less x) with assms show ?case
by (cases x, simp) (metis less_Suc_eq_0_disj less_Suc_eq)
qed
lemma
fixes x y h :: nat
shows "\<exists>x y. 2(x::nat) + 5(y::nat) = (h::nat)+4"
proof (induct h rule: nat_plus2_induct)
case Zero ...
next
case One ...
next
case (SucSuc n) ...
qed
Email Gateway (Aug 19 2022 at 08:46):From: Tobias Nipkow <nipkow@in.tum.de>
Technically speaking, "strong induction" (also called "complete induction") is
exactly the induction principle less_induct, which you can use the way René has
shown. However, you do not need to derive a separate induction rule first, it
can be just as easy to use less_induct directly.
Tobias
Last updated: Apr 19 2024 at 08:19 UTC