author | wenzelm |
Tue, 26 Oct 2010 15:57:16 +0200 | |
changeset 40153 | b6fe3b189725 |
parent 40126 | 916cb4a28ffd |
child 40406 | 313a24b66a8d |
permissions | -rw-r--r-- |
30296 | 1 |
% |
2 |
\begin{isabellebody}% |
|
3 |
\def\isabellecontext{Proof}% |
|
4 |
% |
|
5 |
\isadelimtheory |
|
6 |
% |
|
7 |
\endisadelimtheory |
|
8 |
% |
|
9 |
\isatagtheory |
|
10 |
\isacommand{theory}\isamarkupfalse% |
|
11 |
\ Proof\isanewline |
|
12 |
\isakeyword{imports}\ Base\isanewline |
|
13 |
\isakeyword{begin}% |
|
14 |
\endisatagtheory |
|
15 |
{\isafoldtheory}% |
|
16 |
% |
|
17 |
\isadelimtheory |
|
18 |
% |
|
19 |
\endisadelimtheory |
|
20 |
% |
|
21 |
\isamarkupchapter{Structured proofs% |
|
22 |
} |
|
23 |
\isamarkuptrue% |
|
24 |
% |
|
25 |
\isamarkupsection{Variables \label{sec:variables}% |
|
26 |
} |
|
27 |
\isamarkuptrue% |
|
28 |
% |
|
29 |
\begin{isamarkuptext}% |
|
30 |
Any variable that is not explicitly bound by \isa{{\isasymlambda}}-abstraction |
|
31 |
is considered as ``free''. Logically, free variables act like |
|
32 |
outermost universal quantification at the sequent level: \isa{A\isactrlisub {\isadigit{1}}{\isacharparenleft}x{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n{\isacharparenleft}x{\isacharparenright}\ {\isasymturnstile}\ B{\isacharparenleft}x{\isacharparenright}} means that the result |
|
33 |
holds \emph{for all} values of \isa{x}. Free variables for |
|
34 |
terms (not types) can be fully internalized into the logic: \isa{{\isasymturnstile}\ B{\isacharparenleft}x{\isacharparenright}} and \isa{{\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ B{\isacharparenleft}x{\isacharparenright}} are interchangeable, provided |
|
35 |
that \isa{x} does not occur elsewhere in the context. |
|
36 |
Inspecting \isa{{\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ B{\isacharparenleft}x{\isacharparenright}} more closely, we see that inside the |
|
37 |
quantifier, \isa{x} is essentially ``arbitrary, but fixed'', |
|
38 |
while from outside it appears as a place-holder for instantiation |
|
39 |
(thanks to \isa{{\isasymAnd}} elimination). |
|
40 |
||
41 |
The Pure logic represents the idea of variables being either inside |
|
42 |
or outside the current scope by providing separate syntactic |
|
43 |
categories for \emph{fixed variables} (e.g.\ \isa{x}) vs.\ |
|
44 |
\emph{schematic variables} (e.g.\ \isa{{\isacharquery}x}). Incidently, a |
|
35001 | 45 |
universal result \isa{{\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ B{\isacharparenleft}x{\isacharparenright}} has the HHF normal form \isa{{\isasymturnstile}\ B{\isacharparenleft}{\isacharquery}x{\isacharparenright}}, which represents its generality without requiring an |
46 |
explicit quantifier. The same principle works for type variables: |
|
47 |
\isa{{\isasymturnstile}\ B{\isacharparenleft}{\isacharquery}{\isasymalpha}{\isacharparenright}} represents the idea of ``\isa{{\isasymturnstile}\ {\isasymforall}{\isasymalpha}{\isachardot}\ B{\isacharparenleft}{\isasymalpha}{\isacharparenright}}'' |
|
48 |
without demanding a truly polymorphic framework. |
|
30296 | 49 |
|
50 |
\medskip Additional care is required to treat type variables in a |
|
51 |
way that facilitates type-inference. In principle, term variables |
|
52 |
depend on type variables, which means that type variables would have |
|
53 |
to be declared first. For example, a raw type-theoretic framework |
|
54 |
would demand the context to be constructed in stages as follows: |
|
55 |
\isa{{\isasymGamma}\ {\isacharequal}\ {\isasymalpha}{\isacharcolon}\ type{\isacharcomma}\ x{\isacharcolon}\ {\isasymalpha}{\isacharcomma}\ a{\isacharcolon}\ A{\isacharparenleft}x\isactrlisub {\isasymalpha}{\isacharparenright}}. |
|
56 |
||
57 |
We allow a slightly less formalistic mode of operation: term |
|
58 |
variables \isa{x} are fixed without specifying a type yet |
|
59 |
(essentially \emph{all} potential occurrences of some instance |
|
60 |
\isa{x\isactrlisub {\isasymtau}} are fixed); the first occurrence of \isa{x} |
|
61 |
within a specific term assigns its most general type, which is then |
|
62 |
maintained consistently in the context. The above example becomes |
|
63 |
\isa{{\isasymGamma}\ {\isacharequal}\ x{\isacharcolon}\ term{\isacharcomma}\ {\isasymalpha}{\isacharcolon}\ type{\isacharcomma}\ A{\isacharparenleft}x\isactrlisub {\isasymalpha}{\isacharparenright}}, where type \isa{{\isasymalpha}} is fixed \emph{after} term \isa{x}, and the constraint |
|
64 |
\isa{x\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}} is an implicit consequence of the occurrence of |
|
65 |
\isa{x\isactrlisub {\isasymalpha}} in the subsequent proposition. |
|
66 |
||
67 |
This twist of dependencies is also accommodated by the reverse |
|
68 |
operation of exporting results from a context: a type variable |
|
69 |
\isa{{\isasymalpha}} is considered fixed as long as it occurs in some fixed |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
70 |
term variable of the context. For example, exporting \isa{x{\isacharcolon}\ term{\isacharcomma}\ {\isasymalpha}{\isacharcolon}\ type\ {\isasymturnstile}\ x\isactrlisub {\isasymalpha}\ {\isasymequiv}\ x\isactrlisub {\isasymalpha}} produces in the first step \isa{x{\isacharcolon}\ term\ {\isasymturnstile}\ x\isactrlisub {\isasymalpha}\ {\isasymequiv}\ x\isactrlisub {\isasymalpha}} for fixed \isa{{\isasymalpha}}, and only in the second step |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
71 |
\isa{{\isasymturnstile}\ {\isacharquery}x\isactrlisub {\isacharquery}\isactrlisub {\isasymalpha}\ {\isasymequiv}\ {\isacharquery}x\isactrlisub {\isacharquery}\isactrlisub {\isasymalpha}} for schematic \isa{{\isacharquery}x} and \isa{{\isacharquery}{\isasymalpha}}. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
72 |
The following Isar source text illustrates this scenario.% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
73 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
74 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
75 |
\isacommand{example{\isacharunderscore}proof}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
76 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
77 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
78 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
79 |
\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
80 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
81 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
82 |
\isatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
83 |
\isacommand{{\isacharbraceleft}}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
84 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
85 |
\ \ \ \ \isacommand{fix}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
86 |
\ x\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
87 |
\isamarkupcmt{all potential occurrences of some \isa{x{\isacharcolon}{\isacharcolon}{\isasymtau}} are fixed% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
88 |
} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
89 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
90 |
\ \ \ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
91 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
92 |
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
93 |
\ {\isachardoublequoteopen}x{\isacharcolon}{\isacharcolon}{\isacharprime}a\ {\isasymequiv}\ x{\isachardoublequoteclose}\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
94 |
\isamarkupcmt{implicit type assigment by concrete occurrence% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
95 |
} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
96 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
97 |
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
98 |
\ {\isacharparenleft}rule\ reflexive{\isacharparenright}\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
99 |
\ \ \ \ \isacommand{{\isacharbraceright}}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
100 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
101 |
\endisatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
102 |
{\isafoldproof}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
103 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
104 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
105 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
106 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
107 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
108 |
\ \ \ \ \isacommand{thm}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
109 |
\ this\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
110 |
\isamarkupcmt{result still with fixed type \isa{{\isacharprime}a}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
111 |
} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
112 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
113 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
114 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
115 |
\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
116 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
117 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
118 |
\isatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
119 |
\isacommand{{\isacharbraceright}}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
120 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
121 |
\endisatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
122 |
{\isafoldproof}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
123 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
124 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
125 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
126 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
127 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
128 |
\ \ \isacommand{thm}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
129 |
\ this\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
130 |
\isamarkupcmt{fully general result for arbitrary \isa{{\isacharquery}x{\isacharcolon}{\isacharcolon}{\isacharquery}{\isacharprime}a}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
131 |
} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
132 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
133 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
134 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
135 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
136 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
137 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
138 |
\isatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
139 |
\isacommand{qed}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
140 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
141 |
\endisatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
142 |
{\isafoldproof}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
143 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
144 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
145 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
146 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
147 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
148 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
149 |
The Isabelle/Isar proof context manages the details of term |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
150 |
vs.\ type variables, with high-level principles for moving the |
30296 | 151 |
frontier between fixed and schematic variables. |
152 |
||
153 |
The \isa{add{\isacharunderscore}fixes} operation explictly declares fixed |
|
154 |
variables; the \isa{declare{\isacharunderscore}term} operation absorbs a term into |
|
155 |
a context by fixing new type variables and adding syntactic |
|
156 |
constraints. |
|
157 |
||
158 |
The \isa{export} operation is able to perform the main work of |
|
159 |
generalizing term and type variables as sketched above, assuming |
|
160 |
that fixing variables and terms have been declared properly. |
|
161 |
||
162 |
There \isa{import} operation makes a generalized fact a genuine |
|
163 |
part of the context, by inventing fixed variables for the schematic |
|
164 |
ones. The effect can be reversed by using \isa{export} later, |
|
165 |
potentially with an extended context; the result is equivalent to |
|
166 |
the original modulo renaming of schematic variables. |
|
167 |
||
168 |
The \isa{focus} operation provides a variant of \isa{import} |
|
169 |
for nested propositions (with explicit quantification): \isa{{\isasymAnd}x\isactrlisub {\isadigit{1}}\ {\isasymdots}\ x\isactrlisub n{\isachardot}\ B{\isacharparenleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlisub n{\isacharparenright}} is |
|
170 |
decomposed by inventing fixed variables \isa{x\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlisub n} for the body.% |
|
171 |
\end{isamarkuptext}% |
|
172 |
\isamarkuptrue% |
|
173 |
% |
|
174 |
\isadelimmlref |
|
175 |
% |
|
176 |
\endisadelimmlref |
|
177 |
% |
|
178 |
\isatagmlref |
|
179 |
% |
|
180 |
\begin{isamarkuptext}% |
|
181 |
\begin{mldecls} |
|
182 |
\indexdef{}{ML}{Variable.add\_fixes}\verb|Variable.add_fixes: |\isasep\isanewline% |
|
183 |
\verb| string list -> Proof.context -> string list * Proof.context| \\ |
|
184 |
\indexdef{}{ML}{Variable.variant\_fixes}\verb|Variable.variant_fixes: |\isasep\isanewline% |
|
185 |
\verb| string list -> Proof.context -> string list * Proof.context| \\ |
|
186 |
\indexdef{}{ML}{Variable.declare\_term}\verb|Variable.declare_term: term -> Proof.context -> Proof.context| \\ |
|
187 |
\indexdef{}{ML}{Variable.declare\_constraints}\verb|Variable.declare_constraints: term -> Proof.context -> Proof.context| \\ |
|
188 |
\indexdef{}{ML}{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\ |
|
189 |
\indexdef{}{ML}{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\ |
|
31794
71af1fd6a5e4
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
wenzelm
parents:
30296
diff
changeset
|
190 |
\indexdef{}{ML}{Variable.import}\verb|Variable.import: bool -> thm list -> Proof.context ->|\isasep\isanewline% |
32302 | 191 |
\verb| (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context| \\ |
35001 | 192 |
\indexdef{}{ML}{Variable.focus}\verb|Variable.focus: cterm -> Proof.context ->|\isasep\isanewline% |
193 |
\verb| ((string * cterm) list * cterm) * Proof.context| \\ |
|
30296 | 194 |
\end{mldecls} |
195 |
||
196 |
\begin{description} |
|
197 |
||
198 |
\item \verb|Variable.add_fixes|~\isa{xs\ ctxt} fixes term |
|
199 |
variables \isa{xs}, returning the resulting internal names. By |
|
200 |
default, the internal representation coincides with the external |
|
201 |
one, which also means that the given variables must not be fixed |
|
202 |
already. There is a different policy within a local proof body: the |
|
203 |
given names are just hints for newly invented Skolem variables. |
|
204 |
||
205 |
\item \verb|Variable.variant_fixes| is similar to \verb|Variable.add_fixes|, but always produces fresh variants of the given |
|
206 |
names. |
|
207 |
||
208 |
\item \verb|Variable.declare_term|~\isa{t\ ctxt} declares term |
|
209 |
\isa{t} to belong to the context. This automatically fixes new |
|
210 |
type variables, but not term variables. Syntactic constraints for |
|
211 |
type and term variables are declared uniformly, though. |
|
212 |
||
213 |
\item \verb|Variable.declare_constraints|~\isa{t\ ctxt} declares |
|
214 |
syntactic constraints from term \isa{t}, without making it part |
|
215 |
of the context yet. |
|
216 |
||
217 |
\item \verb|Variable.export|~\isa{inner\ outer\ thms} generalizes |
|
218 |
fixed type and term variables in \isa{thms} according to the |
|
219 |
difference of the \isa{inner} and \isa{outer} context, |
|
220 |
following the principles sketched above. |
|
221 |
||
222 |
\item \verb|Variable.polymorphic|~\isa{ctxt\ ts} generalizes type |
|
223 |
variables in \isa{ts} as far as possible, even those occurring |
|
224 |
in fixed term variables. The default policy of type-inference is to |
|
225 |
fix newly introduced type variables, which is essentially reversed |
|
226 |
with \verb|Variable.polymorphic|: here the given terms are detached |
|
227 |
from the context as far as possible. |
|
228 |
||
31794
71af1fd6a5e4
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
wenzelm
parents:
30296
diff
changeset
|
229 |
\item \verb|Variable.import|~\isa{open\ thms\ ctxt} invents fixed |
30296 | 230 |
type and term variables for the schematic ones occurring in \isa{thms}. The \isa{open} flag indicates whether the fixed names |
231 |
should be accessible to the user, otherwise newly introduced names |
|
232 |
are marked as ``internal'' (\secref{sec:names}). |
|
233 |
||
234 |
\item \verb|Variable.focus|~\isa{B} decomposes the outermost \isa{{\isasymAnd}} prefix of proposition \isa{B}. |
|
235 |
||
236 |
\end{description}% |
|
237 |
\end{isamarkuptext}% |
|
238 |
\isamarkuptrue% |
|
239 |
% |
|
240 |
\endisatagmlref |
|
241 |
{\isafoldmlref}% |
|
242 |
% |
|
243 |
\isadelimmlref |
|
244 |
% |
|
245 |
\endisadelimmlref |
|
246 |
% |
|
35001 | 247 |
\isadelimmlex |
248 |
% |
|
249 |
\endisadelimmlex |
|
250 |
% |
|
251 |
\isatagmlex |
|
252 |
% |
|
253 |
\begin{isamarkuptext}% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
254 |
The following example shows how to work with fixed term |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
255 |
and type parameters and with type-inference.% |
35001 | 256 |
\end{isamarkuptext}% |
257 |
\isamarkuptrue% |
|
258 |
% |
|
259 |
\endisatagmlex |
|
260 |
{\isafoldmlex}% |
|
261 |
% |
|
262 |
\isadelimmlex |
|
263 |
% |
|
264 |
\endisadelimmlex |
|
265 |
% |
|
266 |
\isadelimML |
|
267 |
% |
|
268 |
\endisadelimML |
|
269 |
% |
|
270 |
\isatagML |
|
271 |
\isacommand{ML}\isamarkupfalse% |
|
272 |
\ {\isacharverbatimopen}\isanewline |
|
273 |
\ \ {\isacharparenleft}{\isacharasterisk}static\ compile{\isacharminus}time\ context\ {\isacharminus}{\isacharminus}\ for\ testing\ only{\isacharasterisk}{\isacharparenright}\isanewline |
|
274 |
\ \ val\ ctxt{\isadigit{0}}\ {\isacharequal}\ % |
|
275 |
\isaantiq |
|
276 |
context% |
|
277 |
\endisaantiq |
|
278 |
{\isacharsemicolon}\isanewline |
|
279 |
\isanewline |
|
280 |
\ \ {\isacharparenleft}{\isacharasterisk}locally\ fixed\ parameters\ {\isacharminus}{\isacharminus}\ no\ type\ assignment\ yet{\isacharasterisk}{\isacharparenright}\isanewline |
|
281 |
\ \ val\ {\isacharparenleft}{\isacharbrackleft}x{\isacharcomma}\ y{\isacharbrackright}{\isacharcomma}\ ctxt{\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ ctxt{\isadigit{0}}\ {\isacharbar}{\isachargreater}\ Variable{\isachardot}add{\isacharunderscore}fixes\ {\isacharbrackleft}{\isachardoublequote}x{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}y{\isachardoublequote}{\isacharbrackright}{\isacharsemicolon}\isanewline |
|
282 |
\isanewline |
|
283 |
\ \ {\isacharparenleft}{\isacharasterisk}t{\isadigit{1}}{\isacharcolon}\ most\ general\ fixed\ type{\isacharsemicolon}\ t{\isadigit{1}}{\isacharprime}{\isacharcolon}\ most\ general\ arbitrary\ type{\isacharasterisk}{\isacharparenright}\isanewline |
|
284 |
\ \ val\ t{\isadigit{1}}\ {\isacharequal}\ Syntax{\isachardot}read{\isacharunderscore}term\ ctxt{\isadigit{1}}\ {\isachardoublequote}x{\isachardoublequote}{\isacharsemicolon}\isanewline |
|
285 |
\ \ val\ t{\isadigit{1}}{\isacharprime}\ {\isacharequal}\ singleton\ {\isacharparenleft}Variable{\isachardot}polymorphic\ ctxt{\isadigit{1}}{\isacharparenright}\ t{\isadigit{1}}{\isacharsemicolon}\isanewline |
|
286 |
\isanewline |
|
287 |
\ \ {\isacharparenleft}{\isacharasterisk}term\ u\ enforces\ specific\ type\ assignment{\isacharasterisk}{\isacharparenright}\isanewline |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
288 |
\ \ val\ u\ {\isacharequal}\ Syntax{\isachardot}read{\isacharunderscore}term\ ctxt{\isadigit{1}}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isasymequiv}\ y{\isachardoublequote}{\isacharsemicolon}\isanewline |
35001 | 289 |
\isanewline |
290 |
\ \ {\isacharparenleft}{\isacharasterisk}official\ declaration\ of\ u\ {\isacharminus}{\isacharminus}\ propagates\ constraints\ etc{\isachardot}{\isacharasterisk}{\isacharparenright}\isanewline |
|
291 |
\ \ val\ ctxt{\isadigit{2}}\ {\isacharequal}\ ctxt{\isadigit{1}}\ {\isacharbar}{\isachargreater}\ Variable{\isachardot}declare{\isacharunderscore}term\ u{\isacharsemicolon}\isanewline |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
292 |
\ \ val\ t{\isadigit{2}}\ {\isacharequal}\ Syntax{\isachardot}read{\isacharunderscore}term\ ctxt{\isadigit{2}}\ {\isachardoublequote}x{\isachardoublequote}{\isacharsemicolon}\ \ {\isacharparenleft}{\isacharasterisk}x{\isacharcolon}{\isacharcolon}nat\ is\ enforced{\isacharasterisk}{\isacharparenright}\isanewline |
35001 | 293 |
{\isacharverbatimclose}% |
294 |
\endisatagML |
|
295 |
{\isafoldML}% |
|
296 |
% |
|
297 |
\isadelimML |
|
298 |
% |
|
299 |
\endisadelimML |
|
300 |
% |
|
301 |
\begin{isamarkuptext}% |
|
40126 | 302 |
In the above example, the starting context is derived from the |
303 |
toplevel theory, which means that fixed variables are internalized |
|
40153 | 304 |
literally: \isa{x} is mapped again to \isa{x}, and |
40126 | 305 |
attempting to fix it again in the subsequent context is an error. |
306 |
Alternatively, fixed parameters can be renamed explicitly as |
|
307 |
follows:% |
|
35001 | 308 |
\end{isamarkuptext}% |
309 |
\isamarkuptrue% |
|
310 |
% |
|
311 |
\isadelimML |
|
312 |
% |
|
313 |
\endisadelimML |
|
314 |
% |
|
315 |
\isatagML |
|
316 |
\isacommand{ML}\isamarkupfalse% |
|
317 |
\ {\isacharverbatimopen}\isanewline |
|
318 |
\ \ val\ ctxt{\isadigit{0}}\ {\isacharequal}\ % |
|
319 |
\isaantiq |
|
320 |
context% |
|
321 |
\endisaantiq |
|
322 |
{\isacharsemicolon}\isanewline |
|
323 |
\ \ val\ {\isacharparenleft}{\isacharbrackleft}x{\isadigit{1}}{\isacharcomma}\ x{\isadigit{2}}{\isacharcomma}\ x{\isadigit{3}}{\isacharbrackright}{\isacharcomma}\ ctxt{\isadigit{1}}{\isacharparenright}\ {\isacharequal}\isanewline |
|
324 |
\ \ \ \ ctxt{\isadigit{0}}\ {\isacharbar}{\isachargreater}\ Variable{\isachardot}variant{\isacharunderscore}fixes\ {\isacharbrackleft}{\isachardoublequote}x{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}x{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}x{\isachardoublequote}{\isacharbrackright}{\isacharsemicolon}\isanewline |
|
325 |
{\isacharverbatimclose}% |
|
326 |
\endisatagML |
|
327 |
{\isafoldML}% |
|
328 |
% |
|
329 |
\isadelimML |
|
330 |
% |
|
331 |
\endisadelimML |
|
332 |
% |
|
333 |
\begin{isamarkuptext}% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
334 |
The following ML code can now work with the invented names of |
40153 | 335 |
\isa{x{\isadigit{1}}}, \isa{x{\isadigit{2}}}, \isa{x{\isadigit{3}}}, without depending on |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
336 |
the details on the system policy for introducing these variants. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
337 |
Recall that within a proof body the system always invents fresh |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
338 |
``skolem constants'', e.g.\ as follows:% |
35001 | 339 |
\end{isamarkuptext}% |
340 |
\isamarkuptrue% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
341 |
\isacommand{example{\isacharunderscore}proof}\isamarkupfalse% |
35001 | 342 |
\isanewline |
343 |
% |
|
344 |
\isadelimML |
|
345 |
\ \ % |
|
346 |
\endisadelimML |
|
347 |
% |
|
348 |
\isatagML |
|
349 |
\isacommand{ML{\isacharunderscore}prf}\isamarkupfalse% |
|
350 |
\ {\isacharverbatimopen}\isanewline |
|
351 |
\ \ \ \ val\ ctxt{\isadigit{0}}\ {\isacharequal}\ % |
|
352 |
\isaantiq |
|
353 |
context% |
|
354 |
\endisaantiq |
|
355 |
{\isacharsemicolon}\isanewline |
|
356 |
\isanewline |
|
357 |
\ \ \ \ val\ {\isacharparenleft}{\isacharbrackleft}x{\isadigit{1}}{\isacharbrackright}{\isacharcomma}\ ctxt{\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ ctxt{\isadigit{0}}\ {\isacharbar}{\isachargreater}\ Variable{\isachardot}add{\isacharunderscore}fixes\ {\isacharbrackleft}{\isachardoublequote}x{\isachardoublequote}{\isacharbrackright}{\isacharsemicolon}\isanewline |
|
358 |
\ \ \ \ val\ {\isacharparenleft}{\isacharbrackleft}x{\isadigit{2}}{\isacharbrackright}{\isacharcomma}\ ctxt{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ ctxt{\isadigit{1}}\ {\isacharbar}{\isachargreater}\ Variable{\isachardot}add{\isacharunderscore}fixes\ {\isacharbrackleft}{\isachardoublequote}x{\isachardoublequote}{\isacharbrackright}{\isacharsemicolon}\isanewline |
|
359 |
\ \ \ \ val\ {\isacharparenleft}{\isacharbrackleft}x{\isadigit{3}}{\isacharbrackright}{\isacharcomma}\ ctxt{\isadigit{3}}{\isacharparenright}\ {\isacharequal}\ ctxt{\isadigit{2}}\ {\isacharbar}{\isachargreater}\ Variable{\isachardot}add{\isacharunderscore}fixes\ {\isacharbrackleft}{\isachardoublequote}x{\isachardoublequote}{\isacharbrackright}{\isacharsemicolon}\isanewline |
|
360 |
\isanewline |
|
361 |
\ \ \ \ val\ {\isacharparenleft}{\isacharbrackleft}y{\isadigit{1}}{\isacharcomma}\ y{\isadigit{2}}{\isacharbrackright}{\isacharcomma}\ ctxt{\isadigit{4}}{\isacharparenright}\ {\isacharequal}\isanewline |
|
362 |
\ \ \ \ \ \ ctxt{\isadigit{3}}\ {\isacharbar}{\isachargreater}\ Variable{\isachardot}variant{\isacharunderscore}fixes\ {\isacharbrackleft}{\isachardoublequote}y{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}y{\isachardoublequote}{\isacharbrackright}{\isacharsemicolon}\isanewline |
|
363 |
\ \ {\isacharverbatimclose}\isanewline |
|
364 |
\ \ \isacommand{oops}\isamarkupfalse% |
|
365 |
% |
|
366 |
\endisatagML |
|
367 |
{\isafoldML}% |
|
368 |
% |
|
369 |
\isadelimML |
|
370 |
% |
|
371 |
\endisadelimML |
|
372 |
% |
|
373 |
\begin{isamarkuptext}% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
374 |
In this situation \verb|Variable.add_fixes| and \verb|Variable.variant_fixes| are very similar, but identical name |
35001 | 375 |
proposals given in a row are only accepted by the second version.% |
376 |
\end{isamarkuptext}% |
|
377 |
\isamarkuptrue% |
|
378 |
% |
|
30296 | 379 |
\isamarkupsection{Assumptions \label{sec:assumptions}% |
380 |
} |
|
381 |
\isamarkuptrue% |
|
382 |
% |
|
383 |
\begin{isamarkuptext}% |
|
384 |
An \emph{assumption} is a proposition that it is postulated in the |
|
385 |
current context. Local conclusions may use assumptions as |
|
386 |
additional facts, but this imposes implicit hypotheses that weaken |
|
387 |
the overall statement. |
|
388 |
||
389 |
Assumptions are restricted to fixed non-schematic statements, i.e.\ |
|
390 |
all generality needs to be expressed by explicit quantifiers. |
|
391 |
Nevertheless, the result will be in HHF normal form with outermost |
|
392 |
quantifiers stripped. For example, by assuming \isa{{\isasymAnd}x\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}{\isachardot}\ P\ x} we get \isa{{\isasymAnd}x\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}{\isachardot}\ P\ x\ {\isasymturnstile}\ P\ {\isacharquery}x} for schematic \isa{{\isacharquery}x} |
|
393 |
of fixed type \isa{{\isasymalpha}}. Local derivations accumulate more and |
|
394 |
more explicit references to hypotheses: \isa{A\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n\ {\isasymturnstile}\ B} where \isa{A\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n} needs to |
|
395 |
be covered by the assumptions of the current context. |
|
396 |
||
397 |
\medskip The \isa{add{\isacharunderscore}assms} operation augments the context by |
|
398 |
local assumptions, which are parameterized by an arbitrary \isa{export} rule (see below). |
|
399 |
||
400 |
The \isa{export} operation moves facts from a (larger) inner |
|
401 |
context into a (smaller) outer context, by discharging the |
|
402 |
difference of the assumptions as specified by the associated export |
|
403 |
rules. Note that the discharged portion is determined by the |
|
35001 | 404 |
difference of contexts, not the facts being exported! There is a |
30296 | 405 |
separate flag to indicate a goal context, where the result is meant |
406 |
to refine an enclosing sub-goal of a structured proof state. |
|
407 |
||
408 |
\medskip The most basic export rule discharges assumptions directly |
|
409 |
by means of the \isa{{\isasymLongrightarrow}} introduction rule: |
|
410 |
\[ |
|
35001 | 411 |
\infer[(\isa{{\isasymLongrightarrow}{\isasymdash}intro})]{\isa{{\isasymGamma}\ {\isacharminus}\ A\ {\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}} |
30296 | 412 |
\] |
413 |
||
414 |
The variant for goal refinements marks the newly introduced |
|
415 |
premises, which causes the canonical Isar goal refinement scheme to |
|
416 |
enforce unification with local premises within the goal: |
|
417 |
\[ |
|
35001 | 418 |
\infer[(\isa{{\isacharhash}{\isasymLongrightarrow}{\isasymdash}intro})]{\isa{{\isasymGamma}\ {\isacharminus}\ A\ {\isasymturnstile}\ {\isacharhash}A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}} |
30296 | 419 |
\] |
420 |
||
421 |
\medskip Alternative versions of assumptions may perform arbitrary |
|
422 |
transformations on export, as long as the corresponding portion of |
|
423 |
hypotheses is removed from the given facts. For example, a local |
|
424 |
definition works by fixing \isa{x} and assuming \isa{x\ {\isasymequiv}\ t}, |
|
425 |
with the following export rule to reverse the effect: |
|
426 |
\[ |
|
35001 | 427 |
\infer[(\isa{{\isasymequiv}{\isasymdash}expand})]{\isa{{\isasymGamma}\ {\isacharminus}\ {\isacharparenleft}x\ {\isasymequiv}\ t{\isacharparenright}\ {\isasymturnstile}\ B\ t}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B\ x}} |
30296 | 428 |
\] |
429 |
This works, because the assumption \isa{x\ {\isasymequiv}\ t} was introduced in |
|
430 |
a context with \isa{x} being fresh, so \isa{x} does not |
|
431 |
occur in \isa{{\isasymGamma}} here.% |
|
432 |
\end{isamarkuptext}% |
|
433 |
\isamarkuptrue% |
|
434 |
% |
|
435 |
\isadelimmlref |
|
436 |
% |
|
437 |
\endisadelimmlref |
|
438 |
% |
|
439 |
\isatagmlref |
|
440 |
% |
|
441 |
\begin{isamarkuptext}% |
|
442 |
\begin{mldecls} |
|
443 |
\indexdef{}{ML type}{Assumption.export}\verb|type Assumption.export| \\ |
|
444 |
\indexdef{}{ML}{Assumption.assume}\verb|Assumption.assume: cterm -> thm| \\ |
|
445 |
\indexdef{}{ML}{Assumption.add\_assms}\verb|Assumption.add_assms: Assumption.export ->|\isasep\isanewline% |
|
446 |
\verb| cterm list -> Proof.context -> thm list * Proof.context| \\ |
|
447 |
\indexdef{}{ML}{Assumption.add\_assumes}\verb|Assumption.add_assumes: |\isasep\isanewline% |
|
448 |
\verb| cterm list -> Proof.context -> thm list * Proof.context| \\ |
|
449 |
\indexdef{}{ML}{Assumption.export}\verb|Assumption.export: bool -> Proof.context -> Proof.context -> thm -> thm| \\ |
|
450 |
\end{mldecls} |
|
451 |
||
452 |
\begin{description} |
|
453 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
454 |
\item Type \verb|Assumption.export| represents arbitrary export |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
455 |
rules, which is any function of type \verb|bool -> cterm list|\isasep\isanewline% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
456 |
\verb| -> thm -> thm|, where the \verb|bool| indicates goal mode, |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
457 |
and the \verb|cterm list| the collection of assumptions to be |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
458 |
discharged simultaneously. |
30296 | 459 |
|
35001 | 460 |
\item \verb|Assumption.assume|~\isa{A} turns proposition \isa{A} into a primitive assumption \isa{A\ {\isasymturnstile}\ A{\isacharprime}}, where the |
461 |
conclusion \isa{A{\isacharprime}} is in HHF normal form. |
|
30296 | 462 |
|
463 |
\item \verb|Assumption.add_assms|~\isa{r\ As} augments the context |
|
464 |
by assumptions \isa{As} with export rule \isa{r}. The |
|
465 |
resulting facts are hypothetical theorems as produced by the raw |
|
466 |
\verb|Assumption.assume|. |
|
467 |
||
468 |
\item \verb|Assumption.add_assumes|~\isa{As} is a special case of |
|
35001 | 469 |
\verb|Assumption.add_assms| where the export rule performs \isa{{\isasymLongrightarrow}{\isasymdash}intro} or \isa{{\isacharhash}{\isasymLongrightarrow}{\isasymdash}intro}, depending on goal |
470 |
mode. |
|
30296 | 471 |
|
472 |
\item \verb|Assumption.export|~\isa{is{\isacharunderscore}goal\ inner\ outer\ thm} |
|
473 |
exports result \isa{thm} from the the \isa{inner} context |
|
474 |
back into the \isa{outer} one; \isa{is{\isacharunderscore}goal\ {\isacharequal}\ true} means |
|
475 |
this is a goal context. The result is in HHF normal form. Note |
|
476 |
that \verb|ProofContext.export| combines \verb|Variable.export| |
|
477 |
and \verb|Assumption.export| in the canonical way. |
|
478 |
||
479 |
\end{description}% |
|
480 |
\end{isamarkuptext}% |
|
481 |
\isamarkuptrue% |
|
482 |
% |
|
483 |
\endisatagmlref |
|
484 |
{\isafoldmlref}% |
|
485 |
% |
|
486 |
\isadelimmlref |
|
487 |
% |
|
488 |
\endisadelimmlref |
|
489 |
% |
|
35001 | 490 |
\isadelimmlex |
491 |
% |
|
492 |
\endisadelimmlex |
|
493 |
% |
|
494 |
\isatagmlex |
|
495 |
% |
|
496 |
\begin{isamarkuptext}% |
|
497 |
The following example demonstrates how rules can be |
|
498 |
derived by building up a context of assumptions first, and exporting |
|
499 |
some local fact afterwards. We refer to \hyperlink{theory.Pure}{\mbox{\isa{Pure}}} equality |
|
500 |
here for testing purposes.% |
|
501 |
\end{isamarkuptext}% |
|
502 |
\isamarkuptrue% |
|
503 |
% |
|
504 |
\endisatagmlex |
|
505 |
{\isafoldmlex}% |
|
506 |
% |
|
507 |
\isadelimmlex |
|
508 |
% |
|
509 |
\endisadelimmlex |
|
510 |
% |
|
511 |
\isadelimML |
|
512 |
% |
|
513 |
\endisadelimML |
|
514 |
% |
|
515 |
\isatagML |
|
516 |
\isacommand{ML}\isamarkupfalse% |
|
517 |
\ {\isacharverbatimopen}\isanewline |
|
518 |
\ \ {\isacharparenleft}{\isacharasterisk}static\ compile{\isacharminus}time\ context\ {\isacharminus}{\isacharminus}\ for\ testing\ only{\isacharasterisk}{\isacharparenright}\isanewline |
|
519 |
\ \ val\ ctxt{\isadigit{0}}\ {\isacharequal}\ % |
|
520 |
\isaantiq |
|
521 |
context% |
|
522 |
\endisaantiq |
|
523 |
{\isacharsemicolon}\isanewline |
|
524 |
\isanewline |
|
525 |
\ \ val\ {\isacharparenleft}{\isacharbrackleft}eq{\isacharbrackright}{\isacharcomma}\ ctxt{\isadigit{1}}{\isacharparenright}\ {\isacharequal}\isanewline |
|
526 |
\ \ \ \ ctxt{\isadigit{0}}\ {\isacharbar}{\isachargreater}\ Assumption{\isachardot}add{\isacharunderscore}assumes\ {\isacharbrackleft}% |
|
527 |
\isaantiq |
|
528 |
cprop\ {\isachardoublequote}x\ {\isasymequiv}\ y{\isachardoublequote}% |
|
529 |
\endisaantiq |
|
530 |
{\isacharbrackright}{\isacharsemicolon}\isanewline |
|
531 |
\ \ val\ eq{\isacharprime}\ {\isacharequal}\ Thm{\isachardot}symmetric\ eq{\isacharsemicolon}\isanewline |
|
532 |
\isanewline |
|
533 |
\ \ {\isacharparenleft}{\isacharasterisk}back\ to\ original\ context\ {\isacharminus}{\isacharminus}\ discharges\ assumption{\isacharasterisk}{\isacharparenright}\isanewline |
|
534 |
\ \ val\ r\ {\isacharequal}\ Assumption{\isachardot}export\ false\ ctxt{\isadigit{1}}\ ctxt{\isadigit{0}}\ eq{\isacharprime}{\isacharsemicolon}\isanewline |
|
535 |
{\isacharverbatimclose}% |
|
536 |
\endisatagML |
|
537 |
{\isafoldML}% |
|
538 |
% |
|
539 |
\isadelimML |
|
540 |
% |
|
541 |
\endisadelimML |
|
542 |
% |
|
543 |
\begin{isamarkuptext}% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
544 |
Note that the variables of the resulting rule are not |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
545 |
generalized. This would have required to fix them properly in the |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
546 |
context beforehand, and export wrt.\ variables afterwards (cf.\ \verb|Variable.export| or the combined \verb|ProofContext.export|).% |
35001 | 547 |
\end{isamarkuptext}% |
548 |
\isamarkuptrue% |
|
549 |
% |
|
550 |
\isamarkupsection{Structured goals and results \label{sec:struct-goals}% |
|
30296 | 551 |
} |
552 |
\isamarkuptrue% |
|
553 |
% |
|
554 |
\begin{isamarkuptext}% |
|
555 |
Local results are established by monotonic reasoning from facts |
|
556 |
within a context. This allows common combinations of theorems, |
|
557 |
e.g.\ via \isa{{\isasymAnd}{\isacharslash}{\isasymLongrightarrow}} elimination, resolution rules, or equational |
|
558 |
reasoning, see \secref{sec:thms}. Unaccounted context manipulations |
|
559 |
should be avoided, notably raw \isa{{\isasymAnd}{\isacharslash}{\isasymLongrightarrow}} introduction or ad-hoc |
|
560 |
references to free variables or assumptions not present in the proof |
|
561 |
context. |
|
562 |
||
563 |
\medskip The \isa{SUBPROOF} combinator allows to structure a |
|
564 |
tactical proof recursively by decomposing a selected sub-goal: |
|
565 |
\isa{{\isacharparenleft}{\isasymAnd}x{\isachardot}\ A{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ B{\isacharparenleft}x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}} is turned into \isa{B{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}} |
|
566 |
after fixing \isa{x} and assuming \isa{A{\isacharparenleft}x{\isacharparenright}}. This means |
|
567 |
the tactic needs to solve the conclusion, but may use the premise as |
|
568 |
a local fact, for locally fixed variables. |
|
569 |
||
35001 | 570 |
The family of \isa{FOCUS} combinators is similar to \isa{SUBPROOF}, but allows to retain schematic variables and pending |
571 |
subgoals in the resulting goal state. |
|
572 |
||
30296 | 573 |
The \isa{prove} operation provides an interface for structured |
574 |
backwards reasoning under program control, with some explicit sanity |
|
575 |
checks of the result. The goal context can be augmented by |
|
576 |
additional fixed variables (cf.\ \secref{sec:variables}) and |
|
577 |
assumptions (cf.\ \secref{sec:assumptions}), which will be available |
|
578 |
as local facts during the proof and discharged into implications in |
|
579 |
the result. Type and term variables are generalized as usual, |
|
580 |
according to the context. |
|
581 |
||
582 |
The \isa{obtain} operation produces results by eliminating |
|
583 |
existing facts by means of a given tactic. This acts like a dual |
|
584 |
conclusion: the proof demonstrates that the context may be augmented |
|
35001 | 585 |
by parameters and assumptions, without affecting any conclusions |
586 |
that do not mention these parameters. See also |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
587 |
\cite{isabelle-isar-ref} for the user-level \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}} and |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
588 |
\hyperlink{command.guess}{\mbox{\isa{\isacommand{guess}}}} elements. Final results, which may not refer to |
30296 | 589 |
the parameters in the conclusion, need to exported explicitly into |
590 |
the original context.% |
|
591 |
\end{isamarkuptext}% |
|
592 |
\isamarkuptrue% |
|
593 |
% |
|
594 |
\isadelimmlref |
|
595 |
% |
|
596 |
\endisadelimmlref |
|
597 |
% |
|
598 |
\isatagmlref |
|
599 |
% |
|
600 |
\begin{isamarkuptext}% |
|
601 |
\begin{mldecls} |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
602 |
\indexdef{}{ML}{SUBPROOF}\verb|SUBPROOF: (Subgoal.focus -> tactic) ->|\isasep\isanewline% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
603 |
\verb| Proof.context -> int -> tactic| \\ |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
604 |
\indexdef{}{ML}{Subgoal.FOCUS}\verb|Subgoal.FOCUS: (Subgoal.focus -> tactic) ->|\isasep\isanewline% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
605 |
\verb| Proof.context -> int -> tactic| \\ |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
606 |
\indexdef{}{ML}{Subgoal.FOCUS\_PREMS}\verb|Subgoal.FOCUS_PREMS: (Subgoal.focus -> tactic) ->|\isasep\isanewline% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
607 |
\verb| Proof.context -> int -> tactic| \\ |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
608 |
\indexdef{}{ML}{Subgoal.FOCUS\_PARAMS}\verb|Subgoal.FOCUS_PARAMS: (Subgoal.focus -> tactic) ->|\isasep\isanewline% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
609 |
\verb| Proof.context -> int -> tactic| \\ |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
610 |
\indexdef{}{ML}{Subgoal.focus}\verb|Subgoal.focus: Proof.context -> int -> thm -> Subgoal.focus * thm| \\ |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
611 |
\indexdef{}{ML}{Subgoal.focus\_prems}\verb|Subgoal.focus_prems: Proof.context -> int -> thm -> Subgoal.focus * thm| \\ |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
612 |
\indexdef{}{ML}{Subgoal.focus\_params}\verb|Subgoal.focus_params: Proof.context -> int -> thm -> Subgoal.focus * thm| \\ |
30296 | 613 |
\end{mldecls} |
35001 | 614 |
|
30296 | 615 |
\begin{mldecls} |
616 |
\indexdef{}{ML}{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline% |
|
617 |
\verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\ |
|
618 |
\indexdef{}{ML}{Goal.prove\_multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline% |
|
619 |
\verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm list| \\ |
|
620 |
\end{mldecls} |
|
621 |
\begin{mldecls} |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
622 |
\indexdef{}{ML}{Obtain.result}\verb|Obtain.result: (Proof.context -> tactic) -> thm list ->|\isasep\isanewline% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
623 |
\verb| Proof.context -> ((string * cterm) list * thm list) * Proof.context| \\ |
30296 | 624 |
\end{mldecls} |
625 |
||
626 |
\begin{description} |
|
627 |
||
628 |
\item \verb|SUBPROOF|~\isa{tac\ ctxt\ i} decomposes the structure |
|
629 |
of the specified sub-goal, producing an extended context and a |
|
630 |
reduced goal, which needs to be solved by the given tactic. All |
|
631 |
schematic parameters of the goal are imported into the context as |
|
632 |
fixed ones, which may not be instantiated in the sub-proof. |
|
633 |
||
35001 | 634 |
\item \verb|Subgoal.FOCUS|, \verb|Subgoal.FOCUS_PREMS|, and \verb|Subgoal.FOCUS_PARAMS| are similar to \verb|SUBPROOF|, but are |
635 |
slightly more flexible: only the specified parts of the subgoal are |
|
636 |
imported into the context, and the body tactic may introduce new |
|
637 |
subgoals and schematic variables. |
|
638 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
639 |
\item \verb|Subgoal.focus|, \verb|Subgoal.focus_prems|, \verb|Subgoal.focus_params| extract the focus information from a goal |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
640 |
state in the same way as the corresponding tacticals above. This is |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
641 |
occasionally useful to experiment without writing actual tactics |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
642 |
yet. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
643 |
|
30296 | 644 |
\item \verb|Goal.prove|~\isa{ctxt\ xs\ As\ C\ tac} states goal \isa{C} in the context augmented by fixed variables \isa{xs} and |
645 |
assumptions \isa{As}, and applies tactic \isa{tac} to solve |
|
646 |
it. The latter may depend on the local assumptions being presented |
|
647 |
as facts. The result is in HHF normal form. |
|
648 |
||
649 |
\item \verb|Goal.prove_multi| is simular to \verb|Goal.prove|, but |
|
650 |
states several conclusions simultaneously. The goal is encoded by |
|
651 |
means of Pure conjunction; \verb|Goal.conjunction_tac| will turn this |
|
652 |
into a collection of individual subgoals. |
|
653 |
||
654 |
\item \verb|Obtain.result|~\isa{tac\ thms\ ctxt} eliminates the |
|
655 |
given facts using a tactic, which results in additional fixed |
|
656 |
variables and assumptions in the context. Final results need to be |
|
657 |
exported explicitly. |
|
658 |
||
659 |
\end{description}% |
|
660 |
\end{isamarkuptext}% |
|
661 |
\isamarkuptrue% |
|
662 |
% |
|
663 |
\endisatagmlref |
|
664 |
{\isafoldmlref}% |
|
665 |
% |
|
666 |
\isadelimmlref |
|
667 |
% |
|
668 |
\endisadelimmlref |
|
669 |
% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
670 |
\isadelimmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
671 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
672 |
\endisadelimmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
673 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
674 |
\isatagmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
675 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
676 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
677 |
The following minimal example illustrates how to access |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
678 |
the focus information of a structured goal state.% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
679 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
680 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
681 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
682 |
\endisatagmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
683 |
{\isafoldmlex}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
684 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
685 |
\isadelimmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
686 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
687 |
\endisadelimmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
688 |
\isacommand{example{\isacharunderscore}proof}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
689 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
690 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
691 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
692 |
\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
693 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
694 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
695 |
\isatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
696 |
\isacommand{fix}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
697 |
\ A\ B\ C\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
698 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
699 |
\ \ \isacommand{have}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
700 |
\ {\isachardoublequoteopen}{\isasymAnd}x{\isachardot}\ A\ x\ {\isasymLongrightarrow}\ B\ x\ {\isasymLongrightarrow}\ C\ x{\isachardoublequoteclose}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
701 |
\endisatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
702 |
{\isafoldproof}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
703 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
704 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
705 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
706 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
707 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
708 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
709 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
710 |
\ \ \ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
711 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
712 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
713 |
\isatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
714 |
\isacommand{ML{\isacharunderscore}val}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
715 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
716 |
\ \ \ \ {\isacharverbatimopen}\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
717 |
\ \ \ \ \ \ val\ {\isacharbraceleft}goal{\isacharcomma}\ context\ {\isacharequal}\ goal{\isacharunderscore}ctxt{\isacharcomma}\ {\isachardot}{\isachardot}{\isachardot}{\isacharbraceright}\ {\isacharequal}\ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
718 |
\isaantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
719 |
Isar{\isachardot}goal% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
720 |
\endisaantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
721 |
{\isacharsemicolon}\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
722 |
\ \ \ \ \ \ val\ {\isacharparenleft}focus\ as\ {\isacharbraceleft}params{\isacharcomma}\ asms{\isacharcomma}\ concl{\isacharcomma}\ {\isachardot}{\isachardot}{\isachardot}{\isacharbraceright}{\isacharcomma}\ goal{\isacharprime}{\isacharparenright}\ {\isacharequal}\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
723 |
\ \ \ \ \ \ \ \ Subgoal{\isachardot}focus\ goal{\isacharunderscore}ctxt\ {\isadigit{1}}\ goal{\isacharsemicolon}\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
724 |
\ \ \ \ \ \ val\ {\isacharbrackleft}A{\isacharcomma}\ B{\isacharbrackright}\ {\isacharequal}\ {\isacharhash}prems\ focus{\isacharsemicolon}\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
725 |
\ \ \ \ \ \ val\ {\isacharbrackleft}{\isacharparenleft}{\isacharunderscore}{\isacharcomma}\ x{\isacharparenright}{\isacharbrackright}\ {\isacharequal}\ {\isacharhash}params\ focus{\isacharsemicolon}\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
726 |
\ \ \ \ {\isacharverbatimclose}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
727 |
\endisatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
728 |
{\isafoldML}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
729 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
730 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
731 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
732 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
733 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
734 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
735 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
736 |
\ \ \ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
737 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
738 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
739 |
\isatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
740 |
\isacommand{oops}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
741 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
742 |
\endisatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
743 |
{\isafoldproof}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
744 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
745 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
746 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
747 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
748 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
749 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
750 |
\medskip The next example demonstrates forward-elimination in |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
751 |
a local context, using \verb|Obtain.result|.% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
752 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
753 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
754 |
\isacommand{example{\isacharunderscore}proof}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
755 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
756 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
757 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
758 |
\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
759 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
760 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
761 |
\isatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
762 |
\isacommand{assume}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
763 |
\ ex{\isacharcolon}\ {\isachardoublequoteopen}{\isasymexists}x{\isachardot}\ B\ x{\isachardoublequoteclose}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
764 |
\endisatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
765 |
{\isafoldproof}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
766 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
767 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
768 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
769 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
770 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
771 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
772 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
773 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
774 |
\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
775 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
776 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
777 |
\isatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
778 |
\isacommand{ML{\isacharunderscore}prf}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
779 |
\ {\isacharverbatimopen}\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
780 |
\ \ \ \ val\ ctxt{\isadigit{0}}\ {\isacharequal}\ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
781 |
\isaantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
782 |
context% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
783 |
\endisaantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
784 |
{\isacharsemicolon}\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
785 |
\ \ \ \ val\ {\isacharparenleft}{\isacharparenleft}{\isacharbrackleft}{\isacharparenleft}{\isacharunderscore}{\isacharcomma}\ x{\isacharparenright}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}B{\isacharbrackright}{\isacharparenright}{\isacharcomma}\ ctxt{\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ ctxt{\isadigit{0}}\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
786 |
\ \ \ \ \ \ {\isacharbar}{\isachargreater}\ Obtain{\isachardot}result\ {\isacharparenleft}fn\ {\isacharunderscore}\ {\isacharequal}{\isachargreater}\ etac\ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
787 |
\isaantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
788 |
thm\ exE% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
789 |
\endisaantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
790 |
\ {\isadigit{1}}{\isacharparenright}\ {\isacharbrackleft}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
791 |
\isaantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
792 |
thm\ ex% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
793 |
\endisaantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
794 |
{\isacharbrackright}{\isacharsemicolon}\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
795 |
\ \ {\isacharverbatimclose}\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
796 |
\ \ \isacommand{ML{\isacharunderscore}prf}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
797 |
\ {\isacharverbatimopen}\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
798 |
\ \ \ \ singleton\ {\isacharparenleft}ProofContext{\isachardot}export\ ctxt{\isadigit{1}}\ ctxt{\isadigit{0}}{\isacharparenright}\ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
799 |
\isaantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
800 |
thm\ refl% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
801 |
\endisaantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
802 |
{\isacharsemicolon}\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
803 |
\ \ {\isacharverbatimclose}\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
804 |
\ \ \isacommand{ML{\isacharunderscore}prf}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
805 |
\ {\isacharverbatimopen}\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
806 |
\ \ \ \ ProofContext{\isachardot}export\ ctxt{\isadigit{1}}\ ctxt{\isadigit{0}}\ {\isacharbrackleft}Thm{\isachardot}reflexive\ x{\isacharbrackright}\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
807 |
\ \ \ \ \ \ handle\ ERROR\ msg\ {\isacharequal}{\isachargreater}\ {\isacharparenleft}warning\ msg{\isacharsemicolon}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharsemicolon}\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
808 |
\ \ {\isacharverbatimclose}\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
809 |
\isacommand{qed}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
810 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
811 |
\endisatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
812 |
{\isafoldML}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
813 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
814 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
815 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
816 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
817 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
818 |
% |
30296 | 819 |
\isadelimtheory |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
820 |
\isanewline |
30296 | 821 |
% |
822 |
\endisadelimtheory |
|
823 |
% |
|
824 |
\isatagtheory |
|
825 |
\isacommand{end}\isamarkupfalse% |
|
826 |
% |
|
827 |
\endisatagtheory |
|
828 |
{\isafoldtheory}% |
|
829 |
% |
|
830 |
\isadelimtheory |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
831 |
\isanewline |
30296 | 832 |
% |
833 |
\endisadelimtheory |
|
834 |
\end{isabellebody}% |
|
835 |
%%% Local Variables: |
|
836 |
%%% mode: latex |
|
837 |
%%% TeX-master: "root" |
|
838 |
%%% End: |