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