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.
CookBook/Tactical.thy
changeset 102 5e309df58557
parent 99 de625e5f6a36
child 104 5dcad9348e4d
equal deleted inserted replaced
101:123401a5c8e9 102:5e309df58557 
     4 
     4 
     5 chapter {* Tactical Reasoning\label{chp:tactical} *}
 
     5 chapter {* Tactical Reasoning\label{chp:tactical} *}
 
     6 
     6 
     7 text {*
 
     7 text {*
 
     8 
     8 
     9   The main reason for descending to the ML-level of Isabelle is to be able to
 
     9   The main reason for descending to the ML-level of Isabelle is to be
 
    10   implement automatic proof procedures. Such proof procedures usually lessen
 
    10   able to implement automatic proof procedures. Such proof procedures usually
 
    11   considerably the burden of manual reasoning, for example, when introducing
 
    11   lessen considerably the burden of manual reasoning, for example, when
 
    12   new definitions. These proof procedures are centred around refining a goal
 
    12   introducing new definitions. These proof procedures are centred around
 
    13   state using tactics. This is similar to the @{text apply}-style reasoning at
 
    13   refining a goal state using tactics. This is similar to the @{text
 
    14   the user level, where goals are modified in a sequence of proof steps until
 
    14   apply}-style reasoning at the user level, where goals are modified in a
 
    15   all of them are solved. However, there are also more structured operations
 
    15   sequence of proof steps until all of them are solved. However, there are
 
    16   that help with handling of variables and assumptions.
 
    16   also more structured operations available on the ML-level that help with 
    17 *}
 
    17   the handling of variables and assumptions.
 
    18 
    18 
    19 section {* Tactical Reasoning *}
 
    19 *}
 
    20 
    20 
    21 text {*
 
    21 section {* Basics of Reasoning with Tactics*}
 
    22   To see how tactics work, let us first transcribe a simple @{text apply}-style proof 
    22 
       
    23 text {*
 
       
    24   To see how tactics work, let us first transcribe a simple \isacommand{apply}-style proof 
    23   into ML. Consider the following proof.
 
    25   into ML. Consider the following proof.
 
    24 *}
 
    26 *}
 
    25 
    27 
    26 lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"
 
    28 lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"
 
    27 apply(erule disjE)
 
    29 apply(erule disjE)
 
    55   @{text xs} that will be generalised once the goal is proved (in our case
 
    57   @{text xs} that will be generalised once the goal is proved (in our case
 
    56   @{text P} and @{text Q}). The @{text "tac"} is the tactic that proves the goal;
 
    58   @{text P} and @{text Q}). The @{text "tac"} is the tactic that proves the goal;
 
    57   it can make use of the local assumptions (there are none in this example). 
    59   it can make use of the local assumptions (there are none in this example). 
    58   The functions @{ML etac}, @{ML rtac} and @{ML atac} correspond to 
    60   The functions @{ML etac}, @{ML rtac} and @{ML atac} correspond to 
    59   @{text erule}, @{text rule} and @{text assumption}, respectively. 
    61   @{text erule}, @{text rule} and @{text assumption}, respectively. 
    60   The operator @{ML THEN} strings the tactics together.
 
    62   The operator @{ML THEN} strings the tactics together. A difference
 
       
    63   between the \isacommand{apply}-script and the ML-code is that the
 
       
    64   former causes the lemma to be stored under the name @{text "disj_swap"}, 
       
    65   whereas the latter does not include any code for this.
 
    61 
    66 
    62   \begin{readmore}
 
    67   \begin{readmore}
 
    63   To learn more about the function @{ML Goal.prove} see \isccite{sec:results}
 
    68   To learn more about the function @{ML Goal.prove} see \isccite{sec:results}
 
    64   and the file @{ML_file "Pure/goal.ML"}. For more information about the
 
    69   and the file @{ML_file "Pure/goal.ML"}. For more information about the
 
    65   internals of goals see \isccite{sec:tactical-goals}.  See @{ML_file
 
    70   internals of goals see \isccite{sec:tactical-goals}.  See @{ML_file
 
    73   style. The reason is that the binding for @{ML disjE} can be re-assigned by 
    78   style. The reason is that the binding for @{ML disjE} can be re-assigned by 
    74   the user and thus one does not have complete control over which theorem is
 
    79   the user and thus one does not have complete control over which theorem is
 
    75   actually applied. This problem is nicely prevented by using antiquotations, 
    80   actually applied. This problem is nicely prevented by using antiquotations, 
    76   because then the theorems are fixed statically at compile-time.
 
    81   because then the theorems are fixed statically at compile-time.
 
    77 
    82 
    78   During the development of automatic proof procedures, it will often be necessary 
    83   During the development of automatic proof procedures, you will often find it 
    79   to test a tactic on examples. This can be conveniently 
    84   necessary to test a tactic on examples. This can be conveniently 
    80   done with the command \isacommand{apply}@{text "(tactic \<verbopen> \<dots> \<verbclose>)"}. 
    85   done with the command \isacommand{apply}@{text "(tactic \<verbopen> \<dots> \<verbclose>)"}. 
    81   Consider the following sequence of tactics
 
    86   Consider the following sequence of tactics
 
    82 *}
 
    87 *}
 
    83 
    88 
    84 ML{*val foo_tac = 
    89 ML{*val foo_tac = 
    94 apply(tactic {* foo_tac *})
 
    99 apply(tactic {* foo_tac *})
 
    95 done
 
   100 done
 
    96 
   101 
    97 text {*
 
   102 text {*
 
    98   By using @{text "tactic \<verbopen> \<dots> \<verbclose>"} in the apply-step,
 
   103   By using @{text "tactic \<verbopen> \<dots> \<verbclose>"} in the apply-step,
 
    99   you can call @{ML foo_tac} or any function that returns a tactic from the
 
   104   you can call from the user level of Isabelle the tactic @{ML foo_tac} or 
   100   user level of Isabelle.
 
   105   any other function that returns a tactic.
 
   101 
   106 
   102   As can be seen, each tactic in @{ML foo_tac} has a hard-coded number that
 
   107   The tactic @{ML foo_tac} is just a sequence of simple tactics stringed
 
   103   stands for the subgoal analysed by the tactic. In our case, we only focus on the first
 
   108   together by @{ML THEN}. As can be seen, each simple tactic in @{ML foo_tac}
 
   104   subgoal. This is sometimes wanted, but usually not. To avoid the explicit numbering in the 
   109   has a hard-coded number that stands for the subgoal analysed by the
 
   105   tactic, you can write
 
   110   tactic (@{text "1"} stands for the first, or top-most, subgoal). This is 
       
   111   sometimes wanted, but usually not. To avoid the explicit numbering in 
       
   112   the tactic, you can write
 
   106 *}
 
   113 *}
 
   107 
   114 
   108 ML{*val foo_tac' = 
   115 ML{*val foo_tac' = 
   109       (etac @{thm disjE} 
   116       (etac @{thm disjE} 
   110        THEN' rtac @{thm disjI2} 
   117        THEN' rtac @{thm disjI2} 
   112        THEN' rtac @{thm disjI1} 
   119        THEN' rtac @{thm disjI1} 
   113        THEN' atac)*}
 
   120        THEN' atac)*}
 
   114 
   121 
   115 text {* 
   122 text {* 
   116   and then give the number for the subgoal explicitly when the tactic is
 
   123   and then give the number for the subgoal explicitly when the tactic is
 
   117   called. For every operator that combines tactics, such a primed version 
   124   called. For every operator that combines tactics (@{ML THEN} is only one 
   118   exists. So in the next proof we can first discharge the second subgoal,
 
   125   such operator), a primed version exists. So in the next proof you 
   119   and after that the first.
 
   126   can first discharge the second subgoal, and after that the first.
 
   120 *}
 
   127 *}
 
   121 
   128 
   122 lemma "P1 \<or> Q1 \<Longrightarrow> Q1 \<or> P1"
 
   129 lemma "P1 \<or> Q1 \<Longrightarrow> Q1 \<or> P1"
 
   123    and "P2 \<or> Q2 \<Longrightarrow> Q2 \<or> P2"
 
   130    and "P2 \<or> Q2 \<Longrightarrow> Q2 \<or> P2"
 
   124 apply(tactic {* foo_tac' 2 *})
 
   131 apply(tactic {* foo_tac' 2 *})
 
   125 apply(tactic {* foo_tac' 1 *})
 
   132 apply(tactic {* foo_tac' 1 *})
 
   126 done
 
   133 done
 
   127 
   134 
   128 text {*
 
   135 text {*
 
   129   (FIXME: maybe add something about how each goal state is interpreted
 
   136   This kind of addressing is more difficult to achieve when the goal is 
   130   as a theorem)
 
   137   hard-coded inside the tactic.
 
   131 
   138 
   132   The tactic @{ML foo_tac} (and @{ML foo_tac'}) are very specific for
 
   139   The tactics @{ML foo_tac} and @{ML foo_tac'} are very specific for
 
   133   analysing goals only of the form @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. If the goal is not
 
   140   analysing goals being only of the form @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. If the goal is not
 
   134   of this form, then @{ML foo_tac} throws the error message:
 
   141   of this form, then @{ML foo_tac} throws the error message:
 
   135 
   142 
   136   \begin{isabelle}
 
   143   \begin{isabelle}
 
   137   @{text "*** empty result sequence -- proof command failed"}\\
 
   144   @{text "*** empty result sequence -- proof command failed"}\\
 
   138   @{text "*** At command \"apply\"."}
 
   145   @{text "*** At command \"apply\"."}
 
   139   \end{isabelle}
 
   146   \end{isabelle}
 
   140 
   147 
   141   Meaning the tactic failed. The reason for this error message is that tactics 
   148   Meaning the tactic failed. The reason for this error message is that tactics 
   142   are functions that map a goal state to a (lazy) sequence of successor states, 
   149   are functions that map a goal state to a (lazy) sequence of successor states, 
   143   hence the type of a tactic is
 
   150   hence the type of a tactic is:
 
   144   
   151   
   145   @{text [display, gray] "type tactic = thm -> thm Seq.seq"}
 
   152   @{text [display, gray] "type tactic = thm -> thm Seq.seq"}
 
   146 
   153 
   147   It is custom that if a tactic fails, it should return the empty sequence: 
   154   It is custom that if a tactic fails, it should return the empty sequence: 
   148   tactics should not raise exceptions willy-nilly.
 
   155   your own tactics should not raise exceptions willy-nilly.
 
       
   156 
       
   157   The simplest tactics are @{ML no_tac} and @{ML all_tac}. The first returns
 
       
   158   the empty sequence and is defined as
 
       
   159 *}
 
       
   160 
       
   161 ML{*fun no_tac thm = Seq.empty*}
 
       
   162 
       
   163 text {*
 
       
   164   which means @{ML no_tac} always fails. The second returns the given theorem wrapped 
       
   165   as a single member sequence. It is defined as
 
       
   166 *}
 
       
   167 
       
   168 ML{*fun all_tac thm = Seq.single thm*}
 
       
   169 
       
   170 text {*
 
       
   171   which means @{ML all_tac} always succeeds (but also does not make any progress 
       
   172   with the proof).
 
   149 
   173 
   150   The lazy list of possible successor states shows through to the user-level 
   174   The lazy list of possible successor states shows through to the user-level 
   151   of Isabelle when using the command \isacommand{back}. For instance in the 
   175   of Isabelle when using the command \isacommand{back}. For instance in the 
   152   following proof, there are two possibilities for how to apply 
   176   following proof, there are two possibilities for how to apply 
   153   @{ML foo_tac'}.
 
   177   @{ML foo_tac'}.
 
   156 lemma "\<lbrakk>P \<or> Q; P \<or> Q\<rbrakk> \<Longrightarrow> Q \<or> P"
 
   180 lemma "\<lbrakk>P \<or> Q; P \<or> Q\<rbrakk> \<Longrightarrow> Q \<or> P"
 
   157 apply(tactic {* foo_tac' 1 *})
 
   181 apply(tactic {* foo_tac' 1 *})
 
   158 back
 
   182 back
 
   159 done
 
   183 done
 
   160 
   184 
       
   185 
   161 text {*
 
   186 text {*
 
   162   By using \isacommand{back}, we construct the proof that uses the
 
   187   By using \isacommand{back}, we construct the proof that uses the
 
   163   second assumption to complete the proof. In more interesting 
   188   second assumption. In more interesting situations, different possibilities 
   164   situations, different possibilities can lead to different proofs.
 
   189   can lead to different proofs and even often need to be explored when
 
       
   190   a first proof attempt is unsuccessful.
 
   165   
   191   
   166   \begin{readmore}
 
   192   \begin{readmore}
 
   167   See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy
 
   193   See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy
 
   168   sequences. However in day-to-day Isabelle programming, one rarely 
   194   sequences. However in day-to-day Isabelle programming, one rarely 
   169   constructs sequences explicitly, but uses the predefined functions
 
   195   constructs sequences explicitly, but uses the predefined functions
 
   170   instead.
 
   196   instead.
 
   171   \end{readmore}
 
   197   \end{readmore}
 
   172 
   198 
   173 *}
 
   199   For a beginner it might be surprising that tactics, which transform
 
   174 
   200   one proof state to the next, are functions from theorems to theorem 
   175 section {* Basic Tactics *}
 
   201   (sequences). The surprise resolves by knowing that every 
       
   202   proof state is indeed a theorem. To shed more light on this,
 
       
   203   let us modify the code of @{ML all_tac} to obtain the following
 
       
   204   tactic
 
       
   205 *}
 
       
   206 
       
   207 ML{*fun my_print_tac ctxt thm =
 
       
   208  let
 
       
   209    val _ = warning (str_of_thm ctxt thm)
 
       
   210  in 
       
   211    Seq.single thm
 
       
   212  end*}
 
       
   213 
       
   214 text {*
 
       
   215   which prints out the given theorem (using the string-function defined 
       
   216   in Section~\ref{sec:printing}) and then behaves like @{ML all_tac}. We
 
       
   217   now can inspect every proof state in the follwing proof. On the left-hand
 
       
   218   side we show the goal state as shown by the system; on the right-hand
 
       
   219   side the print out from our @{ML my_print_tac}.
 
       
   220 *}
 
       
   221 
       
   222 lemma shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"
 
       
   223 apply(tactic {* my_print_tac @{context} *})
 
       
   224 
       
   225 txt{* \small 
       
   226       \begin{tabular}{@ {}l@ {}p{0.7\textwidth}@ {}}
 
       
   227       \begin{minipage}[t]{0.3\textwidth}
 
       
   228       @{subgoals [display]} 
       
   229       \end{minipage} &
 
       
   230       \hfill@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
 
       
   231       \end{tabular}
 
       
   232 *}
 
       
   233 
       
   234 apply(rule conjI)
 
       
   235 apply(tactic {* my_print_tac @{context} *})
 
       
   236 
       
   237 txt{* \small 
       
   238       \begin{tabular}{@ {}l@ {}p{0.76\textwidth}@ {}}
 
       
   239       \begin{minipage}[t]{0.26\textwidth}
 
       
   240       @{subgoals [display]} 
       
   241       \end{minipage} &
 
       
   242       \hfill@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
 
       
   243       \end{tabular}
 
       
   244 *}
 
       
   245 
       
   246 apply(assumption)
 
       
   247 apply(tactic {* my_print_tac @{context} *})
 
       
   248 
       
   249 txt{* \small 
       
   250       \begin{tabular}{@ {}l@ {}p{0.7\textwidth}@ {}}
 
       
   251       \begin{minipage}[t]{0.3\textwidth}
 
       
   252       @{subgoals [display]} 
       
   253       \end{minipage} &
 
       
   254       \hfill@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
 
       
   255       \end{tabular}
 
       
   256 *}
 
       
   257 
       
   258 apply(assumption)
 
       
   259 apply(tactic {* my_print_tac @{context} *})
 
       
   260 
       
   261 txt{* \small 
       
   262       \begin{tabular}{@ {}l@ {}p{0.7\textwidth}@ {}}
 
       
   263       \begin{minipage}[t]{0.3\textwidth}
 
       
   264       @{subgoals [display]} 
       
   265       \end{minipage} &
 
       
   266       \hfill@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}
 
       
   267       \end{tabular}
 
       
   268 *}
 
       
   269 
       
   270 done
 
       
   271 
       
   272 text {*
 
       
   273   As can be seen, internally every goal state is an implication of the form
 
       
   274 
       
   275   @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> (C)"}
 
       
   276 
       
   277   where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the  
       
   278   subgoals. Since the goal @{term C} can potentially be an implication, 
       
   279   there is a protector (invisible in the print out above) wrapped around 
       
   280   it. This prevents that premises are misinterpreted as open subgoals. 
       
   281   While tactics can operate on the subgoals (the @{text "A\<^isub>i"} above), they 
       
   282   are expected to leave the conclusion @{term C} intact, with the 
       
   283   exception of possibly instantiating schematic variables. 
       
   284  
       
   285 *}
 
       
   286 
       
   287 section {* Simple Tactics *}
 
   176 
   288 
   177 text {*
 
   289 text {*
 
   178   As seen above, the function @{ML atac} corresponds to the assumption tactic.
 
   290   As seen above, the function @{ML atac} corresponds to the assumption tactic.
 
   179 *}
 
   291 *}
 
   180 
   292 
   182 apply(tactic {* atac 1 *})
 
   294 apply(tactic {* atac 1 *})
 
   183 done
 
   295 done
 
   184 
   296 
   185 text {*
 
   297 text {*
 
   186   Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond
 
   298   Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond
 
   187   to @{ML_text rule}, @{ML_text drule}, @{ML_text erule} and @{ML_text frule}, 
   299   to @{text rule}, @{text drule}, @{text erule} and @{text frule}, 
   188   respectively. Below are three examples with the resulting goal state. How
 
   300   respectively. Below are three examples with the resulting goal state. How
 
   189   they work should therefore be self-explanatory.  
   301   they work should therefore be self-explanatory.  
   190 *}
 
   302 *}
 
   191 
   303 
   192 lemma shows "P \<and> Q"
 
   304 lemma shows "P \<and> Q"
 
   245 lemma shows "False \<Longrightarrow> True"
 
   357 lemma shows "False \<Longrightarrow> True"
 
   246 apply(tactic {* print_tac "foo message" *})
 
   358 apply(tactic {* print_tac "foo message" *})
 
   247 (*<*)oops(*>*)
 
   359 (*<*)oops(*>*)
 
   248 
   360 
   249 text {*
 
   361 text {*
 
   250   Also for useful for debugging, but not exclusively, are the tactics @{ML all_tac} and
 
   362   Also for useful for debugging purposes are the tactics @{ML all_tac} and
 
   251   @{ML no_tac}. The former always succeeds (but does not change the goal state), and
 
   363   @{ML no_tac}. The former always succeeds (but does not change the goal state), and
 
   252   the latter always fails.
 
   364   the latter always fails.
 
   253 
   365 
   254   (FIXME explain RS MRS)
 
   366   (FIXME explain RS MRS)
 
   255 
   367 
   272     val str_of_prems = str_of_thms context prems   
   384     val str_of_prems = str_of_thms context prems   
   273     val str_of_schms = str_of_cterms context (snd schematics)    
   385     val str_of_schms = str_of_cterms context (snd schematics)    
   274  
   386  
   275     val _ = (warning ("params: " ^ str_of_params);
 
   387     val _ = (warning ("params: " ^ str_of_params);
 
   276              warning ("schematics: " ^ str_of_schms);
 
   388              warning ("schematics: " ^ str_of_schms);
 
   277              warning ("asms: " ^ str_of_asms);
 
   389              warning ("assumptions: " ^ str_of_asms);
 
   278              warning ("concl: " ^ str_of_concl);
 
   390              warning ("conclusion: " ^ str_of_concl);
 
   279              warning ("prems: " ^ str_of_prems))
 
   391              warning ("premises: " ^ str_of_prems))
 
   280   in
 
   392   in
 
   281     no_tac 
   393     no_tac 
   282   end*}
 
   394   end*}
 
   283 text_raw{*
 
   395 text_raw{*
 
   284 \end{isabelle}
 
   396 \end{isabelle}
 
   301 txt {*
 
   413 txt {*
 
   302   which yields the printout:
 
   414   which yields the printout:
 
   303 
   415 
   304   \begin{quote}\small
 
   416   \begin{quote}\small
 
   305   \begin{tabular}{ll}
 
   417   \begin{tabular}{ll}
 
   306   params:     & @{term x}, @{term y}\\
 
   418   params:      & @{term x}, @{term y}\\
 
   307   schematics: & @{term z}\\
 
   419   schematics:  & @{term z}\\
 
   308   asms:       & @{term "A x y"}\\
 
   420   assumptions: & @{term "A x y"}\\
 
   309   concl:      & @{term "B y x \<longrightarrow> C (z y) x"}\\
 
   421   conclusion:  & @{term "B y x \<longrightarrow> C (z y) x"}\\
 
   310   prems:      & @{term "A x y"}
 
   422   premises:    & @{term "A x y"}
 
   311   \end{tabular}
 
   423   \end{tabular}
 
   312   \end{quote}
 
   424   \end{quote}
 
   313 
   425 
   314   Note in the actual output the brown colour of the variables @{term x} and 
   426   Note in the actual output the brown colour of the variables @{term x} and 
   315   @{term y}. Although parameters in the original goal, they are fixed inside
 
   427   @{term y}. Although parameters in the original goal, they are fixed inside
 
   333 txt {*
 
   445 txt {*
 
   334   then @{ML SUBPROOF} prints out 
   446   then @{ML SUBPROOF} prints out 
   335 
   447 
   336   \begin{quote}\small
 
   448   \begin{quote}\small
 
   337   \begin{tabular}{ll}
 
   449   \begin{tabular}{ll}
 
   338   params:     & @{term x}, @{term y}\\
 
   450   params:      & @{term x}, @{term y}\\
 
   339   schematics: & @{term z}\\
 
   451   schematics:  & @{term z}\\
 
   340   asms:       & @{term "A x y"}, @{term "B y x"}\\
 
   452   assumptions: & @{term "A x y"}, @{term "B y x"}\\
 
   341   concl:      & @{term "C (z y) x"}\\
 
   453   conclusion:  & @{term "C (z y) x"}\\
 
   342   prems:      & @{term "A x y"}, @{term "B y x"}
 
   454   premises:    & @{term "A x y"}, @{term "B y x"}
 
   343   \end{tabular}
 
   455   \end{tabular}
 
   344   \end{quote}
 
   456   \end{quote}
 
   345 *}
 
   457 *}
 
   346 (*<*)oops(*>*)
 
   458 (*<*)oops(*>*)
 
   347 
   459 
   424   @{ML rewrite_goals_tac}
 
   536   @{ML rewrite_goals_tac}
 
   425   @{ML cut_facts_tac}
 
   537   @{ML cut_facts_tac}
 
   426   @{ML ObjectLogic.full_atomize_tac}
 
   538   @{ML ObjectLogic.full_atomize_tac}
 
   427   @{ML ObjectLogic.rulify_tac}
 
   539   @{ML ObjectLogic.rulify_tac}
 
   428   @{ML resolve_tac}
 
   540   @{ML resolve_tac}
 
   429 *}
 
       
   430 
       
   431 
       
   432 
       
   433 text {*
 
       
   434 
       
   435 
       
   436   A goal (or goal state) is a special @{ML_type thm}, which by
 
       
   437   convention is an implication of the form:
 
       
   438 
       
   439   @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> #(C)"}
 
       
   440 
       
   441   where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the open 
       
   442   subgoals. 
       
   443   Since the goal @{term C} can potentially be an implication, there is a
 
       
   444   @{text "#"} wrapped around it, which prevents that premises are 
       
   445   misinterpreted as open subgoals. The wrapper @{text "# :: prop \<Rightarrow>
 
       
   446   prop"} is just the identity function and used as a syntactic marker. 
       
   447   
       
   448  
       
   449 
       
   450  
       
   451 
       
   452   While tactics can operate on the subgoals (the @{text "A\<^isub>i"} above), they 
       
   453   are expected to leave the conclusion @{term C} intact, with the 
       
   454   exception of possibly instantiating schematic variables. 
       
   455  
       
   456 
       
   457 
       
   458 *}
 
   541 *}
 
   459 
   542 
   460 section {* Structured Proofs *}
 
   543 section {* Structured Proofs *}
 
   461 
   544 
   462 lemma True
 
   545 lemma True
 
   493   val this = Assumption.export false ctxt ctxt0 this 
   576   val this = Assumption.export false ctxt ctxt0 this 
   494   val this = Variable.export ctxt ctxt0 [this] 
   577   val this = Variable.export ctxt ctxt0 [this] 
   495 *}
 
   578 *}
 
   496 
   579 
   497 
   580 
       
   581 
   498 end
 
   582 end
isabelle-cookbook