--- 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}
*}