-
Notifications
You must be signed in to change notification settings - Fork 1
/
Z_Toolkit_Pretty.thy
67 lines (45 loc) · 1.6 KB
/
Z_Toolkit_Pretty.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
section \<open> Pretty Notation for Z \<close>
theory Z_Toolkit_Pretty
imports Relation_Toolkit Number_Toolkit
abbrevs "+>" = "\<Zpfun>" and "+>" = "\<Zpsurj>" and "++>" = "\<Zffun>"
and ">->" = "\<Zinj>" and ">->" = "\<Zbij>" and ">+>" = "\<Zpinj>" and ">++>" = "\<Zfinj>"
and "<|" = "\<lhd>" and "<|" = "\<Zdres>" and "<|" = "\<Zndres>" and "<|" = "\<lblot>"
and "|>" = "\<rhd>" and "|>" = "\<Zrres>" and "|>" = "\<Znrres>" and "|>" = "\<rblot>"
and "|`" = "\<restriction>" and "|`" = "\<upharpoonleft>" and "|`" = "\<Zproject>"
and "O+" = "\<oplus>"
and ";;" = "\<Zcomp>" and ";;" = "\<Zsemi>"
and "PP" = "\<bbbP>" and "FF" = "\<bbbF>"
begin
declare [[coercion_enabled]]
text \<open> Code generation set up \<close>
code_datatype pfun_of_alist
text \<open> Allow partial functions to be written with braces \<close>
syntax
"_Pfun" :: "maplets => ('a, 'b) pfun" ("(1{_})")
bundle Z_Syntax
begin
unbundle Z_Type_Syntax
notation relcomp (infixr "\<Zcomp>" 75)
end
text \<open> Relation Function Syntax \<close>
bundle Z_RFun_Syntax
begin
unbundle Z_Syntax
no_notation funcset (infixr "\<rightarrow>" 60)
notation rel_tfun (infixr "\<rightarrow>" 60)
notation rel_pfun (infixr "\<Zpfun>" 60)
notation rel_ffun (infixr "\<Zffun>" 60)
end
context
includes Z_RFun_Syntax
begin
subsection \<open> Examples \<close>
typ "\<bbbP> \<nat> \<rightarrow> \<nat>"
typ "\<bbbP> \<nat> \<Zpfun> \<bool>"
term "{}"
term "P \<Zcomp> Q"
term "A \<Zdres> B \<Zndres> (P :: \<bbbP>(\<nat>) \<Zpfun> \<bool>)"
term "\<bbbP> \<nat> \<rightarrow> \<nat>"
term "\<nat> \<Zffun> \<nat>"
end
end