1.1 --- a/src/HOL/Tools/ATP/atp_redirect.ML Mon Jan 23 17:40:31 2012 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,223 +0,0 @@
1.4 -(* Title: HOL/Tools/ATP/atp_redirect.ML
1.5 - Author: Jasmin Blanchette, TU Muenchen
1.6 -
1.7 -Transformation of a proof by contradiction into a direct proof.
1.8 -*)
1.9 -
1.10 -signature ATP_ATOM =
1.11 -sig
1.12 - type key
1.13 - val ord : key * key -> order
1.14 - val string_of : key -> string
1.15 -end;
1.16 -
1.17 -signature ATP_REDIRECT =
1.18 -sig
1.19 - type atom
1.20 -
1.21 - structure Atom_Graph : GRAPH
1.22 -
1.23 - type ref_sequent = atom list * atom
1.24 - type ref_graph = unit Atom_Graph.T
1.25 -
1.26 - type clause = atom list
1.27 - type direct_sequent = atom list * clause
1.28 - type direct_graph = unit Atom_Graph.T
1.29 -
1.30 - type rich_sequent = clause list * clause
1.31 -
1.32 - datatype direct_inference =
1.33 - Have of rich_sequent |
1.34 - Hence of rich_sequent |
1.35 - Cases of (clause * direct_inference list) list
1.36 -
1.37 - type direct_proof = direct_inference list
1.38 -
1.39 - val make_ref_graph : (atom list * atom) list -> ref_graph
1.40 - val axioms_of_ref_graph : ref_graph -> atom list -> atom list
1.41 - val tainted_atoms_of_ref_graph : ref_graph -> atom list -> atom list
1.42 - val sequents_of_ref_graph : ref_graph -> ref_sequent list
1.43 - val redirect_sequent : atom list -> atom -> ref_sequent -> direct_sequent
1.44 - val direct_graph : direct_sequent list -> direct_graph
1.45 - val redirect_graph : atom list -> atom list -> ref_graph -> direct_proof
1.46 - val succedent_of_cases : (clause * direct_inference list) list -> clause
1.47 - val chain_direct_proof : direct_proof -> direct_proof
1.48 - val string_of_direct_proof : direct_proof -> string
1.49 -end;
1.50 -
1.51 -functor ATP_Redirect(Atom : ATP_ATOM): ATP_REDIRECT =
1.52 -struct
1.53 -
1.54 -type atom = Atom.key
1.55 -
1.56 -structure Atom_Graph = Graph(Atom)
1.57 -
1.58 -type ref_sequent = atom list * atom
1.59 -type ref_graph = unit Atom_Graph.T
1.60 -
1.61 -type clause = atom list
1.62 -type direct_sequent = atom list * clause
1.63 -type direct_graph = unit Atom_Graph.T
1.64 -
1.65 -type rich_sequent = clause list * clause
1.66 -
1.67 -datatype direct_inference =
1.68 - Have of rich_sequent |
1.69 - Hence of rich_sequent |
1.70 - Cases of (clause * direct_inference list) list
1.71 -
1.72 -type direct_proof = direct_inference list
1.73 -
1.74 -fun atom_eq p = (Atom.ord p = EQUAL)
1.75 -fun clause_eq (c, d) = (length c = length d andalso forall atom_eq (c ~~ d))
1.76 -fun direct_sequent_eq ((gamma, c), (delta, d)) =
1.77 - clause_eq (gamma, delta) andalso clause_eq (c, d)
1.78 -
1.79 -fun make_ref_graph infers =
1.80 - let
1.81 - fun add_edge to from =
1.82 - Atom_Graph.default_node (from, ())
1.83 - #> Atom_Graph.default_node (to, ())
1.84 - #> Atom_Graph.add_edge_acyclic (from, to)
1.85 - fun add_infer (froms, to) = fold (add_edge to) froms
1.86 - in Atom_Graph.empty |> fold add_infer infers end
1.87 -
1.88 -fun axioms_of_ref_graph ref_graph conjs =
1.89 - subtract atom_eq conjs (Atom_Graph.minimals ref_graph)
1.90 -fun tainted_atoms_of_ref_graph ref_graph = Atom_Graph.all_succs ref_graph
1.91 -
1.92 -fun sequents_of_ref_graph ref_graph =
1.93 - map (`(Atom_Graph.immediate_preds ref_graph))
1.94 - (filter_out (Atom_Graph.is_minimal ref_graph) (Atom_Graph.keys ref_graph))
1.95 -
1.96 -fun redirect_sequent tainted bot (gamma, c) =
1.97 - if member atom_eq tainted c then
1.98 - gamma |> List.partition (not o member atom_eq tainted)
1.99 - |>> not (atom_eq (c, bot)) ? cons c
1.100 - else
1.101 - (gamma, [c])
1.102 -
1.103 -fun direct_graph seqs =
1.104 - let
1.105 - fun add_edge from to =
1.106 - Atom_Graph.default_node (from, ())
1.107 - #> Atom_Graph.default_node (to, ())
1.108 - #> Atom_Graph.add_edge_acyclic (from, to)
1.109 - fun add_seq (gamma, c) = fold (fn l => fold (add_edge l) c) gamma
1.110 - in Atom_Graph.empty |> fold add_seq seqs end
1.111 -
1.112 -fun disj cs = fold (union atom_eq) cs [] |> sort Atom.ord
1.113 -
1.114 -fun succedent_of_inference (Have (_, c)) = c
1.115 - | succedent_of_inference (Hence (_, c)) = c
1.116 - | succedent_of_inference (Cases cases) = succedent_of_cases cases
1.117 -and succedent_of_case (c, []) = c
1.118 - | succedent_of_case (_, infs) = succedent_of_inference (List.last infs)
1.119 -and succedent_of_cases cases = disj (map succedent_of_case cases)
1.120 -
1.121 -fun dest_Have (Have z) = z
1.122 - | dest_Have _ = raise Fail "non-Have"
1.123 -
1.124 -fun enrich_Have nontrivs trivs (cs, c) =
1.125 - (cs |> map (fn c => if member clause_eq nontrivs c then disj (c :: trivs)
1.126 - else c),
1.127 - disj (c :: trivs))
1.128 - |> Have
1.129 -
1.130 -fun s_cases cases =
1.131 - case cases |> List.partition (null o snd) of
1.132 - (trivs, nontrivs as [(nontriv0, proof)]) =>
1.133 - if forall (can dest_Have) proof then
1.134 - let val seqs = proof |> map dest_Have in
1.135 - seqs |> map (enrich_Have (nontriv0 :: map snd seqs) (map fst trivs))
1.136 - end
1.137 - else
1.138 - [Cases nontrivs]
1.139 - | (_, nontrivs) => [Cases nontrivs]
1.140 -
1.141 -fun descendants direct_graph =
1.142 - these o try (Atom_Graph.all_succs direct_graph) o single
1.143 -
1.144 -fun zones_of 0 _ = []
1.145 - | zones_of n (bs :: bss) =
1.146 - (fold (subtract atom_eq) bss) bs :: zones_of (n - 1) (bss @ [bs])
1.147 -
1.148 -fun redirect_graph axioms tainted ref_graph =
1.149 - let
1.150 - val [bot] = Atom_Graph.maximals ref_graph
1.151 - val seqs =
1.152 - map (redirect_sequent tainted bot) (sequents_of_ref_graph ref_graph)
1.153 - val direct_graph = direct_graph seqs
1.154 -
1.155 - fun redirect c proved seqs =
1.156 - if null seqs then
1.157 - []
1.158 - else if length c < 2 then
1.159 - let
1.160 - val proved = c @ proved
1.161 - val provable =
1.162 - filter (fn (gamma, _) => subset atom_eq (gamma, proved)) seqs
1.163 - val horn_provable = filter (fn (_, [_]) => true | _ => false) provable
1.164 - val seq as (gamma, c) = hd (horn_provable @ provable)
1.165 - in
1.166 - Have (map single gamma, c) ::
1.167 - redirect c proved (filter (curry (not o direct_sequent_eq) seq) seqs)
1.168 - end
1.169 - else
1.170 - let
1.171 - fun subsequents seqs zone =
1.172 - filter (fn (gamma, _) => subset atom_eq (gamma, zone @ proved)) seqs
1.173 - val zones = zones_of (length c) (map (descendants direct_graph) c)
1.174 - val subseqss = map (subsequents seqs) zones
1.175 - val seqs = fold (subtract direct_sequent_eq) subseqss seqs
1.176 - val cases =
1.177 - map2 (fn l => fn subseqs => ([l], redirect [l] proved subseqs))
1.178 - c subseqss
1.179 - in s_cases cases @ redirect (succedent_of_cases cases) proved seqs end
1.180 - in redirect [] axioms seqs end
1.181 -
1.182 -val chain_direct_proof =
1.183 - let
1.184 - fun chain_inf cl0 (seq as Have (cs, c)) =
1.185 - if member clause_eq cs cl0 then
1.186 - Hence (filter_out (curry clause_eq cl0) cs, c)
1.187 - else
1.188 - seq
1.189 - | chain_inf _ (Cases cases) = Cases (map chain_case cases)
1.190 - and chain_case (c, is) = (c, chain_proof (SOME c) is)
1.191 - and chain_proof _ [] = []
1.192 - | chain_proof (SOME prev) (i :: is) =
1.193 - chain_inf prev i :: chain_proof (SOME (succedent_of_inference i)) is
1.194 - | chain_proof _ (i :: is) =
1.195 - i :: chain_proof (SOME (succedent_of_inference i)) is
1.196 - in chain_proof NONE end
1.197 -
1.198 -fun indent 0 = ""
1.199 - | indent n = " " ^ indent (n - 1)
1.200 -
1.201 -fun string_of_clause [] = "\<bottom>"
1.202 - | string_of_clause ls = space_implode " \<or> " (map Atom.string_of ls)
1.203 -
1.204 -fun string_of_rich_sequent ch ([], c) = ch ^ " " ^ string_of_clause c
1.205 - | string_of_rich_sequent ch (cs, c) =
1.206 - commas (map string_of_clause cs) ^ " " ^ ch ^ " " ^ string_of_clause c
1.207 -
1.208 -fun string_of_case depth (c, proof) =
1.209 - indent (depth + 1) ^ "[" ^ string_of_clause c ^ "]"
1.210 - |> not (null proof) ? suffix ("\n" ^ string_of_subproof (depth + 1) proof)
1.211 -
1.212 -and string_of_inference depth (Have seq) =
1.213 - indent depth ^ string_of_rich_sequent "\<triangleright>" seq
1.214 - | string_of_inference depth (Hence seq) =
1.215 - indent depth ^ string_of_rich_sequent "\<guillemotright>" seq
1.216 - | string_of_inference depth (Cases cases) =
1.217 - indent depth ^ "[\n" ^
1.218 - space_implode ("\n" ^ indent depth ^ "|\n")
1.219 - (map (string_of_case depth) cases) ^ "\n" ^
1.220 - indent depth ^ "]"
1.221 -
1.222 -and string_of_subproof depth = cat_lines o map (string_of_inference depth)
1.223 -
1.224 -val string_of_direct_proof = string_of_subproof 0
1.225 -
1.226 -end;