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)


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