Hi,
Dear All,
I am working in HOL4. I want to extract the domain of the set of binary
relations.
For example, when I tried this goal,
g `! S. (FST (S CROSS S)) SUBSET (FST (S CROSS S))`;
It could not run. Can any one guide me?
Regards,
Nadeem Iqbal
HoD School of Computing and Information Scie
``S CROSS S`` is a set of pairs. Although ``S`` is usually parsed as a
constant, so you might want to use a different letter, or use Parse.hide"S".
Do you want the set of first components of the pairs? That would be ``IMAGE
FST (S CROSS S)``, and should be equal to ``S``.
On 5 February 2016 at 14
Yes, I want the set of first components of the pairs. I replaced S with A,
and used IMAGE FST (A CROSS A), but the problem is not solved.
On Fri, Feb 5, 2016 at 8:52 AM, Ramana Kumar
wrote:
> ``S CROSS S`` is a set of pairs. Although ``S`` is usually parsed as a
> constant, so you might want t
What's the problem/what is going wrong?
On 5 February 2016 at 17:48, Nadeem Iqbal wrote:
> Yes, I want the set of first components of the pairs. I replaced S with A,
> and used IMAGE FST (A CROSS A), but the problem is not solved.
>
>
>
> On Fri, Feb 5, 2016 at 8:52 AM, Ramana Kumar
> wrote:
>
Your original goal seemed to be just an instance of
pred_setTheory.SUBSET_REFL
|- !s. s SUBSET s
Are you actually trying to prove:
!A. IMAGE FST (A CROSS A) SUBSET A
?
If so, you could have:
Q.prove(
`!A. IMAGE FST (A CROSS A) SUBSET A`,
simp [pred_setTheory.SUBSET_DEF]
\\ metis_tac
Many thanks to Mr. Ramana Kumar and Mr. Anthony Fox for their kind help.
The goal got accepted upon proper parenthesisation.
Regards,
Nadeem
On Fri, Feb 5, 2016 at 1:56 PM, Anthony Fox wrote:
> Your original goal seemed to be just an instance of
>
> pred_setTheory.SUBSET_REFL
>
> |- !s. s SU
