Re: [isabelle] Controlling the simplification steps



On 16.09.2015 16:18, Thomas Genet wrote:
> 
> 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

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




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