Re: [isabelle] simp vs Simplifier.rewrite



There's a few components to the simplifier, and its various incarnations
enable different ones.

The feature you've seen here is called the splitter. It can be run
independently via

  apply (split split_if)

or

  apply (tactic {* Splitter.split_tac @{context} [ at {thm split_if}] 1 *})

The simplifier uses the splitter after normal simplification when it is
in "tactic" form (apply simp or Simplifier.simp_tac) and never uses it
when it is in "forward" form (Simplifier.rewrite or thm
foo[simplified]). There might be ways to change this or work around it.

Cheers,
    Thomas.


On 27/06/15 00:18, Iulia Dragomir wrote:
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



________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




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