> 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
