src/HOL/Library/OptionalSugar.thy
author wenzelm
Tue Mar 10 10:59:59 2009 +0100 (2009-03-10)
changeset 30404 d03dd6301678
parent 29494 a189c6274c7a
child 30474 52e92009aacb
permissions -rw-r--r--
more robust treatment of (authentic) consts within translations;
     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
     8 begin
     9 
    10 (* set *)
    11 translations
    12   "xs" <= "CONST set xs"
    13 
    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 *)
    23 notation (tab output)
    24   "op ="  ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
    25   "=="  ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
    26 
    27 (* Let *)
    28 translations 
    29   "_bind (p,DUMMY) e" <= "_bind p (CONST fst e)"
    30   "_bind (DUMMY,p) e" <= "_bind p (CONST 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 (CONST the e)"
    36   "_bind (p#DUMMY) e" <= "_bind p (CONST hd e)"
    37   "_bind (DUMMY#p) e" <= "_bind p (CONST tl e)"
    38 
    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 *}
    69 
    70 end
    71 (*>*)