Email Gateway (Aug 22 2022 at 15:40): Email Gateway (Aug 22 2022 at 15:40):From: Nemouchi Yakoub <y.nemouchi@gmail.com>
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.
Last updated: Apr 30 2024 at 12:28 UTC