# HG changeset patch
# User wenzelm
# Date 963773353 -7200
# Node ID 93cd32adc402f03fdb0f524501b9907aabb7fd58
# Parent  416b2ecd97a173caffa66c3a4745e0cfbb18107c
added ex/Tuple.thy;

diff -r 416b2ecd97a1 -r 93cd32adc402 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sun Jul 16 20:48:35 2000 +0200
+++ b/src/HOL/IsaMakefile	Sun Jul 16 20:49:13 2000 +0200
@@ -435,7 +435,7 @@
   ex/StringEx.thy ex/Tarski.ML ex/Tarski.thy \
   ex/BinEx.ML ex/BinEx.thy ex/svc_test.thy ex/svc_test.ML ex/MonoidGroup.thy \
   ex/PiSets.thy ex/PiSets.ML ex/LocaleGroup.thy ex/LocaleGroup.ML \
-  ex/Antiquote.thy ex/Multiquote.thy ex/Points.thy
+  ex/Antiquote.thy ex/Multiquote.thy ex/Points.thy ex/Tuple.thy
 	@$(ISATOOL) usedir $(OUT)/HOL ex
 
 
diff -r 416b2ecd97a1 -r 93cd32adc402 src/HOL/ex/Tuple.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Tuple.thy	Sun Jul 16 20:49:13 2000 +0200
@@ -0,0 +1,100 @@
+(*  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