|
1 theory LaTeXsugar |
|
2 imports Main |
|
3 begin |
|
4 |
|
5 (* LOGIC *) |
|
6 syntax (latex output) |
|
7 If :: "[bool, 'a, 'a] => 'a" |
|
8 ("(\<^raw:\textsf{>if\<^raw:}> (_)/ \<^raw:\textsf{>then\<^raw:}> (_)/ \<^raw:\textsf{>else\<^raw:}> (_))" 10) |
|
9 |
|
10 "_Let" :: "[letbinds, 'a] => 'a" |
|
11 ("(\<^raw:\textsf{>let\<^raw:}> (_)/ \<^raw:\textsf{>in\<^raw:}> (_))" 10) |
|
12 |
|
13 "_case_syntax":: "['a, cases_syn] => 'b" |
|
14 ("(\<^raw:\textsf{>case\<^raw:}> _ \<^raw:\textsf{>of\<^raw:}>/ _)" 10) |
|
15 |
|
16 (* SETS *) |
|
17 |
|
18 (* empty set *) |
|
19 syntax (latex output) |
|
20 "_emptyset" :: "'a set" ("\<emptyset>") |
|
21 translations |
|
22 "_emptyset" <= "{}" |
|
23 |
|
24 (* insert *) |
|
25 translations |
|
26 "{x} \<union> A" <= "insert x A" |
|
27 "{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)" |
|
28 |
|
29 (* set comprehension *) |
|
30 syntax (latex output) |
|
31 "_Collect" :: "pttrn => bool => 'a set" ("(1{_ | _})") |
|
32 translations |
|
33 "_Collect p P" <= "{p. P}" |
|
34 |
|
35 (* LISTS *) |
|
36 |
|
37 (* Cons *) |
|
38 syntax (latex) |
|
39 Cons :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" ("_\<cdot>/_" [66,65] 65) |
|
40 |
|
41 (* length *) |
|
42 syntax (latex output) |
|
43 length :: "'a list \<Rightarrow> nat" ("|_|") |
|
44 |
|
45 (* nth *) |
|
46 syntax (latex output) |
|
47 nth :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" ("_\<^raw:$_{[\mathit{>_\<^raw:}]}$>" [1000,0] 1000) |
|
48 |
|
49 (* append |
|
50 syntax (latex output) |
|
51 "appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" ("_ \<^raw:\isacharat>/ _" [65,66] 65) |
|
52 translations |
|
53 "appendL xs ys" <= "xs @ ys" |
|
54 "appendL (appendL xs ys) zs" <= "appendL xs (appendL ys zs)" |
|
55 *) |
|
56 |
|
57 (* THEOREMS *) |
|
58 syntax (Rule output) |
|
59 "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop" |
|
60 ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{>_\<^raw:}>") |
|
61 |
|
62 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" |
|
63 ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{>_\<^raw:}>") |
|
64 |
|
65 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" |
|
66 ("_\<^raw:\\>/ _") |
|
67 |
|
68 "_asm" :: "prop \<Rightarrow> asms" ("_") |
|
69 |
|
70 syntax (IfThen output) |
|
71 "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop" |
|
72 ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.") |
|
73 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" |
|
74 ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.") |
|
75 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _") |
|
76 "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>") |
|
77 |
|
78 syntax (IfThenNoBox output) |
|
79 "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop" |
|
80 ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.") |
|
81 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" |
|
82 ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.") |
|
83 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _") |
|
84 "_asm" :: "prop \<Rightarrow> asms" ("_") |
|
85 |
|
86 end |