tuned whitespace;
authorwenzelm
Fri Feb 21 20:47:48 2014 +0100 (2014-02-21)
changeset 55661ec14796cd140
parent 55660 f0f895716a8b
child 55662 b45af39fcdae
tuned whitespace;
tuned names;
src/HOL/Hoare/hoare_tac.ML
     1.1 --- a/src/HOL/Hoare/hoare_tac.ML	Fri Feb 21 20:37:13 2014 +0100
     1.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Fri Feb 21 20:47:48 2014 +0100
     1.3 @@ -6,7 +6,8 @@
     1.4  
     1.5  signature HOARE =
     1.6  sig
     1.7 -  val hoare_rule_tac: Proof.context -> term list * thm -> (int -> tactic) -> bool -> int -> tactic
     1.8 +  val hoare_rule_tac: Proof.context -> term list * thm -> (int -> tactic) -> bool ->
     1.9 +    int -> tactic
    1.10    val hoare_tac: Proof.context -> (int -> tactic) -> int -> tactic
    1.11  end;
    1.12  
    1.13 @@ -52,26 +53,30 @@
    1.14        end;
    1.15  
    1.16  (** maps [x1,...,xn] to (x1,...,xn) and types**)
    1.17 -fun mk_bodyC []      = HOLogic.unit
    1.18 -  | mk_bodyC (x::xs) = if xs=[] then x
    1.19 -               else let val (n, T) = dest_Free x ;
    1.20 -                        val z = mk_bodyC xs;
    1.21 -                        val T2 = case z of Free(_, T) => T
    1.22 -                                         | Const (@{const_name Pair}, Type ("fun", [_, Type
    1.23 -                                            ("fun", [_, T])])) $ _ $ _ => T;
    1.24 -                 in Const (@{const_name Pair}, [T, T2] ---> HOLogic.mk_prodT (T, T2)) $ x $ z end;
    1.25 +fun mk_bodyC [] = HOLogic.unit
    1.26 +  | mk_bodyC [x] = x
    1.27 +  | mk_bodyC (x :: xs) =
    1.28 +      let
    1.29 +        val (_, T) = dest_Free x;
    1.30 +        val z = mk_bodyC xs;
    1.31 +        val T2 =
    1.32 +          (case z of
    1.33 +            Free (_, T) => T
    1.34 +          | Const (@{const_name Pair}, Type ("fun", [_, Type ("fun", [_, T])])) $ _ $ _ => T);
    1.35 +     in Const (@{const_name Pair}, [T, T2] ---> HOLogic.mk_prodT (T, T2)) $ x $ z end;
    1.36  
    1.37  (** maps a subgoal of the form:
    1.38 -        VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]**)
    1.39 +    VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]
    1.40 +**)
    1.41  fun get_vars c =
    1.42    let
    1.43      val d = Logic.strip_assums_concl c;
    1.44      val Const _ $ pre $ _ $ _ = HOLogic.dest_Trueprop d;
    1.45    in mk_vars pre end;
    1.46  
    1.47 -fun mk_CollectC trm =
    1.48 -  let val T as Type ("fun",[t,_]) = fastype_of trm
    1.49 -  in HOLogic.Collect_const t $ trm end;
    1.50 +fun mk_CollectC tm =
    1.51 +  let val T as Type ("fun",[t,_]) = fastype_of tm;
    1.52 +  in HOLogic.Collect_const t $ tm end;
    1.53  
    1.54  fun inclt ty = Const (@{const_name Orderings.less_eq}, [ty,ty] ---> HOLogic.boolT);
    1.55  
    1.56 @@ -83,8 +88,10 @@
    1.57  
    1.58      val vars = get_vars prop;
    1.59      val varsT = fastype_of (mk_bodyC vars);
    1.60 -    val big_Collect = mk_CollectC (mk_abstupleC vars (Free (P, varsT --> HOLogic.boolT) $ mk_bodyC vars));
    1.61 -    val small_Collect = mk_CollectC (Abs ("x", varsT, Free (P, varsT --> HOLogic.boolT) $ Bound 0));
    1.62 +    val big_Collect =
    1.63 +      mk_CollectC (mk_abstupleC vars (Free (P, varsT --> HOLogic.boolT) $ mk_bodyC vars));
    1.64 +    val small_Collect =
    1.65 +      mk_CollectC (Abs ("x", varsT, Free (P, varsT --> HOLogic.boolT) $ Bound 0));
    1.66  
    1.67      val MsetT = fastype_of big_Collect;
    1.68      fun Mset_incl t = HOLogic.mk_Trueprop (inclt MsetT $ Free (Mset, MsetT) $ t);
    1.69 @@ -111,7 +118,7 @@
    1.70    simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]);
    1.71  
    1.72  (*****************************************************************************)
    1.73 -(** set2pred_tac transforms sets inclusion into predicates implication,     **)
    1.74 +(** set_to_pred_tac transforms sets inclusion into predicates implication,  **)
    1.75  (** maintaining the original variable names.                                **)
    1.76  (** Ex. "{x. x=0} <= {x. x <= 1}" -set2pred-> "x=0 --> x <= 1"              **)
    1.77  (** Subgoals containing intersections (A Int B) or complement sets (-A)     **)
    1.78 @@ -122,7 +129,7 @@
    1.79  (** simplification done by (split_all_tac)                                  **)
    1.80  (*****************************************************************************)
    1.81  
    1.82 -fun set2pred_tac ctxt var_names = SUBGOAL (fn (_, i) =>
    1.83 +fun set_to_pred_tac ctxt var_names = SUBGOAL (fn (_, i) =>
    1.84    before_set2pred_simp_tac ctxt i THEN_MAYBE
    1.85    EVERY [
    1.86      rtac subsetI i,
    1.87 @@ -132,22 +139,22 @@
    1.88       (rename_tac var_names i THEN
    1.89        full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]) i)]);
    1.90  
    1.91 -(*****************************************************************************)
    1.92 -(** BasicSimpTac is called to simplify all verification conditions. It does **)
    1.93 -(** a light simplification by applying "mem_Collect_eq", then it calls      **)
    1.94 -(** MaxSimpTac, which solves subgoals of the form "A <= A",                 **)
    1.95 -(** and transforms any other into predicates, applying then                 **)
    1.96 -(** the tactic chosen by the user, which may solve the subgoal completely.  **)
    1.97 -(*****************************************************************************)
    1.98 +(*******************************************************************************)
    1.99 +(** basic_simp_tac is called to simplify all verification conditions. It does **)
   1.100 +(** a light simplification by applying "mem_Collect_eq", then it calls        **)
   1.101 +(** max_simp_tac, which solves subgoals of the form "A <= A",                 **)
   1.102 +(** and transforms any other into predicates, applying then                   **)
   1.103 +(** the tactic chosen by the user, which may solve the subgoal completely.    **)
   1.104 +(*******************************************************************************)
   1.105  
   1.106 -fun MaxSimpTac ctxt var_names tac =
   1.107 -  FIRST'[rtac subset_refl, set2pred_tac ctxt var_names THEN_MAYBE' tac];
   1.108 +fun max_simp_tac ctxt var_names tac =
   1.109 +  FIRST' [rtac subset_refl, set_to_pred_tac ctxt var_names THEN_MAYBE' tac];
   1.110  
   1.111 -fun BasicSimpTac ctxt var_names tac =
   1.112 +fun basic_simp_tac ctxt var_names tac =
   1.113    simp_tac
   1.114      (put_simpset HOL_basic_ss ctxt
   1.115        addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [Record.simproc])
   1.116 -  THEN_MAYBE' MaxSimpTac ctxt var_names tac;
   1.117 +  THEN_MAYBE' max_simp_tac ctxt var_names tac;
   1.118  
   1.119  
   1.120  (** hoare_rule_tac **)
   1.121 @@ -173,9 +180,9 @@
   1.122              rule_tac false (i + 1)],
   1.123            EVERY [
   1.124              rtac @{thm WhileRule} i,
   1.125 -            BasicSimpTac ctxt var_names tac (i + 2),
   1.126 +            basic_simp_tac ctxt var_names tac (i + 2),
   1.127              rule_tac true (i + 1)]]
   1.128 -         THEN (if pre_cond then BasicSimpTac ctxt var_names tac i else rtac subset_refl i)));
   1.129 +         THEN (if pre_cond then basic_simp_tac ctxt var_names tac i else rtac subset_refl i)));
   1.130    in rule_tac end;
   1.131  
   1.132