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