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