Theory LaTeXsugar

(*  Title:      HOL/Library/LaTeXsugar.thy
    Author:     Gerwin Klain, Tobias Nipkow, Norbert Schirmer
    Copyright   2005 NICTA and TUM
*)

(*<*)
theory LaTeXsugar
imports Main
begin

(* LOGIC *)
notation (latex output)
  If  ("(\textsf{if} (_)/ \textsf{then} (_)/ \textsf{else} (_))" 10)

syntax (latex output)

  "_Let"        :: "[letbinds, 'a] => 'a"
  ("(\textsf{let} (_)/ \textsf{in} (_))" 10)

  "_case_syntax":: "['a, cases_syn] => 'b"
  ("(\textsf{case} _ \textsf{of}/ _)" 10)

(* should become standard syntax once x-symbols supports it *)
syntax (latex)
  nexists :: "('a => bool) => bool"           (binder "\<nexists>" 10)
translations
  "\<nexists>x. P" <= "¬(∃x. P)"

(* SETS *)

(* empty set *)
notation (latex)
  "Set.empty" ("∅")

(* insert *)
translations 
  "{x} ∪ A" <= "CONST insert x A"
  "{x,y}" <= "{x} ∪ {y}"
  "{x,y} ∪ A" <= "{x} ∪ ({y} ∪ A)"
  "{x}" <= "{x} ∪ ∅"

(* set comprehension *)
syntax (latex output)
  "_Collect" :: "pttrn => bool => 'a set"              ("(1{_ | _})")
translations
  "_Collect p P"      <= "{p. P}"
  "_Collect p P"      <= "{p|xs. P}"

(* LISTS *)

(* Cons *)
notation (latex)
  Cons  ("_·/_" [66,65] 65)

(* length *)
notation (latex output)
  length  ("|_|")

(* nth *)
notation (latex output)
  nth  ("_\ensuremath{_{[\mathit{_}]}}" [1000,0] 1000)

(* DUMMY *)
consts DUMMY :: 'a ("\_")

(* THEOREMS *)
notation (Rule output)
  "==>"  ("\mbox{}\inferrule{\mbox{_}}{\mbox{_}}")

syntax (Rule output)
  "_bigimpl" :: "asms => prop => prop"
  ("\mbox{}\inferrule{_}{\mbox{_}}")

  "_asms" :: "prop => asms => asms" 
  ("\mbox{_}\\/ _")

  "_asm" :: "prop => asms" ("\mbox{_}")

notation (Axiom output)
  "Trueprop"  ("\mbox{}\inferrule{\mbox{}}{\mbox{_}}")

notation (IfThen output)
  "==>"  ("{\normalsize{}If\,} _/ {\normalsize \,then\,}/ _.")
syntax (IfThen output)
  "_bigimpl" :: "asms => prop => prop"
  ("{\normalsize{}If\,} _ /{\normalsize \,then\,}/ _.")
  "_asms" :: "prop => asms => asms" ("\mbox{_} /{\normalsize \,and\,}/ _")
  "_asm" :: "prop => asms" ("\mbox{_}")

notation (IfThenNoBox output)
  "==>"  ("{\normalsize{}If\,} _/ {\normalsize \,then\,}/ _.")
syntax (IfThenNoBox output)
  "_bigimpl" :: "asms => prop => prop"
  ("{\normalsize{}If\,} _ /{\normalsize \,then\,}/ _.")
  "_asms" :: "prop => asms => asms" ("_ /{\normalsize \,and\,}/ _")
  "_asm" :: "prop => asms" ("_")

end
(*>*)