Isabelle: adjusting lemma to form required for `rule` method

2
votes

I define an inductive relation called step_g. Here is one of the inference rules:

G_No_Op:
  "∀j ∈ the (T i). ¬ (eval_bool p (the (γ ⇩t⇩s j)))
  ⟹ step_g a i T (γ, (Barrier, p)) (Some γ)"

I want to invoke this rule in a proof, so I type

apply (rule step_g.G_No_Op)

but the rule cannot be applied, because its conclusion must be of a particular form already (the two γ's must match). So I adapt the rule like so:

lemma G_No_Op_helper:
  "⟦ ∀j ∈ the (T i). ¬ (eval_bool p (the (γ ⇩t⇩s j))) ; γ = γ' ⟧
  ⟹ step_g a i T (γ, (Barrier, p)) (Some γ')"
by (simp add: step_g.G_No_Op)

Now, when I invoke rule G_No_Op_helper, the requirement that "the two γ's must match" becomes a subgoal to be proven.

The transformation of G_No_Op into G_No_Op_helper looks rather mechanical. My question is: is there a way to make Isabelle do this automatically?

Edit. I came up with a "minimal working example". In the following, lemma A is equivalent to A2, but rule A doesn't help to prove the theorem, only rule A2 works.

consts foo :: "nat ⇒ nat ⇒ nat ⇒ bool"

lemma A: "x < y ⟹ foo y x x"
sorry

lemma A2: "⟦ x < y ; x = z ⟧ ⟹ foo y x z"
sorry

theorem "foo y x z"
apply (rule A)
3
isabelle
Intersting; I have had similar issues like this before. A „Match this rule, dammit, and give me all failed unifications as subgoals!“ might be handy from time to time. – Joachim Breitner
I suspect that could be problematic because there might be many different possibilities to add equations to make something unifiable. But I'm not sure. – Manuel Eberl

3 Answers

2
votes

To my knowledge, nothing exists to automate these things. One could probably implement this as an attribute, i.e.

thm A[generalised x]

to obtain something like A2. The attribute would replace every occurence of the variable it is given (i.e. x here) but the first in the conclusion of the theorem with a fresh variable x' and add the premise x' = x to the theorem.

This shouldn't be very hard to implement for someone more skilled in Isabelle/ML than me – maybe some of the advanced Isabelle/ML hackers who read this could comment on the idea.

2
votes

There is a well-known principle "proof-by-definition", i.e. you write your initial specifications in a way such the the resulting rules are easy to apply. This might occasionally look unexpected to informal readers, but is normal for formalists.

0
votes

I had similar problems and wrote a method named fuzzy_rule, which can be used like this:

theorem "foo y x z"
  apply (fuzzy_rule A)
  subgoal "x < y" 
    sorry
  subgoal "x = z"
    sorry

The code is available at https://github.com/peterzeller/isabelle_fuzzy_rule