src/HOL/Library/LaTeXsugar.thy
author nipkow
Fri, 28 Sep 2012 08:39:48 +0200
changeset 49628 8262d35eff20
parent 41757 7bbd11360bd3
child 55077 4cf280104b85
child 55111 5792f5106c40
permissions -rw-r--r--
new antiquotation const_typ
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15469
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/Library/LaTeXsugar.thy
nipkow
parents:
diff changeset
     2
    Author:     Gerwin Klain, Tobias Nipkow, Norbert Schirmer
nipkow
parents:
diff changeset
     3
    Copyright   2005 NICTA and TUM
nipkow
parents:
diff changeset
     4
*)
nipkow
parents:
diff changeset
     5
nipkow
parents:
diff changeset
     6
(*<*)
nipkow
parents:
diff changeset
     7
theory LaTeXsugar
30663
0b6aff7451b2 Main is (Complex_Main) base entry point in library theories
haftmann
parents: 30304
diff changeset
     8
imports Main
15469
nipkow
parents:
diff changeset
     9
begin
nipkow
parents:
diff changeset
    10
nipkow
parents:
diff changeset
    11
(* LOGIC *)
21210
c17fd2df4e9e renamed 'const_syntax' to 'notation';
wenzelm
parents: 19674
diff changeset
    12
notation (latex output)
19674
22b635240905 const_syntax;
wenzelm
parents: 16110
diff changeset
    13
  If  ("(\<^raw:\textsf{>if\<^raw:}> (_)/ \<^raw:\textsf{>then\<^raw:}> (_)/ \<^raw:\textsf{>else\<^raw:}> (_))" 10)
22b635240905 const_syntax;
wenzelm
parents: 16110
diff changeset
    14
15469
nipkow
parents:
diff changeset
    15
syntax (latex output)
nipkow
parents:
diff changeset
    16
nipkow
parents:
diff changeset
    17
  "_Let"        :: "[letbinds, 'a] => 'a"
nipkow
parents:
diff changeset
    18
  ("(\<^raw:\textsf{>let\<^raw:}> (_)/ \<^raw:\textsf{>in\<^raw:}> (_))" 10)
nipkow
parents:
diff changeset
    19
nipkow
parents:
diff changeset
    20
  "_case_syntax":: "['a, cases_syn] => 'b"
nipkow
parents:
diff changeset
    21
  ("(\<^raw:\textsf{>case\<^raw:}> _ \<^raw:\textsf{>of\<^raw:}>/ _)" 10)
nipkow
parents:
diff changeset
    22
16110
c423bb89186d added \nexists
nipkow
parents: 15690
diff changeset
    23
(* should become standard syntax once x-symbols supports it *)
c423bb89186d added \nexists
nipkow
parents: 15690
diff changeset
    24
syntax (latex)
c423bb89186d added \nexists
nipkow
parents: 15690
diff changeset
    25
  nexists :: "('a => bool) => bool"           (binder "\<nexists>" 10)
c423bb89186d added \nexists
nipkow
parents: 15690
diff changeset
    26
translations
c423bb89186d added \nexists
nipkow
parents: 15690
diff changeset
    27
  "\<nexists>x. P" <= "\<not>(\<exists>x. P)"
c423bb89186d added \nexists
nipkow
parents: 15690
diff changeset
    28
15469
nipkow
parents:
diff changeset
    29
(* SETS *)
nipkow
parents:
diff changeset
    30
nipkow
parents:
diff changeset
    31
(* empty set *)
27688
397de75836a1 *** empty log message ***
nipkow
parents: 27487
diff changeset
    32
notation (latex)
30304
d8e4cd2ac2a1 set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents: 29493
diff changeset
    33
  "Set.empty" ("\<emptyset>")
15469
nipkow
parents:
diff changeset
    34
nipkow
parents:
diff changeset
    35
(* insert *)
nipkow
parents:
diff changeset
    36
translations 
31462
4fcbf17b5a98 Set.insert with authentic syntax
haftmann
parents: 30663
diff changeset
    37
  "{x} \<union> A" <= "CONST insert x A"
15690
nipkow
parents: 15476
diff changeset
    38
  "{x,y}" <= "{x} \<union> {y}"
15469
nipkow
parents:
diff changeset
    39
  "{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)"
27688
397de75836a1 *** empty log message ***
nipkow
parents: 27487
diff changeset
    40
  "{x}" <= "{x} \<union> \<emptyset>"
15469
nipkow
parents:
diff changeset
    41
nipkow
parents:
diff changeset
    42
(* set comprehension *)
nipkow
parents:
diff changeset
    43
syntax (latex output)
nipkow
parents:
diff changeset
    44
  "_Collect" :: "pttrn => bool => 'a set"              ("(1{_ | _})")
41757
7bbd11360bd3 more pretty set comprehension sugar
nipkow
parents: 35251
diff changeset
    45
  "_CollectIn" :: "pttrn => 'a set => bool => 'a set"   ("(1{_ \<in> _ | _})")
15469
nipkow
parents:
diff changeset
    46
translations
nipkow
parents:
diff changeset
    47
  "_Collect p P"      <= "{p. P}"
15690
nipkow
parents: 15476
diff changeset
    48
  "_Collect p P"      <= "{p|xs. P}"
41757
7bbd11360bd3 more pretty set comprehension sugar
nipkow
parents: 35251
diff changeset
    49
  "_CollectIn p A P"  <= "{p : A. P}"
15469
nipkow
parents:
diff changeset
    50
nipkow
parents:
diff changeset
    51
(* LISTS *)
nipkow
parents:
diff changeset
    52
nipkow
parents:
diff changeset
    53
(* Cons *)
21210
c17fd2df4e9e renamed 'const_syntax' to 'notation';
wenzelm
parents: 19674
diff changeset
    54
notation (latex)
19674
22b635240905 const_syntax;
wenzelm
parents: 16110
diff changeset
    55
  Cons  ("_\<cdot>/_" [66,65] 65)
15469
nipkow
parents:
diff changeset
    56
nipkow
parents:
diff changeset
    57
(* length *)
21210
c17fd2df4e9e renamed 'const_syntax' to 'notation';
wenzelm
parents: 19674
diff changeset
    58
notation (latex output)
19674
22b635240905 const_syntax;
wenzelm
parents: 16110
diff changeset
    59
  length  ("|_|")
15469
nipkow
parents:
diff changeset
    60
nipkow
parents:
diff changeset
    61
(* nth *)
21210
c17fd2df4e9e renamed 'const_syntax' to 'notation';
wenzelm
parents: 19674
diff changeset
    62
notation (latex output)
19674
22b635240905 const_syntax;
wenzelm
parents: 16110
diff changeset
    63
  nth  ("_\<^raw:\ensuremath{_{[\mathit{>_\<^raw:}]}}>" [1000,0] 1000)
15469
nipkow
parents:
diff changeset
    64
nipkow
parents:
diff changeset
    65
(* DUMMY *)
nipkow
parents:
diff changeset
    66
consts DUMMY :: 'a ("\<^raw:\_>")
nipkow
parents:
diff changeset
    67
nipkow
parents:
diff changeset
    68
(* THEOREMS *)
35251
e244adbbc28f modernized notation -- to make it work for authentic syntax;
wenzelm
parents: 31462
diff changeset
    69
notation (Rule output)
e244adbbc28f modernized notation -- to make it work for authentic syntax;
wenzelm
parents: 31462
diff changeset
    70
  "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
e244adbbc28f modernized notation -- to make it work for authentic syntax;
wenzelm
parents: 31462
diff changeset
    71
15469
nipkow
parents:
diff changeset
    72
syntax (Rule output)
nipkow
parents:
diff changeset
    73
  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
nipkow
parents:
diff changeset
    74
  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
nipkow
parents:
diff changeset
    75
nipkow
parents:
diff changeset
    76
  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
nipkow
parents:
diff changeset
    77
  ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
nipkow
parents:
diff changeset
    78
nipkow
parents:
diff changeset
    79
  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
nipkow
parents:
diff changeset
    80
35251
e244adbbc28f modernized notation -- to make it work for authentic syntax;
wenzelm
parents: 31462
diff changeset
    81
notation (Axiom output)
e244adbbc28f modernized notation -- to make it work for authentic syntax;
wenzelm
parents: 31462
diff changeset
    82
  "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
22328
cc403d881873 added print-mode Axiom to print theorems without premises with a rule on top.
schirmer
parents: 21210
diff changeset
    83
35251
e244adbbc28f modernized notation -- to make it work for authentic syntax;
wenzelm
parents: 31462
diff changeset
    84
notation (IfThen output)
e244adbbc28f modernized notation -- to make it work for authentic syntax;
wenzelm
parents: 31462
diff changeset
    85
  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
15469
nipkow
parents:
diff changeset
    86
syntax (IfThen output)
nipkow
parents:
diff changeset
    87
  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
25467
bba589a88022 Removed forced roman font in mode=IfThen.
nipkow
parents: 22328
diff changeset
    88
  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
bba589a88022 Removed forced roman font in mode=IfThen.
nipkow
parents: 22328
diff changeset
    89
  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
15469
nipkow
parents:
diff changeset
    90
  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
nipkow
parents:
diff changeset
    91
35251
e244adbbc28f modernized notation -- to make it work for authentic syntax;
wenzelm
parents: 31462
diff changeset
    92
notation (IfThenNoBox output)
e244adbbc28f modernized notation -- to make it work for authentic syntax;
wenzelm
parents: 31462
diff changeset
    93
  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
15469
nipkow
parents:
diff changeset
    94
syntax (IfThenNoBox output)
nipkow
parents:
diff changeset
    95
  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
25467
bba589a88022 Removed forced roman font in mode=IfThen.
nipkow
parents: 22328
diff changeset
    96
  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
bba589a88022 Removed forced roman font in mode=IfThen.
nipkow
parents: 22328
diff changeset
    97
  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
15469
nipkow
parents:
diff changeset
    98
  "_asm" :: "prop \<Rightarrow> asms" ("_")
nipkow
parents:
diff changeset
    99
49628
8262d35eff20 new antiquotation const_typ
nipkow
parents: 41757
diff changeset
   100
setup{*
8262d35eff20 new antiquotation const_typ
nipkow
parents: 41757
diff changeset
   101
  let
8262d35eff20 new antiquotation const_typ
nipkow
parents: 41757
diff changeset
   102
    fun pretty ctxt c =
8262d35eff20 new antiquotation const_typ
nipkow
parents: 41757
diff changeset
   103
      let val tc = Proof_Context.read_const_proper ctxt false c
8262d35eff20 new antiquotation const_typ
nipkow
parents: 41757
diff changeset
   104
      in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
8262d35eff20 new antiquotation const_typ
nipkow
parents: 41757
diff changeset
   105
            Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
8262d35eff20 new antiquotation const_typ
nipkow
parents: 41757
diff changeset
   106
      end
8262d35eff20 new antiquotation const_typ
nipkow
parents: 41757
diff changeset
   107
  in
8262d35eff20 new antiquotation const_typ
nipkow
parents: 41757
diff changeset
   108
    Thy_Output.antiquotation @{binding "const_typ"}
8262d35eff20 new antiquotation const_typ
nipkow
parents: 41757
diff changeset
   109
     (Scan.lift Args.name_source)
8262d35eff20 new antiquotation const_typ
nipkow
parents: 41757
diff changeset
   110
       (fn {source = src, context = ctxt, ...} => fn arg =>
8262d35eff20 new antiquotation const_typ
nipkow
parents: 41757
diff changeset
   111
          Thy_Output.output ctxt
8262d35eff20 new antiquotation const_typ
nipkow
parents: 41757
diff changeset
   112
            (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
8262d35eff20 new antiquotation const_typ
nipkow
parents: 41757
diff changeset
   113
  end;
8262d35eff20 new antiquotation const_typ
nipkow
parents: 41757
diff changeset
   114
*}
8262d35eff20 new antiquotation const_typ
nipkow
parents: 41757
diff changeset
   115
15469
nipkow
parents:
diff changeset
   116
end
nipkow
parents:
diff changeset
   117
(*>*)