4 *) |
4 *) |
5 |
5 |
6 header "Separation Logic Tactics" |
6 header "Separation Logic Tactics" |
7 |
7 |
8 theory Sep_Tactics |
8 theory Sep_Tactics |
9 imports Separation_Algebra |
9 imports Separation_Algebra |
|
10 uses "sep_tactics.ML" |
10 begin |
11 begin |
11 |
12 |
12 ML_file "sep_tactics.ML" |
|
13 |
13 |
14 text {* A number of proof methods to assist with reasoning about separation logic. *} |
14 text {* A number of proof methods to assist with reasoning about separation logic. *} |
15 |
15 |
16 |
16 |
17 section {* Selection (move-to-front) tactics *} |
17 section {* Selection (move-to-front) tactics *} |
18 |
18 |
|
19 ML {* |
|
20 fun sep_select_method n ctxt = |
|
21 Method.SIMPLE_METHOD' (sep_select_tac ctxt n); |
|
22 fun sep_select_asm_method n ctxt = |
|
23 Method.SIMPLE_METHOD' (sep_select_asm_tac ctxt n); |
|
24 *} |
|
25 |
19 method_setup sep_select = {* |
26 method_setup sep_select = {* |
20 Scan.lift Parse.int >> (fn n => fn ctxt => SIMPLE_METHOD' (sep_select_tac ctxt n)) |
27 Scan.lift Parse.int >> sep_select_method |
21 *} "Select nth separation conjunct in conclusion" |
28 *} "Select nth separation conjunct in conclusion" |
22 |
29 |
23 method_setup sep_select_asm = {* |
30 method_setup sep_select_asm = {* |
24 Scan.lift Parse.int >> (fn n => fn ctxt => SIMPLE_METHOD' (sep_select_asm_tac ctxt n)) |
31 Scan.lift Parse.int >> sep_select_asm_method |
25 *} "Select nth separation conjunct in assumptions" |
32 *} "Select nth separation conjunct in assumptions" |
26 |
33 |
27 |
34 |
28 section {* Substitution *} |
35 section {* Substitution *} |
29 |
36 |
|
37 ML {* |
|
38 fun sep_subst_method ctxt occs thms = |
|
39 SIMPLE_METHOD' (sep_subst_tac ctxt occs thms); |
|
40 fun sep_subst_asm_method ctxt occs thms = |
|
41 SIMPLE_METHOD' (sep_subst_asm_tac ctxt occs thms); |
|
42 |
|
43 val sep_subst_parser = |
|
44 Args.mode "asm" |
|
45 -- Scan.lift (Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) |
|
46 -- Attrib.thms; |
|
47 *} |
|
48 |
30 method_setup "sep_subst" = {* |
49 method_setup "sep_subst" = {* |
31 Scan.lift (Args.mode "asm" -- Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) -- |
50 sep_subst_parser >> |
32 Attrib.thms >> (fn ((asm, occs), thms) => fn ctxt => |
51 (fn ((asm, occs), thms) => fn ctxt => |
33 SIMPLE_METHOD' ((if asm then sep_subst_asm_tac else sep_subst_tac) ctxt occs thms)) |
52 (if asm then sep_subst_asm_method else sep_subst_method) ctxt occs thms) |
34 *} |
53 *} |
35 "single-step substitution after solving one separation logic assumption" |
54 "single-step substitution after solving one separation logic assumption" |
36 |
55 |
37 |
56 |
38 section {* Forward Reasoning *} |
57 section {* Forward Reasoning *} |
39 |
58 |
|
59 ML {* |
|
60 fun sep_drule_method thms ctxt = SIMPLE_METHOD' (sep_dtac ctxt thms); |
|
61 fun sep_frule_method thms ctxt = SIMPLE_METHOD' (sep_ftac ctxt thms); |
|
62 *} |
|
63 |
40 method_setup "sep_drule" = {* |
64 method_setup "sep_drule" = {* |
41 Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (sep_dtac ctxt thms)) |
65 Attrib.thms >> sep_drule_method |
42 *} "drule after separating conjunction reordering" |
66 *} "drule after separating conjunction reordering" |
43 |
67 |
44 method_setup "sep_frule" = {* |
68 method_setup "sep_frule" = {* |
45 Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (sep_ftac ctxt thms)) |
69 Attrib.thms >> sep_frule_method |
46 *} "frule after separating conjunction reordering" |
70 *} "frule after separating conjunction reordering" |
47 |
71 |
48 |
72 |
49 section {* Backward Reasoning *} |
73 section {* Backward Reasoning *} |
50 |
74 |
|
75 ML {* |
|
76 fun sep_rule_method thms ctxt = SIMPLE_METHOD' (sep_rtac ctxt thms) |
|
77 *} |
|
78 |
51 method_setup "sep_rule" = {* |
79 method_setup "sep_rule" = {* |
52 Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (sep_rtac ctxt thms)) |
80 Attrib.thms >> sep_rule_method |
53 *} "applies rule after separating conjunction reordering" |
81 *} "applies rule after separating conjunction reordering" |
54 |
82 |
55 |
83 |
56 section {* Cancellation of Common Conjuncts via Elimination Rules *} |
84 section {* Cancellation of Common Conjuncts via Elimination Rules *} |
57 |
85 |
95 end; |
123 end; |
96 |
124 |
97 fun sep_cancel_smart_tac_rules ctxt etacs = |
125 fun sep_cancel_smart_tac_rules ctxt etacs = |
98 sep_cancel_smart_tac ctxt (FIRST' ([atac] @ etacs)); |
126 sep_cancel_smart_tac ctxt (FIRST' ([atac] @ etacs)); |
99 |
127 |
100 val sep_cancel_syntax = Method.sections [ |
128 fun sep_cancel_method ctxt = |
101 Args.add -- Args.colon >> K (I, SepCancel_Rules.add)] >> K (); |
|
102 *} |
|
103 |
|
104 method_setup sep_cancel = {* |
|
105 sep_cancel_syntax >> (fn _ => fn ctxt => |
|
106 let |
129 let |
107 val etacs = map etac (SepCancel_Rules.get ctxt); |
130 val etacs = map etac (SepCancel_Rules.get ctxt); |
108 in |
131 in |
109 SIMPLE_METHOD' (sep_cancel_smart_tac_rules ctxt etacs) |
132 SIMPLE_METHOD' (sep_cancel_smart_tac_rules ctxt etacs) |
110 end) |
133 end; |
|
134 |
|
135 val sep_cancel_syntax = Method.sections [ |
|
136 Args.add -- Args.colon >> K (I, SepCancel_Rules.add)]; |
|
137 *} |
|
138 |
|
139 method_setup sep_cancel = {* |
|
140 sep_cancel_syntax >> K sep_cancel_method |
111 *} "Separating conjunction conjunct cancellation" |
141 *} "Separating conjunction conjunct cancellation" |
112 |
142 |
113 text {* |
143 text {* |
114 As above, but use blast with a depth limit to figure out where cancellation |
144 As above, but use blast with a depth limit to figure out where cancellation |
115 can be done. *} |
145 can be done. *} |
116 |
146 |
117 method_setup sep_cancel_blast = {* |
147 ML {* |
118 sep_cancel_syntax >> (fn _ => fn ctxt => |
148 fun sep_cancel_blast_method ctxt = |
119 let |
149 let |
120 val rules = SepCancel_Rules.get ctxt; |
150 val rules = SepCancel_Rules.get ctxt; |
121 val tac = Blast.depth_tac (ctxt addIs rules) 10; |
151 val tac = Blast.depth_tac (ctxt addIs rules) 10; |
122 in |
152 in |
123 SIMPLE_METHOD' (sep_cancel_smart_tac ctxt tac) |
153 SIMPLE_METHOD' (sep_cancel_smart_tac ctxt tac) |
124 end) |
154 end; |
|
155 *} |
|
156 |
|
157 method_setup sep_cancel_blast = {* |
|
158 sep_cancel_syntax >> K sep_cancel_blast_method |
125 *} "Separating conjunction conjunct cancellation using blast" |
159 *} "Separating conjunction conjunct cancellation using blast" |
126 |
160 |
127 end |
161 end |