104 \isamarkupsection{Assumptions% |
104 \isamarkupsection{Assumptions% |
105 } |
105 } |
106 \isamarkuptrue% |
106 \isamarkuptrue% |
107 % |
107 % |
108 \begin{isamarkuptext}% |
108 \begin{isamarkuptext}% |
109 FIXME% |
109 An \emph{assumption} is a proposition that it is postulated in the |
110 \end{isamarkuptext}% |
110 current context. Local conclusions may use assumptions as |
111 \isamarkuptrue% |
111 additional facts, but this imposes implicit hypotheses that weaken |
|
112 the overall statement. |
|
113 |
|
114 Assumptions are restricted to fixed non-schematic statements, all |
|
115 generality needs to be expressed by explicit quantifiers. |
|
116 Nevertheless, the result will be in HHF normal form with outermost |
|
117 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 arbitrary \isa{{\isacharquery}x} |
|
118 of the fixed type \isa{{\isasymalpha}}. Local derivations accumulate more |
|
119 and 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 |
|
120 be covered by the assumptions of the current context. |
|
121 |
|
122 \medskip The \isa{add{\isacharunderscore}assm} operation augments the context by |
|
123 local assumptions, parameterized by an \isa{export} rule (see |
|
124 below). |
|
125 |
|
126 The \isa{export} operation moves facts from a (larger) inner |
|
127 context into a (smaller) outer context, by discharging the |
|
128 difference of the assumptions as specified by the associated export |
|
129 rules. Note that the discharged portion is determined by the |
|
130 contexts, not the facts being exported! There is a separate flag to |
|
131 indicate a goal context, where the result is meant to refine an |
|
132 enclosing sub-goal of a structured proof state (cf.\ FIXME). |
|
133 |
|
134 \medskip The most basic export rule discharges assumptions directly |
|
135 by means of the \isa{{\isasymLongrightarrow}} introduction rule: |
|
136 \[ |
|
137 \infer[(\isa{{\isasymLongrightarrow}{\isacharunderscore}intro})]{\isa{{\isasymGamma}\ {\isacharbackslash}\ A\ {\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}} |
|
138 \] |
|
139 |
|
140 The variant for goal refinements marks the newly introduced |
|
141 premises, which causes the builtin goal refinement scheme of Isar to |
|
142 enforce unification with local premises within the goal: |
|
143 \[ |
|
144 \infer[(\isa{{\isacharhash}{\isasymLongrightarrow}{\isacharunderscore}intro})]{\isa{{\isasymGamma}\ {\isacharbackslash}\ A\ {\isasymturnstile}\ {\isacharhash}A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}} |
|
145 \] |
|
146 |
|
147 \medskip Alternative versions of assumptions may perform arbitrary |
|
148 transformations as long as a particular portion of hypotheses is |
|
149 removed from the given facts. |
|
150 |
|
151 For example, a local definition works by fixing \isa{x} and |
|
152 assuming \isa{x\ {\isasymequiv}\ t}, with the following export rule to reverse |
|
153 the effect: |
|
154 \[ |
|
155 \infer{\isa{{\isasymGamma}\ {\isacharbackslash}\ x\ {\isasymequiv}\ t\ {\isasymturnstile}\ B\ t}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B\ x}} |
|
156 \] |
|
157 |
|
158 \medskip The general concept supports block-structured reasoning |
|
159 nicely, with arbitrary mechanisms for introducing local assumptions. |
|
160 The common reasoning pattern is as follows: |
|
161 |
|
162 \medskip |
|
163 \begin{tabular}{l} |
|
164 \isa{add{\isacharunderscore}assm\ e\isactrlisub {\isadigit{1}}\ A\isactrlisub {\isadigit{1}}} \\ |
|
165 \isa{{\isasymdots}} \\ |
|
166 \isa{add{\isacharunderscore}assm\ e\isactrlisub n\ A\isactrlisub n} \\ |
|
167 \isa{export} \\ |
|
168 \end{tabular} |
|
169 \medskip |
|
170 |
|
171 \noindent The final \isa{export} will turn any fact \isa{A\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n\ {\isasymturnstile}\ B} into some \isa{{\isasymturnstile}\ B{\isacharprime}}, by |
|
172 applying the export rules \isa{e\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ e\isactrlisub n} |
|
173 inside-out.% |
|
174 \end{isamarkuptext}% |
|
175 \isamarkuptrue% |
|
176 % |
|
177 \isadelimmlref |
|
178 % |
|
179 \endisadelimmlref |
|
180 % |
|
181 \isatagmlref |
|
182 % |
|
183 \begin{isamarkuptext}% |
|
184 \begin{mldecls} |
|
185 \indexmltype{Assumption.export}\verb|type Assumption.export| \\ |
|
186 \indexml{Assumption.assume}\verb|Assumption.assume: cterm -> thm| \\ |
|
187 \indexml{Assumption.add-assumes}\verb|Assumption.add_assumes: cterm list -> Proof.context -> thm list * Proof.context| \\ |
|
188 \indexml{Assumption.add-assms}\verb|Assumption.add_assms: Assumption.export -> cterm list -> Proof.context -> thm list * Proof.context| \\ |
|
189 \indexml{Assumption.export}\verb|Assumption.export: bool -> Proof.context -> Proof.context -> thm -> thm| \\ |
|
190 \end{mldecls} |
|
191 |
|
192 \begin{description} |
|
193 |
|
194 \item \verb|Assumption.export| |
|
195 |
|
196 \item \verb|Assumption.assume|~\isa{A} produces a raw assumption |
|
197 \isa{A\ {\isasymturnstile}\ A{\isacharprime}}, where the conclusion \isa{A{\isacharprime}} is in HHF normal |
|
198 form. |
|
199 |
|
200 \item \verb|Assumption.add_assumes|~\isa{As} augments the context |
|
201 by plain assumptions that are discharged via \isa{{\isasymLongrightarrow}{\isacharunderscore}intro} or |
|
202 \isa{{\isacharhash}{\isasymLongrightarrow}{\isacharunderscore}intro}, depending on goal mode. The resulting facts are |
|
203 hypothetical theorems as produced by \verb|Assumption.assume|. |
|
204 |
|
205 \item \verb|Assumption.add_assms|~\isa{e\ As} augments the context |
|
206 by generic assumptions that are discharged via rule \isa{e}. |
|
207 |
|
208 \item \verb|Assumption.export|~\isa{is{\isacharunderscore}goal\ inner\ outer\ th} |
|
209 exports result \isa{th} from the the \isa{inner} context |
|
210 back into the \isa{outer} one. The \isa{is{\isacharunderscore}goal} flag is |
|
211 \isa{true} for goal mode. The result is in HHF normal form. |
|
212 |
|
213 \end{description}% |
|
214 \end{isamarkuptext}% |
|
215 \isamarkuptrue% |
|
216 % |
|
217 \endisatagmlref |
|
218 {\isafoldmlref}% |
|
219 % |
|
220 \isadelimmlref |
|
221 % |
|
222 \endisadelimmlref |
112 % |
223 % |
113 \isamarkupsection{Conclusions% |
224 \isamarkupsection{Conclusions% |
114 } |
225 } |
115 \isamarkuptrue% |
226 \isamarkuptrue% |
116 % |
227 % |