# 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.
```
```
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.