diff -r ac01ddb285f6 -r e60dbcba719d ProgTutorial/Tactical.thy --- a/ProgTutorial/Tactical.thy Fri Mar 27 18:19:42 2009 +0000 +++ b/ProgTutorial/Tactical.thy Mon Mar 30 08:17:22 2009 +0000 @@ -5,7 +5,7 @@ chapter {* Tactical Reasoning\label{chp:tactical} *} text {* - The main reason for descending to the ML-level of Isabelle is to be able to + One of the main reason for descending to the ML-level of Isabelle is to be able to implement automatic proof procedures. Such proof procedures usually lessen considerably the burden of manual reasoning, for example, when introducing new definitions. These proof procedures are centred around refining a goal @@ -119,7 +119,8 @@ THEN' atac)*} text {* - and then give the number for the subgoal explicitly when the tactic is + where @{ML THEN'} is used instead of @{ML THEN}. With @{ML foo_tac'} you can give + the number for the subgoal explicitly when the tactic is called. So in the next proof you can first discharge the second subgoal, and subsequently the first. *} @@ -310,7 +311,7 @@ the subgoals. So after setting up the lemma, the goal state is always of the form @{text "C \ (C)"}; when the proof is finished we are left with @{text "(C)"}. Since the goal @{term C} can potentially be an implication, there is - a ``protector'' wrapped around it (in from of an outermost constant @{text + a ``protector'' wrapped around it (the wrapper is the outermost constant @{text "Const (\"prop\", bool \ bool)"}; however this constant is invisible in the figure). This wrapper prevents that premises of @{text C} are mis-interpreted as open subgoals. While tactics can operate on the subgoals @@ -347,13 +348,13 @@ (*<*)oops(*>*) text {* - A simple tactic for ``easily'' discharging proof obligations is + A simple tactic for easy discharge of any proof obligations is @{ML SkipProof.cheat_tac}. This tactic corresponds to the Isabelle command \isacommand{sorry} and is sometimes useful during the development of tactics. *} -lemma shows "False" and "something_else_obviously_false" +lemma shows "False" and "Goldbach_conjecture" apply(tactic {* SkipProof.cheat_tac @{theory} *}) txt{*\begin{minipage}{\textwidth} @{subgoals [display]} @@ -375,7 +376,7 @@ text {* Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond to @{text rule}, @{text drule}, @{text erule} and @{text frule}, - respectively. Each of them takes a theorem as argument and attempts to + respectively. Each of them take a theorem as argument and attempt to apply it to a goal. Below are three self-explanatory examples. *} @@ -401,20 +402,6 @@ (*<*)oops(*>*) text {* - Note the number in each tactic call. Also as mentioned in the previous section, most - basic tactics take such a number as argument: this argument addresses the subgoal - the tacics are analysing. In the proof below, we first split up the conjunction in - the second subgoal by focusing on this subgoal first. -*} - -lemma shows "Foo" and "P \ Q" -apply(tactic {* rtac @{thm conjI} 2 *}) -txt {*\begin{minipage}{\textwidth} - @{subgoals [display]} - \end{minipage}*} -(*<*)oops(*>*) - -text {* The function @{ML resolve_tac} is similar to @{ML rtac}, except that it expects a list of theorems as arguments. From this list it will apply the first applicable theorem (later theorems that are also applicable can be @@ -494,7 +481,7 @@ takes an additional number as argument that makes explicit which premise should be instantiated. - To improve readability of the theorems we produce below, we shall use the + To improve readability of the theorems we shall produce below, we will use the function @{ML no_vars} from Section~\ref{sec:printing}, which transforms schematic variables into free ones. Using this function for the first @{ML RS}-expression above produces the more readable result: @@ -764,7 +751,8 @@ (*<*)oops(*>*) text {* - If you want to avoid the hard-coded subgoal addressing, then you can use + If you want to avoid the hard-coded subgoal addressing, then, as + seen earlier, you can use the ``primed'' version of @{ML THEN}. For example: *} @@ -776,7 +764,7 @@ (*<*)oops(*>*) text {* - Here you only have to specify the subgoal of interest only once and + Here you have to specify the subgoal of interest only once and it is consistently applied to the component tactics. For most tactic combinators such a ``primed'' version exists and in what follows we will usually prefer it over the ``unprimed'' one. @@ -1275,7 +1263,7 @@ lemma shows "MyTrue \ True \ True" apply(rule conjI) -apply(tactic {* rewrite_goals_tac [@{thm MyTrue_def}] *}) +apply(tactic {* rewrite_goals_tac @{thms MyTrue_def} *}) txt{* producing the goal state \begin{minipage}{\textwidth} @@ -1391,10 +1379,10 @@ added to the simplifier, because now the right-hand side is not anymore an instance of the left-hand side. In a sense it freezes all redexes of permutation compositions after one step. In this way, we can split simplification of permutations - into three phases without the user not noticing anything about the auxiliary + into three phases without the user noticing anything about the auxiliary contant. We first freeze any instance of permutation compositions in the term using lemma @{thm [source] "perm_aux_expand"} (Line 9); - then simplifiy all other permutations including pusing permutations over + then simplifiy all other permutations including pushing permutations over other permutations by rule @{thm [source] perm_compose_aux} (Line 10); and finally ``unfreeze'' all instances of permutation compositions by unfolding the definition of the auxiliary constant. @@ -1492,6 +1480,11 @@ (*<*)oops(*>*) text {* + \begin{isabelle} + @{text "> The redex: Suc 0"}\\ + @{text "> The redex: Suc 0"}\\ + \end{isabelle} + This will print out the message twice: once for the left-hand side and once for the right-hand side. The reason is that during simplification the simplifier will at some point reduce the term @{term "1::nat"} to @{term "Suc