src/HOL/Library/LaTeXsugar.thy
author nipkow
Sun Apr 10 11:42:07 2005 +0200 (2005-04-10)
changeset 15690 1da2cfd1ca45
parent 15476 b8cb20cc0c0b
child 16110 c423bb89186d
permissions -rw-r--r--
tuned
nipkow@15469
     1
(*  Title:      HOL/Library/LaTeXsugar.thy
nipkow@15469
     2
    ID:         $Id$
nipkow@15469
     3
    Author:     Gerwin Klain, Tobias Nipkow, Norbert Schirmer
nipkow@15469
     4
    Copyright   2005 NICTA and TUM
nipkow@15469
     5
*)
nipkow@15469
     6
nipkow@15469
     7
(*<*)
nipkow@15469
     8
theory LaTeXsugar
nipkow@15469
     9
imports Main
nipkow@15469
    10
begin
nipkow@15469
    11
nipkow@15469
    12
(* LOGIC *)
nipkow@15469
    13
syntax (latex output)
nipkow@15469
    14
  If            :: "[bool, 'a, 'a] => 'a"
nipkow@15469
    15
  ("(\<^raw:\textsf{>if\<^raw:}> (_)/ \<^raw:\textsf{>then\<^raw:}> (_)/ \<^raw:\textsf{>else\<^raw:}> (_))" 10)
nipkow@15469
    16
nipkow@15469
    17
  "_Let"        :: "[letbinds, 'a] => 'a"
nipkow@15469
    18
  ("(\<^raw:\textsf{>let\<^raw:}> (_)/ \<^raw:\textsf{>in\<^raw:}> (_))" 10)
nipkow@15469
    19
nipkow@15469
    20
  "_case_syntax":: "['a, cases_syn] => 'b"
nipkow@15469
    21
  ("(\<^raw:\textsf{>case\<^raw:}> _ \<^raw:\textsf{>of\<^raw:}>/ _)" 10)
nipkow@15469
    22
nipkow@15469
    23
(* SETS *)
nipkow@15469
    24
nipkow@15469
    25
(* empty set *)
nipkow@15469
    26
syntax (latex output)
nipkow@15469
    27
  "_emptyset" :: "'a set"              ("\<emptyset>")
nipkow@15469
    28
translations
nipkow@15469
    29
  "_emptyset"      <= "{}"
nipkow@15469
    30
nipkow@15469
    31
(* insert *)
nipkow@15469
    32
translations 
nipkow@15469
    33
  "{x} \<union> A" <= "insert x A"
nipkow@15690
    34
  "{x,y}" <= "{x} \<union> {y}"
nipkow@15469
    35
  "{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)"
nipkow@15476
    36
  "{x}" <= "{x} \<union> _emptyset"
nipkow@15469
    37
nipkow@15469
    38
(* set comprehension *)
nipkow@15469
    39
syntax (latex output)
nipkow@15469
    40
  "_Collect" :: "pttrn => bool => 'a set"              ("(1{_ | _})")
nipkow@15469
    41
translations
nipkow@15469
    42
  "_Collect p P"      <= "{p. P}"
nipkow@15690
    43
  "_Collect p P"      <= "{p|xs. P}"
nipkow@15469
    44
nipkow@15469
    45
(* LISTS *)
nipkow@15469
    46
nipkow@15469
    47
(* Cons *)
nipkow@15469
    48
syntax (latex)
nipkow@15469
    49
  Cons :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" ("_\<cdot>/_" [66,65] 65)
nipkow@15469
    50
nipkow@15469
    51
(* length *)
nipkow@15469
    52
syntax (latex output)
nipkow@15469
    53
  length :: "'a list \<Rightarrow> nat" ("|_|")
nipkow@15469
    54
nipkow@15469
    55
(* nth *)
nipkow@15469
    56
syntax (latex output)
nipkow@15469
    57
  nth :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" ("_\<^raw:\ensuremath{_{[\mathit{>_\<^raw:}]}}>" [1000,0] 1000)
nipkow@15469
    58
nipkow@15469
    59
(* DUMMY *)
nipkow@15469
    60
consts DUMMY :: 'a ("\<^raw:\_>")
nipkow@15469
    61
nipkow@15469
    62
(* THEOREMS *)
nipkow@15469
    63
syntax (Rule output)
nipkow@15469
    64
  "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
nipkow@15469
    65
  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
nipkow@15469
    66
nipkow@15469
    67
  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
nipkow@15469
    68
  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
nipkow@15469
    69
nipkow@15469
    70
  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
nipkow@15469
    71
  ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
nipkow@15469
    72
nipkow@15469
    73
  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
nipkow@15469
    74
nipkow@15469
    75
syntax (IfThen output)
nipkow@15469
    76
  "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
nipkow@15469
    77
  ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
nipkow@15469
    78
  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
nipkow@15469
    79
  ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
nipkow@15469
    80
  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _")
nipkow@15469
    81
  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
nipkow@15469
    82
nipkow@15469
    83
syntax (IfThenNoBox output)
nipkow@15469
    84
  "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
nipkow@15469
    85
  ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
nipkow@15469
    86
  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
nipkow@15469
    87
  ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
nipkow@15469
    88
  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _")
nipkow@15469
    89
  "_asm" :: "prop \<Rightarrow> asms" ("_")
nipkow@15469
    90
nipkow@15469
    91
end
nipkow@15469
    92
(*>*)