src/HOL/Tools/ATP/atp_proof_redirect.ML
author blanchet
Wed May 16 18:16:51 2012 +0200 (2012-05-16)
changeset 47930 c06aa331bb76
parent 47928 fb2bc5a1eb32
child 50004 c96e8e40d789
permissions -rw-r--r--
more helpful error message
     1 (*  Title:      HOL/Tools/ATP/atp_proof_redirect.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3 
     4 Transformation of a proof by contradiction into a direct proof.
     5 *)
     6 
     7 signature ATP_ATOM =
     8 sig
     9   type key
    10   val ord : key * key -> order
    11   val string_of : key -> string
    12 end;
    13 
    14 signature ATP_PROOF_REDIRECT =
    15 sig
    16   type atom
    17 
    18   structure Atom_Graph : GRAPH
    19 
    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
    26 
    27   type rich_sequent = clause list * clause
    28 
    29   datatype direct_inference =
    30     Have of rich_sequent |
    31     Hence of rich_sequent |
    32     Cases of (clause * direct_inference list) list
    33 
    34   type direct_proof = direct_inference list
    35 
    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
    39   val sequents_of_ref_graph : ref_graph -> ref_sequent list
    40   val string_of_ref_graph : ref_graph -> string
    41   val redirect_sequent : atom list -> atom -> ref_sequent -> direct_sequent
    42   val direct_graph : direct_sequent list -> direct_graph
    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
    47 end;
    48 
    49 functor ATP_Proof_Redirect(Atom : ATP_ATOM): ATP_PROOF_REDIRECT =
    50 struct
    51 
    52 type atom = Atom.key
    53 
    54 structure Atom_Graph = Graph(Atom)
    55 
    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
    62 
    63 type rich_sequent = clause list * clause
    64 
    65 datatype direct_inference =
    66   Have of rich_sequent |
    67   Hence of rich_sequent |
    68   Cases of (clause * direct_inference list) list
    69 
    70 type direct_proof = direct_inference list
    71 
    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)
    76 
    77 fun make_ref_graph infers =
    78   let
    79     fun add_edge to from =
    80       Atom_Graph.default_node (from, ())
    81       #> Atom_Graph.default_node (to, ())
    82       #> Atom_Graph.add_edge_acyclic (from, to)
    83     fun add_infer (froms, to) = fold (add_edge to) froms
    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
    89 
    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))
    93 
    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 fun string_of_ref_graph ref_graph =
   100   ref_graph |> sequents_of_ref_graph |> map string_of_sequent |> cat_lines
   101 
   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
   106   else
   107     (gamma, [c])
   108 
   109 fun direct_graph seqs =
   110   let
   111     fun add_edge from to =
   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
   117 
   118 fun disj cs = fold (union atom_eq) cs [] |> sort Atom.ord
   119 
   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)
   126 
   127 fun dest_Have (Have z) = z
   128   | dest_Have _ = raise Fail "non-Have"
   129 
   130 fun enrich_Have nontrivs trivs (cs, c) =
   131   (cs |> map (fn c => if member clause_eq nontrivs c then disj (c :: trivs)
   132                       else c),
   133    disj (c :: trivs))
   134   |> Have
   135 
   136 fun s_cases cases =
   137   case cases |> List.partition (null o snd) of
   138     (trivs, nontrivs as [(nontriv0, proof)]) =>
   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
   144       [Cases nontrivs]
   145   | (_, nontrivs) => [Cases nontrivs]
   146 
   147 fun descendants direct_graph =
   148   these o try (Atom_Graph.all_succs direct_graph) o single
   149 
   150 fun zones_of 0 _ = []
   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 =
   157       case Atom_Graph.maximals ref_graph of
   158         [bot] => bot
   159       | bots => raise Fail ("malformed refutation graph with " ^
   160                             string_of_int (length bots) ^ " maximal nodes")
   161     val seqs =
   162       map (redirect_sequent tainted bot) (sequents_of_ref_graph ref_graph)
   163     val direct_graph = direct_graph seqs
   164 
   165     fun redirect c proved seqs =
   166       if null seqs then
   167         []
   168       else if length c < 2 then
   169         let
   170           val proved = c @ proved
   171           val provable =
   172             filter (fn (gamma, _) => subset atom_eq (gamma, proved)) seqs
   173           val horn_provable = filter (fn (_, [_]) => true | _ => false) provable
   174           val seq as (gamma, c) = hd (horn_provable @ provable)
   175         in
   176           Have (map single gamma, c) ::
   177           redirect c proved (filter (curry (not o direct_sequent_eq) seq) seqs)
   178         end
   179       else
   180         let
   181           fun subsequents seqs zone =
   182             filter (fn (gamma, _) => subset atom_eq (gamma, zone @ proved)) seqs
   183           val zones = zones_of (length c) (map (descendants direct_graph) c)
   184           val subseqss = map (subsequents seqs) zones
   185           val seqs = fold (subtract direct_sequent_eq) subseqss seqs
   186           val cases =
   187             map2 (fn l => fn subseqs => ([l], redirect [l] proved subseqs))
   188                  c subseqss
   189         in s_cases cases @ redirect (succedent_of_cases cases) proved seqs end
   190   in redirect [] axioms seqs end
   191 
   192 val chain_direct_proof =
   193   let
   194     fun chain_inf cl0 (seq as Have (cs, c)) =
   195         if member clause_eq cs cl0 then
   196           Hence (filter_out (curry clause_eq cl0) cs, c)
   197         else
   198           seq
   199       | chain_inf _ (Cases cases) = Cases (map chain_case cases)
   200     and chain_case (c, is) = (c, chain_proof (SOME c) is)
   201     and chain_proof _ [] = []
   202       | chain_proof (SOME prev) (i :: is) =
   203         chain_inf prev i :: chain_proof (SOME (succedent_of_inference i)) is
   204       | chain_proof _ (i :: is) =
   205         i :: chain_proof (SOME (succedent_of_inference i)) is
   206   in chain_proof NONE end
   207 
   208 fun indent 0 = ""
   209   | indent n = "  " ^ indent (n - 1)
   210 
   211 fun string_of_clause [] = "\<bottom>"
   212   | string_of_clause ls = space_implode " \<or> " (map Atom.string_of ls)
   213 
   214 fun string_of_rich_sequent ch ([], c) = ch ^ " " ^ string_of_clause c
   215   | string_of_rich_sequent ch (cs, c) =
   216     commas (map string_of_clause cs) ^ " " ^ ch ^ " " ^ string_of_clause c
   217 
   218 fun string_of_case depth (c, proof) =
   219   indent (depth + 1) ^ "[" ^ string_of_clause c ^ "]"
   220   |> not (null proof) ? suffix ("\n" ^ string_of_subproof (depth + 1) proof)
   221 
   222 and string_of_inference depth (Have seq) =
   223     indent depth ^ string_of_rich_sequent "\<triangleright>" seq
   224   | string_of_inference depth (Hence seq) =
   225     indent depth ^ string_of_rich_sequent "\<guillemotright>" seq
   226   | string_of_inference depth (Cases cases) =
   227     indent depth ^ "[\n" ^
   228     space_implode ("\n" ^ indent depth ^ "|\n")
   229                   (map (string_of_case depth) cases) ^ "\n" ^
   230     indent depth ^ "]"
   231 
   232 and string_of_subproof depth = cat_lines o map (string_of_inference depth)
   233 
   234 val string_of_direct_proof = string_of_subproof 0
   235 
   236 end;