src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
author hoelzl
Thu, 07 Jan 2010 17:43:35 +0100
changeset 34290 1edf0f223c6e
parent 34289 c9c14c72d035
child 34291 4e896680897e
permissions -rw-r--r--
added syntax translation to automatically add finite typeclass to index type of cartesian product type
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     1
(* Title:      HOL/Library/Finite_Cartesian_Product
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     2
   Author:     Amine Chaieb, University of Cambridge
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     3
*)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     4
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     5
header {* Definition of finite Cartesian product types. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     6
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     7
theory Finite_Cartesian_Product
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     8
imports Main (*FIXME: ATP_Linkup is only needed for metis at a few places. We could dispense of that by changing the proofs.*)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     9
begin
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    10
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    11
subsection {* Finite Cartesian products, with indexing and lambdas. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    12
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    13
typedef (open Cart)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    14
  ('a, 'b) "^" (infixl "^" 15)
34289
c9c14c72d035 Made finite cartesian products finite
himmelma
parents: 33715
diff changeset
    15
    = "UNIV :: (('b::finite) \<Rightarrow> 'a) set"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    16
  morphisms Cart_nth Cart_lambda ..
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    17
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    18
notation Cart_nth (infixl "$" 90)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    19
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    20
notation (xsymbols) Cart_lambda (binder "\<chi>" 10)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    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
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    42
lemma stupid_ext: "(\<forall>x. f x = g x) \<longleftrightarrow> (f = g)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    43
  apply auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    44
  apply (rule ext)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    45
  apply auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    46
  done
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    47
34289
c9c14c72d035 Made finite cartesian products finite
himmelma
parents: 33715
diff changeset
    48
lemma Cart_eq: "((x:: 'a ^ 'b::finite) = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    49
  by (simp add: Cart_nth_inject [symmetric] expand_fun_eq)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    50
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    51
lemma Cart_lambda_beta [simp]: "Cart_lambda g $ i = g i"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    52
  by (simp add: Cart_lambda_inverse)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    53
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    54
lemma Cart_lambda_unique:
34289
c9c14c72d035 Made finite cartesian products finite
himmelma
parents: 33715
diff changeset
    55
  fixes f :: "'a ^ 'b::finite"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    56
  shows "(\<forall>i. f$i = g i) \<longleftrightarrow> Cart_lambda g = f"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    57
  by (auto simp add: Cart_eq)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    58
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    59
lemma Cart_lambda_eta: "(\<chi> i. (g$i)) = g"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    60
  by (simp add: Cart_eq)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    61
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    62
text{* A non-standard sum to "paste" Cartesian products. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    63
34289
c9c14c72d035 Made finite cartesian products finite
himmelma
parents: 33715
diff changeset
    64
definition pastecart :: "'a ^ 'm::finite \<Rightarrow> 'a ^ 'n::finite \<Rightarrow> 'a ^ ('m + 'n)" where
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    65
  "pastecart f g = (\<chi> i. case i of Inl a \<Rightarrow> f$a | Inr b \<Rightarrow> g$b)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    66
34289
c9c14c72d035 Made finite cartesian products finite
himmelma
parents: 33715
diff changeset
    67
definition fstcart:: "'a ^('m::finite + 'n::finite) \<Rightarrow> 'a ^ 'm" where
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    68
  "fstcart f = (\<chi> i. (f$(Inl i)))"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    69
34289
c9c14c72d035 Made finite cartesian products finite
himmelma
parents: 33715
diff changeset
    70
definition sndcart:: "'a ^('m::finite + 'n::finite) \<Rightarrow> 'a ^ 'n" where
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    71
  "sndcart f = (\<chi> i. (f$(Inr i)))"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    72
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    73
lemma nth_pastecart_Inl [simp]: "pastecart f g $ Inl a = f$a"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    74
  unfolding pastecart_def by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    75
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    76
lemma nth_pastecart_Inr [simp]: "pastecart f g $ Inr b = g$b"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    77
  unfolding pastecart_def by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    78
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    79
lemma nth_fstcart [simp]: "fstcart f $ i = f $ Inl i"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    80
  unfolding fstcart_def by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    81
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    82
lemma nth_sndtcart [simp]: "sndcart f $ i = f $ Inr i"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    83
  unfolding sndcart_def by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    84
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    85
lemma finite_sum_image: "(UNIV::('a + 'b) set) = range Inl \<union> range Inr"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    86
by (auto, case_tac x, auto)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    87
34289
c9c14c72d035 Made finite cartesian products finite
himmelma
parents: 33715
diff changeset
    88
lemma fstcart_pastecart: "fstcart (pastecart (x::'a ^'m::finite ) (y:: 'a ^ 'n::finite)) = x"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    89
  by (simp add: Cart_eq)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    90
34289
c9c14c72d035 Made finite cartesian products finite
himmelma
parents: 33715
diff changeset
    91
lemma sndcart_pastecart: "sndcart (pastecart (x::'a ^'m::finite ) (y:: 'a ^ 'n::finite)) = y"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    92
  by (simp add: Cart_eq)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    93
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    94
lemma pastecart_fst_snd: "pastecart (fstcart z) (sndcart z) = z"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    95
  by (simp add: Cart_eq pastecart_def fstcart_def sndcart_def split: sum.split)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    96
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    97
lemma pastecart_eq: "(x = y) \<longleftrightarrow> (fstcart x = fstcart y) \<and> (sndcart x = sndcart y)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    98
  using pastecart_fst_snd[of x] pastecart_fst_snd[of y] by metis
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    99
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   100
lemma forall_pastecart: "(\<forall>p. P p) \<longleftrightarrow> (\<forall>x y. P (pastecart x y))"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   101
  by (metis pastecart_fst_snd fstcart_pastecart sndcart_pastecart)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   102
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   103
lemma exists_pastecart: "(\<exists>p. P p)  \<longleftrightarrow> (\<exists>x y. P (pastecart x y))"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   104
  by (metis pastecart_fst_snd fstcart_pastecart sndcart_pastecart)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   105
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   106
end