# [isabelle] Same proof state, different metis behaviour

```Hi,

consider this theory, which uses Nominal2

theory strangemetis
imports "Nominal/Nominal/Nominal2"
begin

lemma  "x ♯ d ⟹ x ♯ fset d"
using [[show_sorts]] [[show_consts]]
apply (erule fresh_fun_eqvt_app[rotated])
apply (rule eqvtI)
apply (rule eq_reflection)
by (metis  fset_eqvt permute_fun_def permute_minus_cancel(1))

lemma  "x ♯ d ⟹ x ♯ fset d"
apply (erule fresh_fun_eqvt_app[rotated])
using [[show_sorts]] [[show_consts]]
unfolding eqvt_def
apply rule
by (metis  fset_eqvt permute_fun_def permute_minus_cancel(1))

Before the call to metis, the proof state is identical, at least as far
as I could get jedit to tell me about it:

proof (prove): step 4

goal (1 subgoal):
1. ⋀p∷perm. p ∙ fset = fset
constants:
fresh :: atom ⇒ 'a set ⇒ bool
fresh :: atom ⇒ 'a fset ⇒ bool
prop :: prop ⇒ prop
fset :: 'a fset ⇒ 'a set
permute :: perm ⇒ ('a fset ⇒ 'a set) ⇒ 'a fset ⇒ 'a set
op = :: ('a fset ⇒ 'a set) ⇒ ('a fset ⇒ 'a set) ⇒ bool
Trueprop :: bool ⇒ prop
all :: (perm ⇒ prop) ⇒ prop
op ⟹ :: prop ⇒ prop ⇒ prop
variables:
d :: 'a fset
x :: atom
type variables:
'a :: pt

Nevertheless, in the first lemma, metis finds the proof sufficiently
fast, while in the second, it does not find any proof. As this is
probably not the intended behavior I was told to report that here.

Greetings,
Joachim

--
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.info.uni-karlsruhe.de/~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.