# HG changeset patch # User boehmes # Date 1267033164 -3600 # Node ID 5c937073e1d5ed56aeb9791b5a368cf21868c22e # Parent 0df9c8a37f64e0aa8c56cecf5197e9ebebefecb1 added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals diff -r 0df9c8a37f64 -r 5c937073e1d5 src/HOL/Boogie/Tools/boogie_commands.ML --- a/src/HOL/Boogie/Tools/boogie_commands.ML Wed Feb 24 07:06:39 2010 -0800 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML Wed Feb 24 18:39:24 2010 +0100 @@ -30,7 +30,8 @@ VC_Take of int list * (bool * string list) option | VC_Only of string list | VC_Without of string list | - VC_Examine of string list + VC_Examine of string list | + VC_Single of string fun get_vc thy vc_name = (case Boogie_VCs.lookup thy vc_name of @@ -42,11 +43,37 @@ | _ => error ("There is no verification condition " ^ quote vc_name ^ "."))) +local + fun split_goal t = + (case Boogie_Tactics.split t of + [tp] => tp + | _ => error "Multiple goals.") + + fun single_prep t = + let + val (us, u) = split_goal t + val assms = [((@{binding vc_trace}, []), map (rpair []) us)] + in + pair [u] o snd o ProofContext.add_assms_i Assumption.assume_export assms + end + + fun single_prove goal ctxt thm = + Goal.prove ctxt [] [] goal (fn {context, ...} => HEADGOAL ( + Boogie_Tactics.split_tac + THEN' Boogie_Tactics.drop_assert_at_tac + THEN' SUBPROOF (fn _ => Tactic.rtac thm 1) context)) +in fun boogie_vc (vc_name, vc_opts) lthy = let val thy = ProofContext.theory_of lthy val vc = get_vc thy vc_name + fun extract vc l = + (case Boogie_VCs.extract vc l of + SOME vc' => vc' + | NONE => error ("There is no assertion to be proved with label " ^ + quote l ^ ".")) + val vcs = (case vc_opts of VC_Complete => [vc] @@ -55,18 +82,29 @@ | VC_Take (ps, SOME (false, ls)) => [Boogie_VCs.paths_without ps ls vc] | VC_Only ls => [Boogie_VCs.only ls vc] | VC_Without ls => [Boogie_VCs.without ls vc] - | VC_Examine ls => map_filter (Boogie_VCs.extract vc) ls) + | VC_Examine ls => map (extract vc) ls + | VC_Single l => [extract vc l]) val ts = map Boogie_VCs.prop_of_vc vcs + val (prepare, finish) = + (case vc_opts of + VC_Single _ => (single_prep (hd ts), single_prove (hd ts)) + | _ => (pair ts, K I)) + val discharge = fold (Boogie_VCs.discharge o pair vc_name) fun after_qed [thms] = Local_Theory.theory (discharge (vcs ~~ thms)) | after_qed _ = I in lthy |> fold Variable.auto_fixes ts - |> Proof.theorem_i NONE after_qed [map (rpair []) ts] + |> (fn lthy1 => lthy1 + |> prepare + |-> (fn us => fn lthy2 => lthy2 + |> Proof.theorem_i NONE (fn thmss => fn ctxt => + let val export = map (finish lthy1) o ProofContext.export ctxt lthy2 + in after_qed (map export thmss) ctxt end) [map (rpair []) us])) end - +end fun write_list head = map Pretty.str o sort (dict_ord string_ord o pairself explode) #> @@ -239,7 +277,8 @@ val vc_name = OuterParse.name -val vc_labels = Scan.repeat1 OuterParse.name +val vc_label = OuterParse.name +val vc_labels = Scan.repeat1 vc_label val vc_paths = OuterParse.nat -- (Args.$$$ "-" |-- OuterParse.nat) >> (op upto) || @@ -247,13 +286,14 @@ val vc_opts = scan_arg - (scan_val "examine" vc_labels >> VC_Examine || + (scan_val "assertion" vc_label >> VC_Single || + scan_val "examine" vc_labels >> VC_Examine || scan_val "take" ((OuterParse.list vc_paths >> flat) -- Scan.option ( scan_val "without" vc_labels >> pair false || scan_val "and_also" vc_labels >> pair true) >> VC_Take) || scan_val "only" vc_labels >> VC_Only || scan_val "without" vc_labels >> VC_Without) || - Scan.succeed VC_Complete + Scan.succeed VC_Complete val _ = OuterSyntax.command "boogie_vc" diff -r 0df9c8a37f64 -r 5c937073e1d5 src/HOL/Boogie/Tools/boogie_tactics.ML --- a/src/HOL/Boogie/Tools/boogie_tactics.ML Wed Feb 24 07:06:39 2010 -0800 +++ b/src/HOL/Boogie/Tools/boogie_tactics.ML Wed Feb 24 18:39:24 2010 +0100 @@ -9,6 +9,9 @@ val unfold_labels_tac: Proof.context -> int -> tactic val boogie_tac: Proof.context -> thm list -> int -> tactic val boogie_all_tac: Proof.context -> thm list -> tactic + val split: term -> (term list * term) list + val split_tac: int -> tactic + val drop_assert_at_tac: int -> tactic val setup: theory -> theory end @@ -47,25 +50,38 @@ local - fun prep_tac facts = - Method.insert_tac facts - THEN' REPEAT_ALL_NEW - (Tactic.resolve_tac [@{thm impI}, @{thm conjI}, @{thm TrueI}] - ORELSE' Tactic.etac @{thm conjE}) + fun explode_conj (@{term "op &"} $ t $ u) = explode_conj t @ explode_conj u + | explode_conj t = [t] - val drop_assert_at = Conv.concl_conv ~1 (Conv.try_conv (Conv.arg_conv - (Conv.rewr_conv assert_at_def))) + fun splt (ts, @{term "op -->"} $ t $ u) = splt (ts @ explode_conj t, u) + | splt (ts, @{term "op &"} $ t $ u) = splt (ts, t) @ splt (ts, u) + | splt (ts, @{term assert_at} $ _ $ t) = [(ts, t)] + | splt (_, @{term True}) = [] + | splt tp = [tp] +in +fun split t = + splt ([], HOLogic.dest_Trueprop t) + |> map (fn (us, u) => (map HOLogic.mk_Trueprop us, HOLogic.mk_Trueprop u)) +end +val split_tac = REPEAT_ALL_NEW ( + Tactic.resolve_tac [@{thm impI}, @{thm conjI}, @{thm TrueI}] + ORELSE' Tactic.etac @{thm conjE}) + +val drop_assert_at_tac = CONVERSION (Conv.concl_conv ~1 (Conv.try_conv ( + Conv.arg_conv (Conv.rewr_conv assert_at_def)))) + +local fun case_name_of t = (case HOLogic.dest_Trueprop (Logic.strip_imp_concl t) of @{term assert_at} $ Free (n, _) $ _ => n | _ => raise TERM ("case_name_of", [t])) fun boogie_cases ctxt = METHOD_CASES (fn facts => - ALLGOALS (prep_tac facts) #> + ALLGOALS (Method.insert_tac facts THEN' split_tac) #> Seq.maps (fn st => st - |> ALLGOALS (CONVERSION drop_assert_at) + |> ALLGOALS drop_assert_at_tac |> Seq.map (pair (map (rpair [] o case_name_of) (Thm.prems_of st)))) #> Seq.maps (fn (names, st) => CASES