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