Re: [isabelle] Pairs and automation



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





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