# 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" ("_ \\/ _" [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" + + +(* 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