Hi,
there is "GEN_EXISTS_TAC "y" `5`" from bossLib. It is more general than
what was asked for here originally. It also knows about the usual
boolean connectives.
For example, it can instantiate also
?x. P x /\ ?z y. ... y ...
or with negation
?x. (P x /\ (!z y. ... y ...)) ==> Q x
"GEN_EXISTS_TAC" is a special case of quantHeuristicsLib.QUANT_TAC.
This one allows _partially_ instantiating multiple variables in one go,
whereas "GEN_EXISTS_TAC" allows _completely_ instantiating_ one var.
With QUANT_TAC you can for example instantiate "l" in the following
`?x l. (HD l > x /\ P x l)`
with "QUANT_TAC [("l", `(SUC x)::(l1++l2)` [`l1`])]" to get
`?x l1. HD ((SUC x) :: (l1++l2)) /\ P x ((SUC x) :: (l1++l2))`
notice that "QUANT_TAC [("l", `(SUC x)::(l1++l2)` [`x`, `l1`])]" would
lead to
`?x x' l1. HD ((SUC x') :: (l1++l2)) /\ P x ((SUC x') :: (l1++l2))`
Best
Thomas
On 22.03.2016 04:08, Yong Kiam wrote:
> Out of curiosity:
>
> How would one do the instantiation that Magnus doesn't need i.e.
> instantiate using (and under) and existential?
>
> On Tue, Mar 22, 2016 at 4:12 AM, Ramana Kumar <ramana.ku...@cl.cam.ac.uk
> <mailto:ramana.ku...@cl.cam.ac.uk>> wrote:
>
> Yes there is:
> CONV_TAC(RESORT_EXISTS_CONV(sort_vars["y"])) \\ qexists_tac`5`
>
> On 22 March 2016 at 07:08, Magnus Myreen <mo...@cam.ac.uk
> <mailto:mo...@cam.ac.uk>> wrote:
>
> Hi hol-info,
>
> Quick question: is there a tactic for instantiating a nested
> existential based on a name? Example: for a goal such as
>
> ?x y z. ... y ...
>
> I want to use a tactic foo_tac `y` `5` and get:
>
> ?x z. ... 5 ...
>
> Is there such a foo_tac tactic? I suspect this functionality is
> there
> somewhere already. If not, then I'll implement it.
>
> Note: I don't need the advanced feature of being able to instantiate
> it with `x+z+1` where the variables refer to the other existentially
> quantified variables.
>
> Many thanks,
> Magnus
>
>
> ------------------------------------------------------------------------------
> Transform Data into Opportunity.
> Accelerate data analysis in your applications with
> Intel Data Analytics Acceleration Library.
> Click to learn more.
> http://pubads.g.doubleclick.net/gampad/clk?id=278785351&iu=/4140
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> <mailto:hol-info@lists.sourceforge.net>
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
>
>
> ------------------------------------------------------------------------------
> Transform Data into Opportunity.
> Accelerate data analysis in your applications with
> Intel Data Analytics Acceleration Library.
> Click to learn more.
> http://pubads.g.doubleclick.net/gampad/clk?id=278785351&iu=/4140
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net>
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
>
>
> ------------------------------------------------------------------------------
> Transform Data into Opportunity.
> Accelerate data analysis in your applications with
> Intel Data Analytics Acceleration Library.
> Click to learn more.
> http://pubads.g.doubleclick.net/gampad/clk?id=278785351&iu=/4140
>
>
>
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
Transform Data into Opportunity.
Accelerate data analysis in your applications with
Intel Data Analytics Acceleration Library.
Click to learn more.
http://pubads.g.doubleclick.net/gampad/clk?id=278785351&iu=/4140
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
