# [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.