src/HOL/Library/LaTeXsugar.thy
author nipkow
Mon Jul 28 20:49:07 2008 +0200 (2008-07-28)
changeset 27688 397de75836a1
parent 27487 c8a6ce181805
child 29493 ddcbd5e4041d
permissions -rw-r--r--
*** empty log message ***
     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 Plain "~~/src/HOL/List"
    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 notation (latex)
    34   "{}" ("\<emptyset>")
    35 
    36 (* insert *)
    37 translations 
    38   "{x} \<union> A" <= "insert x A"
    39   "{x,y}" <= "{x} \<union> {y}"
    40   "{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)"
    41   "{x}" <= "{x} \<union> \<emptyset>"
    42 
    43 (* set comprehension *)
    44 syntax (latex output)
    45   "_Collect" :: "pttrn => bool => 'a set"              ("(1{_ | _})")
    46 translations
    47   "_Collect p P"      <= "{p. P}"
    48   "_Collect p P"      <= "{p|xs. P}"
    49 
    50 (* LISTS *)
    51 
    52 (* Cons *)
    53 notation (latex)
    54   Cons  ("_\<cdot>/_" [66,65] 65)
    55 
    56 (* length *)
    57 notation (latex output)
    58   length  ("|_|")
    59 
    60 (* nth *)
    61 notation (latex output)
    62   nth  ("_\<^raw:\ensuremath{_{[\mathit{>_\<^raw:}]}}>" [1000,0] 1000)
    63 
    64 (* DUMMY *)
    65 consts DUMMY :: 'a ("\<^raw:\_>")
    66 
    67 (* THEOREMS *)
    68 syntax (Rule output)
    69   "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
    70   ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
    71 
    72   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    73   ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
    74 
    75   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
    76   ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
    77 
    78   "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
    79 
    80 syntax (Axiom output)
    81   "Trueprop" :: "bool \<Rightarrow> prop"
    82   ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
    83 
    84 syntax (IfThen output)
    85   "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
    86   ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    87   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    88   ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    89   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
    90   "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
    91 
    92 syntax (IfThenNoBox output)
    93   "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
    94   ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    95   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    96   ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    97   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
    98   "_asm" :: "prop \<Rightarrow> asms" ("_")
    99 
   100 end
   101 (*>*)