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