15469
|
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} \<union> A" <= "{x} \<union> ({y} \<union> A)"
|
15476
|
35 |
"{x}" <= "{x} \<union> _emptyset"
|
15469
|
36 |
|
|
37 |
(* set comprehension *)
|
|
38 |
syntax (latex output)
|
|
39 |
"_Collect" :: "pttrn => bool => 'a set" ("(1{_ | _})")
|
|
40 |
translations
|
|
41 |
"_Collect p P" <= "{p. P}"
|
|
42 |
|
|
43 |
(* LISTS *)
|
|
44 |
|
|
45 |
(* Cons *)
|
|
46 |
syntax (latex)
|
|
47 |
Cons :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" ("_\<cdot>/_" [66,65] 65)
|
|
48 |
|
|
49 |
(* length *)
|
|
50 |
syntax (latex output)
|
|
51 |
length :: "'a list \<Rightarrow> nat" ("|_|")
|
|
52 |
|
|
53 |
(* nth *)
|
|
54 |
syntax (latex output)
|
|
55 |
nth :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" ("_\<^raw:\ensuremath{_{[\mathit{>_\<^raw:}]}}>" [1000,0] 1000)
|
|
56 |
|
|
57 |
(* DUMMY *)
|
|
58 |
consts DUMMY :: 'a ("\<^raw:\_>")
|
|
59 |
|
|
60 |
(* THEOREMS *)
|
|
61 |
syntax (Rule output)
|
|
62 |
"==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
|
|
63 |
("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
|
|
64 |
|
|
65 |
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
|
|
66 |
("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
|
|
67 |
|
|
68 |
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms"
|
|
69 |
("\<^raw:\mbox{>_\<^raw:}\\>/ _")
|
|
70 |
|
|
71 |
"_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
|
|
72 |
|
|
73 |
syntax (IfThen output)
|
|
74 |
"==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
|
|
75 |
("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
|
|
76 |
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
|
|
77 |
("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
|
|
78 |
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _")
|
|
79 |
"_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
|
|
80 |
|
|
81 |
syntax (IfThenNoBox output)
|
|
82 |
"==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
|
|
83 |
("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
|
|
84 |
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
|
|
85 |
("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
|
|
86 |
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _")
|
|
87 |
"_asm" :: "prop \<Rightarrow> asms" ("_")
|
|
88 |
|
|
89 |
end
|
|
90 |
(*>*) |