135   hard-coded inside the tactic. For most operators that combine tactics 

   135   hard-coded inside the tactic. For most operators that combine tactics 

   136   (@{ML THEN} is only one such operator) a ``primed'' version exists.

   136   (@{ML THEN} is only one such operator) a ``primed'' version exists.

   137 

   137 

   138   The tactics @{ML foo_tac} and @{ML foo_tac'} are very specific for

   138   The tactics @{ML foo_tac} and @{ML foo_tac'} are very specific for

   139   analysing goals being only of the form @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. If the goal is not

   139   analysing goals being only of the form @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. If the goal is not

   141 

   141 

   142   \begin{isabelle}

   142   \begin{isabelle}

   143   @{text "*** empty result sequence -- proof command failed"}\\

   143   @{text "*** empty result sequence -- proof command failed"}\\

   144   @{text "*** At command \"apply\"."}

   144   @{text "*** At command \"apply\"."}

   145   \end{isabelle}

   145   \end{isabelle}

   146 

   146 

   148   are functions mapping a goal state to a (lazy) sequence of successor states. 

   148   are functions mapping a goal state to a (lazy) sequence of successor states. 

   149   Hence the type of a tactic is:

   149   Hence the type of a tactic is:

   150 *}

   150 *}

   151   

   151   

   152 ML{*type tactic = thm -> thm Seq.seq*}

   152 ML{*type tactic = thm -> thm Seq.seq*}

   421      @{subgoals [display]} 

   421      @{subgoals [display]} 

   422      \end{minipage}*}

   422      \end{minipage}*}

   423 (*<*)oops(*>*)

   423 (*<*)oops(*>*)

   424 

   424 

   425 text {* 

   425 text {* 

   427   @{ML dtac} (@{ML dresolve_tac}), @{ML etac} (@{ML eresolve_tac}) and so on.

   427   @{ML dtac} (@{ML dresolve_tac}), @{ML etac} (@{ML eresolve_tac}) and so on.

   428 

   428 

   429 

   429 

   430   Another simple tactic is @{ML cut_facts_tac}. It inserts a list of theorems

   430   Another simple tactic is @{ML cut_facts_tac}. It inserts a list of theorems

   431   into the assumptions of the current goal state. For example

   431   into the assumptions of the current goal state. For example

   675    | Const (@{const_name "All"}, _) $ _ => rtac @{thm allI} i

   675    | Const (@{const_name "All"}, _) $ _ => rtac @{thm allI} i

   676    | _ => all_tac*}

   676    | _ => all_tac*}

   677 

   677 

   678 text {*

   678 text {*

   679   The input of the function is a term representing the subgoal and a number

   679   The input of the function is a term representing the subgoal and a number

   681   outermost @{term "Trueprop"} in order to get to the connective you like to

   681   outermost @{term "Trueprop"} in order to get to the connective you like to

   682   analyse. Otherwise goals like @{prop "A \<and> B"} are not properly

   682   analyse. Otherwise goals like @{prop "A \<and> B"} are not properly

   683   analysed. Similarly with meta-implications in the next line.  While for the

   683   analysed. Similarly with meta-implications in the next line.  While for the

   684   first five patterns we can use the @{text "@term"}-antiquotation to

   684   first five patterns we can use the @{text "@term"}-antiquotation to

   685   construct the patterns, the pattern in Line 8 cannot be constructed in this

   685   construct the patterns, the pattern in Line 8 cannot be constructed in this

  1152   all printable information stored in a simpset. We are here only interested in the 

  1152   all printable information stored in a simpset. We are here only interested in the 

  1153   simplifcation rules, congruence rules and simprocs.\label{fig:printss}}

  1153   simplifcation rules, congruence rules and simprocs.\label{fig:printss}}

  1154 \end{figure} *}

  1154 \end{figure} *}

  1155 

  1155 

  1156 text {* 

  1156 text {* 

  1160   

  1160   

  1161   @{ML_response_fake [display,gray]

  1161   @{ML_response_fake [display,gray]

  1162   "print_ss @{context} empty_ss"

  1162   "print_ss @{context} empty_ss"

  1163 "Simplification rules:

  1163 "Simplification rules:

  1164 Congruences rules:

  1164 Congruences rules:

  1212 Congruences rules:

  1212 Congruences rules:

  1213 Simproc patterns:"}

  1213 Simproc patterns:"}

  1214 

  1214 

  1215   also produces ``nothing'', the printout is misleading. In fact

  1215   also produces ``nothing'', the printout is misleading. In fact

  1216   the @{ML HOL_basic_ss} is setup so that it can solve goals of the

  1216   the @{ML HOL_basic_ss} is setup so that it can solve goals of the

  1218   and also resolve with assumptions. For example:

  1223   and also resolve with assumptions. For example:

  1219 *}

  1224 *}

  1220 

  1225 

  1221 lemma 

  1226 lemma 

  1222  "True" and "t = t" and "t \<equiv> t" and "False \<Longrightarrow> Foo" and "\<lbrakk>A; B; C\<rbrakk> \<Longrightarrow> A"

  1227  "True" and "t = t" and "t \<equiv> t" and "False \<Longrightarrow> Foo" and "\<lbrakk>A; B; C\<rbrakk> \<Longrightarrow> A"

  1223 apply(tactic {* ALLGOALS (simp_tac HOL_basic_ss) *})

  1228 apply(tactic {* ALLGOALS (simp_tac HOL_basic_ss) *})

  1224 done

  1229 done

  1225 

  1230 

  1226 text {*

  1231 text {*

  1227   This behaviour is not because of simplification rules, but how the subgoaler, solver 

  1232   This behaviour is not because of simplification rules, but how the subgoaler, solver 

  1231 

  1234 

  1232   The simpset @{ML HOL_ss} is an extention of @{ML HOL_basic_ss} containing 

  1235   The simpset @{ML HOL_ss} is an extention of @{ML HOL_basic_ss} containing 

  1233   already many useful simplification and congruence rules for the logical 

  1236   already many useful simplification and congruence rules for the logical 

  1234   connectives in HOL. 

  1237   connectives in HOL. 

  1235 

  1238 

  1253   definition

  1256   definition

  1254 *}

  1257 *}

  1255 

  1258 

  1256 definition "MyTrue \<equiv> True"

  1259 definition "MyTrue \<equiv> True"

  1257 

  1260 

  1258 lemma shows "MyTrue \<Longrightarrow> True \<and> True"

  1265 lemma shows "MyTrue \<Longrightarrow> True \<and> True"

  1259 apply(rule conjI)

  1266 apply(rule conjI)

  1260 apply(tactic {* rewrite_goals_tac [@{thm MyTrue_def}] *})

  1267 apply(tactic {* rewrite_goals_tac [@{thm MyTrue_def}] *})

  1262 

  1269 

  1263       \begin{minipage}{\textwidth}

  1270       \begin{minipage}{\textwidth}

  1264       @{subgoals [display]}

  1271       @{subgoals [display]}

  1265       \end{minipage} *}

  1272       \end{minipage} *}

  1266 (*<*)oops(*>*)

  1273 (*<*)oops(*>*)

  1735   act on @{ML_type cterm}s while the latter acts on @{ML_type thm}s. 

  1742   act on @{ML_type cterm}s while the latter acts on @{ML_type thm}s. 

  1736   However, we will also show in this section how conversions can be applied

  1743   However, we will also show in this section how conversions can be applied

  1737   to theorems via tactics. The type for conversions is

  1744   to theorems via tactics. The type for conversions is

  1738 *}

  1745 *}

  1739 

  1746 

  1741 

  1748 

  1742 text {*

  1749 text {*

  1743   whereby the produced theorem is always a meta-equality. A simple conversion

  1750   whereby the produced theorem is always a meta-equality. A simple conversion

  1744   is the function @{ML "Conv.all_conv"}, which maps a @{ML_type cterm} to an

  1751   is the function @{ML "Conv.all_conv"}, which maps a @{ML_type cterm} to an

  1745   instance of the (meta)reflexivity theorem. For example:

  1752   instance of the (meta)reflexivity theorem. For example:

  2007   Assume we want to apply @{ML all_true1_conv} only in the conclusion

  2014   Assume we want to apply @{ML all_true1_conv} only in the conclusion

  2008   of the goal, and @{ML if_true1_conv} should only apply to the premises.

  2015   of the goal, and @{ML if_true1_conv} should only apply to the premises.

  2009   Here is a tactic doing exactly that:

  2016   Here is a tactic doing exactly that:

  2010 *}

  2017 *}

  2011 

  2018 

  2021 

  2024 

  2022 text {* 

  2025 text {* 

  2023   We call the conversions with the argument @{ML "~1"}. This is to 

  2026   We call the conversions with the argument @{ML "~1"}. This is to 

  2024   analyse all parameters, premises and conclusions. If we call them with 

  2027   analyse all parameters, premises and conclusions. If we call them with 

  2025   a non-negative number, say @{text n}, then these conversions will 

  2028   a non-negative number, say @{text n}, then these conversions will 

  2028 *}

  2031 *}

  2029 

  2032 

  2030 lemma

  2033 lemma

  2031   "if True \<and> P then P else True \<and> False \<Longrightarrow>

  2034   "if True \<and> P then P else True \<and> False \<Longrightarrow>

  2032   (if True \<and> Q then True \<and> Q else P) \<longrightarrow> True \<and> (True \<and> Q)"

  2035   (if True \<and> Q then True \<and> Q else P) \<longrightarrow> True \<and> (True \<and> Q)"

  2034 txt {* where the tactic yields the goal state

  2037 txt {* where the tactic yields the goal state

  2035 

  2038 

  2036   \begin{minipage}{\textwidth}

  2039   \begin{minipage}{\textwidth}

  2037   @{subgoals [display]}

  2040   @{subgoals [display]}

  2038   \end{minipage}*}

  2041   \end{minipage}*}