356 val ([x], ctxt') = Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (concl_of th))] ctxt; |
356 val ([x], ctxt') = Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (concl_of th))] ctxt; |
357 val spec' = Thm.instantiate ([], [(spec_var, cert (Free (x, spec_varT)))]) spec; |
357 val spec' = Thm.instantiate ([], [(spec_var, cert (Free (x, spec_varT)))]) spec; |
358 in (th RS spec', ctxt') end |
358 in (th RS spec', ctxt') end |
359 end; |
359 end; |
360 |
360 |
361 (*Used with METAHYPS below. There is one assumption, which gets bound to prem |
|
362 and then normalized via function nf. The normal form is given to resolve_tac, |
|
363 instantiate a Boolean variable created by resolution with disj_forward. Since |
|
364 (nf prem) returns a LIST of theorems, we can backtrack to get all combinations.*) |
|
365 fun resop nf [prem] = resolve_tac (nf prem) 1; |
|
366 |
|
367 fun apply_skolem_theorem (th, rls) = |
361 fun apply_skolem_theorem (th, rls) = |
368 let |
362 let |
369 fun tryall [] = raise THM ("apply_skolem_theorem", 0, th::rls) |
363 fun tryall [] = raise THM ("apply_skolem_theorem", 0, th::rls) |
370 | tryall (rl :: rls) = |
364 | tryall (rl :: rls) = |
371 first_order_resolve th rl handle THM _ => tryall rls |
365 first_order_resolve th rl handle THM _ => tryall rls |
390 (*existential quantifier: Insert Skolem functions*) |
384 (*existential quantifier: Insert Skolem functions*) |
391 cnf_aux (apply_skolem_theorem (th, old_skolem_ths), ths) |
385 cnf_aux (apply_skolem_theorem (th, old_skolem_ths), ths) |
392 | Const (@{const_name HOL.disj}, _) => |
386 | Const (@{const_name HOL.disj}, _) => |
393 (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using |
387 (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using |
394 all combinations of converting P, Q to CNF.*) |
388 all combinations of converting P, Q to CNF.*) |
395 let val tac = |
389 (*There is one assumption, which gets bound to prem and then normalized via |
396 Misc_Legacy.METAHYPS ctxt (resop cnf_nil) 1 THEN |
390 cnf_nil. The normal form is given to resolve_tac, instantiate a Boolean |
397 (fn st' => st' |> Misc_Legacy.METAHYPS ctxt (resop cnf_nil) 1) |
391 variable created by resolution with disj_forward. Since (cnf_nil prem) |
398 in Seq.list_of (tac (th RS disj_forward)) @ ths end |
392 returns a LIST of theorems, we can backtrack to get all combinations.*) |
|
393 let val tac = Misc_Legacy.METAHYPS ctxt (fn [prem] => resolve_tac (cnf_nil prem) 1) 1 |
|
394 in Seq.list_of ((tac THEN tac) (th RS disj_forward)) @ ths end |
399 | _ => nodups ctxt th :: ths (*no work to do*) |
395 | _ => nodups ctxt th :: ths (*no work to do*) |
400 and cnf_nil th = cnf_aux (th, []) |
396 and cnf_nil th = cnf_aux (th, []) |
401 val cls = |
397 val cls = |
402 if has_too_many_clauses ctxt (concl_of th) then |
398 if has_too_many_clauses ctxt (concl_of th) then |
403 (trace_msg ctxt (fn () => |
399 (trace_msg ctxt (fn () => |