--- a/ProgTutorial/Solutions.thy	Wed Aug 19 09:25:49 2009 +0200
+++ b/ProgTutorial/Solutions.thy	Thu Aug 20 10:38:26 2009 +0200
@@ -74,6 +74,102 @@
 "(\"foo bar\", \"foo (**test**) bar (**test**)\")"}
 *}
 
+text {* \solution{ex:dyckhoff} *}
+
+text {*
+  The axiom rule can be implemented with the function @{ML atac}. The other
+  rules correspond to the theorems:
+
+  \begin{center}
+  \begin{tabular}{cc}
+  \begin{tabular}{rl}
+  $\wedge_R$ & @{thm [source] conjI}\\
+  $\vee_{R_1}$ & @{thm [source] disjI1}\\
+  $\vee_{R_2}$ & @{thm [source] disjI2}\\
+  $\longrightarrow_R$ & @{thm [source] impI}\\
+  $=_R$ & @{thm [source] iffI}\\
+  \end{tabular}
+  &
+  \begin{tabular}{rl}
+  $False$ & @{thm [source] FalseE}\\
+  $\wedge_L$ & @{thm [source] conjE}\\
+  $\vee_L$ & @{thm [source] disjE}\\
+  $=_L$ & @{thm [source] iffE}
+  \end{tabular}
+  \end{tabular}
+  \end{center}
+
+  For the other rules we need to prove the following lemmas.
+*}
+
+lemma impE1:
+  shows "\<lbrakk>A \<longrightarrow> B; A; B \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+  by iprover
+
+lemma impE2:
+  shows "\<lbrakk>(C \<and> D) \<longrightarrow> B; C \<longrightarrow> (D \<longrightarrow>B) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+  by iprover
+
+lemma impE3:
+  shows "\<lbrakk>(C \<or> D) \<longrightarrow> B; \<lbrakk>C \<longrightarrow> B; D \<longrightarrow> B\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+  by iprover
+
+lemma impE4:
+  shows "\<lbrakk>(C \<longrightarrow> D) \<longrightarrow> B; D \<longrightarrow> B \<Longrightarrow> C \<longrightarrow> D; B \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+  by iprover
+
+lemma impE5:
+  shows "\<lbrakk>(C = D) \<longrightarrow> B; (C \<longrightarrow> D) \<longrightarrow> ((D \<longrightarrow> C) \<longrightarrow> B) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+  by iprover
+
+text {*
+  Now the tactic which applies a single rule can be implemented
+  as follows.
+*}
+
+ML %linenosgray{*val apply_tac =
+let
+  val intros = [@{thm conjI}, @{thm disjI1}, @{thm disjI2}, 
+                @{thm impI}, @{thm iffI}]
+  val elims  = [@{thm FalseE}, @{thm conjE}, @{thm disjE}, @{thm iffE},
+                @{thm impE2}, @{thm impE3}, @{thm impE4}, @{thm impE5}]
+in
+  atac
+  ORELSE' resolve_tac intros
+  ORELSE' eresolve_tac elims
+  ORELSE' (etac @{thm impE1} THEN' atac)
+end*}
+
+text {*
+  In Line 11 we apply the rule @{thm [source] impE1} in concjunction 
+  with @{ML atac} in order to reduce the number of possibilities that
+  need to be explored. You can use the tactic as follows.
+*}
+
+lemma
+  shows "((((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P) \<longrightarrow> Q) \<longrightarrow> Q"
+apply(tactic {* (DEPTH_SOLVE o apply_tac) 1 *})
+done
+
+text {*
+  We can use the tactic to prove or disprove automatically the
+  de Bruijn formulae from Exercise \ref{ex:debruijn}.
+*}
+
+ML{*fun de_bruijn_prove ctxt n =
+let 
+  val goal = HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))
+in
+  Goal.prove ctxt ["P"] [] goal
+   (fn _ => (DEPTH_SOLVE o apply_tac) 1)
+end*}
+
+text {* 
+  You can use this function to prove de Bruijn formulae.
+*}
+
+ML{*de_bruijn_prove @{context} 3 *}
+
 text {* \solution{ex:addsimproc} *}
 
 ML{*fun dest_sum term =