Email Gateway (Aug 19 2022 at 13:55): Email Gateway (Aug 19 2022 at 13:55):From: Andrei Popescu <uuomul@yahoo.com>
Greetings,
Larry wrote:
I think that "card (A \<rightarrow>\<^sub>E B) = card B ^ card A" might work
Actually, the theorem is almost there, disguised under the constant PiE---it can be proved as follows:
lemma card_Func:
assumes A: "finite (A::'a set)"
shows "card (A \<rightarrow>\<^sub>E B) = card B ^ card A"
unfolding card_PiE[OF A] setprod_constant[OF A] ..
Andrei
Email Gateway (Aug 19 2022 at 13:56):From: Gottfried Barrow <igbi@gmx.com>
Dialogue is optional, I have found, and though finite is tempting, I
have thought for a while it would not be a good first choice, since
defining and using typedefs is never a one-liner, unlike how defining
and using sets can be.
My contribution from listening and looking a little at FuncSet is this:
definition frule :: "'a set => 'b set => ('a => 'b) => ('a * 'b) set" where
"frule D C f == if (!x. x \<in> D --> f x \<in> C) then {(x,y). x
\<in> D & y = f x}
else {}"
Or maybe it's this, where these eliminate a need for a predicate I
thought I would need, with related things in the past:
definition frule2 :: "'a set => 'b set => ('a => 'b) => 'a => 'b" where
"frule2 D C f x == if (!x. x \<in> D --> f x \<in> C)
then (if x \<in> D then f x else undefined) else
undefined"
The value of listening was the
"definition-acid-test-did-you-forget-to-remember-that-HOL-is-total-cause-that-will-haunt-you-dude-if-you-do-or-did-do-that".
That test is, "the cardinality of the set of all f such that...". If the
conditions aren't built in to the definition, it seems I should fail the
test.
There are these people and culture, call them, and it, Z. They almost
always try to teach you something about the math they produce, but they
consider a 5mm mechanical pencil high tech.
There are these other people and culture, call them, and it, H. They're
high tech when it comes to math, but they teach you nothing about the
math they produce, the last phrase being only a slight exaggeration.
There being a certain amount of animosity between Z and H, I figure if I
offend them equally then the sum total of my offenses will be zero.
When I have to teach myself, it's can be easier to go on tangents, and
even try to build things from the ground up.
I could enlighten some users, from some info I have, about why it's
normal for nitpick to find counterexamples when things are
underspecificed, but I'll do that and ask some more question about that
some other day. There's one of those below in relation to card.
Feel free to jump on my frule and frule2 and work the details out.
Regards,
GB
(******************)
(Src_0*****************)
definition frule :: "'a set => 'b set => ('a => 'b) => ('a * 'b) set" where
"frule D C f == if (!x. x \<in> D --> f x \<in> C) then {(x,y). x
\<in> D & y = f x}
else {}"
abbreviation (input) fruleA :: "('a => 'b) => 'a set => 'b set => ('a *
'b) set"
where "fruleA f D C == frule D C f"
notation (input)
fruleA ("'(_|_=>_')")
lemma "(x,y) \<in> (f|D => C) ==> y = f x"
by(simp add: frule_def, metis (lifting, full_types)
all_not_in_conv mem_Collect_eq splitD)
lemma temp01: "{A. EX f. A = (f|{0::nat} => {0::nat})} = {{(0,0)},{}}"
by(auto simp add: frule_def)
lemma "card{A. EX f. A = (f|{0::nat} => {0::nat})} = 2"
(nitpick finds a counterexample. Underspecified goin ons somewhere.)
by(simp only: temp01, auto)
abbreviation (input) fruleF :: "('a => 'b) => 'a set => 'b set => 'a => 'b"
where "fruleF f D C x == f x"
notation (input)
fruleF ("'(_|_=>_')[_]")
lemma "(id|D => C)[x] = x &
x \<in> D --> (x, (id|D => D)[x]) \<in> (id|D => D)"
by(simp add: frule_def)
(******************)
(Src_1*****************)
definition frule2 :: "'a set => 'b set => ('a => 'b) => 'a => 'b" where
"frule2 D C f x == if (!x. x \<in> D --> f x \<in> C)
then (if x \<in> D then f x else undefined) else
undefined"
abbreviation (input) frule2Map :: "('a => 'b) => 'a set => 'b set => 'a
=> 'b"
where "frule2Map f D C == frule2 D C f"
notation (input)
frule2Map ("'(_|_=>_')")
lemma
"x \<in> D ==> (id|D => D)(x) = x"
"EX z. z \<in> D & f z ~: C ==> (f|D => C)(x) = undefined"
by(auto simp add: frule2_def)
abbreviation (input) frule2Set :: "('a => 'b) => 'a set => 'b set => ('a
lemma "x \<in> D ==> (x, (id|D => D)(x)) \<in> {id|D => D}"
by(auto simp add: frule2_def)
Email Gateway (Aug 19 2022 at 13:58):From: Josh Tilles <merelyapseudonym@gmail.com>
Does anyone have any recommendations for how to go about solving a problem like “How many functions are there between a set of three elements and a set of two elements”? (I’ve attached a page from Lawvere & Schanuel’s “Conceptual Mathematics”, the source of this exercise, in case the extra context is helpful in answering my question)
I’ve found three different ways of phrasing the exercise in Isabelle/HOL:
theory Article_I
imports Main "~~/src/HOL/Library/FuncSet"
begin
datatype person = John | Mary | Sam
datatype food = coffee | eggs
lemma "card (UNIV :: (person ⇒ food) set) = 8"
oops
lemma
assumes "card A = 3" and "card B = 2"
shows "card {F. ∀a∈A. ∃!b∈B. (a,b) ∈ F} = 8"
(* quickcheck finds a counterexample. I don't know what to make of that... *)
oops
lemma
assumes "card A = 3" and "card B = 2"
shows "card (A → B) = 8"
oops
Are there different, better approaches that I should know about? Is one of the methods a known anti-pattern? I’d appreciate any thoughts.
--Josh
signature.asc
Email Gateway (Aug 19 2022 at 13:59):From: Lawrence Paulson <lp15@cam.ac.uk>
I suggest proving the general case
"card (A → B) = card B ^ card A”
(where A and B are both finite) by induction on A.
Your second lemma fails because F could contain junk elements outside A.
Larry Paulson
Email Gateway (Aug 19 2022 at 13:59):From: Johannes Hölzl <hoelzl@in.tum.de>
Hi Josh,
what you want is card_PiE:
lemma card_PiE:
"finite S ⟹ card (PIE i : S. T i) = (∏ i∈S. card (T i))"
Where (PIE i : S. T i) is the set of all functions f with
(I) f i : T i for all i : S, and
(II) f i = undefined for i ~: S.
This is necessary in HOL, as the functions are always total.
This is proved by induction over S, see ~~/src/HOL/Library/FuncSet.
You might wonder why there is no assumption "finite (T i)". In this case
both sides of the equation are 0, as card S = 0 for an infinite S.
It should be easy to prove "(PIE i : S. T i :: (person ⇒ food) set) =
UNIV".
Greetings,
Johannes
Email Gateway (Aug 19 2022 at 14:00):From: Josh Tilles <merelyapseudonym@gmail.com>
I had expected that proving some particular cases first would be easier, but I’ll give what you recommend a shot.
Thanks!
signature.asc
Email Gateway (Aug 19 2022 at 14:01):From: Josh Tilles <merelyapseudonym@gmail.com>
Huh. Auto-Quickcheck also finds a counterexample for:
lemma
assumes "finite A" and "finite B"
shows "card (A → B) = (card B) ^ (card A)”
Apparently when A and B are both empty, there are four members to the set “A → B”. That doesn’t make any sense to me, but I haven’t spent a lot of time with the implementation of FuncSet yet.
signature.asc
Email Gateway (Aug 19 2022 at 14:02):From: Tobias Nipkow <nipkow@in.tum.de>
Well, Larry's suggestion runs into the same problem as your original attempts:
functions that behave the same on A may still differ outside A. You need to
restrict A -> B to those functions that map values outside A to some fixed
value. The theory offers function "restrict" for that purpose, but the theorem
doesn't look quite as nice anymore. I guess it is something like
... ==> card {g. EX f : A → B. g = restrict f A} = card B ^ card A
Tobias
Email Gateway (Aug 19 2022 at 14:03):From: Elsa L Gunter <egunter@illinois.edu>
I have know AUto-Quickcheck to "find" counterexamples that weren't.
Set-theoretically, there is exactly one function from the empty set to
anything, namely the empty function (represented by the empty set).
There cannot be any other, for it would have to have a pair in its
representation and that pair would have to have a first element that was
in the empty set.
---Elsa
Email Gateway (Aug 19 2022 at 14:04):From: Lawrence Paulson <lp15@cam.ac.uk>
I think that
"card ((A → B) ∩ extensional A) = (card B) ^ (card A)”
might work, but the proof looks non-trivial.
Larry Paulson
Email Gateway (Aug 19 2022 at 14:05):From: Gottfried Barrow <igbi@gmx.com>
After reading the other replies, and looking at FuncSet.thy, it gives me
an appreciation for the finite type class.
The type class finite and UNIV are a standard part of HOL, but I
haven't found much magic when it comes to card UNIV, so maybe you'll
take the route I show below, and create some magic, and post it.
Using finite and UNIV, the following seems like it should work,
based on Larry's initial suggestion:
lemma "card(UNIV::('a => 'b) set) = card(UNIV::'b::finite set) ^
card(UNIV::'a::finite set)"
Maybe I have fundamental misunderstanding of what card(UNIV::'a::finite
set) is, but nitpick gives a counterexample. However, I'm guessing
that's okay, since there could be some underspecified things involved.
I can't even prove a simple example like this:
datatype dataT = OneT | TwoT | ThreeT
lemma dataT_set: "(UNIV::dataT set) = {OneT, TwoT, ThreeT}"
by(auto, metis dataT.exhaust)
lemma dataT_card: "card (UNIV::dataT set) = 3"
by(simp add: dataT_set)
lemma dataT_27: "card(UNIV::dataT set) ^ card(UNIV::dataT set) = 27"
by(simp add: dataT_card)
lemma "card(UNIV::(dataT => dataT) set) = 27"
oops
I've only briefly looked at Finite_Set.thy, but it seems to me the
solution could be in defining a bijective function to use, from
UNIV::'a::finite set to nat, something like this:
definition ftype2nat :: "'a::finite => nat" where
"ftype2nat = (SOME f. EX n. f ` (UNIV::'a::finite set) = {i. i < n}
& bij_betw f (UNIV::'a::finite set) {i. i < n})"
You then have a set, {i. i < n}, and the cardinality of that set is the
cardinality of UNIV::'a::finite set, and another {i. i < n} for
card(UNIV::'b::finite set). With a lot of work that might give you the
right numbers.
I guess it would need to be shown that some f = ftype2nat exists. I do
the easy part, and show the injective part:
lemma injective_f_UNIV_to_nset_exists:
"EX(n::nat) f. {i. i < n} = f (UNIV::'a::finite set) & inj_on f UNIV"
proof-
have "EX(n::nat) f. (UNIV::'a::finite set) = f {i. i < n} & inj_on f
{i. i < n}"
proof-
have "finite (UNIV::'a::finite set)" by(metis finite_code)
thus ?thesis by(simp add: finite_imp_nat_seg_image_inj_on) qed
thus ?thesis
by(metis inj_on_the_inv_into the_inv_into_onto)
qed
It seems like proving "card(UNIV::(dataT => dataT) set) = 27" should be
easy. Everything might be all there in Fun.thy and Finite_Set.thy. I'd
like to know.
Regards,
GB
Last updated: Apr 26 2024 at 20:16 UTC