src/HOL/Library/OptionalSugar.thy
author wenzelm
Sat Jan 18 20:20:56 2014 +0100 (2014-01-18)
changeset 55038 f2179be64805
parent 42297 140f283266b7
child 55052 c602013f127e
permissions -rw-r--r--
prefer Isar commands over old-fashioned ML (see also a189c6274c7a);
removed pointless space: the second "_ \<Colon> _" should take precendence anyway;
nipkow@15469
     1
(*  Title:      HOL/Library/OptionalSugar.thy
nipkow@15469
     2
    Author:     Gerwin Klain, Tobias Nipkow
nipkow@15469
     3
    Copyright   2005 NICTA and TUM
nipkow@15469
     4
*)
nipkow@15476
     5
(*<*)
nipkow@15469
     6
theory OptionalSugar
haftmann@30663
     7
imports Complex_Main LaTeXsugar
nipkow@15469
     8
begin
nipkow@15469
     9
nipkow@30474
    10
(* hiding set *)
nipkow@22835
    11
translations
wenzelm@30404
    12
  "xs" <= "CONST set xs"
nipkow@22835
    13
nipkow@30474
    14
(* hiding numeric conversions - embeddings only *)
nipkow@30474
    15
translations
nipkow@30474
    16
  "n" <= "CONST of_nat n"
nipkow@30474
    17
  "n" <= "CONST int n"
wenzelm@35115
    18
  "n" <= "CONST real n"
nipkow@30474
    19
  "n" <= "CONST real_of_nat n"
nipkow@30474
    20
  "n" <= "CONST real_of_int n"
nipkow@30502
    21
  "n" <= "CONST of_real n"
nipkow@30502
    22
  "n" <= "CONST complex_of_real n"
nipkow@30474
    23
nipkow@15469
    24
(* append *)
nipkow@15469
    25
syntax (latex output)
wenzelm@35115
    26
  "_appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65)
nipkow@15469
    27
translations
wenzelm@35115
    28
  "_appendL xs ys" <= "xs @ ys" 
wenzelm@35115
    29
  "_appendL (_appendL xs ys) zs" <= "_appendL xs (_appendL ys zs)"
nipkow@15469
    30
nipkow@15469
    31
haftmann@32891
    32
(* deprecated, use thm with style instead, will be removed *)
nipkow@15469
    33
(* aligning equations *)
wenzelm@21210
    34
notation (tab output)
haftmann@38864
    35
  "HOL.eq"  ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
wenzelm@19674
    36
  "=="  ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
nipkow@15469
    37
nipkow@15469
    38
(* Let *)
nipkow@15469
    39
translations 
wenzelm@35250
    40
  "_bind (p, CONST DUMMY) e" <= "_bind p (CONST fst e)"
wenzelm@35250
    41
  "_bind (CONST DUMMY, p) e" <= "_bind p (CONST snd e)"
nipkow@15469
    42
nipkow@15469
    43
  "_tuple_args x (_tuple_args y z)" ==
nipkow@15469
    44
    "_tuple_args x (_tuple_arg (_tuple y z))"
nipkow@15469
    45
wenzelm@35250
    46
  "_bind (CONST Some p) e" <= "_bind p (CONST the e)"
wenzelm@35250
    47
  "_bind (p # CONST DUMMY) e" <= "_bind p (CONST hd e)"
wenzelm@35250
    48
  "_bind (CONST DUMMY # p) e" <= "_bind p (CONST tl e)"
nipkow@15469
    49
haftmann@29494
    50
(* type constraints with spacing *)
wenzelm@55038
    51
wenzelm@55038
    52
no_syntax (xsymbols output)
wenzelm@55038
    53
  "_constrain" :: "logic => type => logic"  ("_\<Colon>_" [4, 0] 3)
wenzelm@55038
    54
  "_constrain" :: "prop' => type => prop'"  ("_\<Colon>_" [4, 0] 3)
wenzelm@55038
    55
wenzelm@55038
    56
syntax (xsymbols output)
wenzelm@55038
    57
  "_constrain" :: "logic => type => logic"  ("_ \<Colon> _" [4, 0] 3)
wenzelm@55038
    58
  "_constrain" :: "prop' => type => prop'"  ("_ \<Colon> _" [4, 0] 3)
wenzelm@55038
    59
haftmann@29494
    60
haftmann@29494
    61
(* sorts as intersections *)
wenzelm@55038
    62
wenzelm@55038
    63
syntax (xsymbols output)
wenzelm@55038
    64
  "_topsort" :: "sort"  ("\<top>" 1000)
wenzelm@55038
    65
  "_sort" :: "classes => sort"  ("'(_')" 1000)
wenzelm@55038
    66
  "_classes" :: "id => classes => classes"  ("_ \<inter> _" 1000)
wenzelm@55038
    67
  "_classes" :: "longid => classes => classes"  ("_ \<inter> _" 1000)
nipkow@15469
    68
nipkow@15476
    69
end
nipkow@15476
    70
(*>*)