Theory LaTeXsugar

theory LaTeXsugar
imports Main
(*  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{_ | _})")
"_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}"

(* 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" ("_")

setup{*
let
fun pretty ctxt c =
let val tc = Proof_Context.read_const_proper ctxt false 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_source)
(fn {source = src, context = ctxt, ...} => fn arg =>
Thy_Output.output ctxt
(Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
end;
*}


end
(*>*)