Email Gateway (Aug 19 2022 at 07:53): Email Gateway (Aug 19 2022 at 07:53):From: John Munroe <munddr@gmail.com>
Hi,
I'm trying to prove the cardinality of the set {1,2} being greater
than 1, but I seem to be able to only prove that the cardinality is
greater than 0:
axiomatization
S :: "nat set" where
ax1 : "S = {1,2}"
lemma "card S > 0"
using ax1
by (metis card_eq_0_iff finite.emptyI finite.insertI gr0I insert_not_empty)
Now I'm trying to prove:
lemma "card S > 1"
sledgehammer
but sledgehammer can't seem to find a proof. Could someone please help?
Thanks a lot for your time.
John
Email Gateway (Aug 19 2022 at 07:53):From: Christian Sternagel <c-sterna@jaist.ac.jp>
How about
definition S :: "nat set" where
"S ≡ {1,2}"
lemma "card S > 1"
by (simp add: S_def)
The same should work with your axiomatic version (but I don't see why
you would use an axiom in this case). Just give the equation of the
axiom an explicit name and supply it to simp.
Maybe a nicer way to state S would be
context
fixes S :: "nat set"
assumes S_def: "S = {1, 2}"
begin
lemma "card S > 1"
by (simp add: S_def)
end
cheers
chris
Email Gateway (Aug 19 2022 at 07:54):From: John Munroe <munddr@gmail.com>
Thanks. Do you know why 'auto' wouldn't work even if S_def/ax1 is
already given as a fact?
John
Email Gateway (Aug 19 2022 at 07:54):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear John,
I can reproduce your problem but do not have an explanation. There is a
thread about "using" in the mailing list archives:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-February/msg00019.html
which is interesting, but does not give an explanation for your case
(since S is not polymorphic).
To make it easier for others to follow, here is the problem again:
definition S :: "nat set" where "S == {1, 2, 3}"
lemma "card S > 1" by (auto simp: S_def) (this works)
lemma "card S > 1" using S_def apply auto (leaves the goal)
cheers
chris
Email Gateway (Aug 19 2022 at 07:55):From: Tobias Nipkow <nipkow@in.tum.de>
Am 26/07/2012 04:13, schrieb Christian Sternagel:
Dear John,
I can reproduce your problem but do not have an explanation. There is a thread
about "using" in the mailing list archives:https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-February/msg00019.html
which is interesting, but does not give an explanation for your case (since S is
not polymorphic).To make it easier for others to follow, here is the problem again:
definition S :: "nat set" where "S == {1, 2, 3}"
lemma "card S > 1" by (auto simp: S_def) (this works)
lemma "card S > 1" using S_def apply auto (leaves the goal)
1. S = {Suc 0, 2, 3} ⟹ Suc 0 < card S
This is the result of a simplifier heuristic: if it finds an equation "constant
= term" among the assumptions, it turns it around. Otherwise the following
frequently happens: an equation like "0 = x" is produced in the middle of
simplification and then 0 is replaced by x everywhere - not a good idea. The
heuristic does not apply to equation that are added to the simplifier explicitly.
Tobias
cheers
chris
On 07/26/2012 10:06 AM, John Munroe wrote:
I gave it with 'using S_def'. Do you know why 'using S_def; by auto'
wouldn't work?On Thu, Jul 26, 2012 at 12:57 AM, Christian Sternagel wrote:
For me, by (auto simp: S_def) did the job. So how did you give S_def/ax1 as
fact?
Last updated: Apr 20 2024 at 12:26 UTC