|
15366
|
1 |
theory OptionalSugar
|
|
|
2 |
imports LaTeXsugar
|
|
|
3 |
begin
|
|
|
4 |
|
|
|
5 |
(* append *)
|
|
|
6 |
syntax (latex output)
|
|
|
7 |
"appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65)
|
|
|
8 |
translations
|
|
|
9 |
"appendL xs ys" <= "xs @ ys"
|
|
|
10 |
"appendL (appendL xs ys) zs" <= "appendL xs (appendL ys zs)"
|
|
|
11 |
|
|
|
12 |
|
|
|
13 |
(* and *)
|
|
|
14 |
syntax (latex output)
|
|
|
15 |
"_andL" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "\<^raw:\isasymand>" 35)
|
|
|
16 |
translations
|
|
|
17 |
"_andL A B" <= "A \<and> B"
|
|
|
18 |
"_andL (_andL A B) C" <= "_andL A (_andL B C)"
|
|
|
19 |
|
|
|
20 |
|
|
|
21 |
(* aligning equations *)
|
|
|
22 |
syntax (tab output)
|
|
|
23 |
"op =" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50)
|
|
|
24 |
"==" :: "prop \<Rightarrow> prop \<Rightarrow> prop" ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
|
|
|
25 |
|
|
|
26 |
(* Let *)
|
|
|
27 |
translations
|
|
|
28 |
"_bind (p,DUMMY) e" <= "_bind p (fst e)"
|
|
|
29 |
"_bind (DUMMY,p) e" <= "_bind p (snd e)"
|
|
|
30 |
|
|
|
31 |
"_tuple_args x (_tuple_args y z)" ==
|
|
|
32 |
"_tuple_args x (_tuple_arg (_tuple y z))"
|
|
|
33 |
|
|
|
34 |
"_bind (Some p) e" <= "_bind p (the e)"
|
|
|
35 |
"_bind (p#DUMMY) e" <= "_bind p (hd e)"
|
|
|
36 |
"_bind (DUMMY#p) e" <= "_bind p (tl e)"
|
|
|
37 |
|
|
|
38 |
|
|
|
39 |
end |