author | himmelma |
Fri, 23 Oct 2009 13:23:18 +0200 | |
changeset 33175 | 2083bde13ce1 |
child 33712 | 8cce3a34c122 |
permissions | -rw-r--r-- |
himmelma@33175 | 1 |
(* Title: HOL/Library/Finite_Cartesian_Product |
himmelma@33175 | 2 |
Author: Amine Chaieb, University of Cambridge |
himmelma@33175 | 3 |
*) |
himmelma@33175 | 4 |
|
himmelma@33175 | 5 |
header {* Definition of finite Cartesian product types. *} |
himmelma@33175 | 6 |
|
himmelma@33175 | 7 |
theory Finite_Cartesian_Product |
himmelma@33175 | 8 |
imports Main (*FIXME: ATP_Linkup is only needed for metis at a few places. We could dispense of that by changing the proofs.*) |
himmelma@33175 | 9 |
begin |
himmelma@33175 | 10 |
|
himmelma@33175 | 11 |
definition hassize (infixr "hassize" 12) where |
himmelma@33175 | 12 |
"(S hassize n) = (finite S \<and> card S = n)" |
himmelma@33175 | 13 |
|
himmelma@33175 | 14 |
lemma hassize_image_inj: assumes f: "inj_on f S" and S: "S hassize n" |
himmelma@33175 | 15 |
shows "f ` S hassize n" |
himmelma@33175 | 16 |
using f S card_image[OF f] |
himmelma@33175 | 17 |
by (simp add: hassize_def inj_on_def) |
himmelma@33175 | 18 |
|
himmelma@33175 | 19 |
|
himmelma@33175 | 20 |
subsection {* Finite Cartesian products, with indexing and lambdas. *} |
himmelma@33175 | 21 |
|
himmelma@33175 | 22 |
typedef (open Cart) |
himmelma@33175 | 23 |
('a, 'b) "^" (infixl "^" 15) |
himmelma@33175 | 24 |
= "UNIV :: ('b \<Rightarrow> 'a) set" |
himmelma@33175 | 25 |
morphisms Cart_nth Cart_lambda .. |
himmelma@33175 | 26 |
|
himmelma@33175 | 27 |
notation Cart_nth (infixl "$" 90) |
himmelma@33175 | 28 |
|
himmelma@33175 | 29 |
notation (xsymbols) Cart_lambda (binder "\<chi>" 10) |
himmelma@33175 | 30 |
|
himmelma@33175 | 31 |
lemma stupid_ext: "(\<forall>x. f x = g x) \<longleftrightarrow> (f = g)" |
himmelma@33175 | 32 |
apply auto |
himmelma@33175 | 33 |
apply (rule ext) |
himmelma@33175 | 34 |
apply auto |
himmelma@33175 | 35 |
done |
himmelma@33175 | 36 |
|
himmelma@33175 | 37 |
lemma Cart_eq: "((x:: 'a ^ 'b) = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)" |
himmelma@33175 | 38 |
by (simp add: Cart_nth_inject [symmetric] expand_fun_eq) |
himmelma@33175 | 39 |
|
himmelma@33175 | 40 |
lemma Cart_lambda_beta [simp]: "Cart_lambda g $ i = g i" |
himmelma@33175 | 41 |
by (simp add: Cart_lambda_inverse) |
himmelma@33175 | 42 |
|
himmelma@33175 | 43 |
lemma Cart_lambda_unique: |
himmelma@33175 | 44 |
fixes f :: "'a ^ 'b" |
himmelma@33175 | 45 |
shows "(\<forall>i. f$i = g i) \<longleftrightarrow> Cart_lambda g = f" |
himmelma@33175 | 46 |
by (auto simp add: Cart_eq) |
himmelma@33175 | 47 |
|
himmelma@33175 | 48 |
lemma Cart_lambda_eta: "(\<chi> i. (g$i)) = g" |
himmelma@33175 | 49 |
by (simp add: Cart_eq) |
himmelma@33175 | 50 |
|
himmelma@33175 | 51 |
text{* A non-standard sum to "paste" Cartesian products. *} |
himmelma@33175 | 52 |
|
himmelma@33175 | 53 |
definition pastecart :: "'a ^ 'm \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a ^ ('m + 'n)" where |
himmelma@33175 | 54 |
"pastecart f g = (\<chi> i. case i of Inl a \<Rightarrow> f$a | Inr b \<Rightarrow> g$b)" |
himmelma@33175 | 55 |
|
himmelma@33175 | 56 |
definition fstcart:: "'a ^('m + 'n) \<Rightarrow> 'a ^ 'm" where |
himmelma@33175 | 57 |
"fstcart f = (\<chi> i. (f$(Inl i)))" |
himmelma@33175 | 58 |
|
himmelma@33175 | 59 |
definition sndcart:: "'a ^('m + 'n) \<Rightarrow> 'a ^ 'n" where |
himmelma@33175 | 60 |
"sndcart f = (\<chi> i. (f$(Inr i)))" |
himmelma@33175 | 61 |
|
himmelma@33175 | 62 |
lemma nth_pastecart_Inl [simp]: "pastecart f g $ Inl a = f$a" |
himmelma@33175 | 63 |
unfolding pastecart_def by simp |
himmelma@33175 | 64 |
|
himmelma@33175 | 65 |
lemma nth_pastecart_Inr [simp]: "pastecart f g $ Inr b = g$b" |
himmelma@33175 | 66 |
unfolding pastecart_def by simp |
himmelma@33175 | 67 |
|
himmelma@33175 | 68 |
lemma nth_fstcart [simp]: "fstcart f $ i = f $ Inl i" |
himmelma@33175 | 69 |
unfolding fstcart_def by simp |
himmelma@33175 | 70 |
|
himmelma@33175 | 71 |
lemma nth_sndtcart [simp]: "sndcart f $ i = f $ Inr i" |
himmelma@33175 | 72 |
unfolding sndcart_def by simp |
himmelma@33175 | 73 |
|
himmelma@33175 | 74 |
lemma finite_sum_image: "(UNIV::('a + 'b) set) = range Inl \<union> range Inr" |
himmelma@33175 | 75 |
by (auto, case_tac x, auto) |
himmelma@33175 | 76 |
|
himmelma@33175 | 77 |
lemma fstcart_pastecart: "fstcart (pastecart (x::'a ^'m ) (y:: 'a ^ 'n)) = x" |
himmelma@33175 | 78 |
by (simp add: Cart_eq) |
himmelma@33175 | 79 |
|
himmelma@33175 | 80 |
lemma sndcart_pastecart: "sndcart (pastecart (x::'a ^'m ) (y:: 'a ^ 'n)) = y" |
himmelma@33175 | 81 |
by (simp add: Cart_eq) |
himmelma@33175 | 82 |
|
himmelma@33175 | 83 |
lemma pastecart_fst_snd: "pastecart (fstcart z) (sndcart z) = z" |
himmelma@33175 | 84 |
by (simp add: Cart_eq pastecart_def fstcart_def sndcart_def split: sum.split) |
himmelma@33175 | 85 |
|
himmelma@33175 | 86 |
lemma pastecart_eq: "(x = y) \<longleftrightarrow> (fstcart x = fstcart y) \<and> (sndcart x = sndcart y)" |
himmelma@33175 | 87 |
using pastecart_fst_snd[of x] pastecart_fst_snd[of y] by metis |
himmelma@33175 | 88 |
|
himmelma@33175 | 89 |
lemma forall_pastecart: "(\<forall>p. P p) \<longleftrightarrow> (\<forall>x y. P (pastecart x y))" |
himmelma@33175 | 90 |
by (metis pastecart_fst_snd fstcart_pastecart sndcart_pastecart) |
himmelma@33175 | 91 |
|
himmelma@33175 | 92 |
lemma exists_pastecart: "(\<exists>p. P p) \<longleftrightarrow> (\<exists>x y. P (pastecart x y))" |
himmelma@33175 | 93 |
by (metis pastecart_fst_snd fstcart_pastecart sndcart_pastecart) |
himmelma@33175 | 94 |
|
himmelma@33175 | 95 |
end |