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;