src/HOL/Library/LaTeXsugar.thy
author nipkow
Sun Apr 10 11:42:07 2005 +0200 (2005-04-10)
changeset 15690 1da2cfd1ca45
parent 15476 b8cb20cc0c0b
child 16110 c423bb89186d
permissions -rw-r--r--
tuned
     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 syntax (latex output)
    14   If            :: "[bool, 'a, 'a] => 'a"
    15   ("(\<^raw:\textsf{>if\<^raw:}> (_)/ \<^raw:\textsf{>then\<^raw:}> (_)/ \<^raw:\textsf{>else\<^raw:}> (_))" 10)
    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 (* SETS *)
    24 
    25 (* empty set *)
    26 syntax (latex output)
    27   "_emptyset" :: "'a set"              ("\<emptyset>")
    28 translations
    29   "_emptyset"      <= "{}"
    30 
    31 (* insert *)
    32 translations 
    33   "{x} \<union> A" <= "insert x A"
    34   "{x,y}" <= "{x} \<union> {y}"
    35   "{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)"
    36   "{x}" <= "{x} \<union> _emptyset"
    37 
    38 (* set comprehension *)
    39 syntax (latex output)
    40   "_Collect" :: "pttrn => bool => 'a set"              ("(1{_ | _})")
    41 translations
    42   "_Collect p P"      <= "{p. P}"
    43   "_Collect p P"      <= "{p|xs. P}"
    44 
    45 (* LISTS *)
    46 
    47 (* Cons *)
    48 syntax (latex)
    49   Cons :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" ("_\<cdot>/_" [66,65] 65)
    50 
    51 (* length *)
    52 syntax (latex output)
    53   length :: "'a list \<Rightarrow> nat" ("|_|")
    54 
    55 (* nth *)
    56 syntax (latex output)
    57   nth :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" ("_\<^raw:\ensuremath{_{[\mathit{>_\<^raw:}]}}>" [1000,0] 1000)
    58 
    59 (* DUMMY *)
    60 consts DUMMY :: 'a ("\<^raw:\_>")
    61 
    62 (* THEOREMS *)
    63 syntax (Rule output)
    64   "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
    65   ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
    66 
    67   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    68   ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
    69 
    70   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
    71   ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
    72 
    73   "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
    74 
    75 syntax (IfThen output)
    76   "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
    77   ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
    78   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    79   ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
    80   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _")
    81   "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
    82 
    83 syntax (IfThenNoBox output)
    84   "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
    85   ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
    86   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    87   ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
    88   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _")
    89   "_asm" :: "prop \<Rightarrow> asms" ("_")
    90 
    91 end
    92 (*>*)