76 

    77 text {* \solution{ex:dyckhoff} *}

    78 

    79 text {*

    80   The axiom rule can be implemented with the function @{ML atac}. The other

    81   rules correspond to the theorems:

    82 

    83   \begin{center}

    84   \begin{tabular}{cc}

    85   \begin{tabular}{rl}

    86   $\wedge_R$ & @{thm [source] conjI}\\

    87   $\vee_{R_1}$ & @{thm [source] disjI1}\\

    88   $\vee_{R_2}$ & @{thm [source] disjI2}\\

    89   $\longrightarrow_R$ & @{thm [source] impI}\\

    90   $=_R$ & @{thm [source] iffI}\\

    91   \end{tabular}

    92   &

    93   \begin{tabular}{rl}

    94   $False$ & @{thm [source] FalseE}\\

    95   $\wedge_L$ & @{thm [source] conjE}\\

    96   $\vee_L$ & @{thm [source] disjE}\\

    97   $=_L$ & @{thm [source] iffE}

    98   \end{tabular}

    99   \end{tabular}

   100   \end{center}

   101 

   102   For the other rules we need to prove the following lemmas.

   103 *}

   104 

   105 lemma impE1:

   106   shows "\<lbrakk>A \<longrightarrow> B; A; B \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"

   107   by iprover

   108 

   109 lemma impE2:

   110   shows "\<lbrakk>(C \<and> D) \<longrightarrow> B; C \<longrightarrow> (D \<longrightarrow>B) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"

   111   by iprover

   112 

   113 lemma impE3:

   114   shows "\<lbrakk>(C \<or> D) \<longrightarrow> B; \<lbrakk>C \<longrightarrow> B; D \<longrightarrow> B\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"

   115   by iprover

   116 

   117 lemma impE4:

   118   shows "\<lbrakk>(C \<longrightarrow> D) \<longrightarrow> B; D \<longrightarrow> B \<Longrightarrow> C \<longrightarrow> D; B \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"

   119   by iprover

   120 

   121 lemma impE5:

   122   shows "\<lbrakk>(C = D) \<longrightarrow> B; (C \<longrightarrow> D) \<longrightarrow> ((D \<longrightarrow> C) \<longrightarrow> B) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"

   123   by iprover

   124 

   125 text {*

   126   Now the tactic which applies a single rule can be implemented

   127   as follows.

   128 *}

   129 

   130 ML %linenosgray{*val apply_tac =

   131 let

   132   val intros = [@{thm conjI}, @{thm disjI1}, @{thm disjI2}, 

   133                 @{thm impI}, @{thm iffI}]

   134   val elims  = [@{thm FalseE}, @{thm conjE}, @{thm disjE}, @{thm iffE},

   135                 @{thm impE2}, @{thm impE3}, @{thm impE4}, @{thm impE5}]

   136 in

   137   atac

   138   ORELSE' resolve_tac intros

   139   ORELSE' eresolve_tac elims

   140   ORELSE' (etac @{thm impE1} THEN' atac)

   141 end*}

   142 

   143 text {*

   144   In Line 11 we apply the rule @{thm [source] impE1} in concjunction 

   145   with @{ML atac} in order to reduce the number of possibilities that

   146   need to be explored. You can use the tactic as follows.

   147 *}

   148 

   149 lemma

   150   shows "((((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P) \<longrightarrow> Q) \<longrightarrow> Q"

   151 apply(tactic {* (DEPTH_SOLVE o apply_tac) 1 *})

   152 done

   153 

   154 text {*

   155   We can use the tactic to prove or disprove automatically the

   156   de Bruijn formulae from Exercise \ref{ex:debruijn}.

   157 *}

   158 

   159 ML{*fun de_bruijn_prove ctxt n =

   160 let 

   161   val goal = HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))

   162 in

   163   Goal.prove ctxt ["P"] [] goal

   164    (fn _ => (DEPTH_SOLVE o apply_tac) 1)

   165 end*}

   166 

   167 text {* 

   168   You can use this function to prove de Bruijn formulae.

   169 *}

   170 

   171 ML{*de_bruijn_prove @{context} 3 *}