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