[isabelle] Not the same behavior for the simplifier wrt lemma [attribute], declare [attribute], lemas [attribute]



Dear all,

I figure out that the simplifier does not behave the same way wrt a given
simpset.

In my example I did the following:

named_theorems THMs1

lemma lemma1[THMs1]:
  "blah 1=  blah2"  proof (...)

lemmas lemma2 [THMs1] =
   lemma1 [of "term", simplified]

lemma lemma3 :
  "blah 1=  blah2"
   apply (simp only: THMs1) (*the proof supposed to terminate but it is not
the case*)
oops

However if I create a specific lemma for lemma2 as follow:

lemma lemma2[THMs1]:
  "blah 1' =  blah2' "  proof (...)

Then:

lemma lemma3 :
  "blah 1=  blah2"
   apply (simp only: THMs1) (*somehow, in this case the simplifier applies
lemma2 *)
done

I tried declare lemma2[THMs1] but the simplifier do not finish the proof
neither.

Is that normal that the simplifier behaves differently with wrt the same
simpset or something is wrong with the backend of lemmas and declare?

Best,

Yakoub.



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