[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.