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