Re: [isabelle] Simplification of unique elements



2009/12/8 Juan Antonio Navarro Pérez <juannavarroperez at gmail.com>:
> Suppose I have some unary predicate P, and I have proved that it has a
> unique satisfying solution. That is, I prove the theorem:
>
> theorem unique [simp]: "[| P a; P b |] ==> a = b"
>
> It seems that, even after declaring the rule as a simplification, the
> rule is not always applied by Isabelle. As an example, the following
> proof attempt fails.
>
> theorem foo: "[| P a; P b |] ==> f a = f b"
> apply (simp)

Hi Juan,

When you declare "unique" as a simp rule, Isabelle's simplifier
immediately notices that it would cause looping in its original form.
Instead, it uses this rule for simplification:

"[| P a; P b |] ==> (a = b) == True"

(I determined this by doing "simp add: unique" with "Trace Simplifier" enabled.)
This modified form won't loop, but it is not sufficient to prove your
theorem "foo".

One possibility is to use "unique" with auto, as a dest rule:

theorem foo: "[| P a; P b |] ==> f a = f b"
by (auto dest: unique)

The effect of "dest: unique" is that when auto finds "P a" and "P b"
in the assumptions, it will remove "P a" and replace it by "a = b".


Another possibility is to do some trickery with Isabelle's
definite-choice operator. This method works using only ordinary simp
rules, but you will need to prove existence as well as uniqueness, and
it also requires the definition of an extra constant.

lemma exists: "EX x. P x"
sorry

lemma exists1: "EX! x. P x"
using exists unique by (rule ex_ex1I)

definition "theP = (THE x. P x)"

lemma P_iff: "P a = (a = theP)"
unfolding theP_def
apply safe
apply (rule the1_equality [symmetric])
apply (rule exists1)
apply assumption
apply (rule theI')
apply (rule exists1)
done

Unlike "unique", lemma "P_iff" is a well-behaved simp rule.

theorem foo: "[| P a; P b |] ==> f a = f b"
by (simp add: P_iff)

Hope this helps,
- Brian





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