Re: [isabelle] Proof help on Cardinality and list_all2

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.

  "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]

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.


On 07/05/12 12:22, Aaron W. Hsu wrote:

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.

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