diff -r 1ca2f41770cc -r 79202e2eab6a ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Wed Aug 19 09:25:49 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Thu Aug 20 10:38:26 2009 +0200
@@ -1065,9 +1065,61 @@
   Most tactic combinators described in this section are defined in @{ML_file "Pure/tactical.ML"}.
   Some combinators for the purpose of proof search are implemented in @{ML_file "Pure/search.ML"}.
   \end{readmore}
+*}
 
+text {*
   \begin{exercise}\label{ex:dyckhoff}
+  Dyckhoff presents in \cite{Dyckhoff92} inference rules for a sequent
+  calculus, called G4ip, in which no contraction rule is needed in order to be
+  complete. As a result the rules applied in any order give a simple decision
+  procedure for propositional intuitionistic logic. His rules are
+
+  \begin{center}
+  \def\arraystretch{2.3}
+  \begin{tabular}{cc}
+  \infer[Ax]{A,\varGamma \Rightarrow A}{} &
+  \infer[False]{False,\varGamma \Rightarrow G}{}\\
+
+  \infer[\wedge_L]{A \wedge B, \varGamma \Rightarrow G}{A, B, \varGamma \Rightarrow G} &
+  \infer[\wedge_R]
+  {\varGamma \Rightarrow A\wedge B}{\varGamma \Rightarrow A & \varGamma \Rightarrow B}\\
   
+  \infer[\vee_L]
+  {A\vee B, \varGamma \Rightarrow G}{A,\varGamma \Rightarrow G & B,\varGamma \Rightarrow G} &
+  \infer[\vee_{R_1}]
+  {\varGamma \Rightarrow A \vee B}{\varGamma \Rightarrow A} \hspace{3mm}
+  \infer[\vee_{R_2}]
+  {\varGamma \Rightarrow A \vee B}{\varGamma \Rightarrow B}\\
+  
+  \infer[\longrightarrow_{L_1}]
+  {A\longrightarrow B, A, \varGamma \Rightarrow G}{B, A, \varGamma \Rightarrow G} &
+  \infer[\longrightarrow_R]
+  {\varGamma \Rightarrow A\longrightarrow B}{A,\varGamma \Rightarrow B}\\
+
+  \infer[\longrightarrow_{L_2}]
+  {(C \wedge D)\longrightarrow B, \varGamma \Rightarrow G}
+  {C\longrightarrow (D \longrightarrow B), \varGamma \Rightarrow G} &
+  
+  \infer[\longrightarrow_{L_3}]
+  {(C \vee D)\longrightarrow B, \varGamma \Rightarrow G}
+  {C\longrightarrow B, D\longrightarrow B, \varGamma \Rightarrow G}\\
+
+  \multicolumn{2}{c}{
+  \infer[\longrightarrow_{L_4}]
+  {(C \longrightarrow D)\longrightarrow B, \varGamma \Rightarrow G}
+  {D\longrightarrow B, \varGamma \Rightarrow C \longrightarrow D &
+  B, \varGamma \Rightarrow G}}\\
+  \end{tabular}
+  \end{center}
+
+  Implement a tactic that explores all possibilites of applying these rules to
+  a propositional formula until a goal state is reached in which all subgoals
+  are discharged.  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}}$.  In order to explore all possibilities of applying 
+  the rules, use the tactic combinator @{ML [index] DEPTH_SOLVE}, which searches 
+  for a state in which all subgoals are solved. Add also rules for equality and
+  run your tactic on the de Bruijn formulae discussed in Exercise~\ref{ex:debruijn}. 
   \end{exercise}
 
 *}