[isabelle] Controlling the simplification steps
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
(if 2=1 then True else (member 2 [2,3])) = True
(member 2 [2,3]) = True
(if 2=2 then True else (member 2 )) = True
True = True
Is this possible? For the moment, I am using:
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,
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