Theory HOL-Library.LaTeXsugar

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

(*<*)
theory LaTeXsugar
imports Main
begin

(* Boxing *)

definition mbox :: "'a ⇒ 'a" where
"mbox x = x"

definition mbox0 :: "'a ⇒ 'a" where
"mbox0 x = x"

notation (latex) mbox (‹\<^latex>‹\mbox{›_\<^latex>‹}›› [999] 999)

notation (latex) mbox0 (‹\<^latex>‹\mbox{›_\<^latex>‹}›› [0] 999)

(* 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 ‹
  Document_Output.antiquotation_pretty_source_embedded \<^binding>‹const_typ›
    (Scan.lift Parse.embedded_inner_syntax)
    (fn ctxt => fn c =>
      let val tc = Proof_Context.read_const {proper = false, strict = false} ctxt c in
        Pretty.block [Document_Output.pretty_term ctxt tc, Pretty.str " ::",
          Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
      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 ((=) ) 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
›

setup ‹
let

fun eta_expand Ts t xs = case t of
    Abs(x,T,t) =>
      let val (t', xs') = eta_expand (T::Ts) t xs
      in (Abs (x, T, t'), xs') end
  | _ =>
      let
        val (a,ts) = strip_comb t (* assume a atomic *)
        val (ts',xs') = fold_map (eta_expand Ts) ts xs
        val t' = list_comb (a, ts');
        val Bs = binder_types (fastype_of1 (Ts,t));
        val n = Int.min (length Bs, length xs');
        val bs = map Bound ((n - 1) downto 0);
        val xBs = ListPair.zip (xs',Bs);
        val xs'' = drop n xs';
        val t'' = fold_rev Term.abs xBs (list_comb(t', bs))
      in (t'', xs'') end

val style_eta_expand =
  (Scan.repeat Args.name) >> (fn xs => fn ctxt => fn t => fst (eta_expand [] t xs))

in Term_Style.setup \<^binding>‹eta_expand› style_eta_expand end
›

end
(*>*)