added new proof redirection code
authorblanchet
Wed Dec 14 18:07:32 2011 +0100 (2011-12-14)
changeset 45877b18f62e40429
parent 45876 40952db4e57b
child 45878 2dad374cf440
added new proof redirection code
src/HOL/ATP.thy
src/HOL/IsaMakefile
src/HOL/Tools/ATP/atp_redirect.ML
     1.1 --- a/src/HOL/ATP.thy	Wed Dec 14 18:07:32 2011 +0100
     1.2 +++ b/src/HOL/ATP.thy	Wed Dec 14 18:07:32 2011 +0100
     1.3 @@ -12,6 +12,7 @@
     1.4       "Tools/ATP/atp_util.ML"
     1.5       "Tools/ATP/atp_problem.ML"
     1.6       "Tools/ATP/atp_proof.ML"
     1.7 +     "Tools/ATP/atp_redirect.ML"
     1.8       ("Tools/ATP/atp_translate.ML")
     1.9       ("Tools/ATP/atp_reconstruct.ML")
    1.10       ("Tools/ATP/atp_systems.ML")
     2.1 --- a/src/HOL/IsaMakefile	Wed Dec 14 18:07:32 2011 +0100
     2.2 +++ b/src/HOL/IsaMakefile	Wed Dec 14 18:07:32 2011 +0100
     2.3 @@ -206,6 +206,7 @@
     2.4    Tools/ATP/atp_problem.ML \
     2.5    Tools/ATP/atp_proof.ML \
     2.6    Tools/ATP/atp_reconstruct.ML \
     2.7 +  Tools/ATP/atp_redirect.ML \
     2.8    Tools/ATP/atp_systems.ML \
     2.9    Tools/ATP/atp_translate.ML \
    2.10    Tools/ATP/atp_util.ML \
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/ATP/atp_redirect.ML	Wed Dec 14 18:07:32 2011 +0100
     3.3 @@ -0,0 +1,192 @@
     3.4 +(*  Title:      HOL/Tools/ATP/atp_redirect.ML
     3.5 +    Author:     Jasmin Blanchette, TU Muenchen
     3.6 +
     3.7 +Transformation of a proof by contradiction into a direct proof.
     3.8 +*)
     3.9 +
    3.10 +signature ATP_REDIRECT =
    3.11 +sig
    3.12 +  type ref_sequent = int list * int
    3.13 +  type ref_graph = unit Int_Graph.T
    3.14 +
    3.15 +  type clause = int list
    3.16 +  type direct_sequent = int list * clause
    3.17 +  type direct_graph = unit Int_Graph.T
    3.18 +
    3.19 +  type rich_sequent = clause list * clause
    3.20 +
    3.21 +  datatype inference =
    3.22 +    Have of rich_sequent |
    3.23 +    Hence of rich_sequent |
    3.24 +    Cases of (clause * inference list) list
    3.25 +
    3.26 +  type proof = inference list
    3.27 +
    3.28 +  val make_ref_graph : (int list * int) list -> ref_graph
    3.29 +  val sequents_of_ref_graph : ref_graph -> ref_sequent list
    3.30 +  val redirect_sequent : int list -> int -> ref_sequent -> direct_sequent
    3.31 +  val direct_graph : direct_sequent list -> direct_graph
    3.32 +  val redirect_graph : int list -> ref_graph -> proof
    3.33 +  val chain_proof : proof -> proof
    3.34 +  val string_of_proof : proof -> string
    3.35 +end;
    3.36 +
    3.37 +structure ATP_Redirect : ATP_REDIRECT =
    3.38 +struct
    3.39 +
    3.40 +type ref_sequent = int list * int
    3.41 +type ref_graph = unit Int_Graph.T
    3.42 +
    3.43 +type clause = int list
    3.44 +type direct_sequent = int list * clause
    3.45 +type direct_graph = unit Int_Graph.T
    3.46 +
    3.47 +type rich_sequent = clause list * clause
    3.48 +
    3.49 +datatype inference =
    3.50 +  Have of rich_sequent |
    3.51 +  Hence of rich_sequent |
    3.52 +  Cases of (clause * inference list) list
    3.53 +
    3.54 +type proof = inference list
    3.55 +
    3.56 +fun make_ref_graph infers =
    3.57 +  let
    3.58 +    fun add_edge to from =
    3.59 +      Int_Graph.default_node (from, ())
    3.60 +      #> Int_Graph.default_node (to, ())
    3.61 +      #> Int_Graph.add_edge_acyclic (from, to)
    3.62 +    fun add_infer (froms, to) = fold (add_edge to) froms
    3.63 +  in Int_Graph.empty |> fold add_infer infers end
    3.64 +
    3.65 +fun sequents_of_ref_graph g =
    3.66 +  map (`(Int_Graph.immediate_preds g))
    3.67 +      (filter_out (Int_Graph.is_minimal g) (Int_Graph.keys g))
    3.68 +
    3.69 +fun redirect_sequent tainted bot (ante, l) =
    3.70 +  if member (op =) tainted l then
    3.71 +    ante |> List.partition (not o member (op =) tainted) |>> l <> bot ? cons l
    3.72 +  else
    3.73 +    (ante, [l])
    3.74 +
    3.75 +fun direct_graph seqs =
    3.76 +  let
    3.77 +    fun add_edge from to =
    3.78 +      Int_Graph.default_node (from, ())
    3.79 +      #> Int_Graph.default_node (to, ())
    3.80 +      #> Int_Graph.add_edge_acyclic (from, to)
    3.81 +    fun add_seq (ante, c) = fold (fn l => fold (add_edge l) c) ante
    3.82 +  in Int_Graph.empty |> fold add_seq seqs end
    3.83 +
    3.84 +fun disj cs = fold (union (op =)) cs [] |> sort int_ord
    3.85 +
    3.86 +fun concl_of_inf (Have (_, c)) = c
    3.87 +  | concl_of_inf (Hence (_, c)) = c
    3.88 +  | concl_of_inf (Cases cases) = concl_of_cases cases
    3.89 +and concl_of_case (c, []) = c
    3.90 +  | concl_of_case (_, infs) = concl_of_inf (List.last infs)
    3.91 +and concl_of_cases cases = disj (map concl_of_case cases)
    3.92 +
    3.93 +fun dest_Have (Have z) = z
    3.94 +  | dest_Have _ = raise Fail "non-Have"
    3.95 +
    3.96 +fun enrich_Have nontrivs trivs (cs, c) =
    3.97 +  (cs |> map (fn c => if member (op =) nontrivs c then disj (c :: trivs)
    3.98 +                      else c),
    3.99 +   disj (c :: trivs))
   3.100 +  |> Have
   3.101 +
   3.102 +fun s_cases cases =
   3.103 +  case cases |> List.partition (null o snd) of
   3.104 +    (trivs, [(nontriv0, proof)]) =>
   3.105 +    if forall (can dest_Have) proof then
   3.106 +      let val seqs = proof |> map dest_Have in
   3.107 +        seqs |> map (enrich_Have (nontriv0 :: map snd seqs) (map fst trivs))
   3.108 +      end
   3.109 +    else
   3.110 +      [Cases cases]
   3.111 +  | _ => [Cases cases]
   3.112 +
   3.113 +fun descendants seqs =
   3.114 +  these o try (Int_Graph.all_succs (direct_graph seqs)) o single
   3.115 +
   3.116 +fun zones_of 0 _ = []
   3.117 +  | zones_of n (ls :: lss) =
   3.118 +    (fold (subtract (op =)) lss) ls :: zones_of (n - 1) (lss @ [ls])
   3.119 +
   3.120 +fun redirect c proved seqs =
   3.121 +  if null seqs then
   3.122 +    []
   3.123 +  else if length c < 2 then
   3.124 +    let
   3.125 +      val proved = c @ proved
   3.126 +      val provable = filter (fn (ante, _) => subset (op =) (ante, proved)) seqs
   3.127 +      val horn_provable = filter (fn (_, [_]) => true | _ => false) provable
   3.128 +      val seq as (ante, c) = hd (horn_provable @ provable)
   3.129 +    in
   3.130 +      Have (map single ante, c) ::
   3.131 +      redirect c proved (filter (curry (op <>) seq) seqs)
   3.132 +    end
   3.133 +  else
   3.134 +    let
   3.135 +      fun subsequents seqs zone =
   3.136 +        filter (fn (ante, _) => subset (op =) (ante, zone @ proved)) seqs
   3.137 +      val zones = zones_of (length c) (map (descendants seqs) c)
   3.138 +      val subseqss = map (subsequents seqs) zones
   3.139 +      val seqs = fold (subtract (op =)) subseqss seqs
   3.140 +      val cases =
   3.141 +        map2 (fn l => fn subseqs => ([l], redirect [l] proved subseqs))
   3.142 +             c subseqss
   3.143 +    in [Cases cases] @ redirect (concl_of_cases cases) proved seqs end
   3.144 +
   3.145 +fun redirect_graph conjecture g =
   3.146 +  let
   3.147 +    val axioms = subtract (op =) conjecture (Int_Graph.minimals g)
   3.148 +    val tainted = Int_Graph.all_succs g conjecture
   3.149 +    val [bot] = Int_Graph.maximals g
   3.150 +    val seqs = map (redirect_sequent tainted bot) (sequents_of_ref_graph g)
   3.151 +  in redirect [] axioms seqs end
   3.152 +
   3.153 +val chain_proof =
   3.154 +  let
   3.155 +    fun chain_inf cl0 (seq as Have (cs, c)) =
   3.156 +        if member (op =) cs cl0 then Hence (filter_out (curry (op =) cl0) cs, c)
   3.157 +        else seq
   3.158 +      | chain_inf _ (Cases cases) = Cases (map chain_case cases)
   3.159 +    and chain_case (c, is) = (c, chain_proof (SOME c) is)
   3.160 +    and chain_proof _ [] = []
   3.161 +      | chain_proof (SOME prev) (i :: is) =
   3.162 +        chain_inf prev i :: chain_proof (SOME (concl_of_inf i)) is
   3.163 +      | chain_proof _ (i :: is) = i :: chain_proof (SOME (concl_of_inf i)) is
   3.164 +  in chain_proof NONE end
   3.165 +
   3.166 +fun indent 0 = ""
   3.167 +  | indent n = "  " ^ indent (n - 1)
   3.168 +
   3.169 +fun string_of_clause [] = "\<bottom>"
   3.170 +  | string_of_clause ls = space_implode " \<or> " (map signed_string_of_int ls)
   3.171 +
   3.172 +fun string_of_rich_sequent ch ([], c) = ch ^ " " ^ string_of_clause c
   3.173 +  | string_of_rich_sequent ch (cs, c) =
   3.174 +    commas (map string_of_clause cs) ^ " " ^ ch ^ " " ^ string_of_clause c
   3.175 +
   3.176 +fun string_of_case depth (c, proof) =
   3.177 +  indent (depth + 1) ^ "[" ^ string_of_clause c ^ "]"
   3.178 +  |> not (null proof) ? suffix ("\n" ^ string_of_subproof (depth + 1) proof)
   3.179 +
   3.180 +and string_of_inference depth (Have seq) =
   3.181 +    indent depth ^ string_of_rich_sequent "\<triangleright>" seq
   3.182 +  | string_of_inference depth (Hence seq) =
   3.183 +    indent depth ^ string_of_rich_sequent "\<guillemotright>" seq
   3.184 +  | string_of_inference depth (Cases cases) =
   3.185 +    indent depth ^ "[\n" ^
   3.186 +    space_implode ("\n" ^ indent depth ^ "|\n")
   3.187 +                  (map (string_of_case depth) cases) ^ "\n" ^
   3.188 +    indent depth ^ "]"
   3.189 +
   3.190 +and string_of_subproof depth proof =
   3.191 +  cat_lines (map (string_of_inference depth) proof)
   3.192 +
   3.193 +val string_of_proof = string_of_subproof 0
   3.194 +
   3.195 +end;