src/HOL/Hoare/hoare_tac.ML
author haftmann
Sun Sep 06 22:14:51 2015 +0200 (2015-09-06)
changeset 61125 4c68426800de
parent 60754 02924903a6fd
child 61424 c3658c18b7bc
permissions -rw-r--r--
prefer "uncurry" as canonical name for case distinction on products in combinatorial view
     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 uncurry}, _) $ 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 uncurry},
    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