more modularization
authorhaftmann
Sat Sep 10 19:44:41 2011 +0200 (2011-09-10)
changeset 4486892be5b32ca71
parent 44860 56101fa00193
child 44869 328825888426
more modularization
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Tools/hologic.ML
src/HOL/Tools/inductive.ML
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Sat Sep 10 10:29:24 2011 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Sat Sep 10 19:44:41 2011 +0200
     1.3 @@ -14,7 +14,6 @@
     1.4  structure NominalInductive : NOMINAL_INDUCTIVE =
     1.5  struct
     1.6  
     1.7 -val inductive_forall_name = "HOL.induct_forall";
     1.8  val inductive_forall_def = @{thm induct_forall_def};
     1.9  val inductive_atomize = @{thms induct_atomize};
    1.10  val inductive_rulify = @{thms induct_rulify};
    1.11 @@ -42,7 +41,7 @@
    1.12  
    1.13  fun mk_perm_bool_simproc names = Simplifier.simproc_global_i
    1.14    (theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn thy => fn ss =>
    1.15 -    fn Const ("Nominal.perm", _) $ _ $ t =>
    1.16 +    fn Const (@{const_name Nominal.perm}, _) $ _ $ t =>
    1.17           if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
    1.18           then SOME perm_bool else NONE
    1.19       | _ => NONE);
    1.20 @@ -93,13 +92,13 @@
    1.21        (case head_of p of
    1.22           Const (name, _) =>
    1.23             if member (op =) names name then SOME (HOLogic.mk_conj (p,
    1.24 -             Const ("Fun.id", HOLogic.boolT --> HOLogic.boolT) $
    1.25 +             Const (@{const_name Fun.id}, HOLogic.boolT --> HOLogic.boolT) $
    1.26                 (subst_bounds (pis, strip_all pis q))))
    1.27             else NONE
    1.28         | _ => NONE)
    1.29    | inst_conj_all names ps pis t u =
    1.30        if member (op aconv) ps (head_of u) then
    1.31 -        SOME (Const ("Fun.id", HOLogic.boolT --> HOLogic.boolT) $
    1.32 +        SOME (Const (@{const_name Fun.id}, HOLogic.boolT --> HOLogic.boolT) $
    1.33            (subst_bounds (pis, strip_all pis t)))
    1.34        else NONE
    1.35    | inst_conj_all _ _ _ _ _ = NONE;
    1.36 @@ -214,10 +213,8 @@
    1.37      fun lift_prem (t as (f $ u)) =
    1.38            let val (p, ts) = strip_comb t
    1.39            in
    1.40 -            if member (op =) ps p then
    1.41 -              Const (inductive_forall_name,
    1.42 -                (fsT --> HOLogic.boolT) --> HOLogic.boolT) $
    1.43 -                  Abs ("z", fsT, lift_pred p (map (incr_boundvars 1) ts))
    1.44 +            if member (op =) ps p then HOLogic.mk_induct_forall fsT $
    1.45 +              Abs ("z", fsT, lift_pred p (map (incr_boundvars 1) ts))
    1.46              else lift_prem f $ lift_prem u
    1.47            end
    1.48        | lift_prem (Abs (s, T, t)) = Abs (s, T, lift_prem t)
    1.49 @@ -276,7 +273,7 @@
    1.50        ("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
    1.51      val eqvt_ss = Simplifier.global_context thy HOL_basic_ss
    1.52        addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
    1.53 -      addsimprocs [mk_perm_bool_simproc ["Fun.id"],
    1.54 +      addsimprocs [mk_perm_bool_simproc [@{const_name Fun.id}],
    1.55          NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
    1.56      val fresh_bij = Global_Theory.get_thms thy "fresh_bij";
    1.57      val perm_bij = Global_Theory.get_thms thy "perm_bij";
    1.58 @@ -292,7 +289,7 @@
    1.59          (** protect terms to avoid that fresh_prod interferes with  **)
    1.60          (** pairs used in introduction rules of inductive predicate **)
    1.61          fun protect t =
    1.62 -          let val T = fastype_of t in Const ("Fun.id", T --> T) $ t end;
    1.63 +          let val T = fastype_of t in Const (@{const_name Fun.id}, T --> T) $ t end;
    1.64          val p = foldr1 HOLogic.mk_prod (map protect ts @ freshs1);
    1.65          val ex = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop
    1.66              (HOLogic.exists_const T $ Abs ("x", T,
    1.67 @@ -335,7 +332,7 @@
    1.68                   fun concat_perm pi1 pi2 =
    1.69                     let val T = fastype_of pi1
    1.70                     in if T = fastype_of pi2 then
    1.71 -                       Const ("List.append", T --> T --> T) $ pi1 $ pi2
    1.72 +                       Const (@{const_name List.append}, T --> T --> T) $ pi1 $ pi2
    1.73                       else pi2
    1.74                     end;
    1.75                   val pis'' = fold (concat_perm #> map) pis' pis;
     2.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Sat Sep 10 10:29:24 2011 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Sat Sep 10 19:44:41 2011 +0200
     2.3 @@ -15,7 +15,6 @@
     2.4  structure NominalInductive2 : NOMINAL_INDUCTIVE2 =
     2.5  struct
     2.6  
     2.7 -val inductive_forall_name = "HOL.induct_forall";
     2.8  val inductive_forall_def = @{thm induct_forall_def};
     2.9  val inductive_atomize = @{thms induct_atomize};
    2.10  val inductive_rulify = @{thms induct_rulify};
    2.11 @@ -240,10 +239,8 @@
    2.12      fun lift_prem (t as (f $ u)) =
    2.13            let val (p, ts) = strip_comb t
    2.14            in
    2.15 -            if member (op =) ps p then
    2.16 -              Const (inductive_forall_name,
    2.17 -                (fsT --> HOLogic.boolT) --> HOLogic.boolT) $
    2.18 -                  Abs ("z", fsT, lift_pred p (map (incr_boundvars 1) ts))
    2.19 +            if member (op =) ps p then HOLogic.mk_induct_forall fsT $
    2.20 +              Abs ("z", fsT, lift_pred p (map (incr_boundvars 1) ts))
    2.21              else lift_prem f $ lift_prem u
    2.22            end
    2.23        | lift_prem (Abs (s, T, t)) = Abs (s, T, lift_prem t)
     3.1 --- a/src/HOL/Tools/hologic.ML	Sat Sep 10 10:29:24 2011 +0200
     3.2 +++ b/src/HOL/Tools/hologic.ML	Sat Sep 10 19:44:41 2011 +0200
     3.3 @@ -17,6 +17,7 @@
     3.4    val dest_Trueprop: term -> term
     3.5    val true_const: term
     3.6    val false_const: term
     3.7 +  val mk_induct_forall: typ -> term
     3.8    val mk_setT: typ -> typ
     3.9    val dest_setT: typ -> typ
    3.10    val Collect_const: typ -> term
    3.11 @@ -164,6 +165,8 @@
    3.12  val true_const =  Const ("HOL.True", boolT);
    3.13  val false_const = Const ("HOL.False", boolT);
    3.14  
    3.15 +fun mk_induct_forall T = Const ("HOL.induct_forall", (T --> boolT) --> boolT);
    3.16 +
    3.17  fun mk_setT T = T --> boolT;
    3.18  
    3.19  fun dest_setT (Type ("fun", [T, Type ("HOL.bool", [])])) = T
     4.1 --- a/src/HOL/Tools/inductive.ML	Sat Sep 10 10:29:24 2011 +0200
     4.2 +++ b/src/HOL/Tools/inductive.ML	Sat Sep 10 19:44:41 2011 +0200
     4.3 @@ -31,7 +31,6 @@
     4.4    val mono_del: attribute
     4.5    val get_monos: Proof.context -> thm list
     4.6    val mk_cases: Proof.context -> term -> thm
     4.7 -  val inductive_forall_name: string
     4.8    val inductive_forall_def: thm
     4.9    val rulify: thm -> thm
    4.10    val inductive_cases: (Attrib.binding * string list) list -> local_theory ->
    4.11 @@ -92,7 +91,6 @@
    4.12  
    4.13  (** theory context references **)
    4.14  
    4.15 -val inductive_forall_name = "HOL.induct_forall";
    4.16  val inductive_forall_def = @{thm induct_forall_def};
    4.17  val inductive_conj_name = "HOL.induct_conj";
    4.18  val inductive_conj_def = @{thm induct_conj_def};