1structure ARM_prover_toolsLib :> ARM_prover_toolsLib = 2struct 3 4open Abbrev HolKernel boolLib bossLib Parse proofManagerLib; 5open arm_seq_monadTheory ; 6open tacticsLib inference_rulesTheory ARM_proverLib; 7open switching_lemma_helperTheory user_lemma_basicsTheory; 8 9(***************************************************) 10(* Tools to interact with ARM prover *) 11(* (and some tactics for mode mixes) *) 12(* Oliver Schwarz *) 13(***************************************************) 14 15 16structure Parse = 17struct 18open Parse 19val (Type,Term) = parse_from_grammars 20 user_lemma_basicsTheory.user_lemma_basics_grammars 21end; 22 23 24exception not_matched_pattern; 25 26val _ = temp_overload_on("priv_mode_constraints", ``priv_mode_constraints_v1``); 27val priv_mode_constraints_def = priv_mode_constraints_v1_def; 28 29 30fun add_to_simplist thm = simp_thms_list := (thm::(!simp_thms_list)); 31 32 33fun update_mode_changing_comp_list opr = mode_changing_comp_list := (opr::(! mode_changing_comp_list)); 34 35 36fun save_comb_thm (name, th, listelement) = 37 let val () = update_mode_changing_comp_list listelement 38 in 39 save_thm(name, th) 40 end; 41 42 43fun get_trans_thm uf = 44 if (uf ~~ ``priv_mode_constraints``) then 45 trans_priv_mode_constraints_thm 46 else if (uf ~~ ``strict_unt``) then 47 trans_strict_unt_thm 48 else 49 trans_empty_unt_thm; 50 51 52fun get_reflex_thm uf = 53 if (uf ~~``priv_mode_constraints``) then 54 reflex_priv_mode_constraints_thm 55 else if (uf ~~ ``strict_unt``) then 56 reflex_strict_unt_thm 57 else 58 reflex_empty_unt_thm; 59 60fun get_sim_reflex_thm uy = 61 if (uy ~~ ``priv_mode_similar``) then 62 reflex_priv_mode_similar_thm 63 else 64 reflex_empty_sim_thm; 65 66 67fun get_unt_def uf = 68 if (uf ~~ ``priv_mode_constraints``) then 69 priv_mode_constraints_def 70 else if (uf ~~ ``strict_unt``) then 71 strict_unt_def 72 else 73 empty_unt_def; 74 75 76fun get_sim_def uy = 77 if (uy ~~ ``priv_mode_similar``) then 78 priv_mode_similar_def 79 else if (uy ~~ ``empty_similar_def``) then 80 empty_sim_def 81 else 82 CONJ fixed_flags_def (CONJ fix_flags_def (CONJ empty_sim_def priv_mode_similar_def)) ; 83 84 85fun prove_it a src_inv trg_inv uf uy = 86 let val () = global_mode := ``16w:bool[5]`` 87 in 88 prove a src_inv trg_inv ([uf, uy, ``27w:word5``, ``_thm``]) ([(get_trans_thm uf), (get_reflex_thm uf), (get_unt_def uf), (get_sim_def uy), errorT_thm, (get_sim_reflex_thm uy)]) 89 end; 90 91fun obtain_proofs() = 92 case top_goals() of 93 [] => trivial_true 94 | (_, to_show)::_ => 95 let 96 val (rcstu, simp) = dest_comb to_show 97 val (rcst, unt) = dest_comb rcstu 98 val (rcs, i2) = dest_comb rcst 99 val (rc, i1) = dest_comb rcs 100 val (rel, comp) = dest_comb rc 101 val (thm, _) = prove_it comp i1 i2 unt simp 102 in 103 thm 104 end handle HOL_ERR _ => trivial_true 105 106fun GO_ON_TAC () = 107 let val thm = obtain_proofs () 108 in 109 ASSUME_TAC thm THEN FULL_SIMP_TAC (srw_ss()) [] 110 end; 111 112fun go_on cnt = case cnt of 113 0 => e(GO_ON_TAC()) 114 |1 => e(GO_ON_TAC()) 115 |_ => let val _= e(GO_ON_TAC()) in go_on (cnt-1) end; 116 117fun go_on_p cnt = go_on cnt; 118 119 120fun thm_prove a = 121 let val (cplx_thm, _) = (prove_it a ``assert_mode 16w`` ``assert_mode 16w`` ``empty_unt`` ``empty_sim``) 122 in 123 cplx_thm 124 end; 125 126fun thm_proveP a = 127 let val (cplx_thm, _) = (prove_it a ``assert_mode 16w`` ``comb_mode 16w 27w`` ``priv_mode_constraints`` ``priv_mode_similar``) 128 in 129 cplx_thm 130 end; 131 132 133fun thm_proveS a = 134 let val (cplx_thm, _) = (prove_it a ``assert_mode 16w`` ``assert_mode 16w`` ``strict_unt`` ``empty_sim``) 135 in 136 cplx_thm 137 end; 138 139 140fun prove_and_save (a, name) = 141 let val th = thm_prove a 142 in 143 save_thm(name, th) 144 end; 145 146 147fun prove_and_save_e (a, name) = 148 let val th = thm_prove a 149 in 150 save_thm(name, (MATCH_MP extras_lem2 th)) 151 end; 152 153fun prove_and_save_s (a, name) = 154 let val th = thm_proveS a 155 in 156 save_thm(name, (MATCH_MP extras_lem4 th)) 157 end; 158 159fun prove_and_save_p (a, name, lelement) = 160 let val th = thm_proveP a 161 in 162 save_comb_thm(name, th, lelement) 163 end; 164 165fun prove_and_save_p_helper (a, name) = 166 let val th = thm_proveP a 167 in 168 save_thm(name, th) 169 end; 170 171 172 173 174 175fun MODE_MIX_TAC newtrg (assumptions, gl) = 176 case (dest_term gl) of 177 COMB (rcstu, sim) 178 => (case dest_term rcstu of 179 COMB (rcst, unt) 180 => (case dest_term rcst of 181 COMB (rcs, i2) 182 => (case (dest_term rcs) of 183 COMB (rc, i1) => 184 (case (dest_term rc) of 185 COMB (rel, comp) => 186 if ((i2 ~~ ``mode_mix:(arm_state->bool)``) andalso ((unt ~~ ``priv_mode_constraints_v2a``) andalso (sim ~~ ``priv_mode_similar``))) 187 then ((SUBGOAL_THEN (mk_comb(mk_comb((mk_comb(rcs, newtrg)), (if (newtrg ~~ ``comb_mode 16w 19w``) then ``priv_mode_constraints_v2a`` else ``priv_mode_constraints_v1``)), sim)) (fn thm => RW_TAC (srw_ss()) [thm, mode_mix_upgrade])) (assumptions, gl)) 188 else (ALL_TAC (assumptions, gl)) 189 | _ => (ALL_TAC (assumptions, gl))) 190 | _ => (ALL_TAC (assumptions, gl))) 191 | _ => (ALL_TAC (assumptions, gl))) 192 | _ => (ALL_TAC (assumptions, gl))) 193 | _ => (ALL_TAC (assumptions, gl)); 194 195 196fun LITTLE_MODE_MIX_TAC newtrg (assumptions, gl) = 197 case (dest_term gl) of 198 COMB (rcstu, sim) 199 => (case dest_term rcstu of 200 COMB (rcst, unt) 201 => (case dest_term rcst of 202 COMB (rcs, i2) 203 => (case (dest_term rcs) of 204 COMB (rc, i1) => 205 (case (dest_term rc) of 206 COMB (rel, comp) => if (i2 ~~ ``little_mode_mix:(arm_state->bool)``) 207 then ((SUBGOAL_THEN (mk_comb(mk_comb((mk_comb(rcs, newtrg)),unt), sim)) (fn thm => RW_TAC (srw_ss()) [thm, little_mode_mix_upgrade])) (assumptions, gl)) 208 else (ALL_TAC (assumptions, gl)) 209 | _ => (ALL_TAC (assumptions, gl))) 210 | _ => (ALL_TAC (assumptions, gl))) 211 | _ => (ALL_TAC (assumptions, gl))) 212 | _ => (ALL_TAC (assumptions, gl))) 213 | _ => (ALL_TAC (assumptions, gl)); 214 215 216 217 218 219end 220