src/HOL/Hoare/hoare_tac.ML
author wenzelm
Fri Feb 21 20:47:48 2014 +0100 (2014-02-21)
changeset 55661 ec14796cd140
parent 55660 f0f895716a8b
child 60754 02924903a6fd
permissions -rw-r--r--
tuned whitespace;
tuned names;
wenzelm@24475
     1
(*  Title:      HOL/Hoare/hoare_tac.ML
wenzelm@24475
     2
    Author:     Leonor Prensa Nieto & Tobias Nipkow
wenzelm@24475
     3
wenzelm@24475
     4
Derivation of the proof rules and, most importantly, the VCG tactic.
wenzelm@24475
     5
*)
wenzelm@24475
     6
wenzelm@55660
     7
signature HOARE =
wenzelm@55660
     8
sig
wenzelm@55661
     9
  val hoare_rule_tac: Proof.context -> term list * thm -> (int -> tactic) -> bool ->
wenzelm@55661
    10
    int -> tactic
wenzelm@55660
    11
  val hoare_tac: Proof.context -> (int -> tactic) -> int -> tactic
wenzelm@55660
    12
end;
wenzelm@55660
    13
wenzelm@55660
    14
structure Hoare: HOARE =
wenzelm@55660
    15
struct
wenzelm@41449
    16
wenzelm@24475
    17
(*** The tactics ***)
wenzelm@24475
    18
wenzelm@24475
    19
(*****************************************************************************)
wenzelm@24475
    20
(** The function Mset makes the theorem                                     **)
wenzelm@24475
    21
(** "?Mset <= {(x1,...,xn). ?P (x1,...,xn)} ==> ?Mset <= {s. ?P s}",        **)
wenzelm@24475
    22
(** where (x1,...,xn) are the variables of the particular program we are    **)
wenzelm@24475
    23
(** working on at the moment of the call                                    **)
wenzelm@24475
    24
(*****************************************************************************)
wenzelm@24475
    25
wenzelm@41449
    26
local
wenzelm@24475
    27
wenzelm@24475
    28
(** maps (%x1 ... xn. t) to [x1,...,xn] **)
blanchet@55414
    29
fun abs2list (Const (@{const_name case_prod}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
wenzelm@55659
    30
  | abs2list (Abs (x, T, _)) = [Free (x, T)]
wenzelm@24475
    31
  | abs2list _ = [];
wenzelm@24475
    32
wenzelm@24475
    33
(** maps {(x1,...,xn). t} to [x1,...,xn] **)
haftmann@37677
    34
fun mk_vars (Const (@{const_name Collect},_) $ T) = abs2list T
wenzelm@24475
    35
  | mk_vars _ = [];
wenzelm@24475
    36
wenzelm@28457
    37
(** abstraction of body over a tuple formed from a list of free variables.
wenzelm@24475
    38
Types are also built **)
wenzelm@44241
    39
fun mk_abstupleC [] body = absfree ("x", HOLogic.unitT) body
wenzelm@44241
    40
  | mk_abstupleC [v] body = absfree (dest_Free v) body
wenzelm@44241
    41
  | mk_abstupleC (v :: w) body =
wenzelm@44241
    42
      let
wenzelm@44241
    43
        val (x, T) = dest_Free v;
wenzelm@44241
    44
        val z = mk_abstupleC w body;
wenzelm@44241
    45
        val T2 =
wenzelm@44241
    46
          (case z of
wenzelm@44241
    47
            Abs (_, T, _) => T
wenzelm@44241
    48
          | Const (_, Type (_, [_, Type (_, [T, _])])) $ _ => T);
wenzelm@44241
    49
      in
blanchet@55414
    50
        Const (@{const_name case_prod},
wenzelm@44241
    51
            (T --> T2 --> HOLogic.boolT) --> HOLogic.mk_prodT (T, T2) --> HOLogic.boolT) $
wenzelm@44241
    52
          absfree (x, T) z
wenzelm@44241
    53
      end;
wenzelm@24475
    54
wenzelm@24475
    55
(** maps [x1,...,xn] to (x1,...,xn) and types**)
wenzelm@55661
    56
fun mk_bodyC [] = HOLogic.unit
wenzelm@55661
    57
  | mk_bodyC [x] = x
wenzelm@55661
    58
  | mk_bodyC (x :: xs) =
wenzelm@55661
    59
      let
wenzelm@55661
    60
        val (_, T) = dest_Free x;
wenzelm@55661
    61
        val z = mk_bodyC xs;
wenzelm@55661
    62
        val T2 =
wenzelm@55661
    63
          (case z of
wenzelm@55661
    64
            Free (_, T) => T
wenzelm@55661
    65
          | Const (@{const_name Pair}, Type ("fun", [_, Type ("fun", [_, T])])) $ _ $ _ => T);
wenzelm@55661
    66
     in Const (@{const_name Pair}, [T, T2] ---> HOLogic.mk_prodT (T, T2)) $ x $ z end;
wenzelm@24475
    67
wenzelm@28457
    68
(** maps a subgoal of the form:
wenzelm@55661
    69
    VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]
wenzelm@55661
    70
**)
wenzelm@28457
    71
fun get_vars c =
wenzelm@28457
    72
  let
wenzelm@28457
    73
    val d = Logic.strip_assums_concl c;
wenzelm@41449
    74
    val Const _ $ pre $ _ $ _ = HOLogic.dest_Trueprop d;
wenzelm@28457
    75
  in mk_vars pre end;
wenzelm@24475
    76
wenzelm@55661
    77
fun mk_CollectC tm =
wenzelm@55661
    78
  let val T as Type ("fun",[t,_]) = fastype_of tm;
wenzelm@55661
    79
  in HOLogic.Collect_const t $ tm end;
wenzelm@24475
    80
wenzelm@41449
    81
fun inclt ty = Const (@{const_name Orderings.less_eq}, [ty,ty] ---> HOLogic.boolT);
wenzelm@24475
    82
wenzelm@41449
    83
in
wenzelm@24475
    84
wenzelm@28457
    85
fun Mset ctxt prop =
wenzelm@28457
    86
  let
wenzelm@28457
    87
    val [(Mset, _), (P, _)] = Variable.variant_frees ctxt [] [("Mset", ()), ("P", ())];
wenzelm@24475
    88
wenzelm@28457
    89
    val vars = get_vars prop;
wenzelm@28457
    90
    val varsT = fastype_of (mk_bodyC vars);
wenzelm@55661
    91
    val big_Collect =
wenzelm@55661
    92
      mk_CollectC (mk_abstupleC vars (Free (P, varsT --> HOLogic.boolT) $ mk_bodyC vars));
wenzelm@55661
    93
    val small_Collect =
wenzelm@55661
    94
      mk_CollectC (Abs ("x", varsT, Free (P, varsT --> HOLogic.boolT) $ Bound 0));
wenzelm@28457
    95
wenzelm@28457
    96
    val MsetT = fastype_of big_Collect;
wenzelm@41449
    97
    fun Mset_incl t = HOLogic.mk_Trueprop (inclt MsetT $ Free (Mset, MsetT) $ t);
wenzelm@28457
    98
    val impl = Logic.mk_implies (Mset_incl big_Collect, Mset_incl small_Collect);
wenzelm@42793
    99
    val th = Goal.prove ctxt [Mset, P] [] impl (fn _ => blast_tac ctxt 1);
wenzelm@28457
   100
 in (vars, th) end;
wenzelm@24475
   101
wenzelm@24475
   102
end;
wenzelm@24475
   103
wenzelm@24475
   104
wenzelm@24475
   105
(*****************************************************************************)
wenzelm@24475
   106
(** Simplifying:                                                            **)
wenzelm@24475
   107
(** Some useful lemmata, lists and simplification tactics to control which  **)
wenzelm@24475
   108
(** theorems are used to simplify at each moment, so that the original      **)
wenzelm@24475
   109
(** input does not suffer any unexpected transformation                     **)
wenzelm@24475
   110
(*****************************************************************************)
wenzelm@24475
   111
wenzelm@24475
   112
(**Simp_tacs**)
wenzelm@24475
   113
wenzelm@51717
   114
fun before_set2pred_simp_tac ctxt =
wenzelm@51717
   115
  simp_tac (put_simpset HOL_basic_ss ctxt addsimps [Collect_conj_eq RS sym, @{thm Compl_Collect}]);
wenzelm@24475
   116
wenzelm@51717
   117
fun split_simp_tac ctxt =
wenzelm@51717
   118
  simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]);
wenzelm@24475
   119
wenzelm@24475
   120
(*****************************************************************************)
wenzelm@55661
   121
(** set_to_pred_tac transforms sets inclusion into predicates implication,  **)
wenzelm@24475
   122
(** maintaining the original variable names.                                **)
wenzelm@24475
   123
(** Ex. "{x. x=0} <= {x. x <= 1}" -set2pred-> "x=0 --> x <= 1"              **)
wenzelm@24475
   124
(** Subgoals containing intersections (A Int B) or complement sets (-A)     **)
wenzelm@24475
   125
(** are first simplified by "before_set2pred_simp_tac", that returns only   **)
wenzelm@24475
   126
(** subgoals of the form "{x. P x} <= {x. Q x}", which are easily           **)
wenzelm@24475
   127
(** transformed.                                                            **)
wenzelm@24475
   128
(** This transformation may solve very easy subgoals due to a ligth         **)
wenzelm@24475
   129
(** simplification done by (split_all_tac)                                  **)
wenzelm@24475
   130
(*****************************************************************************)
wenzelm@24475
   131
wenzelm@55661
   132
fun set_to_pred_tac ctxt var_names = SUBGOAL (fn (_, i) =>
wenzelm@51717
   133
  before_set2pred_simp_tac ctxt i THEN_MAYBE
wenzelm@28457
   134
  EVERY [
wenzelm@28457
   135
    rtac subsetI i,
wenzelm@28457
   136
    rtac CollectI i,
wenzelm@28457
   137
    dtac CollectD i,
wenzelm@51717
   138
    TRY (split_all_tac ctxt i) THEN_MAYBE
wenzelm@51717
   139
     (rename_tac var_names i THEN
wenzelm@51717
   140
      full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]) i)]);
wenzelm@24475
   141
wenzelm@55661
   142
(*******************************************************************************)
wenzelm@55661
   143
(** basic_simp_tac is called to simplify all verification conditions. It does **)
wenzelm@55661
   144
(** a light simplification by applying "mem_Collect_eq", then it calls        **)
wenzelm@55661
   145
(** max_simp_tac, which solves subgoals of the form "A <= A",                 **)
wenzelm@55661
   146
(** and transforms any other into predicates, applying then                   **)
wenzelm@55661
   147
(** the tactic chosen by the user, which may solve the subgoal completely.    **)
wenzelm@55661
   148
(*******************************************************************************)
wenzelm@24475
   149
wenzelm@55661
   150
fun max_simp_tac ctxt var_names tac =
wenzelm@55661
   151
  FIRST' [rtac subset_refl, set_to_pred_tac ctxt var_names THEN_MAYBE' tac];
wenzelm@24475
   152
wenzelm@55661
   153
fun basic_simp_tac ctxt var_names tac =
wenzelm@28457
   154
  simp_tac
wenzelm@51717
   155
    (put_simpset HOL_basic_ss ctxt
wenzelm@51717
   156
      addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [Record.simproc])
wenzelm@55661
   157
  THEN_MAYBE' max_simp_tac ctxt var_names tac;
wenzelm@24475
   158
wenzelm@24475
   159
wenzelm@28457
   160
(** hoare_rule_tac **)
wenzelm@28457
   161
wenzelm@51717
   162
fun hoare_rule_tac ctxt (vars, Mlem) tac =
wenzelm@28457
   163
  let
wenzelm@28457
   164
    val var_names = map (fst o dest_Free) vars;
wenzelm@28457
   165
    fun wlp_tac i =
wenzelm@28457
   166
      rtac @{thm SeqRule} i THEN rule_tac false (i + 1)
wenzelm@28457
   167
    and rule_tac pre_cond i st = st |> (*abstraction over st prevents looping*)
wenzelm@28457
   168
      ((wlp_tac i THEN rule_tac pre_cond i)
wenzelm@28457
   169
        ORELSE
wenzelm@28457
   170
        (FIRST [
wenzelm@28457
   171
          rtac @{thm SkipRule} i,
wenzelm@28457
   172
          rtac @{thm AbortRule} i,
wenzelm@28457
   173
          EVERY [
wenzelm@28457
   174
            rtac @{thm BasicRule} i,
wenzelm@28457
   175
            rtac Mlem i,
wenzelm@51717
   176
            split_simp_tac ctxt i],
wenzelm@28457
   177
          EVERY [
wenzelm@28457
   178
            rtac @{thm CondRule} i,
wenzelm@28457
   179
            rule_tac false (i + 2),
wenzelm@28457
   180
            rule_tac false (i + 1)],
wenzelm@28457
   181
          EVERY [
wenzelm@28457
   182
            rtac @{thm WhileRule} i,
wenzelm@55661
   183
            basic_simp_tac ctxt var_names tac (i + 2),
wenzelm@28457
   184
            rule_tac true (i + 1)]]
wenzelm@55661
   185
         THEN (if pre_cond then basic_simp_tac ctxt var_names tac i else rtac subset_refl i)));
wenzelm@28457
   186
  in rule_tac end;
wenzelm@28457
   187
wenzelm@28457
   188
wenzelm@28457
   189
(** tac is the tactic the user chooses to solve or simplify **)
wenzelm@28457
   190
(** the final verification conditions                       **)
wenzelm@28457
   191
wenzelm@55659
   192
fun hoare_tac ctxt tac = SUBGOAL (fn (goal, i) =>
wenzelm@51717
   193
  SELECT_GOAL (hoare_rule_tac ctxt (Mset ctxt goal) tac true 1) i);
wenzelm@28457
   194
wenzelm@55660
   195
end;
wenzelm@55660
   196