The x and y should be universally quantified in Ramana's suggestion:
relations A = { R | !x y. R x y ==> x IN A /\ y IN A }
Michael
> On 21 Nov 2015, at 01:46, Ramana Kumar <ram...@member.fsf.org> wrote:
>
> maybe this?
> val relns_def = Define`relns A = { R | R x y ==> x IN A /\ y IN A }`
>
> On 20 November 2015 at 14:29, Muhammad Nadeem Iqbal
> <muhammadnadeemiq...@uoslahore.edu.pk> wrote:
>> Let me rephrase my problem:
>>
>> I have a set A and I want the definition of set of binary relations between
>> A and A in HOL.
>>
>> Regards,
>> Nadeem
>>
>> On Thu, Nov 19, 2015 at 4:21 PM, Yong Kiam <tanyongk...@gmail.com> wrote:
>>>
>>> Or you can type annotate them:
>>>
>>> Define`numeq (x:num) y <=> x = y`
>>>
>>> which gives numeq with type num -> num -> bool
>>>
>>> On Thu, Nov 19, 2015 at 7:14 PM, Ramana Kumar <ram...@member.fsf.org>
>>> wrote:
>>>>
>>>> How about this?
>>>> Define`issucsuc x y <=> x < y /\ (y - 2 = x)`;
>>>>
>>>> On 19 November 2015 at 10:31, Muhammad Nadeem Iqbal
>>>> <muhammadnadeemiq...@uoslahore.edu.pk> wrote:
>>>>> in your first example, you have specified two constants to x and y.
>>>>> Mine is
>>>>> a bit different case. I want the one in which there should not be such
>>>>> specification.
>>>>>
>>>>> On Wed, Nov 18, 2015 at 10:28 PM, Ramana Kumar <ram...@member.fsf.org>
>>>>> wrote:
>>>>>>
>>>>>> Which binary relation? What do you mean?
>>>>>>
>>>>>> Here's a binary relation that relates natural numbers 1 and 2:
>>>>>> val a_binary_relation_def = Define`a_binary_relation x y <=> (x = 1)
>>>>>> /\ (y
>>>>>> = 2)`;
>>>>>>
>>>>>> Here's a binary relation that relates two Booleans iff exactly one of
>>>>>> them
>>>>>> is true:
>>>>>> val another_binary_relation_def = Define`
>>>>>> (another_binary_relation T T = F) /\
>>>>>> (another_binary_relation T F = T) /\
>>>>>> (another_binary_relation F T = T) /\
>>>>>> (another_binary_relation F F = F)`;
>>>>>>
>>>>>> On 18 November 2015 at 17:01, Muhammad Nadeem Iqbal
>>>>>> <muhammadnadeemiq...@uoslahore.edu.pk> wrote:
>>>>>>>
>>>>>>> I have a query that how can we define a binary relation in HOL with a
>>>>>>> specified type?
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>> ------------------------------------------------------------------------------
>>>>>>>
>>>>>>> _______________________________________________
>>>>>>> hol-info mailing list
>>>>>>> hol-info@lists.sourceforge.net
>>>>>>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>>>>>>
>>>>>>
>>>>>
>>>>>
>>>>>
>>>>> ------------------------------------------------------------------------------
>>>>>
>>>>> _______________________________________________
>>>>> hol-info mailing list
>>>>> hol-info@lists.sourceforge.net
>>>>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>>>>
>>>>
>>>>
>>>> ------------------------------------------------------------------------------
>>>> _______________________________________________
>>>> hol-info mailing list
>>>> hol-info@lists.sourceforge.net
>>>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>>
>>>
>>
>
> ------------------------------------------------------------------------------
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
________________________________
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
