# HG changeset patch # User blanchet # Date 1323900483 -3600 # Node ID 5d8a7fe36ce51dc594093dbd85b6263c43057014 # Parent 3be79bdcc70293a57315ca2407eb35e01b8c092f use new redirection algorithm in Sledgehammer diff -r 3be79bdcc702 -r 5d8a7fe36ce5 src/HOL/Tools/ATP/atp_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Dec 14 23:08:03 2011 +0100 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Dec 14 23:08:03 2011 +0100 @@ -10,7 +10,6 @@ sig type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula - type step_name = ATP_Proof.step_name type 'a proof = 'a ATP_Proof.proof type locality = ATP_Translate.locality @@ -76,6 +75,12 @@ open ATP_Proof open ATP_Translate +structure String_Redirect = + ATP_Redirect(type key = step_name + val ord = fast_string_ord o pairself fst + val string_of = fst) +open String_Redirect + datatype reconstructor = Metis of string * string | SMT @@ -285,9 +290,9 @@ val indent_size = 2 val no_label = ("", ~1) -val raw_prefix = "X" -val assum_prefix = "A" -val have_prefix = "F" +val raw_prefix = "x" +val assum_prefix = "a" +val have_prefix = "f" fun raw_label_for_name (num, ss) = case resolve_conjecture ss of @@ -676,13 +681,13 @@ Fix of (string * typ) list | Let of term * term | Assume of label * term | - Have of isar_qualifier list * label * term * byline + Prove of isar_qualifier list * label * term * byline and byline = - ByMetis of facts | - CaseSplit of isar_step list list * facts + By_Metis of facts | + Case_Split of isar_step list list * facts -fun smart_case_split [] facts = ByMetis facts - | smart_case_split proofs facts = CaseSplit (proofs, facts) +fun smart_case_split [] facts = By_Metis facts + | smart_case_split proofs facts = Case_Split (proofs, facts) fun add_fact_from_dependency fact_names (name as (_, ss)) = if is_fact fact_names ss then @@ -694,9 +699,9 @@ | step_for_line _ _ (Inference (name, t, _, [])) = Assume (raw_label_for_name name, t) | step_for_line fact_names j (Inference (name, t, _, deps)) = - Have (if j = 1 then [Show] else [], raw_label_for_name name, - fold_rev forall_of (map Var (Term.add_vars t [])) t, - ByMetis (fold (add_fact_from_dependency fact_names) deps ([], []))) + Prove (if j = 1 then [Show] else [], raw_label_for_name name, + fold_rev forall_of (map Var (Term.add_vars t [])) t, + By_Metis (fold (add_fact_from_dependency fact_names) deps ([], []))) fun repair_name "$true" = "c_True" | repair_name "$false" = "c_False" @@ -736,10 +741,10 @@ case split. *) type backpatches = (label * facts) list * (label list * label list) -fun used_labels_of_step (Have (_, _, _, by)) = +fun used_labels_of_step (Prove (_, _, _, by)) = (case by of - ByMetis (ls, _) => ls - | CaseSplit (proofs, (ls, _)) => + By_Metis (ls, _) => ls + | Case_Split (proofs, (ls, _)) => fold (union (op =) o used_labels_of) proofs ls) | used_labels_of_step _ = [] and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof [] @@ -747,7 +752,7 @@ fun new_labels_of_step (Fix _) = [] | new_labels_of_step (Let _) = [] | new_labels_of_step (Assume (l, _)) = [l] - | new_labels_of_step (Have (_, l, _, _)) = [l] + | new_labels_of_step (Prove (_, l, _, _)) = [l] val new_labels_of = maps new_labels_of_step val join_proofs = @@ -759,8 +764,8 @@ else if forall (curry (op =) (hd proof1) o hd) (tl proofs) then aux (hd proof1 :: proof_tail) (map tl proofs) else case hd proof1 of - Have ([], l, t, _) => (* FIXME: should we really ignore the "by"? *) - if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t') + Prove ([], l, t, _) => (* FIXME: should we really ignore the "by"? *) + if forall (fn Prove ([], l', t', _) :: _ => (l, t) = (l', t') | _ => false) (tl proofs) andalso not (exists (member (op =) (maps new_labels_of proofs)) (used_labels_of proof_tail)) then @@ -791,8 +796,8 @@ | first_pass ((step as Assume (l as (_, j), _)) :: proof, contra) = if l = concl_l then first_pass (proof, contra ||> cons step) else first_pass (proof, contra) |>> cons (Assume (l, nth hyp_ts j)) - | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) = - let val step = Have (qs, l, t, ByMetis (ls, ss)) in + | first_pass (Prove (qs, l, t, By_Metis (ls, ss)) :: proof, contra) = + let val step = Prove (qs, l, t, By_Metis (ls, ss)) in if exists (member (op =) (fst contra)) ls then first_pass (proof, contra |>> cons l ||> cons step) else @@ -805,11 +810,11 @@ fun backpatch_labels patches ls = fold merge_fact_sets (map (backpatch_label patches) ls) ([], []) fun second_pass end_qs ([], assums, patches) = - ([Have (end_qs, no_label, concl_t, - ByMetis (backpatch_labels patches (map snd assums)))], patches) + ([Prove (end_qs, no_label, concl_t, + By_Metis (backpatch_labels patches (map snd assums)))], patches) | second_pass end_qs (Assume (l, t) :: proof, assums, patches) = second_pass end_qs (proof, (t, l) :: assums, patches) - | second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums, + | second_pass end_qs (Prove (qs, l, t, By_Metis (ls, ss)) :: proof, assums, patches) = (if member (op =) (snd (snd patches)) l andalso not (member (op =) (fst (snd patches)) l) andalso @@ -827,8 +832,8 @@ |>> cons (if member (op =) (fst (snd patches)) l then Assume (l, s_not t) else - Have (qs, l, s_not t, - ByMetis (backpatch_label patches l))) + Prove (qs, l, s_not t, + By_Metis (backpatch_label patches l))) | (contra_ls as _ :: _, co_ls) => let val proofs = @@ -854,12 +859,12 @@ in (case join_proofs proofs of SOME (l, t, proofs, proof_tail) => - Have (case_split_qualifiers proofs @ - (if null proof_tail then end_qs else []), l, t, - smart_case_split proofs facts) :: proof_tail + Prove (case_split_qualifiers proofs @ + (if null proof_tail then end_qs else []), l, t, + smart_case_split proofs facts) :: proof_tail | NONE => - [Have (case_split_qualifiers proofs @ end_qs, no_label, - concl_t, smart_case_split proofs facts)], + [Prove (case_split_qualifiers proofs @ end_qs, no_label, + concl_t, smart_case_split proofs facts)], patches) |>> append assumes end @@ -878,12 +883,13 @@ (case AList.lookup (op aconv) assums t of SOME l' => (proof, (l, l') :: subst, assums) | NONE => (step :: proof, subst, (t, l) :: assums)) - | do_step (Have (qs, l, t, by)) (proof, subst, assums) = - (Have (qs, l, t, - case by of - ByMetis facts => ByMetis (relabel_facts subst facts) - | CaseSplit (proofs, facts) => - CaseSplit (map do_proof proofs, relabel_facts subst facts)) :: + | do_step (Prove (qs, l, t, by)) (proof, subst, assums) = + (Prove (qs, l, t, + case by of + By_Metis facts => By_Metis (relabel_facts subst facts) + | Case_Split (proofs, facts) => + Case_Split (map do_proof proofs, + relabel_facts subst facts)) :: proof, subst, assums) | do_step step (proof, subst, assums) = (step :: proof, subst, assums) and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev @@ -893,16 +899,16 @@ let fun aux _ [] = [] | aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof - | aux l' (Have (qs, l, t, by) :: proof) = + | aux l' (Prove (qs, l, t, by) :: proof) = (case by of - ByMetis (ls, ss) => - Have (if member (op =) ls l' then - (Then :: qs, l, t, - ByMetis (filter_out (curry (op =) l') ls, ss)) - else - (qs, l, t, ByMetis (ls, ss))) - | CaseSplit (proofs, facts) => - Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) :: + By_Metis (ls, ss) => + Prove (if member (op =) ls l' then + (Then :: qs, l, t, + By_Metis (filter_out (curry (op =) l') ls, ss)) + else + (qs, l, t, By_Metis (ls, ss))) + | Case_Split (proofs, facts) => + Prove (qs, l, t, Case_Split (map (aux no_label) proofs, facts))) :: aux l proof | aux _ (step :: proof) = step :: aux no_label proof in aux no_label end @@ -912,12 +918,12 @@ val used_ls = used_labels_of proof fun do_label l = if member (op =) used_ls l then l else no_label fun do_step (Assume (l, t)) = Assume (do_label l, t) - | do_step (Have (qs, l, t, by)) = - Have (qs, do_label l, t, - case by of - CaseSplit (proofs, facts) => - CaseSplit (map (map do_step) proofs, facts) - | _ => by) + | do_step (Prove (qs, l, t, by)) = + Prove (qs, do_label l, t, + case by of + Case_Split (proofs, facts) => + Case_Split (map (map do_step) proofs, facts) + | _ => by) | do_step step = step in map do_step proof end @@ -934,7 +940,8 @@ Assume (l', t) :: aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof end - | aux subst depth (next_assum, next_fact) (Have (qs, l, t, by) :: proof) = + | aux subst depth (next_assum, next_fact) + (Prove (qs, l, t, by) :: proof) = let val (l', subst, next_fact) = if l = no_label then @@ -947,13 +954,12 @@ apfst (maps (the_list o AList.lookup (op =) subst)) val by = case by of - ByMetis facts => ByMetis (relabel_facts facts) - | CaseSplit (proofs, facts) => - CaseSplit (map (aux subst (depth + 1) (1, 1)) proofs, - relabel_facts facts) + By_Metis facts => By_Metis (relabel_facts facts) + | Case_Split (proofs, facts) => + Case_Split (map (aux subst (depth + 1) (1, 1)) proofs, + relabel_facts facts) in - Have (qs, l', t, by) :: - aux subst depth (next_assum, next_fact) proof + Prove (qs, l', t, by) :: aux subst depth (next_assum, next_fact) proof end | aux subst depth nextp (step :: proof) = step :: aux subst depth nextp proof @@ -992,12 +998,12 @@ do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n" | do_step ind (Assume (l, t)) = do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n" - | do_step ind (Have (qs, l, t, ByMetis facts)) = + | do_step ind (Prove (qs, l, t, By_Metis facts)) = do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n" - | do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) = - space_implode (do_indent ind ^ "moreover\n") - (map (do_block ind) proofs) ^ + | do_step ind (Prove (qs, l, t, Case_Split (proofs, facts))) = + implode (map (prefix (do_indent ind ^ "moreover\n") o do_block ind) + proofs) ^ do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n" and do_steps prefix suffix ind steps = @@ -1010,7 +1016,7 @@ and do_block ind proof = do_steps "{ " " }" (ind + 1) proof (* One-step proofs are pointless; better use the Metis one-liner directly. *) - and do_proof [Have (_, _, _, ByMetis _)] = "" + and do_proof [Prove (_, _, _, By_Metis _)] = "" | do_proof proof = (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^ @@ -1030,6 +1036,82 @@ if is_typed_helper_used_in_atp_proof atp_proof then full_typesN else partial_typesN val lam_trans = lam_trans_from_atp_proof atp_proof metis_default_lam_trans + + val atp_proof' = (*###*) + atp_proof + |> clean_up_atp_proof_dependencies + |> nasty_atp_proof pool + |> map_term_names_in_atp_proof repair_name + |> decode_lines ctxt sym_tab + |> rpair [] |-> fold_rev (add_line fact_names) + |> rpair [] |-> fold_rev add_nontrivial_line + |> rpair (0, []) + |-> fold_rev (add_desired_line isar_shrink_factor fact_names frees) + |> snd +(* + |> tap (map (tracing o PolyML.makestring)) +*) + + val conj_name = conjecture_prefix ^ string_of_int (length hyp_ts) + val conjs = + atp_proof' + |> map_filter (fn Inference (name as (_, ss), _, _, []) => + if member (op =) ss conj_name then SOME name else NONE + | _ => NONE) + + + fun dep_of_step (Definition _) = NONE + | dep_of_step (Inference (name, _, _, from)) = SOME (from, name) + + val ref_graph = atp_proof' |> map_filter dep_of_step |> make_ref_graph + val axioms = axioms_of_ref_graph ref_graph conjs + val tainted = tainted_atoms_of_ref_graph ref_graph conjs + + val props = + Symtab.empty + |> fold (fn Definition _ => I (* FIXME *) + | Inference ((s, _), t, _, _) => + Symtab.update_new (s, + t |> member (op = o apsnd fst) tainted s ? s_not)) + atp_proof' + + val direct_proof = + ref_graph |> redirect_graph axioms tainted + |> chain_direct_proof + |> tap (tracing o string_of_direct_proof) (*###*) + + fun prop_of_clause c = + fold (curry s_disj) (map_filter (Symtab.lookup props o fst) c) + @{term False} + + fun label_of_clause c = (space_implode "___" (map fst c), 0) + + fun maybe_show outer c = + (outer andalso length c = 1 andalso subset (op =) (c, conjs)) ? cons Show + + fun do_have outer qs (gamma, c) = + Prove (maybe_show outer c qs, label_of_clause c, prop_of_clause c, + By_Metis (fold (add_fact_from_dependency fact_names o the_single) + gamma ([], []))) + fun do_inf outer (Have z) = do_have outer [] z + | do_inf outer (Hence z) = do_have outer [Then] z + | do_inf outer (Cases cases) = + let val c = succedent_of_cases cases in + Prove (maybe_show outer c [Ultimately], label_of_clause c, + prop_of_clause c, + Case_Split (map (do_case false) cases, ([], []))) + end + and do_case outer (c, infs) = + Assume (label_of_clause c, prop_of_clause c) :: map (do_inf outer) infs + + val isar_proof = + (if null params then [] else [Fix params]) @ + (map (do_inf true) direct_proof + |> kill_useless_labels_in_proof + |> relabel_proof) + |> string_for_proof ctxt type_enc lam_trans subgoal subgoal_count + |> tap tracing (*###*) + fun isar_proof_for () = case atp_proof |> isar_proof_from_atp_proof pool ctxt isar_shrink_factor fact_names @@ -1052,13 +1134,12 @@ val isar_proof = if debug then isar_proof_for () - else - case try isar_proof_for () of - SOME s => s - | NONE => if isar_proof_requested then - "\nWarning: The Isar proof construction failed." - else - "" + else case try isar_proof_for () of + SOME s => s + | NONE => if isar_proof_requested then + "\nWarning: The Isar proof construction failed." + else + "" in one_line_proof ^ isar_proof end fun proof_text ctxt isar_proof isar_params diff -r 3be79bdcc702 -r 5d8a7fe36ce5 src/HOL/Tools/ATP/atp_redirect.ML --- 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 [] = "\" - | string_of_clause ls = space_implode " \ " (map signed_string_of_int ls) + | string_of_clause ls = space_implode " \ " (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;