src/HOL/Library/LaTeXsugar.thy
author wenzelm
Sun Feb 21 20:54:07 2010 +0100 (2010-02-21)
changeset 35251 e244adbbc28f
parent 31462 4fcbf17b5a98
child 41757 7bbd11360bd3
permissions -rw-r--r--
modernized notation -- to make it work for authentic syntax;
     1 (*  Title:      HOL/Library/LaTeXsugar.thy
     2     Author:     Gerwin Klain, 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 translations
    46   "_Collect p P"      <= "{p. P}"
    47   "_Collect p P"      <= "{p|xs. P}"
    48 
    49 (* LISTS *)
    50 
    51 (* Cons *)
    52 notation (latex)
    53   Cons  ("_\<cdot>/_" [66,65] 65)
    54 
    55 (* length *)
    56 notation (latex output)
    57   length  ("|_|")
    58 
    59 (* nth *)
    60 notation (latex output)
    61   nth  ("_\<^raw:\ensuremath{_{[\mathit{>_\<^raw:}]}}>" [1000,0] 1000)
    62 
    63 (* DUMMY *)
    64 consts DUMMY :: 'a ("\<^raw:\_>")
    65 
    66 (* THEOREMS *)
    67 notation (Rule output)
    68   "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
    69 
    70 syntax (Rule output)
    71   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    72   ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
    73 
    74   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
    75   ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
    76 
    77   "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
    78 
    79 notation (Axiom output)
    80   "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
    81 
    82 notation (IfThen output)
    83   "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    84 syntax (IfThen output)
    85   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    86   ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    87   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
    88   "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
    89 
    90 notation (IfThenNoBox output)
    91   "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    92 syntax (IfThenNoBox output)
    93   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    94   ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    95   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
    96   "_asm" :: "prop \<Rightarrow> asms" ("_")
    97 
    98 end
    99 (*>*)