Email Gateway (Aug 19 2022 at 16:34): Email Gateway (Aug 19 2022 at 16:34):From: Amarin Phaosawasdi <phaosaw2@illinois.edu>
Suppose I have an inductive definition "is_number n" which specifies
whether n is a number. If n is even, then n is a number. If n is odd,
then n is a number. "even n" and "odd n" are also inductive definitions.
theory MyNumber imports Main begin
inductive even :: "nat ⇒ bool" where
even0: "even 0" |
evenSS: "⟦even n⟧ ⟹ even (Suc (Suc n))"
inductive odd :: "nat ⇒ bool" where
odd1: "odd (Suc 0)" |
oddSS: "⟦odd n⟧ ⟹ odd (Suc (Suc n))"
inductive is_number :: "nat ⇒ bool" where
o: "⟦odd n⟧ ⟹ is_number n" |
e: "⟦even n⟧ ⟹ is_number n"
end
Suppose I wanted to prove that (Suc (Suc (Suc (Suc 0)))) is a number. I
could do the following.
lemma "is_number (Suc (Suc (Suc (Suc 0))))"
apply (rule e)
apply (rule evenSS)+
apply (rule even0)
done
The problem is that this proof is not "reusable" in the MyNumber theory.
If will fail if I try to prove whether 0 or any odd number is a number.
One way to have a proof that can be "reused" (at least in this case) is
to use code_pred.
code_pred is_number .
lemma "is_number (Suc (Suc (Suc (Suc 0))))"
by eval
lemma "is_number 0"
by eval
lemma "is_number (Suc (Suc (Suc 0)))"
by eval
Are there any other proof techniques other than using code_pred such
that the proofs are more "reusable"?
Thank you,
Amarin
Email Gateway (Aug 19 2022 at 16:34):From: Lawrence Paulson <lp15@cam.ac.uk>
Try one of these:
by (simp add: is_number.intros odd.intros even.intros)
by (metis is_number.intros odd.intros even.intros)
by (blast intro: is_number.intros intro!: odd.intros even.intros)
They all work with, e.g.,
lemma "is_number (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))))))))))))))))))))))))))))))))))))))))"
Larry Paulson
Email Gateway (Aug 19 2022 at 16:34):From: Wenda Li <wl302@cam.ac.uk>
Alternatively, we can prove some general lemmas:
lemma even_or_odd:"even n ∨ odd n"
apply (induct n rule:nat_less_induct)
apply (case_tac n,simp add:even0)
apply (case_tac nat,simp add:odd1)
by (metis evenSS less_Suc_eq oddSS)
lemma is_number: "is_number n" by (metis e even_or_odd o)
Then, we can have
lemma "is_number (Suc (Suc (Suc (Suc 0))))" by (rule is_number)
Wenda
Email Gateway (Aug 19 2022 at 16:35):From: Amarin Phaosawasdi <phaosaw2@illinois.edu>
Thank you.
Amarin
Last updated: Apr 24 2024 at 08:20 UTC