src/HOL/Library/LaTeXsugar.thy
author wenzelm
Mon Dec 28 17:43:30 2015 +0100 (2015-12-28)
changeset 61952 546958347e05
parent 60500 903bb1495239
child 62522 d32c23d29968
permissions -rw-r--r--
prefer symbols for "Union", "Inter";
     1 (*  Title:      HOL/Library/LaTeXsugar.thy
     2     Author:     Gerwin Klein, Tobias Nipkow, Norbert Schirmer
     3     Copyright   2005 NICTA and TUM
     4 *)
     5 
     6 (*<*)
     7 theory LaTeXsugar
     8 imports Main
     9 begin
    10 
    11 (* LOGIC *)
    12 notation (latex output)
    13   If  ("(\<^raw:\textsf{>if\<^raw:}> (_)/ \<^raw:\textsf{>then\<^raw:}> (_)/ \<^raw:\textsf{>else\<^raw:}> (_))" 10)
    14 
    15 syntax (latex output)
    16 
    17   "_Let"        :: "[letbinds, 'a] => 'a"
    18   ("(\<^raw:\textsf{>let\<^raw:}> (_)/ \<^raw:\textsf{>in\<^raw:}> (_))" 10)
    19 
    20   "_case_syntax":: "['a, cases_syn] => 'b"
    21   ("(\<^raw:\textsf{>case\<^raw:}> _ \<^raw:\textsf{>of\<^raw:}>/ _)" 10)
    22 
    23 (* should become standard syntax once x-symbols supports it *)
    24 syntax (latex)
    25   nexists :: "('a => bool) => bool"           (binder "\<nexists>" 10)
    26 translations
    27   "\<nexists>x. P" <= "\<not>(\<exists>x. P)"
    28 
    29 (* SETS *)
    30 
    31 (* empty set *)
    32 notation (latex)
    33   "Set.empty" ("\<emptyset>")
    34 
    35 (* insert *)
    36 translations 
    37   "{x} \<union> A" <= "CONST insert x A"
    38   "{x,y}" <= "{x} \<union> {y}"
    39   "{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)"
    40   "{x}" <= "{x} \<union> \<emptyset>"
    41 
    42 (* set comprehension *)
    43 syntax (latex output)
    44   "_Collect" :: "pttrn => bool => 'a set"              ("(1{_ | _})")
    45   "_CollectIn" :: "pttrn => 'a set => bool => 'a set"   ("(1{_ \<in> _ | _})")
    46 translations
    47   "_Collect p P"      <= "{p. P}"
    48   "_Collect p P"      <= "{p|xs. P}"
    49   "_CollectIn p A P"  <= "{p : A. P}"
    50 
    51 (* card *)
    52 notation (latex output)
    53   card  ("|_|")
    54 
    55 (* LISTS *)
    56 
    57 (* Cons *)
    58 notation (latex)
    59   Cons  ("_ \<cdot>/ _" [66,65] 65)
    60 
    61 (* length *)
    62 notation (latex output)
    63   length  ("|_|")
    64 
    65 (* nth *)
    66 notation (latex output)
    67   nth  ("_\<^raw:\ensuremath{_{[\mathit{>_\<^raw:}]}}>" [1000,0] 1000)
    68 
    69 (* DUMMY *)
    70 consts DUMMY :: 'a ("\<^raw:\_>")
    71 
    72 (* THEOREMS *)
    73 notation (Rule output)
    74   Pure.imp  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
    75 
    76 syntax (Rule output)
    77   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    78   ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
    79 
    80   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
    81   ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
    82 
    83   "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
    84 
    85 notation (Axiom output)
    86   "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
    87 
    88 notation (IfThen output)
    89   Pure.imp  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    90 syntax (IfThen output)
    91   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    92   ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    93   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
    94   "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
    95 
    96 notation (IfThenNoBox output)
    97   Pure.imp  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    98 syntax (IfThenNoBox output)
    99   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
   100   ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
   101   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
   102   "_asm" :: "prop \<Rightarrow> asms" ("_")
   103 
   104 setup\<open>
   105   let
   106     fun pretty ctxt c =
   107       let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c
   108       in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
   109             Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
   110       end
   111   in
   112     Thy_Output.antiquotation @{binding "const_typ"}
   113      (Scan.lift Args.name_inner_syntax)
   114        (fn {source = src, context = ctxt, ...} => fn arg =>
   115           Thy_Output.output ctxt
   116             (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
   117   end;
   118 \<close>
   119 
   120 end
   121 (*>*)