1 2open HolKernel Parse boolLib bossLib; val _ = new_theory "milawa_soundness"; 3 4(* open prog_armTheory prog_ppcTheory prog_x86Theory; *) 5 6open helperLib set_sepTheory progTheory; 7open lisp_correctnessTheory milawa_proofpTheory lisp_semanticsTheory; 8 9infix \\ val op \\ = op THEN 10 11val R_exec_T_11 = prove( 12 ``!x y. R_exec x y ==> !z. SND y /\ R_exec x z ==> (y = z)``, 13 HO_MATCH_MP_TAC R_exec_ind \\ STRIP_TAC 14 \\ REPEAT STRIP_TAC \\ POP_ASSUM MP_TAC 15 \\ ONCE_REWRITE_TAC [R_exec_cases] 16 \\ FULL_SIMP_TAC std_ss [] 17 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 18 \\ IMP_RES_TAC R_ev_T_11 19 \\ FULL_SIMP_TAC std_ss [] \\ RES_TAC \\ FULL_SIMP_TAC std_ss []); 20 21val milawa_soundness_thm = save_thm("milawa_soundness_thm",let 22 val th1 = milawa_main_soundness 23 val th = jitawa_correctness_thm 24 val assum = fst (dest_imp (concl th1)) 25 val pc = find_term (can (match_term ``zPC xxx``)) (concl th |> rand) 26 val th = Q.INST [`input`|->`STRCAT MILAWA_CORE_TEXT rest`] th 27 val th = SPEC_BOOL_FRAME_RULE th assum 28 val (th,goal) = SPEC_WEAKEN_RULE th 29 ``zERROR_MESSAGE ex \/ 30 let output = compute_output cmds in 31 cond (EVERY line_ok output) * ~zS * ^pc * zLISP_OUTPUT 32 (IO_STREAMS "" (output_to_string output ++ "SUCCESS\n"),T)`` 33 val lemma = prove(goal, 34 SIMP_TAC std_ss [SEP_IMP_MOVE_COND,LET_DEF] \\ REPEAT STRIP_TAC 35 \\ MATCH_MP_TAC SEP_IMP_DISJ \\ SIMP_TAC std_ss [SEP_IMP_REFL] 36 \\ SIMP_TAC std_ss [SEP_IMP_def,SEP_EXISTS_THM] \\ REPEAT STRIP_TAC 37 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 38 \\ IMP_RES_TAC th1 \\ IMP_RES_TAC R_exec_T_11 39 \\ FULL_SIMP_TAC std_ss [LET_DEF]) 40 val th = MP th lemma 41 val th = th |> SIMP_RULE (std_ss++sep_cond_ss) [] |> REWRITE_RULE [SPEC_MOVE_COND] 42 val assum2 = fst (dest_imp (concl th)) 43 val goal = mk_imp(assum,assum2) 44 val lemma = prove(goal,SIMP_TAC std_ss [R_exec_TERMINATES_def] \\ METIS_TAC [th1]) 45 val th = DISCH_ALL (MP th (UNDISCH lemma)) 46 val th = REWRITE_RULE [GSYM SPEC_MOVE_COND] th 47 in th end); 48 49val _ = export_theory(); 50