54 val full_ak_names = map (Sign.intern_type (sign_of thy1)) ak_names; |
54 val full_ak_names = map (Sign.intern_type (sign_of thy1)) ak_names; |
55 val ak_names_types = ak_names ~~ map (Type o rpair []) full_ak_names; |
55 val ak_names_types = ak_names ~~ map (Type o rpair []) full_ak_names; |
56 |
56 |
57 (* adds for every atom-kind an axiom *) |
57 (* adds for every atom-kind an axiom *) |
58 (* <ak>_infinite: infinite (UNIV::<ak_type> set) *) |
58 (* <ak>_infinite: infinite (UNIV::<ak_type> set) *) |
59 val (thy2,inf_axs) = PureThy.add_axioms_i (map (fn (ak_name, T) => |
59 val (inf_axs,thy2) = PureThy.add_axioms_i (map (fn (ak_name, T) => |
60 let |
60 let |
61 val name = ak_name ^ "_infinite" |
61 val name = ak_name ^ "_infinite" |
62 val axiom = HOLogic.mk_Trueprop (HOLogic.mk_not |
62 val axiom = HOLogic.mk_Trueprop (HOLogic.mk_not |
63 (HOLogic.mk_mem (HOLogic.mk_UNIV T, |
63 (HOLogic.mk_mem (HOLogic.mk_UNIV T, |
64 Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT T))))) |
64 Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT T))))) |
147 end) ak_names_types thy) ak_names_types thy4; |
147 end) ak_names_types thy) ak_names_types thy4; |
148 |
148 |
149 (* proves that every atom-kind is an instance of at *) |
149 (* proves that every atom-kind is an instance of at *) |
150 (* lemma at_<ak>_inst: *) |
150 (* lemma at_<ak>_inst: *) |
151 (* at TYPE(<ak>) *) |
151 (* at TYPE(<ak>) *) |
152 val (thy6, prm_cons_thms) = |
152 val (prm_cons_thms,thy6) = |
153 thy5 |> PureThy.add_thms (map (fn (ak_name, T) => |
153 thy5 |> PureThy.add_thms (map (fn (ak_name, T) => |
154 let |
154 let |
155 val ak_name_qu = Sign.full_name (sign_of thy5) (ak_name); |
155 val ak_name_qu = Sign.full_name (sign_of thy5) (ak_name); |
156 val i_type = Type(ak_name_qu,[]); |
156 val i_type = Type(ak_name_qu,[]); |
157 val cat = Const ("nominal.at",(Term.itselfT i_type) --> HOLogic.boolT); |
157 val cat = Const ("nominal.at",(Term.itselfT i_type) --> HOLogic.boolT); |
208 |
208 |
209 (* proves that every pt_<ak>-type together with <ak>-type *) |
209 (* proves that every pt_<ak>-type together with <ak>-type *) |
210 (* instance of pt *) |
210 (* instance of pt *) |
211 (* lemma pt_<ak>_inst: *) |
211 (* lemma pt_<ak>_inst: *) |
212 (* pt TYPE('x::pt_<ak>) TYPE(<ak>) *) |
212 (* pt TYPE('x::pt_<ak>) TYPE(<ak>) *) |
213 val (thy8, prm_inst_thms) = |
213 val (prm_inst_thms,thy8) = |
214 thy7 |> PureThy.add_thms (map (fn (ak_name, T) => |
214 thy7 |> PureThy.add_thms (map (fn (ak_name, T) => |
215 let |
215 let |
216 val ak_name_qu = Sign.full_name (sign_of thy7) (ak_name); |
216 val ak_name_qu = Sign.full_name (sign_of thy7) (ak_name); |
217 val pt_name_qu = Sign.full_name (sign_of thy7) ("pt_"^ak_name); |
217 val pt_name_qu = Sign.full_name (sign_of thy7) ("pt_"^ak_name); |
218 val i_type1 = TFree("'x",[pt_name_qu]); |
218 val i_type1 = TFree("'x",[pt_name_qu]); |
254 |
254 |
255 (* proves that every fs_<ak>-type together with <ak>-type *) |
255 (* proves that every fs_<ak>-type together with <ak>-type *) |
256 (* instance of fs-type *) |
256 (* instance of fs-type *) |
257 (* lemma abst_<ak>_inst: *) |
257 (* lemma abst_<ak>_inst: *) |
258 (* fs TYPE('x::pt_<ak>) TYPE (<ak>) *) |
258 (* fs TYPE('x::pt_<ak>) TYPE (<ak>) *) |
259 val (thy12, fs_inst_thms) = |
259 val (fs_inst_thms,thy12) = |
260 thy11 |> PureThy.add_thms (map (fn (ak_name, T) => |
260 thy11 |> PureThy.add_thms (map (fn (ak_name, T) => |
261 let |
261 let |
262 val ak_name_qu = Sign.full_name (sign_of thy11) (ak_name); |
262 val ak_name_qu = Sign.full_name (sign_of thy11) (ak_name); |
263 val fs_name_qu = Sign.full_name (sign_of thy11) ("fs_"^ak_name); |
263 val fs_name_qu = Sign.full_name (sign_of thy11) ("fs_"^ak_name); |
264 val i_type1 = TFree("'x",[fs_name_qu]); |
264 val i_type1 = TFree("'x",[fs_name_qu]); |
303 (thy, ak_names_types)) (thy12, ak_names_types) |
303 (thy, ak_names_types)) (thy12, ak_names_types) |
304 |
304 |
305 (* proves for every <ak>-combination a cp_<ak1>_<ak2>_inst theorem; *) |
305 (* proves for every <ak>-combination a cp_<ak1>_<ak2>_inst theorem; *) |
306 (* lemma cp_<ak1>_<ak2>_inst: *) |
306 (* lemma cp_<ak1>_<ak2>_inst: *) |
307 (* cp TYPE('a::cp_<ak1>_<ak2>) TYPE(<ak1>) TYPE(<ak2>) *) |
307 (* cp TYPE('a::cp_<ak1>_<ak2>) TYPE(<ak1>) TYPE(<ak2>) *) |
308 val (thy12c, cp_thms) = foldl_map (fn (thy, (ak_name, T)) => |
308 val (cp_thms,thy12c) = fold_map (fn (ak_name, T) => fn thy => |
309 foldl_map (fn (thy', (ak_name', T')) => |
309 fold_map (fn (ak_name', T') => fn thy' => |
310 let |
310 let |
311 val ak_name_qu = Sign.full_name (sign_of thy') (ak_name); |
311 val ak_name_qu = Sign.full_name (sign_of thy') (ak_name); |
312 val ak_name_qu' = Sign.full_name (sign_of thy') (ak_name'); |
312 val ak_name_qu' = Sign.full_name (sign_of thy') (ak_name'); |
313 val cp_name_qu = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name'); |
313 val cp_name_qu = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name'); |
314 val i_type0 = TFree("'a",[cp_name_qu]); |
314 val i_type0 = TFree("'a",[cp_name_qu]); |
326 val name = "cp_"^ak_name^ "_"^ak_name'^"_inst"; |
326 val name = "cp_"^ak_name^ "_"^ak_name'^"_inst"; |
327 val statement = HOLogic.mk_Trueprop (ccp $ cp_type $ at_type $ at_type'); |
327 val statement = HOLogic.mk_Trueprop (ccp $ cp_type $ at_type $ at_type'); |
328 |
328 |
329 val proof = fn _ => EVERY [auto_tac (claset(),simp_s), rtac cp1 1]; |
329 val proof = fn _ => EVERY [auto_tac (claset(),simp_s), rtac cp1 1]; |
330 in |
330 in |
331 thy' |> PureThy.add_thms |
331 PureThy.add_thms [((name, standard (Goal.prove thy' [] [] statement proof)), [])] thy' |
332 [((name, standard (Goal.prove thy' [] [] statement proof)), [])] |
|
333 end) |
332 end) |
334 (thy, ak_names_types)) (thy12b, ak_names_types); |
333 ak_names_types thy) ak_names_types thy12b; |
335 |
334 |
336 (* proves for every non-trivial <ak>-combination a disjointness *) |
335 (* proves for every non-trivial <ak>-combination a disjointness *) |
337 (* theorem; i.e. <ak1> != <ak2> *) |
336 (* theorem; i.e. <ak1> != <ak2> *) |
338 (* lemma ds_<ak1>_<ak2>: *) |
337 (* lemma ds_<ak1>_<ak2>: *) |
339 (* dj TYPE(<ak1>) TYPE(<ak2>) *) |
338 (* dj TYPE(<ak1>) TYPE(<ak2>) *) |
340 val (thy12d, dj_thms) = foldl_map (fn (thy, (ak_name, T)) => |
339 val (dj_thms, thy12d) = fold_map (fn (ak_name,T) => fn thy => |
341 foldl_map (fn (thy', (ak_name', T')) => |
340 fold_map (fn (ak_name',T') => fn thy' => |
342 (if not (ak_name = ak_name') |
341 (if not (ak_name = ak_name') |
343 then |
342 then |
344 let |
343 let |
345 val ak_name_qu = Sign.full_name (sign_of thy') (ak_name); |
344 val ak_name_qu = Sign.full_name (sign_of thy') (ak_name); |
346 val ak_name_qu' = Sign.full_name (sign_of thy') (ak_name'); |
345 val ak_name_qu' = Sign.full_name (sign_of thy') (ak_name'); |
358 val name = "dj_"^ak_name^"_"^ak_name'; |
357 val name = "dj_"^ak_name^"_"^ak_name'; |
359 val statement = HOLogic.mk_Trueprop (cdj $ at_type $ at_type'); |
358 val statement = HOLogic.mk_Trueprop (cdj $ at_type $ at_type'); |
360 |
359 |
361 val proof = fn _ => auto_tac (claset(),simp_s); |
360 val proof = fn _ => auto_tac (claset(),simp_s); |
362 in |
361 in |
363 thy' |> PureThy.add_thms |
362 PureThy.add_thms [((name, standard (Goal.prove thy' [] [] statement proof)), [])] thy' |
364 [((name, standard (Goal.prove thy' [] [] statement proof)), []) ] |
|
365 end |
363 end |
366 else |
364 else |
367 (thy',[]))) (* do nothing branch, if ak_name = ak_name' *) |
365 ([],thy'))) (* do nothing branch, if ak_name = ak_name' *) |
368 (thy, ak_names_types)) (thy12c, ak_names_types); |
366 ak_names_types thy) ak_names_types thy12c; |
369 |
367 |
370 (*<<<<<<< pt_<ak> class instances >>>>>>>*) |
368 (*<<<<<<< pt_<ak> class instances >>>>>>>*) |
371 (*=========================================*) |
369 (*=========================================*) |
372 (* some abbreviations for theorems *) |
370 (* some abbreviations for theorems *) |
373 val pt1 = thm "pt1"; |
371 val pt1 = thm "pt1"; |
820 |
818 |
821 (* Now we collect and instantiate some lemmas w.r.t. all atom *) |
819 (* Now we collect and instantiate some lemmas w.r.t. all atom *) |
822 (* types; this allows for example to use abs_perm (which is a *) |
820 (* types; this allows for example to use abs_perm (which is a *) |
823 (* collection of theorems) instead of thm abs_fun_pi with explicit *) |
821 (* collection of theorems) instead of thm abs_fun_pi with explicit *) |
824 (* instantiations. *) |
822 (* instantiations. *) |
825 val (thy33,_) = |
823 val (_,thy33) = |
826 let |
824 let |
827 (* takes a theorem thm and a list of theorems [t1,..,tn] *) |
825 (* takes a theorem thm and a list of theorems [t1,..,tn] *) |
828 (* produces a list of theorems of the form [t1 RS thm,..,tn RS thm] *) |
826 (* produces a list of theorems of the form [t1 RS thm,..,tn RS thm] *) |
829 fun instR thm thms = map (fn ti => ti RS thm) thms; |
827 fun instR thm thms = map (fn ti => ti RS thm) thms; |
830 |
828 |
877 val i_pt_pt_at_cp_dj = inst_zip djs i_pt_pt_at_cp; |
875 val i_pt_pt_at_cp_dj = inst_zip djs i_pt_pt_at_cp; |
878 in i_pt_pt_at_cp_dj end; |
876 in i_pt_pt_at_cp_dj end; |
879 in |
877 in |
880 thy32 |
878 thy32 |
881 |> PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])] |
879 |> PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])] |
882 |>>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij]),[])] |
880 ||>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij]),[])] |
883 |>>> PureThy.add_thmss [(("perm_fresh_fresh", inst_pt_at [pt_fresh_fresh]),[])] |
881 ||>> PureThy.add_thmss [(("perm_fresh_fresh", inst_pt_at [pt_fresh_fresh]),[])] |
884 |>>> PureThy.add_thmss [(("perm_bij", inst_pt_at [pt_bij]),[])] |
882 ||>> PureThy.add_thmss [(("perm_bij", inst_pt_at [pt_bij]),[])] |
885 |>>> PureThy.add_thmss [(("perm_compose", inst_pt_at [pt_perm_compose]),[])] |
883 ||>> PureThy.add_thmss [(("perm_compose", inst_pt_at [pt_perm_compose]),[])] |
886 |>>> PureThy.add_thmss [(("perm_app_eq", inst_pt_at [perm_eq_app]),[])] |
884 ||>> PureThy.add_thmss [(("perm_app_eq", inst_pt_at [perm_eq_app]),[])] |
887 |>>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])] |
885 ||>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])] |
888 |>>> PureThy.add_thmss [(("fresh_atm", inst_at [at_fresh]),[])] |
886 ||>> PureThy.add_thmss [(("fresh_atm", inst_at [at_fresh]),[])] |
889 |>>> PureThy.add_thmss [(("calc_atm", inst_at at_calc),[])] |
887 ||>> PureThy.add_thmss [(("calc_atm", inst_at at_calc),[])] |
890 |>>> PureThy.add_thmss |
888 ||>> PureThy.add_thmss |
891 let val thms1 = inst_pt_at [abs_fun_pi] |
889 let val thms1 = inst_pt_at [abs_fun_pi] |
892 and thms2 = inst_pt_pt_at_cp [abs_fun_pi_ineq] |
890 and thms2 = inst_pt_pt_at_cp [abs_fun_pi_ineq] |
893 in [(("abs_perm", thms1 @ thms2),[])] end |
891 in [(("abs_perm", thms1 @ thms2),[])] end |
894 |>>> PureThy.add_thmss |
892 ||>> PureThy.add_thmss |
895 let val thms1 = inst_dj [dj_perm_forget] |
893 let val thms1 = inst_dj [dj_perm_forget] |
896 and thms2 = inst_dj [dj_pp_forget] |
894 and thms2 = inst_dj [dj_pp_forget] |
897 in [(("perm_dj", thms1 @ thms2),[])] end |
895 in [(("perm_dj", thms1 @ thms2),[])] end |
898 |>>> PureThy.add_thmss |
896 ||>> PureThy.add_thmss |
899 let val thms1 = inst_pt_at_fs [fresh_iff] |
897 let val thms1 = inst_pt_at_fs [fresh_iff] |
900 and thms2 = inst_pt_pt_at_cp_dj [fresh_iff_ineq] |
898 and thms2 = inst_pt_pt_at_cp_dj [fresh_iff_ineq] |
901 in [(("abs_fresh", thms1 @ thms2),[])] end |
899 in [(("abs_fresh", thms1 @ thms2),[])] end |
902 |>>> PureThy.add_thmss |
900 ||>> PureThy.add_thmss |
903 let val thms1 = inst_pt_at [abs_fun_supp] |
901 let val thms1 = inst_pt_at [abs_fun_supp] |
904 and thms2 = inst_pt_at_fs [abs_fun_supp] |
902 and thms2 = inst_pt_at_fs [abs_fun_supp] |
905 and thms3 = inst_pt_pt_at_cp_dj [abs_fun_supp_ineq] |
903 and thms3 = inst_pt_pt_at_cp_dj [abs_fun_supp_ineq] |
906 in [(("abs_supp", thms1 @ thms2 @ thms3),[])] end |
904 in [(("abs_supp", thms1 @ thms2 @ thms3),[])] end |
907 end; |
905 end; |