|
1 (* Title: HOL/Library/Finite_Cartesian_Product |
|
2 Author: Amine Chaieb, University of Cambridge |
|
3 *) |
|
4 |
|
5 header {* Definition of finite Cartesian product types. *} |
|
6 |
|
7 theory Finite_Cartesian_Product |
|
8 imports Main (*FIXME: ATP_Linkup is only needed for metis at a few places. We could dispense of that by changing the proofs.*) |
|
9 begin |
|
10 |
|
11 definition hassize (infixr "hassize" 12) where |
|
12 "(S hassize n) = (finite S \<and> card S = n)" |
|
13 |
|
14 lemma hassize_image_inj: assumes f: "inj_on f S" and S: "S hassize n" |
|
15 shows "f ` S hassize n" |
|
16 using f S card_image[OF f] |
|
17 by (simp add: hassize_def inj_on_def) |
|
18 |
|
19 |
|
20 subsection {* Finite Cartesian products, with indexing and lambdas. *} |
|
21 |
|
22 typedef (open Cart) |
|
23 ('a, 'b) "^" (infixl "^" 15) |
|
24 = "UNIV :: ('b \<Rightarrow> 'a) set" |
|
25 morphisms Cart_nth Cart_lambda .. |
|
26 |
|
27 notation Cart_nth (infixl "$" 90) |
|
28 |
|
29 notation (xsymbols) Cart_lambda (binder "\<chi>" 10) |
|
30 |
|
31 lemma stupid_ext: "(\<forall>x. f x = g x) \<longleftrightarrow> (f = g)" |
|
32 apply auto |
|
33 apply (rule ext) |
|
34 apply auto |
|
35 done |
|
36 |
|
37 lemma Cart_eq: "((x:: 'a ^ 'b) = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)" |
|
38 by (simp add: Cart_nth_inject [symmetric] expand_fun_eq) |
|
39 |
|
40 lemma Cart_lambda_beta [simp]: "Cart_lambda g $ i = g i" |
|
41 by (simp add: Cart_lambda_inverse) |
|
42 |
|
43 lemma Cart_lambda_unique: |
|
44 fixes f :: "'a ^ 'b" |
|
45 shows "(\<forall>i. f$i = g i) \<longleftrightarrow> Cart_lambda g = f" |
|
46 by (auto simp add: Cart_eq) |
|
47 |
|
48 lemma Cart_lambda_eta: "(\<chi> i. (g$i)) = g" |
|
49 by (simp add: Cart_eq) |
|
50 |
|
51 text{* A non-standard sum to "paste" Cartesian products. *} |
|
52 |
|
53 definition pastecart :: "'a ^ 'm \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a ^ ('m + 'n)" where |
|
54 "pastecart f g = (\<chi> i. case i of Inl a \<Rightarrow> f$a | Inr b \<Rightarrow> g$b)" |
|
55 |
|
56 definition fstcart:: "'a ^('m + 'n) \<Rightarrow> 'a ^ 'm" where |
|
57 "fstcart f = (\<chi> i. (f$(Inl i)))" |
|
58 |
|
59 definition sndcart:: "'a ^('m + 'n) \<Rightarrow> 'a ^ 'n" where |
|
60 "sndcart f = (\<chi> i. (f$(Inr i)))" |
|
61 |
|
62 lemma nth_pastecart_Inl [simp]: "pastecart f g $ Inl a = f$a" |
|
63 unfolding pastecart_def by simp |
|
64 |
|
65 lemma nth_pastecart_Inr [simp]: "pastecart f g $ Inr b = g$b" |
|
66 unfolding pastecart_def by simp |
|
67 |
|
68 lemma nth_fstcart [simp]: "fstcart f $ i = f $ Inl i" |
|
69 unfolding fstcart_def by simp |
|
70 |
|
71 lemma nth_sndtcart [simp]: "sndcart f $ i = f $ Inr i" |
|
72 unfolding sndcart_def by simp |
|
73 |
|
74 lemma finite_sum_image: "(UNIV::('a + 'b) set) = range Inl \<union> range Inr" |
|
75 by (auto, case_tac x, auto) |
|
76 |
|
77 lemma fstcart_pastecart: "fstcart (pastecart (x::'a ^'m ) (y:: 'a ^ 'n)) = x" |
|
78 by (simp add: Cart_eq) |
|
79 |
|
80 lemma sndcart_pastecart: "sndcart (pastecart (x::'a ^'m ) (y:: 'a ^ 'n)) = y" |
|
81 by (simp add: Cart_eq) |
|
82 |
|
83 lemma pastecart_fst_snd: "pastecart (fstcart z) (sndcart z) = z" |
|
84 by (simp add: Cart_eq pastecart_def fstcart_def sndcart_def split: sum.split) |
|
85 |
|
86 lemma pastecart_eq: "(x = y) \<longleftrightarrow> (fstcart x = fstcart y) \<and> (sndcart x = sndcart y)" |
|
87 using pastecart_fst_snd[of x] pastecart_fst_snd[of y] by metis |
|
88 |
|
89 lemma forall_pastecart: "(\<forall>p. P p) \<longleftrightarrow> (\<forall>x y. P (pastecart x y))" |
|
90 by (metis pastecart_fst_snd fstcart_pastecart sndcart_pastecart) |
|
91 |
|
92 lemma exists_pastecart: "(\<exists>p. P p) \<longleftrightarrow> (\<exists>x y. P (pastecart x y))" |
|
93 by (metis pastecart_fst_snd fstcart_pastecart sndcart_pastecart) |
|
94 |
|
95 end |