Email Gateway (Aug 22 2022 at 10:24): Email Gateway (Aug 22 2022 at 10:24):From: Iulia Dragomir <iulia.dragomir@aalto.fi>
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
Email Gateway (Aug 22 2022 at 10:46):From: Thomas Sewell <thomas.sewell@nicta.com.au>
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} [@{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.
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.
Email Gateway (Aug 22 2022 at 10:46):From: Lars Noschinski <noschinl@in.tum.de>
For an overview of the components, one can look at the latter sections
of chapter 9.3 in the isar-ref manual.
Last updated: Apr 23 2024 at 20:15 UTC