# HG changeset patch
# User wenzelm
# Date 1393012068 -3600
# Node ID ec14796cd140bd238f6b720450a0a7b8125e02f2
# Parent  f0f895716a8bb4006076a0267b9bb7789b35b2b1
tuned whitespace;
tuned names;

diff -r f0f895716a8b -r ec14796cd140 src/HOL/Hoare/hoare_tac.ML
--- a/src/HOL/Hoare/hoare_tac.ML	Fri Feb 21 20:37:13 2014 +0100
+++ b/src/HOL/Hoare/hoare_tac.ML	Fri Feb 21 20:47:48 2014 +0100
@@ -6,7 +6,8 @@
 
 signature HOARE =
 sig
-  val hoare_rule_tac: Proof.context -> term list * thm -> (int -> tactic) -> bool -> int -> tactic
+  val hoare_rule_tac: Proof.context -> term list * thm -> (int -> tactic) -> bool ->
+    int -> tactic
   val hoare_tac: Proof.context -> (int -> tactic) -> int -> tactic
 end;
 
@@ -52,26 +53,30 @@
       end;
 
 (** maps [x1,...,xn] to (x1,...,xn) and types**)
-fun mk_bodyC []      = HOLogic.unit
-  | mk_bodyC (x::xs) = if xs=[] then x
-               else let val (n, T) = dest_Free x ;
-                        val z = mk_bodyC xs;
-                        val T2 = case z of Free(_, T) => T
-                                         | Const (@{const_name Pair}, Type ("fun", [_, Type
-                                            ("fun", [_, T])])) $ _ $ _ => T;
-                 in Const (@{const_name Pair}, [T, T2] ---> HOLogic.mk_prodT (T, T2)) $ x $ z end;
+fun mk_bodyC [] = HOLogic.unit
+  | mk_bodyC [x] = x
+  | mk_bodyC (x :: xs) =
+      let
+        val (_, T) = dest_Free x;
+        val z = mk_bodyC xs;
+        val T2 =
+          (case z of
+            Free (_, T) => T
+          | Const (@{const_name Pair}, Type ("fun", [_, Type ("fun", [_, T])])) $ _ $ _ => T);
+     in Const (@{const_name Pair}, [T, T2] ---> HOLogic.mk_prodT (T, T2)) $ x $ z end;
 
 (** maps a subgoal of the form:
-        VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]**)
+    VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]
+**)
 fun get_vars c =
   let
     val d = Logic.strip_assums_concl c;
     val Const _ $ pre $ _ $ _ = HOLogic.dest_Trueprop d;
   in mk_vars pre end;
 
-fun mk_CollectC trm =
-  let val T as Type ("fun",[t,_]) = fastype_of trm
-  in HOLogic.Collect_const t $ trm end;
+fun mk_CollectC tm =
+  let val T as Type ("fun",[t,_]) = fastype_of tm;
+  in HOLogic.Collect_const t $ tm end;
 
 fun inclt ty = Const (@{const_name Orderings.less_eq}, [ty,ty] ---> HOLogic.boolT);
 
@@ -83,8 +88,10 @@
 
     val vars = get_vars prop;
     val varsT = fastype_of (mk_bodyC vars);
-    val big_Collect = mk_CollectC (mk_abstupleC vars (Free (P, varsT --> HOLogic.boolT) $ mk_bodyC vars));
-    val small_Collect = mk_CollectC (Abs ("x", varsT, Free (P, varsT --> HOLogic.boolT) $ Bound 0));
+    val big_Collect =
+      mk_CollectC (mk_abstupleC vars (Free (P, varsT --> HOLogic.boolT) $ mk_bodyC vars));
+    val small_Collect =
+      mk_CollectC (Abs ("x", varsT, Free (P, varsT --> HOLogic.boolT) $ Bound 0));
 
     val MsetT = fastype_of big_Collect;
     fun Mset_incl t = HOLogic.mk_Trueprop (inclt MsetT $ Free (Mset, MsetT) $ t);
@@ -111,7 +118,7 @@
   simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]);
 
 (*****************************************************************************)
-(** set2pred_tac transforms sets inclusion into predicates implication,     **)
+(** set_to_pred_tac transforms sets inclusion into predicates implication,  **)
 (** maintaining the original variable names.                                **)
 (** Ex. "{x. x=0} <= {x. x <= 1}" -set2pred-> "x=0 --> x <= 1"              **)
 (** Subgoals containing intersections (A Int B) or complement sets (-A)     **)
@@ -122,7 +129,7 @@
 (** simplification done by (split_all_tac)                                  **)
 (*****************************************************************************)
 
-fun set2pred_tac ctxt var_names = SUBGOAL (fn (_, i) =>
+fun set_to_pred_tac ctxt var_names = SUBGOAL (fn (_, i) =>
   before_set2pred_simp_tac ctxt i THEN_MAYBE
   EVERY [
     rtac subsetI i,
@@ -132,22 +139,22 @@
      (rename_tac var_names i THEN
       full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]) i)]);
 
-(*****************************************************************************)
-(** BasicSimpTac is called to simplify all verification conditions. It does **)
-(** a light simplification by applying "mem_Collect_eq", then it calls      **)
-(** MaxSimpTac, which solves subgoals of the form "A <= A",                 **)
-(** and transforms any other into predicates, applying then                 **)
-(** the tactic chosen by the user, which may solve the subgoal completely.  **)
-(*****************************************************************************)
+(*******************************************************************************)
+(** basic_simp_tac is called to simplify all verification conditions. It does **)
+(** a light simplification by applying "mem_Collect_eq", then it calls        **)
+(** max_simp_tac, which solves subgoals of the form "A <= A",                 **)
+(** and transforms any other into predicates, applying then                   **)
+(** the tactic chosen by the user, which may solve the subgoal completely.    **)
+(*******************************************************************************)
 
-fun MaxSimpTac ctxt var_names tac =
-  FIRST'[rtac subset_refl, set2pred_tac ctxt var_names THEN_MAYBE' tac];
+fun max_simp_tac ctxt var_names tac =
+  FIRST' [rtac subset_refl, set_to_pred_tac ctxt var_names THEN_MAYBE' tac];
 
-fun BasicSimpTac ctxt var_names tac =
+fun basic_simp_tac ctxt var_names tac =
   simp_tac
     (put_simpset HOL_basic_ss ctxt
       addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [Record.simproc])
-  THEN_MAYBE' MaxSimpTac ctxt var_names tac;
+  THEN_MAYBE' max_simp_tac ctxt var_names tac;
 
 
 (** hoare_rule_tac **)
@@ -173,9 +180,9 @@
             rule_tac false (i + 1)],
           EVERY [
             rtac @{thm WhileRule} i,
-            BasicSimpTac ctxt var_names tac (i + 2),
+            basic_simp_tac ctxt var_names tac (i + 2),
             rule_tac true (i + 1)]]
-         THEN (if pre_cond then BasicSimpTac ctxt var_names tac i else rtac subset_refl i)));
+         THEN (if pre_cond then basic_simp_tac ctxt var_names tac i else rtac subset_refl i)));
   in rule_tac end;