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