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