new
authornipkow
Wed Jan 26 13:50:59 2005 +0100 (2005-01-26)
changeset 15469f5d22f504ab9
parent 15468 f0138af74b38
child 15470 7e12ad2f6672
new
src/HOL/Library/LaTeXsugar.thy
src/HOL/Library/OptionalSugar.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Wed Jan 26 13:50:59 2005 +0100
     1.3 @@ -0,0 +1,89 @@
     1.4 +(*  Title:      HOL/Library/LaTeXsugar.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Gerwin Klain, Tobias Nipkow, Norbert Schirmer
     1.7 +    Copyright   2005 NICTA and TUM
     1.8 +*)
     1.9 +
    1.10 +(*<*)
    1.11 +theory LaTeXsugar
    1.12 +imports Main
    1.13 +begin
    1.14 +
    1.15 +(* LOGIC *)
    1.16 +syntax (latex output)
    1.17 +  If            :: "[bool, 'a, 'a] => 'a"
    1.18 +  ("(\<^raw:\textsf{>if\<^raw:}> (_)/ \<^raw:\textsf{>then\<^raw:}> (_)/ \<^raw:\textsf{>else\<^raw:}> (_))" 10)
    1.19 +
    1.20 +  "_Let"        :: "[letbinds, 'a] => 'a"
    1.21 +  ("(\<^raw:\textsf{>let\<^raw:}> (_)/ \<^raw:\textsf{>in\<^raw:}> (_))" 10)
    1.22 +
    1.23 +  "_case_syntax":: "['a, cases_syn] => 'b"
    1.24 +  ("(\<^raw:\textsf{>case\<^raw:}> _ \<^raw:\textsf{>of\<^raw:}>/ _)" 10)
    1.25 +
    1.26 +(* SETS *)
    1.27 +
    1.28 +(* empty set *)
    1.29 +syntax (latex output)
    1.30 +  "_emptyset" :: "'a set"              ("\<emptyset>")
    1.31 +translations
    1.32 +  "_emptyset"      <= "{}"
    1.33 +
    1.34 +(* insert *)
    1.35 +translations 
    1.36 +  "{x} \<union> A" <= "insert x A"
    1.37 +  "{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)"
    1.38 +
    1.39 +(* set comprehension *)
    1.40 +syntax (latex output)
    1.41 +  "_Collect" :: "pttrn => bool => 'a set"              ("(1{_ | _})")
    1.42 +translations
    1.43 +  "_Collect p P"      <= "{p. P}"
    1.44 +
    1.45 +(* LISTS *)
    1.46 +
    1.47 +(* Cons *)
    1.48 +syntax (latex)
    1.49 +  Cons :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" ("_\<cdot>/_" [66,65] 65)
    1.50 +
    1.51 +(* length *)
    1.52 +syntax (latex output)
    1.53 +  length :: "'a list \<Rightarrow> nat" ("|_|")
    1.54 +
    1.55 +(* nth *)
    1.56 +syntax (latex output)
    1.57 +  nth :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" ("_\<^raw:\ensuremath{_{[\mathit{>_\<^raw:}]}}>" [1000,0] 1000)
    1.58 +
    1.59 +(* DUMMY *)
    1.60 +consts DUMMY :: 'a ("\<^raw:\_>")
    1.61 +
    1.62 +(* THEOREMS *)
    1.63 +syntax (Rule output)
    1.64 +  "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
    1.65 +  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
    1.66 +
    1.67 +  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    1.68 +  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
    1.69 +
    1.70 +  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
    1.71 +  ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
    1.72 +
    1.73 +  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
    1.74 +
    1.75 +syntax (IfThen output)
    1.76 +  "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
    1.77 +  ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
    1.78 +  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    1.79 +  ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
    1.80 +  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _")
    1.81 +  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
    1.82 +
    1.83 +syntax (IfThenNoBox output)
    1.84 +  "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
    1.85 +  ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
    1.86 +  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    1.87 +  ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
    1.88 +  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _")
    1.89 +  "_asm" :: "prop \<Rightarrow> asms" ("_")
    1.90 +
    1.91 +end
    1.92 +(*>*)
    1.93 \ No newline at end of file
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/OptionalSugar.thy	Wed Jan 26 13:50:59 2005 +0100
     2.3 @@ -0,0 +1,37 @@
     2.4 +(*  Title:      HOL/Library/OptionalSugar.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Gerwin Klain, Tobias Nipkow
     2.7 +    Copyright   2005 NICTA and TUM
     2.8 +*)
     2.9 +
    2.10 +theory OptionalSugar
    2.11 +imports LaTeXsugar
    2.12 +begin
    2.13 +
    2.14 +(* append *)
    2.15 +syntax (latex output)
    2.16 +  "appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65)
    2.17 +translations
    2.18 +  "appendL xs ys" <= "xs @ ys" 
    2.19 +  "appendL (appendL xs ys) zs" <= "appendL xs (appendL ys zs)"
    2.20 +
    2.21 +
    2.22 +(* aligning equations *)
    2.23 +syntax (tab output)
    2.24 +  "op =" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50)
    2.25 +  "==" :: "prop \<Rightarrow> prop \<Rightarrow> prop" ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
    2.26 +
    2.27 +(* Let *)
    2.28 +translations 
    2.29 +  "_bind (p,DUMMY) e" <= "_bind p (fst e)"
    2.30 +  "_bind (DUMMY,p) e" <= "_bind p (snd e)"
    2.31 +
    2.32 +  "_tuple_args x (_tuple_args y z)" ==
    2.33 +    "_tuple_args x (_tuple_arg (_tuple y z))"
    2.34 +
    2.35 +  "_bind (Some p) e" <= "_bind p (the e)"
    2.36 +  "_bind (p#DUMMY) e" <= "_bind p (hd e)"
    2.37 +  "_bind (DUMMY#p) e" <= "_bind p (tl e)"
    2.38 +
    2.39 +
    2.40 +end
    2.41 \ No newline at end of file