60484

1 
theory Proof_Script


2 
imports Base Main


3 
begin


4 


5 
chapter \<open>Proof scripts\<close>


6 


7 
text \<open>


8 
Interactive theorem proving is traditionally associated with ``proof


9 
scripts'', but Isabelle/Isar is centered around structured \emph{proof


10 
documents} instead (see also \chref{ch:proofs}).


11 


12 
Nonetheless, it is possible to emulate proof scripts by sequential


13 
refinements of a proof state in backwards mode, notably with the @{command


14 
apply} command (see \secref{sec:tacticcommands}). There are also various


15 
proof methods that allow to refer to implicit goal state information that


16 
is normally not accessible to structured Isar proofs (see


17 
\secref{sec:tactics}).


18 
\<close>


19 


20 


21 
section \<open>Commands for stepwise refinement \label{sec:tacticcommands}\<close>


22 


23 
text \<open>


24 
\begin{matharray}{rcl}


25 
@{command_def "supply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\


26 
@{command_def "apply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\


27 
@{command_def "apply_end"}@{text "\<^sup>*"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\


28 
@{command_def "done"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(state)  local_theory  theory"} \\


29 
@{command_def "defer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\


30 
@{command_def "prefer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\


31 
@{command_def "back"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\


32 
\end{matharray}


33 


34 
@{rail \<open>


35 
@@{command supply} (@{syntax thmdef}? @{syntax thmrefs} + @'and')


36 
;


37 
( @@{command apply}  @@{command apply_end} ) @{syntax method}


38 
;


39 
@@{command defer} @{syntax nat}?


40 
;


41 
@@{command prefer} @{syntax nat}


42 
\<close>}


43 


44 
\begin{description}


45 


46 
\item @{command "supply"} supports fact definitions during goal


47 
refinement: it is similar to @{command "note"}, but it operates in


48 
backwards mode and does not have any impact on chained facts.


49 


50 
\item @{command "apply"}~@{text m} applies proof method @{text m} in


51 
initial position, but unlike @{command "proof"} it retains ``@{text


52 
"proof(prove)"}'' mode. Thus consecutive method applications may be


53 
given just as in tactic scripts.


54 


55 
Facts are passed to @{text m} as indicated by the goal's


56 
forwardchain mode, and are \emph{consumed} afterwards. Thus any


57 
further @{command "apply"} command would always work in a purely


58 
backward manner.


59 


60 
\item @{command "apply_end"}~@{text "m"} applies proof method @{text


61 
m} as if in terminal position. Basically, this simulates a


62 
multistep tactic script for @{command "qed"}, but may be given


63 
anywhere within the proof body.


64 


65 
No facts are passed to @{text m} here. Furthermore, the static


66 
context is that of the enclosing goal (as for actual @{command


67 
"qed"}). Thus the proof method may not refer to any assumptions


68 
introduced in the current body, for example.


69 


70 
\item @{command "done"} completes a proof script, provided that the


71 
current goal state is solved completely. Note that actual


72 
structured proof commands (e.g.\ ``@{command "."}'' or @{command


73 
"sorry"}) may be used to conclude proof scripts as well.


74 


75 
\item @{command "defer"}~@{text n} and @{command "prefer"}~@{text n}


76 
shuffle the list of pending goals: @{command "defer"} puts off


77 
subgoal @{text n} to the end of the list (@{text "n = 1"} by


78 
default), while @{command "prefer"} brings subgoal @{text n} to the


79 
front.


80 


81 
\item @{command "back"} does backtracking over the result sequence


82 
of the latest proof command. Any proof command may return multiple


83 
results, and this command explores the possibilities stepbystep.


84 
It is mainly useful for experimentation and interactive exploration,


85 
and should be avoided in finished proofs.


86 


87 
\end{description}


88 
\<close>


89 


90 

60631

91 
section \<open>Explicit subgoal structure\<close>


92 


93 
text \<open>


94 
\begin{matharray}{rcl}


95 
@{command_def "subgoal"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\


96 
\end{matharray}


97 


98 
@{rail \<open>


99 
@@{command subgoal} @{syntax thmbind}? prems? params?


100 
;


101 
prems: @'premises' @{syntax thmbind}?


102 
;


103 
params: @'for' '\<dots>'? (('_'  @{syntax name})+)


104 
\<close>}


105 


106 
\begin{description}


107 


108 
\item @{command "subgoal"} allows to impose some structure on backward


109 
refinements, to avoid proof scripts degenerating into long of @{command


110 
apply} sequences.


111 


112 
The current goal state, which is essentially a hidden part of the Isar/VM


113 
configurtation, is turned into a proof context and remaining conclusion.


114 
This correponds to @{command fix}~/ @{command assume}~/ @{command show} in


115 
structured proofs, but the text of the parameters, premises and conclusion


116 
is not given explicitly.


117 


118 
Goal parameters may be specified separately, in order to allow referring


119 
to them in the proof body: ``@{command subgoal}~@{keyword "for"}~@{text "x


120 
y z"}'' names a \emph{prefix}, and ``@{command subgoal}~@{keyword


121 
"for"}~@{text "\<dots> x y z"}'' names a \emph{suffix} of goal parameters. The


122 
latter uses a literal @{verbatim "\<dots>"} symbol as notation. Parameter


123 
positions may be skipped via dummies (underscore). Unspecified names


124 
remain internal, and thus inaccessible in the proof text.


125 


126 
``@{command subgoal}~@{keyword "premises"}~@{text prems}'' indicates that


127 
goal premises should be turned into assumptions of the context (otherwise


128 
the remaining conclusion is a Pure implication). The fact name and


129 
attributes are optional; the particular name ``@{text prems}'' is a common


130 
convention for the premises of an arbitrary goal context in proof scripts.


131 


132 
``@{command subgoal}~@{text result}'' indicates a fact name for the result


133 
of a proven subgoal. Thus it may be reused in further reasoning, similar


134 
to the result of @{command show} in structured Isar proofs.


135 


136 
\end{description}


137 


138 
Here are some abstract examples:


139 
\<close>


140 


141 
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"


142 
and "\<And>u v. X u \<Longrightarrow> Y v"


143 
subgoal sorry


144 
subgoal sorry


145 
done


146 


147 
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"


148 
and "\<And>u v. X u \<Longrightarrow> Y v"


149 
subgoal for x y z sorry


150 
subgoal for u v sorry


151 
done


152 


153 
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"


154 
and "\<And>u v. X u \<Longrightarrow> Y v"


155 
subgoal premises for x y z


156 
using \<open>A x\<close> \<open>B y\<close>


157 
sorry


158 
subgoal premises for u v


159 
using \<open>X u\<close>


160 
sorry


161 
done


162 


163 
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"


164 
and "\<And>u v. X u \<Longrightarrow> Y v"


165 
subgoal r premises prems for x y z


166 
proof 


167 
have "A x" by (fact prems)


168 
moreover have "B y" by (fact prems)


169 
ultimately show ?thesis sorry


170 
qed


171 
subgoal premises prems for u v


172 
proof 


173 
have "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z" by (fact r)


174 
moreover


175 
have "X u" by (fact prems)


176 
ultimately show ?thesis sorry


177 
qed


178 
done


179 


180 
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"


181 
subgoal premises prems for \<dots> z


182 
proof 


183 
from prems show "C z" sorry


184 
qed


185 
done


186 


187 

60484

188 
section \<open>Tactics: improper proof methods \label{sec:tactics}\<close>


189 


190 
text \<open>


191 
The following improper proof methods emulate traditional tactics.


192 
These admit direct access to the goal state, which is normally


193 
considered harmful! In particular, this may involve both numbered


194 
goal addressing (default 1), and dynamic instantiation within the


195 
scope of some subgoal.


196 


197 
\begin{warn}


198 
Dynamic instantiations refer to universally quantified parameters


199 
of a subgoal (the dynamic context) rather than fixed variables and


200 
term abbreviations of a (static) Isar context.


201 
\end{warn}


202 


203 
Tactic emulation methods, unlike their ML counterparts, admit


204 
simultaneous instantiation from both dynamic and static contexts.


205 
If names occur in both contexts goal parameters hide locally fixed


206 
variables. Likewise, schematic variables refer to term


207 
abbreviations, if present in the static context. Otherwise the


208 
schematic variable is interpreted as a schematic variable and left


209 
to be solved by unification with certain parts of the subgoal.


210 


211 
Note that the tactic emulation proof methods in Isabelle/Isar are


212 
consistently named @{text foo_tac}. Note also that variable names


213 
occurring on left hand sides of instantiations must be preceded by a


214 
question mark if they coincide with a keyword or contain dots. This


215 
is consistent with the attribute @{attribute "where"} (see


216 
\secref{sec:puremethatt}).


217 


218 
\begin{matharray}{rcl}


219 
@{method_def rule_tac}@{text "\<^sup>*"} & : & @{text method} \\


220 
@{method_def erule_tac}@{text "\<^sup>*"} & : & @{text method} \\


221 
@{method_def drule_tac}@{text "\<^sup>*"} & : & @{text method} \\


222 
@{method_def frule_tac}@{text "\<^sup>*"} & : & @{text method} \\


223 
@{method_def cut_tac}@{text "\<^sup>*"} & : & @{text method} \\


224 
@{method_def thin_tac}@{text "\<^sup>*"} & : & @{text method} \\


225 
@{method_def subgoal_tac}@{text "\<^sup>*"} & : & @{text method} \\


226 
@{method_def rename_tac}@{text "\<^sup>*"} & : & @{text method} \\


227 
@{method_def rotate_tac}@{text "\<^sup>*"} & : & @{text method} \\


228 
@{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\


229 
@{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\


230 
\end{matharray}


231 


232 
@{rail \<open>


233 
(@@{method rule_tac}  @@{method erule_tac}  @@{method drule_tac} 


234 
@@{method frule_tac}  @@{method cut_tac}) @{syntax goal_spec}? \<newline>


235 
(@{syntax named_insts} @{syntax for_fixes} @'in' @{syntax thmref}  @{syntax thmrefs} )


236 
;


237 
@@{method thin_tac} @{syntax goal_spec}? @{syntax prop} @{syntax for_fixes}


238 
;


239 
@@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +) @{syntax for_fixes}


240 
;


241 
@@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +)


242 
;


243 
@@{method rotate_tac} @{syntax goal_spec}? @{syntax int}?


244 
;


245 
(@@{method tactic}  @@{method raw_tactic}) @{syntax text}


246 
\<close>}


247 


248 
\begin{description}


249 


250 
\item @{method rule_tac} etc. do resolution of rules with explicit


251 
instantiation. This works the same way as the ML tactics @{ML


252 
Rule_Insts.res_inst_tac} etc.\ (see @{cite "isabelleimplementation"}).


253 


254 
Multiple rules may be only given if there is no instantiation; then


255 
@{method rule_tac} is the same as @{ML resolve_tac} in ML (see


256 
@{cite "isabelleimplementation"}).


257 


258 
\item @{method cut_tac} inserts facts into the proof state as


259 
assumption of a subgoal; instantiations may be given as well. Note


260 
that the scope of schematic variables is spread over the main goal


261 
statement and rule premises are turned into new subgoals. This is


262 
in contrast to the regular method @{method insert} which inserts


263 
closed rule statements.


264 


265 
\item @{method thin_tac}~@{text \<phi>} deletes the specified premise


266 
from a subgoal. Note that @{text \<phi>} may contain schematic


267 
variables, to abbreviate the intended proposition; the first


268 
matching subgoal premise will be deleted. Removing useless premises


269 
from a subgoal increases its readability and can make search tactics


270 
run faster.


271 


272 
\item @{method subgoal_tac}~@{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} adds the propositions


273 
@{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} as local premises to a subgoal, and poses the same


274 
as new subgoals (in the original context).


275 


276 
\item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a


277 
goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the


278 
\emph{suffix} of variables.


279 


280 
\item @{method rotate_tac}~@{text n} rotates the premises of a


281 
subgoal by @{text n} positions: from right to left if @{text n} is


282 
positive, and from left to right if @{text n} is negative; the


283 
default value is 1.


284 


285 
\item @{method tactic}~@{text "text"} produces a proof method from


286 
any ML text of type @{ML_type tactic}. Apart from the usual ML


287 
environment and the current proof context, the ML code may refer to


288 
the locally bound values @{ML_text facts}, which indicates any


289 
current facts used for forwardchaining.


290 


291 
\item @{method raw_tactic} is similar to @{method tactic}, but


292 
presents the goal state in its raw internal form, where simultaneous


293 
subgoals appear as conjunction of the logical framework instead of


294 
the usual split into several subgoals. While feature this is useful


295 
for debugging of complex method definitions, it should not never


296 
appear in production theories.


297 


298 
\end{description}


299 
\<close>


300 


301 
end 