Mercurial Mercurial > hg > isabelle-cookbook / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ProgTutorial/Tactical.thy
changeset 318 efb5fff99c96
parent 316 74f0a06f751f
child 329 5dffcab68680
equal deleted inserted replaced
317:d69214e47ef9 318:efb5fff99c96 
    47       THEN atac 1
 
    47       THEN atac 1
 
    48       THEN rtac @{thm disjI1} 1
 
    48       THEN rtac @{thm disjI1} 1
 
    49       THEN atac 1)
 
    49       THEN atac 1)
 
    50 end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P"}
 
    50 end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P"}
 
    51   
    51   
    52   To start the proof, the function @{ML "Goal.prove"}~@{text "ctxt xs As C
 
    52   To start the proof, the function @{ML_ind "Goal.prove"}~@{text "ctxt xs As C
 
    53   tac"} sets up a goal state for proving the goal @{text C} 
    53   tac"} sets up a goal state for proving the goal @{text C} (that is @{prop "P
 
    54   (that is @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"} in the proof at hand) under the
 
    54   \<or> Q \<Longrightarrow> Q \<or> P"} in the proof at hand) under the assumptions @{text As}
 
    55   assumptions @{text As} (happens to be empty) with the variables
 
    55   (happens to be empty) with the variables @{text xs} that will be generalised
 
    56   @{text xs} that will be generalised once the goal is proved (in our case
 
    56   once the goal is proved (in our case @{text P} and @{text
 
    57   @{text P} and @{text Q}). The @{text "tac"} is the tactic that proves the goal;
 
    57   Q}).\footnote{FIXME: explain prove earlier} The @{text "tac"} is the tactic
 
    58   it can make use of the local assumptions (there are none in this example). 
    58   that proves the goal; it can make use of the local assumptions (there are
 
    59   The tactics @{ML_ind  etac}, @{ML_ind  rtac} and @{ML_ind  atac} 
    59   none in this example). The tactics @{ML_ind etac}, @{ML_ind rtac} and
 
    60   in the code above correspond 
    60   @{ML_ind atac} in the code above correspond roughly to @{text erule}, @{text
 
    61   roughly to @{text erule}, @{text rule} and @{text assumption}, respectively. 
    61   rule} and @{text assumption}, respectively. The operator @{ML_ind THEN}
 
    62   The operator @{ML_ind  THEN} strings the tactics together. 
    62   strings the tactics together.
 
    63 
    63 
    64   \begin{readmore}
 
    64   \begin{readmore}
 
    65   To learn more about the function @{ML_ind  prove in Goal} see \isccite{sec:results}
 
    65   To learn more about the function @{ML_ind prove in Goal} see
 
    66   and the file @{ML_file "Pure/goal.ML"}.  See @{ML_file
 
    66   \isccite{sec:results} and the file @{ML_file "Pure/goal.ML"}.  See @{ML_file
 
    67   "Pure/tactic.ML"} and @{ML_file "Pure/tactical.ML"} for the code of basic
 
    67   "Pure/tactic.ML"} and @{ML_file "Pure/tactical.ML"} for the code of basic
 
    68   tactics and tactic combinators; see also Chapters 3 and 4 in the old
 
    68   tactics and tactic combinators; see also Chapters 3 and 4 in the old
 
    69   Isabelle Reference Manual, and Chapter 3 in the Isabelle/Isar Implementation Manual. 
    69   Isabelle Reference Manual, and Chapter 3 in the Isabelle/Isar Implementation
 
       
    70   Manual.
 
    70   \end{readmore}
 
    71   \end{readmore}
 
    71 
    72 
    72   Note that in the code above we use antiquotations for referencing the theorems. Many theorems
 
    73   Note that in the code above we use antiquotations for referencing the
 
    73   also have ML-bindings with the same name. Therefore, we could also just have
 
    74   theorems. Many theorems also have ML-bindings with the same name. Therefore,
 
    74   written @{ML "etac disjE 1"}, or in case where there is no ML-binding obtain
 
    75   we could also just have written @{ML "etac disjE 1"}, or in case where there
 
    75   the theorem dynamically using the function @{ML thm}; for example 
    76   is no ML-binding obtain the theorem dynamically using the function @{ML
 
    76   \mbox{@{ML  "etac (thm \"disjE\") 1"}}. Both ways however are considered bad style! 
    77   thm}; for example \mbox{@{ML "etac (thm \"disjE\") 1"}}. Both ways however
 
    77   The reason
 
    78   are considered bad style! The reason is that the binding for @{ML disjE} can
 
    78   is that the binding for @{ML disjE} can be re-assigned by the user and thus
 
    79   be re-assigned by the user and thus one does not have complete control over
 
    79   one does not have complete control over which theorem is actually
 
    80   which theorem is actually applied. This problem is nicely prevented by using
 
    80   applied. This problem is nicely prevented by using antiquotations, because
 
    81   antiquotations, because then the theorems are fixed statically at
 
    81   then the theorems are fixed statically at compile-time.
 
    82   compile-time.
 
    82 
    83 
    83   During the development of automatic proof procedures, you will often find it 
    84   During the development of automatic proof procedures, you will often find it
 
    84   necessary to test a tactic on examples. This can be conveniently 
    85   necessary to test a tactic on examples. This can be conveniently done with
 
    85   done with the command \isacommand{apply}@{text "(tactic \<verbopen> \<dots> \<verbclose>)"}. 
    86   the command \isacommand{apply}@{text "(tactic \<verbopen> \<dots> \<verbclose>)"}. 
    86   Consider the following sequence of tactics
 
    87   Consider the following sequence of tactics
 
       
    88 
    87 *}
 
    89 *}
 
    88 
    90 
    89 ML{*val foo_tac = 
    91 ML{*val foo_tac = 
    90       (etac @{thm disjE} 1
 
    92       (etac @{thm disjE} 1
 
    91        THEN rtac @{thm disjI2} 1
 
    93        THEN rtac @{thm disjI2} 1
 
   300   @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> #(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}; when you finish the proof the
 
   302   @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> #(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}; when you finish the proof the
 
   301   theorem is @{text "#(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}.\label{fig:goalstates}}
 
   303   theorem is @{text "#(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}.\label{fig:goalstates}}
 
   302   \end{figure}
 
   304   \end{figure}
 
   303 *}
 
   305 *}
 
   304 
   306 
   305 
       
   306 text {*
 
   307 text {*
 
   307   which prints out the given theorem (using the string-function defined in
 
   308   which prints out the given theorem (using the string-function defined in
 
   308   Section~\ref{sec:printing}) and then behaves like @{ML all_tac}. With this
 
   309   Section~\ref{sec:printing}) and then behaves like @{ML all_tac}. With this
 
   309   tactic we are in the position to inspect every goal state in a
 
   310   tactic we are in the position to inspect every goal state in a
 
   310   proof. Consider now the proof in Figure~\ref{fig:goalstates}: as can be seen, 
   311   proof. Consider now the proof in Figure~\ref{fig:goalstates}: as can be seen, 
   313   @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> #C"}
 
   314   @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> #C"}
 
   314 
   315 
   315   where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are
 
   316   where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are
 
   316   the subgoals. So after setting up the lemma, the goal state is always of the
 
   317   the subgoals. So after setting up the lemma, the goal state is always of the
 
   317   form @{text "C \<Longrightarrow> #C"}; when the proof is finished we are left with @{text
 
   318   form @{text "C \<Longrightarrow> #C"}; when the proof is finished we are left with @{text
 
   318   "#C"}.\footnote{This only applies to single statements. If the lemma
 
   319   "#C"}. Since the goal @{term C} can potentially be an implication, there is a
 
   319   contains more than one statement, then one has more such implications.} 
       
   320   Since the goal @{term C} can potentially be an implication, there is a
 
       
   321   ``protector'' wrapped around it (the wrapper is the outermost constant
 
   320   ``protector'' wrapped around it (the wrapper is the outermost constant
 
   322   @{text "Const (\"prop\", bool \<Rightarrow> bool)"}; in the figure we make it visible
 
   321   @{text "Const (\"prop\", bool \<Rightarrow> bool)"}; in the figure we make it visible
 
   323   as an @{text #}). This wrapper prevents that premises of @{text C} are
 
   322   as an @{text #}). This wrapper prevents that premises of @{text C} are
 
   324   misinterpreted as open subgoals. While tactics can operate on the subgoals
 
   323   misinterpreted as open subgoals. While tactics can operate on the subgoals
 
   325   (the @{text "A\<^isub>i"} above), they are expected to leave the conclusion
 
   324   (the @{text "A\<^isub>i"} above), they are expected to leave the conclusion
 
  1264 \end{minipage}
 
  1263 \end{minipage}
 
  1265 \caption{The function @{ML_ind  dest_ss in Simplifier} returns a record containing
 
  1264 \caption{The function @{ML_ind  dest_ss in Simplifier} returns a record containing
 
  1266   all printable information stored in a simpset. We are here only interested in the 
  1265   all printable information stored in a simpset. We are here only interested in the 
  1267   simplification rules, congruence rules and simprocs.\label{fig:printss}}
 
  1266   simplification rules, congruence rules and simprocs.\label{fig:printss}}
 
  1268 \end{figure} *}
 
  1267 \end{figure} *}
 
       
  1268 
  1269 
  1269 
  1270 text {* 
  1270 text {* 
  1271   To see how they work, consider the function in Figure~\ref{fig:printss}, which
 
  1271   To see how they work, consider the function in Figure~\ref{fig:printss}, which
 
  1272   prints out some parts of a simpset. If you use it to print out the components of the
 
  1272   prints out some parts of a simpset. If you use it to print out the components of the
 
  1273   empty simpset, i.e., @{ML_ind  empty_ss}
 
  1273   empty simpset, i.e., @{ML_ind  empty_ss}
isabelle-cookbook