author | blanchet |
Wed, 18 Dec 2013 16:50:14 +0100 | |
changeset 54799 | 565f9af86d67 |
parent 54762 | c3ef7b572213 |
child 57699 | a6cf197c1f1e |
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 |
|
54755 | 20 |
type refute_sequent = atom list * atom |
51145 | 21 |
type refute_graph = unit Atom_Graph.T |
45882 | 22 |
|
23 |
type clause = atom list |
|
54755 | 24 |
type direct_sequent = atom * (atom list * clause) |
45882 | 25 |
type direct_graph = unit Atom_Graph.T |
45877 | 26 |
|
54755 | 27 |
type rich_sequent = atom * (clause list * clause) |
45877 | 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 |
|
51208
44f0bfe67b01
remove needless steps from refutation graph -- these confuse the proof redirection algorithm (and are needless)
blanchet
parents:
51207
diff
changeset
|
35 |
val make_refute_graph : atom -> (atom list * atom) list -> refute_graph |
51145 | 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 |
|
54755 | 38 |
val sequents_of_refute_graph : refute_graph -> refute_sequent list |
51145 | 39 |
val string_of_refute_graph : refute_graph -> string |
54755 | 40 |
val redirect_sequent : atom list -> atom -> refute_sequent -> direct_sequent |
45877 | 41 |
val direct_graph : direct_sequent list -> direct_graph |
54714
ae01c51eadff
removed inlined rewriting'' for one-branch case splits in Isar proofs, since these can yield huge unreadable formulas
blanchet
parents:
51243
diff
changeset
|
42 |
val redirect_graph : atom list -> atom list -> atom -> refute_graph -> direct_proof |
45882 | 43 |
val succedent_of_cases : (clause * direct_inference list) list -> clause |
44 |
val string_of_direct_proof : direct_proof -> string |
|
45877 | 45 |
end; |
46 |
||
46320 | 47 |
functor ATP_Proof_Redirect(Atom : ATP_ATOM): ATP_PROOF_REDIRECT = |
45877 | 48 |
struct |
49 |
||
45882 | 50 |
type atom = Atom.key |
51 |
||
52 |
structure Atom_Graph = Graph(Atom) |
|
45877 | 53 |
|
54755 | 54 |
type refute_sequent = atom list * atom |
51145 | 55 |
type refute_graph = unit Atom_Graph.T |
45882 | 56 |
|
57 |
type clause = atom list |
|
54755 | 58 |
type direct_sequent = atom * (atom list * clause) |
45882 | 59 |
type direct_graph = unit Atom_Graph.T |
45877 | 60 |
|
54755 | 61 |
type rich_sequent = atom * (clause list * clause) |
45877 | 62 |
|
45882 | 63 |
datatype direct_inference = |
45877 | 64 |
Have of rich_sequent | |
45882 | 65 |
Cases of (clause * direct_inference list) list |
66 |
||
67 |
type direct_proof = direct_inference list |
|
45877 | 68 |
|
51213 | 69 |
val atom_eq = is_equal o Atom.ord |
70 |
val clause_ord = dict_ord Atom.ord |
|
54762 | 71 |
fun direct_sequent_ord seqp = prod_ord clause_ord clause_ord (pairself snd seqp) |
72 |
fun direct_sequent_eq seqp = is_equal (direct_sequent_ord seqp) |
|
45877 | 73 |
|
51208
44f0bfe67b01
remove needless steps from refutation graph -- these confuse the proof redirection algorithm (and are needless)
blanchet
parents:
51207
diff
changeset
|
74 |
fun make_refute_graph bot infers = |
45877 | 75 |
let |
76 |
fun add_edge to from = |
|
45882 | 77 |
Atom_Graph.default_node (from, ()) |
78 |
#> Atom_Graph.add_edge_acyclic (from, to) |
|
54754 | 79 |
fun add_infer (froms, to) = |
80 |
Atom_Graph.default_node (to, ()) |
|
81 |
#> fold (add_edge to) froms |
|
54735 | 82 |
|
51208
44f0bfe67b01
remove needless steps from refutation graph -- these confuse the proof redirection algorithm (and are needless)
blanchet
parents:
51207
diff
changeset
|
83 |
val graph = fold add_infer infers Atom_Graph.empty |
44f0bfe67b01
remove needless steps from refutation graph -- these confuse the proof redirection algorithm (and are needless)
blanchet
parents:
51207
diff
changeset
|
84 |
val reachable = Atom_Graph.all_preds graph [bot] |
54714
ae01c51eadff
removed inlined rewriting'' for one-branch case splits in Isar proofs, since these can yield huge unreadable formulas
blanchet
parents:
51243
diff
changeset
|
85 |
in |
ae01c51eadff
removed inlined rewriting'' for one-branch case splits in Isar proofs, since these can yield huge unreadable formulas
blanchet
parents:
51243
diff
changeset
|
86 |
graph |> Atom_Graph.restrict (member (is_equal o Atom.ord) reachable) |
ae01c51eadff
removed inlined rewriting'' for one-branch case splits in Isar proofs, since these can yield huge unreadable formulas
blanchet
parents:
51243
diff
changeset
|
87 |
end |
45882 | 88 |
|
51145 | 89 |
fun axioms_of_refute_graph refute_graph conjs = |
90 |
subtract atom_eq conjs (Atom_Graph.minimals refute_graph) |
|
45877 | 91 |
|
54735 | 92 |
fun tainted_atoms_of_refute_graph refute_graph = Atom_Graph.all_succs refute_graph |
51145 | 93 |
|
94 |
fun sequents_of_refute_graph refute_graph = |
|
54714
ae01c51eadff
removed inlined rewriting'' for one-branch case splits in Isar proofs, since these can yield huge unreadable formulas
blanchet
parents:
51243
diff
changeset
|
95 |
Atom_Graph.keys refute_graph |
ae01c51eadff
removed inlined rewriting'' for one-branch case splits in Isar proofs, since these can yield huge unreadable formulas
blanchet
parents:
51243
diff
changeset
|
96 |
|> filter_out (Atom_Graph.is_minimal refute_graph) |
ae01c51eadff
removed inlined rewriting'' for one-branch case splits in Isar proofs, since these can yield huge unreadable formulas
blanchet
parents:
51243
diff
changeset
|
97 |
|> map (`(Atom_Graph.immediate_preds refute_graph)) |
45877 | 98 |
|
47915 | 99 |
val string_of_context = map Atom.string_of #> space_implode ", " |
100 |
||
101 |
fun string_of_sequent (gamma, c) = |
|
102 |
string_of_context gamma ^ " \<turnstile> " ^ Atom.string_of c |
|
103 |
||
54735 | 104 |
fun string_of_refute_graph refute_graph = |
105 |
refute_graph |> sequents_of_refute_graph |> map string_of_sequent |> cat_lines |
|
47915 | 106 |
|
45882 | 107 |
fun redirect_sequent tainted bot (gamma, c) = |
54755 | 108 |
(c, |
109 |
if member atom_eq tainted c then |
|
110 |
gamma |> List.partition (not o member atom_eq tainted) |
|
111 |
|>> not (atom_eq (c, bot)) ? cons c |
|
112 |
else |
|
113 |
(gamma, [c])) |
|
45877 | 114 |
|
115 |
fun direct_graph seqs = |
|
116 |
let |
|
117 |
fun add_edge from to = |
|
45882 | 118 |
Atom_Graph.default_node (from, ()) |
119 |
#> Atom_Graph.default_node (to, ()) |
|
120 |
#> Atom_Graph.add_edge_acyclic (from, to) |
|
54755 | 121 |
fun add_seq (_, (gamma, c)) = fold (fn l => fold (add_edge l) c) gamma |
54735 | 122 |
in |
123 |
fold add_seq seqs Atom_Graph.empty |
|
124 |
end |
|
45877 | 125 |
|
45882 | 126 |
fun disj cs = fold (union atom_eq) cs [] |> sort Atom.ord |
45877 | 127 |
|
54755 | 128 |
fun succedent_of_inference (Have (_, (_, c))) = c |
45882 | 129 |
| succedent_of_inference (Cases cases) = succedent_of_cases cases |
130 |
and succedent_of_case (c, []) = c |
|
131 |
| succedent_of_case (_, infs) = succedent_of_inference (List.last infs) |
|
132 |
and succedent_of_cases cases = disj (map succedent_of_case cases) |
|
45877 | 133 |
|
54760
a1ac3eaa0d11
generate proper succedent for cases with trivial branches
blanchet
parents:
54755
diff
changeset
|
134 |
fun s_cases cases = [Cases cases] |
45877 | 135 |
|
54714
ae01c51eadff
removed inlined rewriting'' for one-branch case splits in Isar proofs, since these can yield huge unreadable formulas
blanchet
parents:
51243
diff
changeset
|
136 |
fun descendants direct_graph = these o try (Atom_Graph.all_succs direct_graph) o single |
45877 | 137 |
|
138 |
fun zones_of 0 _ = [] |
|
54714
ae01c51eadff
removed inlined rewriting'' for one-branch case splits in Isar proofs, since these can yield huge unreadable formulas
blanchet
parents:
51243
diff
changeset
|
139 |
| zones_of n (bs :: bss) = (fold (subtract atom_eq) bss) bs :: zones_of (n - 1) (bss @ [bs]) |
45882 | 140 |
|
51145 | 141 |
fun redirect_graph axioms tainted bot refute_graph = |
45882 | 142 |
let |
54735 | 143 |
val seqs = map (redirect_sequent tainted bot) (sequents_of_refute_graph refute_graph) |
45882 | 144 |
val direct_graph = direct_graph seqs |
54735 | 145 |
|
45882 | 146 |
fun redirect c proved seqs = |
147 |
if null seqs then |
|
148 |
[] |
|
149 |
else if length c < 2 then |
|
150 |
let |
|
151 |
val proved = c @ proved |
|
54755 | 152 |
val provable = filter (fn (_, (gamma, _)) => subset atom_eq (gamma, proved)) seqs |
153 |
val horn_provable = filter (fn (_, (_, [_])) => true | _ => false) provable |
|
154 |
val seq as (id, (gamma, c)) = |
|
54714
ae01c51eadff
removed inlined rewriting'' for one-branch case splits in Isar proofs, since these can yield huge unreadable formulas
blanchet
parents:
51243
diff
changeset
|
155 |
(case horn_provable @ provable of |
51207 | 156 |
[] => raise Fail "ill-formed refutation graph" |
54714
ae01c51eadff
removed inlined rewriting'' for one-branch case splits in Isar proofs, since these can yield huge unreadable formulas
blanchet
parents:
51243
diff
changeset
|
157 |
| next :: _ => next) |
45882 | 158 |
in |
54755 | 159 |
Have (id, (map single gamma, c)) :: |
45882 | 160 |
redirect c proved (filter (curry (not o direct_sequent_eq) seq) seqs) |
161 |
end |
|
162 |
else |
|
163 |
let |
|
164 |
fun subsequents seqs zone = |
|
54755 | 165 |
filter (fn (_, (gamma, _)) => subset atom_eq (gamma, zone @ proved)) seqs |
45882 | 166 |
val zones = zones_of (length c) (map (descendants direct_graph) c) |
167 |
val subseqss = map (subsequents seqs) zones |
|
168 |
val seqs = fold (subtract direct_sequent_eq) subseqss seqs |
|
54714
ae01c51eadff
removed inlined rewriting'' for one-branch case splits in Isar proofs, since these can yield huge unreadable formulas
blanchet
parents:
51243
diff
changeset
|
169 |
val cases = map2 (fn l => fn subseqs => ([l], redirect [l] proved subseqs)) c subseqss |
ae01c51eadff
removed inlined rewriting'' for one-branch case splits in Isar proofs, since these can yield huge unreadable formulas
blanchet
parents:
51243
diff
changeset
|
170 |
in |
ae01c51eadff
removed inlined rewriting'' for one-branch case splits in Isar proofs, since these can yield huge unreadable formulas
blanchet
parents:
51243
diff
changeset
|
171 |
s_cases cases @ redirect (succedent_of_cases cases) proved seqs |
ae01c51eadff
removed inlined rewriting'' for one-branch case splits in Isar proofs, since these can yield huge unreadable formulas
blanchet
parents:
51243
diff
changeset
|
172 |
end |
54735 | 173 |
in |
174 |
redirect [] axioms seqs |
|
175 |
end |
|
45877 | 176 |
|
177 |
fun indent 0 = "" |
|
178 |
| indent n = " " ^ indent (n - 1) |
|
179 |
||
180 |
fun string_of_clause [] = "\<bottom>" |
|
45882 | 181 |
| string_of_clause ls = space_implode " \<or> " (map Atom.string_of ls) |
45877 | 182 |
|
54755 | 183 |
fun string_of_rich_sequent ch (id, (cs, c)) = |
184 |
(if null cs then "" else commas (map string_of_clause cs) ^ " ") ^ ch ^ " " ^ string_of_clause c ^ |
|
54760
a1ac3eaa0d11
generate proper succedent for cases with trivial branches
blanchet
parents:
54755
diff
changeset
|
185 |
" (* " ^ Atom.string_of id ^ " *)" |
45877 | 186 |
|
187 |
fun string_of_case depth (c, proof) = |
|
188 |
indent (depth + 1) ^ "[" ^ string_of_clause c ^ "]" |
|
189 |
|> not (null proof) ? suffix ("\n" ^ string_of_subproof (depth + 1) proof) |
|
190 |
||
191 |
and string_of_inference depth (Have seq) = |
|
192 |
indent depth ^ string_of_rich_sequent "\<triangleright>" seq |
|
193 |
| string_of_inference depth (Cases cases) = |
|
194 |
indent depth ^ "[\n" ^ |
|
54735 | 195 |
space_implode ("\n" ^ indent depth ^ "|\n") (map (string_of_case depth) cases) ^ "\n" ^ |
45877 | 196 |
indent depth ^ "]" |
197 |
||
45882 | 198 |
and string_of_subproof depth = cat_lines o map (string_of_inference depth) |
45877 | 199 |
|
45882 | 200 |
val string_of_direct_proof = string_of_subproof 0 |
45877 | 201 |
|
202 |
end; |