# [isabelle] Controlling the simplification steps

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
`
apply (???)
(if 2=1 then True else (member 2 [2,3])) = True
apply (???)
(member 2 [2,3]) = True
apply (???)
(if 2=2 then True else (member 2 [3])) = True
apply (???)
True = True
Is this possible? For the moment, I am using:
using [[simp_trace=true]]
apply auto

`that is already nice but a little to much verbose for my purpose... and
``if I am right tweaking simp_trace_depth_limit will not help me.
`
Thanks in advance,
Thomas
--
Thomas Genet
ISTIC/IRISA
Campus de Beaulieu, 35042 Rennes cedex, France
TÃl: +33 (0) 2 99 84 73 44 E-mail: genet at irisa.fr
http://www.irisa.fr/celtique/genet

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