7 views

Skip to first unread message

Feb 24, 2009, 10:41:44 AM2/24/09

to vdash

I'm an Isabelle novice.

Let there is therorem "exists X such that P(X)". I want to define Y as

arbitrarily chosen (fixed) X confirming to this theorem.

What is the syntax for this?

Let there is therorem "exists X such that P(X)". I want to define Y as

arbitrarily chosen (fixed) X confirming to this theorem.

What is the syntax for this?

Feb 24, 2009, 10:06:32 AM2/24/09

to vd...@googlegroups.com

On Tue, Feb 24, 2009 at 07:41:44AM -0800, Victor Porton wrote:

>

> I'm an Isabelle novice.

>

> Let there is therorem "exists X such that P(X)". I want to define Y as

> arbitrarily chosen (fixed) X confirming to this theorem.

>

> I'm an Isabelle novice.

>

> Let there is therorem "exists X such that P(X)". I want to define Y as

> arbitrarily chosen (fixed) X confirming to this theorem.

Would being able to use this notation be equivalent to the axiom of

choice?

-- hendrik

Feb 24, 2009, 12:33:43 PM2/24/09

to vdash

> Let there is therorem "exists X such that P(X)". I want to define Y as

> arbitrarily chosen (fixed) X confirming to this theorem.

>

> What is the syntax for this?

Then you can say in some proof:

obtain Y where "P(Y)" using my_theorem by auto

From that point on you can refer to the set Y and its property P(Y) in

this proof. This type of reasoning does not require the axiom of

choice.

Feb 24, 2009, 12:49:34 PM2/24/09

to vd...@googlegroups.com

24.02.09, 20:33, "slawekk" <skok...@yahoo.com>:

As far as I understand, "obtain" can be used only in proofs.

I want something similar to "obtain" but in definitions (outside of proofs).

Feb 24, 2009, 1:48:43 PM2/24/09

to vdash

>

> I want something similar to "obtain" but in definitions (outside of proofs).

If you had uniqueness you could use the "THE" keyword. Something like:
> I want something similar to "obtain" but in definitions (outside of proofs).

definition

"Q \<equiv> THE Y. P(Y)"

I used it a couple of times, although I prefer different ways of

getting the only set satisfying a predicate.

Since you don't have uniqueness you may check the similar SOME

construct.

definition

"Q \<equiv> SOME Y. P(Y)"

It might be what you want but I have never used it so I am not sure.

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu