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

author | paulson |

Wed, 18 Oct 2006 10:15:39 +0200 | |

changeset 21050 | d0447a511edb |

parent 21049 | 379542c9d951 |

child 21051 | c49467a9c1e1 |

More robust error handling in make_nnf and forward_res

--- a/src/HOL/Tools/meson.ML Wed Oct 18 10:07:36 2006 +0200 +++ b/src/HOL/Tools/meson.ML Wed Oct 18 10:15:39 2006 +0200 @@ -91,12 +91,22 @@ | tryall (rl::rls) = (th RS rl handle THM _ => tryall rls) in tryall rls end; -(*Permits forward proof from rules that discharge assumptions*) +(*Permits forward proof from rules that discharge assumptions. The supplied proof state st, + e.g. from conj_forward, should have the form + "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q" + and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*) fun forward_res nf st = - case Seq.pull (ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)) st) - of SOME(th,_) => th - | NONE => raise THM("forward_res", 0, [st]); - + let fun forward_tacf [prem] = rtac (nf prem) 1 + | forward_tacf prems = + error ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:\n" ^ + string_of_thm st ^ + "\nPremises:\n" ^ + cat_lines (map string_of_thm prems)) + in + case Seq.pull (ALLGOALS (METAHYPS forward_tacf) st) + of SOME(th,_) => th + | NONE => raise THM("forward_res", 0, [st]) + end; (*Are any of the logical connectives in "bs" present in the term?*) fun has_conns bs = @@ -421,9 +431,11 @@ HOL_basic_ss addsimps nnf_extra_simps addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc]; -fun make_nnf th = th |> rewrite_rule (map safe_mk_meta_eq nnf_simps) - |> simplify nnf_ss (*But this doesn't simplify premises...*) - |> make_nnf1 +fun make_nnf th = case prems_of th of + [] => th |> rewrite_rule (map safe_mk_meta_eq nnf_simps) + |> simplify nnf_ss (*But this doesn't simplify premises...*) + |> make_nnf1 + | _ => raise THM ("make_nnf: premises in argument", 0, [th]); (*Pull existential quantifiers to front. This accomplishes Skolemization for clauses that arise from a subgoal.*)