9 begin |
9 begin |
10 |
10 |
11 subsection {* Finite Cartesian products, with indexing and lambdas. *} |
11 subsection {* Finite Cartesian products, with indexing and lambdas. *} |
12 |
12 |
13 typedef (open Cart) |
13 typedef (open Cart) |
14 ('a, 'b) "^" (infixl "^" 15) |
14 ('a, 'b) cart = "UNIV :: (('b::finite) \<Rightarrow> 'a) set" |
15 = "UNIV :: (('b::finite) \<Rightarrow> 'a) set" |
|
16 morphisms Cart_nth Cart_lambda .. |
15 morphisms Cart_nth Cart_lambda .. |
17 |
16 |
18 notation Cart_nth (infixl "$" 90) |
17 notation Cart_nth (infixl "$" 90) |
19 |
18 |
20 notation (xsymbols) Cart_lambda (binder "\<chi>" 10) |
19 notation (xsymbols) Cart_lambda (binder "\<chi>" 10) |
21 |
20 |
22 (* |
21 (* |
23 Translate "'b ^ 'n" into "'b ^ ('n :: finite)". When 'n needs more than one |
22 Translate "'b ^ 'n" into "'b ^ ('n :: finite)". When 'n has already more than |
24 type class write "cart 'b ('n::{finite, ...})" |
23 the finite type class write "cart 'b 'n" |
25 *) |
24 *) |
26 |
25 |
27 syntax "_finite_cart" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ ^/ _)" [15, 16] 15) |
26 syntax "_finite_cart" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ ^/ _)" [15, 16] 15) |
28 |
27 |
29 parse_translation {* |
28 parse_translation {* |
43 apply auto |
42 apply auto |
44 apply (rule ext) |
43 apply (rule ext) |
45 apply auto |
44 apply auto |
46 done |
45 done |
47 |
46 |
48 lemma Cart_eq: "((x:: 'a ^ 'b::finite) = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)" |
47 lemma Cart_eq: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)" |
49 by (simp add: Cart_nth_inject [symmetric] expand_fun_eq) |
48 by (simp add: Cart_nth_inject [symmetric] expand_fun_eq) |
50 |
49 |
51 lemma Cart_lambda_beta [simp]: "Cart_lambda g $ i = g i" |
50 lemma Cart_lambda_beta [simp]: "Cart_lambda g $ i = g i" |
52 by (simp add: Cart_lambda_inverse) |
51 by (simp add: Cart_lambda_inverse) |
53 |
52 |
54 lemma Cart_lambda_unique: |
53 lemma Cart_lambda_unique: "(\<forall>i. f$i = g i) \<longleftrightarrow> Cart_lambda g = f" |
55 fixes f :: "'a ^ 'b::finite" |
|
56 shows "(\<forall>i. f$i = g i) \<longleftrightarrow> Cart_lambda g = f" |
|
57 by (auto simp add: Cart_eq) |
54 by (auto simp add: Cart_eq) |
58 |
55 |
59 lemma Cart_lambda_eta: "(\<chi> i. (g$i)) = g" |
56 lemma Cart_lambda_eta: "(\<chi> i. (g$i)) = g" |
60 by (simp add: Cart_eq) |
57 by (simp add: Cart_eq) |
61 |
58 |
62 text{* A non-standard sum to "paste" Cartesian products. *} |
59 text{* A non-standard sum to "paste" Cartesian products. *} |
63 |
60 |
64 definition pastecart :: "'a ^ 'm::finite \<Rightarrow> 'a ^ 'n::finite \<Rightarrow> 'a ^ ('m + 'n)" where |
61 definition "pastecart f g = (\<chi> i. case i of Inl a \<Rightarrow> f$a | Inr b \<Rightarrow> g$b)" |
65 "pastecart f g = (\<chi> i. case i of Inl a \<Rightarrow> f$a | Inr b \<Rightarrow> g$b)" |
62 definition "fstcart f = (\<chi> i. (f$(Inl i)))" |
66 |
63 definition "sndcart f = (\<chi> i. (f$(Inr i)))" |
67 definition fstcart:: "'a ^('m::finite + 'n::finite) \<Rightarrow> 'a ^ 'm" where |
|
68 "fstcart f = (\<chi> i. (f$(Inl i)))" |
|
69 |
|
70 definition sndcart:: "'a ^('m::finite + 'n::finite) \<Rightarrow> 'a ^ 'n" where |
|
71 "sndcart f = (\<chi> i. (f$(Inr i)))" |
|
72 |
64 |
73 lemma nth_pastecart_Inl [simp]: "pastecart f g $ Inl a = f$a" |
65 lemma nth_pastecart_Inl [simp]: "pastecart f g $ Inl a = f$a" |
74 unfolding pastecart_def by simp |
66 unfolding pastecart_def by simp |
75 |
67 |
76 lemma nth_pastecart_Inr [simp]: "pastecart f g $ Inr b = g$b" |
68 lemma nth_pastecart_Inr [simp]: "pastecart f g $ Inr b = g$b" |
83 unfolding sndcart_def by simp |
75 unfolding sndcart_def by simp |
84 |
76 |
85 lemma finite_sum_image: "(UNIV::('a + 'b) set) = range Inl \<union> range Inr" |
77 lemma finite_sum_image: "(UNIV::('a + 'b) set) = range Inl \<union> range Inr" |
86 by (auto, case_tac x, auto) |
78 by (auto, case_tac x, auto) |
87 |
79 |
88 lemma fstcart_pastecart: "fstcart (pastecart (x::'a ^'m::finite ) (y:: 'a ^ 'n::finite)) = x" |
80 lemma fstcart_pastecart: "fstcart (pastecart x y) = x" |
89 by (simp add: Cart_eq) |
81 by (simp add: Cart_eq) |
90 |
82 |
91 lemma sndcart_pastecart: "sndcart (pastecart (x::'a ^'m::finite ) (y:: 'a ^ 'n::finite)) = y" |
83 lemma sndcart_pastecart: "sndcart (pastecart x y) = y" |
92 by (simp add: Cart_eq) |
84 by (simp add: Cart_eq) |
93 |
85 |
94 lemma pastecart_fst_snd: "pastecart (fstcart z) (sndcart z) = z" |
86 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) |
87 by (simp add: Cart_eq pastecart_def fstcart_def sndcart_def split: sum.split) |
96 |
88 |