Theory LaTeXsugar

(*  Title:      HOL/Library/LaTeXsugar.thy
    Author:     Gerwin Klein, 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)


(* 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{_ | _})")
  "_CollectIn" :: "pttrn => 'a set => bool => 'a set"   ("(1{_ ∈ _ | _})")
translations
  "_Collect p P"      <= "{p. P}"
  "_Collect p P"      <= "{p|xs. P}"
  "_CollectIn p A P"  <= "{p : A. P}"

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

(* 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)
  Pure.imp  ("\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)
  Pure.imp  ("{\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)
  Pure.imp  ("{\normalsize{}If\,} _/ {\normalsize \,then\,}/ _.")
syntax (IfThenNoBox output)
  "_bigimpl" :: "asms ⇒ prop ⇒ prop"
  ("{\normalsize{}If\,} _ /{\normalsize \,then\,}/ _.")
  "_asms" :: "prop ⇒ asms ⇒ asms" ("_ /{\normalsize \,and\,}/ _")
  "_asm" :: "prop ⇒ asms" ("_")

setup‹
  let
    fun pretty ctxt c =
      let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c
      in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
            Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
      end
  in
    Thy_Output.antiquotation @{binding "const_typ"}
     (Scan.lift Args.name_inner_syntax)
       (fn {source = src, context = ctxt, ...} => fn arg =>
          Thy_Output.output ctxt
            (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
  end;
›

end
(*>*)