author | hoelzl |
Thu, 07 Jan 2010 17:43:35 +0100 | |
changeset 34290 | 1edf0f223c6e |
parent 34289 | c9c14c72d035 |
child 34291 | 4e896680897e |
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) |
|
14 |
('a, 'b) "^" (infixl "^" 15) |
|
34289 | 15 |
= "UNIV :: (('b::finite) \<Rightarrow> 'a) set" |
33175 | 16 |
morphisms Cart_nth Cart_lambda .. |
17 |
||
18 |
notation Cart_nth (infixl "$" 90) |
|
19 |
||
20 |
notation (xsymbols) Cart_lambda (binder "\<chi>" 10) |
|
21 |
||
34290
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
22 |
(* |
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
23 |
Translate "'b ^ 'n" into "'b ^ ('n :: finite)". When 'n needs more than one |
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
24 |
type class write "cart 'b ('n::{finite, ...})" |
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 |
|
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
27 |
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
|
28 |
|
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
29 |
parse_translation {* |
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
30 |
let |
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
31 |
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
|
32 |
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
|
33 |
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
|
34 |
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
|
35 |
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
|
36 |
| 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
|
37 |
in |
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
38 |
[("_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
|
39 |
end |
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
40 |
*} |
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
41 |
|
33175 | 42 |
lemma stupid_ext: "(\<forall>x. f x = g x) \<longleftrightarrow> (f = g)" |
43 |
apply auto |
|
44 |
apply (rule ext) |
|
45 |
apply auto |
|
46 |
done |
|
47 |
||
34289 | 48 |
lemma Cart_eq: "((x:: 'a ^ 'b::finite) = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)" |
33175 | 49 |
by (simp add: Cart_nth_inject [symmetric] expand_fun_eq) |
50 |
||
51 |
lemma Cart_lambda_beta [simp]: "Cart_lambda g $ i = g i" |
|
52 |
by (simp add: Cart_lambda_inverse) |
|
53 |
||
54 |
lemma Cart_lambda_unique: |
|
34289 | 55 |
fixes f :: "'a ^ 'b::finite" |
33175 | 56 |
shows "(\<forall>i. f$i = g i) \<longleftrightarrow> Cart_lambda g = f" |
57 |
by (auto simp add: Cart_eq) |
|
58 |
||
59 |
lemma Cart_lambda_eta: "(\<chi> i. (g$i)) = g" |
|
60 |
by (simp add: Cart_eq) |
|
61 |
||
62 |
text{* A non-standard sum to "paste" Cartesian products. *} |
|
63 |
||
34289 | 64 |
definition pastecart :: "'a ^ 'm::finite \<Rightarrow> 'a ^ 'n::finite \<Rightarrow> 'a ^ ('m + 'n)" where |
33175 | 65 |
"pastecart f g = (\<chi> i. case i of Inl a \<Rightarrow> f$a | Inr b \<Rightarrow> g$b)" |
66 |
||
34289 | 67 |
definition fstcart:: "'a ^('m::finite + 'n::finite) \<Rightarrow> 'a ^ 'm" where |
33175 | 68 |
"fstcart f = (\<chi> i. (f$(Inl i)))" |
69 |
||
34289 | 70 |
definition sndcart:: "'a ^('m::finite + 'n::finite) \<Rightarrow> 'a ^ 'n" where |
33175 | 71 |
"sndcart f = (\<chi> i. (f$(Inr i)))" |
72 |
||
73 |
lemma nth_pastecart_Inl [simp]: "pastecart f g $ Inl a = f$a" |
|
74 |
unfolding pastecart_def by simp |
|
75 |
||
76 |
lemma nth_pastecart_Inr [simp]: "pastecart f g $ Inr b = g$b" |
|
77 |
unfolding pastecart_def by simp |
|
78 |
||
79 |
lemma nth_fstcart [simp]: "fstcart f $ i = f $ Inl i" |
|
80 |
unfolding fstcart_def by simp |
|
81 |
||
82 |
lemma nth_sndtcart [simp]: "sndcart f $ i = f $ Inr i" |
|
83 |
unfolding sndcart_def by simp |
|
84 |
||
85 |
lemma finite_sum_image: "(UNIV::('a + 'b) set) = range Inl \<union> range Inr" |
|
86 |
by (auto, case_tac x, auto) |
|
87 |
||
34289 | 88 |
lemma fstcart_pastecart: "fstcart (pastecart (x::'a ^'m::finite ) (y:: 'a ^ 'n::finite)) = x" |
33175 | 89 |
by (simp add: Cart_eq) |
90 |
||
34289 | 91 |
lemma sndcart_pastecart: "sndcart (pastecart (x::'a ^'m::finite ) (y:: 'a ^ 'n::finite)) = y" |
33175 | 92 |
by (simp add: Cart_eq) |
93 |
||
94 |
lemma pastecart_fst_snd: "pastecart (fstcart z) (sndcart z) = z" |
|
95 |
by (simp add: Cart_eq pastecart_def fstcart_def sndcart_def split: sum.split) |
|
96 |
||
97 |
lemma pastecart_eq: "(x = y) \<longleftrightarrow> (fstcart x = fstcart y) \<and> (sndcart x = sndcart y)" |
|
98 |
using pastecart_fst_snd[of x] pastecart_fst_snd[of y] by metis |
|
99 |
||
100 |
lemma forall_pastecart: "(\<forall>p. P p) \<longleftrightarrow> (\<forall>x y. P (pastecart x y))" |
|
101 |
by (metis pastecart_fst_snd fstcart_pastecart sndcart_pastecart) |
|
102 |
||
103 |
lemma exists_pastecart: "(\<exists>p. P p) \<longleftrightarrow> (\<exists>x y. P (pastecart x y))" |
|
104 |
by (metis pastecart_fst_snd fstcart_pastecart sndcart_pastecart) |
|
105 |
||
106 |
end |