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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
