(* 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