CODEWITHSUNDEEP
isabelle
John Wickerson
John Wickerson

Reputation: 1232

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

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)

Upvotes: 2

Views: 206

Answers (3)

Peter Zeller
Peter Zeller

Reputation: 2296

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

Upvotes: 0

Makarius
Makarius

Reputation: 2224

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.

Upvotes: 2

Manuel Eberl
Manuel Eberl

Reputation: 8278

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.

Upvotes: 2

Related Questions