# HG changeset patch # User wenzelm # Date 1357739961 -3600 # Node ID 8f42d300748fa83126dc096cd39ca25809e9f2e7 # Parent 4174abe2c5fd1909761ac1947a486dc8373c1463# Parent a26f7cf81d2f416d12087ca6866db80164a62224 merged diff -r a26f7cf81d2f -r 8f42d300748f src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Wed Jan 09 14:01:50 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Wed Jan 09 14:59:21 2013 +0100 @@ -68,13 +68,14 @@ val metis_fail = ref false in fun handle_metis_fail try_metis () = - try_metis () handle _ => (metis_fail := true; SOME Time.zeroTime) + try_metis () handle exp => + (if debug then raise exp else metis_fail := true; SOME Time.zeroTime) fun get_time lazy_time = if !metis_fail then SOME Time.zeroTime else Lazy.force lazy_time val metis_fail = fn () => !metis_fail end - (* Shrink top level proof - do not shrink case splits *) + (* Shrink proof on top level - do not shrink case splits *) fun shrink_top_level on_top_level ctxt proof = let (* proof vector *) @@ -104,11 +105,12 @@ (* candidates for elimination, use table as priority queue (greedy algorithm) *) - (* TODO: consider adding "Obtain" cases *) fun add_if_cand proof_vect (i, [j]) = (case (the (get i proof_vect), the (get j proof_vect)) of (Prove (_, _, t, By_Metis _), Prove (_, _, _, By_Metis _)) => - cons (Term.size_of_term t, i) + cons (Term.size_of_term t, i) + | (Prove (_, _, t, By_Metis _), Obtain (_, _, _, _, By_Metis _)) => + cons (Term.size_of_term t, i) | _ => I) | add_if_cand _ _ = I val cand_tab = @@ -123,32 +125,64 @@ |> maps (thms_of_name ctxt) (* TODO: add "Obtain" case *) - fun try_metis timeout (succedent, Prove (_, _, t, byline)) = - if not preplay then K (SOME Time.zeroTime) else - let - val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt) - val facts = - (case byline of - By_Metis fact_names => resolve_fact_names fact_names - | Case_Split (cases, fact_names) => - resolve_fact_names fact_names - @ (case the succedent of - Assume (_, t) => make_thm t - | Obtain (_, _, _, t, _) => make_thm t - | Prove (_, _, t, _) => make_thm t - | _ => error "Internal error: unexpected succedent of case split") - :: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t) - | _ => error "Internal error: malformed case split") - #> make_thm) - cases) - val goal = - Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t - fun tac {context = ctxt, prems = _} = - Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1 - in - take_time timeout (fn () => goal tac) - end - | try_metis _ _ = K (SOME Time.zeroTime) + exception ZeroTime + fun try_metis timeout (succedent, step) = + (if not preplay then K (SOME Time.zeroTime) else + let + val (t, byline, obtain) = + (case step of + Prove (_, _, t, byline) => (t, byline, false) + | Obtain (_, xs, _, t, byline) => + (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis + (see ~~/src/Pure/Isar/obtain.ML) *) + let + (*val thesis = Term.Free ("thesis", HOLogic.boolT) + |> HOLogic.mk_Trueprop + val frees = map Term.Free xs + + (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *) + val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis)) + + (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *) + val prop = Logic.all thesis (Logic.mk_implies (inner_prop, thesis))*) + + val thesis = Term.Free ("thesis", HOLogic.boolT) + val prop = + HOLogic.mk_imp (HOLogic.dest_Trueprop t, thesis) + |> fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) xs + |> rpair thesis + |> HOLogic.mk_imp + |> (fn t => HOLogic.mk_all ("thesis", HOLogic.boolT, t)) + |> HOLogic.mk_Trueprop + in + (prop, byline, true) + end + | _ => raise ZeroTime) + val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt) + val facts = + (case byline of + By_Metis fact_names => resolve_fact_names fact_names + | Case_Split (cases, fact_names) => + resolve_fact_names fact_names + @ (case the succedent of + Assume (_, t) => make_thm t + | Obtain (_, _, _, t, _) => make_thm t + | Prove (_, _, t, _) => make_thm t + | _ => error "Internal error: unexpected succedent of case split") + :: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t) + | _ => error "Internal error: malformed case split") + #> make_thm) + cases) + val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug + |> obtain ? Config.put Metis_Tactic.new_skolem true + val goal = + Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t + fun tac {context = ctxt, prems = _} = + Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1 + in + take_time timeout (fn () => goal tac) + end) + handle ZeroTime => K (SOME Time.zeroTime) val try_metis_quietly = the_default NONE oo try oo try_metis @@ -167,12 +201,17 @@ (* Merging *) (* TODO: consider adding "Obtain" cases *) - fun merge (Prove (_, label1, _, By_Metis (lfs1, gfs1))) - (Prove (qs2, label2, t, By_Metis (lfs2, gfs2))) = + fun merge (Prove (_, label1, _, By_Metis (lfs1, gfs1))) step2 = let + val (step_constructor, lfs2, gfs2) = + (case step2 of + (Prove (qs2, label2, t, By_Metis (lfs2, gfs2))) => + (fn by => Prove (qs2, label2, t, by), lfs2, gfs2) + | (Obtain(qs2, xs, label2, t, By_Metis (lfs2, gfs2))) => + (fn by => Obtain (qs2, xs, label2, t, by), lfs2, gfs2) ) val lfs = remove (op =) label1 lfs2 |> union (op =) lfs1 val gfs = union (op =) gfs1 gfs2 - in Prove (qs2, label2, t, By_Metis (lfs, gfs)) end + in step_constructor (By_Metis (lfs, gfs)) end | merge _ _ = error "Internal error: Unmergeable Isar steps" fun try_merge metis_time (s1, i) (s2, j) =