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 


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


92 


93 
text \<open>


94 
The following improper proof methods emulate traditional tactics.


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


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


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


98 
scope of some subgoal.


99 


100 
\begin{warn}


101 
Dynamic instantiations refer to universally quantified parameters


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


103 
term abbreviations of a (static) Isar context.


104 
\end{warn}


105 


106 
Tactic emulation methods, unlike their ML counterparts, admit


107 
simultaneous instantiation from both dynamic and static contexts.


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


109 
variables. Likewise, schematic variables refer to term


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


111 
schematic variable is interpreted as a schematic variable and left


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


113 


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


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


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


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


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


119 
\secref{sec:puremethatt}).


120 


121 
\begin{matharray}{rcl}


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


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


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


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


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


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


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


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


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


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


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


133 
\end{matharray}


134 


135 
@{rail \<open>


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


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


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


139 
;


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


141 
;


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


143 
;


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


145 
;


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


147 
;


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


149 
\<close>}


150 


151 
\begin{description}


152 


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


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


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


156 


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


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


159 
@{cite "isabelleimplementation"}).


160 


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


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


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


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


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


166 
closed rule statements.


167 


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


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


170 
variables, to abbreviate the intended proposition; the first


171 
matching subgoal premise will be deleted. Removing useless premises


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


173 
run faster.


174 


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


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


177 
as new subgoals (in the original context).


178 


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


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


181 
\emph{suffix} of variables.


182 


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


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


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


186 
default value is 1.


187 


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


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


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


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


192 
current facts used for forwardchaining.


193 


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


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


196 
subgoals appear as conjunction of the logical framework instead of


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


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


199 
appear in production theories.


200 


201 
\end{description}


202 
\<close>


203 


204 
end 