src/HOL/Hoare/hoare_tac.ML
 changeset 41449 7339f0e7c513 parent 38012 3ca193a6ae5a child 42793 88bee9f6eec7
```     1.1 --- a/src/HOL/Hoare/hoare_tac.ML	Fri Jan 07 18:07:27 2011 +0100
1.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Fri Jan 07 18:32:19 2011 +0100
1.3 @@ -4,6 +4,8 @@
1.4  Derivation of the proof rules and, most importantly, the VCG tactic.
1.5  *)
1.6
1.7 +(* FIXME structure Hoare: HOARE *)
1.8 +
1.9  (*** The tactics ***)
1.10
1.11  (*****************************************************************************)
1.12 @@ -13,7 +15,7 @@
1.13  (** working on at the moment of the call                                    **)
1.14  (*****************************************************************************)
1.15
1.16 -local open HOLogic in
1.17 +local
1.18
1.19  (** maps (%x1 ... xn. t) to [x1,...,xn] **)
1.20  fun abs2list (Const (@{const_name prod_case}, _) \$ Abs (x, T, t)) = Free (x, T) :: abs2list t
1.21 @@ -26,14 +28,17 @@
1.22
1.23  (** abstraction of body over a tuple formed from a list of free variables.
1.24  Types are also built **)
1.25 -fun mk_abstupleC []     body = absfree ("x", unitT, body)
1.26 +fun mk_abstupleC []     body = absfree ("x", HOLogic.unitT, body)
1.27    | mk_abstupleC (v::w) body = let val (n,T) = dest_Free v
1.28                                 in if w=[] then absfree (n, T, body)
1.29          else let val z  = mk_abstupleC w body;
1.30                   val T2 = case z of Abs(_,T,_) => T
1.31                          | Const (_, Type (_,[_, Type (_,[T,_])])) \$ _ => T;
1.32 -       in Const (@{const_name prod_case}, (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT)
1.33 -          \$ absfree (n, T, z) end end;
1.34 +       in
1.35 +        Const (@{const_name prod_case},
1.36 +          (T --> T2 --> HOLogic.boolT) --> HOLogic.mk_prodT (T,T2) --> HOLogic.boolT)
1.37 +            \$ absfree (n, T, z)
1.38 +       end end;
1.39
1.40  (** maps [x1,...,xn] to (x1,...,xn) and types**)
1.41  fun mk_bodyC []      = HOLogic.unit
1.42 @@ -43,22 +48,23 @@
1.43                          val T2 = case z of Free(_, T) => T
1.44                                           | Const (@{const_name Pair}, Type ("fun", [_, Type
1.45                                              ("fun", [_, T])])) \$ _ \$ _ => T;
1.46 -                 in Const (@{const_name Pair}, [T, T2] ---> mk_prodT (T, T2)) \$ x \$ z end;
1.47 +                 in Const (@{const_name Pair}, [T, T2] ---> HOLogic.mk_prodT (T, T2)) \$ x \$ z end;
1.48
1.49  (** maps a subgoal of the form:
1.50          VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]**)
1.51  fun get_vars c =
1.52    let
1.53      val d = Logic.strip_assums_concl c;
1.54 -    val Const _ \$ pre \$ _ \$ _ = dest_Trueprop d;
1.55 +    val Const _ \$ pre \$ _ \$ _ = HOLogic.dest_Trueprop d;
1.56    in mk_vars pre end;
1.57
1.58  fun mk_CollectC trm =
1.59    let val T as Type ("fun",[t,_]) = fastype_of trm
1.60 -  in Collect_const t \$ trm end;
1.61 +  in HOLogic.Collect_const t \$ trm end;
1.62
1.63 -fun inclt ty = Const (@{const_name Orderings.less_eq}, [ty,ty] ---> boolT);
1.64 +fun inclt ty = Const (@{const_name Orderings.less_eq}, [ty,ty] ---> HOLogic.boolT);
1.65
1.66 +in
1.67
1.68  fun Mset ctxt prop =
1.69    let
1.70 @@ -66,11 +72,11 @@
1.71
1.72      val vars = get_vars prop;
1.73      val varsT = fastype_of (mk_bodyC vars);
1.74 -    val big_Collect = mk_CollectC (mk_abstupleC vars (Free (P, varsT --> boolT) \$ mk_bodyC vars));
1.75 -    val small_Collect = mk_CollectC (Abs ("x", varsT, Free (P, varsT --> boolT) \$ Bound 0));
1.76 +    val big_Collect = mk_CollectC (mk_abstupleC vars (Free (P, varsT --> HOLogic.boolT) \$ mk_bodyC vars));
1.77 +    val small_Collect = mk_CollectC (Abs ("x", varsT, Free (P, varsT --> HOLogic.boolT) \$ Bound 0));
1.78
1.79      val MsetT = fastype_of big_Collect;
1.80 -    fun Mset_incl t = mk_Trueprop (inclt MsetT \$ Free (Mset, MsetT) \$ t);
1.81 +    fun Mset_incl t = HOLogic.mk_Trueprop (inclt MsetT \$ Free (Mset, MsetT) \$ t);
1.82      val impl = Logic.mk_implies (Mset_incl big_Collect, Mset_incl small_Collect);
1.83      val th = Goal.prove ctxt [Mset, P] [] impl (fn _ => blast_tac (claset_of ctxt) 1);
1.84   in (vars, th) end;
```