In my theory I have some bigger definitions, from which I derive some simple properties using lemmas.
My problem is, that the lemmas for deriving the properties are not used by the simplifier and I have to manually instantiate them. Is there a way to make this more automatic?
A minimal example is shown below:
definition complexFact :: "int ⇒ int ⇒ int ⇒ bool" where
"complexFact x y z ≡ x = y + z"
lemma useComplexFact: "complexFact x y z ⟹ x = y + z"
by (simp add: complexFact_def)
lemma example_1:
assumes cf: "complexFact a b c"
shows "a = b + c"
apply (simp add: cf useComplexFact) (* easy, works *)
done
lemma example_2a:
assumes cf: "complexFact a b c"
shows "a - b = c"
apply (simp add: cf useComplexFact) (* does not work *)
oops
lemma example_2b:
assumes cf: "complexFact a b c"
shows "a - b = c"
apply (simp add: useComplexFact[OF cf]) (* works *)
done
lemma example_2c:
assumes cf: "complexFact a b c"
shows "a - b = c"
apply (subst useComplexFact) (* manually it also works*)
apply (subst cf)
apply simp+
done
I found the following paragraph in the reference manual, so I guess I could solve my problem with a custom solver. However, I never really touched the internal ML part of Isabelle and don't know where to start.
Rewriting does not instantiate unknowns. For example, rewriting alone can- not prove a ∈ ?A since this requires instantiating ?A . The solver, however, is an arbitrary tactic and may instantiate unknowns as it pleases. This is the only way the Simplifier can handle a conditional rewrite rule whose condition contains extra variables.
The Isabelle simplifier by itself never instantiates unknowns in assumptions of conditional rewrite rules. However, the solvers can do that, and the most reliable one is assumption. So if complex_fact a b c literally appears in the assumptions of the goal (rather than being added to the simpset with simp add: or with [simp]), the assumption solver kicks in and instantiated the unknowns. However, it will only use the first instance of complex_fact in the assumptions. So if there are several of them, it will not try all of them. In summary, it is better to write
lemma
assumes cf: "complexFact a b c"
shows "a = b + c"
using cf
apply(simp add: useComplexFact)
The second problem with your example is that a = b + c with a, b, and c being free is not a good rewrite rule, because the head symbol on the left-hand side is not a constant, but the free variable a. Therefore, the simplifier will not use the equation a = b + c to replace a with b + c, but to replace literal occurrences of the equation a = b + c with True. You can see this preprocessing in the trace of the simplifer (enable it locally with using [[simp_trace]]). That's the reason why example_1 works and the others don't. If you can change your left hand side such that there is a constant as the head symbol, then some decent proof automation should be possible without writing a custom solver.
Further, you can do some (limited) form of forward reasoning by using useComplexFact as a destruction rule. That is,
using assms
apply(auto dest!: useComplexFact)
can also work in some cases. However, this is pretty close to unfolding the definition in terms of scalability.