Re: [isabelle] Controlling the simplification steps

Le 16/09/2015 16:38, Lars Noschinski a Ãcrit :
lemma "member (2::nat) [1,2,3] = True"
   apply (rewrite member.simps)
   apply (simp only: semiring_norm)
   apply (rewrite member.simps)
   apply (simp only: semiring_norm)

The "rewrite" proof method is from "~~/src/HOL/Library/Rewrite". You
could also use "subst" instead. Both perform a single rewrite step, but
rewrite allows for better control where to rewrite (which isn't needed

The rewrite proof method does not seem to be part of Isabelle2014 that I use with my students, but subst is! I'll get by with it.

Note that this isn't really "step by step simplification", as the
simplification of arithmetic expressions takes more then a single step.

Yes but this is exactly what I want to highlight.

Thank you very much, again.

Thomas Genet
Campus de Beaulieu, 35042 Rennes cedex, France
TÃl: +33 (0) 2 99 84 73 44 E-mail: genet at

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