src/HOL/ex/Tuple.thy

final tuning;

(*  Title:      HOL/ex/Tuple.thy
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen
    License:    GPL (GNU GENERAL PUBLIC LICENSE)

Properly nested products (see also theory Prod).

Unquestionably, this should be used as the standard representation of
tuples in HOL, but it breaks many existing theories!
*)

theory Tuple = HOL:


(** abstract syntax **)

typedecl unit
typedecl ('a, 'b) prod

consts
  Pair :: "'a => 'b => ('a, 'b) prod"
  fst :: "('a, 'b) prod => 'a"
  snd :: "('a, 'b) prod => 'b"
  split :: "('a => 'b => 'c) => ('a, 'b) prod => 'c"
  "()" :: unit  ("'(')")


(** concrete syntax **)

(* tuple types *)

nonterminals
  tuple_type_args
syntax
  "_tuple_type_arg"  :: "type => tuple_type_args"                    ("_" [21] 21)
  "_tuple_type_args" :: "type => tuple_type_args => tuple_type_args" ("_ */ _" [21, 20] 20)
  "_tuple_type"      :: "type => tuple_type_args => type"            ("(_ */ _)" [21, 20] 20)

syntax (symbols)
  "_tuple_type_args" :: "type => tuple_type_args => tuple_type_args" ("_ \<times>/ _" [21, 20] 20)
  "_tuple_type"      :: "type => tuple_type_args => type"          ("(_ \<times>/ _)" [21, 20] 20)

syntax (HTML output)
  "_tuple_type_args" :: "type => tuple_type_args => tuple_type_args" ("_ \<times>/ _" [21, 20] 20)
  "_tuple_type"      :: "type => tuple_type_args => type"          ("(_ \<times>/ _)" [21, 20] 20)

translations
  (type) "'a * 'b" == (type) "('a, ('b, unit) prod) prod"
  (type) "('a, ('b, 'cs) _tuple_type_args) _tuple_type" ==
    (type) "('a, ('b, 'cs) _tuple_type) prod"


(* tuples *)

nonterminals
  tuple_args
syntax
  "_tuple"      :: "'a => tuple_args => 'b"             ("(1'(_,/ _'))")
  "_tuple_arg"  :: "'a => tuple_args"                   ("_")
  "_tuple_args" :: "'a => tuple_args => tuple_args"     ("_,/ _")
translations
  "(x, y)" == "Pair x (Pair y ())"
  "_tuple x (_tuple_args y zs)" == "Pair x (_tuple y zs)"


(* tuple patterns *)

(*extends pre-defined type "pttrn" syntax used in abstractions*)
nonterminals
  tuple_pat_args
syntax
  "_tuple_pat_arg"  :: "pttrn => tuple_pat_args"                     ("_")
  "_tuple_pat_args" :: "pttrn => tuple_pat_args => tuple_pat_args"   ("_,/ _")
  "_tuple_pat"      :: "pttrn => tuple_pat_args => pttrn"            ("'(_,/ _')")

translations
  "%(x,y). b" => "split (%x. split (%y. (_K b) :: unit => _))"
  "%(x,y). b" <= "split (%x. split (%y. _K b))"
  "_abs (_tuple_pat x (_tuple_pat_args y zs)) b" == "split (%x. (_abs (_tuple_pat y zs) b))"

(* FIXME test *)
  (*the following rules accommodate tuples in `case C ... (x,y,...) ... => ...' where
     (x,y,...) is parsed as `Pair x (Pair y ...)' because it is logic, not pttrn*)
  "_abs (Pair x (Pair y ())) b" => "%(x,y). b"
  "_abs (Pair x (_abs (_tuple_pat y zs) b))" => "_abs (_tuple_pat x (_tuple_pat_args y zs)) b"

(* FIXME improve handling of nested patterns *)
typed_print_translation {*
  let
    fun split_tr' _ T1
            (Abs (x, xT, Const ("split", T2) $ Abs (y, yT, Abs (_, Type ("unit", []), b))) :: ts) =
          if Term.loose_bvar1 (b, 0) then raise Match
          else Term.list_comb
            (Const ("split", T1) $ Abs (x, xT, Const ("split", T2) $
              Abs (y, yT, Syntax.const "_K" $ Term.incr_boundvars ~1 b)), ts)
      | split_tr' _ _ _ = raise Match;
  in [("split", split_tr')] end
*}

end