author  hoelzl 
Thu, 07 Jan 2010 17:43:35 +0100  
changeset 34290  1edf0f223c6e 
parent 34289  c9c14c72d035 
child 34291  4e896680897e 
permissions  rwrr 
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 nonstandard 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 