CODEWITHSUNDEEP
verificationisabelleformal-verification
Huan Sun
Huan Sun

Reputation: 167

Is there a way to apply the rule to a specific assumption in Isabelle?

Here is my goal

...
∀a b. P1 a b  ⟹ 
∀a b. P2 a b  ⟹
...
⟹ some goal

I want to apply the lemma to the second assumption

lemma K: ⟦ ∀a b. P a b⟧ ⟹ ∀b. P a b"

by using

apply (drule_tac a = "x" in K)

but Isabelle always firstly applies the tactic to the first assumption, how can I only apply the tactic to the second assumption?

Actually, my goal is

...
∀b. Γ b ≠ Γ' b ⟶
           b ∉ set (llocked C1) ∧ (Γ b, Γ' b) ∈ RGUnion R G2 b ∧ disjoint (dom h1) (dom (Γ' b)) ⟶
           rgsep_safe n C1 s h1 Γ' (RGUnion R G2) G1 Q1 ⟹
       ∀b. Γ b ≠ Γ' b ⟶
           b ∉ set (llocked C2) ∧ (Γ b, Γ' b) ∈ RGUnion R G1 b ∧ disjoint (dom h2) (dom (Γ' b)) ⟶
           rgsep_safe n C2 s h2 Γ' (RGUnion R G1) G2 Q2 ⟹
       rgsep_safe n C2 s h2 Γ' (RGUnion R G1) G2 Q2

and I want to use the lemma on the second assumtion

theorem K1: ∀b. ?P b ⟶ ?Q ⟹ ∀b. ?P b ⟹ ?Q

to make the goal become

...
∀b. Γ b ≠ Γ' b ⟶
           b ∉ set (llocked C1) ∧ (Γ b, Γ' b) ∈ RGUnion R G2 b ∧ disjoint (dom h1) (dom (Γ' b)) ⟶
           rgsep_safe n C1 s h1 Γ' (RGUnion R G2) G1 Q1 ⟹
∀b. Γ b ≠ Γ' b ⟶
           b ∉ set (llocked C2) ∧ (Γ b, Γ' b) ∈ RGUnion R G1 b ∧ disjoint (dom h2) (dom (Γ' b))

Upvotes: 1

Views: 214

Answers (1)

Lawrence Paulson
Lawrence Paulson

Reputation: 589

There are a lot of ugly hacks that can allow you to bypass the first assumption (e.g. by deleting it or reordering them). Already drule_tac is heading in that direction. Better by far is to use a structured proof, if it's practical for your problem. Then it's easy to name your assumptions and join them to "K" using the OF attribute.

Your theorem K1 is useless: it doesn't do what you think it does because of how the scope of quantifiers works. I tried an experiment with a simpler version of your goal and made quite a bit of progress by typing

apply (simp flip: imp_conjL)

This admittedly obscure step converts your implications into conjunctions; the simplifier notices that the quantified variable doesn't appear on the right-hand side, so all you need to do now is exhibit a b satisfying the three conditions

  1. Γ b ≠ Γ' b
  2. b ∉ set (llocked C2)
  3. (Γ b, Γ' b) ∈ RGUnion R G1 b ∧ disjoint (dom h2) (dom (Γ' b))

You will get a much nicer looking proof if you prove these facts first. If they are available then you may find that the automation proves the goal you wanted automatically.

Upvotes: 1

Related Questions