t (top_goal());
val it = ([], fn): goal list * validation
t (top_goal());
Exception- HOL_ERR {message = "first subgoal not solved by second tactic",
origin_function = "THEN1", origin_structure = "Tactical"} raised
I didn't think there were any refs touched by t, but I'll have a look more
closely...
On Sun, Jun 16, 2013 at 10:21 PM, Konrad Slind <konrad.sl...@gmail.com>wrote:
> > Could you perhaps tell me what could possibly be behind the behaviour
> above?
>
> Superficial answer: refs
>
> Do you get the same behaviour if you invoke t away from the goalstack?
>
> t (top_goal()) = t (top_goal())
>
>
> Konrad.
>
>
> On Sun, Jun 16, 2013 at 3:03 PM, Ramana Kumar
> <ramana.ku...@cl.cam.ac.uk>wrote:
>
>> I have run into strange problem:
>> e(t); (* succeeds and proves the goal *)
>> b(); (* return to original goal *)
>> e(t); (* fails *)
>>
>> I'll copy the code for t below, but there's a lot of required context,
>> which I won't go into in this first message... Could you perhaps tell me
>> what could possibly be behind the behaviour above?
>>
>> My t is (tac >> t2), where
>> val t2 = metis_tac[RTC_TRANSITIVE,transitive_def]
>> val tac =
>> rpt gen_tac >>
>> Q.PAT_ABBREV_TAC`cs1:compiler_result = X exp` >>
>>
>> qspecl_then[`cmnv`,`cenv`,`t`,`sz`,`exp'`,`0`,`cs1`,`1`](Q.X_CHOOSE_THEN`cb`strip_assume_tac)(CONJUNCT1
>> (CONJUNCT2 compile_append_out)) >>
>> simp[Abbr`cs1`] >>
>> REWRITE_TAC[Once SWAP_REVERSE] >>
>> simp[] >> strip_tac >>
>> qpat_assum`(A.out = cb ++ B)`mp_tac >>
>> Q.PAT_ABBREV_TAC`cs1:compiler_result = X exp` >> strip_tac >>
>> qabbrev_tac`tt = case t of TCNonTail => t | TCTail j k => TCTail
>> j (k + 1)` >>
>>
>> qspecl_then[`cmnv`,`CTLet(sz+1)::cenv`,`tt`,`sz+1`,`cs1`,`exp'`](Q.X_CHOOSE_THEN`cd`strip_assume_tac)(CONJUNCT1
>> compile_append_out) >>
>> first_x_assum(qspecl_then[`rd'`,`cmnv`,`cs1`,`CTLet
>> (sz+1)::cenv`,`sz+1`,`csz`,`bs2`,`bce`,`bcr`
>> ,`bc0 ++ REVERSE cc`
>> ,`REVERSE cd`,`(DROP (LENGTH cd)
>> (REVERSE cb))++bc1`]mp_tac) >>
>> discharge_hyps >- (
>> simp[TAKE_APPEND1,TAKE_APPEND2,Abbr`bs2`] >>
>> conj_asm1_tac >- (
>>
>> qspecl_then[`cmnv`,`cenv`,`t`,`sz`,`exp'`,`0`,`cs1`,`1`,`cb`,`cd`]mp_tac
>> compile_bindings_thm >>
>> simp[DROP_APPEND1,DROP_LENGTH_NIL_rwt] ) >>
>> conj_tac >- PROVE_TAC[] >>
>>
>> fs[Cenv_bs_def,s_refs_def,SUM_APPEND,FILTER_APPEND,ALL_DISTINCT_APPEND,FILTER_REVERSE,EVERY_REVERSE]
>> >>
>>
>> fsrw_tac[DNF_ss][MEM_FILTER,EVERY_MEM,is_Label_rwt,ALL_DISTINCT_REVERSE,MEM_MAP,between_def]
>> >>
>> fsrw_tac[ARITH_ss][Abbr`cs1`] >>
>> rw[] >> spose_not_then strip_assume_tac >> res_tac >>
>> fsrw_tac[ARITH_ss][] ) >>
>> simp[] >>
>> disch_then(qspec_then`tt`mp_tac) >>
>> TRY(disch_then(qspecl_then[`bv::ig`,`sp`,`hdl`,`st`]mp_tac)) >>
>> discharge_hyps >- (
>> simp[Abbr`bs2`] >>
>> simp[Abbr`tt`] >>
>> Cases_on`t`>>fs[] >>
>> qexists_tac`bv::blvs`>>simp[]>>
>> qexists_tac`args`>>simp[])
>>
>>
>>
>> ------------------------------------------------------------------------------
>> This SF.net email is sponsored by Windows:
>>
>> Build for Windows Store.
>>
>> http://p.sf.net/sfu/windows-dev2dev
>> _______________________________________________
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>>
>
------------------------------------------------------------------------------
This SF.net email is sponsored by Windows:
Build for Windows Store.
http://p.sf.net/sfu/windows-dev2dev
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
