Email Gateway (Aug 18 2022 at 10:09): Email Gateway (Aug 18 2022 at 10:09):From: Christian Urban <urbanc@in.tum.de>
John Matthews writes:
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?
Hi John,
I think the best way is to use the facts that there is an
injection from nats to ints and that there are infinitely
many nats. My proof would go as follows
theory Test
imports "Infinite_Set"
begin
lemma infinite_int:
shows "infinite (UNIV::int set)"
proof -
have "inj int" by (rule inj_int)
then have "infinite (range int)" by (rule range_inj_infinite)
moreover
have "range int \<subseteq> (UNIV::int set)" by simp
ultimately show "infinite (UNIV::int set)" by (simp add: infinite_super)
qed
end
This is what you are looking for as "infinite" is defined as
"not finite".
Hope this helps,
Christian
Last updated: May 03 2024 at 12:27 UTC