[isabelle] simp vs Simplifier.rewrite

Dear all,

I have a question with respect to the functionalities of
Simplifier.rewrite versus simp. In the following theory:

theory Test imports Main

Simplifier.rewrite @{context} @{cterm "z = (if b then x else y)"}

lemma "z = (if b then x else y)"
  apply simp


- Simplifier.rewrite keeps the term intact, i.e. val it = "z = (if b
then x else y) â z = (if b then x else y)": thm
- whereas simp reduces z to (b â z = x) â (Â b â z = y).

It seems that simp is more powerful than Simplifier.
Now, how can the same behavior as for simp be achieved through
Simplifier? Are there certain theorems that need to be added when using
ML code for simplification?


Best regards,
Iulia Dragomir

Iulia Dragomir, Ph.D.
Aalto University School of Science
Department of Computer Science
PO Box 15400
FI-00076 Aalto
Email: iulia.dragomir at aalto.fi
Phone: +358 503 872710
Web: http://users.ics.aalto.fi/iulia

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