Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Pairs and automation

Email Gateway (Aug 19 2022 at 10:05):

From: Christian Urban <christian.urban@kcl.ac.uk>
Dear Isabelle-Wizards,

I have a theory where I need to define functions
over tuples, say this contrived one

fun test where
"test (a, b) = False"

Now I like to prove lemmas like

lemma "test x ==> P"
apply(case_tac x)
apply(simp)
done

As can be seen this can be proved, but needs the explicit
case_tac in order to make Isabelle aware the x is in fact
a pair.

Is there a way I can make Isabelle figure this out automatically?

If I had a !!-quantifier around x, then this seems
to do the job:

lemma "!!x. test x ==> P"
apply(simp add: split_paired_all)
done

I toyed with definitions like

fun test2
where
"test2 x = (let (a, b) = x in False)"

lemma "test2 x ==> P"
apply(simp)
done

But I am wondering whether there is some other magic that
lets my problem go away (automatically). Does anybody else
encountered this problem?

Best wishes,
Christian

Email Gateway (Aug 19 2022 at 10:05):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Christian,

You could prove split rules for your functions, similar to prod.splits:

lemma test_split:
"!!x. P (test x) = (!a b. x = (a, b) --> P (test (a, b)))"
"!!x. P (test x) = (~ (∃a b. x = (a, b) & ~ P (test (a, b))))"
by(simp_all add: split_paired_all)

lemma "test x ==> P"
apply(simp split: test_split)
done

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.

Andreas

Email Gateway (Aug 19 2022 at 10:07):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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

Email Gateway (Aug 19 2022 at 10:07):

From: Tobias Nipkow <nipkow@in.tum.de>
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.

Last updated: Apr 25 2024 at 20:15 UTC