Re: [isabelle] Pairs and automation



Dear Christian,

Let's pick a different example:

fun test where "test (a, b) = (a * a = b + 4)"

Then, the split lemma should split the x parameter and do the rewrite with test.simps in one step:

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)))"

The first form splits x if "test x" occurs in the conclusion of a goal, the second does so if "test x" occurs in one of the assumptions. The format of split rules is a bit non-intuitive.

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.

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.