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 
definition hassize (infixr "hassize" 12) where


12 
"(S hassize n) = (finite S \<and> card S = n)"


13 


14 
lemma hassize_image_inj: assumes f: "inj_on f S" and S: "S hassize n"


15 
shows "f ` S hassize n"


16 
using f S card_image[OF f]


17 
by (simp add: hassize_def inj_on_def)


18 


19 


20 
subsection {* Finite Cartesian products, with indexing and lambdas. *}


21 


22 
typedef (open Cart)


23 
('a, 'b) "^" (infixl "^" 15)


24 
= "UNIV :: ('b \<Rightarrow> 'a) set"


25 
morphisms Cart_nth Cart_lambda ..


26 


27 
notation Cart_nth (infixl "$" 90)


28 


29 
notation (xsymbols) Cart_lambda (binder "\<chi>" 10)


30 


31 
lemma stupid_ext: "(\<forall>x. f x = g x) \<longleftrightarrow> (f = g)"


32 
apply auto


33 
apply (rule ext)


34 
apply auto


35 
done


36 


37 
lemma Cart_eq: "((x:: 'a ^ 'b) = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)"


38 
by (simp add: Cart_nth_inject [symmetric] expand_fun_eq)


39 


40 
lemma Cart_lambda_beta [simp]: "Cart_lambda g $ i = g i"


41 
by (simp add: Cart_lambda_inverse)


42 


43 
lemma Cart_lambda_unique:


44 
fixes f :: "'a ^ 'b"


45 
shows "(\<forall>i. f$i = g i) \<longleftrightarrow> Cart_lambda g = f"


46 
by (auto simp add: Cart_eq)


47 


48 
lemma Cart_lambda_eta: "(\<chi> i. (g$i)) = g"


49 
by (simp add: Cart_eq)


50 


51 
text{* A nonstandard sum to "paste" Cartesian products. *}


52 


53 
definition pastecart :: "'a ^ 'm \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a ^ ('m + 'n)" where


54 
"pastecart f g = (\<chi> i. case i of Inl a \<Rightarrow> f$a  Inr b \<Rightarrow> g$b)"


55 


56 
definition fstcart:: "'a ^('m + 'n) \<Rightarrow> 'a ^ 'm" where


57 
"fstcart f = (\<chi> i. (f$(Inl i)))"


58 


59 
definition sndcart:: "'a ^('m + 'n) \<Rightarrow> 'a ^ 'n" where


60 
"sndcart f = (\<chi> i. (f$(Inr i)))"


61 


62 
lemma nth_pastecart_Inl [simp]: "pastecart f g $ Inl a = f$a"


63 
unfolding pastecart_def by simp


64 


65 
lemma nth_pastecart_Inr [simp]: "pastecart f g $ Inr b = g$b"


66 
unfolding pastecart_def by simp


67 


68 
lemma nth_fstcart [simp]: "fstcart f $ i = f $ Inl i"


69 
unfolding fstcart_def by simp


70 


71 
lemma nth_sndtcart [simp]: "sndcart f $ i = f $ Inr i"


72 
unfolding sndcart_def by simp


73 


74 
lemma finite_sum_image: "(UNIV::('a + 'b) set) = range Inl \<union> range Inr"


75 
by (auto, case_tac x, auto)


76 


77 
lemma fstcart_pastecart: "fstcart (pastecart (x::'a ^'m ) (y:: 'a ^ 'n)) = x"


78 
by (simp add: Cart_eq)


79 


80 
lemma sndcart_pastecart: "sndcart (pastecart (x::'a ^'m ) (y:: 'a ^ 'n)) = y"


81 
by (simp add: Cart_eq)


82 


83 
lemma pastecart_fst_snd: "pastecart (fstcart z) (sndcart z) = z"


84 
by (simp add: Cart_eq pastecart_def fstcart_def sndcart_def split: sum.split)


85 


86 
lemma pastecart_eq: "(x = y) \<longleftrightarrow> (fstcart x = fstcart y) \<and> (sndcart x = sndcart y)"


87 
using pastecart_fst_snd[of x] pastecart_fst_snd[of y] by metis


88 


89 
lemma forall_pastecart: "(\<forall>p. P p) \<longleftrightarrow> (\<forall>x y. P (pastecart x y))"


90 
by (metis pastecart_fst_snd fstcart_pastecart sndcart_pastecart)


91 


92 
lemma exists_pastecart: "(\<exists>p. P p) \<longleftrightarrow> (\<exists>x y. P (pastecart x y))"


93 
by (metis pastecart_fst_snd fstcart_pastecart sndcart_pastecart)


94 


95 
end
