1 |
1 |
2 \chapter{Isabelle/HOL specific tools and packages} |
2 \chapter{Isabelle/HOL Tools and Packages} |
3 |
3 |
4 \section{Primitive types} |
4 \section{Primitive types} |
5 |
5 |
6 \section{Records} |
6 \indexisarcmd{typedecl}\indexisarcmd{typedef} |
|
7 \begin{matharray}{rcl} |
|
8 \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\ |
|
9 \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\ |
|
10 \end{matharray} |
7 |
11 |
8 \section{Datatypes} |
12 \begin{rail} |
|
13 'typedecl' typespec infix? comment? |
|
14 ; |
|
15 'typedef' parname? typespec infix? \\ '=' term comment? |
|
16 ; |
|
17 \end{rail} |
|
18 |
|
19 \begin{description} |
|
20 \item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original |
|
21 $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but |
|
22 also declares type arity $t :: (term, \dots, term) term$, making $t$ an |
|
23 actual HOL type constructor. |
|
24 \item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating |
|
25 non-emptiness of the set $A$. After finishing the proof, the theory will be |
|
26 augmented by a Gordon/HOL-style type definitions. See \cite{isabelle-HOL} |
|
27 for more information. Note that user-level work usually does not directly |
|
28 refer to the HOL $\isarkeyword{typedef}$ primitive, but uses more advanced |
|
29 packages such as $\isarkeyword{record}$ (\S\ref{sec:record}) or |
|
30 $\isarkeyword{datatype}$ (\S\ref{sec:datatype}). |
|
31 \end{description} |
|
32 |
|
33 |
|
34 \section{Records}\label{sec:record} |
|
35 |
|
36 %FIXME record_split method |
|
37 \indexisarcmd{record} |
|
38 \begin{matharray}{rcl} |
|
39 \isarcmd{record} & : & \isartrans{theory}{theory} \\ |
|
40 \end{matharray} |
|
41 |
|
42 \begin{rail} |
|
43 'record' typespec '=' (type '+')? (field +) |
|
44 ; |
|
45 |
|
46 field: name '::' type comment? |
|
47 ; |
|
48 \end{rail} |
|
49 |
|
50 \begin{description} |
|
51 \item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$] |
|
52 defines extensible record type $(\vec\alpha)t$, derived from the optional |
|
53 parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$. |
|
54 See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information only |
|
55 simply-typed records. |
|
56 \end{description} |
|
57 |
|
58 |
|
59 \section{Datatypes}\label{sec:datatype} |
|
60 |
|
61 \indexisarcmd{datatype}\indexisarcmd{rep_datatype} |
|
62 \begin{matharray}{rcl} |
|
63 \isarcmd{datatype} & : & \isartrans{theory}{theory} \\ |
|
64 \isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\ |
|
65 \end{matharray} |
|
66 |
|
67 \railalias{repdatatype}{rep\_datatype} |
|
68 \railterm{repdatatype} |
|
69 |
|
70 \begin{rail} |
|
71 'datatype' (parname? typespec infix? \\ '=' (cons + '|') + 'and') |
|
72 ; |
|
73 repdatatype (name * ) \\ 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs |
|
74 ; |
|
75 |
|
76 cons: name (type * ) mixfix? comment? |
|
77 ; |
|
78 \end{rail} |
|
79 |
|
80 \begin{description} |
|
81 \item [$\isarkeyword{datatype}$] FIXME |
|
82 \item [$\isarkeyword{rep_datatype}$] FIXME |
|
83 \end{description} |
|
84 |
9 |
85 |
10 \section{Recursive functions} |
86 \section{Recursive functions} |
11 |
87 |
|
88 \indexisarcmd{primrec}\indexisarcmd{recdef} |
|
89 \begin{matharray}{rcl} |
|
90 \isarcmd{primrec} & : & \isartrans{theory}{theory} \\ |
|
91 \isarcmd{recdef} & : & \isartrans{theory}{theory} \\ |
|
92 %FIXME |
|
93 % \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\ |
|
94 \end{matharray} |
|
95 |
|
96 \begin{rail} |
|
97 'primrec' parname? (thmdecl? prop comment? + ) |
|
98 ; |
|
99 'recdef' name term (term comment? +) \\ ('congs' thmrefs)? ('simpset' name)? |
|
100 ; |
|
101 \end{rail} |
|
102 |
|
103 \begin{description} |
|
104 \item [$\isarkeyword{primrec}$] FIXME |
|
105 \item [$\isarkeyword{recdef}$] FIXME |
|
106 \end{description} |
|
107 |
|
108 |
12 \section{(Co)Inductive sets} |
109 \section{(Co)Inductive sets} |
|
110 |
|
111 \indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisarcmd{inductive\_cases} |
|
112 \begin{matharray}{rcl} |
|
113 \isarcmd{inductive} & : & \isartrans{theory}{theory} \\ |
|
114 \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\ |
|
115 \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\ |
|
116 \end{matharray} |
|
117 |
|
118 \railalias{condefs}{con\_defs} |
|
119 \railalias{indcases}{inductive\_cases} |
|
120 \railterm{condefs,indcases} |
|
121 |
|
122 \begin{rail} |
|
123 ('inductive' | 'coinductive') (term comment? +) \\ |
|
124 'intrs' attributes? (thmdecl? prop comment? +) \\ |
|
125 'monos' thmrefs comment? \\ condefs thmrefs comment? |
|
126 ; |
|
127 indcases thmdef? nameref ':' \\ (prop +) comment? |
|
128 ; |
|
129 \end{rail} |
|
130 |
|
131 \begin{description} |
|
132 \item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] FIXME |
|
133 \item [$\isarkeyword{inductive_cases}$] FIXME |
|
134 \end{description} |
|
135 |
|
136 |
|
137 \section{Proof by induction} |
|
138 |
|
139 %FIXME induct proof method |
13 |
140 |
14 |
141 |
15 %%% Local Variables: |
142 %%% Local Variables: |
16 %%% mode: latex |
143 %%% mode: latex |
17 %%% TeX-master: "isar-ref" |
144 %%% TeX-master: "isar-ref" |