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 []
)
However, it may be better to prove a lemma for this, as it could be useful
elsewhere. For example:
val image_fst_cross = Q.prove(
`!A B. IMAGE FST (A CROSS B) = if B = EMPTY then EMPTY else A`,
rw [pred_setTheory.EXTENSION, pred_setTheory.IN_CROSS,
pred_setTheory.IN_IMAGE]
\\ eq_tac
\\ rw [] >- metis_tac []
\\ fs []
\\ qexists_tac `(x, x')`
\\ simp []
)
(There’s probably a nicer way of proving the above lemma.)
With this, the following works
Q.prove(
`!A. IMAGE FST (A CROSS A) SUBSET A`, rw [image_fst_cross])
Anthony
> On 5 Feb 2016, at 07:19, Ramana Kumar <[email protected]> wrote:
>
> What's the problem/what is going wrong?
>
> On 5 February 2016 at 17:48, Nadeem Iqbal <[email protected]> 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 <[email protected]>
> wrote:
> ``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:42, Nadeem Iqbal <[email protected]> wrote:
> 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 Sciences,
> Imperial College of Business Studies,
> Lahore, Pakistan.
>
>
> ------------------------------------------------------------------------------
> Site24x7 APM Insight: Get Deep Visibility into Application Performance
> APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
> Monitor end-to-end web transactions and take corrective actions now
> Troubleshoot faster and improve end-user experience. Signup Now!
> http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
>
>
> ------------------------------------------------------------------------------
> Site24x7 APM Insight: Get Deep Visibility into Application Performance
> APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
> Monitor end-to-end web transactions and take corrective actions now
> Troubleshoot faster and improve end-user experience. Signup Now!
> http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140_______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
