Re: [Hol-info] assumption matching in SPLIT_LT

2018-10-12 Thread Jeremy Dawson 

Hi Waqar,

Firstly (simplest),

SPLIT_LT 2 (ALLGOALS tac1, ALL_LT)

applies tac1 to the first two subgoals and does nothing to the 
remainder.  Then you can work on the remaining goal.


But you want to also apply EVERY [tac2, tac3, ...] to the third subgoal 
(which is the only remaining one), together in the same step.

  To package this as a list-tactic, you could do

val tac23 = EVERY [tac2, tac3, ...]

then val lt23 = ALLGOALS tac23
or val lt23 = TACS_TO_LT [tac23]

then what you ask would be achieved by
SPLIT_LT 2 (ALLGOALS tac1, lt23)

Cheers,

Jeremy


On 10/13/2018 03:38 AM, Waqar Ahmad via hol-info wrote:

Hi,

Suppose, I have 3 subgoals where first 2 subgoals can be proved by apply 
tac1 and the third goal may takes some set of tacts, say tac2, tac3...


Is it possible that I can use SPLIT_LT in a way such that first two 
subgoals are discharged by applying tac1 and I only end up proving the 
third subgoal?



On Fri, Sep 21, 2018 at 3:00 AM > wrote:


match_mp_tac is indeed causing an error because it is not applicable
in the other subgoals.

__ __

Michael

__ __

*From: *Waqar Ahmad via hol-info mailto:hol-info@lists.sourceforge.net>>
*Reply-To: *Waqar Ahmad <12phdwah...@seecs.edu.pk
>
*Date: *Friday, 21 September 2018 at 08:39
*To: *"konrad.sl...@gmail.com "
mailto:konrad.sl...@gmail.com>>
*Cc: *hol-info mailto:hol-info@lists.sourceforge.net>>
*Subject: *Re: [Hol-info] assumption matching in SPLIT_LT

__ __

Hi, 

__ __

Thanks for the reply. I think the match_mp_tac is causing the error
since if I only pop the assumption the tactic works on first
subgoal.

__ __

rw [] \\ (pop_assum (mp_tac)) THEN_LT SPLIT_LT 1 (ALL_LT, ALLGOALS
(rw[]))

__ __

__ __

 > val it =



    SG3

    

     A1 ==> B1





    SG2

    

     A1 ==> B1





    (A1 ==> B1) ==> B1





3 subgoals

    : proof

__ __

__ __

__ __

__ __

On Thu, Sep 20, 2018 at 6:21 PM Konrad Slind mailto:konrad.sl...@gmail.com>> wrote:

Seems like the rw[] is breaking the proof into 3 subgoals, and
only on the first one is the pop_assum match_mp_tac succeeding.
So the proof is failing before it gets to the THEN_LT. 

__ __

Konrad.

__ __

__ __

On Thu, Sep 20, 2018 at 2:05 PM Waqar Ahmad via hol-info
mailto:hol-info@lists.sourceforge.net>> wrote:

Hi, 

__ __

I'm trying to use the tactical SPLIT_LT to multiple
subgoals. However, I'm facing error with assumption
matching. For instance, I've a proof goal of this form:

__ __

`(A1 ==> B1) ==> (B1 /\ SG2 /\ SG3)`

__ __

rw [] 

\\ (pop_assum (fn th => match_mp_tac th)) THEN_LT SPLIT_LT 1
(ALL_LT, ALLGOALS (rw[]))

__ __

I'm getting following matching error...

__ __

Exception raised at Tactic.MATCH_MP_TAC:

No match

Exception-

    HOL_ERR

      {message = "No match", origin_function =
"MATCH_MP_TAC",

       origin_structure = "Tactic"} raised

__ __

It works otherwise for handling them individually...

-- 

Waqar Ahmad, Ph.D.
Post Doc at Hardware Verification Group (HVG)
Department of Electrical and Computer Engineering
Concordia University, QC, Canada
Web: http://save.seecs.nust.edu.pk/waqar-ahmad/

___
hol-info mailing list
hol-info@lists.sourceforge.net

https://lists.sourceforge.net/lists/listinfo/hol-info




__ __

-- 

Waqar Ahmad, Ph.D.
Post Doc at Hardware Verification Group (HVG)
Department of Electrical and Computer Engineering
Concordia University, QC, Canada
Web: http://save.seecs.nust.edu.pk/waqar-ahmad/

___
hol-info mailing list
hol-info@lists.sourceforge.net 
https://lists.sourceforge.net/lists/listinfo/hol-info



--
Waqar Ahmad, Ph.D.
Post Doc at Hardware Verification Group (HVG)
Department of Electrical and Computer Engineering
Concordia University, QC, Canada
Web: http://save.seecs.nust.edu.pk/waqar-ahmad/

Re: [Hol-info] assumption matching in SPLIT_LT

2018-10-12 Thread Waqar Ahmad via hol-info 
Hi,

Suppose, I have 3 subgoals where first 2 subgoals can be proved by apply
tac1 and the third goal may takes some set of tacts, say tac2, tac3...

Is it possible that I can use SPLIT_LT in a way such that first two
subgoals are discharged by applying tac1 and I only end up proving the
third subgoal?


On Fri, Sep 21, 2018 at 3:00 AM  wrote:

> match_mp_tac is indeed causing an error because it is not applicable in
> the other subgoals.
>
>
>
> Michael
>
>
>
> *From: *Waqar Ahmad via hol-info 
> *Reply-To: *Waqar Ahmad <12phdwah...@seecs.edu.pk>
> *Date: *Friday, 21 September 2018 at 08:39
> *To: *"konrad.sl...@gmail.com" 
> *Cc: *hol-info 
> *Subject: *Re: [Hol-info] assumption matching in SPLIT_LT
>
>
>
> Hi,
>
>
>
> Thanks for the reply. I think the match_mp_tac is causing the error since
> if I only pop the assumption the tactic works on first subgoal.
>
>
>
> rw [] \\ (pop_assum (mp_tac)) THEN_LT SPLIT_LT 1 (ALL_LT, ALLGOALS (rw[]))
>
>
>
>
>
> > val it =
>
>
>
>SG3
>
>
>
> A1 ==> B1
>
>
>
>
>
>SG2
>
>
>
> A1 ==> B1
>
>
>
>
>
>(A1 ==> B1) ==> B1
>
>
>
>
>
> 3 subgoals
>
>: proof
>
>
>
>
>
>
>
>
>
> On Thu, Sep 20, 2018 at 6:21 PM Konrad Slind 
> wrote:
>
> Seems like the rw[] is breaking the proof into 3 subgoals, and only on the
> first one is the pop_assum match_mp_tac succeeding. So the proof is failing
> before it gets to the THEN_LT.
>
>
>
> Konrad.
>
>
>
>
>
> On Thu, Sep 20, 2018 at 2:05 PM Waqar Ahmad via hol-info <
> hol-info@lists.sourceforge.net> wrote:
>
> Hi,
>
>
>
> I'm trying to use the tactical SPLIT_LT to multiple subgoals. However, I'm
> facing error with assumption matching. For instance, I've a proof goal of
> this form:
>
>
>
> `(A1 ==> B1) ==> (B1 /\ SG2 /\ SG3)`
>
>
>
> rw []
>
> \\ (pop_assum (fn th => match_mp_tac th)) THEN_LT SPLIT_LT 1 (ALL_LT,
> ALLGOALS (rw[]))
>
>
>
> I'm getting following matching error...
>
>
>
> Exception raised at Tactic.MATCH_MP_TAC:
>
> No match
>
> Exception-
>
>HOL_ERR
>
>  {message = "No match", origin_function = "MATCH_MP_TAC",
>
>   origin_structure = "Tactic"} raised
>
>
>
> It works otherwise for handling them individually...
>
> --
>
> Waqar Ahmad, Ph.D.
> Post Doc at Hardware Verification Group (HVG)
> Department of Electrical and Computer Engineering
> Concordia University, QC, Canada
> Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
>
>
> --
>
> Waqar Ahmad, Ph.D.
> Post Doc at Hardware Verification Group (HVG)
> Department of Electrical and Computer Engineering
> Concordia University, QC, Canada
> Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>


-- 
Waqar Ahmad, Ph.D.
Post Doc at Hardware Verification Group (HVG)
Department of Electrical and Computer Engineering
Concordia University, QC, Canada
Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] assumption matching in SPLIT_LT

2018-09-21 Thread Michael.Norrish 
match_mp_tac is indeed causing an error because it is not applicable in the 
other subgoals.

Michael

From: Waqar Ahmad via hol-info 
Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Friday, 21 September 2018 at 08:39
To: "konrad.sl...@gmail.com" 
Cc: hol-info 
Subject: Re: [Hol-info] assumption matching in SPLIT_LT

Hi,

Thanks for the reply. I think the match_mp_tac is causing the error since if I 
only pop the assumption the tactic works on first subgoal.

rw [] \\ (pop_assum (mp_tac)) THEN_LT SPLIT_LT 1 (ALL_LT, ALLGOALS (rw[]))


> val it =

   SG3
   
A1 ==> B1


   SG2
   
A1 ==> B1


   (A1 ==> B1) ==> B1


3 subgoals
   : proof




On Thu, Sep 20, 2018 at 6:21 PM Konrad Slind 
mailto:konrad.sl...@gmail.com>> wrote:
Seems like the rw[] is breaking the proof into 3 subgoals, and only on the 
first one is the pop_assum match_mp_tac succeeding. So the proof is failing 
before it gets to the THEN_LT.

Konrad.


On Thu, Sep 20, 2018 at 2:05 PM Waqar Ahmad via hol-info 
mailto:hol-info@lists.sourceforge.net>> wrote:
Hi,

I'm trying to use the tactical SPLIT_LT to multiple subgoals. However, I'm 
facing error with assumption matching. For instance, I've a proof goal of this 
form:

`(A1 ==> B1) ==> (B1 /\ SG2 /\ SG3)`

rw []
\\ (pop_assum (fn th => match_mp_tac th)) THEN_LT SPLIT_LT 1 (ALL_LT, ALLGOALS 
(rw[]))

I'm getting following matching error...

Exception raised at Tactic.MATCH_MP_TAC:
No match
Exception-
   HOL_ERR
 {message = "No match", origin_function = "MATCH_MP_TAC",
  origin_structure = "Tactic"} raised

It works otherwise for handling them individually...
--
Waqar Ahmad, Ph.D.
Post Doc at Hardware Verification Group (HVG)
Department of Electrical and Computer Engineering
Concordia University, QC, Canada
Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
___
hol-info mailing list
hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>
https://lists.sourceforge.net/lists/listinfo/hol-info


--
Waqar Ahmad, Ph.D.
Post Doc at Hardware Verification Group (HVG)
Department of Electrical and Computer Engineering
Concordia University, QC, Canada
Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] assumption matching in SPLIT_LT

2018-09-20 Thread Waqar Ahmad via hol-info 
Hi,

Thanks for the reply. I think the match_mp_tac is causing the error since
if I only pop the assumption the tactic works on first subgoal.

rw [] \\ (pop_assum (mp_tac)) THEN_LT SPLIT_LT 1 (ALL_LT, ALLGOALS (rw[]))


> val it =

   SG3
   
A1 ==> B1


   SG2
   
A1 ==> B1


   (A1 ==> B1) ==> B1


3 subgoals
   : proof




On Thu, Sep 20, 2018 at 6:21 PM Konrad Slind  wrote:

> Seems like the rw[] is breaking the proof into 3 subgoals, and only on the
> first one is the pop_assum match_mp_tac succeeding. So the proof is failing
> before it gets to the THEN_LT.
>
> Konrad.
>
>
> On Thu, Sep 20, 2018 at 2:05 PM Waqar Ahmad via hol-info <
> hol-info@lists.sourceforge.net> wrote:
>
>> Hi,
>>
>> I'm trying to use the tactical SPLIT_LT to multiple subgoals. However,
>> I'm facing error with assumption matching. For instance, I've a proof goal
>> of this form:
>>
>> `(A1 ==> B1) ==> (B1 /\ SG2 /\ SG3)`
>>
>> rw []
>> \\ (pop_assum (fn th => match_mp_tac th)) THEN_LT SPLIT_LT 1 (ALL_LT,
>> ALLGOALS (rw[]))
>>
>> I'm getting following matching error...
>>
>> Exception raised at Tactic.MATCH_MP_TAC:
>> No match
>> Exception-
>>HOL_ERR
>>  {message = "No match", origin_function = "MATCH_MP_TAC",
>>   origin_structure = "Tactic"} raised
>>
>> It works otherwise for handling them individually...
>> --
>> Waqar Ahmad, Ph.D.
>> Post Doc at Hardware Verification Group (HVG)
>> Department of Electrical and Computer Engineering
>> Concordia University, QC, Canada
>> Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
>>
>> ___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>

-- 
Waqar Ahmad, Ph.D.
Post Doc at Hardware Verification Group (HVG)
Department of Electrical and Computer Engineering
Concordia University, QC, Canada
Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] assumption matching in SPLIT_LT

2018-09-20 Thread Konrad Slind 
Seems like the rw[] is breaking the proof into 3 subgoals, and only on the
first one is the pop_assum match_mp_tac succeeding. So the proof is failing
before it gets to the THEN_LT.

Konrad.


On Thu, Sep 20, 2018 at 2:05 PM Waqar Ahmad via hol-info <
hol-info@lists.sourceforge.net> wrote:

> Hi,
>
> I'm trying to use the tactical SPLIT_LT to multiple subgoals. However, I'm
> facing error with assumption matching. For instance, I've a proof goal of
> this form:
>
> `(A1 ==> B1) ==> (B1 /\ SG2 /\ SG3)`
>
> rw []
> \\ (pop_assum (fn th => match_mp_tac th)) THEN_LT SPLIT_LT 1 (ALL_LT,
> ALLGOALS (rw[]))
>
> I'm getting following matching error...
>
> Exception raised at Tactic.MATCH_MP_TAC:
> No match
> Exception-
>HOL_ERR
>  {message = "No match", origin_function = "MATCH_MP_TAC",
>   origin_structure = "Tactic"} raised
>
> It works otherwise for handling them individually...
> --
> Waqar Ahmad, Ph.D.
> Post Doc at Hardware Verification Group (HVG)
> Department of Electrical and Computer Engineering
> Concordia University, QC, Canada
> Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
>
> ___
> 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] assumption matching in SPLIT_LT

2018-09-20 Thread Waqar Ahmad via hol-info 
Hi,

I'm trying to use the tactical SPLIT_LT to multiple subgoals. However, I'm
facing error with assumption matching. For instance, I've a proof goal of
this form:

`(A1 ==> B1) ==> (B1 /\ SG2 /\ SG3)`

rw []
\\ (pop_assum (fn th => match_mp_tac th)) THEN_LT SPLIT_LT 1 (ALL_LT,
ALLGOALS (rw[]))

I'm getting following matching error...

Exception raised at Tactic.MATCH_MP_TAC:
No match
Exception-
   HOL_ERR
 {message = "No match", origin_function = "MATCH_MP_TAC",
  origin_structure = "Tactic"} raised

It works otherwise for handling them individually...
-- 
Waqar Ahmad, Ph.D.
Post Doc at Hardware Verification Group (HVG)
Department of Electrical and Computer Engineering
Concordia University, QC, Canada
Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info