Email Gateway (Mar 29 2024 at 11:18): Email Gateway (Mar 29 2024 at 11:18):From: "\"DongZe Su\"" <cl-isabelle-users@lists.cam.ac.uk>
We now have lemma,
lemma can_not_eq_self[simp]:"∀(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
and I wish to prove lemma:
lemma "
(x::word32) < y∧
x > 0 ⟶
¬(y dvd x)
"
apply(auto)
apply(simp add: dvd_def)
apply(auto)
The subgoal is
proof (prove)
goal (1 subgoal):
why can’t it be verified using auto?
Email Gateway (Mar 31 2024 at 10:54):From: Lawrence Paulson <lp15@cam.ac.uk>
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 01 2024 at 10:17):From: Lawrence Paulson <lp15@cam.ac.uk>
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 05 2024 at 04:19 UTC