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
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
nipkow@30474
     7
imports LaTeXsugar Complex_Main
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"
nipkow@30474
    18
  "n" <= "real n"
nipkow@30474
    19
  "n" <= "CONST real_of_nat n"
nipkow@30474
    20
  "n" <= "CONST real_of_int n"
nipkow@30474
    21
nipkow@15469
    22
(* append *)
nipkow@15469
    23
syntax (latex output)
nipkow@15469
    24
  "appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65)
nipkow@15469
    25
translations
nipkow@15469
    26
  "appendL xs ys" <= "xs @ ys" 
nipkow@15469
    27
  "appendL (appendL xs ys) zs" <= "appendL xs (appendL ys zs)"
nipkow@15469
    28
nipkow@15469
    29
nipkow@15469
    30
(* aligning equations *)
wenzelm@21210
    31
notation (tab output)
wenzelm@21404
    32
  "op ="  ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
wenzelm@19674
    33
  "=="  ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
nipkow@15469
    34
nipkow@15469
    35
(* Let *)
nipkow@15469
    36
translations 
wenzelm@30404
    37
  "_bind (p,DUMMY) e" <= "_bind p (CONST fst e)"
wenzelm@30404
    38
  "_bind (DUMMY,p) e" <= "_bind p (CONST snd e)"
nipkow@15469
    39
nipkow@15469
    40
  "_tuple_args x (_tuple_args y z)" ==
nipkow@15469
    41
    "_tuple_args x (_tuple_arg (_tuple y z))"
nipkow@15469
    42
wenzelm@30404
    43
  "_bind (Some p) e" <= "_bind p (CONST the e)"
wenzelm@30404
    44
  "_bind (p#DUMMY) e" <= "_bind p (CONST hd e)"
wenzelm@30404
    45
  "_bind (DUMMY#p) e" <= "_bind p (CONST tl e)"
nipkow@15469
    46
haftmann@29494
    47
(* type constraints with spacing *)
haftmann@29494
    48
setup {*
haftmann@29494
    49
let
haftmann@29494
    50
  val typ = SimpleSyntax.read_typ;
haftmann@29494
    51
  val typeT = Syntax.typeT;
haftmann@29494
    52
  val spropT = Syntax.spropT;
haftmann@29494
    53
in
haftmann@29494
    54
  Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [
haftmann@29494
    55
    ("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
haftmann@29494
    56
    ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\<Colon>_", [4, 0], 3))]
haftmann@29494
    57
  #> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
haftmann@29494
    58
      ("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
haftmann@29494
    59
      ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \<Colon> _", [4, 0], 3))]
haftmann@29494
    60
end
haftmann@29494
    61
*}
haftmann@29494
    62
haftmann@29494
    63
(* sorts as intersections *)
haftmann@29494
    64
setup {*
haftmann@29494
    65
let
haftmann@29494
    66
  val sortT = Type ("sort", []); (*FIXME*)
haftmann@29494
    67
  val classesT = Type ("classes", []); (*FIXME*)
haftmann@29494
    68
in
haftmann@29494
    69
  Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
haftmann@29494
    70
    ("_topsort", sortT, Mixfix ("\<top>", [], Syntax.max_pri)),
haftmann@29494
    71
    ("_sort", classesT --> sortT, Mixfix ("'(_')", [], Syntax.max_pri)),
haftmann@29494
    72
    ("_classes", Lexicon.idT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], Syntax.max_pri)),
haftmann@29494
    73
    ("_classes", Lexicon.longidT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], Syntax.max_pri))
haftmann@29494
    74
  ]
haftmann@29494
    75
end
haftmann@29494
    76
*}
nipkow@15469
    77
nipkow@15476
    78
end
nipkow@15476
    79
(*>*)