# HG changeset patch # User wenzelm # Date 1205962088 -3600 # Node ID 44473c957672bb6b15a5171e07a1ee9e270fc592 # Parent a0e2b706ce7385a3efeeb15a3a9e723f703bfd1a auxiliary dynamic_thm(s) for fact lookup; diff -r a0e2b706ce73 -r 44473c957672 src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Wed Mar 19 22:27:57 2008 +0100 +++ b/src/HOL/Nominal/nominal_atoms.ML Wed Mar 19 22:28:08 2008 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/Nominal/nominal_atoms.ML +(* title: HOL/Nominal/nominal_atoms.ML ID: $Id$ Author: Christian Urban and Stefan Berghofer, TU Muenchen @@ -230,17 +230,17 @@ let val ak_name_qu = Sign.full_name thy5 (ak_name); val i_type = Type(ak_name_qu,[]); - val cat = Const ("Nominal.at",(Term.itselfT i_type) --> HOLogic.boolT); + val cat = Const ("Nominal.at",(Term.itselfT i_type) --> HOLogic.boolT); val at_type = Logic.mk_type i_type; - val simp_s = HOL_ss addsimps PureThy.get_thmss thy5 - [Name "at_def", - Name (ak_name ^ "_prm_" ^ ak_name ^ "_def"), - Name (ak_name ^ "_prm_" ^ ak_name ^ ".simps"), - Name ("swap_" ^ ak_name ^ "_def"), - Name ("swap_" ^ ak_name ^ ".simps"), - Name (ak_name ^ "_infinite")] - - val name = "at_"^ak_name^ "_inst"; + val simp_s = HOL_ss addsimps maps (dynamic_thms thy5) + ["at_def", + ak_name ^ "_prm_" ^ ak_name ^ "_def", + ak_name ^ "_prm_" ^ ak_name ^ ".simps", + "swap_" ^ ak_name ^ "_def", + "swap_" ^ ak_name ^ ".simps", + ak_name ^ "_infinite"] + + val name = "at_"^ak_name^ "_inst"; val statement = HOLogic.mk_Trueprop (cat $ at_type); val proof = fn _ => simp_tac simp_s 1 @@ -256,7 +256,7 @@ (* pt_3: pi1 ~ pi2 ==> perm pi1 x = perm pi2 x *) val (pt_ax_classes,thy7) = fold_map (fn (ak_name, T) => fn thy => let - val cl_name = "pt_"^ak_name; + val cl_name = "pt_"^ak_name; val ty = TFree("'a",["HOL.type"]); val x = Free ("x", ty); val pi1 = Free ("pi1", mk_permT T); @@ -293,16 +293,16 @@ val pt_name_qu = Sign.full_name thy7 ("pt_"^ak_name); val i_type1 = TFree("'x",[pt_name_qu]); val i_type2 = Type(ak_name_qu,[]); - val cpt = Const ("Nominal.pt",(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT); + val cpt = Const ("Nominal.pt",(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT); val pt_type = Logic.mk_type i_type1; val at_type = Logic.mk_type i_type2; - val simp_s = HOL_ss addsimps PureThy.get_thmss thy7 - [Name "pt_def", - Name ("pt_" ^ ak_name ^ "1"), - Name ("pt_" ^ ak_name ^ "2"), - Name ("pt_" ^ ak_name ^ "3")]; + val simp_s = HOL_ss addsimps maps (dynamic_thms thy7) + ["pt_def", + "pt_" ^ ak_name ^ "1", + "pt_" ^ ak_name ^ "2", + "pt_" ^ ak_name ^ "3"]; - val name = "pt_"^ak_name^ "_inst"; + val name = "pt_"^ak_name^ "_inst"; val statement = HOLogic.mk_Trueprop (cpt $ pt_type $ at_type); val proof = fn _ => simp_tac simp_s 1; @@ -315,8 +315,8 @@ (* fs_1: finite ((supp x):: set) *) val (fs_ax_classes,thy11) = fold_map (fn (ak_name, T) => fn thy => let - val cl_name = "fs_"^ak_name; - val pt_name = Sign.full_name thy ("pt_"^ak_name); + val cl_name = "fs_"^ak_name; + val pt_name = Sign.full_name thy ("pt_"^ak_name); val ty = TFree("'a",["HOL.type"]); val x = Free ("x", ty); val csupp = Const ("Nominal.supp", ty --> HOLogic.mk_setT T); @@ -327,7 +327,7 @@ in AxClass.define_class (cl_name, [pt_name]) [] [((cl_name ^ "1", []), [axiom1])] thy end) ak_names_types thy8; - + (* proves that every fs_-type together with -type *) (* instance of fs-type *) (* lemma abst__inst: *) @@ -339,15 +339,15 @@ val fs_name_qu = Sign.full_name thy11 ("fs_"^ak_name); val i_type1 = TFree("'x",[fs_name_qu]); val i_type2 = Type(ak_name_qu,[]); - val cfs = Const ("Nominal.fs", + val cfs = Const ("Nominal.fs", (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT); val fs_type = Logic.mk_type i_type1; val at_type = Logic.mk_type i_type2; - val simp_s = HOL_ss addsimps PureThy.get_thmss thy11 - [Name "fs_def", - Name ("fs_" ^ ak_name ^ "1")]; + val simp_s = HOL_ss addsimps maps (dynamic_thms thy11) + ["fs_def", + "fs_" ^ ak_name ^ "1"]; - val name = "fs_"^ak_name^ "_inst"; + val name = "fs_"^ak_name^ "_inst"; val statement = HOLogic.mk_Trueprop (cfs $ fs_type $ at_type); val proof = fn _ => simp_tac simp_s 1; @@ -359,54 +359,54 @@ (* cp__ giving a composition property *) (* cp__1: pi1 o pi2 o x = (pi1 o pi2) o (pi1 o x) *) val (cp_ax_classes,thy12b) = fold_map (fn (ak_name, T) => fn thy => - fold_map (fn (ak_name', T') => fn thy' => - let - val cl_name = "cp_"^ak_name^"_"^ak_name'; - val ty = TFree("'a",["HOL.type"]); + fold_map (fn (ak_name', T') => fn thy' => + let + val cl_name = "cp_"^ak_name^"_"^ak_name'; + val ty = TFree("'a",["HOL.type"]); val x = Free ("x", ty); val pi1 = Free ("pi1", mk_permT T); - val pi2 = Free ("pi2", mk_permT T'); - val cperm1 = Const ("Nominal.perm", mk_permT T --> ty --> ty); + val pi2 = Free ("pi2", mk_permT T'); + val cperm1 = Const ("Nominal.perm", mk_permT T --> ty --> ty); val cperm2 = Const ("Nominal.perm", mk_permT T' --> ty --> ty); val cperm3 = Const ("Nominal.perm", mk_permT T --> mk_permT T' --> mk_permT T'); val ax1 = HOLogic.mk_Trueprop - (HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x), + (HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x), cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x))); - in - AxClass.define_class (cl_name, ["HOL.type"]) [] [((cl_name ^ "1", []), [ax1])] thy' - end) ak_names_types thy) ak_names_types thy12; + in + AxClass.define_class (cl_name, ["HOL.type"]) [] [((cl_name ^ "1", []), [ax1])] thy' + end) ak_names_types thy) ak_names_types thy12; (* proves for every -combination a cp___inst theorem; *) (* lemma cp___inst: *) (* cp TYPE('a::cp__) TYPE() TYPE() *) val (cp_thms,thy12c) = fold_map (fn (ak_name, T) => fn thy => - fold_map (fn (ak_name', T') => fn thy' => + fold_map (fn (ak_name', T') => fn thy' => let val ak_name_qu = Sign.full_name thy' (ak_name); - val ak_name_qu' = Sign.full_name thy' (ak_name'); + val ak_name_qu' = Sign.full_name thy' (ak_name'); val cp_name_qu = Sign.full_name thy' ("cp_"^ak_name^"_"^ak_name'); val i_type0 = TFree("'a",[cp_name_qu]); val i_type1 = Type(ak_name_qu,[]); val i_type2 = Type(ak_name_qu',[]); - val ccp = Const ("Nominal.cp", + val ccp = Const ("Nominal.cp", (Term.itselfT i_type0)-->(Term.itselfT i_type1)--> (Term.itselfT i_type2)-->HOLogic.boolT); val at_type = Logic.mk_type i_type1; val at_type' = Logic.mk_type i_type2; - val cp_type = Logic.mk_type i_type0; - val simp_s = HOL_basic_ss addsimps PureThy.get_thmss thy' [(Name "cp_def")]; - val cp1 = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"1")); + val cp_type = Logic.mk_type i_type0; + val simp_s = HOL_basic_ss addsimps maps (dynamic_thms thy') ["cp_def"]; + val cp1 = dynamic_thm thy' ("cp_" ^ ak_name ^ "_" ^ ak_name' ^ "1"); - val name = "cp_"^ak_name^ "_"^ak_name'^"_inst"; + val name = "cp_"^ak_name^ "_"^ak_name'^"_inst"; val statement = HOLogic.mk_Trueprop (ccp $ cp_type $ at_type $ at_type'); val proof = fn _ => EVERY [simp_tac simp_s 1, rtac allI 1, rtac allI 1, rtac allI 1, rtac cp1 1]; - in - PureThy.add_thms [((name, Goal.prove_global thy' [] [] statement proof), [])] thy' - end) + in + PureThy.add_thms [((name, Goal.prove_global thy' [] [] statement proof), [])] thy' + end) ak_names_types thy) ak_names_types thy12b; (* proves for every non-trivial -combination a disjointness *) @@ -414,33 +414,33 @@ (* lemma ds__: *) (* dj TYPE() TYPE() *) val (dj_thms, thy12d) = fold_map (fn (ak_name,T) => fn thy => - fold_map (fn (ak_name',T') => fn thy' => + fold_map (fn (ak_name',T') => fn thy' => (if not (ak_name = ak_name') then - let - val ak_name_qu = Sign.full_name thy' ak_name; - val ak_name_qu' = Sign.full_name thy' ak_name'; + let + val ak_name_qu = Sign.full_name thy' ak_name; + val ak_name_qu' = Sign.full_name thy' ak_name'; val i_type1 = Type(ak_name_qu,[]); val i_type2 = Type(ak_name_qu',[]); - val cdj = Const ("Nominal.disjoint", + val cdj = Const ("Nominal.disjoint", (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT); val at_type = Logic.mk_type i_type1; val at_type' = Logic.mk_type i_type2; - val simp_s = HOL_ss addsimps PureThy.get_thmss thy' - [Name "disjoint_def", - Name (ak_name^"_prm_"^ak_name'^"_def"), - Name (ak_name'^"_prm_"^ak_name^"_def")]; + val simp_s = HOL_ss addsimps maps (dynamic_thms thy') + ["disjoint_def", + ak_name ^ "_prm_" ^ ak_name' ^ "_def", + ak_name' ^ "_prm_" ^ ak_name ^ "_def"]; - val name = "dj_"^ak_name^"_"^ak_name'; + val name = "dj_"^ak_name^"_"^ak_name'; val statement = HOLogic.mk_Trueprop (cdj $ at_type $ at_type'); val proof = fn _ => simp_tac simp_s 1; - in - PureThy.add_thms [((name, Goal.prove_global thy' [] [] statement proof), [])] thy' - end + in + PureThy.add_thms [((name, Goal.prove_global thy' [] [] statement proof), [])] thy' + end else ([],thy'))) (* do nothing branch, if ak_name = ak_name' *) - ak_names_types thy) ak_names_types thy12c; + ak_names_types thy) ak_names_types thy12c; (******** pt_ class instances ********) (*=========================================*) @@ -462,11 +462,11 @@ (* every is an instance of pt_; the proof for *) (* ak!=ak' is by definition; the case ak=ak' uses at_pt_inst. *) val thy13 = fold (fn ak_name => fn thy => - fold (fn ak_name' => fn thy' => + fold (fn ak_name' => fn thy' => let val qu_name = Sign.full_name thy' ak_name'; val cls_name = Sign.full_name thy' ("pt_"^ak_name); - val at_inst = PureThy.get_thm thy' (Name ("at_"^ak_name'^"_inst")); + val at_inst = dynamic_thm thy' ("at_" ^ ak_name' ^ "_inst"); val proof1 = EVERY [Class.intro_classes_tac [], rtac ((at_inst RS at_pt_inst) RS pt1) 1, @@ -474,7 +474,7 @@ rtac ((at_inst RS at_pt_inst) RS pt3) 1, atac 1]; val simp_s = HOL_basic_ss addsimps - PureThy.get_thmss thy' [Name (ak_name^"_prm_"^ak_name'^"_def")]; + maps (dynamic_thms thy') [ak_name ^ "_prm_" ^ ak_name' ^ "_def"]; val proof2 = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)]; in @@ -496,8 +496,8 @@ val thy18 = fold (fn ak_name => fn thy => let val cls_name = Sign.full_name thy ("pt_"^ak_name); - val at_thm = PureThy.get_thm thy (Name ("at_"^ak_name^"_inst")); - val pt_inst = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst")); + val at_thm = dynamic_thm thy ("at_"^ak_name^"_inst"); + val pt_inst = dynamic_thm thy ("pt_"^ak_name^"_inst"); fun pt_proof thm = EVERY [Class.intro_classes_tac [], @@ -546,11 +546,11 @@ val proof = (if ak_name = ak_name' then - let val at_thm = PureThy.get_thm thy' (Name ("at_"^ak_name^"_inst")); + let val at_thm = dynamic_thm thy' ("at_"^ak_name^"_inst"); in EVERY [Class.intro_classes_tac [], rtac ((at_thm RS fs_at_inst) RS fs1) 1] end else - let val dj_inst = PureThy.get_thm thy' (Name ("dj_"^ak_name'^"_"^ak_name)); + let val dj_inst = dynamic_thm thy' ("dj_"^ak_name'^"_"^ak_name); val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, finite_emptyI]; in EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1] end) in @@ -568,7 +568,7 @@ val thy24 = fold (fn ak_name => fn thy => let val cls_name = Sign.full_name thy ("fs_"^ak_name); - val fs_inst = PureThy.get_thm thy (Name ("fs_"^ak_name^"_inst")); + val fs_inst = dynamic_thm thy ("fs_"^ak_name^"_inst"); fun fs_proof thm = EVERY [Class.intro_classes_tac [], rtac (thm RS fs1) 1]; val fs_thm_unit = fs_unit_inst; @@ -613,20 +613,20 @@ val proof = (if (ak_name'=ak_name'') then (let - val pt_inst = PureThy.get_thm thy'' (Name ("pt_"^ak_name''^"_inst")); - val at_inst = PureThy.get_thm thy'' (Name ("at_"^ak_name''^"_inst")); + val pt_inst = dynamic_thm thy'' ("pt_"^ak_name''^"_inst"); + val at_inst = dynamic_thm thy'' ("at_"^ak_name''^"_inst"); in - EVERY [Class.intro_classes_tac [], + EVERY [Class.intro_classes_tac [], rtac (at_inst RS (pt_inst RS pt_perm_compose)) 1] end) - else - (let - val dj_inst = PureThy.get_thm thy'' (Name ("dj_"^ak_name''^"_"^ak_name')); - val simp_s = HOL_basic_ss addsimps + else + (let + val dj_inst = dynamic_thm thy'' ("dj_"^ak_name''^"_"^ak_name'); + val simp_s = HOL_basic_ss addsimps ((dj_inst RS dj_pp_forget):: - (PureThy.get_thmss thy'' - [Name (ak_name' ^"_prm_"^ak_name^"_def"), - Name (ak_name''^"_prm_"^ak_name^"_def")])); + (maps (dynamic_thms thy'') + [ak_name' ^"_prm_"^ak_name^"_def", + ak_name''^"_prm_"^ak_name^"_def"])); in EVERY [Class.intro_classes_tac [], simp_tac simp_s 1] end)) @@ -644,15 +644,15 @@ (* sets *) (* are instances of cp__ for every /-combination *) val thy26 = fold (fn ak_name => fn thy => - fold (fn ak_name' => fn thy' => + fold (fn ak_name' => fn thy' => let val cls_name = Sign.full_name thy' ("cp_"^ak_name^"_"^ak_name'); - val cp_inst = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"_inst")); - val pt_inst = PureThy.get_thm thy' (Name ("pt_"^ak_name^"_inst")); - val at_inst = PureThy.get_thm thy' (Name ("at_"^ak_name^"_inst")); + val cp_inst = dynamic_thm thy' ("cp_"^ak_name^"_"^ak_name'^"_inst"); + val pt_inst = dynamic_thm thy' ("pt_"^ak_name^"_inst"); + val at_inst = dynamic_thm thy' ("at_"^ak_name^"_inst"); fun cp_proof thm = EVERY [Class.intro_classes_tac [],rtac (thm RS cp1) 1]; - + val cp_thm_unit = cp_unit_inst; val cp_thm_prod = cp_inst RS (cp_inst RS cp_prod_inst); val cp_thm_list = cp_inst RS cp_list_inst; @@ -663,7 +663,7 @@ in thy' |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit) - |> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod) + |> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod) |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list) |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun) |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn) @@ -677,36 +677,36 @@ (* which renders the proofs to be simple "simp_all"-proofs. *) val thy32 = let - fun discrete_pt_inst discrete_ty defn = - fold (fn ak_name => fn thy => - let - val qu_class = Sign.full_name thy ("pt_"^ak_name); - val simp_s = HOL_basic_ss addsimps [defn]; + fun discrete_pt_inst discrete_ty defn = + fold (fn ak_name => fn thy => + let + val qu_class = Sign.full_name thy ("pt_"^ak_name); + val simp_s = HOL_basic_ss addsimps [defn]; val proof = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)]; in - AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy + AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy end) ak_names; fun discrete_fs_inst discrete_ty defn = - fold (fn ak_name => fn thy => - let - val qu_class = Sign.full_name thy ("fs_"^ak_name); - val supp_def = @{thm "Nominal.supp_def"}; + fold (fn ak_name => fn thy => + let + val qu_class = Sign.full_name thy ("fs_"^ak_name); + val supp_def = @{thm "Nominal.supp_def"}; val simp_s = HOL_ss addsimps [supp_def,Collect_const,finite_emptyI,defn]; val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1]; in - AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy + AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy end) ak_names; fun discrete_cp_inst discrete_ty defn = - fold (fn ak_name' => (fold (fn ak_name => fn thy => - let - val qu_class = Sign.full_name thy ("cp_"^ak_name^"_"^ak_name'); - val supp_def = @{thm "Nominal.supp_def"}; + fold (fn ak_name' => (fold (fn ak_name => fn thy => + let + val qu_class = Sign.full_name thy ("cp_"^ak_name^"_"^ak_name'); + val supp_def = @{thm "Nominal.supp_def"}; val simp_s = HOL_ss addsimps [defn]; val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1]; in - AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy + AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy end) ak_names)) ak_names; in @@ -771,7 +771,7 @@ val at_exists_fresh = @{thm "Nominal.at_exists_fresh"}; val at_exists_fresh' = @{thm "Nominal.at_exists_fresh'"}; val fresh_perm_app_ineq = @{thm "Nominal.pt_fresh_perm_app_ineq"}; - val fresh_perm_app = @{thm "Nominal.pt_fresh_perm_app"}; + val fresh_perm_app = @{thm "Nominal.pt_fresh_perm_app"}; val fresh_aux = @{thm "Nominal.pt_fresh_aux"}; val pt_perm_supp_ineq = @{thm "Nominal.pt_perm_supp_ineq"}; val pt_perm_supp = @{thm "Nominal.pt_perm_supp"}; @@ -804,58 +804,58 @@ (* list of all at_inst-theorems *) - val ats = map (fn ak => PureThy.get_thm thy32 (Name ("at_"^ak^"_inst"))) ak_names + val ats = map (fn ak => dynamic_thm thy32 ("at_"^ak^"_inst")) ak_names (* list of all pt_inst-theorems *) - val pts = map (fn ak => PureThy.get_thm thy32 (Name ("pt_"^ak^"_inst"))) ak_names + val pts = map (fn ak => dynamic_thm thy32 ("pt_"^ak^"_inst")) ak_names (* list of all cp_inst-theorems as a collection of lists*) val cps = - let fun cps_fun ak1 ak2 = PureThy.get_thm thy32 (Name ("cp_"^ak1^"_"^ak2^"_inst")) - in map (fn aki => (map (cps_fun aki) ak_names)) ak_names end; + let fun cps_fun ak1 ak2 = dynamic_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst") + in map (fn aki => (map (cps_fun aki) ak_names)) ak_names end; (* list of all cp_inst-theorems that have different atom types *) val cps' = - let fun cps'_fun ak1 ak2 = - if ak1=ak2 then NONE else SOME(PureThy.get_thm thy32 (Name ("cp_"^ak1^"_"^ak2^"_inst"))) - in map (fn aki => (List.mapPartial I (map (cps'_fun aki) ak_names))) ak_names end; + let fun cps'_fun ak1 ak2 = + if ak1=ak2 then NONE else SOME (dynamic_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst")) + in map (fn aki => (List.mapPartial I (map (cps'_fun aki) ak_names))) ak_names end; (* list of all dj_inst-theorems *) val djs = - let fun djs_fun ak1 ak2 = - if ak1=ak2 then NONE else SOME(PureThy.get_thm thy32 (Name ("dj_"^ak2^"_"^ak1))) - in map_filter I (map_product djs_fun ak_names ak_names) end; + let fun djs_fun ak1 ak2 = + if ak1=ak2 then NONE else SOME(dynamic_thm thy32 ("dj_"^ak2^"_"^ak1)) + in map_filter I (map_product djs_fun ak_names ak_names) end; (* list of all fs_inst-theorems *) - val fss = map (fn ak => PureThy.get_thm thy32 (Name ("fs_"^ak^"_inst"))) ak_names + val fss = map (fn ak => dynamic_thm thy32 ("fs_"^ak^"_inst")) ak_names (* list of all at_inst-theorems *) - val fs_axs = map (fn ak => PureThy.get_thm thy32 (Name ("fs_"^ak^"1"))) ak_names + val fs_axs = map (fn ak => dynamic_thm thy32 ("fs_"^ak^"1")) ak_names fun inst_pt thms = maps (fn ti => instR ti pts) thms; fun inst_at thms = maps (fn ti => instR ti ats) thms; fun inst_fs thms = maps (fn ti => instR ti fss) thms; fun inst_cp thms cps = flat (inst_mult thms cps); - fun inst_pt_at thms = inst_zip ats (inst_pt thms); + fun inst_pt_at thms = inst_zip ats (inst_pt thms); fun inst_dj thms = maps (fn ti => instR ti djs) thms; - fun inst_pt_pt_at_cp thms = inst_cp (inst_zip ats (inst_zip pts (inst_pt thms))) cps; + fun inst_pt_pt_at_cp thms = inst_cp (inst_zip ats (inst_zip pts (inst_pt thms))) cps; fun inst_pt_at_fs thms = inst_zip (inst_fs [fs1]) (inst_zip ats (inst_pt thms)); - fun inst_pt_pt_at_cp thms = - let val i_pt_pt_at = inst_zip ats (inst_zip pts (inst_pt thms)); + fun inst_pt_pt_at_cp thms = + let val i_pt_pt_at = inst_zip ats (inst_zip pts (inst_pt thms)); val i_pt_pt_at_cp = inst_cp i_pt_pt_at cps'; - in i_pt_pt_at_cp end; + in i_pt_pt_at_cp end; fun inst_pt_pt_at_cp_dj thms = inst_zip djs (inst_pt_pt_at_cp thms); in thy32 - |> PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])] + |> PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])] ||>> PureThy.add_thmss [(("alpha'", inst_pt_at [abs_fun_eq']),[])] ||>> PureThy.add_thmss [(("alpha_fresh", inst_pt_at [abs_fun_fresh]),[])] ||>> PureThy.add_thmss [(("alpha_fresh'", inst_pt_at [abs_fun_fresh']),[])] ||>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij] @ inst_pt_at [pt_swap_bij']),[])] - ||>> PureThy.add_thmss [(("swap_simps", inst_at at_swap_simps),[])] + ||>> PureThy.add_thmss [(("swap_simps", inst_at at_swap_simps),[])] ||>> PureThy.add_thmss - let val thms1 = inst_pt_at [pt_pi_rev]; - val thms2 = inst_pt_at [pt_rev_pi]; + let val thms1 = inst_pt_at [pt_pi_rev]; + val thms2 = inst_pt_at [pt_rev_pi]; in [(("perm_pi_simp",thms1 @ thms2),[])] end ||>> PureThy.add_thmss [(("perm_fresh_fresh", inst_pt_at [pt_fresh_fresh]),[])] ||>> PureThy.add_thmss [(("perm_bij", inst_pt_at [pt_bij]),[])] ||>> PureThy.add_thmss - let val thms1 = inst_pt_at [pt_perm_compose]; - val thms2 = instR cp1 (Library.flat cps'); + let val thms1 = inst_pt_at [pt_perm_compose]; + val thms2 = instR cp1 (Library.flat cps'); in [(("perm_compose",thms1 @ thms2),[])] end ||>> PureThy.add_thmss [(("perm_compose'",inst_pt_at [pt_perm_compose']),[])] ||>> PureThy.add_thmss [(("perm_app", inst_pt_at [perm_app]),[])] @@ -871,74 +871,74 @@ end ||>> PureThy.add_thmss [(("ex_eqvt", inst_pt_at [ex_eqvt]),[NominalThmDecls.eqvt_force_add])] ||>> PureThy.add_thmss - let val thms1 = inst_at [at_fresh] - val thms2 = inst_dj [at_fresh_ineq] - in [(("fresh_atm", thms1 @ thms2),[])] end + let val thms1 = inst_at [at_fresh] + val thms2 = inst_dj [at_fresh_ineq] + in [(("fresh_atm", thms1 @ thms2),[])] end ||>> PureThy.add_thmss - let val thms1 = filter + let val thms1 = filter (fn th => case prop_of th of _ $ _ $ Var _ => true | _ => false) (List.concat (List.concat perm_defs)) in [(("calc_atm", (inst_at at_calc) @ thms1),[])] end ||>> PureThy.add_thmss - let val thms1 = inst_pt_at [abs_fun_pi] - and thms2 = inst_pt_pt_at_cp [abs_fun_pi_ineq] - in [(("abs_perm", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end + let val thms1 = inst_pt_at [abs_fun_pi] + and thms2 = inst_pt_pt_at_cp [abs_fun_pi_ineq] + in [(("abs_perm", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end ||>> PureThy.add_thmss - let val thms1 = inst_dj [dj_perm_forget] - and thms2 = inst_dj [dj_pp_forget] + let val thms1 = inst_dj [dj_perm_forget] + and thms2 = inst_dj [dj_pp_forget] in [(("perm_dj", thms1 @ thms2),[])] end ||>> PureThy.add_thmss - let val thms1 = inst_pt_at_fs [fresh_iff] + let val thms1 = inst_pt_at_fs [fresh_iff] and thms2 = inst_pt_at [fresh_iff] - and thms3 = inst_pt_pt_at_cp_dj [fresh_iff_ineq] - in [(("abs_fresh", thms1 @ thms2 @ thms3),[])] end - ||>> PureThy.add_thmss - let val thms1 = inst_pt_at [abs_fun_supp] - and thms2 = inst_pt_at_fs [abs_fun_supp] - and thms3 = inst_pt_pt_at_cp_dj [abs_fun_supp_ineq] - in [(("abs_supp", thms1 @ thms2 @ thms3),[])] end + and thms3 = inst_pt_pt_at_cp_dj [fresh_iff_ineq] + in [(("abs_fresh", thms1 @ thms2 @ thms3),[])] end + ||>> PureThy.add_thmss + let val thms1 = inst_pt_at [abs_fun_supp] + and thms2 = inst_pt_at_fs [abs_fun_supp] + and thms3 = inst_pt_pt_at_cp_dj [abs_fun_supp_ineq] + in [(("abs_supp", thms1 @ thms2 @ thms3),[])] end ||>> PureThy.add_thmss - let val thms1 = inst_pt_at [fresh_left] - and thms2 = inst_pt_pt_at_cp [fresh_left_ineq] - in [(("fresh_left", thms1 @ thms2),[])] end + let val thms1 = inst_pt_at [fresh_left] + and thms2 = inst_pt_pt_at_cp [fresh_left_ineq] + in [(("fresh_left", thms1 @ thms2),[])] end ||>> PureThy.add_thmss - let val thms1 = inst_pt_at [fresh_right] - and thms2 = inst_pt_pt_at_cp [fresh_right_ineq] - in [(("fresh_right", thms1 @ thms2),[])] end + let val thms1 = inst_pt_at [fresh_right] + and thms2 = inst_pt_pt_at_cp [fresh_right_ineq] + in [(("fresh_right", thms1 @ thms2),[])] end ||>> PureThy.add_thmss - let val thms1 = inst_pt_at [fresh_bij] - and thms2 = inst_pt_pt_at_cp [fresh_bij_ineq] - in [(("fresh_bij", thms1 @ thms2),[])] end + let val thms1 = inst_pt_at [fresh_bij] + and thms2 = inst_pt_pt_at_cp [fresh_bij_ineq] + in [(("fresh_bij", thms1 @ thms2),[])] end ||>> PureThy.add_thmss - let val thms1 = inst_pt_at [fresh_eqvt] + let val thms1 = inst_pt_at [fresh_eqvt] and thms2 = inst_pt_pt_at_cp_dj [fresh_eqvt_ineq] - in [(("fresh_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end + in [(("fresh_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end ||>> PureThy.add_thmss - let val thms1 = inst_pt_at [in_eqvt] - in [(("in_eqvt", thms1),[NominalThmDecls.eqvt_add])] end - ||>> PureThy.add_thmss - let val thms1 = inst_pt_at [eq_eqvt] - in [(("eq_eqvt", thms1),[NominalThmDecls.eqvt_add])] end - ||>> PureThy.add_thmss - let val thms1 = inst_pt_at [set_diff_eqvt] - in [(("set_diff_eqvt", thms1),[NominalThmDecls.eqvt_add])] end + let val thms1 = inst_pt_at [in_eqvt] + in [(("in_eqvt", thms1),[NominalThmDecls.eqvt_add])] end + ||>> PureThy.add_thmss + let val thms1 = inst_pt_at [eq_eqvt] + in [(("eq_eqvt", thms1),[NominalThmDecls.eqvt_add])] end ||>> PureThy.add_thmss - let val thms1 = inst_pt_at [subseteq_eqvt] - in [(("subseteq_eqvt", thms1),[NominalThmDecls.eqvt_add])] end + let val thms1 = inst_pt_at [set_diff_eqvt] + in [(("set_diff_eqvt", thms1),[NominalThmDecls.eqvt_add])] end + ||>> PureThy.add_thmss + let val thms1 = inst_pt_at [subseteq_eqvt] + in [(("subseteq_eqvt", thms1),[NominalThmDecls.eqvt_add])] end ||>> PureThy.add_thmss - let val thms1 = inst_pt_at [fresh_aux] - and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq] - in [(("fresh_aux", thms1 @ thms2),[])] end + let val thms1 = inst_pt_at [fresh_aux] + and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq] + in [(("fresh_aux", thms1 @ thms2),[])] end ||>> PureThy.add_thmss - let val thms1 = inst_pt_at [fresh_perm_app] - and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq] - in [(("fresh_perm_app", thms1 @ thms2),[])] end + let val thms1 = inst_pt_at [fresh_perm_app] + and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq] + in [(("fresh_perm_app", thms1 @ thms2),[])] end ||>> PureThy.add_thmss - let val thms1 = inst_pt_at [pt_perm_supp] - and thms2 = inst_pt_pt_at_cp [pt_perm_supp_ineq] - in [(("supp_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end + let val thms1 = inst_pt_at [pt_perm_supp] + and thms2 = inst_pt_pt_at_cp [pt_perm_supp_ineq] + in [(("supp_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end ||>> PureThy.add_thmss [(("fin_supp",fs_axs),[])] - end; + end; in NominalData.map (fold Symtab.update (full_ak_names ~~ map make_atom_info diff -r a0e2b706ce73 -r 44473c957672 src/HOL/Nominal/nominal_fresh_fun.ML --- a/src/HOL/Nominal/nominal_fresh_fun.ML Wed Mar 19 22:27:57 2008 +0100 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Wed Mar 19 22:28:08 2008 +0100 @@ -56,8 +56,9 @@ fun cut_inst_tac_term' tinst th = res_inst_tac_term' tinst false (Tactic.make_elim_preserve th); -fun get_dyn_thm thy name atom_name = (PureThy.get_thm thy (Name name)) handle _ => - raise ERROR ("The atom type "^atom_name^" is not defined."); +fun get_dyn_thm thy name atom_name = + dynamic_thm thy name handle ERROR _ => + raise ERROR ("The atom type "^atom_name^" is not defined."); (* End of function waiting to be in the library :o) *) @@ -145,8 +146,8 @@ val thy = theory_of_thm thm; val ctx = Context.init_proof thy; val ss = simpset_of thy; - val abs_fresh = PureThy.get_thms thy (Name "abs_fresh"); - val fresh_perm_app = PureThy.get_thms thy (Name "fresh_perm_app"); + val abs_fresh = dynamic_thms thy "abs_fresh"; + val fresh_perm_app = dynamic_thms thy "fresh_perm_app"; val ss' = ss addsimps fresh_prod::abs_fresh; val ss'' = ss' addsimps fresh_perm_app; val x = hd (tl (term_vars (prop_of exI))); diff -r a0e2b706ce73 -r 44473c957672 src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Wed Mar 19 22:27:57 2008 +0100 +++ b/src/HOL/Nominal/nominal_inductive.ML Wed Mar 19 22:28:08 2008 +0100 @@ -273,19 +273,19 @@ (NominalPackage.fresh_const U T $ u $ t)) bvars) (ts ~~ binder_types (fastype_of p)))) prems; - val perm_pi_simp = PureThy.get_thms thy (Name "perm_pi_simp"); - val pt2_atoms = map (fn aT => PureThy.get_thm thy - (Name ("pt_" ^ Sign.base_name (fst (dest_Type aT)) ^ "2"))) atomTs; + val perm_pi_simp = dynamic_thms thy "perm_pi_simp"; + val pt2_atoms = map (fn aT => dynamic_thm thy + ("pt_" ^ Sign.base_name (fst (dest_Type aT)) ^ "2")) atomTs; val eqvt_ss = HOL_basic_ss addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms) addsimprocs [mk_perm_bool_simproc ["Fun.id"]]; - val fresh_bij = PureThy.get_thms thy (Name "fresh_bij"); - val perm_bij = PureThy.get_thms thy (Name "perm_bij"); - val fs_atoms = map (fn aT => PureThy.get_thm thy - (Name ("fs_" ^ Sign.base_name (fst (dest_Type aT)) ^ "1"))) atomTs; - val exists_fresh' = PureThy.get_thms thy (Name "exists_fresh'"); - val fresh_atm = PureThy.get_thms thy (Name "fresh_atm"); - val calc_atm = PureThy.get_thms thy (Name "calc_atm"); - val perm_fresh_fresh = PureThy.get_thms thy (Name "perm_fresh_fresh"); + val fresh_bij = dynamic_thms thy "fresh_bij"; + val perm_bij = dynamic_thms thy "perm_bij"; + val fs_atoms = map (fn aT => dynamic_thm thy + ("fs_" ^ Sign.base_name (fst (dest_Type aT)) ^ "1")) atomTs; + val exists_fresh' = dynamic_thms thy "exists_fresh'"; + val fresh_atm = dynamic_thms thy "fresh_atm"; + val calc_atm = dynamic_thms thy "calc_atm"; + val perm_fresh_fresh = dynamic_thms thy "perm_fresh_fresh"; fun obtain_fresh_name ts T (freshs1, freshs2, ctxt) = let @@ -604,7 +604,7 @@ | xs => error ("No such atoms: " ^ commas xs); atoms) end; - val perm_pi_simp = PureThy.get_thms thy (Name "perm_pi_simp"); + val perm_pi_simp = dynamic_thms thy "perm_pi_simp"; val eqvt_ss = HOL_basic_ss addsimps (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs [mk_perm_bool_simproc names]; diff -r a0e2b706ce73 -r 44473c957672 src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Wed Mar 19 22:27:57 2008 +0100 +++ b/src/HOL/Nominal/nominal_package.ML Wed Mar 19 22:28:08 2008 +0100 @@ -140,8 +140,8 @@ let val a' = Sign.base_name a; val b' = Sign.base_name b; - val cp = PureThy.get_thm thy (Name ("cp_" ^ a' ^ "_" ^ b' ^ "_inst")); - val dj = PureThy.get_thm thy (Name ("dj_" ^ b' ^ "_" ^ a')); + val cp = dynamic_thm thy ("cp_" ^ a' ^ "_" ^ b' ^ "_inst"); + val dj = dynamic_thm thy ("dj_" ^ b' ^ "_" ^ a'); val dj_cp' = [cp, dj] MRS dj_cp; val cert = SOME o cterm_of thy in @@ -309,7 +309,7 @@ val _ = warning ("length new_type_names: " ^ string_of_int (length new_type_names)); val perm_indnames = DatatypeProp.make_tnames (map body_type perm_types); - val perm_fun_def = PureThy.get_thm thy2 (Name "perm_fun_def"); + val perm_fun_def = dynamic_thm thy2 "perm_fun_def"; val unfolded_perm_eq_thms = if length descr = length new_type_names then [] @@ -353,18 +353,17 @@ val _ = warning "perm_append_thms"; (*FIXME: these should be looked up statically*) - val at_pt_inst = PureThy.get_thm thy2 (Name "at_pt_inst"); - val pt2 = PureThy.get_thm thy2 (Name "pt2"); + val at_pt_inst = dynamic_thm thy2 "at_pt_inst"; + val pt2 = dynamic_thm thy2 "pt2"; val perm_append_thms = List.concat (map (fn a => let val permT = mk_permT (Type (a, [])); val pi1 = Free ("pi1", permT); val pi2 = Free ("pi2", permT); - val pt_inst = PureThy.get_thm thy2 (Name ("pt_" ^ Sign.base_name a ^ "_inst")); + val pt_inst = dynamic_thm thy2 ("pt_" ^ Sign.base_name a ^ "_inst"); val pt2' = pt_inst RS pt2; - val pt2_ax = PureThy.get_thm thy2 - (Name (NameSpace.map_base (fn s => "pt_" ^ s ^ "2") a)); + val pt2_ax = dynamic_thm thy2 (NameSpace.map_base (fn s => "pt_" ^ s ^ "2") a); in List.take (map standard (split_conj_thm (Goal.prove_global thy2 [] [] (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj @@ -386,8 +385,8 @@ val _ = warning "perm_eq_thms"; - val pt3 = PureThy.get_thm thy2 (Name "pt3"); - val pt3_rev = PureThy.get_thm thy2 (Name "pt3_rev"); + val pt3 = dynamic_thm thy2 "pt3"; + val pt3_rev = dynamic_thm thy2 "pt3_rev"; val perm_eq_thms = List.concat (map (fn a => let @@ -395,12 +394,11 @@ val pi1 = Free ("pi1", permT); val pi2 = Free ("pi2", permT); (*FIXME: not robust - better access these theorems using NominalData?*) - val at_inst = PureThy.get_thm thy2 (Name ("at_" ^ Sign.base_name a ^ "_inst")); - val pt_inst = PureThy.get_thm thy2 (Name ("pt_" ^ Sign.base_name a ^ "_inst")); + val at_inst = dynamic_thm thy2 ("at_" ^ Sign.base_name a ^ "_inst"); + val pt_inst = dynamic_thm thy2 ("pt_" ^ Sign.base_name a ^ "_inst"); val pt3' = pt_inst RS pt3; val pt3_rev' = at_inst RS (pt_inst RS pt3_rev); - val pt3_ax = PureThy.get_thm thy2 - (Name (NameSpace.map_base (fn s => "pt_" ^ s ^ "3") a)); + val pt3_ax = dynamic_thm thy2 (NameSpace.map_base (fn s => "pt_" ^ s ^ "3") a); in List.take (map standard (split_conj_thm (Goal.prove_global thy2 [] [] (Logic.mk_implies (HOLogic.mk_Trueprop (Const ("Nominal.prm_eq", @@ -421,11 +419,11 @@ (**** prove pi1 \ (pi2 \ t) = (pi1 \ pi2) \ (pi1 \ t) ****) - val cp1 = PureThy.get_thm thy2 (Name "cp1"); - val dj_cp = PureThy.get_thm thy2 (Name "dj_cp"); - val pt_perm_compose = PureThy.get_thm thy2 (Name "pt_perm_compose"); - val pt_perm_compose_rev = PureThy.get_thm thy2 (Name "pt_perm_compose_rev"); - val dj_perm_perm_forget = PureThy.get_thm thy2 (Name "dj_perm_perm_forget"); + val cp1 = dynamic_thm thy2 "cp1"; + val dj_cp = dynamic_thm thy2 "dj_cp"; + val pt_perm_compose = dynamic_thm thy2 "pt_perm_compose"; + val pt_perm_compose_rev = dynamic_thm thy2 "pt_perm_compose_rev"; + val dj_perm_perm_forget = dynamic_thm thy2 "dj_perm_perm_forget"; fun composition_instance name1 name2 thy = let @@ -437,16 +435,15 @@ val augment = map_type_tfree (fn (x, S) => TFree (x, cp_class :: S)); val Ts = map (augment o body_type) perm_types; - val cp_inst = PureThy.get_thm thy - (Name ("cp_" ^ name1' ^ "_" ^ name2' ^ "_inst")); + val cp_inst = dynamic_thm thy ("cp_" ^ name1' ^ "_" ^ name2' ^ "_inst"); val simps = simpset_of thy addsimps (perm_fun_def :: (if name1 <> name2 then - let val dj = PureThy.get_thm thy (Name ("dj_" ^ name2' ^ "_" ^ name1')) + let val dj = dynamic_thm thy ("dj_" ^ name2' ^ "_" ^ name1') in [dj RS (cp_inst RS dj_cp), dj RS dj_perm_perm_forget] end else let - val at_inst = PureThy.get_thm thy (Name ("at_" ^ name1' ^ "_inst")); - val pt_inst = PureThy.get_thm thy (Name ("pt_" ^ name1' ^ "_inst")) + val at_inst = dynamic_thm thy ("at_" ^ name1' ^ "_inst"); + val pt_inst = dynamic_thm thy ("pt_" ^ name1' ^ "_inst"); in [cp_inst RS cp1 RS sym, at_inst RS (pt_inst RS pt_perm_compose) RS sym, @@ -574,7 +571,7 @@ val _ = warning "proving closure under permutation..."; - val abs_perm = PureThy.get_thms thy4 (Name "abs_perm"); + val abs_perm = dynamic_thms thy4 "abs_perm"; val perm_indnames' = List.mapPartial (fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x) @@ -659,8 +656,8 @@ asm_full_simp_tac (simpset_of thy addsimps [Rep_inverse]) 1, asm_full_simp_tac (simpset_of thy addsimps [Rep RS perm_closed RS Abs_inverse]) 1, - asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy - (Name ("pt_" ^ Sign.base_name atom ^ "3"))]) 1]) thy) + asm_full_simp_tac (HOL_basic_ss addsimps [dynamic_thm thy + ("pt_" ^ Sign.base_name atom ^ "3")]) 1]) thy) (Abs_inverse_thms ~~ Rep_inverse_thms ~~ Rep_thms ~~ perm_defs ~~ new_type_names ~~ tyvars ~~ perm_closed_thms); @@ -673,7 +670,7 @@ let val name = "cp_" ^ Sign.base_name atom1 ^ "_" ^ Sign.base_name atom2; val class = Sign.intern_class thy name; - val cp1' = PureThy.get_thm thy (Name (name ^ "_inst")) RS cp1 + val cp1' = dynamic_thm thy (name ^ "_inst") RS cp1 in fold (fn ((((((Abs_inverse, Rep), perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy => AxClass.prove_arity @@ -923,8 +920,8 @@ (** prove injectivity of constructors **) val rep_inject_thms' = map (fn th => th RS sym) rep_inject_thms; - val alpha = PureThy.get_thms thy8 (Name "alpha"); - val abs_fresh = PureThy.get_thms thy8 (Name "abs_fresh"); + val alpha = dynamic_thms thy8 "alpha"; + val abs_fresh = dynamic_thms thy8 "abs_fresh"; val inject_thms = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) => let val T = nth_dtyp' i @@ -1069,8 +1066,8 @@ val indnames = DatatypeProp.make_tnames recTs; - val abs_supp = PureThy.get_thms thy8 (Name "abs_supp"); - val supp_atm = PureThy.get_thms thy8 (Name "supp_atm"); + val abs_supp = dynamic_thms thy8 "abs_supp"; + val supp_atm = dynamic_thms thy8 "supp_atm"; val finite_supp_thms = map (fn atom => let val atomT = Type (atom, []) @@ -1083,7 +1080,7 @@ (fn _ => indtac dt_induct indnames 1 THEN ALLGOALS (asm_full_simp_tac (simpset_of thy8 addsimps (abs_supp @ supp_atm @ - PureThy.get_thms thy8 (Name ("fs_" ^ Sign.base_name atom ^ "1")) @ + dynamic_thms thy8 ("fs_" ^ Sign.base_name atom ^ "1") @ List.concat supp_thms))))), length new_type_names)) end) atoms; @@ -1210,23 +1207,23 @@ (descr'' ~~ recTs ~~ tnames))); val fin_set_supp = map (fn Type (s, _) => - PureThy.get_thm thy9 (Name ("at_" ^ Sign.base_name s ^ "_inst")) RS + dynamic_thm thy9 ("at_" ^ Sign.base_name s ^ "_inst") RS at_fin_set_supp) dt_atomTs; val fin_set_fresh = map (fn Type (s, _) => - PureThy.get_thm thy9 (Name ("at_" ^ Sign.base_name s ^ "_inst")) RS + dynamic_thm thy9 ("at_" ^ Sign.base_name s ^ "_inst") RS at_fin_set_fresh) dt_atomTs; val pt1_atoms = map (fn Type (s, _) => - PureThy.get_thm thy9 (Name ("pt_" ^ Sign.base_name s ^ "1"))) dt_atomTs; + dynamic_thm thy9 ("pt_" ^ Sign.base_name s ^ "1")) dt_atomTs; val pt2_atoms = map (fn Type (s, _) => - PureThy.get_thm thy9 (Name ("pt_" ^ Sign.base_name s ^ "2")) RS sym) dt_atomTs; - val exists_fresh' = PureThy.get_thms thy9 (Name "exists_fresh'"); - val fs_atoms = PureThy.get_thms thy9 (Name "fin_supp"); - val abs_supp = PureThy.get_thms thy9 (Name "abs_supp"); - val perm_fresh_fresh = PureThy.get_thms thy9 (Name "perm_fresh_fresh"); - val calc_atm = PureThy.get_thms thy9 (Name "calc_atm"); - val fresh_atm = PureThy.get_thms thy9 (Name "fresh_atm"); - val fresh_left = PureThy.get_thms thy9 (Name "fresh_left"); - val perm_swap = PureThy.get_thms thy9 (Name "perm_swap"); + dynamic_thm thy9 ("pt_" ^ Sign.base_name s ^ "2") RS sym) dt_atomTs; + val exists_fresh' = dynamic_thms thy9 "exists_fresh'"; + val fs_atoms = dynamic_thms thy9 "fin_supp"; + val abs_supp = dynamic_thms thy9 "abs_supp"; + val perm_fresh_fresh = dynamic_thms thy9 "perm_fresh_fresh"; + val calc_atm = dynamic_thms thy9 "calc_atm"; + val fresh_atm = dynamic_thms thy9 "fresh_atm"; + val fresh_left = dynamic_thms thy9 "fresh_left"; + val perm_swap = dynamic_thms thy9 "perm_swap"; fun obtain_fresh_name' ths ts T (freshs1, freshs2, ctxt) = let @@ -1499,8 +1496,8 @@ (** equivariance **) - val fresh_bij = PureThy.get_thms thy11 (Name "fresh_bij"); - val perm_bij = PureThy.get_thms thy11 (Name "perm_bij"); + val fresh_bij = dynamic_thms thy11 "fresh_bij"; + val perm_bij = dynamic_thms thy11 "perm_bij"; val (rec_equiv_thms, rec_equiv_thms') = ListPair.unzip (map (fn aT => let @@ -1538,7 +1535,7 @@ val rec_fin_supp_thms = map (fn aT => let val name = Sign.base_name (fst (dest_Type aT)); - val fs_name = PureThy.get_thm thy11 (Name ("fs_" ^ name ^ "1")); + val fs_name = dynamic_thm thy11 ("fs_" ^ name ^ "1"); val aset = HOLogic.mk_setT aT; val finite = Const ("Finite_Set.finite", aset --> HOLogic.boolT); val fins = map (fn (f, T) => HOLogic.mk_Trueprop @@ -1571,7 +1568,7 @@ val rec_fresh_thms = map (fn ((aT, eqvt_ths), finite_prems) => let val name = Sign.base_name (fst (dest_Type aT)); - val fs_name = PureThy.get_thm thy11 (Name ("fs_" ^ name ^ "1")); + val fs_name = dynamic_thm thy11 ("fs_" ^ name ^ "1"); val a = Free ("a", aT); val freshs = map (fn (f, fT) => HOLogic.mk_Trueprop (fresh_const aT fT $ a $ f)) (rec_fns ~~ rec_fn_Ts) diff -r a0e2b706ce73 -r 44473c957672 src/HOL/Nominal/nominal_thmdecls.ML --- a/src/HOL/Nominal/nominal_thmdecls.ML Wed Mar 19 22:27:57 2008 +0100 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Wed Mar 19 22:28:08 2008 +0100 @@ -10,6 +10,9 @@ respectively the lemma from the data-slot. *) +fun dynamic_thm thy name = PureThy.get_thm thy (Facts.Named (name, NONE)); +fun dynamic_thms thy name = PureThy.get_thms thy (Facts.Named (name, NONE)); + signature NOMINAL_THMDECLS = sig val print_data: Proof.context -> unit @@ -76,8 +79,6 @@ then (EVERY [tac, print_tac ("after "^msg)]) else tac -fun dynamic_thms thy name = PureThy.get_thms thy (Name name) - fun tactic_eqvt ctx orig_thm pi typi = let val mypi = Thm.cterm_of ctx (Var (pi,typi))