Re: [isabelle] Proof help on Cardinality and list_all2



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 at lists.cam.ac.uk [cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of Aaron W. Hsu [arcfide at sacrideo.us]
Sent: Tuesday, May 08, 2012 4:06 AM
To: cl-isabelle-users at 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

--
Aaron W. Hsu | arcfide at sacrideo.us | http://www.sacrideo.us
Programming is just another word for the lost art of thinking.







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.