Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Controlling the simplification steps

Email Gateway (Aug 22 2022 at 11:27):

From: Thomas Genet <thomas.genet@irisa.fr>
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

Email Gateway (Aug 22 2022 at 11:27):

From: Lars Noschinski <noschinl@in.tum.de>
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

Email Gateway (Aug 22 2022 at 11:28):

From: Thomas Genet <thomas.genet@irisa.fr>
Le 16/09/2015 16:38, Lars Noschinski a écrit :

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

Great!
The rewrite proof method does not seem to be part of Isabelle2014 that I
use with my students, but subst is! I'll get by with it.

Note that this isn't really "step by step simplification", as the
simplification of arithmetic expressions takes more then a single step.

Yes but this is exactly what I want to highlight.

Thank you very much, again.

Thomas

Email Gateway (Aug 22 2022 at 11:28):

From: Lars Noschinski <noschinl@in.tum.de>
On 16.09.2015 17:24, Thomas Genet wrote:

The rewrite proof method does not seem to be part of Isabelle2014 that I
use with my students, but subst is! I'll get by with it.

Indeed, "rewrite" is only part of Isabelle since 2015.

Note that this isn't really "step by step simplification", as the
simplification of arithmetic expressions takes more then a single step.

Yes but this is exactly what I want to highlight.

I guessed so ;)

-- Lars

Last updated: Apr 20 2024 at 04:19 UTC