I have modelled this calculus in Isabelle as an exercise. Here's my code so far.
I use sledgehammer to prove simple theorems which usually suggests to use blast supplemented with a subset of the rules of the calculus, e.g.:
by (blast intro: DH_bdiam2_f Fbox2_R l2)
That works fine and dandy, however if I try to use simp adding the same rules, e.g.:
by (simp only: DH_bdiam2_f Fbox2_R l2)
I get an error that none of the rules were applicable
Failed to apply initial proof method⌂:
What is going on exactly? I was expecting that simp either terminates or times out, but certainly not this. What am I missing?
This is the error message you get when a tactic failed to produce a proof step. For simp, that's the case when no rule matches (i.e. rewriting with neither DH_bdiam2_f ... is impossible). Looking at your code, these rules come from an inductive predicate. Usually, those are not suitable as rewriting (= simplification) rules. Scattered throughout Programming and Proving in Isabelle/HOL, there are hints about what are suitable simplification and introduction rules, along with explanations about what tactics are suitable.