src/HOL/Product_Type.thy
 author paulson Wed Jul 25 13:13:01 2001 +0200 (2001-07-25) changeset 11451 8abfb4f7bd02 parent 11425 4988fd27d6e6 child 11493 f3ff2549cdc8 permissions -rw-r--r--
partial restructuring to reduce dependence on Axiom of Choice
```     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 == THE a. EX b. p = (a, b)"
```
```    90   snd_def:      "snd p == THE 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 => '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
```