src/HOL/Library/LaTeXsugar.thy
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 41757 7bbd11360bd3
child 49628 8262d35eff20
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
     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   "_CollectIn" :: "pttrn => 'a set => bool => 'a set"   ("(1{_ \<in> _ | _})")
    46 translations
    47   "_Collect p P"      <= "{p. P}"
    48   "_Collect p P"      <= "{p|xs. P}"
    49   "_CollectIn p A P"  <= "{p : A. P}"
    50 
    51 (* LISTS *)
    52 
    53 (* Cons *)
    54 notation (latex)
    55   Cons  ("_\<cdot>/_" [66,65] 65)
    56 
    57 (* length *)
    58 notation (latex output)
    59   length  ("|_|")
    60 
    61 (* nth *)
    62 notation (latex output)
    63   nth  ("_\<^raw:\ensuremath{_{[\mathit{>_\<^raw:}]}}>" [1000,0] 1000)
    64 
    65 (* DUMMY *)
    66 consts DUMMY :: 'a ("\<^raw:\_>")
    67 
    68 (* THEOREMS *)
    69 notation (Rule output)
    70   "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
    71 
    72 syntax (Rule output)
    73   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    74   ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
    75 
    76   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
    77   ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
    78 
    79   "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
    80 
    81 notation (Axiom output)
    82   "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
    83 
    84 notation (IfThen output)
    85   "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    86 syntax (IfThen output)
    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 notation (IfThenNoBox output)
    93   "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    94 syntax (IfThenNoBox output)
    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 (*>*)