Theory SyntaxTweaks

theory SyntaxTweaks 
imports Main
begin

syntax (implnl output)
  "⟹" :: "prop ⇒ prop ⇒ prop" ("_ //⟹ _" [0,1] 1)

notation (holimplnl output)
"implies" ("(2_ ⟶// _)" [0,1] 1)
notation (holimplnl output)
"conj" ("_ ∧/ _" [34,35]35)
  

syntax (letnl output)
  "_binds"      :: "[letbind, letbinds] => letbinds"     ("_;//_")
text ‹Theorems as inference rules, usepackage mathpartir›

syntax (eqindent output) "op =" ::"['a, 'a] => bool"               ( "(2_ =/ _)" [49,50]50)

(* LOGIC *)
syntax (latex output)
  If            :: "[bool, 'a, 'a] => 'a"
  ("(\<^latex>‹\\holkeyword{›if\<^latex>‹}›(_)/ \<^latex>‹\\holkeyword{›then\<^latex>‹}› (_)/ \<^latex>‹\\holkeyword{›else\<^latex>‹}› (_))" 10)

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

  "_case_syntax":: "['a, cases_syn] => 'b"
  ("(\<^latex>‹\\holkeyword{›case\<^latex>‹}› _ \<^latex>‹\\holkeyword{›of\<^latex>‹}›/ _)" 10)

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>‹}}›")

syntax (IfThen output)
  "==>" :: "prop ⇒ prop ⇒ prop"
  ("\<^latex>‹{\\normalsize{}›If\<^latex>‹\\,}› _/ \<^latex>‹{\\normalsize \\,›then\<^latex>‹\\,}›/ _.")

  "_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>‹}›")

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


text ‹power›
syntax (latex output)
  power :: "['a::power, nat] => 'a"           ("_⇗_⇖" [1000,0]80)

(* empty set *)
syntax (latex output)
  "_emptyset" :: "'a set"              ("∅")
translations
  "_emptyset"      <= "{}"

text ‹insert›
translations 
(*
  "{x} ∪ A" <= "insert x A"
*)
  "{x,y}" <= "{x} ∪ {y}"
  "{x,y} ∪ A" <= "{x} ∪ ({y} ∪ A)"
  "{x}" <= "{x} ∪ {}"


syntax (latex output)
 Cons :: "'a ⇒ 'a list ⇒ 'a list"    (infixr "⋅" 65)

syntax (latex output)
 "Some" :: "'a ⇒ 'a option" ("(⌊_⌋)")
 "None" :: "'a option" ("⊥")

text ‹lesser indentation as default›
syntax (latex output)
  "ALL "        :: "[idts, bool] => bool"                ("(2∀_./ _)" [0, 10] 10)
  "EX "         :: "[idts, bool] => bool"                ("(2∃_./ _)" [0, 10] 10)

text ‹space around ∈›
syntax (latex output)
  "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3∀_\<^latex>‹\\,›∈_./ _)" [0, 0, 10] 10)
  "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3∃_\<^latex>‹\\,›∈_./ _)" [0, 0, 10] 10)

text ‹compact line breaking for some infix operators›
term "HOL.conj"
notation (compact output)
"conj" ("_ ∧/ _" [34,35]35)
notation (compact output)
"append" ("_ @/ _" [64,65]65)

text ‹force a newline after definition equation›
syntax (defnl output)
  "=="       :: "[prop, prop] => prop"                ("(2_ ≡// _)" [1,2] 2) 
syntax (defeqnl output)
  "=="       :: "[prop, prop] => prop"                ("(2_ =// _)" [1,2] 2) 
syntax (eqnl output)
  "op ="       :: "['a, 'a] => bool"                     ("(2_ =// _)" [1,2] 2) 
syntax (latex output)
  "=="       :: "[prop, prop] => prop"                ("(2_ ≡/ _)" [1,2] 2) 

text ‹New-line after assumptions›
syntax (asmnl output)
  "_asms" :: "prop ⇒ asms ⇒ asms" 
  ("_; // _")

text ‹uncurry functions›
syntax (uncurry output)
"_cargs" :: "'a ⇒ cargs ⇒ cargs" ("_, _")
"_applC" :: "[('b => 'a), cargs] => logic" ("(1_/(1'(_')))" [1000, 0] 1000)

text ‹but keep curried notation for constructors›
syntax (uncurry output)
"_cargs_curry":: "'a ⇒ cargs ⇒ cargs" ("_ _" [1000,1000] 1000)
"_applC_curry":: "[('b => 'a), cargs] => logic" ("(1_/ _)" [1000, 1000] 999)



text ‹`dot'-selector notation for records›
syntax (latex output)
"_rec_sel" :: "'r ⇒ id ⇒ 'a" ("_._" [1000,1000]1000)


ML_command ‹
  Markup.add_mode Latex.latexN (fn (s, props) =>
    if member (op =) [Markup.boundN, Markup.freeN, Markup.varN, Markup.tfreeN, Markup.tvarN] s
    then YXML.output_markup (Markup.latex_macro (s ^ "ify"))
    else Latex.latex_markup (s, props));
›


text ‹invisible binder in case we want to force "bound"-markup›
consts Bind:: "('a ⇒ 'b) ⇒ 'c" (binder "Bind " 10)
translations
  "f" <= "Bind x. f"


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

(* Optional values *)
notation (latex output)
  None ("⊥")

notation (latex output)
  Some ("⌊_⌋")

(* nth *)
notation (latex output)
  nth  ("_\<^latex>‹\\ensuremath{_{[›_\<^latex>‹]}}›" [1000,0] 1000)

end