|
1 (* Title: Tactics for abstract separation algebras |
|
2 Authors: Gerwin Klein and Rafal Kolanski, 2012 |
|
3 Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au> |
|
4 Rafal Kolanski <rafal.kolanski at nicta.com.au> |
|
5 *) |
|
6 |
|
7 (* Separating Conjunction (and Top, AKA sep_true) {{{ |
|
8 |
|
9 This defines all the constants and theorems necessary for the conjunct |
|
10 selection and cancelling tactic, as well as utility functions. |
|
11 *) |
|
12 |
|
13 structure SepConj = |
|
14 struct |
|
15 |
|
16 val sep_conj_term = @{term sep_conj}; |
|
17 val sep_conj_str = "**"; |
|
18 val sep_conj_ac = @{thms sep_conj_ac}; |
|
19 val sep_conj_impl = @{thm sep_conj_impl} |
|
20 |
|
21 fun is_sep_conj_const (Const (@{const_name sep_conj}, _)) = true |
|
22 | is_sep_conj_const _ = false; |
|
23 |
|
24 fun is_sep_conj_term |
|
25 (Const t $ _ $ _ $ _) = is_sep_conj_const (Const t) |
|
26 | is_sep_conj_term _ = false; |
|
27 |
|
28 fun is_sep_conj_prop |
|
29 (Const Trueprop $ t) = is_sep_conj_term t |
|
30 | is_sep_conj_prop _ = false; |
|
31 |
|
32 fun break_sep_conj (Const (@{const_name sep_conj},_) $ t1 $ t2 $ _) = |
|
33 [t1] @ (break_sep_conj t2) |
|
34 | break_sep_conj (Const (@{const_name sep_conj},_) $ t1 $ t2) = |
|
35 [t1] @ (break_sep_conj t2) |
|
36 (* dig through eta exanded terms: *) |
|
37 | break_sep_conj (Abs (_, _, t $ Bound 0)) = break_sep_conj t |
|
38 | break_sep_conj t = [t]; |
|
39 |
|
40 fun is_sep_true_term (Abs (_, _, Const (@{const_name True}, _))) = true |
|
41 | is_sep_true_term _ = false; |
|
42 |
|
43 end; |
|
44 |
|
45 (* }}} *) |
|
46 |
|
47 (* Convenience functions for lists {{{ *) |
|
48 structure ListExtra = |
|
49 struct |
|
50 |
|
51 fun init l = List.take (l, List.length l - 1); |
|
52 |
|
53 fun range _ 0 = [] |
|
54 | range from howmany = from :: (range (from+1) (howmany-1)); |
|
55 |
|
56 (* move nth element in list to the front *) |
|
57 fun nth_to_front i xs = |
|
58 (nth xs i) :: (List.take (xs, i)) @ (List.drop (xs,i+1)); |
|
59 |
|
60 (* assign all members of list an index in the list *) |
|
61 fun index_list xs = ListPair.zip (range 0 (length xs), xs); |
|
62 |
|
63 end; (* }}} *) |
|
64 |
|
65 (* Function application terms {{{ *) |
|
66 (* Dealing with function applications of the type |
|
67 Const/Free(name,type) $ arg1 $ arg2 $ ... $ last_arg *) |
|
68 structure FunApp = |
|
69 struct |
|
70 |
|
71 (* apply a transformation to the args in a function application term *) |
|
72 fun app_args_op f t = strip_comb t |> apsnd f |> list_comb; |
|
73 |
|
74 (* remove last argument *) |
|
75 fun app_del_last_arg t = app_args_op ListExtra.init t; |
|
76 |
|
77 (* apply a function term to a Free with given name *) |
|
78 fun fun_app_free t free_name = t $ Free (free_name, type_of t |> domain_type); |
|
79 |
|
80 (* fold two-argument function over a list of arg names using fun_app_free *) |
|
81 fun fun_app_foldr f [a,b] = fun_app_free (fun_app_free f a) b |
|
82 | fun_app_foldr f (x::xs) = (fun_app_free f x) $ (fun_app_foldr f xs) |
|
83 | fun_app_foldr _ _ = raise Fail "fun_app_foldr"; |
|
84 |
|
85 end; (* }}} *) |
|
86 |
|
87 (* Selecting Conjuncts in Premise or Conclusion {{{ *) |
|
88 |
|
89 (* Constructs a rearrangement lemma of the kind: |
|
90 (A ** B ** C) s ==> (C ** A ** B) s |
|
91 When cjt_select = 2 (0-based index of C) and |
|
92 cjt_select = 3 (number of conjuncts to use), conclusion = true |
|
93 "conclusion" specifies whether the rearrangement occurs in conclusion |
|
94 (for dtac) or the premise (for rtac) of the rule. |
|
95 *) |
|
96 fun mk_sep_select_rule ctxt conclusion (cjt_count, cjt_select) = |
|
97 let |
|
98 fun variants nctxt names = fold_map Name.variant names nctxt; |
|
99 |
|
100 val (state, nctxt0) = Name.variant "s" (Variable.names_of ctxt); |
|
101 fun sep_conj_prop cjts = |
|
102 FunApp.fun_app_free |
|
103 (FunApp.fun_app_foldr SepConj.sep_conj_term cjts) state |
|
104 |> HOLogic.mk_Trueprop; |
|
105 |
|
106 (* concatenate string and string of an int *) |
|
107 fun conc_str_int str int = str ^ Int.toString int; |
|
108 |
|
109 (* make the conjunct names *) |
|
110 val (cjts, _) = ListExtra.range 1 cjt_count |
|
111 |> map (conc_str_int "a") |> variants nctxt0; |
|
112 |
|
113 (* make normal-order separation conjunction terms *) |
|
114 val orig = sep_conj_prop cjts; |
|
115 |
|
116 (* make reordered separation conjunction terms *) |
|
117 val reordered = sep_conj_prop (ListExtra.nth_to_front cjt_select cjts); |
|
118 |
|
119 val goal = Logic.mk_implies |
|
120 (if conclusion then (orig, reordered) else (reordered, orig)); |
|
121 |
|
122 (* simp add: sep_conj_ac *) |
|
123 val sep_conj_ac_tac = Simplifier.asm_full_simp_tac |
|
124 (put_simpset HOL_basic_ss ctxt addsimps SepConj.sep_conj_ac); |
|
125 |
|
126 in |
|
127 (* XXX: normally you'd want to keep track of what variables we want to make |
|
128 schematic and which ones are bound, but we don't use fixed names for |
|
129 the rules we make, so we use Drule.export_without_context to schematise |
|
130 all. *) |
|
131 Goal.prove ctxt [] [] goal (fn _ => sep_conj_ac_tac 1) |
|
132 |> Drule.export_without_context |
|
133 end; |
|
134 |
|
135 (* }}} *) |
|
136 |
|
137 local |
|
138 (* Common tactic functionality {{{ *) |
|
139 |
|
140 (* given two terms of some 'a to bool, can you prove |
|
141 \<And>s. t1 s \<Longrightarrow> t2 s |
|
142 using the supplied proof method? |
|
143 NOTE: t1 and t2 MUST have a function type with one argument, |
|
144 or TYPE dest_Type is raised |
|
145 NOTE: if asm or concl is sep_true, returns false |
|
146 *) |
|
147 fun can_prove ctxt tac asm concl = |
|
148 let |
|
149 fun variant name = Name.variant name (Variable.names_of ctxt) |> fst; |
|
150 val arg_name = variant "s"; |
|
151 val left = FunApp.fun_app_free asm arg_name |> HOLogic.mk_Trueprop; |
|
152 val right = FunApp.fun_app_free concl arg_name |> HOLogic.mk_Trueprop; |
|
153 val goal = Logic.mk_implies (left, right); |
|
154 in |
|
155 if (SepConj.is_sep_true_term asm) orelse (SepConj.is_sep_true_term concl) |
|
156 then false |
|
157 else (Goal.prove ctxt [] [] goal (fn _ => tac 1); true) |
|
158 handle ERROR _ => false |
|
159 end; |
|
160 |
|
161 (* apply function in list until it returns SOME *) |
|
162 fun find_some (x::xs) f = |
|
163 (case f x of SOME v => SOME v |
|
164 | NONE => find_some xs f) |
|
165 | find_some [] _ = NONE; |
|
166 |
|
167 (* Given indices into the separating conjunctions in the assumption and |
|
168 conclusion, rewrite them so that the targeted conjuncts are at the |
|
169 front, then remove them. *) |
|
170 fun eliminate_target_tac ctxt tac |
|
171 ((prem_total,prem_idx), (concl_total,concl_idx)) = |
|
172 let |
|
173 val asm_select = mk_sep_select_rule ctxt true (prem_total,prem_idx); |
|
174 val concl_select = mk_sep_select_rule ctxt false |
|
175 (concl_total,concl_idx); |
|
176 in |
|
177 dtac asm_select THEN' rtac concl_select |
|
178 THEN' etac SepConj.sep_conj_impl THEN' tac |
|
179 end; |
|
180 |
|
181 fun find_target ctxt tac cprem cconcl = |
|
182 let |
|
183 val prem_cjts = cprem |> term_of |> SepConj.break_sep_conj; |
|
184 val concl_cjts = cconcl |> term_of |> SepConj.break_sep_conj; |
|
185 |
|
186 val iprems = ListExtra.index_list prem_cjts; |
|
187 val iconcls = ListExtra.index_list concl_cjts; |
|
188 |
|
189 fun can_prove' (pi,p) (ci,c) = |
|
190 if can_prove ctxt tac p c then SOME (pi, ci) else NONE; |
|
191 |
|
192 val target = find_some iconcls |
|
193 (fn c => find_some iprems (fn p => can_prove' p c)); |
|
194 in |
|
195 case target |
|
196 of SOME (pi,ci) => SOME ((List.length prem_cjts, pi), |
|
197 (List.length concl_cjts, ci)) |
|
198 | NONE => NONE |
|
199 end; |
|
200 |
|
201 fun strip_cprop ct = |
|
202 let val thy = theory_of_cterm ct |
|
203 in ct |> term_of |> HOLogic.dest_Trueprop |> cterm_of thy |
|
204 end; |
|
205 |
|
206 (* }}} *) |
|
207 in |
|
208 |
|
209 (* Tactic: Select nth conjunct in assumption {{{ *) |
|
210 local |
|
211 fun sep_select_asm_tac' ctxt n (ct, i) = |
|
212 let |
|
213 (* digging out prems *) |
|
214 val ((_, ct'), _) = Variable.focus_cterm ct ctxt; |
|
215 val prems = Drule.strip_imp_prems ct'; |
|
216 |
|
217 fun prem_ok ct = SepConj.is_sep_conj_prop (term_of ct) |
|
218 |
|
219 fun mk_tac prem = |
|
220 let |
|
221 val prem = HOLogic.dest_Trueprop (term_of prem) |
|
222 val p = length (SepConj.break_sep_conj prem) |
|
223 val th = mk_sep_select_rule ctxt true (p,n) |
|
224 handle Subscript => error "Conjunct index out of range" |
|
225 in |
|
226 dtac th i |
|
227 end; |
|
228 in |
|
229 if length prems = 0 |
|
230 then error ("No assumption of form: (_ " ^ SepConj.sep_conj_str ^ |
|
231 " _) _") |
|
232 else |
|
233 (* backtrack until first premise that does something *) |
|
234 map mk_tac (filter prem_ok prems) |> FIRST |
|
235 end; |
|
236 in |
|
237 fun sep_select_asm_tac ctxt n = CSUBGOAL (sep_select_asm_tac' ctxt (n-1)) |
|
238 end; (* }}} *) |
|
239 |
|
240 (* Tactic: Select nth conjunct in conclusion {{{ *) |
|
241 local |
|
242 fun sep_select_tac' ctxt n (ct, i) = |
|
243 let |
|
244 (* digging out conclusions *) |
|
245 val ((_, ct'), _) = Variable.focus_cterm ct ctxt; |
|
246 val concl = ct' |> Drule.strip_imp_concl |> term_of; |
|
247 val p = concl |> HOLogic.dest_Trueprop |> SepConj.break_sep_conj |
|
248 |> length; |
|
249 val th = mk_sep_select_rule ctxt false (p,n) |
|
250 handle Subscript => error "Conjunct index out of range" |
|
251 in |
|
252 if not (SepConj.is_sep_conj_prop concl) |
|
253 then error ("Goal not of form: (_ " ^ SepConj.sep_conj_str ^ " _) _") |
|
254 else rtac th i |
|
255 end; |
|
256 in |
|
257 fun sep_select_tac ctxt n = CSUBGOAL (sep_select_tac' ctxt (n-1)) |
|
258 end; (* }}} *) |
|
259 |
|
260 (* Tactic: for all reorderings of the premises try apply tac {{{ *) |
|
261 local |
|
262 fun sep_assm_tac' ctxt tac (ct,i) = |
|
263 let |
|
264 (* digging out prems *) |
|
265 val ((_, ct'), _) = Variable.focus_cterm ct ctxt; |
|
266 val prems = Drule.strip_imp_prems ct'; |
|
267 |
|
268 fun prem_ok ct = SepConj.is_sep_conj_prop (term_of ct) |
|
269 |
|
270 fun mk_tac prem = |
|
271 let |
|
272 val prem = HOLogic.dest_Trueprop (term_of prem) |
|
273 val p = length (SepConj.break_sep_conj prem) |
|
274 fun ord n = mk_sep_select_rule ctxt true (p,n) |
|
275 val ord_thms = map ord (0 upto p-1) |
|
276 in |
|
277 (dresolve_tac ord_thms THEN' tac) i |
|
278 end; |
|
279 in |
|
280 (* backtrack until first premise that does something *) |
|
281 map mk_tac (filter prem_ok prems) |> FIRST |
|
282 end; |
|
283 in |
|
284 fun sep_assm_tac ctxt tac = CSUBGOAL (sep_assm_tac' ctxt tac) |
|
285 end; (* }}} *) |
|
286 |
|
287 (* Tactic: for all reorderings of the conclusion, try apply tac {{{ *) |
|
288 local |
|
289 fun sep_concl_tac' ctxt tac (ct, i) = |
|
290 let |
|
291 (* digging out conclusion *) |
|
292 val ((_, ct'), _) = Variable.focus_cterm ct ctxt; |
|
293 val concl = ct' |> Drule.strip_imp_concl |> term_of; |
|
294 val p = concl |> HOLogic.dest_Trueprop |> SepConj.break_sep_conj |
|
295 |> length; |
|
296 fun ord n = mk_sep_select_rule ctxt false (p,n); |
|
297 val ord_thms = map ord (0 upto p-1); |
|
298 in |
|
299 if not (SepConj.is_sep_conj_prop concl) |
|
300 then (tracing ("Goal not of form: (_ " ^ SepConj.sep_conj_str ^ |
|
301 " _) _"); |
|
302 no_tac) |
|
303 else (resolve_tac ord_thms THEN' tac) i |
|
304 end; |
|
305 in |
|
306 fun sep_concl_tac ctxt tac = CSUBGOAL (sep_concl_tac' ctxt tac) |
|
307 end; (* }}} *) |
|
308 |
|
309 (* Tactic: Cancel conjuncts of assumption and conclusion via tac {{{ *) |
|
310 local |
|
311 fun sep_cancel_tac' ctxt tac (ct, i) = |
|
312 let |
|
313 (* digging out prems and conclusions *) |
|
314 val ((vars, ct'), ctxt') = Variable.focus_cterm ct ctxt; |
|
315 val concl = Drule.strip_imp_concl ct'; |
|
316 val prems = Drule.strip_imp_prems ct'; |
|
317 |
|
318 fun prem_ok ct = |
|
319 let |
|
320 (* name of state in sep conj (should be Free after focus) *) |
|
321 fun state_get (_ $ _ $ _ $ s) = s |
|
322 | state_get t = raise Fail "prem_ok: state_get"; |
|
323 val state_get_ct = state_get o HOLogic.dest_Trueprop o term_of; |
|
324 |
|
325 val concl_state = concl |> state_get_ct; |
|
326 (* states considered equal if they alpha-convert *) |
|
327 fun state_ok ct = (state_get_ct ct) aconv concl_state; |
|
328 in |
|
329 SepConj.is_sep_conj_prop (term_of ct) andalso state_ok ct |
|
330 end; |
|
331 |
|
332 fun mk_tac prem = |
|
333 case find_target ctxt tac (prem |> strip_cprop) |
|
334 (strip_cprop concl) |
|
335 of SOME target => eliminate_target_tac ctxt tac target i |
|
336 | NONE => no_tac; |
|
337 in |
|
338 if (not (concl |> term_of |> SepConj.is_sep_conj_prop)) |
|
339 then (tracing ("Goal not of form: (_ " ^ SepConj.sep_conj_str ^ |
|
340 " _) _"); |
|
341 no_tac) |
|
342 else if (length prems = 0) |
|
343 then (tracing ("No assumption of form: (_ " ^ SepConj.sep_conj_str ^ |
|
344 " _) _"); |
|
345 no_tac) |
|
346 else |
|
347 (* backtrack until first premise that does something *) |
|
348 map mk_tac (filter prem_ok prems) |> FIRST |
|
349 end; |
|
350 in |
|
351 fun sep_cancel_tac ctxt tac = CSUBGOAL (sep_cancel_tac' ctxt tac) |
|
352 end; |
|
353 (* }}} *) |
|
354 |
|
355 (* Derived Tactics *) |
|
356 |
|
357 fun sep_atac ctxt = sep_assm_tac ctxt atac; |
|
358 |
|
359 (* Substitution *) |
|
360 fun sep_subst_tac ctxt occs thms = |
|
361 EqSubst.eqsubst_tac ctxt occs thms THEN' sep_atac ctxt; |
|
362 fun sep_subst_asm_tac ctxt occs thms = |
|
363 EqSubst.eqsubst_asm_tac ctxt occs thms THEN' sep_atac ctxt; |
|
364 |
|
365 (* Forward reasoning *) |
|
366 fun sep_dtac ctxt thms = sep_assm_tac ctxt (dresolve_tac thms) |
|
367 fun sep_ftac ctxt thms = sep_assm_tac ctxt (forward_tac thms) |
|
368 |
|
369 (* Backward reasoning *) |
|
370 fun sep_rtac ctxt thms = sep_concl_tac ctxt (resolve_tac thms) |
|
371 |
|
372 end; |
|
373 |
|
374 (* vim: set foldmethod=marker sw=2 sts=2 et: *) |
|
375 |