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


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

45877

26 


27 
type rich_sequent = clause list * clause


28 

45882

29 
datatype direct_inference =

45877

30 
Have of rich_sequent 


31 
Hence of rich_sequent 

45882

32 
Cases of (clause * direct_inference list) list


33 


34 
type direct_proof = direct_inference list

45877

35 

45882

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

45877

39 
val sequents_of_ref_graph : ref_graph > ref_sequent list

47915

40 
val string_of_ref_graph : ref_graph > string

45882

41 
val redirect_sequent : atom list > atom > ref_sequent > direct_sequent

45877

42 
val direct_graph : direct_sequent list > direct_graph

45882

43 
val redirect_graph : atom list > atom list > ref_graph > direct_proof


44 
val succedent_of_cases : (clause * direct_inference list) list > clause


45 
val chain_direct_proof : direct_proof > direct_proof


46 
val string_of_direct_proof : direct_proof > string

45877

47 
end;


48 

46320

49 
functor ATP_Proof_Redirect(Atom : ATP_ATOM): ATP_PROOF_REDIRECT =

45877

50 
struct


51 

45882

52 
type atom = Atom.key


53 


54 
structure Atom_Graph = Graph(Atom)

45877

55 

45882

56 
type ref_sequent = atom list * atom


57 
type ref_graph = unit Atom_Graph.T


58 


59 
type clause = atom list


60 
type direct_sequent = atom list * clause


61 
type direct_graph = unit Atom_Graph.T

45877

62 


63 
type rich_sequent = clause list * clause


64 

45882

65 
datatype direct_inference =

45877

66 
Have of rich_sequent 


67 
Hence of rich_sequent 

45882

68 
Cases of (clause * direct_inference list) list


69 


70 
type direct_proof = direct_inference list

45877

71 

45882

72 
fun atom_eq p = (Atom.ord p = EQUAL)


73 
fun clause_eq (c, d) = (length c = length d andalso forall atom_eq (c ~~ d))


74 
fun direct_sequent_eq ((gamma, c), (delta, d)) =


75 
clause_eq (gamma, delta) andalso clause_eq (c, d)

45877

76 


77 
fun make_ref_graph infers =


78 
let


79 
fun add_edge to from =

45882

80 
Atom_Graph.default_node (from, ())


81 
#> Atom_Graph.default_node (to, ())


82 
#> Atom_Graph.add_edge_acyclic (from, to)

45877

83 
fun add_infer (froms, to) = fold (add_edge to) froms

45882

84 
in Atom_Graph.empty > fold add_infer infers end


85 


86 
fun axioms_of_ref_graph ref_graph conjs =


87 
subtract atom_eq conjs (Atom_Graph.minimals ref_graph)


88 
fun tainted_atoms_of_ref_graph ref_graph = Atom_Graph.all_succs ref_graph

45877

89 

45882

90 
fun sequents_of_ref_graph ref_graph =


91 
map (`(Atom_Graph.immediate_preds ref_graph))


92 
(filter_out (Atom_Graph.is_minimal ref_graph) (Atom_Graph.keys ref_graph))

45877

93 

47915

94 
val string_of_context = map Atom.string_of #> space_implode ", "


95 


96 
fun string_of_sequent (gamma, c) =


97 
string_of_context gamma ^ " \<turnstile> " ^ Atom.string_of c


98 


99 
val string_of_ref_graph =

47919

100 
sequents_of_ref_graph #> map string_of_sequent #> cat_lines

47915

101 

45882

102 
fun redirect_sequent tainted bot (gamma, c) =


103 
if member atom_eq tainted c then


104 
gamma > List.partition (not o member atom_eq tainted)


105 
>> not (atom_eq (c, bot)) ? cons c

45877

106 
else

45882

107 
(gamma, [c])

45877

108 


109 
fun direct_graph seqs =


110 
let


111 
fun add_edge from to =

45882

112 
Atom_Graph.default_node (from, ())


113 
#> Atom_Graph.default_node (to, ())


114 
#> Atom_Graph.add_edge_acyclic (from, to)


115 
fun add_seq (gamma, c) = fold (fn l => fold (add_edge l) c) gamma


116 
in Atom_Graph.empty > fold add_seq seqs end

45877

117 

45882

118 
fun disj cs = fold (union atom_eq) cs [] > sort Atom.ord

45877

119 

45882

120 
fun succedent_of_inference (Have (_, c)) = c


121 
 succedent_of_inference (Hence (_, 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 "nonHave"


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 


154 
fun redirect_graph axioms tainted ref_graph =


155 
let


156 
val [bot] = Atom_Graph.maximals ref_graph


157 
val seqs =


158 
map (redirect_sequent tainted bot) (sequents_of_ref_graph ref_graph)


159 
val direct_graph = direct_graph seqs

45877

160 

45882

161 
fun redirect c proved seqs =


162 
if null seqs then


163 
[]


164 
else if length c < 2 then


165 
let


166 
val proved = c @ proved


167 
val provable =


168 
filter (fn (gamma, _) => subset atom_eq (gamma, proved)) seqs


169 
val horn_provable = filter (fn (_, [_]) => true  _ => false) provable


170 
val seq as (gamma, c) = hd (horn_provable @ provable)


171 
in


172 
Have (map single gamma, c) ::


173 
redirect c proved (filter (curry (not o direct_sequent_eq) seq) seqs)


174 
end


175 
else


176 
let


177 
fun subsequents seqs zone =


178 
filter (fn (gamma, _) => subset atom_eq (gamma, zone @ proved)) seqs


179 
val zones = zones_of (length c) (map (descendants direct_graph) c)


180 
val subseqss = map (subsequents seqs) zones


181 
val seqs = fold (subtract direct_sequent_eq) subseqss seqs


182 
val cases =


183 
map2 (fn l => fn subseqs => ([l], redirect [l] proved subseqs))


184 
c subseqss


185 
in s_cases cases @ redirect (succedent_of_cases cases) proved seqs end

45877

186 
in redirect [] axioms seqs end


187 

45882

188 
val chain_direct_proof =

45877

189 
let


190 
fun chain_inf cl0 (seq as Have (cs, c)) =

45882

191 
if member clause_eq cs cl0 then


192 
Hence (filter_out (curry clause_eq cl0) cs, c)


193 
else


194 
seq

45877

195 
 chain_inf _ (Cases cases) = Cases (map chain_case cases)


196 
and chain_case (c, is) = (c, chain_proof (SOME c) is)


197 
and chain_proof _ [] = []


198 
 chain_proof (SOME prev) (i :: is) =

45882

199 
chain_inf prev i :: chain_proof (SOME (succedent_of_inference i)) is


200 
 chain_proof _ (i :: is) =


201 
i :: chain_proof (SOME (succedent_of_inference i)) is

45877

202 
in chain_proof NONE end


203 


204 
fun indent 0 = ""


205 
 indent n = " " ^ indent (n  1)


206 


207 
fun string_of_clause [] = "\<bottom>"

45882

208 
 string_of_clause ls = space_implode " \<or> " (map Atom.string_of ls)

45877

209 


210 
fun string_of_rich_sequent ch ([], c) = ch ^ " " ^ string_of_clause c


211 
 string_of_rich_sequent ch (cs, c) =


212 
commas (map string_of_clause cs) ^ " " ^ ch ^ " " ^ string_of_clause c


213 


214 
fun string_of_case depth (c, proof) =


215 
indent (depth + 1) ^ "[" ^ string_of_clause c ^ "]"


216 
> not (null proof) ? suffix ("\n" ^ string_of_subproof (depth + 1) proof)


217 


218 
and string_of_inference depth (Have seq) =


219 
indent depth ^ string_of_rich_sequent "\<triangleright>" seq


220 
 string_of_inference depth (Hence seq) =


221 
indent depth ^ string_of_rich_sequent "\<guillemotright>" seq


222 
 string_of_inference depth (Cases cases) =


223 
indent depth ^ "[\n" ^


224 
space_implode ("\n" ^ indent depth ^ "\n")


225 
(map (string_of_case depth) cases) ^ "\n" ^


226 
indent depth ^ "]"


227 

45882

228 
and string_of_subproof depth = cat_lines o map (string_of_inference depth)

45877

229 

45882

230 
val string_of_direct_proof = string_of_subproof 0

45877

231 


232 
end;
