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 <[email protected]> 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 []
> )
>
> 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
