*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Pairs and automation*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 12 Feb 2013 08:46:13 +0100*In-reply-to*: <5119F1CA.8030407@inf.ethz.ch>*References*: <m2y5eug9iq.fsf@kcl.ac.uk> <5119143A.70501@inf.ethz.ch> <m27gme3fcf.fsf@kcl.ac.uk> <5119F1CA.8030407@inf.ethz.ch>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8; rv:17.0) Gecko/20130107 Thunderbird/17.0.2

Am 12/02/2013 08:39, schrieb Andreas Lochbihler: > I do not know how well the split rules work if you have a recursive call to test > on the rhs, as I am no expert on how exactly the splitter works. However, I > would expect that the same rules as for the simplifier apply, i.e., if the > recursive call is hidden under another operator with a suitable congruence rule, > you're safe - otherwise, it will loop. The splitter ignores congruence rules. Tobias > Best wishes > Andreas > > On 02/11/2013 06:55 PM, Christian Urban wrote: >> >> Dear Andreas, >> >> Thanks a lot for the answer! >> >> > there's less danger if >> > you replace the "test (a, b)" on the rhs with the rhs of the function >> > definition, but then the theorems are less canoncial >> >> I am not sure I understand this. Do you mean I should >> instead of proving >> >> lemma test_split: >> "!!x. P (test x) = (!a b. x = (a, b) --> P (test (a, b)))" >> >> I should prove something like >> >> lemma test_split: >> "!!x. P (test x) = (!a b. x = (a, b) --> P (rhs (a, b)))" >> >> where rhs is the "expanded" version of the rhs of the function. >> But how would that work if the function is defined by >> fun via pattern matching. Then I would get some big >> case-expression on the right. Is this what you had in mind? >> >> Also one more question: I can see the purpose of the >> theorem above, but when is the following used? >> >> "!!x. P (test x) = (~ (∃a b. x = (a, b) & ~ P (test (a, b))))" >> >> >> Best wishes and thanks a lot again! >> Christian >> >> On Monday, February 11, 2013 at 16:54:34 (+0100), Andreas Lochbihler wrote: >> > >> > But these split rules are aggressive, they split the parameter for every >> > occurrence of test. And they make the simplifier loop if the rhs >> > occurrence of test does not get simplified away (there's less danger if >> > you replace the "test (a, b)" on the rhs with the rhs of the function >> > definition, but then the theorems are less canoncial). Fortunately, the >> > simplifier tries split rules after applying its simplification steps, so >> > this should normally work. >> >>

**References**:**[isabelle] Pairs and automation***From:*Christian Urban

**Re: [isabelle] Pairs and automation***From:*Andreas Lochbihler

**Re: [isabelle] Pairs and automation***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Pairs and automation
- Next by Date: [isabelle] Sandboxed evaluation of Isabelle theories?
- Previous by Thread: Re: [isabelle] Pairs and automation
- Next by Thread: [isabelle] The usefulness of smt (and simp)
- Cl-isabelle-users February 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list