# Re: [isabelle] Controlling the simplification steps

On 16.09.2015 16:18, Thomas Genet wrote:
>
> Dear all,
>
>
> Is there any way to perform step by step simplification of an expression
> in a lemma? This is for teaching purposes.
>
> For instance, if I define:
>
> fun member:: "'a => 'a list => bool"
> where
> "member e [] = False" |
> "member e (x#xs) = (if e=x then True else (member e xs))"
>
>
> I would like to show:
>
> lemma "member (2::nat) [1,2,3] = True"
>
> by applying the equations of member.simps step by step, and see the goal
> evoluate as follows
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)
done
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
here).
"semiring_norm" refers to a set of theorems concerned with the
simplification of arithmetic expressions on numerals.
I found it by searching for theorems of the form:
"numeral _ = numeral _ <-> _ = _"
Note that this isn't really "step by step simplification", as the
simplification of arithmetic expressions takes more then a single step.
Best regards,
Lars

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