--- a/src/HOL/Tools/ATP/atp_redirect.ML Wed Dec 14 23:08:03 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_redirect.ML Wed Dec 14 23:08:03 2011 +0100
@@ -4,167 +4,199 @@
Transformation of a proof by contradiction into a direct proof.
*)
+signature ATP_ATOM =
+sig
+ type key
+ val ord : key * key -> order
+ val string_of : key -> string
+end;
+
signature ATP_REDIRECT =
sig
- type ref_sequent = int list * int
- type ref_graph = unit Int_Graph.T
+ type atom
+
+ structure Atom_Graph : GRAPH
- type clause = int list
- type direct_sequent = int list * clause
- type direct_graph = unit Int_Graph.T
+ type ref_sequent = atom list * atom
+ type ref_graph = unit Atom_Graph.T
+
+ type clause = atom list
+ type direct_sequent = atom list * clause
+ type direct_graph = unit Atom_Graph.T
type rich_sequent = clause list * clause
- datatype inference =
+ datatype direct_inference =
Have of rich_sequent |
Hence of rich_sequent |
- Cases of (clause * inference list) list
+ Cases of (clause * direct_inference list) list
+
+ type direct_proof = direct_inference list
- type proof = inference list
-
- val make_ref_graph : (int list * int) list -> ref_graph
+ val make_ref_graph : (atom list * atom) list -> ref_graph
+ val axioms_of_ref_graph : ref_graph -> atom list -> atom list
+ val tainted_atoms_of_ref_graph : ref_graph -> atom list -> atom list
val sequents_of_ref_graph : ref_graph -> ref_sequent list
- val redirect_sequent : int list -> int -> ref_sequent -> direct_sequent
+ val redirect_sequent : atom list -> atom -> ref_sequent -> direct_sequent
val direct_graph : direct_sequent list -> direct_graph
- val redirect_graph : int list -> ref_graph -> proof
- val chain_proof : proof -> proof
- val string_of_proof : proof -> string
+ val redirect_graph : atom list -> atom list -> ref_graph -> direct_proof
+ val succedent_of_cases : (clause * direct_inference list) list -> clause
+ val chain_direct_proof : direct_proof -> direct_proof
+ val string_of_direct_proof : direct_proof -> string
end;
-structure ATP_Redirect : ATP_REDIRECT =
+functor ATP_Redirect(Atom : ATP_ATOM): ATP_REDIRECT =
struct
-type ref_sequent = int list * int
-type ref_graph = unit Int_Graph.T
+type atom = Atom.key
+
+structure Atom_Graph = Graph(Atom)
-type clause = int list
-type direct_sequent = int list * clause
-type direct_graph = unit Int_Graph.T
+type ref_sequent = atom list * atom
+type ref_graph = unit Atom_Graph.T
+
+type clause = atom list
+type direct_sequent = atom list * clause
+type direct_graph = unit Atom_Graph.T
type rich_sequent = clause list * clause
-datatype inference =
+datatype direct_inference =
Have of rich_sequent |
Hence of rich_sequent |
- Cases of (clause * inference list) list
+ Cases of (clause * direct_inference list) list
+
+type direct_proof = direct_inference list
-type proof = inference list
+fun atom_eq p = (Atom.ord p = EQUAL)
+fun clause_eq (c, d) = (length c = length d andalso forall atom_eq (c ~~ d))
+fun direct_sequent_eq ((gamma, c), (delta, d)) =
+ clause_eq (gamma, delta) andalso clause_eq (c, d)
fun make_ref_graph infers =
let
fun add_edge to from =
- Int_Graph.default_node (from, ())
- #> Int_Graph.default_node (to, ())
- #> Int_Graph.add_edge_acyclic (from, to)
+ Atom_Graph.default_node (from, ())
+ #> Atom_Graph.default_node (to, ())
+ #> Atom_Graph.add_edge_acyclic (from, to)
fun add_infer (froms, to) = fold (add_edge to) froms
- in Int_Graph.empty |> fold add_infer infers end
+ in Atom_Graph.empty |> fold add_infer infers end
+
+fun axioms_of_ref_graph ref_graph conjs =
+ subtract atom_eq conjs (Atom_Graph.minimals ref_graph)
+fun tainted_atoms_of_ref_graph ref_graph = Atom_Graph.all_succs ref_graph
-fun sequents_of_ref_graph g =
- map (`(Int_Graph.immediate_preds g))
- (filter_out (Int_Graph.is_minimal g) (Int_Graph.keys g))
+fun sequents_of_ref_graph ref_graph =
+ map (`(Atom_Graph.immediate_preds ref_graph))
+ (filter_out (Atom_Graph.is_minimal ref_graph) (Atom_Graph.keys ref_graph))
-fun redirect_sequent tainted bot (ante, l) =
- if member (op =) tainted l then
- ante |> List.partition (not o member (op =) tainted) |>> l <> bot ? cons l
+fun redirect_sequent tainted bot (gamma, c) =
+ if member atom_eq tainted c then
+ gamma |> List.partition (not o member atom_eq tainted)
+ |>> not (atom_eq (c, bot)) ? cons c
else
- (ante, [l])
+ (gamma, [c])
fun direct_graph seqs =
let
fun add_edge from to =
- Int_Graph.default_node (from, ())
- #> Int_Graph.default_node (to, ())
- #> Int_Graph.add_edge_acyclic (from, to)
- fun add_seq (ante, c) = fold (fn l => fold (add_edge l) c) ante
- in Int_Graph.empty |> fold add_seq seqs end
+ Atom_Graph.default_node (from, ())
+ #> Atom_Graph.default_node (to, ())
+ #> Atom_Graph.add_edge_acyclic (from, to)
+ fun add_seq (gamma, c) = fold (fn l => fold (add_edge l) c) gamma
+ in Atom_Graph.empty |> fold add_seq seqs end
-fun disj cs = fold (union (op =)) cs [] |> sort int_ord
+fun disj cs = fold (union atom_eq) cs [] |> sort Atom.ord
-fun concl_of_inf (Have (_, c)) = c
- | concl_of_inf (Hence (_, c)) = c
- | concl_of_inf (Cases cases) = concl_of_cases cases
-and concl_of_case (c, []) = c
- | concl_of_case (_, infs) = concl_of_inf (List.last infs)
-and concl_of_cases cases = disj (map concl_of_case cases)
+fun succedent_of_inference (Have (_, c)) = c
+ | succedent_of_inference (Hence (_, c)) = c
+ | succedent_of_inference (Cases cases) = succedent_of_cases cases
+and succedent_of_case (c, []) = c
+ | succedent_of_case (_, infs) = succedent_of_inference (List.last infs)
+and succedent_of_cases cases = disj (map succedent_of_case cases)
fun dest_Have (Have z) = z
| dest_Have _ = raise Fail "non-Have"
fun enrich_Have nontrivs trivs (cs, c) =
- (cs |> map (fn c => if member (op =) nontrivs c then disj (c :: trivs)
+ (cs |> map (fn c => if member clause_eq nontrivs c then disj (c :: trivs)
else c),
disj (c :: trivs))
|> Have
fun s_cases cases =
case cases |> List.partition (null o snd) of
- (trivs, [(nontriv0, proof)]) =>
+ (trivs, nontrivs as [(nontriv0, proof)]) =>
if forall (can dest_Have) proof then
let val seqs = proof |> map dest_Have in
seqs |> map (enrich_Have (nontriv0 :: map snd seqs) (map fst trivs))
end
else
- [Cases cases]
- | _ => [Cases cases]
+ [Cases nontrivs]
+ | (_, nontrivs) => [Cases nontrivs]
-fun descendants seqs =
- these o try (Int_Graph.all_succs (direct_graph seqs)) o single
+fun descendants direct_graph =
+ these o try (Atom_Graph.all_succs direct_graph) o single
fun zones_of 0 _ = []
- | zones_of n (ls :: lss) =
- (fold (subtract (op =)) lss) ls :: zones_of (n - 1) (lss @ [ls])
+ | zones_of n (bs :: bss) =
+ (fold (subtract atom_eq) bss) bs :: zones_of (n - 1) (bss @ [bs])
+
+fun redirect_graph axioms tainted ref_graph =
+ let
+ val [bot] = Atom_Graph.maximals ref_graph
+ val seqs =
+ map (redirect_sequent tainted bot) (sequents_of_ref_graph ref_graph)
+ val direct_graph = direct_graph seqs
-fun redirect c proved seqs =
- if null seqs then
- []
- else if length c < 2 then
- let
- val proved = c @ proved
- val provable = filter (fn (ante, _) => subset (op =) (ante, proved)) seqs
- val horn_provable = filter (fn (_, [_]) => true | _ => false) provable
- val seq as (ante, c) = hd (horn_provable @ provable)
- in
- Have (map single ante, c) ::
- redirect c proved (filter (curry (op <>) seq) seqs)
- end
- else
- let
- fun subsequents seqs zone =
- filter (fn (ante, _) => subset (op =) (ante, zone @ proved)) seqs
- val zones = zones_of (length c) (map (descendants seqs) c)
- val subseqss = map (subsequents seqs) zones
- val seqs = fold (subtract (op =)) subseqss seqs
- val cases =
- map2 (fn l => fn subseqs => ([l], redirect [l] proved subseqs))
- c subseqss
- in [Cases cases] @ redirect (concl_of_cases cases) proved seqs end
-
-fun redirect_graph conjecture g =
- let
- val axioms = subtract (op =) conjecture (Int_Graph.minimals g)
- val tainted = Int_Graph.all_succs g conjecture
- val [bot] = Int_Graph.maximals g
- val seqs = map (redirect_sequent tainted bot) (sequents_of_ref_graph g)
+ fun redirect c proved seqs =
+ if null seqs then
+ []
+ else if length c < 2 then
+ let
+ val proved = c @ proved
+ val provable =
+ filter (fn (gamma, _) => subset atom_eq (gamma, proved)) seqs
+ val horn_provable = filter (fn (_, [_]) => true | _ => false) provable
+ val seq as (gamma, c) = hd (horn_provable @ provable)
+ in
+ Have (map single gamma, c) ::
+ redirect c proved (filter (curry (not o direct_sequent_eq) seq) seqs)
+ end
+ else
+ let
+ fun subsequents seqs zone =
+ filter (fn (gamma, _) => subset atom_eq (gamma, zone @ proved)) seqs
+ val zones = zones_of (length c) (map (descendants direct_graph) c)
+ val subseqss = map (subsequents seqs) zones
+ val seqs = fold (subtract direct_sequent_eq) subseqss seqs
+ val cases =
+ map2 (fn l => fn subseqs => ([l], redirect [l] proved subseqs))
+ c subseqss
+ in s_cases cases @ redirect (succedent_of_cases cases) proved seqs end
in redirect [] axioms seqs end
-val chain_proof =
+val chain_direct_proof =
let
fun chain_inf cl0 (seq as Have (cs, c)) =
- if member (op =) cs cl0 then Hence (filter_out (curry (op =) cl0) cs, c)
- else seq
+ if member clause_eq cs cl0 then
+ Hence (filter_out (curry clause_eq cl0) cs, c)
+ else
+ seq
| chain_inf _ (Cases cases) = Cases (map chain_case cases)
and chain_case (c, is) = (c, chain_proof (SOME c) is)
and chain_proof _ [] = []
| chain_proof (SOME prev) (i :: is) =
- chain_inf prev i :: chain_proof (SOME (concl_of_inf i)) is
- | chain_proof _ (i :: is) = i :: chain_proof (SOME (concl_of_inf i)) is
+ chain_inf prev i :: chain_proof (SOME (succedent_of_inference i)) is
+ | chain_proof _ (i :: is) =
+ i :: chain_proof (SOME (succedent_of_inference i)) is
in chain_proof NONE end
fun indent 0 = ""
| indent n = " " ^ indent (n - 1)
fun string_of_clause [] = "\<bottom>"
- | string_of_clause ls = space_implode " \<or> " (map signed_string_of_int ls)
+ | string_of_clause ls = space_implode " \<or> " (map Atom.string_of ls)
fun string_of_rich_sequent ch ([], c) = ch ^ " " ^ string_of_clause c
| string_of_rich_sequent ch (cs, c) =
@@ -184,9 +216,8 @@
(map (string_of_case depth) cases) ^ "\n" ^
indent depth ^ "]"
-and string_of_subproof depth proof =
- cat_lines (map (string_of_inference depth) proof)
+and string_of_subproof depth = cat_lines o map (string_of_inference depth)
-val string_of_proof = string_of_subproof 0
+val string_of_direct_proof = string_of_subproof 0
end;