|
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)
|
|
|
15 |
= "UNIV :: ('b \<Rightarrow> 'a) set"
|
|
|
16 |
morphisms Cart_nth Cart_lambda ..
|
|
|
17 |
|
|
|
18 |
notation Cart_nth (infixl "$" 90)
|
|
|
19 |
|
|
|
20 |
notation (xsymbols) Cart_lambda (binder "\<chi>" 10)
|
|
|
21 |
|
|
|
22 |
lemma stupid_ext: "(\<forall>x. f x = g x) \<longleftrightarrow> (f = g)"
|
|
|
23 |
apply auto
|
|
|
24 |
apply (rule ext)
|
|
|
25 |
apply auto
|
|
|
26 |
done
|
|
|
27 |
|
|
|
28 |
lemma Cart_eq: "((x:: 'a ^ 'b) = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)"
|
|
|
29 |
by (simp add: Cart_nth_inject [symmetric] expand_fun_eq)
|
|
|
30 |
|
|
|
31 |
lemma Cart_lambda_beta [simp]: "Cart_lambda g $ i = g i"
|
|
|
32 |
by (simp add: Cart_lambda_inverse)
|
|
|
33 |
|
|
|
34 |
lemma Cart_lambda_unique:
|
|
|
35 |
fixes f :: "'a ^ 'b"
|
|
|
36 |
shows "(\<forall>i. f$i = g i) \<longleftrightarrow> Cart_lambda g = f"
|
|
|
37 |
by (auto simp add: Cart_eq)
|
|
|
38 |
|
|
|
39 |
lemma Cart_lambda_eta: "(\<chi> i. (g$i)) = g"
|
|
|
40 |
by (simp add: Cart_eq)
|
|
|
41 |
|
|
|
42 |
text{* A non-standard sum to "paste" Cartesian products. *}
|
|
|
43 |
|
|
|
44 |
definition pastecart :: "'a ^ 'm \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a ^ ('m + 'n)" where
|
|
|
45 |
"pastecart f g = (\<chi> i. case i of Inl a \<Rightarrow> f$a | Inr b \<Rightarrow> g$b)"
|
|
|
46 |
|
|
|
47 |
definition fstcart:: "'a ^('m + 'n) \<Rightarrow> 'a ^ 'm" where
|
|
|
48 |
"fstcart f = (\<chi> i. (f$(Inl i)))"
|
|
|
49 |
|
|
|
50 |
definition sndcart:: "'a ^('m + 'n) \<Rightarrow> 'a ^ 'n" where
|
|
|
51 |
"sndcart f = (\<chi> i. (f$(Inr i)))"
|
|
|
52 |
|
|
|
53 |
lemma nth_pastecart_Inl [simp]: "pastecart f g $ Inl a = f$a"
|
|
|
54 |
unfolding pastecart_def by simp
|
|
|
55 |
|
|
|
56 |
lemma nth_pastecart_Inr [simp]: "pastecart f g $ Inr b = g$b"
|
|
|
57 |
unfolding pastecart_def by simp
|
|
|
58 |
|
|
|
59 |
lemma nth_fstcart [simp]: "fstcart f $ i = f $ Inl i"
|
|
|
60 |
unfolding fstcart_def by simp
|
|
|
61 |
|
|
|
62 |
lemma nth_sndtcart [simp]: "sndcart f $ i = f $ Inr i"
|
|
|
63 |
unfolding sndcart_def by simp
|
|
|
64 |
|
|
|
65 |
lemma finite_sum_image: "(UNIV::('a + 'b) set) = range Inl \<union> range Inr"
|
|
|
66 |
by (auto, case_tac x, auto)
|
|
|
67 |
|
|
|
68 |
lemma fstcart_pastecart: "fstcart (pastecart (x::'a ^'m ) (y:: 'a ^ 'n)) = x"
|
|
|
69 |
by (simp add: Cart_eq)
|
|
|
70 |
|
|
|
71 |
lemma sndcart_pastecart: "sndcart (pastecart (x::'a ^'m ) (y:: 'a ^ 'n)) = y"
|
|
|
72 |
by (simp add: Cart_eq)
|
|
|
73 |
|
|
|
74 |
lemma pastecart_fst_snd: "pastecart (fstcart z) (sndcart z) = z"
|
|
|
75 |
by (simp add: Cart_eq pastecart_def fstcart_def sndcart_def split: sum.split)
|
|
|
76 |
|
|
|
77 |
lemma pastecart_eq: "(x = y) \<longleftrightarrow> (fstcart x = fstcart y) \<and> (sndcart x = sndcart y)"
|
|
|
78 |
using pastecart_fst_snd[of x] pastecart_fst_snd[of y] by metis
|
|
|
79 |
|
|
|
80 |
lemma forall_pastecart: "(\<forall>p. P p) \<longleftrightarrow> (\<forall>x y. P (pastecart x y))"
|
|
|
81 |
by (metis pastecart_fst_snd fstcart_pastecart sndcart_pastecart)
|
|
|
82 |
|
|
|
83 |
lemma exists_pastecart: "(\<exists>p. P p) \<longleftrightarrow> (\<exists>x y. P (pastecart x y))"
|
|
|
84 |
by (metis pastecart_fst_snd fstcart_pastecart sndcart_pastecart)
|
|
|
85 |
|
|
|
86 |
end
|