# HG changeset patch # User smolkas # Date 1360878562 -3600 # Node ID 0021ea86112905e0ed530d8f1e250b680d674e5e # Parent 5cf1604b9ef550ecc2872f6551097b66e7240d1d introduced subblock in isar_step datatype for conjecture herbrandization diff -r 5cf1604b9ef5 -r 0021ea861129 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Feb 14 21:31:25 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Feb 14 22:49:22 2013 +0100 @@ -92,7 +92,9 @@ :: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t) | _ => error "preplay error: malformed case split") #> make_thm) - cases) + cases + (* TODO: implement *) + | Subblock _ => []) val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug |> obtain ? Config.put Metis_Tactic.new_skolem true val goal = diff -r 5cf1604b9ef5 -r 0021ea861129 src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Thu Feb 14 21:31:25 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Thu Feb 14 22:49:22 2013 +0100 @@ -22,7 +22,8 @@ Prove of isar_qualifier list * label * term * byline and byline = By_Metis of facts | - Case_Split of isar_step list list * facts + Case_Split of isar_step list list * facts | + Subblock of isar_step list val string_for_label : label -> string val metis_steps_top_level : isar_step list -> int @@ -45,7 +46,8 @@ Prove of isar_qualifier list * label * term * byline and byline = By_Metis of facts | - Case_Split of isar_step list list * facts + Case_Split of isar_step list list * facts | + Subblock of isar_step list fun string_for_label (s, num) = s ^ string_of_int num @@ -57,6 +59,8 @@ | Prove (_, _, _, By_Metis _) => Integer.add 1 | Prove (_, _, _, Case_Split (cases, _)) => Integer.add (fold (Integer.add o metis_steps_total) cases 1) + | Prove (_, _, _, Subblock subproof) => + Integer.add (metis_steps_total subproof) | _ => I) proof 0 end diff -r 5cf1604b9ef5 -r 0021ea861129 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Feb 14 21:31:25 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Feb 14 22:49:22 2013 +0100 @@ -499,14 +499,14 @@ (E and Vampire -- but see also "atp_proof_reconstruct.ML" regarding Vampire). *) do_metis ind "using [[metis_new_skolem]] " facts ^ "\n" - | do_step ind (Prove (qs, l, t, By_Metis facts)) = - do_indent ind ^ do_have qs ^ " " ^ - do_label l ^ do_term t ^ do_metis ind "" facts ^ "\n" + | do_step ind (Prove (qs, l, t, By_Metis facts)) = + do_prove ind qs l t facts | do_step ind (Prove (qs, l, t, Case_Split (proofs, facts))) = implode (map (prefix (do_indent ind ^ "moreover\n") o do_block ind) proofs) ^ - do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ - do_metis ind "" facts ^ "\n" + do_prove ind qs l t facts + | do_step ind (Prove (qs, l, t, Subblock proof)) = + do_block ind proof ^ do_prove ind qs l t ([], []) and do_steps prefix suffix ind steps = let val s = implode (map (do_step ind) steps) in replicate_string (ind * indent_size - size prefix) " " ^ prefix ^ @@ -515,6 +515,9 @@ suffix ^ "\n" end and do_block ind proof = do_steps "{ " " }" (ind + 1) proof + and do_prove ind qs l t facts = + do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ + do_metis ind "" facts ^ "\n" (* One-step proofs are pointless; better use the Metis one-liner directly. *) and do_proof [Prove (_, _, _, By_Metis _)] = "" @@ -529,7 +532,8 @@ (case by of By_Metis (ls, _) => ls | Case_Split (proofs, (ls, _)) => - fold (union (op =) o used_labels_of) proofs ls) + fold (union (op =) o used_labels_of) proofs ls + | Subblock proof => used_labels_of proof) | used_labels_of_step _ = [] and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof [] @@ -543,10 +547,12 @@ Prove (qs, do_label l, t, case by of Case_Split (proofs, facts) => - Case_Split (map (map do_step) proofs, facts) + Case_Split (map do_proof proofs, facts) + | Subblock proof => Subblock (do_proof proof) | _ => by) | do_step step = step - in map do_step proof end + and do_proof proof = map do_step proof + in do_proof proof end fun prefix_for_depth n = replicate_string (n + 1) @@ -561,12 +567,13 @@ end fun do_facts subst = apfst (maps (the_list o AList.lookup (op =) subst)) - fun do_byline subst depth by = + fun do_byline subst depth nexts by = case by of By_Metis facts => By_Metis (do_facts subst facts) | Case_Split (proofs, facts) => Case_Split (map (do_proof subst (depth + 1) (1, 1)) proofs, do_facts subst facts) + | Subblock proof => Subblock (do_proof subst depth nexts proof) and do_proof _ _ _ [] = [] | do_proof subst depth (next_assum, next_have) (Assume (l, t) :: proof) = if l = no_label then @@ -576,26 +583,26 @@ Assume (l', t) :: do_proof ((l, l') :: subst) depth (next_assum + 1, next_have) proof end - | do_proof subst depth (next_assum, next_have) + | do_proof subst depth (nexts as (next_assum, next_have)) (Obtain (qs, xs, l, t, by) :: proof) = let val (l, subst, next_have) = (l, subst, next_have) |> fresh_label depth - val by = by |> do_byline subst depth + val by = by |> do_byline subst depth nexts in Obtain (qs, xs, l, t, by) :: do_proof subst depth (next_assum, next_have) proof end - | do_proof subst depth (next_assum, next_have) + | do_proof subst depth (nexts as (next_assum, next_have)) (Prove (qs, l, t, by) :: proof) = let val (l, subst, next_have) = (l, subst, next_have) |> fresh_label depth - val by = by |> do_byline subst depth + val by = by |> do_byline subst depth nexts in Prove (qs, l, t, by) :: do_proof subst depth (next_assum, next_have) proof end - | do_proof subst depth nextp (step :: proof) = - step :: do_proof subst depth nextp proof + | do_proof subst depth nexts (step :: proof) = + step :: do_proof subst depth nexts proof in do_proof [] 0 (1, 1) end val chain_direct_proof = @@ -617,7 +624,9 @@ else step | chain_step _ (Prove (qs, l, t, Case_Split (proofs, facts))) = - Prove (qs, l, t, Case_Split ((map (chain_proof NONE) proofs), facts)) + Prove (qs, l, t, Case_Split (map (chain_proof NONE) proofs, facts)) + | chain_step _ (Prove (qs, l, t, Subblock proof)) = + Prove (qs, l, t, Subblock (chain_proof NONE proof)) | chain_step _ step = step and chain_proof _ [] = [] | chain_proof (prev as SOME _) (i :: is) = diff -r 5cf1604b9ef5 -r 0021ea861129 src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Thu Feb 14 21:31:25 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Thu Feb 14 22:49:22 2013 +0100 @@ -91,6 +91,7 @@ | refs (Prove (_, _, _, By_Metis (lfs, _))) = lookup_indices lfs | refs (Prove (_, _, _, Case_Split (cases, (lfs, _)))) = lookup_indices lfs @ maps (maps refs) cases + | refs (Prove (_, _, _, Subblock proof)) = maps refs proof | refs _ = [] val refed_by_vect = Vector.tabulate (n, (fn _ => [])) @@ -218,24 +219,27 @@ | enrich_with_step _ = I val rich_ctxt = fold enrich_with_step proof ctxt - (* Shrink case_splits and top-levl *) + (* Shrink subproofs (case_splits and subblocks) and top-levl *) val ((proof, top_level_time), lower_level_time) = - proof |> do_case_splits rich_ctxt + proof |> do_subproof rich_ctxt |>> shrink_top_level on_top_level rich_ctxt in (proof, add_preplay_time lower_level_time top_level_time) end - and do_case_splits ctxt proof = + and do_subproof ctxt proof = let fun shrink_each_and_collect_time shrink candidates = let fun f_m cand time = shrink cand ||> add_preplay_time time in fold_map f_m candidates zero_preplay_time end - val shrink_case_split = + val shrink_subproof = shrink_each_and_collect_time (do_proof false ctxt) fun shrink (Prove (qs, l, t, Case_Split (cases, facts))) = - let val (cases, time) = shrink_case_split cases + let val (cases, time) = shrink_subproof cases in (Prove (qs, l, t, Case_Split (cases, facts)), time) end + | shrink (Prove (qs, l, t, Subblock proof)) = + let val ([proof], time) = shrink_subproof [proof] + in (Prove (qs, l, t, Subblock proof), time) end | shrink step = (step, zero_preplay_time) in shrink_each_and_collect_time shrink proof