src/HOL/ex/Tuple.thy
author kleing
Sat, 01 Mar 2003 16:45:51 +0100
changeset 13840 399c8103a98f
parent 12114 a8e860c86252
child 14981 e73f8140af78
permissions -rw-r--r--
keep a copy of generated files in repository
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9353
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/ex/Tuple.thy
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
     5
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
     6
Properly nested products (see also theory Prod).
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
     7
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
     8
Unquestionably, this should be used as the standard representation of
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
     9
tuples in HOL, but it breaks many existing theories!
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    10
*)
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    11
10357
wenzelm
parents: 9503
diff changeset
    12
header {* Properly nested products *}
wenzelm
parents: 9503
diff changeset
    13
9353
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    14
theory Tuple = HOL:
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    15
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    16
10357
wenzelm
parents: 9503
diff changeset
    17
subsection {* Abstract syntax *}
9353
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    18
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    19
typedecl unit
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    20
typedecl ('a, 'b) prod
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    21
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    22
consts
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    23
  Pair :: "'a => 'b => ('a, 'b) prod"
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    24
  fst :: "('a, 'b) prod => 'a"
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    25
  snd :: "('a, 'b) prod => 'b"
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    26
  split :: "('a => 'b => 'c) => ('a, 'b) prod => 'c"
11606
43abedd4467e renamed "()" to Unity;
wenzelm
parents: 10357
diff changeset
    27
  Unity :: unit    ("'(')")
9353
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    28
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    29
10357
wenzelm
parents: 9503
diff changeset
    30
subsection {* Concrete syntax *}
9353
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    31
10357
wenzelm
parents: 9503
diff changeset
    32
subsubsection {* Tuple types *}
9353
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    33
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    34
nonterminals
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    35
  tuple_type_args
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    36
syntax
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    37
  "_tuple_type_arg"  :: "type => tuple_type_args"                    ("_" [21] 21)
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    38
  "_tuple_type_args" :: "type => tuple_type_args => tuple_type_args" ("_ */ _" [21, 20] 20)
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    39
  "_tuple_type"      :: "type => tuple_type_args => type"            ("(_ */ _)" [21, 20] 20)
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    40
12114
a8e860c86252 eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents: 11606
diff changeset
    41
syntax (xsymbols)
9503
wenzelm
parents: 9353
diff changeset
    42
  "_tuple_type_args" :: "type => tuple_type_args => tuple_type_args" ("_ \<times>/ _" [21, 20] 20)
wenzelm
parents: 9353
diff changeset
    43
  "_tuple_type"      :: "type => tuple_type_args => type"          ("(_ \<times>/ _)" [21, 20] 20)
9353
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    44
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    45
syntax (HTML output)
9503
wenzelm
parents: 9353
diff changeset
    46
  "_tuple_type_args" :: "type => tuple_type_args => tuple_type_args" ("_ \<times>/ _" [21, 20] 20)
wenzelm
parents: 9353
diff changeset
    47
  "_tuple_type"      :: "type => tuple_type_args => type"          ("(_ \<times>/ _)" [21, 20] 20)
9353
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    48
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    49
translations
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    50
  (type) "'a * 'b" == (type) "('a, ('b, unit) prod) prod"
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    51
  (type) "('a, ('b, 'cs) _tuple_type_args) _tuple_type" ==
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    52
    (type) "('a, ('b, 'cs) _tuple_type) prod"
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    53
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    54
10357
wenzelm
parents: 9503
diff changeset
    55
subsubsection {* Tuples *}
9353
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    56
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    57
nonterminals
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    58
  tuple_args
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    59
syntax
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    60
  "_tuple"      :: "'a => tuple_args => 'b"             ("(1'(_,/ _'))")
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    61
  "_tuple_arg"  :: "'a => tuple_args"                   ("_")
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    62
  "_tuple_args" :: "'a => tuple_args => tuple_args"     ("_,/ _")
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    63
translations
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    64
  "(x, y)" == "Pair x (Pair y ())"
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    65
  "_tuple x (_tuple_args y zs)" == "Pair x (_tuple y zs)"
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    66
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    67
10357
wenzelm
parents: 9503
diff changeset
    68
subsubsection {* Tuple patterns *}
9353
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    69
10357
wenzelm
parents: 9503
diff changeset
    70
nonterminals tuple_pat_args
wenzelm
parents: 9503
diff changeset
    71
  -- {* extends pre-defined type "pttrn" syntax used in abstractions *}
9353
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    72
syntax
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    73
  "_tuple_pat_arg"  :: "pttrn => tuple_pat_args"                     ("_")
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    74
  "_tuple_pat_args" :: "pttrn => tuple_pat_args => tuple_pat_args"   ("_,/ _")
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    75
  "_tuple_pat"      :: "pttrn => tuple_pat_args => pttrn"            ("'(_,/ _')")
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    76
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    77
translations
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    78
  "%(x,y). b" => "split (%x. split (%y. (_K b) :: unit => _))"
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    79
  "%(x,y). b" <= "split (%x. split (%y. _K b))"
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    80
  "_abs (_tuple_pat x (_tuple_pat_args y zs)) b" == "split (%x. (_abs (_tuple_pat y zs) b))"
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    81
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    82
(* FIXME test *)
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    83
  (*the following rules accommodate tuples in `case C ... (x,y,...) ... => ...' where
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    84
     (x,y,...) is parsed as `Pair x (Pair y ...)' because it is logic, not pttrn*)
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    85
  "_abs (Pair x (Pair y ())) b" => "%(x,y). b"
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    86
  "_abs (Pair x (_abs (_tuple_pat y zs) b))" => "_abs (_tuple_pat x (_tuple_pat_args y zs)) b"
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    87
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    88
(* FIXME improve handling of nested patterns *)
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    89
typed_print_translation {*
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    90
  let
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    91
    fun split_tr' _ T1
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    92
            (Abs (x, xT, Const ("split", T2) $ Abs (y, yT, Abs (_, Type ("unit", []), b))) :: ts) =
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    93
          if Term.loose_bvar1 (b, 0) then raise Match
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    94
          else Term.list_comb
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    95
            (Const ("split", T1) $ Abs (x, xT, Const ("split", T2) $
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    96
              Abs (y, yT, Syntax.const "_K" $ Term.incr_boundvars ~1 b)), ts)
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    97
      | split_tr' _ _ _ = raise Match;
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    98
  in [("split", split_tr')] end
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
    99
*}
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
   100
93cd32adc402 added ex/Tuple.thy;
wenzelm
parents:
diff changeset
   101
end