Email Gateway (Aug 18 2022 at 19:40): Email Gateway (Aug 18 2022 at 19:40):From: "Aaron W. Hsu" <arcfide@sacrideo.us>
Thank you for your explanation. I am still going through things, but
this thread has been most educational.
Email Gateway (Aug 18 2022 at 20:04):From: "Aaron W. Hsu" <arcfide@sacrideo.us>
Hello:
I have been trying to see if there is a straightforward way to prove the
following in Isabelle:
card {x. list_all2 op < x (a # s)} = a * card {x. list_all2 op < x s}
Specifically, I suspect that this must have come up somewhere before, and
I seet some statements that might be related in the various built-in
theories, but I am so new to Isabelle that I am having trouble putting
them together into a simple proof. I would appreciate any help on the
nicest way to go about this proof.
Email Gateway (Aug 18 2022 at 20:05):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
Probably nothing exactly like this has come up before. There is a
relevant fact, list_all2_Cons2, which you can find by searching for
"list_all2 _ _ (_ # _)" with the find_theorems facility.
I can prove your equality by showing your set construction analogous to
a cartesian product.
lemma
"card {x. list_all2 op < x (a # s)} = a * card {x. list_all2 op < x s}"
proof -
have eq_cart: "{x. list_all2 op < x (a # s)}
= (%(x, y). x # y) ` ({..< a} <*> {x. list_all2 op < x s})"
by (auto simp: list_all2_Cons2)
have inj: "inj (%(x, y). x # y)"
by (auto intro: inj_onI)
show ?thesis
by (simp add: eq_cart card_image subset_inj_on[OF inj]
card_cartesian_product)
qed
I wonder if there is a simpler proof.
Constructing terms using simple operators like image () and cartesian
product (<*>) tends to make life easier in Isabelle, since it is clear
what combinations of operators to search for rules about. Searching for
"card (_ <*> _)" locates card_cartesian_product and "card (_ _)"
yields card_image, etc.
Yours,
Thomas.
Email Gateway (Aug 18 2022 at 20:05):From: "Aaron W. Hsu" <arcfide@sacrideo.us>
Hello Thomas:
Thank you for the detailed response...
On Mon, 07 May 2012 14:21:16 +1000, Thomas Sewell wrote:
Probably nothing exactly like this has come up before. There is a
relevant fact, list_all2_Cons2, which you can find by searching for
"list_all2 _ _ (_ # _)" with the find_theorems facility.
Thank you for reminding me! I had forgotten about the find_theorems
facility, or maybe I thought that was a Proof General specific feature. I
just tested it and it works fine in Isabelle/jEdit, so I am happy.
lemma
"card {x. list_all2 op < x (a # s)} = a * card {x. list_all2 op < x
s}"
proof -
have eq_cart: "{x. list_all2 op < x (a # s)}
= (%(x, y). x # y) ` ({..< a} <*> {x. list_all2 op < x s})"
by (auto simp: list_all2_Cons2)
The above I understand...
have inj: "inj (%(x, y). x # y)"
by (auto intro: inj_onI)
This is proving injectivity, but I do not understand the use of intro. I
have mostly used auto and simp up to this point in my experience with
Isabelle. I shall have to read up on that.
show ?thesis
by (simp add: eq_cart card_image subset_inj_on[OF inj]
card_cartesian_product)
qed
What is the OF here? I understand the other elements, but what does the
subset_inj_on[OF inj] part do?
Thank you again for your assistance.
Yours truly,
Aaron W. Hsu
Email Gateway (Aug 18 2022 at 20:05):From: Lars Noschinski <noschinl@in.tum.de>
A[OF B] discharges the first premise of A with B.
-- Lars
Email Gateway (Aug 18 2022 at 20:06):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
Apologies about the dense proofs. If you know how the various tactics
work you can give them hints about how to use rules, which may speed
them up enormously. I now do this by habit.
This may not be best practice for proofs anyone wants to read.
Anyway, feel free to look up the various classical annotations (intro:
inj_on does the same thing as declare inj_on[intro] locally). The
attributes OF, rotated and THEN can be quite useful, and on rare
occasions the attributes where and simplified can help. See the
documentation, I guess.
The point of the OF was that card_image needs the function to be
injective only on the relevant set, but to save typing, I proved it
fully injective (an abbreviation for inj_on f UNIV). The subset_inj_on
rule connects these facts. An alternative would be to prove "ALL S.
inj_on f S".
The reason I didn't just give subset_inj_on and inj to the simplifier is
that I was concerned it might use subset_inj_on again to solve its own
argument and thus go on vacation. The OF construction mandates that the
rules be used together in a particular way.
As for finding a simpler proof:
lemma
"card {x. list_all2 op < x (a # s)} = a * card {x. list_all2 op < x s}"
proof -
have eq_cart: "{x. list_all2 op < x (a # s)}
= (%(x, y). x # y) ` ({..< a} <*> {x. list_all2 op < x s})"
by (auto simp: list_all2_Cons2)
thus ?thesis
by (simp add: card_image inj_on_def card_cartesian_product)
qed
The injective bit was trivial, for appropriate definitions of triviality.
Yours,
Thomas.
From: cl-isabelle-users-bounces@lists.cam.ac.uk
[cl-isabelle-users-bounces@lists.cam.ac.uk] On Behalf Of Aaron W. Hsu
[arcfide@sacrideo.us]
Sent: Tuesday, May 08, 2012 4:06 AM
To: cl-isabelle-users@lists.cam.ac.uk
Subject: Re: [isabelle] Proof help on Cardinality and list_all2
Hello Thomas:
Thank you for the detailed response...
On Mon, 07 May 2012 14:21:16 +1000, Thomas Sewell wrote:
Probably nothing exactly like this has come up before. There is a
relevant fact, list_all2_Cons2, which you can find by searching for
"list_all2 _ _ (_ # _)" with the find_theorems facility.
Thank you for reminding me! I had forgotten about the find_theorems
facility, or maybe I thought that was a Proof General specific feature. I
just tested it and it works fine in Isabelle/jEdit, so I am happy.
lemma
"card {x. list_all2 op < x (a # s)} = a * card {x. list_all2 op < x
s}"
proof -
have eq_cart: "{x. list_all2 op < x (a # s)}
= (%(x, y). x # y) ` ({..< a} <*> {x. list_all2 op < x s})"
by (auto simp: list_all2_Cons2)
The above I understand...
have inj: "inj (%(x, y). x # y)"
by (auto intro: inj_onI)
This is proving injectivity, but I do not understand the use of intro. I
have mostly used auto and simp up to this point in my experience with
Isabelle. I shall have to read up on that.
show ?thesis
by (simp add: eq_cart card_image subset_inj_on[OF inj]
card_cartesian_product)
qed
What is the OF here? I understand the other elements, but what does the
subset_inj_on[OF inj] part do?
Thank you again for your assistance.
Yours truly,
Aaron W. Hsu
Last updated: Apr 24 2024 at 08:20 UTC