equal
deleted
inserted
replaced
683 SOME (from, name) |
683 SOME (from, name) |
684 val refute_graph = |
684 val refute_graph = |
685 atp_proof |> map_filter dep_of_step |> make_refute_graph |
685 atp_proof |> map_filter dep_of_step |> make_refute_graph |
686 val axioms = axioms_of_refute_graph refute_graph conjs |
686 val axioms = axioms_of_refute_graph refute_graph conjs |
687 val tainted = tainted_atoms_of_refute_graph refute_graph conjs |
687 val tainted = tainted_atoms_of_refute_graph refute_graph conjs |
|
688 val is_clause_tainted = exists (member (op =) tainted) |
688 val bot = atp_proof |> List.last |> dep_of_step |> the |> snd |
689 val bot = atp_proof |> List.last |> dep_of_step |> the |> snd |
689 val steps = |
690 val steps = |
690 Symtab.empty |
691 Symtab.empty |
691 |> fold (fn Definition_Step _ => I (* FIXME *) |
692 |> fold (fn Definition_Step _ => I (* FIXME *) |
692 | Inference_Step (name as (s, ss), role, t, rule, _) => |
693 | Inference_Step (name as (s, ss), role, t, rule, _) => |
693 Symtab.update_new (s, (rule, |
694 Symtab.update_new (s, (rule, |
694 t |> (if member (op = o apsnd fst) tainted s then |
695 t |> (if is_clause_tainted [name] then |
695 s_maybe_not role |
696 s_maybe_not role |
696 #> fold exists_of (map Var (Term.add_vars t [])) |
697 #> fold exists_of (map Var (Term.add_vars t [])) |
697 else |
698 else |
698 I)))) |
699 I)))) |
699 atp_proof |
700 atp_proof |
739 val t = prop_of_clause c |
740 val t = prop_of_clause c |
740 val by = |
741 val by = |
741 By_Metis (fold (add_fact_from_dependencies fact_names) gamma |
742 By_Metis (fold (add_fact_from_dependencies fact_names) gamma |
742 ([], [])) |
743 ([], [])) |
743 fun prove outer = Prove (maybe_show outer c [], l, t, by) |
744 fun prove outer = Prove (maybe_show outer c [], l, t, by) |
744 val redirected = exists (member (op =) tainted) c |
|
745 in |
745 in |
746 if redirected then |
746 if is_clause_tainted c then |
747 case gamma of |
747 case gamma of |
748 [g] => |
748 [g] => |
749 if is_clause_skolemize_rule g then |
749 if is_clause_skolemize_rule g andalso |
|
750 is_clause_tainted g then |
750 let |
751 let |
751 val proof = |
752 val proof = |
752 Fix (skolems_of (prop_of_clause g)) :: rev accum |
753 Fix (skolems_of (prop_of_clause g)) :: rev accum |
753 in |
754 in |
754 isar_proof_of_direct_proof outer |
755 isar_proof_of_direct_proof outer |