# [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
begin
ML{*
Simplifier.rewrite @{context} @{cterm "z = (if b then x else y)"}
*}
lemma "z = (if b then x else y)"
apply simp
sorry
end
- 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?
Thanks.
Best regards,
Iulia Dragomir
--
Iulia Dragomir, Ph.D.
Aalto University School of Science
Department of Computer Science
PO Box 15400
FI-00076 Aalto
Finland
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.*