[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"
"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 Genet
Campus de Beaulieu, 35042 Rennes cedex, France
TÃl: +33 (0) 2 99 84 73 44 E-mail: genet at irisa.fr

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