[isabelle] "show" taking very long with goals with many hypothesis



Hi,

I have an inductive proof where the induction rule has a lot of very
similar assumptions, due to the Nominal machinery: (Don’t worry about
the details, this is just to give an impression of what I mean by
„many“).

1. ⋀n Γ Γ' Δ Δ' x e y Θ Θ' z e' u xa.
       atom n ♯ xa ⟹
       atom z ♯ xa ⟹
       atom n ♯ Γ ⟹
       atom n ♯ Γ' ⟹
       atom n ♯ Δ ⟹
       atom n ♯ Δ' ⟹
       atom n ♯ x ⟹
       atom n ♯ e ⟹
       atom n ♯ y ⟹
       atom n ♯ Θ ⟹
       atom n ♯ Θ' ⟹
       atom n ♯ z ⟹
       atom z ♯ Γ ⟹
       atom z ♯ Γ' ⟹
       atom z ♯ Δ ⟹
       atom z ♯ Δ' ⟹
       atom z ♯ x ⟹
       atom z ♯ e ⟹
       atom z ♯ y ⟹
       atom z ♯ Θ ⟹
       atom z ♯ Θ' ⟹
       distinctVars (((x, App e y) # Γ') @ Γ) ⟹
       distinctVars (((n, e) # (x, App (Var n) y) # Γ') @ Γ) ⟹
       distinctVars (((n, Lam [z]. e') # (x, App (Var n) y) # Δ') @ Δ) ⟹
       distinctVars (((x, e'[z::=y]) # Δ') @ Δ) ⟹
       distinctVars (Θ' @ Θ) ⟹
       Γ : (n, e) # (x, App (Var n) y) # Γ' ⇓⇧×⇧u⇧d Δ : (n, Lam [z]. e') # (x, App (Var n) y) # Δ' ⟹
       (⋀b. atom b ♯ (Γ, snd (hd ((n, e) # (x, App (Var n) y) # Γ'))) ⟹
            atom b ♯ (Δ, snd (hd ((n, Lam [z]. e') # (x, App (Var n) y) # Δ'))) ∨ b ∈ heapVars Δ) ⟹
       Δ : (x, e'[z::=y]) # Δ' ⇓⇧×⇧u⇧d Θ : Θ' ⟹
       (⋀b. atom b ♯ (Δ, snd (hd ((x, e'[z::=y]) # Δ'))) ⟹
            atom b ♯ (Θ, snd (hd Θ')) ∨ b ∈ heapVars Θ) ⟹
       atom xa ♯ (Γ, snd (hd ((x, App e y) # Γ'))) ⟹ atom xa ♯ (Θ, snd (hd Θ')) ∨ xa ∈ heapVars Θ

I handle the case using a named case:

case (DApplicationInd n Γ Γ' Δ Δ' xa e y Θ Θ' z e' u x)
  [..]
  thus ?case
  proof [..]
  qed

At the "thus", as well as at the "qed", Isabelle sits there for a long
time (minutes) before continuing.

My guess is that there are many ways to unify my assumptions with the
assumptions of the goal, and Isabelle tries a lot of wrong ones before
ruling them out according to the statement shown and the other
assumptions.

Is there a way to help out Isabelle here? And coudn’t the "case Foo"
command somehow ensure that Isabelle will try the „right“ unification
first?

Thanks,
Joachim

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.