From f52bc18b4c6ad674bf824a5dce8595d41b8ae4be Mon Sep 17 00:00:00 2001 From: Hrutvik Kanabar Date: Mon, 9 Sep 2024 23:32:25 +0100 Subject: [PATCH] Fix `pure_eval_surj` after change in HOL --- meta-theory/pure_eval_surjScript.sml | 45 +++++++++++++++------------- 1 file changed, 24 insertions(+), 21 deletions(-) diff --git a/meta-theory/pure_eval_surjScript.sml b/meta-theory/pure_eval_surjScript.sml index af85b701..146e2f24 100644 --- a/meta-theory/pure_eval_surjScript.sml +++ b/meta-theory/pure_eval_surjScript.sml @@ -353,27 +353,30 @@ Proof rw[] >> ‘LENGTH nl - n = 0’ by DECIDE_TAC >> simp[]) - >- (qspec_then ‘nl’ strip_assume_tac SNOC_CASES >> gvs[SNOC_APPEND] >> - rw[DISJ_EQ_IMP] >> - gvs[IS_PREFIX_SNOC |> REWRITE_RULE[SNOC_APPEND]] >> - gvs[IS_PREFIX_APPEND] >> - gvs[LIST_EQ_REWRITE,EL_APPEND_EQN,EL_REPLICATE] >> - first_x_assum(qspec_then ‘LENGTH l’ mp_tac) >> - rw[]) - >- (qspec_then ‘nl’ strip_assume_tac SNOC_CASES >> gvs[SNOC_APPEND] >> - rw[DISJ_EQ_IMP] >> - gvs[IS_PREFIX_SNOC |> REWRITE_RULE[SNOC_APPEND]] >> - gvs[IS_PREFIX_APPEND] >> - gvs[LIST_EQ_REWRITE,EL_APPEND_EQN,EL_REPLICATE] >> - first_x_assum(qspec_then ‘LENGTH l’ mp_tac) >> - rw[]) - >- (qspec_then ‘nl’ strip_assume_tac SNOC_CASES >> gvs[SNOC_APPEND] >> - rw[DISJ_EQ_IMP] >> - gvs[IS_PREFIX_SNOC |> REWRITE_RULE[SNOC_APPEND]] >> - gvs[IS_PREFIX_APPEND] >> - gvs[LIST_EQ_REWRITE,EL_APPEND_EQN,EL_REPLICATE] >> - rw[DISJ_EQ_IMP] >> - qexists_tac ‘LENGTH l’ >> rw[])) >> + >- ( + qspec_then ‘nl’ strip_assume_tac SNOC_CASES >> gvs[SNOC_APPEND] >> + rw[DISJ_EQ_IMP] >> gvs[IS_PREFIX_APPEND] >> + qsuff_tac ‘l' = []’ >- (rw[] >> gvs[]) >> + gvs[APPEND_EQ_APPEND, APPEND_EQ_CONS] >> + gvs[LIST_EQ_REWRITE, EL_REPLICATE, EL_APPEND_EQN] >> + pop_assum $ qspec_then ‘LENGTH l’ mp_tac >> simp[] + ) + >- ( + qspec_then ‘nl’ strip_assume_tac SNOC_CASES >> gvs[SNOC_APPEND] >> + rw[DISJ_EQ_IMP] >> gvs[IS_PREFIX_APPEND] >> + qsuff_tac ‘l' = []’ >- (rw[] >> gvs[]) >> + gvs[APPEND_EQ_APPEND, APPEND_EQ_CONS] >> + gvs[LIST_EQ_REWRITE, EL_REPLICATE, EL_APPEND_EQN] >> + pop_assum $ qspec_then ‘LENGTH l’ mp_tac >> simp[] + ) + >- ( + qspec_then ‘nl’ strip_assume_tac SNOC_CASES >> gvs[SNOC_APPEND] >> + rw[IS_PREFIX_APPEND] >> CCONTR_TAC >> gvs[] >> + gvs[APPEND_EQ_APPEND, APPEND_EQ_CONS] >> + gvs[LIST_EQ_REWRITE, EL_REPLICATE, EL_APPEND_EQN] >> + pop_assum $ qspec_then ‘LENGTH l’ mp_tac >> simp[] + ) + ) >> rw[] QED