author | wenzelm |
Wed, 04 Mar 2009 23:05:32 +0100 | |
changeset 30266 | 970bf4f594c9 |
parent 29494 | a189c6274c7a |
child 30404 | d03dd6301678 |
permissions | -rw-r--r-- |
15469 | 1 |
(* Title: HOL/Library/OptionalSugar.thy |
2 |
Author: Gerwin Klain, Tobias Nipkow |
|
3 |
Copyright 2005 NICTA and TUM |
|
4 |
*) |
|
15476 | 5 |
(*<*) |
15469 | 6 |
theory OptionalSugar |
7 |
imports LaTeXsugar |
|
8 |
begin |
|
9 |
||
22835 | 10 |
(* set *) |
11 |
translations |
|
12 |
"xs" <= "set xs" |
|
13 |
||
15469 | 14 |
(* append *) |
15 |
syntax (latex output) |
|
16 |
"appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65) |
|
17 |
translations |
|
18 |
"appendL xs ys" <= "xs @ ys" |
|
19 |
"appendL (appendL xs ys) zs" <= "appendL xs (appendL ys zs)" |
|
20 |
||
21 |
||
22 |
(* aligning equations *) |
|
21210 | 23 |
notation (tab output) |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
24 |
"op =" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and |
19674 | 25 |
"==" ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)") |
15469 | 26 |
|
27 |
(* Let *) |
|
28 |
translations |
|
29 |
"_bind (p,DUMMY) e" <= "_bind p (fst e)" |
|
30 |
"_bind (DUMMY,p) e" <= "_bind p (snd e)" |
|
31 |
||
32 |
"_tuple_args x (_tuple_args y z)" == |
|
33 |
"_tuple_args x (_tuple_arg (_tuple y z))" |
|
34 |
||
35 |
"_bind (Some p) e" <= "_bind p (the e)" |
|
36 |
"_bind (p#DUMMY) e" <= "_bind p (hd e)" |
|
37 |
"_bind (DUMMY#p) e" <= "_bind p (tl e)" |
|
38 |
||
29494 | 39 |
(* type constraints with spacing *) |
40 |
setup {* |
|
41 |
let |
|
42 |
val typ = SimpleSyntax.read_typ; |
|
43 |
val typeT = Syntax.typeT; |
|
44 |
val spropT = Syntax.spropT; |
|
45 |
in |
|
46 |
Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [ |
|
47 |
("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)), |
|
48 |
("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\<Colon>_", [4, 0], 3))] |
|
49 |
#> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [ |
|
50 |
("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)), |
|
51 |
("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \<Colon> _", [4, 0], 3))] |
|
52 |
end |
|
53 |
*} |
|
54 |
||
55 |
(* sorts as intersections *) |
|
56 |
setup {* |
|
57 |
let |
|
58 |
val sortT = Type ("sort", []); (*FIXME*) |
|
59 |
val classesT = Type ("classes", []); (*FIXME*) |
|
60 |
in |
|
61 |
Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [ |
|
62 |
("_topsort", sortT, Mixfix ("\<top>", [], Syntax.max_pri)), |
|
63 |
("_sort", classesT --> sortT, Mixfix ("'(_')", [], Syntax.max_pri)), |
|
64 |
("_classes", Lexicon.idT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], Syntax.max_pri)), |
|
65 |
("_classes", Lexicon.longidT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], Syntax.max_pri)) |
|
66 |
] |
|
67 |
end |
|
68 |
*} |
|
15469 | 69 |
|
15476 | 70 |
end |
71 |
(*>*) |