Email Gateway (Aug 18 2022 at 14:23): Email Gateway (Aug 18 2022 at 14:23):From: Juan Antonio Navarro Pérez <juannavarroperez@gmail.com>
Hi all!
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)
Alternatively, I've been doing something like
theorem foo: "[| P a; P b |] ==> f a = f b"
by (drule unique, assumption, simp)
I can see why the simplification rule wont always be applied by
Isabelle, as it would easily loop forever.
Still, what would be the best way to deal with this kind of
predicates? So that most of the deductions with them, and simple
examples such as theorem "foo", could be proved automatically?
Thanks!
Juan
Email Gateway (Aug 18 2022 at 14:23):From: Brian Huffman <brianh@cs.pdx.edu>
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,
Last updated: Nov 21 2024 at 12:39 UTC