Email Gateway (Aug 22 2022 at 09:34): Email Gateway (Aug 22 2022 at 09:34):From: "W. Douglas Maurer" <maurer@gwu.edu>
This seems like a really simple question, but after weeks of
searching with no success I finally have to ask the list, since my
student is waiting for the answer so he can finish his project: Where
is (P(0) and (for all (j::nat > 0) there exists i < j such that (P(i)
implies P(j)))) implies P(n) for all n? Many thanks! -WDMaurer
Email Gateway (Aug 22 2022 at 09:34):From: "Elsa L. Gunter" <egunter@illinois.edu>
I don't know if that exact theorem is embedded in in Isabelle somewhere,
but it can be derived from strong induction (aka nat_less_induct) as
follows:
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
---Elsa
Email Gateway (Aug 22 2022 at 09:34):From: Christian Sternagel <c.sternagel@gmail.com>
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
Last updated: Apr 19 2024 at 20:15 UTC