# Theory LaTeXsugar

theory LaTeXsugar
imports Main
```(*  Title:      HOL/Library/LaTeXsugar.thy
Author:     Gerwin Klein, Tobias Nipkow, Norbert Schirmer
*)

(*<*)
theory LaTeXsugar
imports Main
begin

(* LOGIC *)
notation (latex output)
If  ("(\<^latex>‹\\textsf{›if\<^latex>‹}› (_)/ \<^latex>‹\\textsf{›then\<^latex>‹}› (_)/ \<^latex>‹\\textsf{›else\<^latex>‹}› (_))" 10)

syntax (latex output)

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

"_case_syntax":: "['a, cases_syn] => 'b"
("(\<^latex>‹\\textsf{›case\<^latex>‹}› _ \<^latex>‹\\textsf{›of\<^latex>‹}›/ _)" 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  ("_\<^latex>‹\\ensuremath{_{[\\mathit{›_\<^latex>‹}]}}›" [1000,0] 1000)

(* DUMMY *)
consts DUMMY :: 'a ("\<^latex>‹\\_›")

(* THEOREMS *)
notation (Rule output)
Pure.imp  ("\<^latex>‹\\mbox{}\\inferrule{\\mbox{›_\<^latex>‹}}›\<^latex>‹{\\mbox{›_\<^latex>‹}}›")

syntax (Rule output)
"_bigimpl" :: "asms ⇒ prop ⇒ prop"
("\<^latex>‹\\mbox{}\\inferrule{›_\<^latex>‹}›\<^latex>‹{\\mbox{›_\<^latex>‹}}›")

"_asms" :: "prop ⇒ asms ⇒ asms"
("\<^latex>‹\\mbox{›_\<^latex>‹}\\\\›/ _")

"_asm" :: "prop ⇒ asms" ("\<^latex>‹\\mbox{›_\<^latex>‹}›")

notation (Axiom output)
"Trueprop"  ("\<^latex>‹\\mbox{}\\inferrule{\\mbox{}}{\\mbox{›_\<^latex>‹}}›")

notation (IfThen output)
Pure.imp  ("\<^latex>‹{\\normalsize{}›If\<^latex>‹\\,}› _/ \<^latex>‹{\\normalsize \\,›then\<^latex>‹\\,}›/ _.")
syntax (IfThen output)
"_bigimpl" :: "asms ⇒ prop ⇒ prop"
("\<^latex>‹{\\normalsize{}›If\<^latex>‹\\,}› _ /\<^latex>‹{\\normalsize \\,›then\<^latex>‹\\,}›/ _.")
"_asms" :: "prop ⇒ asms ⇒ asms" ("\<^latex>‹\\mbox{›_\<^latex>‹}› /\<^latex>‹{\\normalsize \\,›and\<^latex>‹\\,}›/ _")
"_asm" :: "prop ⇒ asms" ("\<^latex>‹\\mbox{›_\<^latex>‹}›")

notation (IfThenNoBox output)
Pure.imp  ("\<^latex>‹{\\normalsize{}›If\<^latex>‹\\,}› _/ \<^latex>‹{\\normalsize \\,›then\<^latex>‹\\,}›/ _.")
syntax (IfThenNoBox output)
"_bigimpl" :: "asms ⇒ prop ⇒ prop"
("\<^latex>‹{\\normalsize{}›If\<^latex>‹\\,}› _ /\<^latex>‹{\\normalsize \\,›then\<^latex>‹\\,}›/ _.")
"_asms" :: "prop ⇒ asms ⇒ asms" ("_ /\<^latex>‹{\\normalsize \\,›and\<^latex>‹\\,}›/ _")
"_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.embedded_inner_syntax)
(fn {source = src, context = ctxt, ...} => fn arg =>
Thy_Output.output ctxt
(Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
end;
›

setup‹
let
fun dummy_pats (wrap \$ (eq \$ lhs \$ rhs)) =
let
val rhs_vars = Term.add_vars rhs [];
fun dummy (v as Var (ixn as (_, T))) =
if member (op = ) rhs_vars ixn then v else Const (@{const_name DUMMY}, T)
| dummy (t \$ u) = dummy t \$ dummy u
| dummy (Abs (n, T, b)) = Abs (n, T, dummy b)
| dummy t = t;
in wrap \$ (eq \$ dummy lhs \$ rhs) end
in
Term_Style.setup @{binding dummy_pats} (Scan.succeed (K dummy_pats))
end
›

end
(*>*)
```