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 |
|
|
12 |
theory Tuple = HOL:
|
|
13 |
|
|
14 |
|
|
15 |
(** abstract syntax **)
|
|
16 |
|
|
17 |
typedecl unit
|
|
18 |
typedecl ('a, 'b) prod
|
|
19 |
|
|
20 |
consts
|
|
21 |
Pair :: "'a => 'b => ('a, 'b) prod"
|
|
22 |
fst :: "('a, 'b) prod => 'a"
|
|
23 |
snd :: "('a, 'b) prod => 'b"
|
|
24 |
split :: "('a => 'b => 'c) => ('a, 'b) prod => 'c"
|
|
25 |
"()" :: unit ("'(')")
|
|
26 |
|
|
27 |
|
|
28 |
(** concrete syntax **)
|
|
29 |
|
|
30 |
(* tuple types *)
|
|
31 |
|
|
32 |
nonterminals
|
|
33 |
tuple_type_args
|
|
34 |
syntax
|
|
35 |
"_tuple_type_arg" :: "type => tuple_type_args" ("_" [21] 21)
|
|
36 |
"_tuple_type_args" :: "type => tuple_type_args => tuple_type_args" ("_ */ _" [21, 20] 20)
|
|
37 |
"_tuple_type" :: "type => tuple_type_args => type" ("(_ */ _)" [21, 20] 20)
|
|
38 |
|
|
39 |
syntax (symbols)
|
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 |
syntax (HTML output)
|
9503
|
44 |
"_tuple_type_args" :: "type => tuple_type_args => tuple_type_args" ("_ \<times>/ _" [21, 20] 20)
|
|
45 |
"_tuple_type" :: "type => tuple_type_args => type" ("(_ \<times>/ _)" [21, 20] 20)
|
9353
|
46 |
|
|
47 |
translations
|
|
48 |
(type) "'a * 'b" == (type) "('a, ('b, unit) prod) prod"
|
|
49 |
(type) "('a, ('b, 'cs) _tuple_type_args) _tuple_type" ==
|
|
50 |
(type) "('a, ('b, 'cs) _tuple_type) prod"
|
|
51 |
|
|
52 |
|
|
53 |
(* tuples *)
|
|
54 |
|
|
55 |
nonterminals
|
|
56 |
tuple_args
|
|
57 |
syntax
|
|
58 |
"_tuple" :: "'a => tuple_args => 'b" ("(1'(_,/ _'))")
|
|
59 |
"_tuple_arg" :: "'a => tuple_args" ("_")
|
|
60 |
"_tuple_args" :: "'a => tuple_args => tuple_args" ("_,/ _")
|
|
61 |
translations
|
|
62 |
"(x, y)" == "Pair x (Pair y ())"
|
|
63 |
"_tuple x (_tuple_args y zs)" == "Pair x (_tuple y zs)"
|
|
64 |
|
|
65 |
|
|
66 |
(* tuple patterns *)
|
|
67 |
|
|
68 |
(*extends pre-defined type "pttrn" syntax used in abstractions*)
|
|
69 |
nonterminals
|
|
70 |
tuple_pat_args
|
|
71 |
syntax
|
|
72 |
"_tuple_pat_arg" :: "pttrn => tuple_pat_args" ("_")
|
|
73 |
"_tuple_pat_args" :: "pttrn => tuple_pat_args => tuple_pat_args" ("_,/ _")
|
|
74 |
"_tuple_pat" :: "pttrn => tuple_pat_args => pttrn" ("'(_,/ _')")
|
|
75 |
|
|
76 |
translations
|
|
77 |
"%(x,y). b" => "split (%x. split (%y. (_K b) :: unit => _))"
|
|
78 |
"%(x,y). b" <= "split (%x. split (%y. _K b))"
|
|
79 |
"_abs (_tuple_pat x (_tuple_pat_args y zs)) b" == "split (%x. (_abs (_tuple_pat y zs) b))"
|
|
80 |
|
|
81 |
(* FIXME test *)
|
|
82 |
(*the following rules accommodate tuples in `case C ... (x,y,...) ... => ...' where
|
|
83 |
(x,y,...) is parsed as `Pair x (Pair y ...)' because it is logic, not pttrn*)
|
|
84 |
"_abs (Pair x (Pair y ())) b" => "%(x,y). b"
|
|
85 |
"_abs (Pair x (_abs (_tuple_pat y zs) b))" => "_abs (_tuple_pat x (_tuple_pat_args y zs)) b"
|
|
86 |
|
|
87 |
(* FIXME improve handling of nested patterns *)
|
|
88 |
typed_print_translation {*
|
|
89 |
let
|
|
90 |
fun split_tr' _ T1
|
|
91 |
(Abs (x, xT, Const ("split", T2) $ Abs (y, yT, Abs (_, Type ("unit", []), b))) :: ts) =
|
|
92 |
if Term.loose_bvar1 (b, 0) then raise Match
|
|
93 |
else Term.list_comb
|
|
94 |
(Const ("split", T1) $ Abs (x, xT, Const ("split", T2) $
|
|
95 |
Abs (y, yT, Syntax.const "_K" $ Term.incr_boundvars ~1 b)), ts)
|
|
96 |
| split_tr' _ _ _ = raise Match;
|
|
97 |
in [("split", split_tr')] end
|
|
98 |
*}
|
|
99 |
|
|
100 |
end
|