src/HOL/Boogie/Tools/boogie_tactics.ML
author boehmes
Sun Aug 08 04:28:51 2010 +0200 (2010-08-08)
changeset 38245 27da291ee202
parent 36936 c52d1c130898
child 38786 e46e7a9cb622
permissions -rw-r--r--
added scanning of if-then-else expressions
     1 (*  Title:      HOL/Boogie/Tools/boogie_tactics.ML
     2     Author:     Sascha Boehme, TU Muenchen
     3 
     4 Boogie tactics and Boogie methods.
     5 *)
     6 
     7 signature BOOGIE_TACTICS =
     8 sig
     9   val unfold_labels_tac: Proof.context -> int -> tactic
    10   val boogie_tac: Proof.context -> thm list -> int -> tactic
    11   val boogie_all_tac: Proof.context -> thm list -> tactic
    12   val split: term -> (term list * term) list
    13   val split_tac: int -> tactic
    14   val drop_assert_at_tac: int -> tactic
    15   val setup: theory -> theory
    16 end
    17 
    18 structure Boogie_Tactics: BOOGIE_TACTICS =
    19 struct
    20 
    21 fun as_meta_eq eq = eq RS @{thm eq_reflection}
    22 
    23 val assert_at_def = as_meta_eq @{thm assert_at_def}
    24 val block_at_def = as_meta_eq @{thm block_at_def}
    25 val label_eqs = [assert_at_def, block_at_def]
    26 
    27 fun unfold_labels_tac ctxt =
    28   let val unfold = Conv.rewrs_conv label_eqs
    29   in CONVERSION (Conv.top_sweep_conv (K unfold) ctxt) end
    30 
    31 fun boogie_tac ctxt rules =
    32   unfold_labels_tac ctxt
    33   THEN' SMT_Solver.smt_tac ctxt (Boogie_Axioms.get ctxt @ rules)
    34 
    35 fun boogie_all_tac ctxt rules =
    36   PARALLEL_GOALS (HEADGOAL (boogie_tac ctxt rules))
    37 
    38 fun boogie_method all =
    39   Scan.optional Attrib.thms [] >> (fn thms => fn ctxt => METHOD (fn facts =>
    40     let val tac = if all then boogie_all_tac else HEADGOAL oo boogie_tac
    41     in tac ctxt (thms @ facts) end))
    42 
    43 val setup_boogie = Method.setup @{binding boogie} (boogie_method false)
    44   ("Applies an SMT solver to the current goal " ^
    45    "using the current set of Boogie background axioms")
    46 
    47 val setup_boogie_all = Method.setup @{binding boogie_all} (boogie_method true)
    48   ("Applies an SMT solver to all goals " ^
    49    "using the current set of Boogie background axioms")
    50 
    51 
    52 local
    53   fun explode_conj (@{term "op &"} $ t $ u) = explode_conj t @ explode_conj u
    54     | explode_conj t = [t] 
    55 
    56   fun splt (ts, @{term "op -->"} $ t $ u) = splt (ts @ explode_conj t, u)
    57     | splt (ts, @{term "op &"} $ t $ u) = splt (ts, t) @ splt (ts, u)
    58     | splt (ts, @{term assert_at} $ _ $ t) = [(ts, t)]
    59     | splt (_, @{term True}) = []
    60     | splt tp = [tp]
    61 in
    62 fun split t =
    63   splt ([], HOLogic.dest_Trueprop t)
    64   |> map (fn (us, u) => (map HOLogic.mk_Trueprop us, HOLogic.mk_Trueprop u))
    65 end
    66 
    67 val split_tac = REPEAT_ALL_NEW (
    68   Tactic.resolve_tac [@{thm impI}, @{thm conjI}, @{thm TrueI}]
    69   ORELSE' Tactic.etac @{thm conjE})
    70 
    71 val drop_assert_at_tac = CONVERSION (Conv.concl_conv ~1 (Conv.try_conv (
    72   Conv.arg_conv (Conv.rewr_conv assert_at_def))))
    73 
    74 local
    75   fun case_name_of t =
    76     (case HOLogic.dest_Trueprop (Logic.strip_imp_concl t) of
    77       @{term assert_at} $ Free (n, _) $ _ => n
    78     | _ => raise TERM ("case_name_of", [t]))
    79 
    80   fun boogie_cases ctxt = METHOD_CASES (fn facts =>
    81     ALLGOALS (Method.insert_tac facts THEN' split_tac) #>
    82     Seq.maps (fn st =>
    83       st
    84       |> ALLGOALS drop_assert_at_tac
    85       |> Seq.map (pair (map (rpair [] o case_name_of) (Thm.prems_of st)))) #>
    86     Seq.maps (fn (names, st) =>
    87       CASES
    88         (Rule_Cases.make_common
    89           (ProofContext.theory_of ctxt,
    90            Thm.prop_of (Rule_Cases.internalize_params st)) names)
    91         Tactical.all_tac st))
    92 in
    93 val setup_boogie_cases = Method.setup @{binding boogie_cases}
    94   (Scan.succeed boogie_cases)
    95   "Prepares a set of Boogie assertions for case-based proofs"
    96 end
    97 
    98 
    99 val setup =
   100   setup_boogie #>
   101   setup_boogie_all #>
   102   setup_boogie_cases
   103 
   104 end