summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | blanchet |

Wed, 11 Dec 2013 22:23:07 +0800 | |

changeset 54714 | ae01c51eadff |

parent 54713 | 6666fc0b9ebc |

child 54715 | a13aa1cac0e8 |

removed inlined rewriting'' for one-branch case splits in Isar proofs, since these can yield huge unreadable formulas

--- a/src/HOL/Tools/ATP/atp_proof_redirect.ML Wed Dec 11 00:17:09 2013 +0000 +++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML Wed Dec 11 22:23:07 2013 +0800 @@ -39,8 +39,7 @@ val string_of_refute_graph : refute_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 -> refute_graph -> direct_proof + val redirect_graph : atom list -> atom list -> atom -> refute_graph -> direct_proof val succedent_of_cases : (clause * direct_inference list) list -> clause val string_of_direct_proof : direct_proof -> string end; @@ -82,7 +81,9 @@ fun add_infer (froms, to) = fold (add_edge to) froms val graph = fold add_infer infers Atom_Graph.empty val reachable = Atom_Graph.all_preds graph [bot] - in graph |> Atom_Graph.restrict (member (is_equal o Atom.ord) reachable) end + in + graph |> Atom_Graph.restrict (member (is_equal o Atom.ord) reachable) + end fun axioms_of_refute_graph refute_graph conjs = subtract atom_eq conjs (Atom_Graph.minimals refute_graph) @@ -91,17 +92,16 @@ Atom_Graph.all_succs refute_graph fun sequents_of_refute_graph refute_graph = - map (`(Atom_Graph.immediate_preds refute_graph)) - (filter_out (Atom_Graph.is_minimal refute_graph) - (Atom_Graph.keys refute_graph)) + Atom_Graph.keys refute_graph + |> filter_out (Atom_Graph.is_minimal refute_graph) + |> map (`(Atom_Graph.immediate_preds refute_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_refute_graph refute_graph = - refute_graph |> sequents_of_refute_graph |> map string_of_sequent |> cat_lines +val string_of_refute_graph = sequents_of_refute_graph #> map string_of_sequent #> cat_lines fun redirect_sequent tainted bot (gamma, c) = if member atom_eq tainted c then @@ -131,28 +131,15 @@ | 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), + Have (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 s_cases cases = [Cases (filter_out (null o snd) cases)] -fun descendants direct_graph = - these o try (Atom_Graph.all_succs direct_graph) o single +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]) + | zones_of n (bs :: bss) = (fold (subtract atom_eq) bss) bs :: zones_of (n - 1) (bss @ [bs]) fun redirect_graph axioms tainted bot refute_graph = let @@ -165,13 +152,12 @@ else if length c < 2 then let val proved = c @ proved - val provable = - filter (fn (gamma, _) => subset atom_eq (gamma, proved)) seqs + val provable = filter (fn (gamma, _) => subset atom_eq (gamma, proved)) seqs val horn_provable = filter (fn (_, [_]) => true | _ => false) provable val seq as (gamma, c) = - case horn_provable @ provable of + (case horn_provable @ provable of [] => raise Fail "ill-formed refutation graph" - | next :: _ => next + | next :: _ => next) in Have (map single gamma, c) :: redirect c proved (filter (curry (not o direct_sequent_eq) seq) seqs) @@ -183,10 +169,10 @@ 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 + 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 = ""