*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Pairs and automation*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Tue, 12 Feb 2013 08:39:54 +0100*In-reply-to*: <m27gme3fcf.fsf@kcl.ac.uk>*References*: <m2y5eug9iq.fsf@kcl.ac.uk> <5119143A.70501@inf.ethz.ch> <m27gme3fcf.fsf@kcl.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130106 Thunderbird/17.0.2

Dear Christian, Let's pick a different example: fun test where "test (a, b) = (a * a = b + 4)"

lemma test_split: "!!x. P (test x) = (!a b. x = (a, b) --> P (a * a = b + 4))" "!!x. P (test x) = (~ (?a b. x = (a, b) & ~ P (a * a = b + 4)))"

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.

**Follow-Ups**:**Re: [isabelle] Pairs and automation***From:*Tobias Nipkow

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

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

- Previous by Date: Re: [isabelle] I/O for Imperative HOL
- Next by Date: Re: [isabelle] Pairs and automation
- Previous by Thread: Re: [isabelle] Pairs and automation
- Next by Thread: Re: [isabelle] Pairs and automation
- 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