src/HOL/Hoare/hoare_tac.ML
changeset 28457 25669513fd4c
parent 27330 1af2598b5f7d
child 32149 ef59550a55d3
     1.1 --- a/src/HOL/Hoare/hoare_tac.ML	Thu Oct 02 13:07:33 2008 +0200
     1.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Thu Oct 02 14:22:36 2008 +0200
     1.3 @@ -1,7 +1,6 @@
     1.4  (*  Title:      HOL/Hoare/hoare_tac.ML
     1.5      ID:         $Id$
     1.6      Author:     Leonor Prensa Nieto & Tobias Nipkow
     1.7 -    Copyright   1998 TUM
     1.8  
     1.9  Derivation of the proof rules and, most importantly, the VCG tactic.
    1.10  *)
    1.11 @@ -26,7 +25,7 @@
    1.12  fun mk_vars (Const ("Collect",_) $ T) = abs2list T
    1.13    | mk_vars _ = [];
    1.14  
    1.15 -(** abstraction of body over a tuple formed from a list of free variables. 
    1.16 +(** abstraction of body over a tuple formed from a list of free variables.
    1.17  Types are also built **)
    1.18  fun mk_abstupleC []     body = absfree ("x", unitT, body)
    1.19    | mk_abstupleC (v::w) body = let val (n,T) = dest_Free v
    1.20 @@ -34,12 +33,12 @@
    1.21          else let val z  = mk_abstupleC w body;
    1.22                   val T2 = case z of Abs(_,T,_) => T
    1.23                          | Const (_, Type (_,[_, Type (_,[T,_])])) $ _ => T;
    1.24 -       in Const ("split", (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT) 
    1.25 +       in Const ("split", (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT)
    1.26            $ absfree (n, T, z) end end;
    1.27  
    1.28  (** maps [x1,...,xn] to (x1,...,xn) and types**)
    1.29  fun mk_bodyC []      = HOLogic.unit
    1.30 -  | mk_bodyC (x::xs) = if xs=[] then x 
    1.31 +  | mk_bodyC (x::xs) = if xs=[] then x
    1.32                 else let val (n, T) = dest_Free x ;
    1.33                          val z = mk_bodyC xs;
    1.34                          val T2 = case z of Free(_, T) => T
    1.35 @@ -47,33 +46,35 @@
    1.36                                              ("fun", [_, T])])) $ _ $ _ => T;
    1.37                   in Const ("Pair", [T, T2] ---> mk_prodT (T, T2)) $ x $ z end;
    1.38  
    1.39 -(** maps a goal of the form:
    1.40 -        1. [| P |] ==> VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]**) 
    1.41 -fun get_vars thm = let  val c = Logic.unprotect (concl_of (thm));
    1.42 -                        val d = Logic.strip_assums_concl c;
    1.43 -                        val Const _ $ pre $ _ $ _ = dest_Trueprop d;
    1.44 -      in mk_vars pre end;
    1.45 +(** maps a subgoal of the form:
    1.46 +        VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]**)
    1.47 +fun get_vars c =
    1.48 +  let
    1.49 +    val d = Logic.strip_assums_concl c;
    1.50 +    val Const _ $ pre $ _ $ _ = dest_Trueprop d;
    1.51 +  in mk_vars pre end;
    1.52  
    1.53 -
    1.54 -(** Makes Collect with type **)
    1.55 -fun mk_CollectC trm = let val T as Type ("fun",[t,_]) = fastype_of trm 
    1.56 -                      in Collect_const t $ trm end;
    1.57 +fun mk_CollectC trm =
    1.58 +  let val T as Type ("fun",[t,_]) = fastype_of trm
    1.59 +  in Collect_const t $ trm end;
    1.60  
    1.61  fun inclt ty = Const (@{const_name HOL.less_eq}, [ty,ty] ---> boolT);
    1.62  
    1.63 -(** Makes "Mset <= t" **)
    1.64 -fun Mset_incl t = let val MsetT = fastype_of t 
    1.65 -                 in mk_Trueprop ((inclt MsetT) $ Free ("Mset", MsetT) $ t) end;
    1.66  
    1.67 +fun Mset ctxt prop =
    1.68 +  let
    1.69 +    val [(Mset, _), (P, _)] = Variable.variant_frees ctxt [] [("Mset", ()), ("P", ())];
    1.70  
    1.71 -fun Mset thm = let val vars = get_vars(thm);
    1.72 -                   val varsT = fastype_of (mk_bodyC vars);
    1.73 -                   val big_Collect = mk_CollectC (mk_abstupleC vars 
    1.74 -                         (Free ("P",varsT --> boolT) $ mk_bodyC vars));
    1.75 -                   val small_Collect = mk_CollectC (Abs("x",varsT,
    1.76 -                           Free ("P",varsT --> boolT) $ Bound 0));
    1.77 -                   val impl = Logic.mk_implies (Mset_incl big_Collect, Mset_incl small_Collect);
    1.78 -   in Goal.prove (ProofContext.init (Thm.theory_of_thm thm)) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
    1.79 +    val vars = get_vars prop;
    1.80 +    val varsT = fastype_of (mk_bodyC vars);
    1.81 +    val big_Collect = mk_CollectC (mk_abstupleC vars (Free (P, varsT --> boolT) $ mk_bodyC vars));
    1.82 +    val small_Collect = mk_CollectC (Abs ("x", varsT, Free (P, varsT --> boolT) $ Bound 0));
    1.83 +
    1.84 +    val MsetT = fastype_of big_Collect;
    1.85 +    fun Mset_incl t = mk_Trueprop (inclt MsetT $ Free (Mset, MsetT) $ t);
    1.86 +    val impl = Logic.mk_implies (Mset_incl big_Collect, Mset_incl small_Collect);
    1.87 +    val th = Goal.prove ctxt [Mset, P] [] impl (fn _ => blast_tac (local_claset_of ctxt) 1);
    1.88 + in (vars, th) end;
    1.89  
    1.90  end;
    1.91  
    1.92 @@ -93,7 +94,7 @@
    1.93  val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [split_conv]));
    1.94  
    1.95  (*****************************************************************************)
    1.96 -(** set2pred transforms sets inclusion into predicates implication,         **)
    1.97 +(** set2pred_tac transforms sets inclusion into predicates implication,     **)
    1.98  (** maintaining the original variable names.                                **)
    1.99  (** Ex. "{x. x=0} <= {x. x <= 1}" -set2pred-> "x=0 --> x <= 1"              **)
   1.100  (** Subgoals containing intersections (A Int B) or complement sets (-A)     **)
   1.101 @@ -104,16 +105,14 @@
   1.102  (** simplification done by (split_all_tac)                                  **)
   1.103  (*****************************************************************************)
   1.104  
   1.105 -fun set2pred i thm =
   1.106 -  let val var_names = map (fst o dest_Free) (get_vars thm) in
   1.107 -    ((before_set2pred_simp_tac i) THEN_MAYBE
   1.108 -     (EVERY [rtac subsetI i, 
   1.109 -             rtac CollectI i,
   1.110 -             dtac CollectD i,
   1.111 -             (TRY(split_all_tac i)) THEN_MAYBE
   1.112 -             ((rename_tac var_names i) THEN
   1.113 -              (full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)) ])) thm
   1.114 -  end;
   1.115 +fun set2pred_tac var_names = SUBGOAL (fn (goal, i) =>
   1.116 +  before_set2pred_simp_tac i THEN_MAYBE
   1.117 +  EVERY [
   1.118 +    rtac subsetI i,
   1.119 +    rtac CollectI i,
   1.120 +    dtac CollectD i,
   1.121 +    TRY (split_all_tac i) THEN_MAYBE
   1.122 +     (rename_tac var_names i THEN full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)]);
   1.123  
   1.124  (*****************************************************************************)
   1.125  (** BasicSimpTac is called to simplify all verification conditions. It does **)
   1.126 @@ -123,37 +122,46 @@
   1.127  (** the tactic chosen by the user, which may solve the subgoal completely.  **)
   1.128  (*****************************************************************************)
   1.129  
   1.130 -fun MaxSimpTac tac = FIRST'[rtac subset_refl, set2pred THEN_MAYBE' tac];
   1.131 -
   1.132 -fun BasicSimpTac tac =
   1.133 -  simp_tac
   1.134 -    (HOL_basic_ss addsimps [mem_Collect_eq,split_conv] addsimprocs [record_simproc])
   1.135 -  THEN_MAYBE' MaxSimpTac tac;
   1.136 -
   1.137 -(** HoareRuleTac **)
   1.138 +fun MaxSimpTac var_names tac = FIRST'[rtac subset_refl, set2pred_tac var_names THEN_MAYBE' tac];
   1.139  
   1.140 -fun WlpTac Mlem tac i =
   1.141 -  rtac @{thm SeqRule} i THEN  HoareRuleTac Mlem tac false (i+1)
   1.142 -and HoareRuleTac Mlem tac pre_cond i st = st |>
   1.143 -        (*abstraction over st prevents looping*)
   1.144 -    ( (WlpTac Mlem tac i THEN HoareRuleTac Mlem tac pre_cond i)
   1.145 -      ORELSE
   1.146 -      (FIRST[rtac @{thm SkipRule} i,
   1.147 -             EVERY[rtac @{thm BasicRule} i,
   1.148 -                   rtac Mlem i,
   1.149 -                   split_simp_tac i],
   1.150 -             EVERY[rtac @{thm CondRule} i,
   1.151 -                   HoareRuleTac Mlem tac false (i+2),
   1.152 -                   HoareRuleTac Mlem tac false (i+1)],
   1.153 -             EVERY[rtac @{thm WhileRule} i,
   1.154 -                   BasicSimpTac tac (i+2),
   1.155 -                   HoareRuleTac Mlem tac true (i+1)] ] 
   1.156 -       THEN (if pre_cond then (BasicSimpTac tac i) else (rtac subset_refl i)) ));
   1.157 +fun BasicSimpTac var_names tac =
   1.158 +  simp_tac
   1.159 +    (HOL_basic_ss addsimps [mem_Collect_eq, split_conv] addsimprocs [record_simproc])
   1.160 +  THEN_MAYBE' MaxSimpTac var_names tac;
   1.161  
   1.162  
   1.163 -(** tac:(int -> tactic) is the tactic the user chooses to solve or simplify **)
   1.164 -(** the final verification conditions                                       **)
   1.165 - 
   1.166 -fun hoare_tac tac i thm =
   1.167 -  let val Mlem = Mset(thm)
   1.168 -  in SELECT_GOAL(EVERY[HoareRuleTac Mlem tac true 1]) i thm end;
   1.169 +(** hoare_rule_tac **)
   1.170 +
   1.171 +fun hoare_rule_tac (vars, Mlem) tac =
   1.172 +  let
   1.173 +    val var_names = map (fst o dest_Free) vars;
   1.174 +    fun wlp_tac i =
   1.175 +      rtac @{thm SeqRule} i THEN rule_tac false (i + 1)
   1.176 +    and rule_tac pre_cond i st = st |> (*abstraction over st prevents looping*)
   1.177 +      ((wlp_tac i THEN rule_tac pre_cond i)
   1.178 +        ORELSE
   1.179 +        (FIRST [
   1.180 +          rtac @{thm SkipRule} i,
   1.181 +          rtac @{thm AbortRule} i,
   1.182 +          EVERY [
   1.183 +            rtac @{thm BasicRule} i,
   1.184 +            rtac Mlem i,
   1.185 +            split_simp_tac i],
   1.186 +          EVERY [
   1.187 +            rtac @{thm CondRule} i,
   1.188 +            rule_tac false (i + 2),
   1.189 +            rule_tac false (i + 1)],
   1.190 +          EVERY [
   1.191 +            rtac @{thm WhileRule} i,
   1.192 +            BasicSimpTac var_names tac (i + 2),
   1.193 +            rule_tac true (i + 1)]]
   1.194 +         THEN (if pre_cond then BasicSimpTac var_names tac i else rtac subset_refl i)));
   1.195 +  in rule_tac end;
   1.196 +
   1.197 +
   1.198 +(** tac is the tactic the user chooses to solve or simplify **)
   1.199 +(** the final verification conditions                       **)
   1.200 +
   1.201 +fun hoare_tac ctxt (tac: int -> tactic) = SUBGOAL (fn (goal, i) =>
   1.202 +  SELECT_GOAL (hoare_rule_tac (Mset ctxt goal) tac true 1) i);
   1.203 +