src/HOL/Library/OptionalSugar.thy
 author nipkow Thu Mar 12 14:27:21 2009 +0100 (2009-03-12) changeset 30474 52e92009aacb parent 30404 d03dd6301678 child 30502 b80d2621caee permissions -rw-r--r--
optional latex sugar
1 (*  Title:      HOL/Library/OptionalSugar.thy
2     Author:     Gerwin Klain, Tobias Nipkow
3     Copyright   2005 NICTA and TUM
4 *)
5 (*<*)
6 theory OptionalSugar
7 imports LaTeXsugar Complex_Main
8 begin
10 (* hiding set *)
11 translations
12   "xs" <= "CONST set xs"
14 (* hiding numeric conversions - embeddings only *)
15 translations
16   "n" <= "CONST of_nat n"
17   "n" <= "CONST int n"
18   "n" <= "real n"
19   "n" <= "CONST real_of_nat n"
20   "n" <= "CONST real_of_int n"
22 (* append *)
23 syntax (latex output)
24   "appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65)
25 translations
26   "appendL xs ys" <= "xs @ ys"
27   "appendL (appendL xs ys) zs" <= "appendL xs (appendL ys zs)"
30 (* aligning equations *)
31 notation (tab output)
32   "op ="  ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
33   "=="  ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
35 (* Let *)
36 translations
37   "_bind (p,DUMMY) e" <= "_bind p (CONST fst e)"
38   "_bind (DUMMY,p) e" <= "_bind p (CONST snd e)"
40   "_tuple_args x (_tuple_args y z)" ==
41     "_tuple_args x (_tuple_arg (_tuple y z))"
43   "_bind (Some p) e" <= "_bind p (CONST the e)"
44   "_bind (p#DUMMY) e" <= "_bind p (CONST hd e)"
45   "_bind (DUMMY#p) e" <= "_bind p (CONST tl e)"
47 (* type constraints with spacing *)
48 setup {*
49 let
51   val typeT = Syntax.typeT;
52   val spropT = Syntax.spropT;
53 in
54   Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [
55     ("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
56     ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\<Colon>_", [4, 0], 3))]
57   #> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
58       ("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
59       ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \<Colon> _", [4, 0], 3))]
60 end
61 *}
63 (* sorts as intersections *)
64 setup {*
65 let
66   val sortT = Type ("sort", []); (*FIXME*)
67   val classesT = Type ("classes", []); (*FIXME*)
68 in