src/HOL/Library/OptionalSugar.thy
author nipkow
Tue Sep 22 14:31:22 2015 +0200 (2015-09-22)
changeset 61225 1a690dce8cfc
parent 61143 5f898411ce87
child 61645 ae5e55d03e45
permissions -rw-r--r--
tuned references
     1 (*  Title:      HOL/Library/OptionalSugar.thy
     2     Author:     Gerwin Klein, 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" <= "CONST 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   "HOL.eq"  ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
    36   "Pure.eq"  ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
    37 
    38 (* Let *)
    39 translations 
    40   "_bind (p, CONST DUMMY) e" <= "_bind p (CONST fst e)"
    41   "_bind (CONST 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 (CONST Some p) e" <= "_bind p (CONST the e)"
    47   "_bind (p # CONST DUMMY) e" <= "_bind p (CONST hd e)"
    48   "_bind (CONST DUMMY # p) e" <= "_bind p (CONST tl e)"
    49 
    50 (* type constraints with spacing *)
    51 no_syntax (output)
    52   "_constrain" :: "logic => type => logic"  ("_::_" [4, 0] 3)
    53   "_constrain" :: "prop' => type => prop'"  ("_::_" [4, 0] 3)
    54 
    55 syntax (output)
    56   "_constrain" :: "logic => type => logic"  ("_ :: _" [4, 0] 3)
    57   "_constrain" :: "prop' => type => prop'"  ("_ :: _" [4, 0] 3)
    58 
    59 
    60 (* sorts as intersections *)
    61 
    62 syntax (xsymbols output)
    63   "_topsort" :: "sort"  ("\<top>" 1000)
    64   "_sort" :: "classes => sort"  ("'(_')" 1000)
    65   "_classes" :: "id => classes => classes"  ("_ \<inter> _" 1000)
    66   "_classes" :: "longid => classes => classes"  ("_ \<inter> _" 1000)
    67 
    68 end
    69 (*>*)