# Theory Tuple

Up to index of Isabelle/HOL/ex

theory Tuple
imports HOL
begin

    (*  Title:      HOL/ex/Tuple.thy
        ID:         $Id: Tuple.thy,v 1.8 2005/09/14 20:08:09 wenzelm Exp $
        Author:     Markus Wenzel, TU Muenchen
    *)

    header {* Properly nested products *}

    theory Tuple imports HOL begin

    subsection {* 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"
      Unity :: unit    ("'(')")

    subsection {* Concrete syntax *}

    subsubsection {* 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 (xsymbols)
      "_tuple_type_args" :: "type => tuple_type_args => tuple_type_args" ("_ ×/ _" [21, 20] 20)
      "_tuple_type"      :: "type => tuple_type_args => type"          ("(_ ×/ _)" [21, 20] 20)

    syntax (HTML output)
      "_tuple_type_args" :: "type => tuple_type_args => tuple_type_args" ("_ ×/ _" [21, 20] 20)
      "_tuple_type"      :: "type => tuple_type_args => type"          ("(_ ×/ _)" [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"

    subsubsection {* 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)"

    subsubsection {* Tuple patterns *}

    nonterminals tuple_pat_args
      -- {* extends pre-defined type "pttrn" syntax used in abstractions *}
    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

### Abstract syntax

### Concrete syntax

#### Tuple types

#### Tuples

#### Tuple patterns