# HG changeset patch # User urbanc # Date 1130941872 -3600 # Node ID 8b9848d150ba7e9583a3358c8658cc8877d38a1d # Parent d1e47ee130705e63734655104e73ba53e4e31676 - completed the list of thms for supp_atm - cleaned up the way how thms are collected under single names diff -r d1e47ee13070 -r 8b9848d150ba src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Wed Nov 02 15:05:22 2005 +0100 +++ b/src/HOL/Nominal/nominal_package.ML Wed Nov 02 15:31:12 2005 +0100 @@ -49,6 +49,9 @@ let val T = fastype_of x in Const ("List.list.Cons", T --> mk_listT T --> mk_listT T) $ x $ xs end; +(* FIXME: should be a library function *) +fun cprod ([], ys) = [] + | cprod (x :: xs, ys) = map (pair x) ys @ cprod (xs, ys); (* this function sets up all matters related to atom- *) (* kinds; the user specifies a list of atom-kind names *) @@ -771,9 +774,9 @@ val pt_perm_compose = PureThy.get_thm thy32 (Name ("nominal.pt_perm_compose")); val perm_eq_app = PureThy.get_thm thy32 (Name ("nominal.perm_eq_app")); val at_fresh = PureThy.get_thm thy32 (Name ("nominal.at_fresh")); - (*val at_calc = PureThy.get_thms thy32 (Name ("nominal.at_calc"));*) + val at_calc = PureThy.get_thms thy32 (Name ("nominal.at_calc")); val at_supp = PureThy.get_thm thy32 (Name ("nominal.at_supp")); - val dj_supp = PureThy.get_thm thy32 (Name ("nominal.at_supp")); + val dj_supp = PureThy.get_thm thy32 (Name ("nominal.dj_supp")); (* abs_perm collects all lemmas for simplifying a permutation *) (* in front of an abs_fun *) @@ -797,34 +800,51 @@ end; val (thy34,_) = - let - fun inst_pt_at thm ak_name = - let - val at_inst = PureThy.get_thm thy33 (Name ("at_"^ak_name^"_inst")); - val pt_inst = PureThy.get_thm thy33 (Name ("pt_"^ak_name^"_inst")); - in - [pt_inst, at_inst] MRS thm - end - fun inst_at thm ak_name = - let - val at_inst = PureThy.get_thm thy33 (Name ("at_"^ak_name^"_inst")); - in - at_inst RS thm - end + let + (* takes a theorem and a list of theorems *) + (* produces a list of theorems of the form *) + (* [t1 RS thm,..,tn RS thm] where t1..tn in thms *) + fun instantiate thm thms = map (fn ti => ti RS thm) thms; + + (* takes two theorem lists (hopefully of the same length) *) + (* produces a list of theorems of the form *) + (* [t1 RS m1,..,tn RS mn] where t1..tn in thms1 and m1..mn in thms2 *) + fun instantiate_zip thms1 thms2 = + map (fn (t1,t2) => t1 RS t2) (thms1 ~~ thms2); + + (* list of all at_inst-theorems *) + val ats = map (fn ak => PureThy.get_thm thy33 (Name ("at_"^ak^"_inst"))) ak_names + (* list of all pt_inst-theorems *) + val pts = map (fn ak => PureThy.get_thm thy33 (Name ("pt_"^ak^"_inst"))) ak_names + (* list of all cp_inst-theorems *) + val cps = + let fun cps_fun (ak1,ak2) = PureThy.get_thm thy33 (Name ("cp_"^ak1^"_"^ak2^"_inst")) + in map cps_fun (cprod (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 thy33 (Name ("dj_"^ak1^"_"^ak2))) + in List.mapPartial I (map djs_fun (cprod (ak_names,ak_names))) end; + + fun inst_pt thms = Library.flat (map (fn ti => instantiate ti pts) thms); + fun inst_at thms = Library.flat (map (fn ti => instantiate ti ats) thms); + fun inst_pt_at thms = instantiate_zip ats (inst_pt thms); + fun inst_dj thms = Library.flat (map (fn ti => instantiate ti djs) thms); in thy33 - |> PureThy.add_thmss [(("alpha", map (inst_pt_at abs_fun_eq) ak_names),[])] - |>>> PureThy.add_thmss [(("perm_swap", map (inst_pt_at pt_swap_bij) ak_names),[])] - |>>> PureThy.add_thmss [(("perm_fresh_fresh", map (inst_pt_at pt_fresh_fresh) ak_names),[])] - |>>> PureThy.add_thmss [(("perm_bij", map (inst_pt_at pt_bij) ak_names),[])] - |>>> PureThy.add_thmss [(("perm_compose", map (inst_pt_at pt_perm_compose) ak_names),[])] - |>>> PureThy.add_thmss [(("perm_app_eq", map (inst_pt_at perm_eq_app) ak_names),[])] - |>>> PureThy.add_thmss [(("supp_at", map (inst_at at_supp) ak_names),[])] - (*|>>> PureThy.add_thmss [(("fresh_at", map (inst_at at_fresh) ak_names), - [Simplifier.simp_add_global])]*) - (*|>>> PureThy.add_thmss [(("calc_at", map (inst_at at_calc) ak_names), - [Simplifier.simp_add_global])]*) + |> PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])] + |>>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij]),[])] + |>>> 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 [(("perm_compose", inst_pt_at [pt_perm_compose]),[])] + |>>> PureThy.add_thmss [(("perm_app_eq", inst_pt_at [perm_eq_app]),[])] + |>>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])] + |>>> PureThy.add_thmss [(("fresh_atm", inst_at [at_fresh]),[])] + |>>> PureThy.add_thmss [(("calc_atm", inst_at at_calc),[])] + end; (* perm_dj collects all lemmas that forget an permutation *) @@ -1900,7 +1920,7 @@ val indnames = DatatypeProp.make_tnames recTs; val abs_supp = PureThy.get_thms thy8 (Name "abs_supp"); - val supp_at = PureThy.get_thms thy8 (Name "supp_at"); + val supp_atm = PureThy.get_thms thy8 (Name "supp_atm"); val finite_supp_thms = map (fn atom => let val atomT = Type (atom, []) @@ -1912,7 +1932,7 @@ (indnames ~~ recTs)))) (fn _ => indtac dt_induct indnames 1 THEN ALLGOALS (asm_full_simp_tac (simpset_of thy8 addsimps - (abs_supp @ supp_at @ + (abs_supp @ supp_atm @ PureThy.get_thms thy8 (Name ("fs_" ^ Sign.base_name atom ^ "1")) @ List.concat supp_thms))))), length new_type_names))