# HG changeset patch # User haftmann # Date 1315676681 -7200 # Node ID 92be5b32ca71e4c6fe227cd4543f7da87aed424e # Parent 56101fa00193b0c02f68041ef215916d48204fc1 more modularization diff -r 56101fa00193 -r 92be5b32ca71 src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Sat Sep 10 10:29:24 2011 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Sat Sep 10 19:44:41 2011 +0200 @@ -14,7 +14,6 @@ structure NominalInductive : NOMINAL_INDUCTIVE = struct -val inductive_forall_name = "HOL.induct_forall"; val inductive_forall_def = @{thm induct_forall_def}; val inductive_atomize = @{thms induct_atomize}; val inductive_rulify = @{thms induct_rulify}; @@ -42,7 +41,7 @@ fun mk_perm_bool_simproc names = Simplifier.simproc_global_i (theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn thy => fn ss => - fn Const ("Nominal.perm", _) $ _ $ t => + fn Const (@{const_name Nominal.perm}, _) $ _ $ t => if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t)) then SOME perm_bool else NONE | _ => NONE); @@ -93,13 +92,13 @@ (case head_of p of Const (name, _) => if member (op =) names name then SOME (HOLogic.mk_conj (p, - Const ("Fun.id", HOLogic.boolT --> HOLogic.boolT) $ + Const (@{const_name Fun.id}, HOLogic.boolT --> HOLogic.boolT) $ (subst_bounds (pis, strip_all pis q)))) else NONE | _ => NONE) | inst_conj_all names ps pis t u = if member (op aconv) ps (head_of u) then - SOME (Const ("Fun.id", HOLogic.boolT --> HOLogic.boolT) $ + SOME (Const (@{const_name Fun.id}, HOLogic.boolT --> HOLogic.boolT) $ (subst_bounds (pis, strip_all pis t))) else NONE | inst_conj_all _ _ _ _ _ = NONE; @@ -214,10 +213,8 @@ fun lift_prem (t as (f $ u)) = let val (p, ts) = strip_comb t in - if member (op =) ps p then - Const (inductive_forall_name, - (fsT --> HOLogic.boolT) --> HOLogic.boolT) $ - Abs ("z", fsT, lift_pred p (map (incr_boundvars 1) ts)) + if member (op =) ps p then HOLogic.mk_induct_forall fsT $ + Abs ("z", fsT, lift_pred p (map (incr_boundvars 1) ts)) else lift_prem f $ lift_prem u end | lift_prem (Abs (s, T, t)) = Abs (s, T, lift_prem t) @@ -276,7 +273,7 @@ ("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs; val eqvt_ss = Simplifier.global_context thy HOL_basic_ss addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms) - addsimprocs [mk_perm_bool_simproc ["Fun.id"], + addsimprocs [mk_perm_bool_simproc [@{const_name Fun.id}], NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]; val fresh_bij = Global_Theory.get_thms thy "fresh_bij"; val perm_bij = Global_Theory.get_thms thy "perm_bij"; @@ -292,7 +289,7 @@ (** protect terms to avoid that fresh_prod interferes with **) (** pairs used in introduction rules of inductive predicate **) fun protect t = - let val T = fastype_of t in Const ("Fun.id", T --> T) $ t end; + let val T = fastype_of t in Const (@{const_name Fun.id}, T --> T) $ t end; val p = foldr1 HOLogic.mk_prod (map protect ts @ freshs1); val ex = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.exists_const T $ Abs ("x", T, @@ -335,7 +332,7 @@ fun concat_perm pi1 pi2 = let val T = fastype_of pi1 in if T = fastype_of pi2 then - Const ("List.append", T --> T --> T) $ pi1 $ pi2 + Const (@{const_name List.append}, T --> T --> T) $ pi1 $ pi2 else pi2 end; val pis'' = fold (concat_perm #> map) pis' pis; diff -r 56101fa00193 -r 92be5b32ca71 src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Sat Sep 10 10:29:24 2011 +0200 +++ b/src/HOL/Nominal/nominal_inductive2.ML Sat Sep 10 19:44:41 2011 +0200 @@ -15,7 +15,6 @@ structure NominalInductive2 : NOMINAL_INDUCTIVE2 = struct -val inductive_forall_name = "HOL.induct_forall"; val inductive_forall_def = @{thm induct_forall_def}; val inductive_atomize = @{thms induct_atomize}; val inductive_rulify = @{thms induct_rulify}; @@ -240,10 +239,8 @@ fun lift_prem (t as (f $ u)) = let val (p, ts) = strip_comb t in - if member (op =) ps p then - Const (inductive_forall_name, - (fsT --> HOLogic.boolT) --> HOLogic.boolT) $ - Abs ("z", fsT, lift_pred p (map (incr_boundvars 1) ts)) + if member (op =) ps p then HOLogic.mk_induct_forall fsT $ + Abs ("z", fsT, lift_pred p (map (incr_boundvars 1) ts)) else lift_prem f $ lift_prem u end | lift_prem (Abs (s, T, t)) = Abs (s, T, lift_prem t) diff -r 56101fa00193 -r 92be5b32ca71 src/HOL/Tools/hologic.ML --- a/src/HOL/Tools/hologic.ML Sat Sep 10 10:29:24 2011 +0200 +++ b/src/HOL/Tools/hologic.ML Sat Sep 10 19:44:41 2011 +0200 @@ -17,6 +17,7 @@ val dest_Trueprop: term -> term val true_const: term val false_const: term + val mk_induct_forall: typ -> term val mk_setT: typ -> typ val dest_setT: typ -> typ val Collect_const: typ -> term @@ -164,6 +165,8 @@ val true_const = Const ("HOL.True", boolT); val false_const = Const ("HOL.False", boolT); +fun mk_induct_forall T = Const ("HOL.induct_forall", (T --> boolT) --> boolT); + fun mk_setT T = T --> boolT; fun dest_setT (Type ("fun", [T, Type ("HOL.bool", [])])) = T diff -r 56101fa00193 -r 92be5b32ca71 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Sat Sep 10 10:29:24 2011 +0200 +++ b/src/HOL/Tools/inductive.ML Sat Sep 10 19:44:41 2011 +0200 @@ -31,7 +31,6 @@ val mono_del: attribute val get_monos: Proof.context -> thm list val mk_cases: Proof.context -> term -> thm - val inductive_forall_name: string val inductive_forall_def: thm val rulify: thm -> thm val inductive_cases: (Attrib.binding * string list) list -> local_theory -> @@ -92,7 +91,6 @@ (** theory context references **) -val inductive_forall_name = "HOL.induct_forall"; val inductive_forall_def = @{thm induct_forall_def}; val inductive_conj_name = "HOL.induct_conj"; val inductive_conj_def = @{thm induct_conj_def};