src/HOL/Tools/ATP/atp_proof_redirect.ML

more robustness in Isar proof reconstruction (cf. bug report by Ondrej)

(*  Title:      HOL/Tools/ATP/atp_proof_redirect.ML
    Author:     Jasmin Blanchette, TU Muenchen

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_PROOF_REDIRECT =
sig
  type atom

  structure Atom_Graph : GRAPH

  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 direct_inference =
    Have of rich_sequent |
    Cases of (clause * direct_inference list) list

  type direct_proof = direct_inference list

  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 string_of_ref_graph : ref_graph -> string
  val redirect_sequent : atom list -> atom -> ref_sequent -> direct_sequent
  val direct_graph : direct_sequent list -> direct_graph
  val redirect_graph :
    atom list -> atom list -> atom -> ref_graph -> direct_proof
  val succedent_of_cases : (clause * direct_inference list) list -> clause
  val string_of_direct_proof : direct_proof -> string
end;

functor ATP_Proof_Redirect(Atom : ATP_ATOM): ATP_PROOF_REDIRECT =
struct

type atom = Atom.key

structure Atom_Graph = Graph(Atom)

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 direct_inference =
  Have of rich_sequent |
  Cases of (clause * direct_inference list) list

type direct_proof = direct_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 =
      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 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 ref_graph =
  map (`(Atom_Graph.immediate_preds ref_graph))
      (filter_out (Atom_Graph.is_minimal ref_graph) (Atom_Graph.keys ref_graph))

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

fun string_of_sequent (gamma, c) =
  string_of_context gamma ^ " \<turnstile> " ^ Atom.string_of c

fun string_of_ref_graph ref_graph =
  ref_graph |> sequents_of_ref_graph |> map string_of_sequent |> cat_lines

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
    (gamma, [c])

fun direct_graph seqs =
  let
    fun add_edge from to =
      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 atom_eq) cs [] |> sort Atom.ord

fun succedent_of_inference (Have (_, 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 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, 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 nontrivs]
  | (_, nontrivs) => [Cases nontrivs]

fun descendants direct_graph =
  these o try (Atom_Graph.all_succs direct_graph) o single

fun zones_of 0 _ = []
  | zones_of n (bs :: bss) =
    (fold (subtract atom_eq) bss) bs :: zones_of (n - 1) (bss @ [bs])

fun redirect_graph axioms tainted bot ref_graph =
  let
    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 (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

fun indent 0 = ""
  | indent n = "  " ^ indent (n - 1)

fun string_of_clause [] = "\<bottom>"
  | 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) =
    commas (map string_of_clause cs) ^ " " ^ ch ^ " " ^ string_of_clause c

fun string_of_case depth (c, proof) =
  indent (depth + 1) ^ "[" ^ string_of_clause c ^ "]"
  |> not (null proof) ? suffix ("\n" ^ string_of_subproof (depth + 1) proof)

and string_of_inference depth (Have seq) =
    indent depth ^ string_of_rich_sequent "\<triangleright>" seq
  | string_of_inference depth (Cases cases) =
    indent depth ^ "[\n" ^
    space_implode ("\n" ^ indent depth ^ "|\n")
                  (map (string_of_case depth) cases) ^ "\n" ^
    indent depth ^ "]"

and string_of_subproof depth = cat_lines o map (string_of_inference depth)

val string_of_direct_proof = string_of_subproof 0

end;