do not open ML structures;
authorwenzelm
Fri Jan 07 18:32:19 2011 +0100 (2011-01-07)
changeset 414497339f0e7c513
parent 41448 72ba43b47c7f
child 41450 3a62f88d9650
do not open ML structures;
src/HOL/Hoare/hoare_tac.ML
src/Sequents/modal.ML
src/ZF/Tools/inductive_package.ML
     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;
     2.1 --- a/src/Sequents/modal.ML	Fri Jan 07 18:07:27 2011 +0100
     2.2 +++ b/src/Sequents/modal.ML	Fri Jan 07 18:32:19 2011 +0100
     2.3 @@ -5,7 +5,6 @@
     2.4  Simple modal reasoner.
     2.5  *)
     2.6  
     2.7 -
     2.8  signature MODAL_PROVER_RULE =
     2.9  sig
    2.10      val rewrite_rls      : thm list
    2.11 @@ -25,8 +24,6 @@
    2.12  
    2.13  functor Modal_ProverFun (Modal_Rule: MODAL_PROVER_RULE) : MODAL_PROVER = 
    2.14  struct
    2.15 -local open Modal_Rule
    2.16 -in 
    2.17  
    2.18  (*Returns the list of all formulas in the sequent*)
    2.19  fun forms_of_seq (Const(@{const_name SeqO'},_) $ P $ u) = P :: forms_of_seq u
    2.20 @@ -62,12 +59,12 @@
    2.21  
    2.22  (* NB No back tracking possible with aside rules *)
    2.23  
    2.24 -fun aside_tac n = DETERM(REPEAT (filt_resolve_tac aside_rls 999 n));
    2.25 +fun aside_tac n = DETERM(REPEAT (filt_resolve_tac Modal_Rule.aside_rls 999 n));
    2.26  fun rule_tac rls n = fresolve_tac rls n THEN aside_tac n;
    2.27  
    2.28 -val fres_safe_tac = fresolve_tac safe_rls;
    2.29 -val fres_unsafe_tac = fresolve_tac unsafe_rls THEN' aside_tac;
    2.30 -val fres_bound_tac = fresolve_tac bound_rls;
    2.31 +val fres_safe_tac = fresolve_tac Modal_Rule.safe_rls;
    2.32 +val fres_unsafe_tac = fresolve_tac Modal_Rule.unsafe_rls THEN' aside_tac;
    2.33 +val fres_bound_tac = fresolve_tac Modal_Rule.bound_rls;
    2.34  
    2.35  fun UPTOGOAL n tf = let fun tac i = if i<n then all_tac
    2.36                                      else tf(i) THEN tac(i-1)
    2.37 @@ -81,7 +78,7 @@
    2.38                   ((fres_unsafe_tac n  THEN UPTOGOAL n (solven_tac d)) APPEND
    2.39                     (fres_bound_tac n  THEN UPTOGOAL n (solven_tac (d-1)))));
    2.40  
    2.41 -fun solve_tac d = rewrite_goals_tac rewrite_rls THEN solven_tac d 1;
    2.42 +fun solve_tac d = rewrite_goals_tac Modal_Rule.rewrite_rls THEN solven_tac d 1;
    2.43  
    2.44  fun step_tac n = 
    2.45      COND (has_fewer_prems 1) all_tac 
    2.46 @@ -89,4 +86,3 @@
    2.47            (fres_unsafe_tac n APPEND fres_bound_tac n));
    2.48  
    2.49  end;
    2.50 -end;
     3.1 --- a/src/ZF/Tools/inductive_package.ML	Fri Jan 07 18:07:27 2011 +0100
     3.2 +++ b/src/ZF/Tools/inductive_package.ML	Fri Jan 07 18:32:19 2011 +0100
     3.3 @@ -43,8 +43,6 @@
     3.4   : INDUCTIVE_PACKAGE =
     3.5  struct
     3.6  
     3.7 -open Ind_Syntax;
     3.8 -
     3.9  val co_prefix = if coind then "co" else "";
    3.10  
    3.11  
    3.12 @@ -84,7 +82,7 @@
    3.13      (fn a => "Base name of recursive set not an identifier: " ^ a);
    3.14  
    3.15    local (*Checking the introduction rules*)
    3.16 -    val intr_sets = map (#2 o rule_concl_msg thy) intr_tms;
    3.17 +    val intr_sets = map (#2 o Ind_Syntax.rule_concl_msg thy) intr_tms;
    3.18      fun intr_ok set =
    3.19          case head_of set of Const(a,recT) => member (op =) rec_names a | _ => false;
    3.20    in
    3.21 @@ -109,16 +107,16 @@
    3.22    (*Makes a disjunct from an introduction rule*)
    3.23    fun fp_part intr = (*quantify over rule's free vars except parameters*)
    3.24      let val prems = map dest_tprop (Logic.strip_imp_prems intr)
    3.25 -        val dummy = List.app (fn rec_hd => List.app (chk_prem rec_hd) prems) rec_hds
    3.26 +        val dummy = List.app (fn rec_hd => List.app (Ind_Syntax.chk_prem rec_hd) prems) rec_hds
    3.27          val exfrees = subtract (op =) rec_params (OldTerm.term_frees intr)
    3.28 -        val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr))
    3.29 +        val zeq = FOLogic.mk_eq (Free(z', Ind_Syntax.iT), #1 (Ind_Syntax.rule_concl intr))
    3.30      in List.foldr FOLogic.mk_exists
    3.31               (Balanced_Tree.make FOLogic.mk_conj (zeq::prems)) exfrees
    3.32      end;
    3.33  
    3.34    (*The Part(A,h) terms -- compose injections to make h*)
    3.35 -  fun mk_Part (Bound 0) = Free(X',iT) (*no mutual rec, no Part needed*)
    3.36 -    | mk_Part h         = @{const Part} $ Free(X',iT) $ Abs(w',iT,h);
    3.37 +  fun mk_Part (Bound 0) = Free(X', Ind_Syntax.iT) (*no mutual rec, no Part needed*)
    3.38 +    | mk_Part h = @{const Part} $ Free(X', Ind_Syntax.iT) $ Abs (w', Ind_Syntax.iT, h);
    3.39  
    3.40    (*Access to balanced disjoint sums via injections*)
    3.41    val parts = map mk_Part
    3.42 @@ -128,9 +126,10 @@
    3.43    (*replace each set by the corresponding Part(A,h)*)
    3.44    val part_intrs = map (subst_free (rec_tms ~~ parts) o fp_part) intr_tms;
    3.45  
    3.46 -  val fp_abs = absfree(X', iT,
    3.47 -                   mk_Collect(z', dom_sum,
    3.48 -                              Balanced_Tree.make FOLogic.mk_disj part_intrs));
    3.49 +  val fp_abs =
    3.50 +    absfree (X', Ind_Syntax.iT,
    3.51 +        Ind_Syntax.mk_Collect (z', dom_sum,
    3.52 +            Balanced_Tree.make FOLogic.mk_disj part_intrs));
    3.53  
    3.54    val fp_rhs = Fp.oper $ dom_sum $ fp_abs
    3.55  
    3.56 @@ -161,7 +160,7 @@
    3.57           (case parts of
    3.58               [_] => []                        (*no mutual recursion*)
    3.59             | _ => rec_tms ~~          (*define the sets as Parts*)
    3.60 -                  map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
    3.61 +                  map (subst_atomic [(Free (X', Ind_Syntax.iT), big_rec_tm)]) parts));
    3.62  
    3.63    (*tracing: print the fixedpoint definition*)
    3.64    val dummy = if !Ind_Syntax.trace then