author | kleing |
Sat, 01 Mar 2003 16:45:51 +0100 | |
changeset 13840 | 399c8103a98f |
parent 12114 | a8e860c86252 |
child 14981 | e73f8140af78 |
permissions | -rw-r--r-- |
9353 | 1 |
(* Title: HOL/ex/Tuple.thy |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5 |
||
6 |
Properly nested products (see also theory Prod). |
|
7 |
||
8 |
Unquestionably, this should be used as the standard representation of |
|
9 |
tuples in HOL, but it breaks many existing theories! |
|
10 |
*) |
|
11 |
||
10357 | 12 |
header {* Properly nested products *} |
13 |
||
9353 | 14 |
theory Tuple = HOL: |
15 |
||
16 |
||
10357 | 17 |
subsection {* Abstract syntax *} |
9353 | 18 |
|
19 |
typedecl unit |
|
20 |
typedecl ('a, 'b) prod |
|
21 |
||
22 |
consts |
|
23 |
Pair :: "'a => 'b => ('a, 'b) prod" |
|
24 |
fst :: "('a, 'b) prod => 'a" |
|
25 |
snd :: "('a, 'b) prod => 'b" |
|
26 |
split :: "('a => 'b => 'c) => ('a, 'b) prod => 'c" |
|
11606 | 27 |
Unity :: unit ("'(')") |
9353 | 28 |
|
29 |
||
10357 | 30 |
subsection {* Concrete syntax *} |
9353 | 31 |
|
10357 | 32 |
subsubsection {* Tuple types *} |
9353 | 33 |
|
34 |
nonterminals |
|
35 |
tuple_type_args |
|
36 |
syntax |
|
37 |
"_tuple_type_arg" :: "type => tuple_type_args" ("_" [21] 21) |
|
38 |
"_tuple_type_args" :: "type => tuple_type_args => tuple_type_args" ("_ */ _" [21, 20] 20) |
|
39 |
"_tuple_type" :: "type => tuple_type_args => type" ("(_ */ _)" [21, 20] 20) |
|
40 |
||
12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
11606
diff
changeset
|
41 |
syntax (xsymbols) |
9503 | 42 |
"_tuple_type_args" :: "type => tuple_type_args => tuple_type_args" ("_ \<times>/ _" [21, 20] 20) |
43 |
"_tuple_type" :: "type => tuple_type_args => type" ("(_ \<times>/ _)" [21, 20] 20) |
|
9353 | 44 |
|
45 |
syntax (HTML output) |
|
9503 | 46 |
"_tuple_type_args" :: "type => tuple_type_args => tuple_type_args" ("_ \<times>/ _" [21, 20] 20) |
47 |
"_tuple_type" :: "type => tuple_type_args => type" ("(_ \<times>/ _)" [21, 20] 20) |
|
9353 | 48 |
|
49 |
translations |
|
50 |
(type) "'a * 'b" == (type) "('a, ('b, unit) prod) prod" |
|
51 |
(type) "('a, ('b, 'cs) _tuple_type_args) _tuple_type" == |
|
52 |
(type) "('a, ('b, 'cs) _tuple_type) prod" |
|
53 |
||
54 |
||
10357 | 55 |
subsubsection {* Tuples *} |
9353 | 56 |
|
57 |
nonterminals |
|
58 |
tuple_args |
|
59 |
syntax |
|
60 |
"_tuple" :: "'a => tuple_args => 'b" ("(1'(_,/ _'))") |
|
61 |
"_tuple_arg" :: "'a => tuple_args" ("_") |
|
62 |
"_tuple_args" :: "'a => tuple_args => tuple_args" ("_,/ _") |
|
63 |
translations |
|
64 |
"(x, y)" == "Pair x (Pair y ())" |
|
65 |
"_tuple x (_tuple_args y zs)" == "Pair x (_tuple y zs)" |
|
66 |
||
67 |
||
10357 | 68 |
subsubsection {* Tuple patterns *} |
9353 | 69 |
|
10357 | 70 |
nonterminals tuple_pat_args |
71 |
-- {* extends pre-defined type "pttrn" syntax used in abstractions *} |
|
9353 | 72 |
syntax |
73 |
"_tuple_pat_arg" :: "pttrn => tuple_pat_args" ("_") |
|
74 |
"_tuple_pat_args" :: "pttrn => tuple_pat_args => tuple_pat_args" ("_,/ _") |
|
75 |
"_tuple_pat" :: "pttrn => tuple_pat_args => pttrn" ("'(_,/ _')") |
|
76 |
||
77 |
translations |
|
78 |
"%(x,y). b" => "split (%x. split (%y. (_K b) :: unit => _))" |
|
79 |
"%(x,y). b" <= "split (%x. split (%y. _K b))" |
|
80 |
"_abs (_tuple_pat x (_tuple_pat_args y zs)) b" == "split (%x. (_abs (_tuple_pat y zs) b))" |
|
81 |
||
82 |
(* FIXME test *) |
|
83 |
(*the following rules accommodate tuples in `case C ... (x,y,...) ... => ...' where |
|
84 |
(x,y,...) is parsed as `Pair x (Pair y ...)' because it is logic, not pttrn*) |
|
85 |
"_abs (Pair x (Pair y ())) b" => "%(x,y). b" |
|
86 |
"_abs (Pair x (_abs (_tuple_pat y zs) b))" => "_abs (_tuple_pat x (_tuple_pat_args y zs)) b" |
|
87 |
||
88 |
(* FIXME improve handling of nested patterns *) |
|
89 |
typed_print_translation {* |
|
90 |
let |
|
91 |
fun split_tr' _ T1 |
|
92 |
(Abs (x, xT, Const ("split", T2) $ Abs (y, yT, Abs (_, Type ("unit", []), b))) :: ts) = |
|
93 |
if Term.loose_bvar1 (b, 0) then raise Match |
|
94 |
else Term.list_comb |
|
95 |
(Const ("split", T1) $ Abs (x, xT, Const ("split", T2) $ |
|
96 |
Abs (y, yT, Syntax.const "_K" $ Term.incr_boundvars ~1 b)), ts) |
|
97 |
| split_tr' _ _ _ = raise Match; |
|
98 |
in [("split", split_tr')] end |
|
99 |
*} |
|
100 |
||
101 |
end |