89 fun tryres (th, rls) = |
89 fun tryres (th, rls) = |
90 let fun tryall [] = raise THM("tryres", 0, th::rls) |
90 let fun tryall [] = raise THM("tryres", 0, th::rls) |
91 | tryall (rl::rls) = (th RS rl handle THM _ => tryall rls) |
91 | tryall (rl::rls) = (th RS rl handle THM _ => tryall rls) |
92 in tryall rls end; |
92 in tryall rls end; |
93 |
93 |
94 (*Permits forward proof from rules that discharge assumptions*) |
94 (*Permits forward proof from rules that discharge assumptions. The supplied proof state st, |
|
95 e.g. from conj_forward, should have the form |
|
96 "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q" |
|
97 and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*) |
95 fun forward_res nf st = |
98 fun forward_res nf st = |
96 case Seq.pull (ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)) st) |
99 let fun forward_tacf [prem] = rtac (nf prem) 1 |
97 of SOME(th,_) => th |
100 | forward_tacf prems = |
98 | NONE => raise THM("forward_res", 0, [st]); |
101 error ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:\n" ^ |
99 |
102 string_of_thm st ^ |
|
103 "\nPremises:\n" ^ |
|
104 cat_lines (map string_of_thm prems)) |
|
105 in |
|
106 case Seq.pull (ALLGOALS (METAHYPS forward_tacf) st) |
|
107 of SOME(th,_) => th |
|
108 | NONE => raise THM("forward_res", 0, [st]) |
|
109 end; |
100 |
110 |
101 (*Are any of the logical connectives in "bs" present in the term?*) |
111 (*Are any of the logical connectives in "bs" present in the term?*) |
102 fun has_conns bs = |
112 fun has_conns bs = |
103 let fun has (Const(a,_)) = false |
113 let fun has (Const(a,_)) = false |
104 | has (Const("Trueprop",_) $ p) = has p |
114 | has (Const("Trueprop",_) $ p) = has p |
419 |
429 |
420 val nnf_ss = |
430 val nnf_ss = |
421 HOL_basic_ss addsimps nnf_extra_simps |
431 HOL_basic_ss addsimps nnf_extra_simps |
422 addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc]; |
432 addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc]; |
423 |
433 |
424 fun make_nnf th = th |> rewrite_rule (map safe_mk_meta_eq nnf_simps) |
434 fun make_nnf th = case prems_of th of |
425 |> simplify nnf_ss (*But this doesn't simplify premises...*) |
435 [] => th |> rewrite_rule (map safe_mk_meta_eq nnf_simps) |
426 |> make_nnf1 |
436 |> simplify nnf_ss (*But this doesn't simplify premises...*) |
|
437 |> make_nnf1 |
|
438 | _ => raise THM ("make_nnf: premises in argument", 0, [th]); |
427 |
439 |
428 (*Pull existential quantifiers to front. This accomplishes Skolemization for |
440 (*Pull existential quantifiers to front. This accomplishes Skolemization for |
429 clauses that arise from a subgoal.*) |
441 clauses that arise from a subgoal.*) |
430 fun skolemize th = |
442 fun skolemize th = |
431 if not (has_conns ["Ex"] (prop_of th)) then th |
443 if not (has_conns ["Ex"] (prop_of th)) then th |