src/HOL/Library/OptionalSugar.thy
author haftmann
Thu Oct 08 15:16:13 2009 +0200 (2009-10-08)
changeset 32891 d403b99287ff
parent 30663 0b6aff7451b2
child 33384 1b5ba4e6a953
permissions -rw-r--r--
new generalized concept for term styles
     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 Complex_Main LaTeXsugar
     8 begin
     9 
    10 (* hiding set *)
    11 translations
    12   "xs" <= "CONST set xs"
    13 
    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"
    21   "n" <= "CONST of_real n"
    22   "n" <= "CONST complex_of_real n"
    23 
    24 (* append *)
    25 syntax (latex output)
    26   "appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65)
    27 translations
    28   "appendL xs ys" <= "xs @ ys" 
    29   "appendL (appendL xs ys) zs" <= "appendL xs (appendL ys zs)"
    30 
    31 
    32 (* deprecated, use thm with style instead, will be removed *)
    33 (* aligning equations *)
    34 notation (tab output)
    35   "op ="  ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
    36   "=="  ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
    37 
    38 (* Let *)
    39 translations 
    40   "_bind (p,DUMMY) e" <= "_bind p (CONST fst e)"
    41   "_bind (DUMMY,p) e" <= "_bind p (CONST snd e)"
    42 
    43   "_tuple_args x (_tuple_args y z)" ==
    44     "_tuple_args x (_tuple_arg (_tuple y z))"
    45 
    46   "_bind (Some p) e" <= "_bind p (CONST the e)"
    47   "_bind (p#DUMMY) e" <= "_bind p (CONST hd e)"
    48   "_bind (DUMMY#p) e" <= "_bind p (CONST tl e)"
    49 
    50 (* type constraints with spacing *)
    51 setup {*
    52 let
    53   val typ = SimpleSyntax.read_typ;
    54   val typeT = Syntax.typeT;
    55   val spropT = Syntax.spropT;
    56 in
    57   Sign.del_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   #> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
    61       ("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
    62       ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \<Colon> _", [4, 0], 3))]
    63 end
    64 *}
    65 
    66 (* sorts as intersections *)
    67 setup {*
    68 let
    69   val sortT = Type ("sort", []); (*FIXME*)
    70   val classesT = Type ("classes", []); (*FIXME*)
    71 in
    72   Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
    73     ("_topsort", sortT, Mixfix ("\<top>", [], Syntax.max_pri)),
    74     ("_sort", classesT --> sortT, Mixfix ("'(_')", [], Syntax.max_pri)),
    75     ("_classes", Lexicon.idT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], Syntax.max_pri)),
    76     ("_classes", Lexicon.longidT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], Syntax.max_pri))
    77   ]
    78 end
    79 *}
    80 
    81 end
    82 (*>*)