One more way of doing it, which actually uses modus ponens more directly:
let open lcsymtacs in
first_x_assum(fn th => first_assum (strip_assume_tac o MATCH_MP th))
end
On Tue, May 13, 2014 at 9:25 AM, Ramana Kumar <ramana.ku...@cl.cam.ac.uk>wrote:
> I suspect lcsymtacs.rfs[] (aka REV_FULL_SIMP_TAC (srw_ss()) []) will do it
> in your particular example.
>
> Alternatively, you could use REPEAT BasicProvers.VAR_EQ_TAC THEN
> FULL_SIMP_TAC std_ss [].
>
> These will all change your goal state in more ways than one.
>
>
> On Tue, May 13, 2014 at 9:01 AM, masoume tajvidi <mas.tajv...@gmail.com>wrote:
>
>> Hi ,
>> I have a subgoal like this:
>>
>> F
>> ------------------------------------
>> 0. (winner' = w) ⇒ (winner = w)
>> 1. Max_vote C' v' = (winner,max)
>> 2. Max_vote C' v = (winner',max')
>> 3. LENGTH v' = LENGTH v
>> 4. w ≠ 0
>> 5. ∀n. n < LENGTH v ⇒ (EL n v' = w) ∨ (EL n v = EL n v')
>> 6. Count w v > max'
>> 7. T
>> 8. Count w v' = max
>> 9. SUC C' = w
>> 10. Count w v' ≥ Count w v
>> 11. winner' ≤ C'
>> 12. winner ≤ C'
>> 13. (SUC C' = w) ⇒ ∀n. n ≤ C' ⇒ n ≠ w
>>
>> I need to reach *∀n. n ≤ C' ⇒ n ≠ w * as another assumption.
>> I think from Assumption 9 and 13 it is inferable, but do not know what
>> Tactic to use.
>> Could anybody suggest me some Tactics?
>>
>> Thank you:)
>>
>>
>>
>>
>> ------------------------------------------------------------------------------
>> "Accelerate Dev Cycles with Automated Cross-Browser Testing - For FREE
>> Instantly run your Selenium tests across 300+ browser/OS combos.
>> Get unparalleled scalability from the best Selenium testing platform
>> available
>> Simple to use. Nothing to install. Get started now for free."
>> http://p.sf.net/sfu/SauceLabs
>> _______________________________________________
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>>
>
------------------------------------------------------------------------------
"Accelerate Dev Cycles with Automated Cross-Browser Testing - For FREE
Instantly run your Selenium tests across 300+ browser/OS combos.
Get unparalleled scalability from the best Selenium testing platform available
Simple to use. Nothing to install. Get started now for free."
http://p.sf.net/sfu/SauceLabs
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
