summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Tools/Meson/meson.ML

changeset 59171 | 75ec7271b426 |

parent 59165 | 115965966e15 |

child 59498 | 50b60f501b05 |

1.1 --- a/src/HOL/Tools/Meson/meson.ML Sun Dec 21 22:49:17 2014 +0100 1.2 +++ b/src/HOL/Tools/Meson/meson.ML Sun Dec 21 22:49:40 2014 +0100 1.3 @@ -358,12 +358,6 @@ 1.4 in (th RS spec', ctxt') end 1.5 end; 1.6 1.7 -(*Used with METAHYPS below. There is one assumption, which gets bound to prem 1.8 - and then normalized via function nf. The normal form is given to resolve_tac, 1.9 - instantiate a Boolean variable created by resolution with disj_forward. Since 1.10 - (nf prem) returns a LIST of theorems, we can backtrack to get all combinations.*) 1.11 -fun resop nf [prem] = resolve_tac (nf prem) 1; 1.12 - 1.13 fun apply_skolem_theorem (th, rls) = 1.14 let 1.15 fun tryall [] = raise THM ("apply_skolem_theorem", 0, th::rls) 1.16 @@ -392,10 +386,12 @@ 1.17 | Const (@{const_name HOL.disj}, _) => 1.18 (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using 1.19 all combinations of converting P, Q to CNF.*) 1.20 - let val tac = 1.21 - Misc_Legacy.METAHYPS ctxt (resop cnf_nil) 1 THEN 1.22 - (fn st' => st' |> Misc_Legacy.METAHYPS ctxt (resop cnf_nil) 1) 1.23 - in Seq.list_of (tac (th RS disj_forward)) @ ths end 1.24 + (*There is one assumption, which gets bound to prem and then normalized via 1.25 + cnf_nil. The normal form is given to resolve_tac, instantiate a Boolean 1.26 + variable created by resolution with disj_forward. Since (cnf_nil prem) 1.27 + returns a LIST of theorems, we can backtrack to get all combinations.*) 1.28 + let val tac = Misc_Legacy.METAHYPS ctxt (fn [prem] => resolve_tac (cnf_nil prem) 1) 1 1.29 + in Seq.list_of ((tac THEN tac) (th RS disj_forward)) @ ths end 1.30 | _ => nodups ctxt th :: ths (*no work to do*) 1.31 and cnf_nil th = cnf_aux (th, []) 1.32 val cls =