src/HOL/Library/LaTeXsugar.thy
author schirmer
Fri Feb 16 11:00:47 2007 +0100 (2007-02-16)
changeset 22328 cc403d881873
parent 21210 c17fd2df4e9e
child 25467 bba589a88022
permissions -rw-r--r--
added print-mode Axiom to print theorems without premises with a rule on top.
     1 (*  Title:      HOL/Library/LaTeXsugar.thy
     2     ID:         $Id$
     3     Author:     Gerwin Klain, Tobias Nipkow, Norbert Schirmer
     4     Copyright   2005 NICTA and TUM
     5 *)
     6 
     7 (*<*)
     8 theory LaTeXsugar
     9 imports Main
    10 begin
    11 
    12 (* LOGIC *)
    13 notation (latex output)
    14   If  ("(\<^raw:\textsf{>if\<^raw:}> (_)/ \<^raw:\textsf{>then\<^raw:}> (_)/ \<^raw:\textsf{>else\<^raw:}> (_))" 10)
    15 
    16 syntax (latex output)
    17 
    18   "_Let"        :: "[letbinds, 'a] => 'a"
    19   ("(\<^raw:\textsf{>let\<^raw:}> (_)/ \<^raw:\textsf{>in\<^raw:}> (_))" 10)
    20 
    21   "_case_syntax":: "['a, cases_syn] => 'b"
    22   ("(\<^raw:\textsf{>case\<^raw:}> _ \<^raw:\textsf{>of\<^raw:}>/ _)" 10)
    23 
    24 (* should become standard syntax once x-symbols supports it *)
    25 syntax (latex)
    26   nexists :: "('a => bool) => bool"           (binder "\<nexists>" 10)
    27 translations
    28   "\<nexists>x. P" <= "\<not>(\<exists>x. P)"
    29 
    30 (* SETS *)
    31 
    32 (* empty set *)
    33 syntax (latex output)
    34   "_emptyset" :: "'a set"              ("\<emptyset>")
    35 translations
    36   "_emptyset"      <= "{}"
    37 
    38 (* insert *)
    39 translations 
    40   "{x} \<union> A" <= "insert x A"
    41   "{x,y}" <= "{x} \<union> {y}"
    42   "{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)"
    43   "{x}" <= "{x} \<union> _emptyset"
    44 
    45 (* set comprehension *)
    46 syntax (latex output)
    47   "_Collect" :: "pttrn => bool => 'a set"              ("(1{_ | _})")
    48 translations
    49   "_Collect p P"      <= "{p. P}"
    50   "_Collect p P"      <= "{p|xs. P}"
    51 
    52 (* LISTS *)
    53 
    54 (* Cons *)
    55 notation (latex)
    56   Cons  ("_\<cdot>/_" [66,65] 65)
    57 
    58 (* length *)
    59 notation (latex output)
    60   length  ("|_|")
    61 
    62 (* nth *)
    63 notation (latex output)
    64   nth  ("_\<^raw:\ensuremath{_{[\mathit{>_\<^raw:}]}}>" [1000,0] 1000)
    65 
    66 (* DUMMY *)
    67 consts DUMMY :: 'a ("\<^raw:\_>")
    68 
    69 (* THEOREMS *)
    70 syntax (Rule output)
    71   "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
    72   ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
    73 
    74   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    75   ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
    76 
    77   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
    78   ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
    79 
    80   "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
    81 
    82 syntax (Axiom output)
    83   "Trueprop" :: "bool \<Rightarrow> prop"
    84   ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
    85 
    86 syntax (IfThen output)
    87   "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
    88   ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
    89   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    90   ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
    91   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _")
    92   "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
    93 
    94 syntax (IfThenNoBox output)
    95   "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
    96   ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
    97   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    98   ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
    99   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _")
   100   "_asm" :: "prop \<Rightarrow> asms" ("_")
   101 
   102 end
   103 (*>*)