Email Gateway (Aug 18 2022 at 10:07): Email Gateway (Aug 18 2022 at 10:07):From: John Matthews <matthews@galois.com>
I have a subgoal of the form
1. "~ (finite (UNIV :: int set))"
However, I can't find a corresponding theorem using find_theorems in
Isabelle/HOL. Nor was find_theorems produce successful on the terms
"card (UNIV :: int set)" or "setsum ?f (UNIV :: int set)".
What is the best way to prove this subgoal?
Thanks,
-john
Email Gateway (Aug 18 2022 at 10:08):From: Michael Norrish <michael.norrish@nicta.com.au>
John Matthews wrote:
I have a subgoal of the form
1. "~ (finite (UNIV :: int set))"
However, I can't find a corresponding theorem using find_theorems in
Isabelle/HOL. Nor was find_theorems produce successful on the terms
"card (UNIV :: int set)" or "setsum ?f (UNIV :: int set)".What is the best way to prove this subgoal?
Show by finite-induction that any finite non-empty set of integers has
a greatest/least element.
Michael.
Email Gateway (Aug 18 2022 at 10:11):From: Peter Gammie <peteg42@gmail.com>
On 01/02/2007, at 12:38 PM, John Matthews wrote:
I have a subgoal of the form
1. "~ (finite (UNIV :: int set))"
However, I can't find a corresponding theorem using find_theorems
in Isabelle/HOL. Nor was find_theorems produce successful on the
terms "card (UNIV :: int set)" or "setsum ?f (UNIV :: int set)".
In my humbling experience you want to avoid "card" for anything
involving (possibly) infinite sets - "card (UNIV :: nat set) = 0".
IIRC setsum only works properly for finite sets, hence this strange
property. Of course "card" has no business having "nat" as a codomain.
With Gerwin's help I cooked up a "has" library, where we can
uniformly say "this set has (at least) this many elements, and here
are the witnesses." It was cheaper than trying to talk about
cardinals. I can polish it up if anyone is interested.
What is the best way to prove this subgoal?
I'm not going to claim this is the best but it does the job in
Isabelle2005:
lemma "infinite (UNIV :: int set)"
using infinite_iff_countable_subset[symmetric] inj_int
by blast
cheers
peter
Email Gateway (Aug 18 2022 at 10:12):From: Stephan Merz <Stephan.Merz@loria.fr>
John,
this is theorem nat_infinite (or nat_not_finite) from theory Infinite_Set.
All the best,
Stephan
John Matthews wrote:
Stephan.Merz.vcf
Email Gateway (Aug 18 2022 at 10:14):From: John Matthews <matthews@galois.com>
Many thanks to all who responded to my query! I ended up with proving
these lemmas:
lemma infinite_UNIV:
"inj (f::nat => 'a) ==> infinite (UNIV::'a set)"
using range_inj_infinite finite_subset subset_UNIV
by blast
lemmas int_infinite[simp] = infinite_UNIV[OF inj_int]
-john
Last updated: May 03 2024 at 04:19 UTC