# HG changeset patch
# User wenzelm
# Date 1128790263 -7200
# Node ID f4453001cbde281b15345e759c10bd9d92436b95
# Parent  aa6ec0efe4d388013046b8311641f139ff44826c
obsolete;

diff -r aa6ec0efe4d3 -r f4453001cbde src/HOL/ex/Tuple.thy
--- a/src/HOL/ex/Tuple.thy	Sat Oct 08 15:20:58 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,95 +0,0 @@
-(*  Title:      HOL/ex/Tuple.thy
-    ID:         $Id$
-    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" ("_ \<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"
-
-
-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