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 |
Programming is just another word for the lost art of thinking.

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