934 tactical proof within new-style theories (to benefit from document |
931 tactical proof within new-style theories (to benefit from document |
935 preparation, for example). |
932 preparation, for example). |
936 |
933 |
937 \indexisarcmd{apply}\indexisarcmd{apply-end} |
934 \indexisarcmd{apply}\indexisarcmd{apply-end} |
938 \indexisarcmd{defer}\indexisarcmd{prefer}\indexisarcmd{back} |
935 \indexisarcmd{defer}\indexisarcmd{prefer}\indexisarcmd{back} |
939 \indexisarmeth{tactic} |
936 \indexisarmeth{tactic}\indexisarmeth{insert} |
940 \indexisarmeth{res-inst-tac}\indexisarmeth{eres-inst-tac} |
937 \indexisarmeth{res-inst-tac}\indexisarmeth{eres-inst-tac} |
941 \indexisarmeth{dres-inst-tac}\indexisarmeth{forw-inst-tac} |
938 \indexisarmeth{dres-inst-tac}\indexisarmeth{forw-inst-tac} |
942 \indexisarmeth{subgoal-tac} |
939 \indexisarmeth{subgoal-tac} |
943 \begin{matharray}{rcl} |
940 \begin{matharray}{rcl} |
944 \isarcmd{apply}^* & : & \isartrans{proof(prove)}{proof(prove)} \\ |
941 \isarcmd{apply}^* & : & \isartrans{proof(prove)}{proof(prove)} \\ |
945 \isarcmd{apply_end}^* & : & \isartrans{proof(state)}{proof(state)} \\ |
942 \isarcmd{apply_end}^* & : & \isartrans{proof(state)}{proof(state)} \\ |
946 \isarcmd{defer}^* & : & \isartrans{proof}{proof} \\ |
943 \isarcmd{defer}^* & : & \isartrans{proof}{proof} \\ |
947 \isarcmd{prefer}^* & : & \isartrans{proof}{proof} \\ |
944 \isarcmd{prefer}^* & : & \isartrans{proof}{proof} \\ |
948 \isarcmd{back}^* & : & \isartrans{proof}{proof} \\ |
945 \isarcmd{back}^* & : & \isartrans{proof}{proof} \\ |
949 tactic^* & : & \isarmeth \\ |
946 tactic^* & : & \isarmeth \\ |
|
947 insert^* & : & \isarmeth \\ |
950 res_inst_tac^* & : & \isarmeth \\ |
948 res_inst_tac^* & : & \isarmeth \\ |
951 eres_inst_tac^* & : & \isarmeth \\ |
949 eres_inst_tac^* & : & \isarmeth \\ |
952 dres_inst_tac^* & : & \isarmeth \\ |
950 dres_inst_tac^* & : & \isarmeth \\ |
953 forw_inst_tac^* & : & \isarmeth \\ |
951 forw_inst_tac^* & : & \isarmeth \\ |
954 subgoal_tac^* & : & \isarmeth \\ |
952 subgoal_tac^* & : & \isarmeth \\ |
1026 \end{verbatim}} |
1026 \end{verbatim}} |
1027 Here \texttt{ctxt} refers to the current proof context, \texttt{facts} |
1027 Here \texttt{ctxt} refers to the current proof context, \texttt{facts} |
1028 indicates any current facts for forward-chaining, and |
1028 indicates any current facts for forward-chaining, and |
1029 \texttt{thm}~/~\texttt{thms} retrieve named facts (including global |
1029 \texttt{thm}~/~\texttt{thms} retrieve named facts (including global |
1030 theorems) from the context. |
1030 theorems) from the context. |
|
1031 \item [$insert~\vec a$] inserts theorems as facts into the proof state; the |
|
1032 current facts indicated for forward chaining are ignored! |
1031 \item [$res_inst_tac$ etc.] do resolution of rules with explicit |
1033 \item [$res_inst_tac$ etc.] do resolution of rules with explicit |
1032 instantiation. This works the same way as the corresponding ML tactics, see |
1034 instantiation. This works the same way as the corresponding ML tactics, see |
1033 \cite[\S3]{isabelle-ref}. |
1035 \cite[\S3]{isabelle-ref}. |
1034 |
1036 |
1035 It is very important to note that the instantiations are read and |
1037 It is very important to note that the instantiations are read and |