equal
deleted
inserted
replaced
313 else |
313 else |
314 let |
314 let |
315 (* optimization: convert the given clauses from "[c_i] |- c_i" to *) |
315 (* optimization: convert the given clauses from "[c_i] |- c_i" to *) |
316 (* "[c_1 && ... && c_n] |- c_i"; this avoids accumulation of *) |
316 (* "[c_1 && ... && c_n] |- c_i"; this avoids accumulation of *) |
317 (* hypotheses during resolution *) |
317 (* hypotheses during resolution *) |
318 (* Thm.cterm list -> Thm.cterm *) |
|
319 fun mk_conjunction_list [x] = x |
|
320 | mk_conjunction_list (x::xs) = Conjunction.mk_conjunction (x, mk_conjunction_list xs) |
|
321 (* [c_1 && ... && c_n] |- c_1 && ... && c_n *) |
318 (* [c_1 && ... && c_n] |- c_1 && ... && c_n *) |
322 val cnf_cterm = mk_conjunction_list (map cprop_of non_triv_clauses) |
319 val cnf_cterm = Conjunction.mk_conjunction_list (map cprop_of non_triv_clauses) |
323 val cnf_thm = Thm.assume cnf_cterm |
320 val cnf_thm = Thm.assume cnf_cterm |
324 (* cf. Conjunction.elim_list *) |
321 (* cf. Conjunction.elim_list *) |
325 fun right_elim_list th = |
322 fun right_elim_list th = |
326 let val (th1, th2) = Conjunction.elim th |
323 let val (th1, th2) = Conjunction.elim th |
327 in th1 :: right_elim_list th2 end handle THM _ => [th] |
324 in th1 :: right_elim_list th2 end handle THM _ => [th] |