86 |
86 |
87 fun mk_Cons x xs = |
87 fun mk_Cons x xs = |
88 let val T = fastype_of x |
88 let val T = fastype_of x |
89 in Const ("List.list.Cons", T --> HOLogic.listT T --> HOLogic.listT T) $ x $ xs end; |
89 in Const ("List.list.Cons", T --> HOLogic.listT T --> HOLogic.listT T) $ x $ xs end; |
90 |
90 |
91 fun add_thms_string args = PureThy.add_thms ((map o apfst o apfst) Binding.name args); |
91 fun add_thms_string args = Global_Theory.add_thms ((map o apfst o apfst) Binding.name args); |
92 fun add_thmss_string args = PureThy.add_thmss ((map o apfst o apfst) Binding.name args); |
92 fun add_thmss_string args = Global_Theory.add_thmss ((map o apfst o apfst) Binding.name args); |
93 |
93 |
94 (* this function sets up all matters related to atom- *) |
94 (* this function sets up all matters related to atom- *) |
95 (* kinds; the user specifies a list of atom-kind names *) |
95 (* kinds; the user specifies a list of atom-kind names *) |
96 (* atom_decl <ak1> ... <akn> *) |
96 (* atom_decl <ak1> ... <akn> *) |
97 fun create_nom_typedecls ak_names thy = |
97 fun create_nom_typedecls ak_names thy = |
187 (cswap_akname $ HOLogic.mk_prod (a,b) $ c, |
187 (cswap_akname $ HOLogic.mk_prod (a,b) $ c, |
188 cif $ HOLogic.mk_eq (a,c) $ b $ (cif $ HOLogic.mk_eq (b,c) $ a $ c))) |
188 cif $ HOLogic.mk_eq (a,c) $ b $ (cif $ HOLogic.mk_eq (b,c) $ a $ c))) |
189 val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c) |
189 val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c) |
190 in |
190 in |
191 thy |> Sign.add_consts_i [(Binding.name ("swap_" ^ ak_name), swapT, NoSyn)] |
191 thy |> Sign.add_consts_i [(Binding.name ("swap_" ^ ak_name), swapT, NoSyn)] |
192 |> PureThy.add_defs_unchecked true [((Binding.name name, def2),[])] |
192 |> Global_Theory.add_defs_unchecked true [((Binding.name name, def2),[])] |
193 |> snd |
193 |> snd |
194 |> OldPrimrec.add_primrec_unchecked_i "" [(("", def1),[])] |
194 |> OldPrimrec.add_primrec_unchecked_i "" [(("", def1),[])] |
195 end) ak_names_types thy1; |
195 end) ak_names_types thy1; |
196 |
196 |
197 (* declares a permutation function for every atom-kind acting *) |
197 (* declares a permutation function for every atom-kind acting *) |
242 |
242 |
243 val name = ak_name ^ "_prm_" ^ ak_name' ^ "_def"; |
243 val name = ak_name ^ "_prm_" ^ ak_name' ^ "_def"; |
244 val def = Logic.mk_equals |
244 val def = Logic.mk_equals |
245 (cperm $ pi $ a, if ak_name = ak_name' then cperm_def $ pi $ a else a) |
245 (cperm $ pi $ a, if ak_name = ak_name' then cperm_def $ pi $ a else a) |
246 in |
246 in |
247 PureThy.add_defs_unchecked true [((Binding.name name, def),[])] thy' |
247 Global_Theory.add_defs_unchecked true [((Binding.name name, def),[])] thy' |
248 end) ak_names_types thy) ak_names_types thy4; |
248 end) ak_names_types thy) ak_names_types thy4; |
249 |
249 |
250 (* proves that every atom-kind is an instance of at *) |
250 (* proves that every atom-kind is an instance of at *) |
251 (* lemma at_<ak>_inst: *) |
251 (* lemma at_<ak>_inst: *) |
252 (* at TYPE(<ak>) *) |
252 (* at TYPE(<ak>) *) |
255 let |
255 let |
256 val ak_name_qu = Sign.full_bname thy5 (ak_name); |
256 val ak_name_qu = Sign.full_bname thy5 (ak_name); |
257 val i_type = Type(ak_name_qu,[]); |
257 val i_type = Type(ak_name_qu,[]); |
258 val cat = Const ("Nominal.at",(Term.itselfT i_type) --> HOLogic.boolT); |
258 val cat = Const ("Nominal.at",(Term.itselfT i_type) --> HOLogic.boolT); |
259 val at_type = Logic.mk_type i_type; |
259 val at_type = Logic.mk_type i_type; |
260 val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy5) |
260 val simp_s = HOL_ss addsimps maps (Global_Theory.get_thms thy5) |
261 ["at_def", |
261 ["at_def", |
262 ak_name ^ "_prm_" ^ ak_name ^ "_def", |
262 ak_name ^ "_prm_" ^ ak_name ^ "_def", |
263 ak_name ^ "_prm_" ^ ak_name ^ ".simps", |
263 ak_name ^ "_prm_" ^ ak_name ^ ".simps", |
264 "swap_" ^ ak_name ^ "_def", |
264 "swap_" ^ ak_name ^ "_def", |
265 "swap_" ^ ak_name ^ ".simps", |
265 "swap_" ^ ak_name ^ ".simps", |
319 val i_type1 = TFree("'x",[pt_name_qu]); |
319 val i_type1 = TFree("'x",[pt_name_qu]); |
320 val i_type2 = Type(ak_name_qu,[]); |
320 val i_type2 = Type(ak_name_qu,[]); |
321 val cpt = Const ("Nominal.pt",(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT); |
321 val cpt = Const ("Nominal.pt",(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT); |
322 val pt_type = Logic.mk_type i_type1; |
322 val pt_type = Logic.mk_type i_type1; |
323 val at_type = Logic.mk_type i_type2; |
323 val at_type = Logic.mk_type i_type2; |
324 val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy7) |
324 val simp_s = HOL_ss addsimps maps (Global_Theory.get_thms thy7) |
325 ["pt_def", |
325 ["pt_def", |
326 "pt_" ^ ak_name ^ "1", |
326 "pt_" ^ ak_name ^ "1", |
327 "pt_" ^ ak_name ^ "2", |
327 "pt_" ^ ak_name ^ "2", |
328 "pt_" ^ ak_name ^ "3"]; |
328 "pt_" ^ ak_name ^ "3"]; |
329 |
329 |
367 val i_type2 = Type(ak_name_qu,[]); |
367 val i_type2 = Type(ak_name_qu,[]); |
368 val cfs = Const ("Nominal.fs", |
368 val cfs = Const ("Nominal.fs", |
369 (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT); |
369 (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT); |
370 val fs_type = Logic.mk_type i_type1; |
370 val fs_type = Logic.mk_type i_type1; |
371 val at_type = Logic.mk_type i_type2; |
371 val at_type = Logic.mk_type i_type2; |
372 val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy11) |
372 val simp_s = HOL_ss addsimps maps (Global_Theory.get_thms thy11) |
373 ["fs_def", |
373 ["fs_def", |
374 "fs_" ^ ak_name ^ "1"]; |
374 "fs_" ^ ak_name ^ "1"]; |
375 |
375 |
376 val name = "fs_"^ak_name^ "_inst"; |
376 val name = "fs_"^ak_name^ "_inst"; |
377 val statement = HOLogic.mk_Trueprop (cfs $ fs_type $ at_type); |
377 val statement = HOLogic.mk_Trueprop (cfs $ fs_type $ at_type); |
420 (Term.itselfT i_type0)-->(Term.itselfT i_type1)--> |
420 (Term.itselfT i_type0)-->(Term.itselfT i_type1)--> |
421 (Term.itselfT i_type2)-->HOLogic.boolT); |
421 (Term.itselfT i_type2)-->HOLogic.boolT); |
422 val at_type = Logic.mk_type i_type1; |
422 val at_type = Logic.mk_type i_type1; |
423 val at_type' = Logic.mk_type i_type2; |
423 val at_type' = Logic.mk_type i_type2; |
424 val cp_type = Logic.mk_type i_type0; |
424 val cp_type = Logic.mk_type i_type0; |
425 val simp_s = HOL_basic_ss addsimps maps (PureThy.get_thms thy') ["cp_def"]; |
425 val simp_s = HOL_basic_ss addsimps maps (Global_Theory.get_thms thy') ["cp_def"]; |
426 val cp1 = PureThy.get_thm thy' ("cp_" ^ ak_name ^ "_" ^ ak_name' ^ "1"); |
426 val cp1 = Global_Theory.get_thm thy' ("cp_" ^ ak_name ^ "_" ^ ak_name' ^ "1"); |
427 |
427 |
428 val name = "cp_"^ak_name^ "_"^ak_name'^"_inst"; |
428 val name = "cp_"^ak_name^ "_"^ak_name'^"_inst"; |
429 val statement = HOLogic.mk_Trueprop (ccp $ cp_type $ at_type $ at_type'); |
429 val statement = HOLogic.mk_Trueprop (ccp $ cp_type $ at_type $ at_type'); |
430 |
430 |
431 val proof = fn _ => EVERY [simp_tac simp_s 1, |
431 val proof = fn _ => EVERY [simp_tac simp_s 1, |
452 val i_type2 = Type(ak_name_qu',[]); |
452 val i_type2 = Type(ak_name_qu',[]); |
453 val cdj = Const ("Nominal.disjoint", |
453 val cdj = Const ("Nominal.disjoint", |
454 (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT); |
454 (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT); |
455 val at_type = Logic.mk_type i_type1; |
455 val at_type = Logic.mk_type i_type1; |
456 val at_type' = Logic.mk_type i_type2; |
456 val at_type' = Logic.mk_type i_type2; |
457 val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy') |
457 val simp_s = HOL_ss addsimps maps (Global_Theory.get_thms thy') |
458 ["disjoint_def", |
458 ["disjoint_def", |
459 ak_name ^ "_prm_" ^ ak_name' ^ "_def", |
459 ak_name ^ "_prm_" ^ ak_name' ^ "_def", |
460 ak_name' ^ "_prm_" ^ ak_name ^ "_def"]; |
460 ak_name' ^ "_prm_" ^ ak_name ^ "_def"]; |
461 |
461 |
462 val name = "dj_"^ak_name^"_"^ak_name'; |
462 val name = "dj_"^ak_name^"_"^ak_name'; |
491 val thy13 = fold (fn ak_name => fn thy => |
491 val thy13 = fold (fn ak_name => fn thy => |
492 fold (fn ak_name' => fn thy' => |
492 fold (fn ak_name' => fn thy' => |
493 let |
493 let |
494 val qu_name = Sign.full_bname thy' ak_name'; |
494 val qu_name = Sign.full_bname thy' ak_name'; |
495 val cls_name = Sign.full_bname thy' ("pt_"^ak_name); |
495 val cls_name = Sign.full_bname thy' ("pt_"^ak_name); |
496 val at_inst = PureThy.get_thm thy' ("at_" ^ ak_name' ^ "_inst"); |
496 val at_inst = Global_Theory.get_thm thy' ("at_" ^ ak_name' ^ "_inst"); |
497 |
497 |
498 val proof1 = EVERY [Class.intro_classes_tac [], |
498 val proof1 = EVERY [Class.intro_classes_tac [], |
499 rtac ((at_inst RS at_pt_inst) RS pt1) 1, |
499 rtac ((at_inst RS at_pt_inst) RS pt1) 1, |
500 rtac ((at_inst RS at_pt_inst) RS pt2) 1, |
500 rtac ((at_inst RS at_pt_inst) RS pt2) 1, |
501 rtac ((at_inst RS at_pt_inst) RS pt3) 1, |
501 rtac ((at_inst RS at_pt_inst) RS pt3) 1, |
502 atac 1]; |
502 atac 1]; |
503 val simp_s = HOL_basic_ss addsimps |
503 val simp_s = HOL_basic_ss addsimps |
504 maps (PureThy.get_thms thy') [ak_name ^ "_prm_" ^ ak_name' ^ "_def"]; |
504 maps (Global_Theory.get_thms thy') [ak_name ^ "_prm_" ^ ak_name' ^ "_def"]; |
505 val proof2 = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)]; |
505 val proof2 = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)]; |
506 |
506 |
507 in |
507 in |
508 thy' |
508 thy' |
509 |> AxClass.prove_arity (qu_name,[],[cls_name]) |
509 |> AxClass.prove_arity (qu_name,[],[cls_name]) |
521 (* set(pt_<ak>) *) |
521 (* set(pt_<ak>) *) |
522 (* are instances of pt_<ak> *) |
522 (* are instances of pt_<ak> *) |
523 val thy18 = fold (fn ak_name => fn thy => |
523 val thy18 = fold (fn ak_name => fn thy => |
524 let |
524 let |
525 val cls_name = Sign.full_bname thy ("pt_"^ak_name); |
525 val cls_name = Sign.full_bname thy ("pt_"^ak_name); |
526 val at_thm = PureThy.get_thm thy ("at_"^ak_name^"_inst"); |
526 val at_thm = Global_Theory.get_thm thy ("at_"^ak_name^"_inst"); |
527 val pt_inst = PureThy.get_thm thy ("pt_"^ak_name^"_inst"); |
527 val pt_inst = Global_Theory.get_thm thy ("pt_"^ak_name^"_inst"); |
528 |
528 |
529 fun pt_proof thm = |
529 fun pt_proof thm = |
530 EVERY [Class.intro_classes_tac [], |
530 EVERY [Class.intro_classes_tac [], |
531 rtac (thm RS pt1) 1, rtac (thm RS pt2) 1, rtac (thm RS pt3) 1, atac 1]; |
531 rtac (thm RS pt1) 1, rtac (thm RS pt2) 1, rtac (thm RS pt3) 1, atac 1]; |
532 |
532 |
569 val qu_name = Sign.full_bname thy' ak_name'; |
569 val qu_name = Sign.full_bname thy' ak_name'; |
570 val qu_class = Sign.full_bname thy' ("fs_"^ak_name); |
570 val qu_class = Sign.full_bname thy' ("fs_"^ak_name); |
571 val proof = |
571 val proof = |
572 (if ak_name = ak_name' |
572 (if ak_name = ak_name' |
573 then |
573 then |
574 let val at_thm = PureThy.get_thm thy' ("at_"^ak_name^"_inst"); |
574 let val at_thm = Global_Theory.get_thm thy' ("at_"^ak_name^"_inst"); |
575 in EVERY [Class.intro_classes_tac [], |
575 in EVERY [Class.intro_classes_tac [], |
576 rtac ((at_thm RS fs_at_inst) RS fs1) 1] end |
576 rtac ((at_thm RS fs_at_inst) RS fs1) 1] end |
577 else |
577 else |
578 let val dj_inst = PureThy.get_thm thy' ("dj_"^ak_name'^"_"^ak_name); |
578 let val dj_inst = Global_Theory.get_thm thy' ("dj_"^ak_name'^"_"^ak_name); |
579 val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, finite_emptyI]; |
579 val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, finite_emptyI]; |
580 in EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1] end) |
580 in EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1] end) |
581 in |
581 in |
582 AxClass.prove_arity (qu_name,[],[qu_class]) proof thy' |
582 AxClass.prove_arity (qu_name,[],[qu_class]) proof thy' |
583 end) ak_names thy) ak_names thy18; |
583 end) ak_names thy) ak_names thy18; |
591 (* are instances of fs_<ak> *) |
591 (* are instances of fs_<ak> *) |
592 |
592 |
593 val thy24 = fold (fn ak_name => fn thy => |
593 val thy24 = fold (fn ak_name => fn thy => |
594 let |
594 let |
595 val cls_name = Sign.full_bname thy ("fs_"^ak_name); |
595 val cls_name = Sign.full_bname thy ("fs_"^ak_name); |
596 val fs_inst = PureThy.get_thm thy ("fs_"^ak_name^"_inst"); |
596 val fs_inst = Global_Theory.get_thm thy ("fs_"^ak_name^"_inst"); |
597 fun fs_proof thm = EVERY [Class.intro_classes_tac [], rtac (thm RS fs1) 1]; |
597 fun fs_proof thm = EVERY [Class.intro_classes_tac [], rtac (thm RS fs1) 1]; |
598 |
598 |
599 val fs_thm_unit = fs_unit_inst; |
599 val fs_thm_unit = fs_unit_inst; |
600 val fs_thm_prod = fs_inst RS (fs_inst RS fs_prod_inst); |
600 val fs_thm_prod = fs_inst RS (fs_inst RS fs_prod_inst); |
601 val fs_thm_nprod = fs_inst RS (fs_inst RS fs_nprod_inst); |
601 val fs_thm_nprod = fs_inst RS (fs_inst RS fs_nprod_inst); |
635 val name = Sign.full_bname thy'' ak_name; |
635 val name = Sign.full_bname thy'' ak_name; |
636 val cls_name = Sign.full_bname thy'' ("cp_"^ak_name'^"_"^ak_name''); |
636 val cls_name = Sign.full_bname thy'' ("cp_"^ak_name'^"_"^ak_name''); |
637 val proof = |
637 val proof = |
638 (if (ak_name'=ak_name'') then |
638 (if (ak_name'=ak_name'') then |
639 (let |
639 (let |
640 val pt_inst = PureThy.get_thm thy'' ("pt_"^ak_name''^"_inst"); |
640 val pt_inst = Global_Theory.get_thm thy'' ("pt_"^ak_name''^"_inst"); |
641 val at_inst = PureThy.get_thm thy'' ("at_"^ak_name''^"_inst"); |
641 val at_inst = Global_Theory.get_thm thy'' ("at_"^ak_name''^"_inst"); |
642 in |
642 in |
643 EVERY [Class.intro_classes_tac [], |
643 EVERY [Class.intro_classes_tac [], |
644 rtac (at_inst RS (pt_inst RS pt_perm_compose)) 1] |
644 rtac (at_inst RS (pt_inst RS pt_perm_compose)) 1] |
645 end) |
645 end) |
646 else |
646 else |
647 (let |
647 (let |
648 val dj_inst = PureThy.get_thm thy'' ("dj_"^ak_name''^"_"^ak_name'); |
648 val dj_inst = Global_Theory.get_thm thy'' ("dj_"^ak_name''^"_"^ak_name'); |
649 val simp_s = HOL_basic_ss addsimps |
649 val simp_s = HOL_basic_ss addsimps |
650 ((dj_inst RS dj_pp_forget):: |
650 ((dj_inst RS dj_pp_forget):: |
651 (maps (PureThy.get_thms thy'') |
651 (maps (Global_Theory.get_thms thy'') |
652 [ak_name' ^"_prm_"^ak_name^"_def", |
652 [ak_name' ^"_prm_"^ak_name^"_def", |
653 ak_name''^"_prm_"^ak_name^"_def"])); |
653 ak_name''^"_prm_"^ak_name^"_def"])); |
654 in |
654 in |
655 EVERY [Class.intro_classes_tac [], simp_tac simp_s 1] |
655 EVERY [Class.intro_classes_tac [], simp_tac simp_s 1] |
656 end)) |
656 end)) |
669 (* are instances of cp_<ak>_<ai> for every <ak>/<ai>-combination *) |
669 (* are instances of cp_<ak>_<ai> for every <ak>/<ai>-combination *) |
670 val thy26 = fold (fn ak_name => fn thy => |
670 val thy26 = fold (fn ak_name => fn thy => |
671 fold (fn ak_name' => fn thy' => |
671 fold (fn ak_name' => fn thy' => |
672 let |
672 let |
673 val cls_name = Sign.full_bname thy' ("cp_"^ak_name^"_"^ak_name'); |
673 val cls_name = Sign.full_bname thy' ("cp_"^ak_name^"_"^ak_name'); |
674 val cp_inst = PureThy.get_thm thy' ("cp_"^ak_name^"_"^ak_name'^"_inst"); |
674 val cp_inst = Global_Theory.get_thm thy' ("cp_"^ak_name^"_"^ak_name'^"_inst"); |
675 val pt_inst = PureThy.get_thm thy' ("pt_"^ak_name^"_inst"); |
675 val pt_inst = Global_Theory.get_thm thy' ("pt_"^ak_name^"_inst"); |
676 val at_inst = PureThy.get_thm thy' ("at_"^ak_name^"_inst"); |
676 val at_inst = Global_Theory.get_thm thy' ("at_"^ak_name^"_inst"); |
677 |
677 |
678 fun cp_proof thm = EVERY [Class.intro_classes_tac [],rtac (thm RS cp1) 1]; |
678 fun cp_proof thm = EVERY [Class.intro_classes_tac [],rtac (thm RS cp1) 1]; |
679 |
679 |
680 val cp_thm_unit = cp_unit_inst; |
680 val cp_thm_unit = cp_unit_inst; |
681 val cp_thm_prod = cp_inst RS (cp_inst RS cp_prod_inst); |
681 val cp_thm_prod = cp_inst RS (cp_inst RS cp_prod_inst); |
837 |
837 |
838 (* FIXME: these lists do not need to be created dynamically again *) |
838 (* FIXME: these lists do not need to be created dynamically again *) |
839 |
839 |
840 |
840 |
841 (* list of all at_inst-theorems *) |
841 (* list of all at_inst-theorems *) |
842 val ats = map (fn ak => PureThy.get_thm thy32 ("at_"^ak^"_inst")) ak_names |
842 val ats = map (fn ak => Global_Theory.get_thm thy32 ("at_"^ak^"_inst")) ak_names |
843 (* list of all pt_inst-theorems *) |
843 (* list of all pt_inst-theorems *) |
844 val pts = map (fn ak => PureThy.get_thm thy32 ("pt_"^ak^"_inst")) ak_names |
844 val pts = map (fn ak => Global_Theory.get_thm thy32 ("pt_"^ak^"_inst")) ak_names |
845 (* list of all cp_inst-theorems as a collection of lists*) |
845 (* list of all cp_inst-theorems as a collection of lists*) |
846 val cps = |
846 val cps = |
847 let fun cps_fun ak1 ak2 = PureThy.get_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst") |
847 let fun cps_fun ak1 ak2 = Global_Theory.get_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst") |
848 in map (fn aki => (map (cps_fun aki) ak_names)) ak_names end; |
848 in map (fn aki => (map (cps_fun aki) ak_names)) ak_names end; |
849 (* list of all cp_inst-theorems that have different atom types *) |
849 (* list of all cp_inst-theorems that have different atom types *) |
850 val cps' = |
850 val cps' = |
851 let fun cps'_fun ak1 ak2 = |
851 let fun cps'_fun ak1 ak2 = |
852 if ak1=ak2 then NONE else SOME (PureThy.get_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst")) |
852 if ak1=ak2 then NONE else SOME (Global_Theory.get_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst")) |
853 in map (fn aki => (map_filter I (map (cps'_fun aki) ak_names))) ak_names end; |
853 in map (fn aki => (map_filter I (map (cps'_fun aki) ak_names))) ak_names end; |
854 (* list of all dj_inst-theorems *) |
854 (* list of all dj_inst-theorems *) |
855 val djs = |
855 val djs = |
856 let fun djs_fun ak1 ak2 = |
856 let fun djs_fun ak1 ak2 = |
857 if ak1=ak2 then NONE else SOME(PureThy.get_thm thy32 ("dj_"^ak2^"_"^ak1)) |
857 if ak1=ak2 then NONE else SOME(Global_Theory.get_thm thy32 ("dj_"^ak2^"_"^ak1)) |
858 in map_filter I (map_product djs_fun ak_names ak_names) end; |
858 in map_filter I (map_product djs_fun ak_names ak_names) end; |
859 (* list of all fs_inst-theorems *) |
859 (* list of all fs_inst-theorems *) |
860 val fss = map (fn ak => PureThy.get_thm thy32 ("fs_"^ak^"_inst")) ak_names |
860 val fss = map (fn ak => Global_Theory.get_thm thy32 ("fs_"^ak^"_inst")) ak_names |
861 (* list of all at_inst-theorems *) |
861 (* list of all at_inst-theorems *) |
862 val fs_axs = map (fn ak => PureThy.get_thm thy32 ("fs_"^ak^"1")) ak_names |
862 val fs_axs = map (fn ak => Global_Theory.get_thm thy32 ("fs_"^ak^"1")) ak_names |
863 |
863 |
864 fun inst_pt thms = maps (fn ti => instR ti pts) thms; |
864 fun inst_pt thms = maps (fn ti => instR ti pts) thms; |
865 fun inst_at thms = maps (fn ti => instR ti ats) thms; |
865 fun inst_at thms = maps (fn ti => instR ti ats) thms; |
866 fun inst_fs thms = maps (fn ti => instR ti fss) thms; |
866 fun inst_fs thms = maps (fn ti => instR ti fss) thms; |
867 fun inst_cp thms cps = flat (inst_mult thms cps); |
867 fun inst_cp thms cps = flat (inst_mult thms cps); |