Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Elementary Isabelle/Isa question

Email Gateway (Aug 22 2022 at 18:17):

From: Christian Sternagel <c.sternagel@gmail.com>
Dear Ching Tsun,

without having had time to actual try your example in Isabelle/jEdit,
one potential issue:

On 09/03/2018 09:28 AM, Ching-Tsun Chou wrote:

Continuing with my previous example below, I add:

lemma evSS_sum: "ev (n+m) ⟹ ev (Suc (Suc (n+m)))"
proof -
assume "ev (n+m)"
then show "ev (Suc (Suc (n+m)))" by (rule ev_SS)

"ev_SS" in the line above refers to one case of the inductive definition
of "ev"

qed

theorem ev_sum: "ev n ⟹ ev m ⟹ ev (n+m)"
proof (induction rule: ev.induct)
case ev_0
then show ?case by (simp)
next
case (ev_SS n)
then have "ev (n+m)" by (auto)
then have "ev (Suc (Suc (n+m)))" by (rule ev_SS)

"ev_SS" in the line above refers to the facts that where introduced by
"case (ev_SS n)", which might be very different from the meaning in the
previous lemma.

You may want to rename the case locally, e.g., via

case A: (ev_SS n)

cheers

chris

then show ?case by (auto simp add: ev_SS)
qed

The proof of evSS_sum works. But in the proof of ev_sum, the boldfaced "by
(rule ev_SS)" fails with the following error message:

Failed to apply initial proof method⌂:
using this:
ev (n + m)
goal (1 subgoal):
1. ev (Suc (Suc (n + m)))

Why??? The proof method seems to be used in identical contexts in both
cases. Why does it work in one case but not in the other?

Thanks!
- Ching Tsun

On Sun, Sep 2, 2018 at 5:07 PM Ching-Tsun Chou <chingtsun.chou@gmail.com>
wrote:

For the life of me, I cannot figure out why the highlighted line of my
proof below does not work. It seems to me that I have proved all facts
necessary to finish the proof. What did I miss?

Many thanks in advance!
- Ching Tsun

theory JustTest
imports Main
begin

inductive ev :: "nat ⇒ bool" where
ev_0: "ev 0" |
ev_SS: "ev n ⟹ ev (Suc (Suc n))"

fun double :: "nat ⇒ nat" where
"double 0 = 0" |
"double (Suc n) = Suc (Suc (double n))"

fun evn :: "nat ⇒ bool" where
"evn 0 = True" |
"evn (Suc 0) = False" |
"evn (Suc (Suc n)) = evn n"

lemma ev_imp_evn: "ev n ⟹ evn n"
apply (induction rule: ev.induct)
apply (simp_all)
done

lemma evn_imp_ev: "evn n ⟹ ev n"
apply (induction n rule: evn.induct)
apply (simp_all add: ev_0 ev_SS)
done

theorem not_ev_1: "¬ ev (Suc 0)"
proof
assume "ev (Suc 0)"
then have "evn (Suc 0)" by (rule ev_imp_evn)
then show False by (simp)
qed

theorem not_ev_double_plus_1: "¬ ev (Suc (double n))"
proof (induction n)
case 0
then show ?case by (simp add: not_ev_1)
next
fix n assume p1: "¬ ev (Suc (double n))"
assume "ev (Suc (double (Suc n)))"
then have "evn (Suc (double (Suc n)))" by (rule ev_imp_evn)
then have "evn (Suc (double n))" by (simp)
then have p2: "ev (Suc (double n))" by (rule evn_imp_ev)
from p1 p2 show ?thesis by (blast)
qed

end

Email Gateway (Aug 22 2022 at 18:30):

From: Ching-Tsun Chou <chingtsun.chou@gmail.com>
For the life of me, I cannot figure out why the highlighted line of my
proof below does not work. It seems to me that I have proved all facts
necessary to finish the proof. What did I miss?

Many thanks in advance!

• Ching Tsun

theory JustTest
imports Main
begin

inductive ev :: "nat ⇒ bool" where
ev_0: "ev 0" |
ev_SS: "ev n ⟹ ev (Suc (Suc n))"

fun double :: "nat ⇒ nat" where
"double 0 = 0" |
"double (Suc n) = Suc (Suc (double n))"

fun evn :: "nat ⇒ bool" where
"evn 0 = True" |
"evn (Suc 0) = False" |
"evn (Suc (Suc n)) = evn n"

lemma ev_imp_evn: "ev n ⟹ evn n"
apply (induction rule: ev.induct)
apply (simp_all)
done

lemma evn_imp_ev: "evn n ⟹ ev n"
apply (induction n rule: evn.induct)
apply (simp_all add: ev_0 ev_SS)
done

theorem not_ev_1: "¬ ev (Suc 0)"
proof
assume "ev (Suc 0)"
then have "evn (Suc 0)" by (rule ev_imp_evn)
then show False by (simp)
qed

theorem not_ev_double_plus_1: "¬ ev (Suc (double n))"
proof (induction n)
case 0
then show ?case by (simp add: not_ev_1)
next
fix n assume p1: "¬ ev (Suc (double n))"
assume "ev (Suc (double (Suc n)))"
then have "evn (Suc (double (Suc n)))" by (rule ev_imp_evn)
then have "evn (Suc (double n))" by (simp)
then have p2: "ev (Suc (double n))" by (rule evn_imp_ev)
from p1 p2 show ?thesis by (blast)
qed

end

Email Gateway (Aug 22 2022 at 18:32):

From: Ching-Tsun Chou <chingtsun.chou@gmail.com>
Continuing with my previous example below, I add:

lemma evSS_sum: "ev (n+m) ⟹ ev (Suc (Suc (n+m)))"
proof -
assume "ev (n+m)"
then show "ev (Suc (Suc (n+m)))" by (rule ev_SS)
qed

theorem ev_sum: "ev n ⟹ ev m ⟹ ev (n+m)"
proof (induction rule: ev.induct)
case ev_0
then show ?case by (simp)
next
case (ev_SS n)
then have "ev (n+m)" by (auto)
then have "ev (Suc (Suc (n+m)))" by (rule ev_SS)
then show ?case by (auto simp add: ev_SS)
qed

The proof of evSS_sum works. But in the proof of ev_sum, the boldfaced "by
(rule ev_SS)" fails with the following error message:

Failed to apply initial proof method⌂:
using this:
ev (n + m)
goal (1 subgoal):

1. ev (Suc (Suc (n + m)))

Why??? The proof method seems to be used in identical contexts in both
cases. Why does it work in one case but not in the other?

Thanks!

• Ching Tsun

Last updated: Apr 26 2024 at 04:17 UTC