diff -r 74ba778b09c9 -r 2494b5b7a85d ProgTutorial/Tactical.thy --- a/ProgTutorial/Tactical.thy Sun Nov 01 10:49:25 2009 +0100 +++ b/ProgTutorial/Tactical.thy Mon Nov 02 12:47:00 2009 +0100 @@ -1253,12 +1253,12 @@ text {* \begin{exercise}\label{ex:dyckhoff} - Dyckhoff presents in \cite{Dyckhoff92} inference rules for a sequent + Dyckhoff presents in \cite{Dyckhoff92} inference rules of a sequent calculus, called G4ip, for intuitionistic propositional logic. The interesting feature of this calculus is that no contraction rule is needed - in order to be complete. As a result applying the rules exhaustively leads - to simple decision procedure for propositional intuitionistic logic. The task - is to implement this decision procedure as a tactic. His rules are + in order to be complete. As a result the rules can be applied exhaustively, which + in turn leads to simple decision procedure for propositional intuitionistic logic. + The task is to implement this decision procedure as a tactic. His rules are \begin{center} \def\arraystretch{2.3} @@ -1298,17 +1298,19 @@ \end{tabular} \end{center} - Note that in Isabelle the left-rules need to be implemented as elimination - rules. You need to prove separate lemmas corresponding to - $\longrightarrow_{L_{1..4}}$. The tactic should explore all possibilites of - applying these rules to a propositional formula until a goal state is - reached in which all subgoals are discharged. For this you can use the tactic - combinator @{ML_ind DEPTH_SOLVE in Search}. + Note that in Isabelle right rules need to be implemented as + introduction rule, the left rules as elimination rules. You have to to + prove separate theorems corresponding to $\longrightarrow_{L_{1..4}}$. The + tactic should explore all possibilites of applying these rules to a + propositional formula until a goal state is reached in which all subgoals + are discharged. For this you can use the tactic combinator @{ML_ind + DEPTH_SOLVE in Search} in the structure @{ML_struct Search}. \end{exercise} \begin{exercise} - Add to the previous exercise also rules for equality and run your tactic on - the de Bruijn formulae discussed in Exercise~\ref{ex:debruijn}. + Add to the sequent calculus from the previous exercise also rules for + equality and run your tactic on the de Bruijn formulae discussed + in Exercise~\ref{ex:debruijn}. \end{exercise} *} @@ -1316,8 +1318,8 @@ text {* A lot of convenience in reasoning with Isabelle derives from its - powerful simplifier. We will describe it in this section, whereby - we can, however, only scratch the surface due to its complexity. + powerful simplifier. We will describe it in this section. However, + due to its complexity, we can mostly only scratch the surface. The power of the simplifier is a strength and a weakness at the same time, because you can easily make the simplifier run into a loop and in general @@ -1338,7 +1340,7 @@ \end{center} \end{isabelle} - All of the tactics take a simpset and an integer as argument (the latter as usual + All these tactics take a simpset and an integer as argument (the latter as usual to specify the goal to be analysed). So the proof *} @@ -1386,17 +1388,20 @@ with @{text "constr"} being a constant, like @{const "If"}, @{const "Let"} and so on. Every simpset contains only one congruence rule for each term-constructor, which however can be overwritten. The user can declare - lemmas to be congruence rules using the attribute @{text "[cong]"}. In HOL, - the user usually states these lemmas as equations, which are then internally - transformed into meta-equations. + lemmas to be congruence rules using the attribute @{text "[cong]"}. Note that + in HOL these congruence theorems are usually stated as equations, which are + then internally transformed into meta-equations. The rewriting with theorems involving premises requires what is in Isabelle called a subgoaler, a solver and a looper. These can be arbitrary tactics that can be installed in a simpset and which are executed at various stages - during simplification. However, simpsets also include simprocs, which can - produce rewrite rules on demand (see next section). Another component are - split-rules, which can simplify for example the ``then'' and ``else'' - branches of if-statements under the corresponding preconditions. + during simplification. + + Simpsets can also include simprocs, which produce rewrite rules on + demand according to a pattern (see next section for a detailed description + of simpsets). Another component are split-rules, which can simplify for + example the ``then'' and ``else'' branches of if-statements under the + corresponding preconditions. \begin{readmore} For more information about the simplifier see @{ML_file "Pure/meta_simplifier.ML"} @@ -1408,10 +1413,10 @@ \footnote{\bf FIXME: Find the right place to mention this: Discrimination nets are implemented in @{ML_file "Pure/net.ML"}.} - The most common combinators to modify simpsets are: + The most common combinators for modifying simpsets are: \begin{isabelle} - \begin{tabular}{ll} + \begin{tabular}{l@ {\hspace{10mm}}l} @{ML_ind addsimps in MetaSimplifier} & @{ML_ind delsimps in MetaSimplifier}\\ @{ML_ind addcongs in MetaSimplifier} & @{ML_ind delcongs in MetaSimplifier}\\ @{ML_ind addsimprocs in MetaSimplifier} & @{ML_ind delsimprocs in MetaSimplifier}\\ @@ -1497,9 +1502,10 @@ Simproc patterns:"} Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss} - expects this form of the simplification and congruence rules. However, even + expects this form of the simplification and congruence rules. This is + different, if we use for example the simpset @{ML HOL_basic_ss} (see below), + where rules are usually added as equation. However, even when adding these lemmas to @{ML empty_ss} we do not end up with anything useful yet. - In the context of HOL, the first really useful simpset is @{ML_ind HOL_basic_ss in Simpdata}. While printing out the components of this simpset @@ -1509,7 +1515,7 @@ Congruences rules: Simproc patterns:"} - also produces ``nothing'', the printout is misleading. In fact + also produces ``nothing'', the printout is somewhat misleading. In fact the @{ML HOL_basic_ss} is setup so that it can solve goals of the form @@ -1565,7 +1571,7 @@ definition "MyTrue \ True" text {* - then we can use this tactic to unfold the definition of the constant. + then we can use this tactic to unfold the definition of this constant. *} lemma @@ -1578,7 +1584,7 @@ (*<*)oops(*>*) text {* - If you want to unfold definitions in \emph{all} subgoals not just one, + If you want to unfold definitions in \emph{all} subgoals, not just one, then use the the tactic @{ML_ind rewrite_goals_tac in MetaSimplifier}. *}