src/HOL/Product_Type.thy
author wenzelm
Fri Feb 02 22:18:10 2001 +0100 (2001-02-02)
changeset 11032 83f723e86dac
parent 11025 a70b796d9af8
child 11425 4988fd27d6e6
permissions -rw-r--r--
added hidden internal_split constant;
tuned;
     1 (*  Title:      HOL/Product_Type.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 
     6 Ordered Pairs and the Cartesian product type.
     7 The unit type.
     8 *)
     9 
    10 theory Product_Type = Fun
    11 files ("Product_Type_lemmas.ML") ("Tools/split_rule.ML"):
    12 
    13 
    14 (** products **)
    15 
    16 (* type definition *)
    17 
    18 constdefs
    19   Pair_Rep :: "['a, 'b] => ['a, 'b] => bool"
    20   "Pair_Rep == (%a b. %x y. x=a & y=b)"
    21 
    22 global
    23 
    24 typedef (Prod)
    25   ('a, 'b) "*"          (infixr 20)
    26     = "{f. EX a b. f = Pair_Rep (a::'a) (b::'b)}"
    27 proof
    28   fix a b show "Pair_Rep a b : ?Prod"
    29     by blast
    30 qed
    31 
    32 syntax (symbols)
    33   "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
    34 syntax (HTML output)
    35   "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
    36 
    37 
    38 (* abstract constants and syntax *)
    39 
    40 consts
    41   fst      :: "'a * 'b => 'a"
    42   snd      :: "'a * 'b => 'b"
    43   split    :: "[['a, 'b] => 'c, 'a * 'b] => 'c"
    44   prod_fun :: "['a => 'b, 'c => 'd, 'a * 'c] => 'b * 'd"
    45   Pair     :: "['a, 'b] => 'a * 'b"
    46   Sigma    :: "['a set, 'a => 'b set] => ('a * 'b) set"
    47 
    48 
    49 (* patterns -- extends pre-defined type "pttrn" used in abstractions *)
    50 
    51 nonterminals
    52   tuple_args patterns
    53 
    54 syntax
    55   "_tuple"      :: "'a => tuple_args => 'a * 'b"        ("(1'(_,/ _'))")
    56   "_tuple_arg"  :: "'a => tuple_args"                   ("_")
    57   "_tuple_args" :: "'a => tuple_args => tuple_args"     ("_,/ _")
    58   "_pattern"    :: "[pttrn, patterns] => pttrn"         ("'(_,/ _')")
    59   ""            :: "pttrn => patterns"                  ("_")
    60   "_patterns"   :: "[pttrn, patterns] => patterns"      ("_,/ _")
    61   "@Sigma" ::"[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" 10)
    62   "@Times" ::"['a set,  'a => 'b set] => ('a * 'b) set" (infixr "<*>" 80)
    63 
    64 translations
    65   "(x, y)"       == "Pair x y"
    66   "_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))"
    67   "%(x,y,zs).b"  == "split(%x (y,zs).b)"
    68   "%(x,y).b"     == "split(%x y. b)"
    69   "_abs (Pair x y) t" => "%(x,y).t"
    70   (* The last rule accommodates tuples in `case C ... (x,y) ... => ...'
    71      The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *)
    72 
    73   "SIGMA x:A. B" => "Sigma A (%x. B)"
    74   "A <*> B"      => "Sigma A (_K B)"
    75 
    76 syntax (symbols)
    77   "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\<Sigma> _\<in>_./ _)"   10)
    78   "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
    79 
    80 print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *}
    81 
    82 
    83 (* definitions *)
    84 
    85 local
    86 
    87 defs
    88   Pair_def:     "Pair a b == Abs_Prod(Pair_Rep a b)"
    89   fst_def:      "fst p == SOME a. EX b. p = (a, b)"
    90   snd_def:      "snd p == SOME b. EX a. p = (a, b)"
    91   split_def:    "split == (%c p. c (fst p) (snd p))"
    92   prod_fun_def: "prod_fun f g == split(%x y.(f(x), g(y)))"
    93   Sigma_def:    "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
    94 
    95 
    96 
    97 (** unit **)
    98 
    99 global
   100 
   101 typedef unit = "{True}"
   102 proof
   103   show "True : ?unit"
   104     by blast
   105 qed
   106 
   107 consts
   108   "()"          :: unit                           ("'(')")
   109 
   110 local
   111 
   112 defs
   113   Unity_def:    "() == Abs_unit True"
   114 
   115 
   116 
   117 (** lemmas and tool setup **)
   118 
   119 use "Product_Type_lemmas.ML"
   120 
   121 constdefs
   122   internal_split :: "('a \<Rightarrow> 'b => 'c) => 'a * 'b => 'c"
   123   "internal_split == split"
   124 
   125 lemma internal_split_conv: "internal_split c (a, b) = c a b"
   126   by (simp only: internal_split_def split_conv)
   127 
   128 hide const internal_split
   129 
   130 use "Tools/split_rule.ML"
   131 setup SplitRule.setup
   132 
   133 end