32 } |
32 } |
33 \isamarkuptrue% |
33 \isamarkuptrue% |
34 % |
34 % |
35 \begin{isamarkuptext}% |
35 \begin{isamarkuptext}% |
36 \begin{matharray}{rcll} |
36 \begin{matharray}{rcll} |
37 \indexdef{}{command}{axiomatization}\mbox{\isa{\isacommand{axiomatization}}} & : & \isarkeep{local{\dsh}theory} & (axiomatic!)\\ |
37 \indexdef{}{command}{axiomatization}\hypertarget{command.axiomatization}{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}} & : & \isarkeep{local{\dsh}theory} & (axiomatic!)\\ |
38 \indexdef{}{command}{definition}\mbox{\isa{\isacommand{definition}}} & : & \isarkeep{local{\dsh}theory} \\ |
38 \indexdef{}{command}{definition}\hypertarget{command.definition}{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}} & : & \isarkeep{local{\dsh}theory} \\ |
39 \indexdef{}{attribute}{defn}\mbox{\isa{defn}} & : & \isaratt \\ |
39 \indexdef{}{attribute}{defn}\hypertarget{attribute.defn}{\hyperlink{attribute.defn}{\mbox{\isa{defn}}}} & : & \isaratt \\ |
40 \indexdef{}{command}{abbreviation}\mbox{\isa{\isacommand{abbreviation}}} & : & \isarkeep{local{\dsh}theory} \\ |
40 \indexdef{}{command}{abbreviation}\hypertarget{command.abbreviation}{\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}} & : & \isarkeep{local{\dsh}theory} \\ |
41 \indexdef{}{command}{print\_abbrevs}\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
41 \indexdef{}{command}{print\_abbrevs}\hypertarget{command.print_abbrevs}{\hyperlink{command.print_abbrevs}{\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
42 \indexdef{}{command}{notation}\mbox{\isa{\isacommand{notation}}} & : & \isarkeep{local{\dsh}theory} \\ |
42 \indexdef{}{command}{notation}\hypertarget{command.notation}{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}} & : & \isarkeep{local{\dsh}theory} \\ |
43 \indexdef{}{command}{no\_notation}\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}} & : & \isarkeep{local{\dsh}theory} \\ |
43 \indexdef{}{command}{no\_notation}\hypertarget{command.no_notation}{\hyperlink{command.no_notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}} & : & \isarkeep{local{\dsh}theory} \\ |
44 \end{matharray} |
44 \end{matharray} |
45 |
45 |
46 These specification mechanisms provide a slightly more abstract view |
46 These specification mechanisms provide a slightly more abstract view |
47 than the underlying primitives of \mbox{\isa{\isacommand{consts}}}, \mbox{\isa{\isacommand{defs}}} (see \secref{sec:consts}), and \mbox{\isa{\isacommand{axioms}}} (see |
47 than the underlying primitives of \hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}, \hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}} (see \secref{sec:consts}), and \hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}} (see |
48 \secref{sec:axms-thms}). In particular, type-inference is commonly |
48 \secref{sec:axms-thms}). In particular, type-inference is commonly |
49 available, and result names need not be given. |
49 available, and result names need not be given. |
50 |
50 |
51 \begin{rail} |
51 \begin{rail} |
52 'axiomatization' target? fixes? ('where' specs)? |
52 'axiomatization' target? fixes? ('where' specs)? |
66 ; |
66 ; |
67 \end{rail} |
67 \end{rail} |
68 |
68 |
69 \begin{descr} |
69 \begin{descr} |
70 |
70 |
71 \item [\mbox{\isa{\isacommand{axiomatization}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub m\ {\isasymWHERE}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}] introduces several constants |
71 \item [\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub m\ {\isasymWHERE}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}] introduces several constants |
72 simultaneously and states axiomatic properties for these. The |
72 simultaneously and states axiomatic properties for these. The |
73 constants are marked as being specified once and for all, which |
73 constants are marked as being specified once and for all, which |
74 prevents additional specifications being issued later on. |
74 prevents additional specifications being issued later on. |
75 |
75 |
76 Note that axiomatic specifications are only appropriate when |
76 Note that axiomatic specifications are only appropriate when |
77 declaring a new logical system. Normal applications should only use |
77 declaring a new logical system. Normal applications should only use |
78 definitional mechanisms! |
78 definitional mechanisms! |
79 |
79 |
80 \item [\mbox{\isa{\isacommand{definition}}}~\isa{{\isachardoublequote}c\ {\isasymWHERE}\ eq{\isachardoublequote}}] produces an |
80 \item [\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}c\ {\isasymWHERE}\ eq{\isachardoublequote}}] produces an |
81 internal definition \isa{{\isachardoublequote}c\ {\isasymequiv}\ t{\isachardoublequote}} according to the specification |
81 internal definition \isa{{\isachardoublequote}c\ {\isasymequiv}\ t{\isachardoublequote}} according to the specification |
82 given as \isa{eq}, which is then turned into a proven fact. The |
82 given as \isa{eq}, which is then turned into a proven fact. The |
83 given proposition may deviate from internal meta-level equality |
83 given proposition may deviate from internal meta-level equality |
84 according to the rewrite rules declared as \mbox{\isa{defn}} by the |
84 according to the rewrite rules declared as \hyperlink{attribute.defn}{\mbox{\isa{defn}}} by the |
85 object-logic. This usually covers object-level equality \isa{{\isachardoublequote}x\ {\isacharequal}\ y{\isachardoublequote}} and equivalence \isa{{\isachardoublequote}A\ {\isasymleftrightarrow}\ B{\isachardoublequote}}. End-users normally need not |
85 object-logic. This usually covers object-level equality \isa{{\isachardoublequote}x\ {\isacharequal}\ y{\isachardoublequote}} and equivalence \isa{{\isachardoublequote}A\ {\isasymleftrightarrow}\ B{\isachardoublequote}}. End-users normally need not |
86 change the \mbox{\isa{defn}} setup. |
86 change the \hyperlink{attribute.defn}{\mbox{\isa{defn}}} setup. |
87 |
87 |
88 Definitions may be presented with explicit arguments on the LHS, as |
88 Definitions may be presented with explicit arguments on the LHS, as |
89 well as additional conditions, e.g.\ \isa{{\isachardoublequote}f\ x\ y\ {\isacharequal}\ t{\isachardoublequote}} instead of |
89 well as additional conditions, e.g.\ \isa{{\isachardoublequote}f\ x\ y\ {\isacharequal}\ t{\isachardoublequote}} instead of |
90 \isa{{\isachardoublequote}f\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t{\isachardoublequote}} and \isa{{\isachardoublequote}y\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ g\ x\ y\ {\isacharequal}\ u{\isachardoublequote}} instead of an |
90 \isa{{\isachardoublequote}f\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t{\isachardoublequote}} and \isa{{\isachardoublequote}y\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ g\ x\ y\ {\isacharequal}\ u{\isachardoublequote}} instead of an |
91 unrestricted \isa{{\isachardoublequote}g\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ u{\isachardoublequote}}. |
91 unrestricted \isa{{\isachardoublequote}g\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ u{\isachardoublequote}}. |
92 |
92 |
93 \item [\mbox{\isa{\isacommand{abbreviation}}}~\isa{{\isachardoublequote}c\ {\isasymWHERE}\ eq{\isachardoublequote}}] introduces |
93 \item [\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}~\isa{{\isachardoublequote}c\ {\isasymWHERE}\ eq{\isachardoublequote}}] introduces |
94 a syntactic constant which is associated with a certain term |
94 a syntactic constant which is associated with a certain term |
95 according to the meta-level equality \isa{eq}. |
95 according to the meta-level equality \isa{eq}. |
96 |
96 |
97 Abbreviations participate in the usual type-inference process, but |
97 Abbreviations participate in the usual type-inference process, but |
98 are expanded before the logic ever sees them. Pretty printing of |
98 are expanded before the logic ever sees them. Pretty printing of |
101 or looping syntactic replacements! |
101 or looping syntactic replacements! |
102 |
102 |
103 The optional \isa{mode} specification restricts output to a |
103 The optional \isa{mode} specification restricts output to a |
104 particular print mode; using ``\isa{input}'' here achieves the |
104 particular print mode; using ``\isa{input}'' here achieves the |
105 effect of one-way abbreviations. The mode may also include an |
105 effect of one-way abbreviations. The mode may also include an |
106 ``\mbox{\isa{\isakeyword{output}}}'' qualifier that affects the concrete syntax |
106 ``\hyperlink{keyword.output}{\mbox{\isa{\isakeyword{output}}}}'' qualifier that affects the concrete syntax |
107 declared for abbreviations, cf.\ \mbox{\isa{\isacommand{syntax}}} in |
107 declared for abbreviations, cf.\ \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} in |
108 \secref{sec:syn-trans}. |
108 \secref{sec:syn-trans}. |
109 |
109 |
110 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}] prints all constant abbreviations |
110 \item [\hyperlink{command.print_abbrevs}{\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}}] prints all constant abbreviations |
111 of the current context. |
111 of the current context. |
112 |
112 |
113 \item [\mbox{\isa{\isacommand{notation}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}}] associates mixfix |
113 \item [\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}}] associates mixfix |
114 syntax with an existing constant or fixed variable. This is a |
114 syntax with an existing constant or fixed variable. This is a |
115 robust interface to the underlying \mbox{\isa{\isacommand{syntax}}} primitive |
115 robust interface to the underlying \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} primitive |
116 (\secref{sec:syn-trans}). Type declaration and internal syntactic |
116 (\secref{sec:syn-trans}). Type declaration and internal syntactic |
117 representation of the given entity is retrieved from the context. |
117 representation of the given entity is retrieved from the context. |
118 |
118 |
119 \item [\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}] is similar to \mbox{\isa{\isacommand{notation}}}, but removes the specified syntax annotation from the |
119 \item [\hyperlink{command.no_notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}] is similar to \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}, but removes the specified syntax annotation from the |
120 present context. |
120 present context. |
121 |
121 |
122 \end{descr} |
122 \end{descr} |
123 |
123 |
124 All of these specifications support local theory targets (cf.\ |
124 All of these specifications support local theory targets (cf.\ |
152 ; |
152 ; |
153 \end{rail} |
153 \end{rail} |
154 |
154 |
155 \begin{descr} |
155 \begin{descr} |
156 |
156 |
157 \item [\mbox{\isa{\isacommand{declaration}}}~\isa{d}] adds the declaration |
157 \item [\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}~\isa{d}] adds the declaration |
158 function \isa{d} of ML type \verb|declaration|, to the current |
158 function \isa{d} of ML type \verb|declaration|, to the current |
159 local theory under construction. In later application contexts, the |
159 local theory under construction. In later application contexts, the |
160 function is transformed according to the morphisms being involved in |
160 function is transformed according to the morphisms being involved in |
161 the interpretation hierarchy. |
161 the interpretation hierarchy. |
162 |
162 |
163 \item [\mbox{\isa{\isacommand{declare}}}~\isa{thms}] declares theorems to the |
163 \item [\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}~\isa{thms}] declares theorems to the |
164 current local theory context. No theorem binding is involved here, |
164 current local theory context. No theorem binding is involved here, |
165 unlike \mbox{\isa{\isacommand{theorems}}} or \mbox{\isa{\isacommand{lemmas}}} (cf.\ |
165 unlike \hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}} or \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}} (cf.\ |
166 \secref{sec:axms-thms}), so \mbox{\isa{\isacommand{declare}}} only has the effect |
166 \secref{sec:axms-thms}), so \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} only has the effect |
167 of applying attributes as included in the theorem specification. |
167 of applying attributes as included in the theorem specification. |
168 |
168 |
169 \end{descr}% |
169 \end{descr}% |
170 \end{isamarkuptext}% |
170 \end{isamarkuptext}% |
171 \isamarkuptrue% |
171 \isamarkuptrue% |
197 ; |
197 ; |
198 \end{rail} |
198 \end{rail} |
199 |
199 |
200 \begin{descr} |
200 \begin{descr} |
201 |
201 |
202 \item [\mbox{\isa{\isacommand{context}}}~\isa{{\isachardoublequote}c\ {\isasymBEGIN}{\isachardoublequote}}] recommences an |
202 \item [\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}~\isa{{\isachardoublequote}c\ {\isasymBEGIN}{\isachardoublequote}}] recommences an |
203 existing locale or class context \isa{c}. Note that locale and |
203 existing locale or class context \isa{c}. Note that locale and |
204 class definitions allow to include the \indexref{}{keyword}{begin}\mbox{\isa{\isakeyword{begin}}} |
204 class definitions allow to include the \indexref{}{keyword}{begin}\hyperlink{keyword.begin}{\mbox{\isa{\isakeyword{begin}}}} |
205 keyword as well, in order to continue the local theory immediately |
205 keyword as well, in order to continue the local theory immediately |
206 after the initial specification. |
206 after the initial specification. |
207 |
207 |
208 \item [\mbox{\isa{\isacommand{end}}}] concludes the current local theory and |
208 \item [\hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}}] concludes the current local theory and |
209 continues the enclosing global theory. Note that a non-local |
209 continues the enclosing global theory. Note that a non-local |
210 \mbox{\isa{\isacommand{end}}} has a different meaning: it concludes the theory |
210 \hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}} has a different meaning: it concludes the theory |
211 itself (\secref{sec:begin-thy}). |
211 itself (\secref{sec:begin-thy}). |
212 |
212 |
213 \item [\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}{\isachardoublequote}}] given after any local theory command |
213 \item [\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}{\isachardoublequote}}] given after any local theory command |
214 specifies an immediate target, e.g.\ ``\mbox{\isa{\isacommand{definition}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}'' or ``\mbox{\isa{\isacommand{theorem}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}''. This works both in a local or |
214 specifies an immediate target, e.g.\ ``\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}'' or ``\hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}''. This works both in a local or |
215 global theory context; the current target context will be suspended |
215 global theory context; the current target context will be suspended |
216 for this command only. Note that ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ {\isacharminus}{\isacharparenright}{\isachardoublequote}}'' will |
216 for this command only. Note that ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ {\isacharminus}{\isacharparenright}{\isachardoublequote}}'' will |
217 always produce a global result independently of the current target |
217 always produce a global result independently of the current target |
218 context. |
218 context. |
219 |
219 |
253 } |
253 } |
254 \isamarkuptrue% |
254 \isamarkuptrue% |
255 % |
255 % |
256 \begin{isamarkuptext}% |
256 \begin{isamarkuptext}% |
257 \begin{matharray}{rcl} |
257 \begin{matharray}{rcl} |
258 \indexdef{}{command}{locale}\mbox{\isa{\isacommand{locale}}} & : & \isartrans{theory}{local{\dsh}theory} \\ |
258 \indexdef{}{command}{locale}\hypertarget{command.locale}{\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\ |
259 \indexdef{}{command}{print\_locale}\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
259 \indexdef{}{command}{print\_locale}\hypertarget{command.print_locale}{\hyperlink{command.print_locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
260 \indexdef{}{command}{print\_locales}\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
260 \indexdef{}{command}{print\_locales}\hypertarget{command.print_locales}{\hyperlink{command.print_locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
261 \indexdef{}{method}{intro\_locales}\mbox{\isa{intro{\isacharunderscore}locales}} & : & \isarmeth \\ |
261 \indexdef{}{method}{intro\_locales}\hypertarget{method.intro_locales}{\hyperlink{method.intro_locales}{\mbox{\isa{intro{\isacharunderscore}locales}}}} & : & \isarmeth \\ |
262 \indexdef{}{method}{unfold\_locales}\mbox{\isa{unfold{\isacharunderscore}locales}} & : & \isarmeth \\ |
262 \indexdef{}{method}{unfold\_locales}\hypertarget{method.unfold_locales}{\hyperlink{method.unfold_locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}} & : & \isarmeth \\ |
263 \end{matharray} |
263 \end{matharray} |
264 |
264 |
265 \indexouternonterm{contextexpr}\indexouternonterm{contextelem} |
265 \indexouternonterm{contextexpr}\indexouternonterm{contextelem} |
266 \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes} |
266 \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes} |
267 \indexisarelem{defines}\indexisarelem{notes}\indexisarelem{includes} |
267 \indexisarelem{defines}\indexisarelem{notes}\indexisarelem{includes} |
318 The \isa{body} consists of basic context elements, further context |
318 The \isa{body} consists of basic context elements, further context |
319 expressions may be included as well. |
319 expressions may be included as well. |
320 |
320 |
321 \begin{descr} |
321 \begin{descr} |
322 |
322 |
323 \item [\mbox{\isa{\isakeyword{fixes}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}}] declares a local |
323 \item [\hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}}] declares a local |
324 parameter of type \isa{{\isasymtau}} and mixfix annotation \isa{mx} (both |
324 parameter of type \isa{{\isasymtau}} and mixfix annotation \isa{mx} (both |
325 are optional). The special syntax declaration ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}{\isachardoublequote}}'' means that \isa{x} may be referenced |
325 are optional). The special syntax declaration ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}{\isachardoublequote}}'' means that \isa{x} may be referenced |
326 implicitly in this context. |
326 implicitly in this context. |
327 |
327 |
328 \item [\mbox{\isa{\isakeyword{constrains}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isachardoublequote}}] introduces a type |
328 \item [\hyperlink{element.constrains}{\mbox{\isa{\isakeyword{constrains}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isachardoublequote}}] introduces a type |
329 constraint \isa{{\isasymtau}} on the local parameter \isa{x}. |
329 constraint \isa{{\isasymtau}} on the local parameter \isa{x}. |
330 |
330 |
331 \item [\mbox{\isa{\isakeyword{assumes}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}] |
331 \item [\hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}] |
332 introduces local premises, similar to \mbox{\isa{\isacommand{assume}}} within a |
332 introduces local premises, similar to \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} within a |
333 proof (cf.\ \secref{sec:proof-context}). |
333 proof (cf.\ \secref{sec:proof-context}). |
334 |
334 |
335 \item [\mbox{\isa{\isakeyword{defines}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ x\ {\isasymequiv}\ t{\isachardoublequote}}] defines a previously |
335 \item [\hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ x\ {\isasymequiv}\ t{\isachardoublequote}}] defines a previously |
336 declared parameter. This is similar to \mbox{\isa{\isacommand{def}}} within a |
336 declared parameter. This is similar to \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}} within a |
337 proof (cf.\ \secref{sec:proof-context}), but \mbox{\isa{\isakeyword{defines}}} |
337 proof (cf.\ \secref{sec:proof-context}), but \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}} |
338 takes an equational proposition instead of variable-term pair. The |
338 takes an equational proposition instead of variable-term pair. The |
339 left-hand side of the equation may have additional arguments, e.g.\ |
339 left-hand side of the equation may have additional arguments, e.g.\ |
340 ``\mbox{\isa{\isakeyword{defines}}}~\isa{{\isachardoublequote}f\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ t{\isachardoublequote}}''. |
340 ``\hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isachardoublequote}f\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ t{\isachardoublequote}}''. |
341 |
341 |
342 \item [\mbox{\isa{\isakeyword{notes}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}] |
342 \item [\hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}] |
343 reconsiders facts within a local context. Most notably, this may |
343 reconsiders facts within a local context. Most notably, this may |
344 include arbitrary declarations in any attribute specifications |
344 include arbitrary declarations in any attribute specifications |
345 included here, e.g.\ a local \mbox{\isa{simp}} rule. |
345 included here, e.g.\ a local \hyperlink{attribute.simp}{\mbox{\isa{simp}}} rule. |
346 |
346 |
347 \item [\mbox{\isa{\isakeyword{includes}}}~\isa{c}] copies the specified context |
347 \item [\hyperlink{element.includes}{\mbox{\isa{\isakeyword{includes}}}}~\isa{c}] copies the specified context |
348 in a statically scoped manner. Only available in the long goal |
348 in a statically scoped manner. Only available in the long goal |
349 format of \secref{sec:goals}. |
349 format of \secref{sec:goals}. |
350 |
350 |
351 In contrast, the initial \isa{import} specification of a locale |
351 In contrast, the initial \isa{import} specification of a locale |
352 expression maintains a dynamic relation to the locales being |
352 expression maintains a dynamic relation to the locales being |
380 The \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}} option of a locale specification prevents both |
380 The \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}} option of a locale specification prevents both |
381 the current \isa{loc{\isacharunderscore}axioms} and cumulative \isa{loc} predicate |
381 the current \isa{loc{\isacharunderscore}axioms} and cumulative \isa{loc} predicate |
382 constructions. Predicates are also omitted for empty specification |
382 constructions. Predicates are also omitted for empty specification |
383 texts. |
383 texts. |
384 |
384 |
385 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}~\isa{{\isachardoublequote}import\ {\isacharplus}\ body{\isachardoublequote}}] prints the |
385 \item [\hyperlink{command.print_locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}import\ {\isacharplus}\ body{\isachardoublequote}}] prints the |
386 specified locale expression in a flattened form. The notable |
386 specified locale expression in a flattened form. The notable |
387 special case \mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}~\isa{loc} just prints the |
387 special case \hyperlink{command.print_locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{loc} just prints the |
388 contents of the named locale, but keep in mind that type-inference |
388 contents of the named locale, but keep in mind that type-inference |
389 will normalize type variables according to the usual alphabetical |
389 will normalize type variables according to the usual alphabetical |
390 order. The command omits \mbox{\isa{\isakeyword{notes}}} elements by default. |
390 order. The command omits \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}} elements by default. |
391 Use \mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to get them included. |
391 Use \hyperlink{command.print_locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to get them included. |
392 |
392 |
393 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}] prints the names of all locales |
393 \item [\hyperlink{command.print_locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}}] prints the names of all locales |
394 of the current theory. |
394 of the current theory. |
395 |
395 |
396 \item [\mbox{\isa{intro{\isacharunderscore}locales}} and \mbox{\isa{unfold{\isacharunderscore}locales}}] |
396 \item [\hyperlink{method.intro_locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} and \hyperlink{method.unfold_locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}] |
397 repeatedly expand all introduction rules of locale predicates of the |
397 repeatedly expand all introduction rules of locale predicates of the |
398 theory. While \mbox{\isa{intro{\isacharunderscore}locales}} only applies the \isa{loc{\isachardot}intro} introduction rules and therefore does not decend to |
398 theory. While \hyperlink{method.intro_locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} only applies the \isa{loc{\isachardot}intro} introduction rules and therefore does not decend to |
399 assumptions, \mbox{\isa{unfold{\isacharunderscore}locales}} is more aggressive and applies |
399 assumptions, \hyperlink{method.unfold_locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}} is more aggressive and applies |
400 \isa{loc{\isacharunderscore}axioms{\isachardot}intro} as well. Both methods are aware of locale |
400 \isa{loc{\isacharunderscore}axioms{\isachardot}intro} as well. Both methods are aware of locale |
401 specifications entailed by the context, both from target and |
401 specifications entailed by the context, both from target and |
402 \mbox{\isa{\isakeyword{includes}}} statements, and from interpretations (see |
402 \hyperlink{element.includes}{\mbox{\isa{\isakeyword{includes}}}} statements, and from interpretations (see |
403 below). New goals that are entailed by the current context are |
403 below). New goals that are entailed by the current context are |
404 discharged automatically. |
404 discharged automatically. |
405 |
405 |
406 \end{descr}% |
406 \end{descr}% |
407 \end{isamarkuptext}% |
407 \end{isamarkuptext}% |
414 \begin{isamarkuptext}% |
414 \begin{isamarkuptext}% |
415 Locale expressions (more precisely, \emph{context expressions}) may |
415 Locale expressions (more precisely, \emph{context expressions}) may |
416 be instantiated, and the instantiated facts added to the current |
416 be instantiated, and the instantiated facts added to the current |
417 context. This requires a proof of the instantiated specification |
417 context. This requires a proof of the instantiated specification |
418 and is called \emph{locale interpretation}. Interpretation is |
418 and is called \emph{locale interpretation}. Interpretation is |
419 possible in theories and locales (command \mbox{\isa{\isacommand{interpretation}}}) and also within a proof body (command \mbox{\isa{\isacommand{interpret}}}). |
419 possible in theories and locales (command \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}) and also within a proof body (command \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}). |
420 |
420 |
421 \begin{matharray}{rcl} |
421 \begin{matharray}{rcl} |
422 \indexdef{}{command}{interpretation}\mbox{\isa{\isacommand{interpretation}}} & : & \isartrans{theory}{proof(prove)} \\ |
422 \indexdef{}{command}{interpretation}\hypertarget{command.interpretation}{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}} & : & \isartrans{theory}{proof(prove)} \\ |
423 \indexdef{}{command}{interpret}\mbox{\isa{\isacommand{interpret}}} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\ |
423 \indexdef{}{command}{interpret}\hypertarget{command.interpret}{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\ |
424 \indexdef{}{command}{print\_interps}\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
424 \indexdef{}{command}{print\_interps}\hypertarget{command.print_interps}{\hyperlink{command.print_interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
425 \end{matharray} |
425 \end{matharray} |
426 |
426 |
427 \indexouternonterm{interp} |
427 \indexouternonterm{interp} |
428 \begin{rail} |
428 \begin{rail} |
429 'interpretation' (interp | name ('<' | subseteq) contextexpr) |
429 'interpretation' (interp | name ('<' | subseteq) contextexpr) |
453 specifications (assumes and defines elements). Once these are |
453 specifications (assumes and defines elements). Once these are |
454 discharged by the user, instantiated facts are added to the theory |
454 discharged by the user, instantiated facts are added to the theory |
455 in a post-processing phase. |
455 in a post-processing phase. |
456 |
456 |
457 Additional equations, which are unfolded in facts during |
457 Additional equations, which are unfolded in facts during |
458 post-processing, may be given after the keyword \mbox{\isa{\isakeyword{where}}}. |
458 post-processing, may be given after the keyword \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}}. |
459 This is useful for interpreting concepts introduced through |
459 This is useful for interpreting concepts introduced through |
460 definition specification elements. The equations must be proved. |
460 definition specification elements. The equations must be proved. |
461 Note that if equations are present, the context expression is |
461 Note that if equations are present, the context expression is |
462 restricted to a locale name. |
462 restricted to a locale name. |
463 |
463 |
478 Adding facts to locales has the effect of adding interpreted facts |
478 Adding facts to locales has the effect of adding interpreted facts |
479 to the theory for all active interpretations also. That is, |
479 to the theory for all active interpretations also. That is, |
480 interpretations dynamically participate in any facts added to |
480 interpretations dynamically participate in any facts added to |
481 locales. |
481 locales. |
482 |
482 |
483 \item [\mbox{\isa{\isacommand{interpretation}}}~\isa{{\isachardoublequote}name\ {\isasymsubseteq}\ expr{\isachardoublequote}}] |
483 \item [\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}name\ {\isasymsubseteq}\ expr{\isachardoublequote}}] |
484 |
484 |
485 This form of the command interprets \isa{expr} in the locale |
485 This form of the command interprets \isa{expr} in the locale |
486 \isa{name}. It requires a proof that the specification of \isa{name} implies the specification of \isa{expr}. As in the |
486 \isa{name}. It requires a proof that the specification of \isa{name} implies the specification of \isa{expr}. As in the |
487 localized version of the theorem command, the proof is in the |
487 localized version of the theorem command, the proof is in the |
488 context of \isa{name}. After the proof obligation has been |
488 context of \isa{name}. After the proof obligation has been |
505 If interpretations of \isa{name} exist in the current theory, the |
505 If interpretations of \isa{name} exist in the current theory, the |
506 command adds interpretations for \isa{expr} as well, with the same |
506 command adds interpretations for \isa{expr} as well, with the same |
507 prefix and attributes, although only for fragments of \isa{expr} |
507 prefix and attributes, although only for fragments of \isa{expr} |
508 that are not interpreted in the theory already. |
508 that are not interpreted in the theory already. |
509 |
509 |
510 \item [\mbox{\isa{\isacommand{interpret}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}] |
510 \item [\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}] |
511 interprets \isa{expr} in the proof context and is otherwise |
511 interprets \isa{expr} in the proof context and is otherwise |
512 similar to interpretation in theories. |
512 similar to interpretation in theories. |
513 |
513 |
514 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}~\isa{loc}] prints the |
514 \item [\hyperlink{command.print_interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}~\isa{loc}] prints the |
515 interpretations of a particular locale \isa{loc} that are active |
515 interpretations of a particular locale \isa{loc} that are active |
516 in the current context, either theory or proof context. The |
516 in the current context, either theory or proof context. The |
517 exclamation point argument triggers printing of \emph{witness} |
517 exclamation point argument triggers printing of \emph{witness} |
518 theorems justifying interpretations. These are normally omitted |
518 theorems justifying interpretations. These are normally omitted |
519 from the output. |
519 from the output. |
554 generality of locales combined with the commodity of type classes |
554 generality of locales combined with the commodity of type classes |
555 (notably type-inference). See \cite{isabelle-classes} for a short |
555 (notably type-inference). See \cite{isabelle-classes} for a short |
556 tutorial. |
556 tutorial. |
557 |
557 |
558 \begin{matharray}{rcl} |
558 \begin{matharray}{rcl} |
559 \indexdef{}{command}{class}\mbox{\isa{\isacommand{class}}} & : & \isartrans{theory}{local{\dsh}theory} \\ |
559 \indexdef{}{command}{class}\hypertarget{command.class}{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\ |
560 \indexdef{}{command}{instantiation}\mbox{\isa{\isacommand{instantiation}}} & : & \isartrans{theory}{local{\dsh}theory} \\ |
560 \indexdef{}{command}{instantiation}\hypertarget{command.instantiation}{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\ |
561 \indexdef{}{command}{instance}\mbox{\isa{\isacommand{instance}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\ |
561 \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\ |
562 \indexdef{}{command}{subclass}\mbox{\isa{\isacommand{subclass}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\ |
562 \indexdef{}{command}{subclass}\hypertarget{command.subclass}{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\ |
563 \indexdef{}{command}{print\_classes}\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
563 \indexdef{}{command}{print\_classes}\hypertarget{command.print_classes}{\hyperlink{command.print_classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
564 \indexdef{}{method}{intro\_classes}\mbox{\isa{intro{\isacharunderscore}classes}} & : & \isarmeth \\ |
564 \indexdef{}{method}{intro\_classes}\hypertarget{method.intro_classes}{\hyperlink{method.intro_classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}} & : & \isarmeth \\ |
565 \end{matharray} |
565 \end{matharray} |
566 |
566 |
567 \begin{rail} |
567 \begin{rail} |
568 'class' name '=' ((superclassexpr '+' (contextelem+)) | superclassexpr | (contextelem+)) \\ |
568 'class' name '=' ((superclassexpr '+' (contextelem+)) | superclassexpr | (contextelem+)) \\ |
569 'begin'? |
569 'begin'? |
581 ; |
581 ; |
582 \end{rail} |
582 \end{rail} |
583 |
583 |
584 \begin{descr} |
584 \begin{descr} |
585 |
585 |
586 \item [\mbox{\isa{\isacommand{class}}}~\isa{{\isachardoublequote}c\ {\isacharequal}\ superclasses\ {\isacharplus}\ body{\isachardoublequote}}] defines |
586 \item [\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}~\isa{{\isachardoublequote}c\ {\isacharequal}\ superclasses\ {\isacharplus}\ body{\isachardoublequote}}] defines |
587 a new class \isa{c}, inheriting from \isa{superclasses}. This |
587 a new class \isa{c}, inheriting from \isa{superclasses}. This |
588 introduces a locale \isa{c} with import of all locales \isa{superclasses}. |
588 introduces a locale \isa{c} with import of all locales \isa{superclasses}. |
589 |
589 |
590 Any \mbox{\isa{\isakeyword{fixes}}} in \isa{body} are lifted to the global |
590 Any \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} in \isa{body} are lifted to the global |
591 theory level (\emph{class operations} \isa{{\isachardoublequote}f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n{\isachardoublequote}} of class \isa{c}), mapping the local type parameter |
591 theory level (\emph{class operations} \isa{{\isachardoublequote}f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n{\isachardoublequote}} of class \isa{c}), mapping the local type parameter |
592 \isa{{\isasymalpha}} to a schematic type variable \isa{{\isachardoublequote}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isachardoublequote}}. |
592 \isa{{\isasymalpha}} to a schematic type variable \isa{{\isachardoublequote}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isachardoublequote}}. |
593 |
593 |
594 Likewise, \mbox{\isa{\isakeyword{assumes}}} in \isa{body} are also lifted, |
594 Likewise, \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} in \isa{body} are also lifted, |
595 mapping each local parameter \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} to its |
595 mapping each local parameter \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} to its |
596 corresponding global constant \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}. The |
596 corresponding global constant \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}. The |
597 corresponding introduction rule is provided as \isa{c{\isacharunderscore}class{\isacharunderscore}axioms{\isachardot}intro}. This rule should be rarely needed directly |
597 corresponding introduction rule is provided as \isa{c{\isacharunderscore}class{\isacharunderscore}axioms{\isachardot}intro}. This rule should be rarely needed directly |
598 --- the \mbox{\isa{intro{\isacharunderscore}classes}} method takes care of the details of |
598 --- the \hyperlink{method.intro_classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method takes care of the details of |
599 class membership proofs. |
599 class membership proofs. |
600 |
600 |
601 \item [\mbox{\isa{\isacommand{instantiation}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s\ {\isasymBEGIN}{\isachardoublequote}}] opens a theory target (cf.\ |
601 \item [\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s\ {\isasymBEGIN}{\isachardoublequote}}] opens a theory target (cf.\ |
602 \secref{sec:target}) which allows to specify class operations \isa{{\isachardoublequote}f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n{\isachardoublequote}} corresponding to sort \isa{s} at the |
602 \secref{sec:target}) which allows to specify class operations \isa{{\isachardoublequote}f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n{\isachardoublequote}} corresponding to sort \isa{s} at the |
603 particular type instance \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ s\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}. A plain \mbox{\isa{\isacommand{instance}}} command |
603 particular type instance \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ s\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}. A plain \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command |
604 in the target body poses a goal stating these type arities. The |
604 in the target body poses a goal stating these type arities. The |
605 target is concluded by an \indexref{}{command}{end}\mbox{\isa{\isacommand{end}}} command. |
605 target is concluded by an \indexref{}{command}{end}\hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}} command. |
606 |
606 |
607 Note that a list of simultaneous type constructors may be given; |
607 Note that a list of simultaneous type constructors may be given; |
608 this corresponds nicely to mutual recursive type definitions, e.g.\ |
608 this corresponds nicely to mutual recursive type definitions, e.g.\ |
609 in Isabelle/HOL. |
609 in Isabelle/HOL. |
610 |
610 |
611 \item [\mbox{\isa{\isacommand{instance}}}] in an instantiation target body sets |
611 \item [\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}] in an instantiation target body sets |
612 up a goal stating the type arities claimed at the opening \mbox{\isa{\isacommand{instantiation}}}. The proof would usually proceed by \mbox{\isa{intro{\isacharunderscore}classes}}, and then establish the characteristic theorems of |
612 up a goal stating the type arities claimed at the opening \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}. The proof would usually proceed by \hyperlink{method.intro_classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}, and then establish the characteristic theorems of |
613 the type classes involved. After finishing the proof, the |
613 the type classes involved. After finishing the proof, the |
614 background theory will be augmented by the proven type arities. |
614 background theory will be augmented by the proven type arities. |
615 |
615 |
616 \item [\mbox{\isa{\isacommand{subclass}}}~\isa{c}] in a class context for class |
616 \item [\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}~\isa{c}] in a class context for class |
617 \isa{d} sets up a goal stating that class \isa{c} is logically |
617 \isa{d} sets up a goal stating that class \isa{c} is logically |
618 contained in class \isa{d}. After finishing the proof, class |
618 contained in class \isa{d}. After finishing the proof, class |
619 \isa{d} is proven to be subclass \isa{c} and the locale \isa{c} is interpreted into \isa{d} simultaneously. |
619 \isa{d} is proven to be subclass \isa{c} and the locale \isa{c} is interpreted into \isa{d} simultaneously. |
620 |
620 |
621 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}] prints all classes in the current |
621 \item [\hyperlink{command.print_classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}] prints all classes in the current |
622 theory. |
622 theory. |
623 |
623 |
624 \item [\mbox{\isa{intro{\isacharunderscore}classes}}] repeatedly expands all class |
624 \item [\hyperlink{method.intro_classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}] repeatedly expands all class |
625 introduction rules of this theory. Note that this method usually |
625 introduction rules of this theory. Note that this method usually |
626 needs not be named explicitly, as it is already included in the |
626 needs not be named explicitly, as it is already included in the |
627 default proof step (e.g.\ of \mbox{\isa{\isacommand{proof}}}). In particular, |
627 default proof step (e.g.\ of \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}). In particular, |
628 instantiation of trivial (syntactic) classes may be performed by a |
628 instantiation of trivial (syntactic) classes may be performed by a |
629 single ``\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}'' proof step. |
629 single ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}'' proof step. |
630 |
630 |
631 \end{descr}% |
631 \end{descr}% |
632 \end{isamarkuptext}% |
632 \end{isamarkuptext}% |
633 \isamarkuptrue% |
633 \isamarkuptrue% |
634 % |
634 % |
683 ; |
683 ; |
684 \end{rail} |
684 \end{rail} |
685 |
685 |
686 \begin{descr} |
686 \begin{descr} |
687 |
687 |
688 \item [\mbox{\isa{\isacommand{axclass}}}~\isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ axms{\isachardoublequote}}] defines an axiomatic type class as the intersection of |
688 \item [\hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}~\isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ axms{\isachardoublequote}}] defines an axiomatic type class as the intersection of |
689 existing classes, with additional axioms holding. Class axioms may |
689 existing classes, with additional axioms holding. Class axioms may |
690 not contain more than one type variable. The class axioms (with |
690 not contain more than one type variable. The class axioms (with |
691 implicit sort constraints added) are bound to the given names. |
691 implicit sort constraints added) are bound to the given names. |
692 Furthermore a class introduction rule is generated (being bound as |
692 Furthermore a class introduction rule is generated (being bound as |
693 \isa{c{\isacharunderscore}class{\isachardot}intro}); this rule is employed by method \mbox{\isa{intro{\isacharunderscore}classes}} to support instantiation proofs of this class. |
693 \isa{c{\isacharunderscore}class{\isachardot}intro}); this rule is employed by method \hyperlink{method.intro_classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} to support instantiation proofs of this class. |
694 |
694 |
695 The ``class axioms'' are stored as theorems according to the given |
695 The ``class axioms'' are stored as theorems according to the given |
696 name specifications, adding \isa{{\isachardoublequote}c{\isacharunderscore}class{\isachardoublequote}} as name space prefix; |
696 name specifications, adding \isa{{\isachardoublequote}c{\isacharunderscore}class{\isachardoublequote}} as name space prefix; |
697 the same facts are also stored collectively as \isa{c{\isacharunderscore}class{\isachardot}axioms}. |
697 the same facts are also stored collectively as \isa{c{\isacharunderscore}class{\isachardot}axioms}. |
698 |
698 |
699 \item [\mbox{\isa{\isacommand{instance}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} and |
699 \item [\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} and |
700 \mbox{\isa{\isacommand{instance}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s{\isachardoublequote}}] |
700 \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s{\isachardoublequote}}] |
701 setup a goal stating a class relation or type arity. The proof |
701 setup a goal stating a class relation or type arity. The proof |
702 would usually proceed by \mbox{\isa{intro{\isacharunderscore}classes}}, and then establish |
702 would usually proceed by \hyperlink{method.intro_classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}, and then establish |
703 the characteristic theorems of the type classes involved. After |
703 the characteristic theorems of the type classes involved. After |
704 finishing the proof, the theory will be augmented by a type |
704 finishing the proof, the theory will be augmented by a type |
705 signature declaration corresponding to the resulting theorem. |
705 signature declaration corresponding to the resulting theorem. |
706 |
706 |
707 \end{descr}% |
707 \end{descr}% |
714 % |
714 % |
715 \begin{isamarkuptext}% |
715 \begin{isamarkuptext}% |
716 Isabelle/Pure's definitional schemes support certain forms of |
716 Isabelle/Pure's definitional schemes support certain forms of |
717 overloading (see \secref{sec:consts}). At most occassions |
717 overloading (see \secref{sec:consts}). At most occassions |
718 overloading will be used in a Haskell-like fashion together with |
718 overloading will be used in a Haskell-like fashion together with |
719 type classes by means of \mbox{\isa{\isacommand{instantiation}}} (see |
719 type classes by means of \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} (see |
720 \secref{sec:class}). Sometimes low-level overloading is desirable. |
720 \secref{sec:class}). Sometimes low-level overloading is desirable. |
721 The \mbox{\isa{\isacommand{overloading}}} target provides a convenient view for |
721 The \hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}} target provides a convenient view for |
722 end-users. |
722 end-users. |
723 |
723 |
724 \begin{matharray}{rcl} |
724 \begin{matharray}{rcl} |
725 \indexdef{}{command}{overloading}\mbox{\isa{\isacommand{overloading}}} & : & \isartrans{theory}{local{\dsh}theory} \\ |
725 \indexdef{}{command}{overloading}\hypertarget{command.overloading}{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\ |
726 \end{matharray} |
726 \end{matharray} |
727 |
727 |
728 \begin{rail} |
728 \begin{rail} |
729 'overloading' \\ |
729 'overloading' \\ |
730 ( string ( '==' | equiv ) term ( '(' 'unchecked' ')' )? + ) 'begin' |
730 ( string ( '==' | equiv ) term ( '(' 'unchecked' ')' )? + ) 'begin' |
731 \end{rail} |
731 \end{rail} |
732 |
732 |
733 \begin{descr} |
733 \begin{descr} |
734 |
734 |
735 \item [\mbox{\isa{\isacommand{overloading}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymequiv}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\isactrlsub n\ {\isasymBEGIN}{\isachardoublequote}}] |
735 \item [\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymequiv}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\isactrlsub n\ {\isasymBEGIN}{\isachardoublequote}}] |
736 opens a theory target (cf.\ \secref{sec:target}) which allows to |
736 opens a theory target (cf.\ \secref{sec:target}) which allows to |
737 specify constants with overloaded definitions. These are identified |
737 specify constants with overloaded definitions. These are identified |
738 by an explicitly given mapping from variable names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} to constants \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} at particular type |
738 by an explicitly given mapping from variable names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} to constants \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} at particular type |
739 instances. The definitions themselves are established using common |
739 instances. The definitions themselves are established using common |
740 specification tools, using the names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} as |
740 specification tools, using the names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} as |
741 reference to the corresponding constants. The target is concluded |
741 reference to the corresponding constants. The target is concluded |
742 by \mbox{\isa{\isacommand{end}}}. |
742 by \hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}}. |
743 |
743 |
744 A \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks for |
744 A \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks for |
745 the corresponding definition, which is occasionally useful for |
745 the corresponding definition, which is occasionally useful for |
746 exotic overloading. It is at the discretion of the user to avoid |
746 exotic overloading. It is at the discretion of the user to avoid |
747 malformed theory specifications! |
747 malformed theory specifications! |
759 within the theory or proof context, with values of type \verb|bool|, \verb|int|, or \verb|string|. Tools may declare |
759 within the theory or proof context, with values of type \verb|bool|, \verb|int|, or \verb|string|. Tools may declare |
760 options in ML, and then refer to these values (relative to the |
760 options in ML, and then refer to these values (relative to the |
761 context). Thus global reference variables are easily avoided. The |
761 context). Thus global reference variables are easily avoided. The |
762 user may change the value of a configuration option by means of an |
762 user may change the value of a configuration option by means of an |
763 associated attribute of the same name. This form of context |
763 associated attribute of the same name. This form of context |
764 declaration works particularly well with commands such as \mbox{\isa{\isacommand{declare}}} or \mbox{\isa{\isacommand{using}}}. |
764 declaration works particularly well with commands such as \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} or \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}. |
765 |
765 |
766 For historical reasons, some tools cannot take the full proof |
766 For historical reasons, some tools cannot take the full proof |
767 context into account and merely refer to the background theory. |
767 context into account and merely refer to the background theory. |
768 This is accommodated by configuration options being declared as |
768 This is accommodated by configuration options being declared as |
769 ``global'', which may not be changed within a local context. |
769 ``global'', which may not be changed within a local context. |
770 |
770 |
771 \begin{matharray}{rcll} |
771 \begin{matharray}{rcll} |
772 \indexdef{}{command}{print\_configs}\mbox{\isa{\isacommand{print{\isacharunderscore}configs}}} & : & \isarkeep{theory~|~proof} \\ |
772 \indexdef{}{command}{print\_configs}\hypertarget{command.print_configs}{\hyperlink{command.print_configs}{\mbox{\isa{\isacommand{print{\isacharunderscore}configs}}}}} & : & \isarkeep{theory~|~proof} \\ |
773 \end{matharray} |
773 \end{matharray} |
774 |
774 |
775 \begin{rail} |
775 \begin{rail} |
776 name ('=' ('true' | 'false' | int | name))? |
776 name ('=' ('true' | 'false' | int | name))? |
777 \end{rail} |
777 \end{rail} |
778 |
778 |
779 \begin{descr} |
779 \begin{descr} |
780 |
780 |
781 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}configs}}}] prints the available |
781 \item [\hyperlink{command.print_configs}{\mbox{\isa{\isacommand{print{\isacharunderscore}configs}}}}] prints the available |
782 configuration options, with names, types, and current values. |
782 configuration options, with names, types, and current values. |
783 |
783 |
784 \item [\isa{{\isachardoublequote}name\ {\isacharequal}\ value{\isachardoublequote}}] as an attribute expression modifies |
784 \item [\isa{{\isachardoublequote}name\ {\isacharequal}\ value{\isachardoublequote}}] as an attribute expression modifies |
785 the named option, with the syntax of the value depending on the |
785 the named option, with the syntax of the value depending on the |
786 option's type. For \verb|bool| the default value is \isa{true}. Any attempt to change a global option in a local context is |
786 option's type. For \verb|bool| the default value is \isa{true}. Any attempt to change a global option in a local context is |
798 } |
798 } |
799 \isamarkuptrue% |
799 \isamarkuptrue% |
800 % |
800 % |
801 \begin{isamarkuptext}% |
801 \begin{isamarkuptext}% |
802 \begin{matharray}{rcl} |
802 \begin{matharray}{rcl} |
803 \indexdef{}{method}{unfold}\mbox{\isa{unfold}} & : & \isarmeth \\ |
803 \indexdef{}{method}{unfold}\hypertarget{method.unfold}{\hyperlink{method.unfold}{\mbox{\isa{unfold}}}} & : & \isarmeth \\ |
804 \indexdef{}{method}{fold}\mbox{\isa{fold}} & : & \isarmeth \\ |
804 \indexdef{}{method}{fold}\hypertarget{method.fold}{\hyperlink{method.fold}{\mbox{\isa{fold}}}} & : & \isarmeth \\ |
805 \indexdef{}{method}{insert}\mbox{\isa{insert}} & : & \isarmeth \\[0.5ex] |
805 \indexdef{}{method}{insert}\hypertarget{method.insert}{\hyperlink{method.insert}{\mbox{\isa{insert}}}} & : & \isarmeth \\[0.5ex] |
806 \indexdef{}{method}{erule}\mbox{\isa{erule}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
806 \indexdef{}{method}{erule}\hypertarget{method.erule}{\hyperlink{method.erule}{\mbox{\isa{erule}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
807 \indexdef{}{method}{drule}\mbox{\isa{drule}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
807 \indexdef{}{method}{drule}\hypertarget{method.drule}{\hyperlink{method.drule}{\mbox{\isa{drule}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
808 \indexdef{}{method}{frule}\mbox{\isa{frule}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
808 \indexdef{}{method}{frule}\hypertarget{method.frule}{\hyperlink{method.frule}{\mbox{\isa{frule}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
809 \indexdef{}{method}{succeed}\mbox{\isa{succeed}} & : & \isarmeth \\ |
809 \indexdef{}{method}{succeed}\hypertarget{method.succeed}{\hyperlink{method.succeed}{\mbox{\isa{succeed}}}} & : & \isarmeth \\ |
810 \indexdef{}{method}{fail}\mbox{\isa{fail}} & : & \isarmeth \\ |
810 \indexdef{}{method}{fail}\hypertarget{method.fail}{\hyperlink{method.fail}{\mbox{\isa{fail}}}} & : & \isarmeth \\ |
811 \end{matharray} |
811 \end{matharray} |
812 |
812 |
813 \begin{rail} |
813 \begin{rail} |
814 ('fold' | 'unfold' | 'insert') thmrefs |
814 ('fold' | 'unfold' | 'insert') thmrefs |
815 ; |
815 ; |
817 ; |
817 ; |
818 \end{rail} |
818 \end{rail} |
819 |
819 |
820 \begin{descr} |
820 \begin{descr} |
821 |
821 |
822 \item [\mbox{\isa{unfold}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} and \mbox{\isa{fold}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] expand (or fold back) the |
822 \item [\hyperlink{method.unfold}{\mbox{\isa{unfold}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} and \hyperlink{method.fold}{\mbox{\isa{fold}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] expand (or fold back) the |
823 given definitions throughout all goals; any chained facts provided |
823 given definitions throughout all goals; any chained facts provided |
824 are inserted into the goal and subject to rewriting as well. |
824 are inserted into the goal and subject to rewriting as well. |
825 |
825 |
826 \item [\mbox{\isa{insert}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] inserts |
826 \item [\hyperlink{method.insert}{\mbox{\isa{insert}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] inserts |
827 theorems as facts into all goals of the proof state. Note that |
827 theorems as facts into all goals of the proof state. Note that |
828 current facts indicated for forward chaining are ignored. |
828 current facts indicated for forward chaining are ignored. |
829 |
829 |
830 \item [\mbox{\isa{erule}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}, \mbox{\isa{drule}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}, and \mbox{\isa{frule}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] are similar to the basic \mbox{\isa{rule}} |
830 \item [\hyperlink{method.erule}{\mbox{\isa{erule}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}, \hyperlink{method.drule}{\mbox{\isa{drule}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}, and \hyperlink{method.frule}{\mbox{\isa{frule}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] are similar to the basic \hyperlink{method.rule}{\mbox{\isa{rule}}} |
831 method (see \secref{sec:pure-meth-att}), but apply rules by |
831 method (see \secref{sec:pure-meth-att}), but apply rules by |
832 elim-resolution, destruct-resolution, and forward-resolution, |
832 elim-resolution, destruct-resolution, and forward-resolution, |
833 respectively \cite{isabelle-ref}. The optional natural number |
833 respectively \cite{isabelle-ref}. The optional natural number |
834 argument (default 0) specifies additional assumption steps to be |
834 argument (default 0) specifies additional assumption steps to be |
835 performed here. |
835 performed here. |
837 Note that these methods are improper ones, mainly serving for |
837 Note that these methods are improper ones, mainly serving for |
838 experimentation and tactic script emulation. Different modes of |
838 experimentation and tactic script emulation. Different modes of |
839 basic rule application are usually expressed in Isar at the proof |
839 basic rule application are usually expressed in Isar at the proof |
840 language level, rather than via implicit proof state manipulations. |
840 language level, rather than via implicit proof state manipulations. |
841 For example, a proper single-step elimination would be done using |
841 For example, a proper single-step elimination would be done using |
842 the plain \mbox{\isa{rule}} method, with forward chaining of current |
842 the plain \hyperlink{method.rule}{\mbox{\isa{rule}}} method, with forward chaining of current |
843 facts. |
843 facts. |
844 |
844 |
845 \item [\mbox{\isa{succeed}}] yields a single (unchanged) result; it is |
845 \item [\hyperlink{method.succeed}{\mbox{\isa{succeed}}}] yields a single (unchanged) result; it is |
846 the identity of the ``\isa{{\isachardoublequote}{\isacharcomma}{\isachardoublequote}}'' method combinator (cf.\ |
846 the identity of the ``\isa{{\isachardoublequote}{\isacharcomma}{\isachardoublequote}}'' method combinator (cf.\ |
847 \secref{sec:syn-meth}). |
847 \secref{sec:syn-meth}). |
848 |
848 |
849 \item [\mbox{\isa{fail}}] yields an empty result sequence; it is the |
849 \item [\hyperlink{method.fail}{\mbox{\isa{fail}}}] yields an empty result sequence; it is the |
850 identity of the ``\isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}'' method combinator (cf.\ |
850 identity of the ``\isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}'' method combinator (cf.\ |
851 \secref{sec:syn-meth}). |
851 \secref{sec:syn-meth}). |
852 |
852 |
853 \end{descr} |
853 \end{descr} |
854 |
854 |
855 \begin{matharray}{rcl} |
855 \begin{matharray}{rcl} |
856 \indexdef{}{attribute}{tagged}\mbox{\isa{tagged}} & : & \isaratt \\ |
856 \indexdef{}{attribute}{tagged}\hypertarget{attribute.tagged}{\hyperlink{attribute.tagged}{\mbox{\isa{tagged}}}} & : & \isaratt \\ |
857 \indexdef{}{attribute}{untagged}\mbox{\isa{untagged}} & : & \isaratt \\[0.5ex] |
857 \indexdef{}{attribute}{untagged}\hypertarget{attribute.untagged}{\hyperlink{attribute.untagged}{\mbox{\isa{untagged}}}} & : & \isaratt \\[0.5ex] |
858 \indexdef{}{attribute}{THEN}\mbox{\isa{THEN}} & : & \isaratt \\ |
858 \indexdef{}{attribute}{THEN}\hypertarget{attribute.THEN}{\hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}} & : & \isaratt \\ |
859 \indexdef{}{attribute}{COMP}\mbox{\isa{COMP}} & : & \isaratt \\[0.5ex] |
859 \indexdef{}{attribute}{COMP}\hypertarget{attribute.COMP}{\hyperlink{attribute.COMP}{\mbox{\isa{COMP}}}} & : & \isaratt \\[0.5ex] |
860 \indexdef{}{attribute}{unfolded}\mbox{\isa{unfolded}} & : & \isaratt \\ |
860 \indexdef{}{attribute}{unfolded}\hypertarget{attribute.unfolded}{\hyperlink{attribute.unfolded}{\mbox{\isa{unfolded}}}} & : & \isaratt \\ |
861 \indexdef{}{attribute}{folded}\mbox{\isa{folded}} & : & \isaratt \\[0.5ex] |
861 \indexdef{}{attribute}{folded}\hypertarget{attribute.folded}{\hyperlink{attribute.folded}{\mbox{\isa{folded}}}} & : & \isaratt \\[0.5ex] |
862 \indexdef{}{attribute}{rotated}\mbox{\isa{rotated}} & : & \isaratt \\ |
862 \indexdef{}{attribute}{rotated}\hypertarget{attribute.rotated}{\hyperlink{attribute.rotated}{\mbox{\isa{rotated}}}} & : & \isaratt \\ |
863 \indexdef{Pure}{attribute}{elim\_format}\mbox{\isa{elim{\isacharunderscore}format}} & : & \isaratt \\ |
863 \indexdef{Pure}{attribute}{elim\_format}\hypertarget{attribute.Pure.elim_format}{\hyperlink{attribute.Pure.elim_format}{\mbox{\isa{elim{\isacharunderscore}format}}}} & : & \isaratt \\ |
864 \indexdef{}{attribute}{standard}\mbox{\isa{standard}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isaratt \\ |
864 \indexdef{}{attribute}{standard}\hypertarget{attribute.standard}{\hyperlink{attribute.standard}{\mbox{\isa{standard}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isaratt \\ |
865 \indexdef{}{attribute}{no\_vars}\mbox{\isa{no{\isacharunderscore}vars}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isaratt \\ |
865 \indexdef{}{attribute}{no\_vars}\hypertarget{attribute.no_vars}{\hyperlink{attribute.no_vars}{\mbox{\isa{no{\isacharunderscore}vars}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isaratt \\ |
866 \end{matharray} |
866 \end{matharray} |
867 |
867 |
868 \begin{rail} |
868 \begin{rail} |
869 'tagged' nameref |
869 'tagged' nameref |
870 ; |
870 ; |
877 'rotated' ( int )? |
877 'rotated' ( int )? |
878 \end{rail} |
878 \end{rail} |
879 |
879 |
880 \begin{descr} |
880 \begin{descr} |
881 |
881 |
882 \item [\mbox{\isa{tagged}}~\isa{{\isachardoublequote}name\ arg{\isachardoublequote}} and \mbox{\isa{untagged}}~\isa{name}] add and remove \emph{tags} of some theorem. |
882 \item [\hyperlink{attribute.tagged}{\mbox{\isa{tagged}}}~\isa{{\isachardoublequote}name\ arg{\isachardoublequote}} and \hyperlink{attribute.untagged}{\mbox{\isa{untagged}}}~\isa{name}] add and remove \emph{tags} of some theorem. |
883 Tags may be any list of string pairs that serve as formal comment. |
883 Tags may be any list of string pairs that serve as formal comment. |
884 The first string is considered the tag name, the second its |
884 The first string is considered the tag name, the second its |
885 argument. Note that \mbox{\isa{untagged}} removes any tags of the |
885 argument. Note that \hyperlink{attribute.untagged}{\mbox{\isa{untagged}}} removes any tags of the |
886 same name. |
886 same name. |
887 |
887 |
888 \item [\mbox{\isa{THEN}}~\isa{a} and \mbox{\isa{COMP}}~\isa{a}] |
888 \item [\hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}~\isa{a} and \hyperlink{attribute.COMP}{\mbox{\isa{COMP}}}~\isa{a}] |
889 compose rules by resolution. \mbox{\isa{THEN}} resolves with the |
889 compose rules by resolution. \hyperlink{attribute.THEN}{\mbox{\isa{THEN}}} resolves with the |
890 first premise of \isa{a} (an alternative position may be also |
890 first premise of \isa{a} (an alternative position may be also |
891 specified); the \mbox{\isa{COMP}} version skips the automatic |
891 specified); the \hyperlink{attribute.COMP}{\mbox{\isa{COMP}}} version skips the automatic |
892 lifting process that is normally intended (cf.\ \verb|"op RS"| and |
892 lifting process that is normally intended (cf.\ \verb|"op RS"| and |
893 \verb|"op COMP"| in \cite[\S5]{isabelle-ref}). |
893 \verb|"op COMP"| in \cite[\S5]{isabelle-ref}). |
894 |
894 |
895 \item [\mbox{\isa{unfolded}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} and |
895 \item [\hyperlink{attribute.unfolded}{\mbox{\isa{unfolded}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} and |
896 \mbox{\isa{folded}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] expand and fold |
896 \hyperlink{attribute.folded}{\mbox{\isa{folded}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] expand and fold |
897 back again the given definitions throughout a rule. |
897 back again the given definitions throughout a rule. |
898 |
898 |
899 \item [\mbox{\isa{rotated}}~\isa{n}] rotate the premises of a |
899 \item [\hyperlink{attribute.rotated}{\mbox{\isa{rotated}}}~\isa{n}] rotate the premises of a |
900 theorem by \isa{n} (default 1). |
900 theorem by \isa{n} (default 1). |
901 |
901 |
902 \item [\mbox{\isa{Pure{\isachardot}elim{\isacharunderscore}format}}] turns a destruction rule into |
902 \item [\hyperlink{attribute.Pure.elim_format}{\mbox{\isa{Pure{\isachardot}elim{\isacharunderscore}format}}}] turns a destruction rule into |
903 elimination rule format, by resolving with the rule \isa{{\isachardoublequote}PROP\ A\ {\isasymLongrightarrow}\ {\isacharparenleft}PROP\ A\ {\isasymLongrightarrow}\ PROP\ B{\isacharparenright}\ {\isasymLongrightarrow}\ PROP\ B{\isachardoublequote}}. |
903 elimination rule format, by resolving with the rule \isa{{\isachardoublequote}PROP\ A\ {\isasymLongrightarrow}\ {\isacharparenleft}PROP\ A\ {\isasymLongrightarrow}\ PROP\ B{\isacharparenright}\ {\isasymLongrightarrow}\ PROP\ B{\isachardoublequote}}. |
904 |
904 |
905 Note that the Classical Reasoner (\secref{sec:classical}) provides |
905 Note that the Classical Reasoner (\secref{sec:classical}) provides |
906 its own version of this operation. |
906 its own version of this operation. |
907 |
907 |
908 \item [\mbox{\isa{standard}}] puts a theorem into the standard form |
908 \item [\hyperlink{attribute.standard}{\mbox{\isa{standard}}}] puts a theorem into the standard form |
909 of object-rules at the outermost theory level. Note that this |
909 of object-rules at the outermost theory level. Note that this |
910 operation violates the local proof context (including active |
910 operation violates the local proof context (including active |
911 locales). |
911 locales). |
912 |
912 |
913 \item [\mbox{\isa{no{\isacharunderscore}vars}}] replaces schematic variables by free |
913 \item [\hyperlink{attribute.no_vars}{\mbox{\isa{no{\isacharunderscore}vars}}}] replaces schematic variables by free |
914 ones; this is mainly for tuning output of pretty printed theorems. |
914 ones; this is mainly for tuning output of pretty printed theorems. |
915 |
915 |
916 \end{descr}% |
916 \end{descr}% |
917 \end{isamarkuptext}% |
917 \end{isamarkuptext}% |
918 \isamarkuptrue% |
918 \isamarkuptrue% |
944 |
944 |
945 Note that the tactic emulation proof methods in Isabelle/Isar are |
945 Note that the tactic emulation proof methods in Isabelle/Isar are |
946 consistently named \isa{foo{\isacharunderscore}tac}. Note also that variable names |
946 consistently named \isa{foo{\isacharunderscore}tac}. Note also that variable names |
947 occurring on left hand sides of instantiations must be preceded by a |
947 occurring on left hand sides of instantiations must be preceded by a |
948 question mark if they coincide with a keyword or contain dots. This |
948 question mark if they coincide with a keyword or contain dots. This |
949 is consistent with the attribute \mbox{\isa{where}} (see |
949 is consistent with the attribute \hyperlink{attribute.where}{\mbox{\isa{where}}} (see |
950 \secref{sec:pure-meth-att}). |
950 \secref{sec:pure-meth-att}). |
951 |
951 |
952 \begin{matharray}{rcl} |
952 \begin{matharray}{rcl} |
953 \indexdef{}{method}{rule\_tac}\mbox{\isa{rule{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
953 \indexdef{}{method}{rule\_tac}\hypertarget{method.rule_tac}{\hyperlink{method.rule_tac}{\mbox{\isa{rule{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
954 \indexdef{}{method}{erule\_tac}\mbox{\isa{erule{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
954 \indexdef{}{method}{erule\_tac}\hypertarget{method.erule_tac}{\hyperlink{method.erule_tac}{\mbox{\isa{erule{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
955 \indexdef{}{method}{drule\_tac}\mbox{\isa{drule{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
955 \indexdef{}{method}{drule\_tac}\hypertarget{method.drule_tac}{\hyperlink{method.drule_tac}{\mbox{\isa{drule{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
956 \indexdef{}{method}{frule\_tac}\mbox{\isa{frule{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
956 \indexdef{}{method}{frule\_tac}\hypertarget{method.frule_tac}{\hyperlink{method.frule_tac}{\mbox{\isa{frule{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
957 \indexdef{}{method}{cut\_tac}\mbox{\isa{cut{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
957 \indexdef{}{method}{cut\_tac}\hypertarget{method.cut_tac}{\hyperlink{method.cut_tac}{\mbox{\isa{cut{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
958 \indexdef{}{method}{thin\_tac}\mbox{\isa{thin{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
958 \indexdef{}{method}{thin\_tac}\hypertarget{method.thin_tac}{\hyperlink{method.thin_tac}{\mbox{\isa{thin{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
959 \indexdef{}{method}{subgoal\_tac}\mbox{\isa{subgoal{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
959 \indexdef{}{method}{subgoal\_tac}\hypertarget{method.subgoal_tac}{\hyperlink{method.subgoal_tac}{\mbox{\isa{subgoal{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
960 \indexdef{}{method}{rename\_tac}\mbox{\isa{rename{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
960 \indexdef{}{method}{rename\_tac}\hypertarget{method.rename_tac}{\hyperlink{method.rename_tac}{\mbox{\isa{rename{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
961 \indexdef{}{method}{rotate\_tac}\mbox{\isa{rotate{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
961 \indexdef{}{method}{rotate\_tac}\hypertarget{method.rotate_tac}{\hyperlink{method.rotate_tac}{\mbox{\isa{rotate{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
962 \indexdef{}{method}{tactic}\mbox{\isa{tactic}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
962 \indexdef{}{method}{tactic}\hypertarget{method.tactic}{\hyperlink{method.tactic}{\mbox{\isa{tactic}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
963 \end{matharray} |
963 \end{matharray} |
964 |
964 |
965 \begin{rail} |
965 \begin{rail} |
966 ( 'rule\_tac' | 'erule\_tac' | 'drule\_tac' | 'frule\_tac' | 'cut\_tac' | 'thin\_tac' ) goalspec? |
966 ( 'rule\_tac' | 'erule\_tac' | 'drule\_tac' | 'frule\_tac' | 'cut\_tac' | 'thin\_tac' ) goalspec? |
967 ( insts thmref | thmrefs ) |
967 ( insts thmref | thmrefs ) |
979 ; |
979 ; |
980 \end{rail} |
980 \end{rail} |
981 |
981 |
982 \begin{descr} |
982 \begin{descr} |
983 |
983 |
984 \item [\mbox{\isa{rule{\isacharunderscore}tac}} etc.] do resolution of rules with explicit |
984 \item [\hyperlink{method.rule_tac}{\mbox{\isa{rule{\isacharunderscore}tac}}} etc.] do resolution of rules with explicit |
985 instantiation. This works the same way as the ML tactics \verb|res_inst_tac| etc. (see \cite[\S3]{isabelle-ref}). |
985 instantiation. This works the same way as the ML tactics \verb|res_inst_tac| etc. (see \cite[\S3]{isabelle-ref}). |
986 |
986 |
987 Multiple rules may be only given if there is no instantiation; then |
987 Multiple rules may be only given if there is no instantiation; then |
988 \mbox{\isa{rule{\isacharunderscore}tac}} is the same as \verb|resolve_tac| in ML (see |
988 \hyperlink{method.rule_tac}{\mbox{\isa{rule{\isacharunderscore}tac}}} is the same as \verb|resolve_tac| in ML (see |
989 \cite[\S3]{isabelle-ref}). |
989 \cite[\S3]{isabelle-ref}). |
990 |
990 |
991 \item [\mbox{\isa{cut{\isacharunderscore}tac}}] inserts facts into the proof state as |
991 \item [\hyperlink{method.cut_tac}{\mbox{\isa{cut{\isacharunderscore}tac}}}] inserts facts into the proof state as |
992 assumption of a subgoal, see also \verb|cut_facts_tac| in |
992 assumption of a subgoal, see also \verb|cut_facts_tac| in |
993 \cite[\S3]{isabelle-ref}. Note that the scope of schematic |
993 \cite[\S3]{isabelle-ref}. Note that the scope of schematic |
994 variables is spread over the main goal statement. Instantiations |
994 variables is spread over the main goal statement. Instantiations |
995 may be given as well, see also ML tactic \verb|cut_inst_tac| in |
995 may be given as well, see also ML tactic \verb|cut_inst_tac| in |
996 \cite[\S3]{isabelle-ref}. |
996 \cite[\S3]{isabelle-ref}. |
997 |
997 |
998 \item [\mbox{\isa{thin{\isacharunderscore}tac}}~\isa{{\isasymphi}}] deletes the specified |
998 \item [\hyperlink{method.thin_tac}{\mbox{\isa{thin{\isacharunderscore}tac}}}~\isa{{\isasymphi}}] deletes the specified |
999 assumption from a subgoal; note that \isa{{\isasymphi}} may contain schematic |
999 assumption from a subgoal; note that \isa{{\isasymphi}} may contain schematic |
1000 variables. See also \verb|thin_tac| in \cite[\S3]{isabelle-ref}. |
1000 variables. See also \verb|thin_tac| in \cite[\S3]{isabelle-ref}. |
1001 |
1001 |
1002 \item [\mbox{\isa{subgoal{\isacharunderscore}tac}}~\isa{{\isasymphi}}] adds \isa{{\isasymphi}} as an |
1002 \item [\hyperlink{method.subgoal_tac}{\mbox{\isa{subgoal{\isacharunderscore}tac}}}~\isa{{\isasymphi}}] adds \isa{{\isasymphi}} as an |
1003 assumption to a subgoal. See also \verb|subgoal_tac| and \verb|subgoals_tac| in \cite[\S3]{isabelle-ref}. |
1003 assumption to a subgoal. See also \verb|subgoal_tac| and \verb|subgoals_tac| in \cite[\S3]{isabelle-ref}. |
1004 |
1004 |
1005 \item [\mbox{\isa{rename{\isacharunderscore}tac}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isachardoublequote}}] renames |
1005 \item [\hyperlink{method.rename_tac}{\mbox{\isa{rename{\isacharunderscore}tac}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isachardoublequote}}] renames |
1006 parameters of a goal according to the list \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub n{\isachardoublequote}}, which refers to the \emph{suffix} of variables. |
1006 parameters of a goal according to the list \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub n{\isachardoublequote}}, which refers to the \emph{suffix} of variables. |
1007 |
1007 |
1008 \item [\mbox{\isa{rotate{\isacharunderscore}tac}}~\isa{n}] rotates the assumptions of a |
1008 \item [\hyperlink{method.rotate_tac}{\mbox{\isa{rotate{\isacharunderscore}tac}}}~\isa{n}] rotates the assumptions of a |
1009 goal by \isa{n} positions: from right to left if \isa{n} is |
1009 goal by \isa{n} positions: from right to left if \isa{n} is |
1010 positive, and from left to right if \isa{n} is negative; the |
1010 positive, and from left to right if \isa{n} is negative; the |
1011 default value is 1. See also \verb|rotate_tac| in |
1011 default value is 1. See also \verb|rotate_tac| in |
1012 \cite[\S3]{isabelle-ref}. |
1012 \cite[\S3]{isabelle-ref}. |
1013 |
1013 |
1014 \item [\mbox{\isa{tactic}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] produces a proof method from |
1014 \item [\hyperlink{method.tactic}{\mbox{\isa{tactic}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] produces a proof method from |
1015 any ML text of type \verb|tactic|. Apart from the usual ML |
1015 any ML text of type \verb|tactic|. Apart from the usual ML |
1016 environment and the current implicit theory context, the ML code may |
1016 environment and the current implicit theory context, the ML code may |
1017 refer to the following locally bound values: |
1017 refer to the following locally bound values: |
1018 |
1018 |
1019 %FIXME check |
1019 %FIXME check |
1073 Splitter (see also \cite{isabelle-ref}), the default is to add. |
1073 Splitter (see also \cite{isabelle-ref}), the default is to add. |
1074 This works only if the Simplifier method has been properly setup to |
1074 This works only if the Simplifier method has been properly setup to |
1075 include the Splitter (all major object logics such HOL, HOLCF, FOL, |
1075 include the Splitter (all major object logics such HOL, HOLCF, FOL, |
1076 ZF do this already). |
1076 ZF do this already). |
1077 |
1077 |
1078 \item [\mbox{\isa{simp{\isacharunderscore}all}}] is similar to \mbox{\isa{simp}}, but acts on |
1078 \item [\hyperlink{method.simp_all}{\mbox{\isa{simp{\isacharunderscore}all}}}] is similar to \hyperlink{method.simp}{\mbox{\isa{simp}}}, but acts on |
1079 all goals (backwards from the last to the first one). |
1079 all goals (backwards from the last to the first one). |
1080 |
1080 |
1081 \end{descr} |
1081 \end{descr} |
1082 |
1082 |
1083 By default the Simplifier methods take local assumptions fully into |
1083 By default the Simplifier methods take local assumptions fully into |
1084 account, using equational assumptions in the subsequent |
1084 account, using equational assumptions in the subsequent |
1085 normalization process, or simplifying assumptions themselves (cf.\ |
1085 normalization process, or simplifying assumptions themselves (cf.\ |
1086 \verb|asm_full_simp_tac| in \cite[\S10]{isabelle-ref}). In |
1086 \verb|asm_full_simp_tac| in \cite[\S10]{isabelle-ref}). In |
1087 structured proofs this is usually quite well behaved in practice: |
1087 structured proofs this is usually quite well behaved in practice: |
1088 just the local premises of the actual goal are involved, additional |
1088 just the local premises of the actual goal are involved, additional |
1089 facts may be inserted via explicit forward-chaining (via \mbox{\isa{\isacommand{then}}}, \mbox{\isa{\isacommand{from}}}, \mbox{\isa{\isacommand{using}}} etc.). The full |
1089 facts may be inserted via explicit forward-chaining (via \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}, \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}, \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}} etc.). The full |
1090 context of premises is only included if the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' (bang) |
1090 context of premises is only included if the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' (bang) |
1091 argument is given, which should be used with some care, though. |
1091 argument is given, which should be used with some care, though. |
1092 |
1092 |
1093 Additional Simplifier options may be specified to tune the behavior |
1093 Additional Simplifier options may be specified to tune the behavior |
1094 further (mostly for unstructured scripts with many accidental local |
1094 further (mostly for unstructured scripts with many accidental local |
1114 } |
1114 } |
1115 \isamarkuptrue% |
1115 \isamarkuptrue% |
1116 % |
1116 % |
1117 \begin{isamarkuptext}% |
1117 \begin{isamarkuptext}% |
1118 \begin{matharray}{rcl} |
1118 \begin{matharray}{rcl} |
1119 \indexdef{}{command}{print\_simpset}\mbox{\isa{\isacommand{print{\isacharunderscore}simpset}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
1119 \indexdef{}{command}{print\_simpset}\hypertarget{command.print_simpset}{\hyperlink{command.print_simpset}{\mbox{\isa{\isacommand{print{\isacharunderscore}simpset}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
1120 \indexdef{}{attribute}{simp}\mbox{\isa{simp}} & : & \isaratt \\ |
1120 \indexdef{}{attribute}{simp}\hypertarget{attribute.simp}{\hyperlink{attribute.simp}{\mbox{\isa{simp}}}} & : & \isaratt \\ |
1121 \indexdef{}{attribute}{cong}\mbox{\isa{cong}} & : & \isaratt \\ |
1121 \indexdef{}{attribute}{cong}\hypertarget{attribute.cong}{\hyperlink{attribute.cong}{\mbox{\isa{cong}}}} & : & \isaratt \\ |
1122 \indexdef{}{attribute}{split}\mbox{\isa{split}} & : & \isaratt \\ |
1122 \indexdef{}{attribute}{split}\hypertarget{attribute.split}{\hyperlink{attribute.split}{\mbox{\isa{split}}}} & : & \isaratt \\ |
1123 \end{matharray} |
1123 \end{matharray} |
1124 |
1124 |
1125 \begin{rail} |
1125 \begin{rail} |
1126 ('simp' | 'cong' | 'split') (() | 'add' | 'del') |
1126 ('simp' | 'cong' | 'split') (() | 'add' | 'del') |
1127 ; |
1127 ; |
1128 \end{rail} |
1128 \end{rail} |
1129 |
1129 |
1130 \begin{descr} |
1130 \begin{descr} |
1131 |
1131 |
1132 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}simpset}}}] prints the collection of rules |
1132 \item [\hyperlink{command.print_simpset}{\mbox{\isa{\isacommand{print{\isacharunderscore}simpset}}}}] prints the collection of rules |
1133 declared to the Simplifier, which is also known as ``simpset'' |
1133 declared to the Simplifier, which is also known as ``simpset'' |
1134 internally \cite{isabelle-ref}. |
1134 internally \cite{isabelle-ref}. |
1135 |
1135 |
1136 \item [\mbox{\isa{simp}}] declares simplification rules. |
1136 \item [\hyperlink{attribute.simp}{\mbox{\isa{simp}}}] declares simplification rules. |
1137 |
1137 |
1138 \item [\mbox{\isa{cong}}] declares congruence rules. |
1138 \item [\hyperlink{attribute.cong}{\mbox{\isa{cong}}}] declares congruence rules. |
1139 |
1139 |
1140 \item [\mbox{\isa{split}}] declares case split rules. |
1140 \item [\hyperlink{attribute.split}{\mbox{\isa{split}}}] declares case split rules. |
1141 |
1141 |
1142 \end{descr}% |
1142 \end{descr}% |
1143 \end{isamarkuptext}% |
1143 \end{isamarkuptext}% |
1144 \isamarkuptrue% |
1144 \isamarkuptrue% |
1145 % |
1145 % |
1161 ; |
1161 ; |
1162 \end{rail} |
1162 \end{rail} |
1163 |
1163 |
1164 \begin{descr} |
1164 \begin{descr} |
1165 |
1165 |
1166 \item [\mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}}] defines a named simplification |
1166 \item [\hyperlink{command.simproc_setup}{\mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}}}] defines a named simplification |
1167 procedure that is invoked by the Simplifier whenever any of the |
1167 procedure that is invoked by the Simplifier whenever any of the |
1168 given term patterns match the current redex. The implementation, |
1168 given term patterns match the current redex. The implementation, |
1169 which is provided as ML source text, needs to be of type \verb|"morphism -> simpset -> cterm -> thm option"|, where the \verb|cterm| represents the current redex \isa{r} and the result is |
1169 which is provided as ML source text, needs to be of type \verb|"morphism -> simpset -> cterm -> thm option"|, where the \verb|cterm| represents the current redex \isa{r} and the result is |
1170 supposed to be some proven rewrite rule \isa{{\isachardoublequote}r\ {\isasymequiv}\ r{\isacharprime}{\isachardoublequote}} (or a |
1170 supposed to be some proven rewrite rule \isa{{\isachardoublequote}r\ {\isasymequiv}\ r{\isacharprime}{\isachardoublequote}} (or a |
1171 generalized version), or \verb|NONE| to indicate failure. The |
1171 generalized version), or \verb|NONE| to indicate failure. The |
1172 \verb|simpset| argument holds the full context of the current |
1172 \verb|simpset| argument holds the full context of the current |
1173 Simplifier invocation, including the actual Isar proof context. The |
1173 Simplifier invocation, including the actual Isar proof context. The |
1174 \verb|morphism| informs about the difference of the original |
1174 \verb|morphism| informs about the difference of the original |
1175 compilation context wrt.\ the one of the actual application later |
1175 compilation context wrt.\ the one of the actual application later |
1176 on. The optional \mbox{\isa{\isakeyword{identifier}}} specifies theorems that |
1176 on. The optional \hyperlink{keyword.identifier}{\mbox{\isa{\isakeyword{identifier}}}} specifies theorems that |
1177 represent the logical content of the abstract theory of this |
1177 represent the logical content of the abstract theory of this |
1178 simproc. |
1178 simproc. |
1179 |
1179 |
1180 Morphisms and identifiers are only relevant for simprocs that are |
1180 Morphisms and identifiers are only relevant for simprocs that are |
1181 defined within a local target context, e.g.\ in a locale. |
1181 defined within a local target context, e.g.\ in a locale. |
1182 |
1182 |
1183 \item [\isa{{\isachardoublequote}simproc\ add{\isacharcolon}\ name{\isachardoublequote}} and \isa{{\isachardoublequote}simproc\ del{\isacharcolon}\ name{\isachardoublequote}}] |
1183 \item [\isa{{\isachardoublequote}simproc\ add{\isacharcolon}\ name{\isachardoublequote}} and \isa{{\isachardoublequote}simproc\ del{\isacharcolon}\ name{\isachardoublequote}}] |
1184 add or delete named simprocs to the current Simplifier context. The |
1184 add or delete named simprocs to the current Simplifier context. The |
1185 default is to add a simproc. Note that \mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}} |
1185 default is to add a simproc. Note that \hyperlink{command.simproc_setup}{\mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}}} |
1186 already adds the new simproc to the subsequent context. |
1186 already adds the new simproc to the subsequent context. |
1187 |
1187 |
1188 \end{descr}% |
1188 \end{descr}% |
1189 \end{isamarkuptext}% |
1189 \end{isamarkuptext}% |
1190 \isamarkuptrue% |
1190 \isamarkuptrue% |
1249 provide the canonical way for automated normalization (see |
1249 provide the canonical way for automated normalization (see |
1250 \secref{sec:simplifier}). |
1250 \secref{sec:simplifier}). |
1251 |
1251 |
1252 \begin{descr} |
1252 \begin{descr} |
1253 |
1253 |
1254 \item [\mbox{\isa{subst}}~\isa{eq}] performs a single substitution |
1254 \item [\hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{eq}] performs a single substitution |
1255 step using rule \isa{eq}, which may be either a meta or object |
1255 step using rule \isa{eq}, which may be either a meta or object |
1256 equality. |
1256 equality. |
1257 |
1257 |
1258 \item [\mbox{\isa{subst}}~\isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharparenright}\ eq{\isachardoublequote}}] substitutes in an |
1258 \item [\hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharparenright}\ eq{\isachardoublequote}}] substitutes in an |
1259 assumption. |
1259 assumption. |
1260 |
1260 |
1261 \item [\mbox{\isa{subst}}~\isa{{\isachardoublequote}{\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}\ eq{\isachardoublequote}}] performs several |
1261 \item [\hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{{\isachardoublequote}{\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}\ eq{\isachardoublequote}}] performs several |
1262 substitutions in the conclusion. The numbers \isa{i} to \isa{j} |
1262 substitutions in the conclusion. The numbers \isa{i} to \isa{j} |
1263 indicate the positions to substitute at. Positions are ordered from |
1263 indicate the positions to substitute at. Positions are ordered from |
1264 the top of the term tree moving down from left to right. For |
1264 the top of the term tree moving down from left to right. For |
1265 example, in \isa{{\isachardoublequote}{\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}c\ {\isacharplus}\ d{\isacharparenright}{\isachardoublequote}} there are three positions |
1265 example, in \isa{{\isachardoublequote}{\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}c\ {\isacharplus}\ d{\isacharparenright}{\isachardoublequote}} there are three positions |
1266 where commutativity of \isa{{\isachardoublequote}{\isacharplus}{\isachardoublequote}} is applicable: 1 refers to the |
1266 where commutativity of \isa{{\isachardoublequote}{\isacharplus}{\isachardoublequote}} is applicable: 1 refers to the |
1269 If the positions in the list \isa{{\isachardoublequote}{\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}{\isachardoublequote}} are non-overlapping |
1269 If the positions in the list \isa{{\isachardoublequote}{\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}{\isachardoublequote}} are non-overlapping |
1270 (e.g.\ \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{2}}\ {\isadigit{3}}{\isacharparenright}{\isachardoublequote}} in \isa{{\isachardoublequote}{\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}c\ {\isacharplus}\ d{\isacharparenright}{\isachardoublequote}}) you may |
1270 (e.g.\ \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{2}}\ {\isadigit{3}}{\isacharparenright}{\isachardoublequote}} in \isa{{\isachardoublequote}{\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}c\ {\isacharplus}\ d{\isacharparenright}{\isachardoublequote}}) you may |
1271 assume all substitutions are performed simultaneously. Otherwise |
1271 assume all substitutions are performed simultaneously. Otherwise |
1272 the behaviour of \isa{subst} is not specified. |
1272 the behaviour of \isa{subst} is not specified. |
1273 |
1273 |
1274 \item [\mbox{\isa{subst}}~\isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharparenright}\ {\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}\ eq{\isachardoublequote}}] performs the |
1274 \item [\hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharparenright}\ {\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}\ eq{\isachardoublequote}}] performs the |
1275 substitutions in the assumptions. Positions \isa{{\isachardoublequote}{\isadigit{1}}\ {\isasymdots}\ i\isactrlsub {\isadigit{1}}{\isachardoublequote}} |
1275 substitutions in the assumptions. Positions \isa{{\isachardoublequote}{\isadigit{1}}\ {\isasymdots}\ i\isactrlsub {\isadigit{1}}{\isachardoublequote}} |
1276 refer to assumption 1, positions \isa{{\isachardoublequote}i\isactrlsub {\isadigit{1}}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymdots}\ i\isactrlsub {\isadigit{2}}{\isachardoublequote}} |
1276 refer to assumption 1, positions \isa{{\isachardoublequote}i\isactrlsub {\isadigit{1}}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymdots}\ i\isactrlsub {\isadigit{2}}{\isachardoublequote}} |
1277 to assumption 2, and so on. |
1277 to assumption 2, and so on. |
1278 |
1278 |
1279 \item [\mbox{\isa{hypsubst}}] performs substitution using some |
1279 \item [\hyperlink{method.hypsubst}{\mbox{\isa{hypsubst}}}] performs substitution using some |
1280 assumption; this only works for equations of the form \isa{{\isachardoublequote}x\ {\isacharequal}\ t{\isachardoublequote}} where \isa{x} is a free or bound variable. |
1280 assumption; this only works for equations of the form \isa{{\isachardoublequote}x\ {\isacharequal}\ t{\isachardoublequote}} where \isa{x} is a free or bound variable. |
1281 |
1281 |
1282 \item [\mbox{\isa{split}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] performs |
1282 \item [\hyperlink{method.split}{\mbox{\isa{split}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] performs |
1283 single-step case splitting using the given rules. By default, |
1283 single-step case splitting using the given rules. By default, |
1284 splitting is performed in the conclusion of a goal; the \isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharparenright}{\isachardoublequote}} option indicates to operate on assumptions instead. |
1284 splitting is performed in the conclusion of a goal; the \isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharparenright}{\isachardoublequote}} option indicates to operate on assumptions instead. |
1285 |
1285 |
1286 Note that the \mbox{\isa{simp}} method already involves repeated |
1286 Note that the \hyperlink{method.simp}{\mbox{\isa{simp}}} method already involves repeated |
1287 application of split rules as declared in the current context. |
1287 application of split rules as declared in the current context. |
1288 |
1288 |
1289 \end{descr}% |
1289 \end{descr}% |
1290 \end{isamarkuptext}% |
1290 \end{isamarkuptext}% |
1291 \isamarkuptrue% |
1291 \isamarkuptrue% |
1298 } |
1298 } |
1299 \isamarkuptrue% |
1299 \isamarkuptrue% |
1300 % |
1300 % |
1301 \begin{isamarkuptext}% |
1301 \begin{isamarkuptext}% |
1302 \begin{matharray}{rcl} |
1302 \begin{matharray}{rcl} |
1303 \indexdef{}{method}{rule}\mbox{\isa{rule}} & : & \isarmeth \\ |
1303 \indexdef{}{method}{rule}\hypertarget{method.rule}{\hyperlink{method.rule}{\mbox{\isa{rule}}}} & : & \isarmeth \\ |
1304 \indexdef{}{method}{contradiction}\mbox{\isa{contradiction}} & : & \isarmeth \\ |
1304 \indexdef{}{method}{contradiction}\hypertarget{method.contradiction}{\hyperlink{method.contradiction}{\mbox{\isa{contradiction}}}} & : & \isarmeth \\ |
1305 \indexdef{}{method}{intro}\mbox{\isa{intro}} & : & \isarmeth \\ |
1305 \indexdef{}{method}{intro}\hypertarget{method.intro}{\hyperlink{method.intro}{\mbox{\isa{intro}}}} & : & \isarmeth \\ |
1306 \indexdef{}{method}{elim}\mbox{\isa{elim}} & : & \isarmeth \\ |
1306 \indexdef{}{method}{elim}\hypertarget{method.elim}{\hyperlink{method.elim}{\mbox{\isa{elim}}}} & : & \isarmeth \\ |
1307 \end{matharray} |
1307 \end{matharray} |
1308 |
1308 |
1309 \begin{rail} |
1309 \begin{rail} |
1310 ('rule' | 'intro' | 'elim') thmrefs? |
1310 ('rule' | 'intro' | 'elim') thmrefs? |
1311 ; |
1311 ; |
1312 \end{rail} |
1312 \end{rail} |
1313 |
1313 |
1314 \begin{descr} |
1314 \begin{descr} |
1315 |
1315 |
1316 \item [\mbox{\isa{rule}}] as offered by the Classical Reasoner is a |
1316 \item [\hyperlink{method.rule}{\mbox{\isa{rule}}}] as offered by the Classical Reasoner is a |
1317 refinement over the primitive one (see \secref{sec:pure-meth-att}). |
1317 refinement over the primitive one (see \secref{sec:pure-meth-att}). |
1318 Both versions essentially work the same, but the classical version |
1318 Both versions essentially work the same, but the classical version |
1319 observes the classical rule context in addition to that of |
1319 observes the classical rule context in addition to that of |
1320 Isabelle/Pure. |
1320 Isabelle/Pure. |
1321 |
1321 |
1322 Common object logics (HOL, ZF, etc.) declare a rich collection of |
1322 Common object logics (HOL, ZF, etc.) declare a rich collection of |
1323 classical rules (even if these would qualify as intuitionistic |
1323 classical rules (even if these would qualify as intuitionistic |
1324 ones), but only few declarations to the rule context of |
1324 ones), but only few declarations to the rule context of |
1325 Isabelle/Pure (\secref{sec:pure-meth-att}). |
1325 Isabelle/Pure (\secref{sec:pure-meth-att}). |
1326 |
1326 |
1327 \item [\mbox{\isa{contradiction}}] solves some goal by contradiction, |
1327 \item [\hyperlink{method.contradiction}{\mbox{\isa{contradiction}}}] solves some goal by contradiction, |
1328 deriving any result from both \isa{{\isachardoublequote}{\isasymnot}\ A{\isachardoublequote}} and \isa{A}. Chained |
1328 deriving any result from both \isa{{\isachardoublequote}{\isasymnot}\ A{\isachardoublequote}} and \isa{A}. Chained |
1329 facts, which are guaranteed to participate, may appear in either |
1329 facts, which are guaranteed to participate, may appear in either |
1330 order. |
1330 order. |
1331 |
1331 |
1332 \item [\mbox{\isa{intro}} and \mbox{\isa{elim}}] repeatedly refine |
1332 \item [\hyperlink{method.intro}{\mbox{\isa{intro}}} and \hyperlink{method.elim}{\mbox{\isa{elim}}}] repeatedly refine some |
1333 some goal by intro- or elim-resolution, after having inserted any |
1333 goal by intro- or elim-resolution, after having inserted any chained |
1334 chained facts. Exactly the rules given as arguments are taken into |
1334 facts. Exactly the rules given as arguments are taken into account; |
1335 account; this allows fine-tuned decomposition of a proof problem, in |
1335 this allows fine-tuned decomposition of a proof problem, in contrast |
1336 contrast to common automated tools. |
1336 to common automated tools. |
1337 |
1337 |
1338 \end{descr}% |
1338 \end{descr}% |
1339 \end{isamarkuptext}% |
1339 \end{isamarkuptext}% |
1340 \isamarkuptrue% |
1340 \isamarkuptrue% |
1341 % |
1341 % |
1343 } |
1343 } |
1344 \isamarkuptrue% |
1344 \isamarkuptrue% |
1345 % |
1345 % |
1346 \begin{isamarkuptext}% |
1346 \begin{isamarkuptext}% |
1347 \begin{matharray}{rcl} |
1347 \begin{matharray}{rcl} |
1348 \indexdef{}{method}{blast}\mbox{\isa{blast}} & : & \isarmeth \\ |
1348 \indexdef{}{method}{blast}\hypertarget{method.blast}{\hyperlink{method.blast}{\mbox{\isa{blast}}}} & : & \isarmeth \\ |
1349 \indexdef{}{method}{fast}\mbox{\isa{fast}} & : & \isarmeth \\ |
1349 \indexdef{}{method}{fast}\hypertarget{method.fast}{\hyperlink{method.fast}{\mbox{\isa{fast}}}} & : & \isarmeth \\ |
1350 \indexdef{}{method}{slow}\mbox{\isa{slow}} & : & \isarmeth \\ |
1350 \indexdef{}{method}{slow}\hypertarget{method.slow}{\hyperlink{method.slow}{\mbox{\isa{slow}}}} & : & \isarmeth \\ |
1351 \indexdef{}{method}{best}\mbox{\isa{best}} & : & \isarmeth \\ |
1351 \indexdef{}{method}{best}\hypertarget{method.best}{\hyperlink{method.best}{\mbox{\isa{best}}}} & : & \isarmeth \\ |
1352 \indexdef{}{method}{safe}\mbox{\isa{safe}} & : & \isarmeth \\ |
1352 \indexdef{}{method}{safe}\hypertarget{method.safe}{\hyperlink{method.safe}{\mbox{\isa{safe}}}} & : & \isarmeth \\ |
1353 \indexdef{}{method}{clarify}\mbox{\isa{clarify}} & : & \isarmeth \\ |
1353 \indexdef{}{method}{clarify}\hypertarget{method.clarify}{\hyperlink{method.clarify}{\mbox{\isa{clarify}}}} & : & \isarmeth \\ |
1354 \end{matharray} |
1354 \end{matharray} |
1355 |
1355 |
1356 \indexouternonterm{clamod} |
1356 \indexouternonterm{clamod} |
1357 \begin{rail} |
1357 \begin{rail} |
1358 'blast' ('!' ?) nat? (clamod *) |
1358 'blast' ('!' ?) nat? (clamod *) |
1388 } |
1388 } |
1389 \isamarkuptrue% |
1389 \isamarkuptrue% |
1390 % |
1390 % |
1391 \begin{isamarkuptext}% |
1391 \begin{isamarkuptext}% |
1392 \begin{matharray}{rcl} |
1392 \begin{matharray}{rcl} |
1393 \indexdef{}{method}{auto}\mbox{\isa{auto}} & : & \isarmeth \\ |
1393 \indexdef{}{method}{auto}\hypertarget{method.auto}{\hyperlink{method.auto}{\mbox{\isa{auto}}}} & : & \isarmeth \\ |
1394 \indexdef{}{method}{force}\mbox{\isa{force}} & : & \isarmeth \\ |
1394 \indexdef{}{method}{force}\hypertarget{method.force}{\hyperlink{method.force}{\mbox{\isa{force}}}} & : & \isarmeth \\ |
1395 \indexdef{}{method}{clarsimp}\mbox{\isa{clarsimp}} & : & \isarmeth \\ |
1395 \indexdef{}{method}{clarsimp}\hypertarget{method.clarsimp}{\hyperlink{method.clarsimp}{\mbox{\isa{clarsimp}}}} & : & \isarmeth \\ |
1396 \indexdef{}{method}{fastsimp}\mbox{\isa{fastsimp}} & : & \isarmeth \\ |
1396 \indexdef{}{method}{fastsimp}\hypertarget{method.fastsimp}{\hyperlink{method.fastsimp}{\mbox{\isa{fastsimp}}}} & : & \isarmeth \\ |
1397 \indexdef{}{method}{slowsimp}\mbox{\isa{slowsimp}} & : & \isarmeth \\ |
1397 \indexdef{}{method}{slowsimp}\hypertarget{method.slowsimp}{\hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}} & : & \isarmeth \\ |
1398 \indexdef{}{method}{bestsimp}\mbox{\isa{bestsimp}} & : & \isarmeth \\ |
1398 \indexdef{}{method}{bestsimp}\hypertarget{method.bestsimp}{\hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}}} & : & \isarmeth \\ |
1399 \end{matharray} |
1399 \end{matharray} |
1400 |
1400 |
1401 \indexouternonterm{clasimpmod} |
1401 \indexouternonterm{clasimpmod} |
1402 \begin{rail} |
1402 \begin{rail} |
1403 'auto' '!'? (nat nat)? (clasimpmod *) |
1403 'auto' '!'? (nat nat)? (clasimpmod *) |
1411 (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs |
1411 (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs |
1412 \end{rail} |
1412 \end{rail} |
1413 |
1413 |
1414 \begin{descr} |
1414 \begin{descr} |
1415 |
1415 |
1416 \item [\mbox{\isa{auto}}, \mbox{\isa{force}}, \mbox{\isa{clarsimp}}, \mbox{\isa{fastsimp}}, \mbox{\isa{slowsimp}}, and \mbox{\isa{bestsimp}}] provide |
1416 \item [\hyperlink{method.auto}{\mbox{\isa{auto}}}, \hyperlink{method.force}{\mbox{\isa{force}}}, \hyperlink{method.clarsimp}{\mbox{\isa{clarsimp}}}, \hyperlink{method.fastsimp}{\mbox{\isa{fastsimp}}}, \hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}, and \hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}}] provide |
1417 access to Isabelle's combined simplification and classical reasoning |
1417 access to Isabelle's combined simplification and classical reasoning |
1418 tactics. These correspond to \verb|auto_tac|, \verb|force_tac|, \verb|clarsimp_tac|, and Classical Reasoner tactics with the Simplifier |
1418 tactics. These correspond to \verb|auto_tac|, \verb|force_tac|, \verb|clarsimp_tac|, and Classical Reasoner tactics with the Simplifier |
1419 added as wrapper, see \cite[\S11]{isabelle-ref} for more |
1419 added as wrapper, see \cite[\S11]{isabelle-ref} for more |
1420 information. The modifier arguments correspond to those given in |
1420 information. The modifier arguments correspond to those given in |
1421 \secref{sec:simplifier} and \secref{sec:classical}. Just note that |
1421 \secref{sec:simplifier} and \secref{sec:classical}. Just note that |
1434 } |
1434 } |
1435 \isamarkuptrue% |
1435 \isamarkuptrue% |
1436 % |
1436 % |
1437 \begin{isamarkuptext}% |
1437 \begin{isamarkuptext}% |
1438 \begin{matharray}{rcl} |
1438 \begin{matharray}{rcl} |
1439 \indexdef{}{command}{print\_claset}\mbox{\isa{\isacommand{print{\isacharunderscore}claset}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
1439 \indexdef{}{command}{print\_claset}\hypertarget{command.print_claset}{\hyperlink{command.print_claset}{\mbox{\isa{\isacommand{print{\isacharunderscore}claset}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
1440 \indexdef{}{attribute}{intro}\mbox{\isa{intro}} & : & \isaratt \\ |
1440 \indexdef{}{attribute}{intro}\hypertarget{attribute.intro}{\hyperlink{attribute.intro}{\mbox{\isa{intro}}}} & : & \isaratt \\ |
1441 \indexdef{}{attribute}{elim}\mbox{\isa{elim}} & : & \isaratt \\ |
1441 \indexdef{}{attribute}{elim}\hypertarget{attribute.elim}{\hyperlink{attribute.elim}{\mbox{\isa{elim}}}} & : & \isaratt \\ |
1442 \indexdef{}{attribute}{dest}\mbox{\isa{dest}} & : & \isaratt \\ |
1442 \indexdef{}{attribute}{dest}\hypertarget{attribute.dest}{\hyperlink{attribute.dest}{\mbox{\isa{dest}}}} & : & \isaratt \\ |
1443 \indexdef{}{attribute}{rule}\mbox{\isa{rule}} & : & \isaratt \\ |
1443 \indexdef{}{attribute}{rule}\hypertarget{attribute.rule}{\hyperlink{attribute.rule}{\mbox{\isa{rule}}}} & : & \isaratt \\ |
1444 \indexdef{}{attribute}{iff}\mbox{\isa{iff}} & : & \isaratt \\ |
1444 \indexdef{}{attribute}{iff}\hypertarget{attribute.iff}{\hyperlink{attribute.iff}{\mbox{\isa{iff}}}} & : & \isaratt \\ |
1445 \end{matharray} |
1445 \end{matharray} |
1446 |
1446 |
1447 \begin{rail} |
1447 \begin{rail} |
1448 ('intro' | 'elim' | 'dest') ('!' | () | '?') nat? |
1448 ('intro' | 'elim' | 'dest') ('!' | () | '?') nat? |
1449 ; |
1449 ; |
1453 ; |
1453 ; |
1454 \end{rail} |
1454 \end{rail} |
1455 |
1455 |
1456 \begin{descr} |
1456 \begin{descr} |
1457 |
1457 |
1458 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}claset}}}] prints the collection of rules |
1458 \item [\hyperlink{command.print_claset}{\mbox{\isa{\isacommand{print{\isacharunderscore}claset}}}}] prints the collection of rules |
1459 declared to the Classical Reasoner, which is also known as |
1459 declared to the Classical Reasoner, which is also known as |
1460 ``claset'' internally \cite{isabelle-ref}. |
1460 ``claset'' internally \cite{isabelle-ref}. |
1461 |
1461 |
1462 \item [\mbox{\isa{intro}}, \mbox{\isa{elim}}, and \mbox{\isa{dest}}] |
1462 \item [\hyperlink{attribute.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.elim}{\mbox{\isa{elim}}}, and \hyperlink{attribute.dest}{\mbox{\isa{dest}}}] |
1463 declare introduction, elimination, and destruction rules, |
1463 declare introduction, elimination, and destruction rules, |
1464 respectively. By default, rules are considered as \emph{unsafe} |
1464 respectively. By default, rules are considered as \emph{unsafe} |
1465 (i.e.\ not applied blindly without backtracking), while ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' classifies as \emph{safe}. Rule declarations marked by |
1465 (i.e.\ not applied blindly without backtracking), while ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' classifies as \emph{safe}. Rule declarations marked by |
1466 ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' coincide with those of Isabelle/Pure, cf.\ |
1466 ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' coincide with those of Isabelle/Pure, cf.\ |
1467 \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps |
1467 \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps |
1468 of the \mbox{\isa{rule}} method). The optional natural number |
1468 of the \hyperlink{method.rule}{\mbox{\isa{rule}}} method). The optional natural number |
1469 specifies an explicit weight argument, which is ignored by automated |
1469 specifies an explicit weight argument, which is ignored by automated |
1470 tools, but determines the search order of single rule steps. |
1470 tools, but determines the search order of single rule steps. |
1471 |
1471 |
1472 \item [\mbox{\isa{rule}}~\isa{del}] deletes introduction, |
1472 \item [\hyperlink{attribute.rule}{\mbox{\isa{rule}}}~\isa{del}] deletes introduction, |
1473 elimination, or destruction rules from the context. |
1473 elimination, or destruction rules from the context. |
1474 |
1474 |
1475 \item [\mbox{\isa{iff}}] declares logical equivalences to the |
1475 \item [\hyperlink{attribute.iff}{\mbox{\isa{iff}}}] declares logical equivalences to the |
1476 Simplifier and the Classical reasoner at the same time. |
1476 Simplifier and the Classical reasoner at the same time. |
1477 Non-conditional rules result in a ``safe'' introduction and |
1477 Non-conditional rules result in a ``safe'' introduction and |
1478 elimination pair; conditional ones are considered ``unsafe''. Rules |
1478 elimination pair; conditional ones are considered ``unsafe''. Rules |
1479 with negative conclusion are automatically inverted (using \isa{{\isachardoublequote}{\isasymnot}{\isachardoublequote}}-elimination internally). |
1479 with negative conclusion are automatically inverted (using \isa{{\isachardoublequote}{\isasymnot}{\isachardoublequote}}-elimination internally). |
1480 |
1480 |
1481 The ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' version of \mbox{\isa{iff}} declares rules to |
1481 The ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' version of \hyperlink{attribute.iff}{\mbox{\isa{iff}}} declares rules to |
1482 the Isabelle/Pure context only, and omits the Simplifier |
1482 the Isabelle/Pure context only, and omits the Simplifier |
1483 declaration. |
1483 declaration. |
1484 |
1484 |
1485 \end{descr}% |
1485 \end{descr}% |
1486 \end{isamarkuptext}% |
1486 \end{isamarkuptext}% |
1512 } |
1512 } |
1513 \isamarkuptrue% |
1513 \isamarkuptrue% |
1514 % |
1514 % |
1515 \begin{isamarkuptext}% |
1515 \begin{isamarkuptext}% |
1516 \begin{matharray}{rcl} |
1516 \begin{matharray}{rcl} |
1517 \indexdef{}{command}{case}\mbox{\isa{\isacommand{case}}} & : & \isartrans{proof(state)}{proof(state)} \\ |
1517 \indexdef{}{command}{case}\hypertarget{command.case}{\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}} & : & \isartrans{proof(state)}{proof(state)} \\ |
1518 \indexdef{}{command}{print\_cases}\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\ |
1518 \indexdef{}{command}{print\_cases}\hypertarget{command.print_cases}{\hyperlink{command.print_cases}{\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\ |
1519 \indexdef{}{attribute}{case\_names}\mbox{\isa{case{\isacharunderscore}names}} & : & \isaratt \\ |
1519 \indexdef{}{attribute}{case\_names}\hypertarget{attribute.case_names}{\hyperlink{attribute.case_names}{\mbox{\isa{case{\isacharunderscore}names}}}} & : & \isaratt \\ |
1520 \indexdef{}{attribute}{case\_conclusion}\mbox{\isa{case{\isacharunderscore}conclusion}} & : & \isaratt \\ |
1520 \indexdef{}{attribute}{case\_conclusion}\hypertarget{attribute.case_conclusion}{\hyperlink{attribute.case_conclusion}{\mbox{\isa{case{\isacharunderscore}conclusion}}}} & : & \isaratt \\ |
1521 \indexdef{}{attribute}{params}\mbox{\isa{params}} & : & \isaratt \\ |
1521 \indexdef{}{attribute}{params}\hypertarget{attribute.params}{\hyperlink{attribute.params}{\mbox{\isa{params}}}} & : & \isaratt \\ |
1522 \indexdef{}{attribute}{consumes}\mbox{\isa{consumes}} & : & \isaratt \\ |
1522 \indexdef{}{attribute}{consumes}\hypertarget{attribute.consumes}{\hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}} & : & \isaratt \\ |
1523 \end{matharray} |
1523 \end{matharray} |
1524 |
1524 |
1525 The puristic way to build up Isar proof contexts is by explicit |
1525 The puristic way to build up Isar proof contexts is by explicit |
1526 language elements like \mbox{\isa{\isacommand{fix}}}, \mbox{\isa{\isacommand{assume}}}, |
1526 language elements like \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}, \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}, |
1527 \mbox{\isa{\isacommand{let}}} (see \secref{sec:proof-context}). This is adequate |
1527 \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}} (see \secref{sec:proof-context}). This is adequate |
1528 for plain natural deduction, but easily becomes unwieldy in concrete |
1528 for plain natural deduction, but easily becomes unwieldy in concrete |
1529 verification tasks, which typically involve big induction rules with |
1529 verification tasks, which typically involve big induction rules with |
1530 several cases. |
1530 several cases. |
1531 |
1531 |
1532 The \mbox{\isa{\isacommand{case}}} command provides a shorthand to refer to a |
1532 The \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}} command provides a shorthand to refer to a |
1533 local context symbolically: certain proof methods provide an |
1533 local context symbolically: certain proof methods provide an |
1534 environment of named ``cases'' of the form \isa{{\isachardoublequote}c{\isacharcolon}\ x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isacharcomma}\ {\isasymphi}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}; the effect of ``\mbox{\isa{\isacommand{case}}}~\isa{c}'' is then equivalent to ``\mbox{\isa{\isacommand{fix}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}~\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}c{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}''. Term bindings may be covered as well, notably |
1534 environment of named ``cases'' of the form \isa{{\isachardoublequote}c{\isacharcolon}\ x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isacharcomma}\ {\isasymphi}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}; the effect of ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{c}'' is then equivalent to ``\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}~\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}c{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}''. Term bindings may be covered as well, notably |
1535 \mbox{\isa{{\isacharquery}case}} for the main conclusion. |
1535 \hyperlink{variable.?case}{\mbox{\isa{{\isacharquery}case}}} for the main conclusion. |
1536 |
1536 |
1537 By default, the ``terminology'' \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isachardoublequote}} of |
1537 By default, the ``terminology'' \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isachardoublequote}} of |
1538 a case value is marked as hidden, i.e.\ there is no way to refer to |
1538 a case value is marked as hidden, i.e.\ there is no way to refer to |
1539 such parameters in the subsequent proof text. After all, original |
1539 such parameters in the subsequent proof text. After all, original |
1540 rule parameters stem from somewhere outside of the current proof |
1540 rule parameters stem from somewhere outside of the current proof |
1541 text. By using the explicit form ``\mbox{\isa{\isacommand{case}}}~\isa{{\isachardoublequote}{\isacharparenleft}c\ y\isactrlsub {\isadigit{1}}\ {\isasymdots}\ y\isactrlsub m{\isacharparenright}{\isachardoublequote}}'' instead, the proof author is able to |
1541 text. By using the explicit form ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{{\isachardoublequote}{\isacharparenleft}c\ y\isactrlsub {\isadigit{1}}\ {\isasymdots}\ y\isactrlsub m{\isacharparenright}{\isachardoublequote}}'' instead, the proof author is able to |
1542 chose local names that fit nicely into the current context. |
1542 chose local names that fit nicely into the current context. |
1543 |
1543 |
1544 \medskip It is important to note that proper use of \mbox{\isa{\isacommand{case}}} does not provide means to peek at the current goal state, |
1544 \medskip It is important to note that proper use of \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}} does not provide means to peek at the current goal state, |
1545 which is not directly observable in Isar! Nonetheless, goal |
1545 which is not directly observable in Isar! Nonetheless, goal |
1546 refinement commands do provide named cases \isa{{\isachardoublequote}goal\isactrlsub i{\isachardoublequote}} |
1546 refinement commands do provide named cases \isa{{\isachardoublequote}goal\isactrlsub i{\isachardoublequote}} |
1547 for each subgoal \isa{{\isachardoublequote}i\ {\isacharequal}\ {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n{\isachardoublequote}} of the resulting goal state. |
1547 for each subgoal \isa{{\isachardoublequote}i\ {\isacharequal}\ {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n{\isachardoublequote}} of the resulting goal state. |
1548 Using this extra feature requires great care, because some bits of |
1548 Using this extra feature requires great care, because some bits of |
1549 the internal tactical machinery intrude the proof text. In |
1549 the internal tactical machinery intrude the proof text. In |
1551 reasoning tools are usually quite unpredictable. |
1551 reasoning tools are usually quite unpredictable. |
1552 |
1552 |
1553 Under normal circumstances, the text of cases emerge from standard |
1553 Under normal circumstances, the text of cases emerge from standard |
1554 elimination or induction rules, which in turn are derived from |
1554 elimination or induction rules, which in turn are derived from |
1555 previous theory specifications in a canonical way (say from |
1555 previous theory specifications in a canonical way (say from |
1556 \mbox{\isa{\isacommand{inductive}}} definitions). |
1556 \hyperlink{command.inductive}{\mbox{\isa{\isacommand{inductive}}}} definitions). |
1557 |
1557 |
1558 \medskip Proper cases are only available if both the proof method |
1558 \medskip Proper cases are only available if both the proof method |
1559 and the rules involved support this. By using appropriate |
1559 and the rules involved support this. By using appropriate |
1560 attributes, case names, conclusions, and parameters may be also |
1560 attributes, case names, conclusions, and parameters may be also |
1561 declared by hand. Thus variant versions of rules that have been |
1561 declared by hand. Thus variant versions of rules that have been |
1578 ; |
1578 ; |
1579 \end{rail} |
1579 \end{rail} |
1580 |
1580 |
1581 \begin{descr} |
1581 \begin{descr} |
1582 |
1582 |
1583 \item [\mbox{\isa{\isacommand{case}}}~\isa{{\isachardoublequote}{\isacharparenleft}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isacharparenright}{\isachardoublequote}}] |
1583 \item [\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{{\isachardoublequote}{\isacharparenleft}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isacharparenright}{\isachardoublequote}}] |
1584 invokes a named local context \isa{{\isachardoublequote}c{\isacharcolon}\ x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isacharcomma}\ {\isasymphi}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymphi}\isactrlsub m{\isachardoublequote}}, as provided by an appropriate |
1584 invokes a named local context \isa{{\isachardoublequote}c{\isacharcolon}\ x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isacharcomma}\ {\isasymphi}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymphi}\isactrlsub m{\isachardoublequote}}, as provided by an appropriate |
1585 proof method (such as \indexref{}{method}{cases}\mbox{\isa{cases}} and \indexref{}{method}{induct}\mbox{\isa{induct}}). |
1585 proof method (such as \indexref{}{method}{cases}\hyperlink{method.cases}{\mbox{\isa{cases}}} and \indexref{}{method}{induct}\hyperlink{method.induct}{\mbox{\isa{induct}}}). |
1586 The command ``\mbox{\isa{\isacommand{case}}}~\isa{{\isachardoublequote}{\isacharparenleft}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isacharparenright}{\isachardoublequote}}'' abbreviates ``\mbox{\isa{\isacommand{fix}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}~\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}c{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}''. |
1586 The command ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{{\isachardoublequote}{\isacharparenleft}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isacharparenright}{\isachardoublequote}}'' abbreviates ``\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}~\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}c{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}''. |
1587 |
1587 |
1588 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}] prints all local contexts of the |
1588 \item [\hyperlink{command.print_cases}{\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}}] prints all local contexts of the |
1589 current state, using Isar proof language notation. |
1589 current state, using Isar proof language notation. |
1590 |
1590 |
1591 \item [\mbox{\isa{case{\isacharunderscore}names}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub k{\isachardoublequote}}] |
1591 \item [\hyperlink{attribute.case_names}{\mbox{\isa{case{\isacharunderscore}names}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub k{\isachardoublequote}}] |
1592 declares names for the local contexts of premises of a theorem; |
1592 declares names for the local contexts of premises of a theorem; |
1593 \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub k{\isachardoublequote}} refers to the \emph{suffix} of the |
1593 \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub k{\isachardoublequote}} refers to the \emph{suffix} of the |
1594 list of premises. |
1594 list of premises. |
1595 |
1595 |
1596 \item [\mbox{\isa{case{\isacharunderscore}conclusion}}~\isa{{\isachardoublequote}c\ d\isactrlsub {\isadigit{1}}\ {\isasymdots}\ d\isactrlsub k{\isachardoublequote}}] declares names for the conclusions of a named premise |
1596 \item [\hyperlink{attribute.case_conclusion}{\mbox{\isa{case{\isacharunderscore}conclusion}}}~\isa{{\isachardoublequote}c\ d\isactrlsub {\isadigit{1}}\ {\isasymdots}\ d\isactrlsub k{\isachardoublequote}}] declares names for the conclusions of a named premise |
1597 \isa{c}; here \isa{{\isachardoublequote}d\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ d\isactrlsub k{\isachardoublequote}} refers to the |
1597 \isa{c}; here \isa{{\isachardoublequote}d\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ d\isactrlsub k{\isachardoublequote}} refers to the |
1598 prefix of arguments of a logical formula built by nesting a binary |
1598 prefix of arguments of a logical formula built by nesting a binary |
1599 connective (e.g.\ \isa{{\isachardoublequote}{\isasymor}{\isachardoublequote}}). |
1599 connective (e.g.\ \isa{{\isachardoublequote}{\isasymor}{\isachardoublequote}}). |
1600 |
1600 |
1601 Note that proof methods such as \mbox{\isa{induct}} and \mbox{\isa{coinduct}} already provide a default name for the conclusion as a |
1601 Note that proof methods such as \hyperlink{method.induct}{\mbox{\isa{induct}}} and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} already provide a default name for the conclusion as a |
1602 whole. The need to name subformulas only arises with cases that |
1602 whole. The need to name subformulas only arises with cases that |
1603 split into several sub-cases, as in common co-induction rules. |
1603 split into several sub-cases, as in common co-induction rules. |
1604 |
1604 |
1605 \item [\mbox{\isa{params}}~\isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub m\ {\isasymAND}\ {\isasymdots}\ q\isactrlsub {\isadigit{1}}\ {\isasymdots}\ q\isactrlsub n{\isachardoublequote}}] renames the innermost parameters of |
1605 \item [\hyperlink{attribute.params}{\mbox{\isa{params}}}~\isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub m\ {\isasymAND}\ {\isasymdots}\ q\isactrlsub {\isadigit{1}}\ {\isasymdots}\ q\isactrlsub n{\isachardoublequote}}] renames the innermost parameters of |
1606 premises \isa{{\isachardoublequote}{\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n{\isachardoublequote}} of some theorem. An empty list of names |
1606 premises \isa{{\isachardoublequote}{\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n{\isachardoublequote}} of some theorem. An empty list of names |
1607 may be given to skip positions, leaving the present parameters |
1607 may be given to skip positions, leaving the present parameters |
1608 unchanged. |
1608 unchanged. |
1609 |
1609 |
1610 Note that the default usage of case rules does \emph{not} directly |
1610 Note that the default usage of case rules does \emph{not} directly |
1611 expose parameters to the proof context. |
1611 expose parameters to the proof context. |
1612 |
1612 |
1613 \item [\mbox{\isa{consumes}}~\isa{n}] declares the number of |
1613 \item [\hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{n}] declares the number of |
1614 ``major premises'' of a rule, i.e.\ the number of facts to be |
1614 ``major premises'' of a rule, i.e.\ the number of facts to be |
1615 consumed when it is applied by an appropriate proof method. The |
1615 consumed when it is applied by an appropriate proof method. The |
1616 default value of \mbox{\isa{consumes}} is \isa{{\isachardoublequote}n\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}}, which is |
1616 default value of \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}} is \isa{{\isachardoublequote}n\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}}, which is |
1617 appropriate for the usual kind of cases and induction rules for |
1617 appropriate for the usual kind of cases and induction rules for |
1618 inductive sets (cf.\ \secref{sec:hol-inductive}). Rules without any |
1618 inductive sets (cf.\ \secref{sec:hol-inductive}). Rules without any |
1619 \mbox{\isa{consumes}} declaration given are treated as if |
1619 \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}} declaration given are treated as if |
1620 \mbox{\isa{consumes}}~\isa{{\isadigit{0}}} had been specified. |
1620 \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{{\isadigit{0}}} had been specified. |
1621 |
1621 |
1622 Note that explicit \mbox{\isa{consumes}} declarations are only |
1622 Note that explicit \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}} declarations are only |
1623 rarely needed; this is already taken care of automatically by the |
1623 rarely needed; this is already taken care of automatically by the |
1624 higher-level \mbox{\isa{cases}}, \mbox{\isa{induct}}, and |
1624 higher-level \hyperlink{attribute.cases}{\mbox{\isa{cases}}}, \hyperlink{attribute.induct}{\mbox{\isa{induct}}}, and |
1625 \mbox{\isa{coinduct}} declarations. |
1625 \hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}} declarations. |
1626 |
1626 |
1627 \end{descr}% |
1627 \end{descr}% |
1628 \end{isamarkuptext}% |
1628 \end{isamarkuptext}% |
1629 \isamarkuptrue% |
1629 \isamarkuptrue% |
1630 % |
1630 % |
1632 } |
1632 } |
1633 \isamarkuptrue% |
1633 \isamarkuptrue% |
1634 % |
1634 % |
1635 \begin{isamarkuptext}% |
1635 \begin{isamarkuptext}% |
1636 \begin{matharray}{rcl} |
1636 \begin{matharray}{rcl} |
1637 \indexdef{}{method}{cases}\mbox{\isa{cases}} & : & \isarmeth \\ |
1637 \indexdef{}{method}{cases}\hypertarget{method.cases}{\hyperlink{method.cases}{\mbox{\isa{cases}}}} & : & \isarmeth \\ |
1638 \indexdef{}{method}{induct}\mbox{\isa{induct}} & : & \isarmeth \\ |
1638 \indexdef{}{method}{induct}\hypertarget{method.induct}{\hyperlink{method.induct}{\mbox{\isa{induct}}}} & : & \isarmeth \\ |
1639 \indexdef{}{method}{coinduct}\mbox{\isa{coinduct}} & : & \isarmeth \\ |
1639 \indexdef{}{method}{coinduct}\hypertarget{method.coinduct}{\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}} & : & \isarmeth \\ |
1640 \end{matharray} |
1640 \end{matharray} |
1641 |
1641 |
1642 The \mbox{\isa{cases}}, \mbox{\isa{induct}}, and \mbox{\isa{coinduct}} |
1642 The \hyperlink{method.cases}{\mbox{\isa{cases}}}, \hyperlink{method.induct}{\mbox{\isa{induct}}}, and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} |
1643 methods provide a uniform interface to common proof techniques over |
1643 methods provide a uniform interface to common proof techniques over |
1644 datatypes, inductive predicates (or sets), recursive functions etc. |
1644 datatypes, inductive predicates (or sets), recursive functions etc. |
1645 The corresponding rules may be specified and instantiated in a |
1645 The corresponding rules may be specified and instantiated in a |
1646 casual manner. Furthermore, these methods provide named local |
1646 casual manner. Furthermore, these methods provide named local |
1647 contexts that may be invoked via the \mbox{\isa{\isacommand{case}}} proof command |
1647 contexts that may be invoked via the \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}} proof command |
1648 within the subsequent proof text. This accommodates compact proof |
1648 within the subsequent proof text. This accommodates compact proof |
1649 texts even when reasoning about large specifications. |
1649 texts even when reasoning about large specifications. |
1650 |
1650 |
1651 The \mbox{\isa{induct}} method also provides some additional |
1651 The \hyperlink{method.induct}{\mbox{\isa{induct}}} method also provides some additional |
1652 infrastructure in order to be applicable to structure statements |
1652 infrastructure in order to be applicable to structure statements |
1653 (either using explicit meta-level connectives, or including facts |
1653 (either using explicit meta-level connectives, or including facts |
1654 and parameters separately). This avoids cumbersome encoding of |
1654 and parameters separately). This avoids cumbersome encoding of |
1655 ``strengthened'' inductive statements within the object-logic. |
1655 ``strengthened'' inductive statements within the object-logic. |
1656 |
1656 |
1674 ; |
1674 ; |
1675 \end{rail} |
1675 \end{rail} |
1676 |
1676 |
1677 \begin{descr} |
1677 \begin{descr} |
1678 |
1678 |
1679 \item [\mbox{\isa{cases}}~\isa{{\isachardoublequote}insts\ R{\isachardoublequote}}] applies method \mbox{\isa{rule}} with an appropriate case distinction theorem, instantiated to |
1679 \item [\hyperlink{method.cases}{\mbox{\isa{cases}}}~\isa{{\isachardoublequote}insts\ R{\isachardoublequote}}] applies method \hyperlink{method.rule}{\mbox{\isa{rule}}} with an appropriate case distinction theorem, instantiated to |
1680 the subjects \isa{insts}. Symbolic case names are bound according |
1680 the subjects \isa{insts}. Symbolic case names are bound according |
1681 to the rule's local contexts. |
1681 to the rule's local contexts. |
1682 |
1682 |
1683 The rule is determined as follows, according to the facts and |
1683 The rule is determined as follows, according to the facts and |
1684 arguments passed to the \mbox{\isa{cases}} method: |
1684 arguments passed to the \hyperlink{method.cases}{\mbox{\isa{cases}}} method: |
1685 |
1685 |
1686 \medskip |
1686 \medskip |
1687 \begin{tabular}{llll} |
1687 \begin{tabular}{llll} |
1688 facts & & arguments & rule \\\hline |
1688 facts & & arguments & rule \\\hline |
1689 & \mbox{\isa{cases}} & & classical case split \\ |
1689 & \hyperlink{method.cases}{\mbox{\isa{cases}}} & & classical case split \\ |
1690 & \mbox{\isa{cases}} & \isa{t} & datatype exhaustion (type of \isa{t}) \\ |
1690 & \hyperlink{method.cases}{\mbox{\isa{cases}}} & \isa{t} & datatype exhaustion (type of \isa{t}) \\ |
1691 \isa{{\isachardoublequote}{\isasymturnstile}\ A\ t{\isachardoublequote}} & \mbox{\isa{cases}} & \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & inductive predicate/set elimination (of \isa{A}) \\ |
1691 \isa{{\isachardoublequote}{\isasymturnstile}\ A\ t{\isachardoublequote}} & \hyperlink{method.cases}{\mbox{\isa{cases}}} & \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & inductive predicate/set elimination (of \isa{A}) \\ |
1692 \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & \mbox{\isa{cases}} & \isa{{\isachardoublequote}{\isasymdots}\ rule{\isacharcolon}\ R{\isachardoublequote}} & explicit rule \isa{R} \\ |
1692 \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & \hyperlink{method.cases}{\mbox{\isa{cases}}} & \isa{{\isachardoublequote}{\isasymdots}\ rule{\isacharcolon}\ R{\isachardoublequote}} & explicit rule \isa{R} \\ |
1693 \end{tabular} |
1693 \end{tabular} |
1694 \medskip |
1694 \medskip |
1695 |
1695 |
1696 Several instantiations may be given, referring to the \emph{suffix} |
1696 Several instantiations may be given, referring to the \emph{suffix} |
1697 of premises of the case rule; within each premise, the \emph{prefix} |
1697 of premises of the case rule; within each premise, the \emph{prefix} |
1698 of variables is instantiated. In most situations, only a single |
1698 of variables is instantiated. In most situations, only a single |
1699 term needs to be specified; this refers to the first variable of the |
1699 term needs to be specified; this refers to the first variable of the |
1700 last premise (it is usually the same for all cases). |
1700 last premise (it is usually the same for all cases). |
1701 |
1701 |
1702 \item [\mbox{\isa{induct}}~\isa{{\isachardoublequote}insts\ R{\isachardoublequote}}] is analogous to the |
1702 \item [\hyperlink{method.induct}{\mbox{\isa{induct}}}~\isa{{\isachardoublequote}insts\ R{\isachardoublequote}}] is analogous to the |
1703 \mbox{\isa{cases}} method, but refers to induction rules, which are |
1703 \hyperlink{method.cases}{\mbox{\isa{cases}}} method, but refers to induction rules, which are |
1704 determined as follows: |
1704 determined as follows: |
1705 |
1705 |
1706 \medskip |
1706 \medskip |
1707 \begin{tabular}{llll} |
1707 \begin{tabular}{llll} |
1708 facts & & arguments & rule \\\hline |
1708 facts & & arguments & rule \\\hline |
1709 & \mbox{\isa{induct}} & \isa{{\isachardoublequote}P\ x{\isachardoublequote}} & datatype induction (type of \isa{x}) \\ |
1709 & \hyperlink{method.induct}{\mbox{\isa{induct}}} & \isa{{\isachardoublequote}P\ x{\isachardoublequote}} & datatype induction (type of \isa{x}) \\ |
1710 \isa{{\isachardoublequote}{\isasymturnstile}\ A\ x{\isachardoublequote}} & \mbox{\isa{induct}} & \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & predicate/set induction (of \isa{A}) \\ |
1710 \isa{{\isachardoublequote}{\isasymturnstile}\ A\ x{\isachardoublequote}} & \hyperlink{method.induct}{\mbox{\isa{induct}}} & \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & predicate/set induction (of \isa{A}) \\ |
1711 \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & \mbox{\isa{induct}} & \isa{{\isachardoublequote}{\isasymdots}\ rule{\isacharcolon}\ R{\isachardoublequote}} & explicit rule \isa{R} \\ |
1711 \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & \hyperlink{method.induct}{\mbox{\isa{induct}}} & \isa{{\isachardoublequote}{\isasymdots}\ rule{\isacharcolon}\ R{\isachardoublequote}} & explicit rule \isa{R} \\ |
1712 \end{tabular} |
1712 \end{tabular} |
1713 \medskip |
1713 \medskip |
1714 |
1714 |
1715 Several instantiations may be given, each referring to some part of |
1715 Several instantiations may be given, each referring to some part of |
1716 a mutual inductive definition or datatype --- only related partial |
1716 a mutual inductive definition or datatype --- only related partial |
1738 The optional ``\isa{{\isachardoublequote}taking{\isacharcolon}\ t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n{\isachardoublequote}}'' |
1738 The optional ``\isa{{\isachardoublequote}taking{\isacharcolon}\ t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n{\isachardoublequote}}'' |
1739 specification provides additional instantiations of a prefix of |
1739 specification provides additional instantiations of a prefix of |
1740 pending variables in the rule. Such schematic induction rules |
1740 pending variables in the rule. Such schematic induction rules |
1741 rarely occur in practice, though. |
1741 rarely occur in practice, though. |
1742 |
1742 |
1743 \item [\mbox{\isa{coinduct}}~\isa{{\isachardoublequote}inst\ R{\isachardoublequote}}] is analogous to the |
1743 \item [\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}~\isa{{\isachardoublequote}inst\ R{\isachardoublequote}}] is analogous to the |
1744 \mbox{\isa{induct}} method, but refers to coinduction rules, which are |
1744 \hyperlink{method.induct}{\mbox{\isa{induct}}} method, but refers to coinduction rules, which are |
1745 determined as follows: |
1745 determined as follows: |
1746 |
1746 |
1747 \medskip |
1747 \medskip |
1748 \begin{tabular}{llll} |
1748 \begin{tabular}{llll} |
1749 goal & & arguments & rule \\\hline |
1749 goal & & arguments & rule \\\hline |
1750 & \mbox{\isa{coinduct}} & \isa{x} & type coinduction (type of \isa{x}) \\ |
1750 & \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} & \isa{x} & type coinduction (type of \isa{x}) \\ |
1751 \isa{{\isachardoublequote}A\ x{\isachardoublequote}} & \mbox{\isa{coinduct}} & \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & predicate/set coinduction (of \isa{A}) \\ |
1751 \isa{{\isachardoublequote}A\ x{\isachardoublequote}} & \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} & \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & predicate/set coinduction (of \isa{A}) \\ |
1752 \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & \mbox{\isa{coinduct}} & \isa{{\isachardoublequote}{\isasymdots}\ rule{\isacharcolon}\ R{\isachardoublequote}} & explicit rule \isa{R} \\ |
1752 \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} & \isa{{\isachardoublequote}{\isasymdots}\ rule{\isacharcolon}\ R{\isachardoublequote}} & explicit rule \isa{R} \\ |
1753 \end{tabular} |
1753 \end{tabular} |
1754 |
1754 |
1755 Coinduction is the dual of induction. Induction essentially |
1755 Coinduction is the dual of induction. Induction essentially |
1756 eliminates \isa{{\isachardoublequote}A\ x{\isachardoublequote}} towards a generic result \isa{{\isachardoublequote}P\ x{\isachardoublequote}}, |
1756 eliminates \isa{{\isachardoublequote}A\ x{\isachardoublequote}} towards a generic result \isa{{\isachardoublequote}P\ x{\isachardoublequote}}, |
1757 while coinduction introduces \isa{{\isachardoublequote}A\ x{\isachardoublequote}} starting with \isa{{\isachardoublequote}B\ x{\isachardoublequote}}, for a suitable ``bisimulation'' \isa{B}. The cases of a |
1757 while coinduction introduces \isa{{\isachardoublequote}A\ x{\isachardoublequote}} starting with \isa{{\isachardoublequote}B\ x{\isachardoublequote}}, for a suitable ``bisimulation'' \isa{B}. The cases of a |
1766 to be used in the coinduction step. |
1766 to be used in the coinduction step. |
1767 |
1767 |
1768 \end{descr} |
1768 \end{descr} |
1769 |
1769 |
1770 Above methods produce named local contexts, as determined by the |
1770 Above methods produce named local contexts, as determined by the |
1771 instantiated rule as given in the text. Beyond that, the \mbox{\isa{induct}} and \mbox{\isa{coinduct}} methods guess further instantiations |
1771 instantiated rule as given in the text. Beyond that, the \hyperlink{method.induct}{\mbox{\isa{induct}}} and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} methods guess further instantiations |
1772 from the goal specification itself. Any persisting unresolved |
1772 from the goal specification itself. Any persisting unresolved |
1773 schematic variables of the resulting rule will render the the |
1773 schematic variables of the resulting rule will render the the |
1774 corresponding case invalid. The term binding \mbox{\isa{{\isacharquery}case}} for |
1774 corresponding case invalid. The term binding \hyperlink{variable.?case}{\mbox{\isa{{\isacharquery}case}}} for |
1775 the conclusion will be provided with each case, provided that term |
1775 the conclusion will be provided with each case, provided that term |
1776 is fully specified. |
1776 is fully specified. |
1777 |
1777 |
1778 The \mbox{\isa{\isacommand{print{\isacharunderscore}cases}}} command prints all named cases present |
1778 The \hyperlink{command.print_cases}{\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}} command prints all named cases present |
1779 in the current proof state. |
1779 in the current proof state. |
1780 |
1780 |
1781 \medskip Despite the additional infrastructure, both \mbox{\isa{cases}} |
1781 \medskip Despite the additional infrastructure, both \hyperlink{method.cases}{\mbox{\isa{cases}}} |
1782 and \mbox{\isa{coinduct}} merely apply a certain rule, after |
1782 and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} merely apply a certain rule, after |
1783 instantiation, while conforming due to the usual way of monotonic |
1783 instantiation, while conforming due to the usual way of monotonic |
1784 natural deduction: the context of a structured statement \isa{{\isachardoublequote}{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ {\isasymdots}{\isachardoublequote}} |
1784 natural deduction: the context of a structured statement \isa{{\isachardoublequote}{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ {\isasymdots}{\isachardoublequote}} |
1785 reappears unchanged after the case split. |
1785 reappears unchanged after the case split. |
1786 |
1786 |
1787 The \mbox{\isa{induct}} method is fundamentally different in this |
1787 The \hyperlink{method.induct}{\mbox{\isa{induct}}} method is fundamentally different in this |
1788 respect: the meta-level structure is passed through the |
1788 respect: the meta-level structure is passed through the |
1789 ``recursive'' course involved in the induction. Thus the original |
1789 ``recursive'' course involved in the induction. Thus the original |
1790 statement is basically replaced by separate copies, corresponding to |
1790 statement is basically replaced by separate copies, corresponding to |
1791 the induction hypotheses and conclusion; the original goal context |
1791 the induction hypotheses and conclusion; the original goal context |
1792 is no longer available. Thus local assumptions, fixed parameters |
1792 is no longer available. Thus local assumptions, fixed parameters |
1794 of the original statement. |
1794 of the original statement. |
1795 |
1795 |
1796 In induction proofs, local assumptions introduced by cases are split |
1796 In induction proofs, local assumptions introduced by cases are split |
1797 into two different kinds: \isa{hyps} stemming from the rule and |
1797 into two different kinds: \isa{hyps} stemming from the rule and |
1798 \isa{prems} from the goal statement. This is reflected in the |
1798 \isa{prems} from the goal statement. This is reflected in the |
1799 extracted cases accordingly, so invoking ``\mbox{\isa{\isacommand{case}}}~\isa{c}'' will provide separate facts \isa{c{\isachardot}hyps} and \isa{c{\isachardot}prems}, |
1799 extracted cases accordingly, so invoking ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{c}'' will provide separate facts \isa{c{\isachardot}hyps} and \isa{c{\isachardot}prems}, |
1800 as well as fact \isa{c} to hold the all-inclusive list. |
1800 as well as fact \isa{c} to hold the all-inclusive list. |
1801 |
1801 |
1802 \medskip Facts presented to either method are consumed according to |
1802 \medskip Facts presented to either method are consumed according to |
1803 the number of ``major premises'' of the rule involved, which is |
1803 the number of ``major premises'' of the rule involved, which is |
1804 usually 0 for plain cases and induction rules of datatypes etc.\ and |
1804 usually 0 for plain cases and induction rules of datatypes etc.\ and |
1833 ; |
1833 ; |
1834 \end{rail} |
1834 \end{rail} |
1835 |
1835 |
1836 \begin{descr} |
1836 \begin{descr} |
1837 |
1837 |
1838 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}induct{\isacharunderscore}rules}}}] prints cases and induct |
1838 \item [\hyperlink{command.print_induct_rules}{\mbox{\isa{\isacommand{print{\isacharunderscore}induct{\isacharunderscore}rules}}}}] prints cases and induct |
1839 rules for predicates (or sets) and types of the current context. |
1839 rules for predicates (or sets) and types of the current context. |
1840 |
1840 |
1841 \item [\mbox{\isa{cases}}, \mbox{\isa{induct}}, and \mbox{\isa{coinduct}}] (as attributes) augment the corresponding context of |
1841 \item [\hyperlink{attribute.cases}{\mbox{\isa{cases}}}, \hyperlink{attribute.induct}{\mbox{\isa{induct}}}, and \hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}}] (as attributes) augment the corresponding context of |
1842 rules for reasoning about (co)inductive predicates (or sets) and |
1842 rules for reasoning about (co)inductive predicates (or sets) and |
1843 types, using the corresponding methods of the same name. Certain |
1843 types, using the corresponding methods of the same name. Certain |
1844 definitional packages of object-logics usually declare emerging |
1844 definitional packages of object-logics usually declare emerging |
1845 cases and induction rules as expected, so users rarely need to |
1845 cases and induction rules as expected, so users rarely need to |
1846 intervene. |
1846 intervene. |
1847 |
1847 |
1848 Manual rule declarations usually refer to the \mbox{\isa{case{\isacharunderscore}names}} and \mbox{\isa{params}} attributes to adjust names of |
1848 Manual rule declarations usually refer to the \hyperlink{attribute.case_names}{\mbox{\isa{case{\isacharunderscore}names}}} and \hyperlink{attribute.params}{\mbox{\isa{params}}} attributes to adjust names of |
1849 cases and parameters of a rule; the \mbox{\isa{consumes}} |
1849 cases and parameters of a rule; the \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}} |
1850 declaration is taken care of automatically: \mbox{\isa{consumes}}~\isa{{\isadigit{0}}} is specified for ``type'' rules and \mbox{\isa{consumes}}~\isa{{\isadigit{1}}} for ``predicate'' / ``set'' rules. |
1850 declaration is taken care of automatically: \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{{\isadigit{0}}} is specified for ``type'' rules and \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{{\isadigit{1}}} for ``predicate'' / ``set'' rules. |
1851 |
1851 |
1852 \end{descr}% |
1852 \end{descr}% |
1853 \end{isamarkuptext}% |
1853 \end{isamarkuptext}% |
1854 \isamarkuptrue% |
1854 \isamarkuptrue% |
1855 % |
1855 % |
1857 } |
1857 } |
1858 \isamarkuptrue% |
1858 \isamarkuptrue% |
1859 % |
1859 % |
1860 \begin{isamarkuptext}% |
1860 \begin{isamarkuptext}% |
1861 \begin{matharray}{rcl} |
1861 \begin{matharray}{rcl} |
1862 \indexdef{}{command}{judgment}\mbox{\isa{\isacommand{judgment}}} & : & \isartrans{theory}{theory} \\ |
1862 \indexdef{}{command}{judgment}\hypertarget{command.judgment}{\hyperlink{command.judgment}{\mbox{\isa{\isacommand{judgment}}}}} & : & \isartrans{theory}{theory} \\ |
1863 \indexdef{}{method}{atomize}\mbox{\isa{atomize}} & : & \isarmeth \\ |
1863 \indexdef{}{method}{atomize}\hypertarget{method.atomize}{\hyperlink{method.atomize}{\mbox{\isa{atomize}}}} & : & \isarmeth \\ |
1864 \indexdef{}{attribute}{atomize}\mbox{\isa{atomize}} & : & \isaratt \\ |
1864 \indexdef{}{attribute}{atomize}\hypertarget{attribute.atomize}{\hyperlink{attribute.atomize}{\mbox{\isa{atomize}}}} & : & \isaratt \\ |
1865 \indexdef{}{attribute}{rule\_format}\mbox{\isa{rule{\isacharunderscore}format}} & : & \isaratt \\ |
1865 \indexdef{}{attribute}{rule\_format}\hypertarget{attribute.rule_format}{\hyperlink{attribute.rule_format}{\mbox{\isa{rule{\isacharunderscore}format}}}} & : & \isaratt \\ |
1866 \indexdef{}{attribute}{rulify}\mbox{\isa{rulify}} & : & \isaratt \\ |
1866 \indexdef{}{attribute}{rulify}\hypertarget{attribute.rulify}{\hyperlink{attribute.rulify}{\mbox{\isa{rulify}}}} & : & \isaratt \\ |
1867 \end{matharray} |
1867 \end{matharray} |
1868 |
1868 |
1869 The very starting point for any Isabelle object-logic is a ``truth |
1869 The very starting point for any Isabelle object-logic is a ``truth |
1870 judgment'' that links object-level statements to the meta-logic |
1870 judgment'' that links object-level statements to the meta-logic |
1871 (with its minimal language of \isa{prop} that covers universal |
1871 (with its minimal language of \isa{prop} that covers universal |
1875 statements over \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}} and \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} within their own |
1875 statements over \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}} and \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} within their own |
1876 language. This is useful in certain situations where a rule needs |
1876 language. This is useful in certain situations where a rule needs |
1877 to be viewed as an atomic statement from the meta-level perspective, |
1877 to be viewed as an atomic statement from the meta-level perspective, |
1878 e.g.\ \isa{{\isachardoublequote}{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymLongrightarrow}\ P\ x{\isachardoublequote}} versus \isa{{\isachardoublequote}{\isasymforall}x\ {\isasymin}\ A{\isachardot}\ P\ x{\isachardoublequote}}. |
1878 e.g.\ \isa{{\isachardoublequote}{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymLongrightarrow}\ P\ x{\isachardoublequote}} versus \isa{{\isachardoublequote}{\isasymforall}x\ {\isasymin}\ A{\isachardot}\ P\ x{\isachardoublequote}}. |
1879 |
1879 |
1880 From the following language elements, only the \mbox{\isa{atomize}} |
1880 From the following language elements, only the \hyperlink{method.atomize}{\mbox{\isa{atomize}}} |
1881 method and \mbox{\isa{rule{\isacharunderscore}format}} attribute are occasionally |
1881 method and \hyperlink{attribute.rule_format}{\mbox{\isa{rule{\isacharunderscore}format}}} attribute are occasionally |
1882 required by end-users, the rest is for those who need to setup their |
1882 required by end-users, the rest is for those who need to setup their |
1883 own object-logic. In the latter case existing formulations of |
1883 own object-logic. In the latter case existing formulations of |
1884 Isabelle/FOL or Isabelle/HOL may be taken as realistic examples. |
1884 Isabelle/FOL or Isabelle/HOL may be taken as realistic examples. |
1885 |
1885 |
1886 Generic tools may refer to the information provided by object-logic |
1886 Generic tools may refer to the information provided by object-logic |
1895 ; |
1895 ; |
1896 \end{rail} |
1896 \end{rail} |
1897 |
1897 |
1898 \begin{descr} |
1898 \begin{descr} |
1899 |
1899 |
1900 \item [\mbox{\isa{\isacommand{judgment}}}~\isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}}] declares |
1900 \item [\hyperlink{command.judgment}{\mbox{\isa{\isacommand{judgment}}}}~\isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}}] declares |
1901 constant \isa{c} as the truth judgment of the current |
1901 constant \isa{c} as the truth judgment of the current |
1902 object-logic. Its type \isa{{\isasymsigma}} should specify a coercion of the |
1902 object-logic. Its type \isa{{\isasymsigma}} should specify a coercion of the |
1903 category of object-level propositions to \isa{prop} of the Pure |
1903 category of object-level propositions to \isa{prop} of the Pure |
1904 meta-logic; the mixfix annotation \isa{{\isachardoublequote}{\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} would typically |
1904 meta-logic; the mixfix annotation \isa{{\isachardoublequote}{\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} would typically |
1905 just link the object language (internally of syntactic category |
1905 just link the object language (internally of syntactic category |
1906 \isa{logic}) with that of \isa{prop}. Only one \mbox{\isa{\isacommand{judgment}}} declaration may be given in any theory development. |
1906 \isa{logic}) with that of \isa{prop}. Only one \hyperlink{command.judgment}{\mbox{\isa{\isacommand{judgment}}}} declaration may be given in any theory development. |
1907 |
1907 |
1908 \item [\mbox{\isa{atomize}} (as a method)] rewrites any non-atomic |
1908 \item [\hyperlink{method.atomize}{\mbox{\isa{atomize}}} (as a method)] rewrites any non-atomic |
1909 premises of a sub-goal, using the meta-level equations declared via |
1909 premises of a sub-goal, using the meta-level equations declared via |
1910 \mbox{\isa{atomize}} (as an attribute) beforehand. As a result, |
1910 \hyperlink{attribute.atomize}{\mbox{\isa{atomize}}} (as an attribute) beforehand. As a result, |
1911 heavily nested goals become amenable to fundamental operations such |
1911 heavily nested goals become amenable to fundamental operations such |
1912 as resolution (cf.\ the \mbox{\isa{rule}} method). Giving the ``\isa{{\isachardoublequote}{\isacharparenleft}full{\isacharparenright}{\isachardoublequote}}'' option here means to turn the whole subgoal into an |
1912 as resolution (cf.\ the \hyperlink{method.rule}{\mbox{\isa{rule}}} method). Giving the ``\isa{{\isachardoublequote}{\isacharparenleft}full{\isacharparenright}{\isachardoublequote}}'' option here means to turn the whole subgoal into an |
1913 object-statement (if possible), including the outermost parameters |
1913 object-statement (if possible), including the outermost parameters |
1914 and assumptions as well. |
1914 and assumptions as well. |
1915 |
1915 |
1916 A typical collection of \mbox{\isa{atomize}} rules for a particular |
1916 A typical collection of \hyperlink{attribute.atomize}{\mbox{\isa{atomize}}} rules for a particular |
1917 object-logic would provide an internalization for each of the |
1917 object-logic would provide an internalization for each of the |
1918 connectives of \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}}, and \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}}. |
1918 connectives of \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}}, and \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}}. |
1919 Meta-level conjunction should be covered as well (this is |
1919 Meta-level conjunction should be covered as well (this is |
1920 particularly important for locales, see \secref{sec:locale}). |
1920 particularly important for locales, see \secref{sec:locale}). |
1921 |
1921 |
1922 \item [\mbox{\isa{rule{\isacharunderscore}format}}] rewrites a theorem by the |
1922 \item [\hyperlink{attribute.rule_format}{\mbox{\isa{rule{\isacharunderscore}format}}}] rewrites a theorem by the |
1923 equalities declared as \mbox{\isa{rulify}} rules in the current |
1923 equalities declared as \hyperlink{attribute.rulify}{\mbox{\isa{rulify}}} rules in the current |
1924 object-logic. By default, the result is fully normalized, including |
1924 object-logic. By default, the result is fully normalized, including |
1925 assumptions and conclusions at any depth. The \isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isachardoublequote}} |
1925 assumptions and conclusions at any depth. The \isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isachardoublequote}} |
1926 option restricts the transformation to the conclusion of a rule. |
1926 option restricts the transformation to the conclusion of a rule. |
1927 |
1927 |
1928 In common object-logics (HOL, FOL, ZF), the effect of \mbox{\isa{rule{\isacharunderscore}format}} is to replace (bounded) universal quantification |
1928 In common object-logics (HOL, FOL, ZF), the effect of \hyperlink{attribute.rule_format}{\mbox{\isa{rule{\isacharunderscore}format}}} is to replace (bounded) universal quantification |
1929 (\isa{{\isachardoublequote}{\isasymforall}{\isachardoublequote}}) and implication (\isa{{\isachardoublequote}{\isasymlongrightarrow}{\isachardoublequote}}) by the corresponding |
1929 (\isa{{\isachardoublequote}{\isasymforall}{\isachardoublequote}}) and implication (\isa{{\isachardoublequote}{\isasymlongrightarrow}{\isachardoublequote}}) by the corresponding |
1930 rule statements over \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}} and \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}}. |
1930 rule statements over \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}} and \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}}. |
1931 |
1931 |
1932 \end{descr}% |
1932 \end{descr}% |
1933 \end{isamarkuptext}% |
1933 \end{isamarkuptext}% |