Email Gateway (Mar 31 2024 at 15:00): Email Gateway (Mar 31 2024 at 15:00):From: "\"日月久照\"" <cl-isabelle-users@lists.cam.ac.uk>
I have revised the theory file as follows:
theory FullTheory
imports "CParser.CTranslation" AutoCorres.AutoCorres
begin
lemma diff_signed_word_is_diff_pointer[simp]:
"
a ≠ b ⟶ ((PTR_COERCE(32 signed word → 32 word) a) ≠ (PTR_COERCE(32 signed word → 32 word) b))
"
by (metis Ptr_ptr_val ptr_val_ptr_coerce)
lemma "
of_int (x + y) = of_int x + of_int y
"
apply(auto)
done
lemma can_not_eq_self:
"∀(k::word32). y * k < y ⟹ 0 < y * k ⟹ x = y * k ⟹ False"
proof (induct k)
case zero
then show ?case by auto
next
case (suc k)
then show ?case
by (metis mult.right_neutral order_less_irrefl)
qed
lemma "
(x::word32) < y∧
x > 0 ⟶
¬(y dvd x)
"
apply(auto)
apply(simp add: dvd_def)
using can_not_eq_self
apply auto
sledgehammer
But it didn’t work. The sledgehammer also can’t find any proof.
subgoal is：
proof (prove)
goal (1 subgoal):
1. ⋀k. y * k < y ⟹
0 < y * k ⟹
(⋀y k x. ∀k. y * k < y ⟹ 0 < y * k ⟹ x = y * k ⟹ False) ⟹
x = y * k ⟹ False
Thanks
------------------ 原始邮件 ------------------
发件人: "Lawrence Paulson" <lp15@cam.ac.uk>;
发送时间: 2024年3月31日(星期天) 晚上6:53
收件人: "日月久照"<riyuejiuzhao@qq.com>;"isabelle-users"<isabelle-users@cl.cam.ac.uk>;
抄送: "Stepan Holub"<cl-isabelle-users@lists.cam.ac.uk>;
主题: Re: [isabelle] Why is the subgoal still unable to be verified even when there is an existing lemma?
Here you declare can_not_eq_self as [simp], but it does not have the form of a simplification rule: in particular, it depends on conditions such as y*k<y, when those variables are not mentioned in the conclusion (which is just False). So [simp] has no useful effect. Arguably, a warning should be given in such cases.
But anyway, get rid of [simp] and try
using can_not_eq_self
apply auto
or instead simply try sledgehammer.
Larry Paulson
>
Email Gateway (Apr 04 2024 at 15:40):From: "\"日月久照\"" <cl-isabelle-users@lists.cam.ac.uk>
That works, thank you very much.
------------------ 原始邮件 ------------------
发件人: "Lawrence Paulson" <lp15@cam.ac.uk>;
发送时间: 2024年4月1日(星期一) 晚上6:17
收件人: "日月久照"<riyuejiuzhao@qq.com>;
抄送: "isabelle-users"<isabelle-users@cl.cam.ac.uk>;"Stepan Holub"<cl-isabelle-users@lists.cam.ac.uk>;
主题: Re: [isabelle] Why is the subgoal still unable to be verified even when there is an existing lemma?
Your problem is here:
> lemma can_not_eq_self:
> "∀(k::word32). y * k < y ⟹ 0 < y * k ⟹ x = y * k ⟹ False"
The scope of ∀ is local to ∀(k::word32). y * k < y, so in particular there’s no connection between the k in that formula and the other instances of k.
It works if you write your lemma like this:
lemma can_not_eq_self:
"⋀(k::word32). y * k < y ⟹ 0 < y * k ⟹ x = y * k ⟹ False"
Or equivalently and more clearly,
lemma can_not_eq_self:
fixes k::word32
assumes "y * k < y" "0 < y * k" "x = y * k"
shows "False"
Last updated: May 04 2024 at 20:16 UTC