From 2fc3b9b98646e0fcef0eee47a1a5a8a41f02b22b Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Fri, 30 Aug 2019 11:15:10 +0200 Subject: [PATCH] Make a proof more robust I suggest avoiding use of EVAL_TAC if several lines of tactic follow the call to EVAL_TAC. --- compiler/backend/proofs/stack_to_labProofScript.sml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/compiler/backend/proofs/stack_to_labProofScript.sml b/compiler/backend/proofs/stack_to_labProofScript.sml index 8eb4bb5fc4..5895df3a91 100644 --- a/compiler/backend/proofs/stack_to_labProofScript.sml +++ b/compiler/backend/proofs/stack_to_labProofScript.sml @@ -1793,11 +1793,12 @@ Proof full_simp_tac(srw_ss())[call_args_def] >> var_eq_tac >> imp_res_tac find_code_lookup >> `dest_to_loc (s.regs \\ t1.link_reg) dest = dest_to_loc' t1.regs dest` by ( - EVAL_TAC >> - CASE_TAC >> full_simp_tac(srw_ss())[] >> + fs [dest_to_loc_def,dest_to_loc'_def] >> + TOP_CASE_TAC >> + fs [find_code_def,option_case_eq,CaseEq"word_loc",num_case_eq] >> + rveq >> fs [DOMSUB_FAPPLY_THM,FLOOKUP_DEF] >> qhdtm_x_assum`state_rel`mp_tac >> - simp[DOMSUB_FAPPLY_THM] >> - simp[state_rel_def,FLOOKUP_DEF] ) >> + simp[state_rel_def,FLOOKUP_DEF]) >> full_simp_tac(srw_ss())[] >> first_assum(fn th => first_assum( tryfind (strip_assume_tac o C MATCH_MP th) o CONJUNCTS o CONV_RULE (REWR_CONV state_rel_def))) >>