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
blanchet@46320
     1
(*  Title:      HOL/Tools/ATP/atp_proof_redirect.ML
blanchet@45877
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@45877
     3
blanchet@45877
     4
Transformation of a proof by contradiction into a direct proof.
blanchet@45877
     5
*)
blanchet@45877
     6
blanchet@45882
     7
signature ATP_ATOM =
blanchet@45882
     8
sig
blanchet@45882
     9
  type key
blanchet@45882
    10
  val ord : key * key -> order
blanchet@45882
    11
  val string_of : key -> string
blanchet@45882
    12
end;
blanchet@45882
    13
blanchet@46320
    14
signature ATP_PROOF_REDIRECT =
blanchet@45877
    15
sig
blanchet@45882
    16
  type atom
blanchet@45882
    17
blanchet@45882
    18
  structure Atom_Graph : GRAPH
blanchet@45877
    19
blanchet@45882
    20
  type ref_sequent = atom list * atom
blanchet@45882
    21
  type ref_graph = unit Atom_Graph.T
blanchet@45882
    22
blanchet@45882
    23
  type clause = atom list
blanchet@45882
    24
  type direct_sequent = atom list * clause
blanchet@45882
    25
  type direct_graph = unit Atom_Graph.T
blanchet@45877
    26
blanchet@45877
    27
  type rich_sequent = clause list * clause
blanchet@45877
    28
blanchet@45882
    29
  datatype direct_inference =
blanchet@45877
    30
    Have of rich_sequent |
blanchet@45877
    31
    Hence of rich_sequent |
blanchet@45882
    32
    Cases of (clause * direct_inference list) list
blanchet@45882
    33
blanchet@45882
    34
  type direct_proof = direct_inference list
blanchet@45877
    35
blanchet@45882
    36
  val make_ref_graph : (atom list * atom) list -> ref_graph
blanchet@45882
    37
  val axioms_of_ref_graph : ref_graph -> atom list -> atom list
blanchet@45882
    38
  val tainted_atoms_of_ref_graph : ref_graph -> atom list -> atom list
blanchet@45877
    39
  val sequents_of_ref_graph : ref_graph -> ref_sequent list
blanchet@47915
    40
  val string_of_ref_graph : ref_graph -> string
blanchet@45882
    41
  val redirect_sequent : atom list -> atom -> ref_sequent -> direct_sequent
blanchet@45877
    42
  val direct_graph : direct_sequent list -> direct_graph
blanchet@45882
    43
  val redirect_graph : atom list -> atom list -> ref_graph -> direct_proof
blanchet@45882
    44
  val succedent_of_cases : (clause * direct_inference list) list -> clause
blanchet@45882
    45
  val chain_direct_proof : direct_proof -> direct_proof
blanchet@45882
    46
  val string_of_direct_proof : direct_proof -> string
blanchet@45877
    47
end;
blanchet@45877
    48
blanchet@46320
    49
functor ATP_Proof_Redirect(Atom : ATP_ATOM): ATP_PROOF_REDIRECT =
blanchet@45877
    50
struct
blanchet@45877
    51
blanchet@45882
    52
type atom = Atom.key
blanchet@45882
    53
blanchet@45882
    54
structure Atom_Graph = Graph(Atom)
blanchet@45877
    55
blanchet@45882
    56
type ref_sequent = atom list * atom
blanchet@45882
    57
type ref_graph = unit Atom_Graph.T
blanchet@45882
    58
blanchet@45882
    59
type clause = atom list
blanchet@45882
    60
type direct_sequent = atom list * clause
blanchet@45882
    61
type direct_graph = unit Atom_Graph.T
blanchet@45877
    62
blanchet@45877
    63
type rich_sequent = clause list * clause
blanchet@45877
    64
blanchet@45882
    65
datatype direct_inference =
blanchet@45877
    66
  Have of rich_sequent |
blanchet@45877
    67
  Hence of rich_sequent |
blanchet@45882
    68
  Cases of (clause * direct_inference list) list
blanchet@45882
    69
blanchet@45882
    70
type direct_proof = direct_inference list
blanchet@45877
    71
blanchet@45882
    72
fun atom_eq p = (Atom.ord p = EQUAL)
blanchet@45882
    73
fun clause_eq (c, d) = (length c = length d andalso forall atom_eq (c ~~ d))
blanchet@45882
    74
fun direct_sequent_eq ((gamma, c), (delta, d)) =
blanchet@45882
    75
  clause_eq (gamma, delta) andalso clause_eq (c, d)
blanchet@45877
    76
blanchet@45877
    77
fun make_ref_graph infers =
blanchet@45877
    78
  let
blanchet@45877
    79
    fun add_edge to from =
blanchet@45882
    80
      Atom_Graph.default_node (from, ())
blanchet@45882
    81
      #> Atom_Graph.default_node (to, ())
blanchet@45882
    82
      #> Atom_Graph.add_edge_acyclic (from, to)
blanchet@45877
    83
    fun add_infer (froms, to) = fold (add_edge to) froms
blanchet@45882
    84
  in Atom_Graph.empty |> fold add_infer infers end
blanchet@45882
    85
blanchet@45882
    86
fun axioms_of_ref_graph ref_graph conjs =
blanchet@45882
    87
  subtract atom_eq conjs (Atom_Graph.minimals ref_graph)
blanchet@45882
    88
fun tainted_atoms_of_ref_graph ref_graph = Atom_Graph.all_succs ref_graph
blanchet@45877
    89
blanchet@45882
    90
fun sequents_of_ref_graph ref_graph =
blanchet@45882
    91
  map (`(Atom_Graph.immediate_preds ref_graph))
blanchet@45882
    92
      (filter_out (Atom_Graph.is_minimal ref_graph) (Atom_Graph.keys ref_graph))
blanchet@45877
    93
blanchet@47915
    94
val string_of_context = map Atom.string_of #> space_implode ", "
blanchet@47915
    95
blanchet@47915
    96
fun string_of_sequent (gamma, c) =
blanchet@47915
    97
  string_of_context gamma ^ " \<turnstile> " ^ Atom.string_of c
blanchet@47915
    98
blanchet@47928
    99
fun string_of_ref_graph ref_graph =
blanchet@47928
   100
  ref_graph |> sequents_of_ref_graph |> map string_of_sequent |> cat_lines
blanchet@47915
   101
blanchet@45882
   102
fun redirect_sequent tainted bot (gamma, c) =
blanchet@45882
   103
  if member atom_eq tainted c then
blanchet@45882
   104
    gamma |> List.partition (not o member atom_eq tainted)
blanchet@45882
   105
          |>> not (atom_eq (c, bot)) ? cons c
blanchet@45877
   106
  else
blanchet@45882
   107
    (gamma, [c])
blanchet@45877
   108
blanchet@45877
   109
fun direct_graph seqs =
blanchet@45877
   110
  let
blanchet@45877
   111
    fun add_edge from to =
blanchet@45882
   112
      Atom_Graph.default_node (from, ())
blanchet@45882
   113
      #> Atom_Graph.default_node (to, ())
blanchet@45882
   114
      #> Atom_Graph.add_edge_acyclic (from, to)
blanchet@45882
   115
    fun add_seq (gamma, c) = fold (fn l => fold (add_edge l) c) gamma
blanchet@45882
   116
  in Atom_Graph.empty |> fold add_seq seqs end
blanchet@45877
   117
blanchet@45882
   118
fun disj cs = fold (union atom_eq) cs [] |> sort Atom.ord
blanchet@45877
   119
blanchet@45882
   120
fun succedent_of_inference (Have (_, c)) = c
blanchet@45882
   121
  | succedent_of_inference (Hence (_, c)) = c
blanchet@45882
   122
  | succedent_of_inference (Cases cases) = succedent_of_cases cases
blanchet@45882
   123
and succedent_of_case (c, []) = c
blanchet@45882
   124
  | succedent_of_case (_, infs) = succedent_of_inference (List.last infs)
blanchet@45882
   125
and succedent_of_cases cases = disj (map succedent_of_case cases)
blanchet@45877
   126
blanchet@45877
   127
fun dest_Have (Have z) = z
blanchet@45877
   128
  | dest_Have _ = raise Fail "non-Have"
blanchet@45877
   129
blanchet@45877
   130
fun enrich_Have nontrivs trivs (cs, c) =
blanchet@45882
   131
  (cs |> map (fn c => if member clause_eq nontrivs c then disj (c :: trivs)
blanchet@45877
   132
                      else c),
blanchet@45877
   133
   disj (c :: trivs))
blanchet@45877
   134
  |> Have
blanchet@45877
   135
blanchet@45877
   136
fun s_cases cases =
blanchet@45877
   137
  case cases |> List.partition (null o snd) of
blanchet@45882
   138
    (trivs, nontrivs as [(nontriv0, proof)]) =>
blanchet@45877
   139
    if forall (can dest_Have) proof then
blanchet@45877
   140
      let val seqs = proof |> map dest_Have in
blanchet@45877
   141
        seqs |> map (enrich_Have (nontriv0 :: map snd seqs) (map fst trivs))
blanchet@45877
   142
      end
blanchet@45877
   143
    else
blanchet@45882
   144
      [Cases nontrivs]
blanchet@45882
   145
  | (_, nontrivs) => [Cases nontrivs]
blanchet@45877
   146
blanchet@45882
   147
fun descendants direct_graph =
blanchet@45882
   148
  these o try (Atom_Graph.all_succs direct_graph) o single
blanchet@45877
   149
blanchet@45877
   150
fun zones_of 0 _ = []
blanchet@45882
   151
  | zones_of n (bs :: bss) =
blanchet@45882
   152
    (fold (subtract atom_eq) bss) bs :: zones_of (n - 1) (bss @ [bs])
blanchet@45882
   153
blanchet@45882
   154
fun redirect_graph axioms tainted ref_graph =
blanchet@45882
   155
  let
blanchet@47930
   156
    val bot =
blanchet@47930
   157
      case Atom_Graph.maximals ref_graph of
blanchet@47930
   158
        [bot] => bot
blanchet@47930
   159
      | bots => raise Fail ("malformed refutation graph with " ^
blanchet@47930
   160
                            string_of_int (length bots) ^ " maximal nodes")
blanchet@45882
   161
    val seqs =
blanchet@45882
   162
      map (redirect_sequent tainted bot) (sequents_of_ref_graph ref_graph)
blanchet@45882
   163
    val direct_graph = direct_graph seqs
blanchet@45877
   164
blanchet@45882
   165
    fun redirect c proved seqs =
blanchet@45882
   166
      if null seqs then
blanchet@45882
   167
        []
blanchet@45882
   168
      else if length c < 2 then
blanchet@45882
   169
        let
blanchet@45882
   170
          val proved = c @ proved
blanchet@45882
   171
          val provable =
blanchet@45882
   172
            filter (fn (gamma, _) => subset atom_eq (gamma, proved)) seqs
blanchet@45882
   173
          val horn_provable = filter (fn (_, [_]) => true | _ => false) provable
blanchet@45882
   174
          val seq as (gamma, c) = hd (horn_provable @ provable)
blanchet@45882
   175
        in
blanchet@45882
   176
          Have (map single gamma, c) ::
blanchet@45882
   177
          redirect c proved (filter (curry (not o direct_sequent_eq) seq) seqs)
blanchet@45882
   178
        end
blanchet@45882
   179
      else
blanchet@45882
   180
        let
blanchet@45882
   181
          fun subsequents seqs zone =
blanchet@45882
   182
            filter (fn (gamma, _) => subset atom_eq (gamma, zone @ proved)) seqs
blanchet@45882
   183
          val zones = zones_of (length c) (map (descendants direct_graph) c)
blanchet@45882
   184
          val subseqss = map (subsequents seqs) zones
blanchet@45882
   185
          val seqs = fold (subtract direct_sequent_eq) subseqss seqs
blanchet@45882
   186
          val cases =
blanchet@45882
   187
            map2 (fn l => fn subseqs => ([l], redirect [l] proved subseqs))
blanchet@45882
   188
                 c subseqss
blanchet@45882
   189
        in s_cases cases @ redirect (succedent_of_cases cases) proved seqs end
blanchet@45877
   190
  in redirect [] axioms seqs end
blanchet@45877
   191
blanchet@45882
   192
val chain_direct_proof =
blanchet@45877
   193
  let
blanchet@45877
   194
    fun chain_inf cl0 (seq as Have (cs, c)) =
blanchet@45882
   195
        if member clause_eq cs cl0 then
blanchet@45882
   196
          Hence (filter_out (curry clause_eq cl0) cs, c)
blanchet@45882
   197
        else
blanchet@45882
   198
          seq
blanchet@45877
   199
      | chain_inf _ (Cases cases) = Cases (map chain_case cases)
blanchet@45877
   200
    and chain_case (c, is) = (c, chain_proof (SOME c) is)
blanchet@45877
   201
    and chain_proof _ [] = []
blanchet@45877
   202
      | chain_proof (SOME prev) (i :: is) =
blanchet@45882
   203
        chain_inf prev i :: chain_proof (SOME (succedent_of_inference i)) is
blanchet@45882
   204
      | chain_proof _ (i :: is) =
blanchet@45882
   205
        i :: chain_proof (SOME (succedent_of_inference i)) is
blanchet@45877
   206
  in chain_proof NONE end
blanchet@45877
   207
blanchet@45877
   208
fun indent 0 = ""
blanchet@45877
   209
  | indent n = "  " ^ indent (n - 1)
blanchet@45877
   210
blanchet@45877
   211
fun string_of_clause [] = "\<bottom>"
blanchet@45882
   212
  | string_of_clause ls = space_implode " \<or> " (map Atom.string_of ls)
blanchet@45877
   213
blanchet@45877
   214
fun string_of_rich_sequent ch ([], c) = ch ^ " " ^ string_of_clause c
blanchet@45877
   215
  | string_of_rich_sequent ch (cs, c) =
blanchet@45877
   216
    commas (map string_of_clause cs) ^ " " ^ ch ^ " " ^ string_of_clause c
blanchet@45877
   217
blanchet@45877
   218
fun string_of_case depth (c, proof) =
blanchet@45877
   219
  indent (depth + 1) ^ "[" ^ string_of_clause c ^ "]"
blanchet@45877
   220
  |> not (null proof) ? suffix ("\n" ^ string_of_subproof (depth + 1) proof)
blanchet@45877
   221
blanchet@45877
   222
and string_of_inference depth (Have seq) =
blanchet@45877
   223
    indent depth ^ string_of_rich_sequent "\<triangleright>" seq
blanchet@45877
   224
  | string_of_inference depth (Hence seq) =
blanchet@45877
   225
    indent depth ^ string_of_rich_sequent "\<guillemotright>" seq
blanchet@45877
   226
  | string_of_inference depth (Cases cases) =
blanchet@45877
   227
    indent depth ^ "[\n" ^
blanchet@45877
   228
    space_implode ("\n" ^ indent depth ^ "|\n")
blanchet@45877
   229
                  (map (string_of_case depth) cases) ^ "\n" ^
blanchet@45877
   230
    indent depth ^ "]"
blanchet@45877
   231
blanchet@45882
   232
and string_of_subproof depth = cat_lines o map (string_of_inference depth)
blanchet@45877
   233
blanchet@45882
   234
val string_of_direct_proof = string_of_subproof 0
blanchet@45877
   235
blanchet@45877
   236
end;