author | hoelzl |
Mon, 25 Jan 2010 16:56:24 +0100 | |
changeset 34964 | 4e8be3c04d37 |
parent 34291 | 4e896680897e |
child 35113 | 1a0c129bb2e0 |
permissions | -rw-r--r-- |
33175 | 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 |
subsection {* Finite Cartesian products, with indexing and lambdas. *} |
|
12 |
||
13 |
typedef (open Cart) |
|
34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34290
diff
changeset
|
14 |
('a, 'b) cart = "UNIV :: (('b::finite) \<Rightarrow> 'a) set" |
33175 | 15 |
morphisms Cart_nth Cart_lambda .. |
16 |
||
17 |
notation Cart_nth (infixl "$" 90) |
|
18 |
||
19 |
notation (xsymbols) Cart_lambda (binder "\<chi>" 10) |
|
20 |
||
34290
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
21 |
(* |
34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34290
diff
changeset
|
22 |
Translate "'b ^ 'n" into "'b ^ ('n :: finite)". When 'n has already more than |
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34290
diff
changeset
|
23 |
the finite type class write "cart 'b 'n" |
34290
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
24 |
*) |
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
25 |
|
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
26 |
syntax "_finite_cart" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ ^/ _)" [15, 16] 15) |
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
27 |
|
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
28 |
parse_translation {* |
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
29 |
let |
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
30 |
fun cart t u = Syntax.const @{type_name cart} $ t $ u |
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
31 |
fun finite_cart_tr [t, u as Free (x, _)] = |
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
32 |
if Syntax.is_tid x |
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
33 |
then cart t (Syntax.const "_ofsort" $ u $ Syntax.const (hd @{sort finite})) |
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
34 |
else cart t u |
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
35 |
| finite_cart_tr [t, u] = cart t u |
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
36 |
in |
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
37 |
[("_finite_cart", finite_cart_tr)] |
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
38 |
end |
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
39 |
*} |
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
40 |
|
33175 | 41 |
lemma stupid_ext: "(\<forall>x. f x = g x) \<longleftrightarrow> (f = g)" |
42 |
apply auto |
|
43 |
apply (rule ext) |
|
44 |
apply auto |
|
45 |
done |
|
46 |
||
34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34290
diff
changeset
|
47 |
lemma Cart_eq: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)" |
33175 | 48 |
by (simp add: Cart_nth_inject [symmetric] expand_fun_eq) |
49 |
||
50 |
lemma Cart_lambda_beta [simp]: "Cart_lambda g $ i = g i" |
|
51 |
by (simp add: Cart_lambda_inverse) |
|
52 |
||
34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34290
diff
changeset
|
53 |
lemma Cart_lambda_unique: "(\<forall>i. f$i = g i) \<longleftrightarrow> Cart_lambda g = f" |
33175 | 54 |
by (auto simp add: Cart_eq) |
55 |
||
56 |
lemma Cart_lambda_eta: "(\<chi> i. (g$i)) = g" |
|
57 |
by (simp add: Cart_eq) |
|
58 |
||
59 |
text{* A non-standard sum to "paste" Cartesian products. *} |
|
60 |
||
34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34290
diff
changeset
|
61 |
definition "pastecart f g = (\<chi> i. case i of Inl a \<Rightarrow> f$a | Inr b \<Rightarrow> g$b)" |
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34290
diff
changeset
|
62 |
definition "fstcart f = (\<chi> i. (f$(Inl i)))" |
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34290
diff
changeset
|
63 |
definition "sndcart f = (\<chi> i. (f$(Inr i)))" |
33175 | 64 |
|
65 |
lemma nth_pastecart_Inl [simp]: "pastecart f g $ Inl a = f$a" |
|
66 |
unfolding pastecart_def by simp |
|
67 |
||
68 |
lemma nth_pastecart_Inr [simp]: "pastecart f g $ Inr b = g$b" |
|
69 |
unfolding pastecart_def by simp |
|
70 |
||
71 |
lemma nth_fstcart [simp]: "fstcart f $ i = f $ Inl i" |
|
72 |
unfolding fstcart_def by simp |
|
73 |
||
74 |
lemma nth_sndtcart [simp]: "sndcart f $ i = f $ Inr i" |
|
75 |
unfolding sndcart_def by simp |
|
76 |
||
77 |
lemma finite_sum_image: "(UNIV::('a + 'b) set) = range Inl \<union> range Inr" |
|
78 |
by (auto, case_tac x, auto) |
|
79 |
||
34964 | 80 |
lemma fstcart_pastecart[simp]: "fstcart (pastecart x y) = x" |
33175 | 81 |
by (simp add: Cart_eq) |
82 |
||
34964 | 83 |
lemma sndcart_pastecart[simp]: "sndcart (pastecart x y) = y" |
33175 | 84 |
by (simp add: Cart_eq) |
85 |
||
34964 | 86 |
lemma pastecart_fst_snd[simp]: "pastecart (fstcart z) (sndcart z) = z" |
33175 | 87 |
by (simp add: Cart_eq pastecart_def fstcart_def sndcart_def split: sum.split) |
88 |
||
89 |
lemma pastecart_eq: "(x = y) \<longleftrightarrow> (fstcart x = fstcart y) \<and> (sndcart x = sndcart y)" |
|
90 |
using pastecart_fst_snd[of x] pastecart_fst_snd[of y] by metis |
|
91 |
||
92 |
lemma forall_pastecart: "(\<forall>p. P p) \<longleftrightarrow> (\<forall>x y. P (pastecart x y))" |
|
93 |
by (metis pastecart_fst_snd fstcart_pastecart sndcart_pastecart) |
|
94 |
||
95 |
lemma exists_pastecart: "(\<exists>p. P p) \<longleftrightarrow> (\<exists>x y. P (pastecart x y))" |
|
96 |
by (metis pastecart_fst_snd fstcart_pastecart sndcart_pastecart) |
|
97 |
||
98 |
end |