1 (* Title: HOL/Tools/ATP/atp_redirect.ML |
|
2 Author: Jasmin Blanchette, TU Muenchen |
|
3 |
|
4 Transformation of a proof by contradiction into a direct proof. |
|
5 *) |
|
6 |
|
7 signature ATP_ATOM = |
|
8 sig |
|
9 type key |
|
10 val ord : key * key -> order |
|
11 val string_of : key -> string |
|
12 end; |
|
13 |
|
14 signature ATP_REDIRECT = |
|
15 sig |
|
16 type atom |
|
17 |
|
18 structure Atom_Graph : GRAPH |
|
19 |
|
20 type ref_sequent = atom list * atom |
|
21 type ref_graph = unit Atom_Graph.T |
|
22 |
|
23 type clause = atom list |
|
24 type direct_sequent = atom list * clause |
|
25 type direct_graph = unit Atom_Graph.T |
|
26 |
|
27 type rich_sequent = clause list * clause |
|
28 |
|
29 datatype direct_inference = |
|
30 Have of rich_sequent | |
|
31 Hence of rich_sequent | |
|
32 Cases of (clause * direct_inference list) list |
|
33 |
|
34 type direct_proof = direct_inference list |
|
35 |
|
36 val make_ref_graph : (atom list * atom) list -> ref_graph |
|
37 val axioms_of_ref_graph : ref_graph -> atom list -> atom list |
|
38 val tainted_atoms_of_ref_graph : ref_graph -> atom list -> atom list |
|
39 val sequents_of_ref_graph : ref_graph -> ref_sequent list |
|
40 val redirect_sequent : atom list -> atom -> ref_sequent -> direct_sequent |
|
41 val direct_graph : direct_sequent list -> direct_graph |
|
42 val redirect_graph : atom list -> atom list -> ref_graph -> direct_proof |
|
43 val succedent_of_cases : (clause * direct_inference list) list -> clause |
|
44 val chain_direct_proof : direct_proof -> direct_proof |
|
45 val string_of_direct_proof : direct_proof -> string |
|
46 end; |
|
47 |
|
48 functor ATP_Redirect(Atom : ATP_ATOM): ATP_REDIRECT = |
|
49 struct |
|
50 |
|
51 type atom = Atom.key |
|
52 |
|
53 structure Atom_Graph = Graph(Atom) |
|
54 |
|
55 type ref_sequent = atom list * atom |
|
56 type ref_graph = unit Atom_Graph.T |
|
57 |
|
58 type clause = atom list |
|
59 type direct_sequent = atom list * clause |
|
60 type direct_graph = unit Atom_Graph.T |
|
61 |
|
62 type rich_sequent = clause list * clause |
|
63 |
|
64 datatype direct_inference = |
|
65 Have of rich_sequent | |
|
66 Hence of rich_sequent | |
|
67 Cases of (clause * direct_inference list) list |
|
68 |
|
69 type direct_proof = direct_inference list |
|
70 |
|
71 fun atom_eq p = (Atom.ord p = EQUAL) |
|
72 fun clause_eq (c, d) = (length c = length d andalso forall atom_eq (c ~~ d)) |
|
73 fun direct_sequent_eq ((gamma, c), (delta, d)) = |
|
74 clause_eq (gamma, delta) andalso clause_eq (c, d) |
|
75 |
|
76 fun make_ref_graph infers = |
|
77 let |
|
78 fun add_edge to from = |
|
79 Atom_Graph.default_node (from, ()) |
|
80 #> Atom_Graph.default_node (to, ()) |
|
81 #> Atom_Graph.add_edge_acyclic (from, to) |
|
82 fun add_infer (froms, to) = fold (add_edge to) froms |
|
83 in Atom_Graph.empty |> fold add_infer infers end |
|
84 |
|
85 fun axioms_of_ref_graph ref_graph conjs = |
|
86 subtract atom_eq conjs (Atom_Graph.minimals ref_graph) |
|
87 fun tainted_atoms_of_ref_graph ref_graph = Atom_Graph.all_succs ref_graph |
|
88 |
|
89 fun sequents_of_ref_graph ref_graph = |
|
90 map (`(Atom_Graph.immediate_preds ref_graph)) |
|
91 (filter_out (Atom_Graph.is_minimal ref_graph) (Atom_Graph.keys ref_graph)) |
|
92 |
|
93 fun redirect_sequent tainted bot (gamma, c) = |
|
94 if member atom_eq tainted c then |
|
95 gamma |> List.partition (not o member atom_eq tainted) |
|
96 |>> not (atom_eq (c, bot)) ? cons c |
|
97 else |
|
98 (gamma, [c]) |
|
99 |
|
100 fun direct_graph seqs = |
|
101 let |
|
102 fun add_edge from to = |
|
103 Atom_Graph.default_node (from, ()) |
|
104 #> Atom_Graph.default_node (to, ()) |
|
105 #> Atom_Graph.add_edge_acyclic (from, to) |
|
106 fun add_seq (gamma, c) = fold (fn l => fold (add_edge l) c) gamma |
|
107 in Atom_Graph.empty |> fold add_seq seqs end |
|
108 |
|
109 fun disj cs = fold (union atom_eq) cs [] |> sort Atom.ord |
|
110 |
|
111 fun succedent_of_inference (Have (_, c)) = c |
|
112 | succedent_of_inference (Hence (_, c)) = c |
|
113 | succedent_of_inference (Cases cases) = succedent_of_cases cases |
|
114 and succedent_of_case (c, []) = c |
|
115 | succedent_of_case (_, infs) = succedent_of_inference (List.last infs) |
|
116 and succedent_of_cases cases = disj (map succedent_of_case cases) |
|
117 |
|
118 fun dest_Have (Have z) = z |
|
119 | dest_Have _ = raise Fail "non-Have" |
|
120 |
|
121 fun enrich_Have nontrivs trivs (cs, c) = |
|
122 (cs |> map (fn c => if member clause_eq nontrivs c then disj (c :: trivs) |
|
123 else c), |
|
124 disj (c :: trivs)) |
|
125 |> Have |
|
126 |
|
127 fun s_cases cases = |
|
128 case cases |> List.partition (null o snd) of |
|
129 (trivs, nontrivs as [(nontriv0, proof)]) => |
|
130 if forall (can dest_Have) proof then |
|
131 let val seqs = proof |> map dest_Have in |
|
132 seqs |> map (enrich_Have (nontriv0 :: map snd seqs) (map fst trivs)) |
|
133 end |
|
134 else |
|
135 [Cases nontrivs] |
|
136 | (_, nontrivs) => [Cases nontrivs] |
|
137 |
|
138 fun descendants direct_graph = |
|
139 these o try (Atom_Graph.all_succs direct_graph) o single |
|
140 |
|
141 fun zones_of 0 _ = [] |
|
142 | zones_of n (bs :: bss) = |
|
143 (fold (subtract atom_eq) bss) bs :: zones_of (n - 1) (bss @ [bs]) |
|
144 |
|
145 fun redirect_graph axioms tainted ref_graph = |
|
146 let |
|
147 val [bot] = Atom_Graph.maximals ref_graph |
|
148 val seqs = |
|
149 map (redirect_sequent tainted bot) (sequents_of_ref_graph ref_graph) |
|
150 val direct_graph = direct_graph seqs |
|
151 |
|
152 fun redirect c proved seqs = |
|
153 if null seqs then |
|
154 [] |
|
155 else if length c < 2 then |
|
156 let |
|
157 val proved = c @ proved |
|
158 val provable = |
|
159 filter (fn (gamma, _) => subset atom_eq (gamma, proved)) seqs |
|
160 val horn_provable = filter (fn (_, [_]) => true | _ => false) provable |
|
161 val seq as (gamma, c) = hd (horn_provable @ provable) |
|
162 in |
|
163 Have (map single gamma, c) :: |
|
164 redirect c proved (filter (curry (not o direct_sequent_eq) seq) seqs) |
|
165 end |
|
166 else |
|
167 let |
|
168 fun subsequents seqs zone = |
|
169 filter (fn (gamma, _) => subset atom_eq (gamma, zone @ proved)) seqs |
|
170 val zones = zones_of (length c) (map (descendants direct_graph) c) |
|
171 val subseqss = map (subsequents seqs) zones |
|
172 val seqs = fold (subtract direct_sequent_eq) subseqss seqs |
|
173 val cases = |
|
174 map2 (fn l => fn subseqs => ([l], redirect [l] proved subseqs)) |
|
175 c subseqss |
|
176 in s_cases cases @ redirect (succedent_of_cases cases) proved seqs end |
|
177 in redirect [] axioms seqs end |
|
178 |
|
179 val chain_direct_proof = |
|
180 let |
|
181 fun chain_inf cl0 (seq as Have (cs, c)) = |
|
182 if member clause_eq cs cl0 then |
|
183 Hence (filter_out (curry clause_eq cl0) cs, c) |
|
184 else |
|
185 seq |
|
186 | chain_inf _ (Cases cases) = Cases (map chain_case cases) |
|
187 and chain_case (c, is) = (c, chain_proof (SOME c) is) |
|
188 and chain_proof _ [] = [] |
|
189 | chain_proof (SOME prev) (i :: is) = |
|
190 chain_inf prev i :: chain_proof (SOME (succedent_of_inference i)) is |
|
191 | chain_proof _ (i :: is) = |
|
192 i :: chain_proof (SOME (succedent_of_inference i)) is |
|
193 in chain_proof NONE end |
|
194 |
|
195 fun indent 0 = "" |
|
196 | indent n = " " ^ indent (n - 1) |
|
197 |
|
198 fun string_of_clause [] = "\<bottom>" |
|
199 | string_of_clause ls = space_implode " \<or> " (map Atom.string_of ls) |
|
200 |
|
201 fun string_of_rich_sequent ch ([], c) = ch ^ " " ^ string_of_clause c |
|
202 | string_of_rich_sequent ch (cs, c) = |
|
203 commas (map string_of_clause cs) ^ " " ^ ch ^ " " ^ string_of_clause c |
|
204 |
|
205 fun string_of_case depth (c, proof) = |
|
206 indent (depth + 1) ^ "[" ^ string_of_clause c ^ "]" |
|
207 |> not (null proof) ? suffix ("\n" ^ string_of_subproof (depth + 1) proof) |
|
208 |
|
209 and string_of_inference depth (Have seq) = |
|
210 indent depth ^ string_of_rich_sequent "\<triangleright>" seq |
|
211 | string_of_inference depth (Hence seq) = |
|
212 indent depth ^ string_of_rich_sequent "\<guillemotright>" seq |
|
213 | string_of_inference depth (Cases cases) = |
|
214 indent depth ^ "[\n" ^ |
|
215 space_implode ("\n" ^ indent depth ^ "|\n") |
|
216 (map (string_of_case depth) cases) ^ "\n" ^ |
|
217 indent depth ^ "]" |
|
218 |
|
219 and string_of_subproof depth = cat_lines o map (string_of_inference depth) |
|
220 |
|
221 val string_of_direct_proof = string_of_subproof 0 |
|
222 |
|
223 end; |
|