src/HOL/Boogie/Tools/boogie_tactics.ML

merged verification condition structure and term representation in one datatype,
extended the set of operations on verification conditions (retrieve more information, advanced splitting of paths),
simplified discharging of verification conditions (due to improved datatype),
added variantions of commands (extract different parts of verification conditions, scan until first "hard" assertion)

(*  Title:      HOL/Boogie/Tools/boogie_tactics.ML
    Author:     Sascha Boehme, TU Muenchen

Boogie tactics and Boogie methods.
*)

signature BOOGIE_TACTICS =
sig
  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 setup: theory -> theory
end

structure Boogie_Tactics: BOOGIE_TACTICS =
struct

fun as_meta_eq eq = eq RS @{thm eq_reflection}

val assert_at_def = as_meta_eq @{thm assert_at_def}
val block_at_def = as_meta_eq @{thm block_at_def}
val label_eqs = [assert_at_def, block_at_def]

fun unfold_labels_tac ctxt =
  let val unfold = More_Conv.rewrs_conv label_eqs
  in CONVERSION (More_Conv.top_sweep_conv (K unfold) ctxt) end

fun boogie_tac ctxt rules =
  unfold_labels_tac ctxt
  THEN' SMT_Solver.smt_tac ctxt (Boogie_Axioms.get ctxt @ rules)

fun boogie_all_tac ctxt rules =
  PARALLEL_GOALS (HEADGOAL (boogie_tac ctxt rules))

fun boogie_method all =
  Scan.optional Attrib.thms [] >> (fn thms => fn ctxt => METHOD (fn facts =>
    let val tac = if all then boogie_all_tac else HEADGOAL oo boogie_tac
    in tac ctxt (thms @ facts) end))

val setup_boogie = Method.setup @{binding boogie} (boogie_method false)
  ("Applies an SMT solver to the current goal " ^
   "using the current set of Boogie background axioms")

val setup_boogie_all = Method.setup @{binding boogie_all} (boogie_method true)
  ("Applies an SMT solver to all goals " ^
   "using the current set of Boogie background axioms")


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})

  val drop_assert_at = Conv.concl_conv ~1 (Conv.try_conv (Conv.arg_conv
    (Conv.rewr_conv assert_at_def)))

  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) #>
    Seq.maps (fn st =>
      st
      |> ALLGOALS (CONVERSION drop_assert_at)
      |> Seq.map (pair (map (rpair [] o case_name_of) (Thm.prems_of st)))) #>
    Seq.maps (fn (names, st) =>
      CASES
        (Rule_Cases.make_common false
          (ProofContext.theory_of ctxt, Thm.prop_of st) names)
        Tactical.all_tac st))
in
val setup_boogie_cases = Method.setup @{binding boogie_cases}
  (Scan.succeed boogie_cases)
  "Prepares a set of Boogie assertions for case-based proofs"
end


val setup =
  setup_boogie #>
  setup_boogie_all #>
  setup_boogie_cases

end