242 val timer = time (timer "Derived simple theorems"); |
242 val timer = time (timer "Derived simple theorems"); |
243 |
243 |
244 (* algebra *) |
244 (* algebra *) |
245 |
245 |
246 val alg_bind = mk_internal_b algN; |
246 val alg_bind = mk_internal_b algN; |
247 val alg_name = Binding.name_of alg_bind; |
|
248 val alg_def_bind = (Thm.def_binding alg_bind, []); |
247 val alg_def_bind = (Thm.def_binding alg_bind, []); |
249 |
248 |
250 (*forall i = 1 ... n: (\<forall>x \<in> Fi_in A1 .. Am B1 ... Bn. si x \<in> Bi)*) |
249 (*forall i = 1 ... n: (\<forall>x \<in> Fi_in A1 .. Am B1 ... Bn. si x \<in> Bi)*) |
251 val alg_spec = |
250 val alg_spec = |
252 let |
251 let |
253 val algT = Library.foldr (op -->) (ATs @ BTs @ sTs, HOLogic.boolT); |
|
254 |
|
255 val ins = map3 mk_in (replicate n (As @ Bs)) setssAs FTsAs; |
252 val ins = map3 mk_in (replicate n (As @ Bs)) setssAs FTsAs; |
256 fun mk_alg_conjunct B s X x x' = |
253 fun mk_alg_conjunct B s X x x' = |
257 mk_Ball X (Term.absfree x' (HOLogic.mk_mem (s $ x, B))); |
254 mk_Ball X (Term.absfree x' (HOLogic.mk_mem (s $ x, B))); |
258 |
255 |
259 val lhs = Term.list_comb (Free (alg_name, algT), As @ Bs @ ss); |
|
260 val rhs = Library.foldr1 HOLogic.mk_conj (map5 mk_alg_conjunct Bs ss ins xFs xFs') |
256 val rhs = Library.foldr1 HOLogic.mk_conj (map5 mk_alg_conjunct Bs ss ins xFs xFs') |
261 in |
257 in |
262 mk_Trueprop_eq (lhs, rhs) |
258 fold_rev (Term.absfree o Term.dest_Free) (As @ Bs @ ss) rhs |
263 end; |
259 end; |
264 |
260 |
265 val ((alg_free, (_, alg_def_free)), (lthy, lthy_old)) = |
261 val ((alg_free, (_, alg_def_free)), (lthy, lthy_old)) = |
266 lthy |
262 lthy |
267 |> Specification.definition (SOME (alg_bind, NONE, NoSyn), (alg_def_bind, alg_spec)) |
263 |> Local_Theory.define ((alg_bind, NoSyn), (alg_def_bind, alg_spec)) |
268 ||> `Local_Theory.restore; |
264 ||> `Local_Theory.restore; |
269 |
265 |
270 val phi = Proof_Context.export_morphism lthy_old lthy; |
266 val phi = Proof_Context.export_morphism lthy_old lthy; |
271 val alg = fst (Term.dest_Const (Morphism.term phi alg_free)); |
267 val alg = fst (Term.dest_Const (Morphism.term phi alg_free)); |
272 val alg_def = Morphism.thm phi alg_def_free; |
268 val alg_def = mk_unabs_def (live + n) (Morphism.thm phi alg_def_free RS meta_eq_to_obj_eq); |
273 |
269 |
274 fun mk_alg As Bs ss = |
270 fun mk_alg As Bs ss = |
275 let |
271 let |
276 val args = As @ Bs @ ss; |
272 val args = As @ Bs @ ss; |
277 val Ts = map fastype_of args; |
273 val Ts = map fastype_of args; |
329 val timer = time (timer "Proved nonemptiness"); |
325 val timer = time (timer "Proved nonemptiness"); |
330 |
326 |
331 (* morphism *) |
327 (* morphism *) |
332 |
328 |
333 val mor_bind = mk_internal_b morN; |
329 val mor_bind = mk_internal_b morN; |
334 val mor_name = Binding.name_of mor_bind; |
|
335 val mor_def_bind = (Thm.def_binding mor_bind, []); |
330 val mor_def_bind = (Thm.def_binding mor_bind, []); |
336 |
331 |
337 (*fbetw) forall i = 1 ... n: (\<forall>x \<in> Bi. f x \<in> B'i)*) |
332 (*fbetw) forall i = 1 ... n: (\<forall>x \<in> Bi. f x \<in> B'i)*) |
338 (*mor) forall i = 1 ... n: (\<forall>x \<in> Fi_in UNIV ... UNIV B1 ... Bn. |
333 (*mor) forall i = 1 ... n: (\<forall>x \<in> Fi_in UNIV ... UNIV B1 ... Bn. |
339 f (s1 x) = s1' (Fi_map id ... id f1 ... fn x))*) |
334 f (s1 x) = s1' (Fi_map id ... id f1 ... fn x))*) |
340 val mor_spec = |
335 val mor_spec = |
341 let |
336 let |
342 val morT = Library.foldr (op -->) (BTs @ sTs @ B'Ts @ s'Ts @ fTs, HOLogic.boolT); |
|
343 |
|
344 fun mk_fbetw f B1 B2 z z' = |
337 fun mk_fbetw f B1 B2 z z' = |
345 mk_Ball B1 (Term.absfree z' (HOLogic.mk_mem (f $ z, B2))); |
338 mk_Ball B1 (Term.absfree z' (HOLogic.mk_mem (f $ z, B2))); |
346 fun mk_mor sets mapAsBs f s s' T x x' = |
339 fun mk_mor sets mapAsBs f s s' T x x' = |
347 mk_Ball (mk_in (passive_UNIVs @ Bs) sets T) |
340 mk_Ball (mk_in (passive_UNIVs @ Bs) sets T) |
348 (Term.absfree x' (HOLogic.mk_eq (f $ (s $ x), s' $ |
341 (Term.absfree x' (HOLogic.mk_eq (f $ (s $ x), s' $ |
349 (Term.list_comb (mapAsBs, passive_ids @ fs) $ x)))); |
342 (Term.list_comb (mapAsBs, passive_ids @ fs) $ x)))); |
350 val lhs = Term.list_comb (Free (mor_name, morT), Bs @ ss @ B's @ s's @ fs); |
|
351 val rhs = HOLogic.mk_conj |
343 val rhs = HOLogic.mk_conj |
352 (Library.foldr1 HOLogic.mk_conj (map5 mk_fbetw fs Bs B's zs zs'), |
344 (Library.foldr1 HOLogic.mk_conj (map5 mk_fbetw fs Bs B's zs zs'), |
353 Library.foldr1 HOLogic.mk_conj |
345 Library.foldr1 HOLogic.mk_conj |
354 (map8 mk_mor setssAs mapsAsBs fs ss s's FTsAs xFs xFs')) |
346 (map8 mk_mor setssAs mapsAsBs fs ss s's FTsAs xFs xFs')) |
355 in |
347 in |
356 mk_Trueprop_eq (lhs, rhs) |
348 fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss @ B's @ s's @ fs) rhs |
357 end; |
349 end; |
358 |
350 |
359 val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) = |
351 val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) = |
360 lthy |
352 lthy |
361 |> Specification.definition (SOME (mor_bind, NONE, NoSyn), (mor_def_bind, mor_spec)) |
353 |> Local_Theory.define ((mor_bind, NoSyn), (mor_def_bind, mor_spec)) |
362 ||> `Local_Theory.restore; |
354 ||> `Local_Theory.restore; |
363 |
355 |
364 val phi = Proof_Context.export_morphism lthy_old lthy; |
356 val phi = Proof_Context.export_morphism lthy_old lthy; |
365 val mor = fst (Term.dest_Const (Morphism.term phi mor_free)); |
357 val mor = fst (Term.dest_Const (Morphism.term phi mor_free)); |
366 val mor_def = Morphism.thm phi mor_def_free; |
358 val mor_def = mk_unabs_def (5 * n) (Morphism.thm phi mor_def_free RS meta_eq_to_obj_eq); |
367 |
359 |
368 fun mk_mor Bs1 ss1 Bs2 ss2 fs = |
360 fun mk_mor Bs1 ss1 Bs2 ss2 fs = |
369 let |
361 let |
370 val args = Bs1 @ ss1 @ Bs2 @ ss2 @ fs; |
362 val args = Bs1 @ ss1 @ Bs2 @ ss2 @ fs; |
371 val Ts = map fastype_of (Bs1 @ ss1 @ Bs2 @ ss2 @ fs); |
363 val Ts = map fastype_of (Bs1 @ ss1 @ Bs2 @ ss2 @ fs); |
717 |
709 |
718 val timer = time (timer "min_algs definition & thms"); |
710 val timer = time (timer "min_algs definition & thms"); |
719 |
711 |
720 val min_alg_binds = mk_internal_bs min_algN; |
712 val min_alg_binds = mk_internal_bs min_algN; |
721 fun min_alg_bind i = nth min_alg_binds (i - 1); |
713 fun min_alg_bind i = nth min_alg_binds (i - 1); |
722 fun min_alg_name i = Binding.name_of (min_alg_bind i); |
|
723 val min_alg_def_bind = rpair [] o Thm.def_binding o min_alg_bind; |
714 val min_alg_def_bind = rpair [] o Thm.def_binding o min_alg_bind; |
724 |
715 |
725 fun min_alg_spec i = |
716 fun min_alg_spec i = |
726 let |
717 let |
727 val min_algT = |
|
728 Library.foldr (op -->) (ATs @ sTs, HOLogic.mk_setT (nth activeAs (i - 1))); |
|
729 |
|
730 val lhs = Term.list_comb (Free (min_alg_name i, min_algT), As @ ss); |
|
731 val rhs = mk_UNION (field_suc_bd) |
718 val rhs = mk_UNION (field_suc_bd) |
732 (Term.absfree idx' (mk_nthN n (mk_min_algs As ss $ idx) i)); |
719 (Term.absfree idx' (mk_nthN n (mk_min_algs As ss $ idx) i)); |
733 in |
720 in |
734 mk_Trueprop_eq (lhs, rhs) |
721 fold_rev (Term.absfree o Term.dest_Free) (As @ ss) rhs |
735 end; |
722 end; |
736 |
723 |
737 val ((min_alg_frees, (_, min_alg_def_frees)), (lthy, lthy_old)) = |
724 val ((min_alg_frees, (_, min_alg_def_frees)), (lthy, lthy_old)) = |
738 lthy |
725 lthy |
739 |> fold_map (fn i => Specification.definition |
726 |> fold_map (fn i => Local_Theory.define |
740 (SOME (min_alg_bind i, NONE, NoSyn), (min_alg_def_bind i, min_alg_spec i))) ks |
727 ((min_alg_bind i, NoSyn), (min_alg_def_bind i, min_alg_spec i))) ks |
741 |>> apsnd split_list o split_list |
728 |>> apsnd split_list o split_list |
742 ||> `Local_Theory.restore; |
729 ||> `Local_Theory.restore; |
743 |
730 |
744 val phi = Proof_Context.export_morphism lthy_old lthy; |
731 val phi = Proof_Context.export_morphism lthy_old lthy; |
745 val min_algs = map (fst o Term.dest_Const o Morphism.term phi) min_alg_frees; |
732 val min_algs = map (fst o Term.dest_Const o Morphism.term phi) min_alg_frees; |
746 val min_alg_defs = map (Morphism.thm phi) min_alg_def_frees; |
733 val min_alg_defs = map (fn def => |
|
734 mk_unabs_def live (Morphism.thm phi def RS meta_eq_to_obj_eq)) min_alg_def_frees; |
747 |
735 |
748 fun mk_min_alg As ss i = |
736 fun mk_min_alg As ss i = |
749 let |
737 let |
750 val T = HOLogic.mk_setT (range_type (fastype_of (nth ss (i - 1)))) |
738 val T = HOLogic.mk_setT (range_type (fastype_of (nth ss (i - 1)))) |
751 val args = As @ ss; |
739 val args = As @ ss; |
830 val select_Bs = map (mk_nthN n (HOLogic.mk_fst (Rep_IIT $ iidx))) ks; |
818 val select_Bs = map (mk_nthN n (HOLogic.mk_fst (Rep_IIT $ iidx))) ks; |
831 val select_ss = map (mk_nthN n (HOLogic.mk_snd (Rep_IIT $ iidx))) ks; |
819 val select_ss = map (mk_nthN n (HOLogic.mk_snd (Rep_IIT $ iidx))) ks; |
832 |
820 |
833 val str_init_binds = mk_internal_bs str_initN; |
821 val str_init_binds = mk_internal_bs str_initN; |
834 fun str_init_bind i = nth str_init_binds (i - 1); |
822 fun str_init_bind i = nth str_init_binds (i - 1); |
835 val str_init_name = Binding.name_of o str_init_bind; |
|
836 val str_init_def_bind = rpair [] o Thm.def_binding o str_init_bind; |
823 val str_init_def_bind = rpair [] o Thm.def_binding o str_init_bind; |
837 |
824 |
838 fun str_init_spec i = |
825 fun str_init_spec i = |
839 let |
826 let |
840 val T = nth init_FTs (i - 1); |
|
841 val init_xF = nth init_xFs (i - 1) |
827 val init_xF = nth init_xFs (i - 1) |
842 val select_s = nth select_ss (i - 1); |
828 val select_s = nth select_ss (i - 1); |
843 val map = mk_map_of_bnf (nth Dss (i - 1)) |
829 val map = mk_map_of_bnf (nth Dss (i - 1)) |
844 (passiveAs @ active_initTs) (passiveAs @ replicate n Asuc_bdT) |
830 (passiveAs @ active_initTs) (passiveAs @ replicate n Asuc_bdT) |
845 (nth bnfs (i - 1)); |
831 (nth bnfs (i - 1)); |
846 val map_args = passive_ids @ replicate n (mk_rapp iidx Asuc_bdT); |
832 val map_args = passive_ids @ replicate n (mk_rapp iidx Asuc_bdT); |
847 val str_initT = T --> IIT --> Asuc_bdT; |
|
848 |
|
849 val lhs = Term.list_comb (Free (str_init_name i, str_initT), [init_xF, iidx]); |
|
850 val rhs = select_s $ (Term.list_comb (map, map_args) $ init_xF); |
833 val rhs = select_s $ (Term.list_comb (map, map_args) $ init_xF); |
851 in |
834 in |
852 mk_Trueprop_eq (lhs, rhs) |
835 fold_rev (Term.absfree o Term.dest_Free) [init_xF, iidx] rhs |
853 end; |
836 end; |
854 |
837 |
855 val ((str_init_frees, (_, str_init_def_frees)), (lthy, lthy_old)) = |
838 val ((str_init_frees, (_, str_init_def_frees)), (lthy, lthy_old)) = |
856 lthy |
839 lthy |
857 |> fold_map (fn i => Specification.definition |
840 |> fold_map (fn i => Local_Theory.define |
858 (SOME (str_init_bind i, NONE, NoSyn), (str_init_def_bind i, str_init_spec i))) ks |
841 ((str_init_bind i, NoSyn), (str_init_def_bind i, str_init_spec i))) ks |
859 |>> apsnd split_list o split_list |
842 |>> apsnd split_list o split_list |
860 ||> `Local_Theory.restore; |
843 ||> `Local_Theory.restore; |
861 |
844 |
862 val phi = Proof_Context.export_morphism lthy_old lthy; |
845 val phi = Proof_Context.export_morphism lthy_old lthy; |
863 val str_inits = |
846 val str_inits = |
864 map (Term.subst_atomic_types (map (`(Morphism.typ phi)) params') o Morphism.term phi) |
847 map (Term.subst_atomic_types (map (`(Morphism.typ phi)) params') o Morphism.term phi) |
865 str_init_frees; |
848 str_init_frees; |
866 |
849 |
867 val str_init_defs = map (Morphism.thm phi) str_init_def_frees; |
850 val str_init_defs = map (fn def => |
|
851 mk_unabs_def 2 (Morphism.thm phi def RS meta_eq_to_obj_eq)) str_init_def_frees; |
868 |
852 |
869 val car_inits = map (mk_min_alg passive_UNIVs str_inits) ks; |
853 val car_inits = map (mk_min_alg passive_UNIVs str_inits) ks; |
870 |
854 |
871 (*TODO: replace with instantiate? (problem: figure out right type instantiation)*) |
855 (*TODO: replace with instantiate? (problem: figure out right type instantiation)*) |
872 val alg_init_thm = Goal.prove_sorry lthy [] [] |
856 val alg_init_thm = Goal.prove_sorry lthy [] [] |
1022 val Izs = map2 retype_free Ts zs; |
1006 val Izs = map2 retype_free Ts zs; |
1023 val phis = map2 retype_free (map mk_pred1T Ts) init_phis; |
1007 val phis = map2 retype_free (map mk_pred1T Ts) init_phis; |
1024 val phi2s = map2 retype_free (map2 mk_pred2T Ts Ts') init_phis; |
1008 val phi2s = map2 retype_free (map2 mk_pred2T Ts Ts') init_phis; |
1025 |
1009 |
1026 fun ctor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctorN ^ "_"); |
1010 fun ctor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctorN ^ "_"); |
1027 val ctor_name = Binding.name_of o ctor_bind; |
|
1028 val ctor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o ctor_bind; |
1011 val ctor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o ctor_bind; |
1029 |
1012 |
1030 fun ctor_spec i abs str map_FT_init x x' = |
1013 fun ctor_spec abs str map_FT_init x x' = |
1031 let |
1014 Term.absfree x' (abs $ (str $ |
1032 val ctorT = nth FTs (i - 1) --> nth Ts (i - 1); |
|
1033 |
|
1034 val lhs = Free (ctor_name i, ctorT); |
|
1035 val rhs = Term.absfree x' (abs $ (str $ |
|
1036 (Term.list_comb (map_FT_init, map HOLogic.id_const passiveAs @ Rep_Ts) $ x))); |
1015 (Term.list_comb (map_FT_init, map HOLogic.id_const passiveAs @ Rep_Ts) $ x))); |
1037 in |
|
1038 mk_Trueprop_eq (lhs, rhs) |
|
1039 end; |
|
1040 |
1016 |
1041 val ((ctor_frees, (_, ctor_def_frees)), (lthy, lthy_old)) = |
1017 val ((ctor_frees, (_, ctor_def_frees)), (lthy, lthy_old)) = |
1042 lthy |
1018 lthy |
1043 |> fold_map6 (fn i => fn abs => fn str => fn mapx => fn x => fn x' => |
1019 |> fold_map6 (fn i => fn abs => fn str => fn mapx => fn x => fn x' => |
1044 Specification.definition |
1020 Local_Theory.define |
1045 (SOME (ctor_bind i, NONE, NoSyn), (ctor_def_bind i, ctor_spec i abs str mapx x x'))) |
1021 ((ctor_bind i, NoSyn), (ctor_def_bind i, ctor_spec abs str mapx x x'))) |
1046 ks Abs_Ts str_inits map_FT_inits xFs xFs' |
1022 ks Abs_Ts str_inits map_FT_inits xFs xFs' |
1047 |>> apsnd split_list o split_list |
1023 |>> apsnd split_list o split_list |
1048 ||> `Local_Theory.restore; |
1024 ||> `Local_Theory.restore; |
1049 |
1025 |
1050 val phi = Proof_Context.export_morphism lthy_old lthy; |
1026 val phi = Proof_Context.export_morphism lthy_old lthy; |
1051 fun mk_ctors passive = |
1027 fun mk_ctors passive = |
1052 map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (mk_params passive)) o |
1028 map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (mk_params passive)) o |
1053 Morphism.term phi) ctor_frees; |
1029 Morphism.term phi) ctor_frees; |
1054 val ctors = mk_ctors passiveAs; |
1030 val ctors = mk_ctors passiveAs; |
1055 val ctor's = mk_ctors passiveBs; |
1031 val ctor's = mk_ctors passiveBs; |
1056 val ctor_defs = map (Morphism.thm phi) ctor_def_frees; |
1032 val ctor_defs = map (fn def => Morphism.thm phi def RS meta_eq_to_obj_eq) ctor_def_frees; |
1057 |
1033 |
1058 val (mor_Rep_thm, mor_Abs_thm) = |
1034 val (mor_Rep_thm, mor_Abs_thm) = |
1059 let |
1035 let |
1060 val copy = alg_init_thm RS copy_alg_thm; |
1036 val copy = alg_init_thm RS copy_alg_thm; |
1061 fun mk_bij inj Rep cases = @{thm bij_betwI'} OF [inj, Rep, cases]; |
1037 fun mk_bij inj Rep cases = @{thm bij_betwI'} OF [inj, Rep, cases]; |
1082 val fold_fun = Term.absfree fold_f' |
1058 val fold_fun = Term.absfree fold_f' |
1083 (mk_mor UNIVs ctors active_UNIVs ss (map (mk_nthN n fold_f) ks)); |
1059 (mk_mor UNIVs ctors active_UNIVs ss (map (mk_nthN n fold_f) ks)); |
1084 val foldx = HOLogic.choice_const foldT $ fold_fun; |
1060 val foldx = HOLogic.choice_const foldT $ fold_fun; |
1085 |
1061 |
1086 fun fold_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctor_foldN ^ "_"); |
1062 fun fold_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctor_foldN ^ "_"); |
1087 val fold_name = Binding.name_of o fold_bind; |
|
1088 val fold_def_bind = rpair [] o Binding.conceal o Thm.def_binding o fold_bind; |
1063 val fold_def_bind = rpair [] o Binding.conceal o Thm.def_binding o fold_bind; |
1089 |
1064 |
1090 fun fold_spec i T AT = |
1065 fun fold_spec i = fold_rev (Term.absfree o Term.dest_Free) ss (mk_nthN n foldx i); |
1091 let |
|
1092 val foldT = Library.foldr (op -->) (sTs, T --> AT); |
|
1093 |
|
1094 val lhs = Term.list_comb (Free (fold_name i, foldT), ss); |
|
1095 val rhs = mk_nthN n foldx i; |
|
1096 in |
|
1097 mk_Trueprop_eq (lhs, rhs) |
|
1098 end; |
|
1099 |
1066 |
1100 val ((fold_frees, (_, fold_def_frees)), (lthy, lthy_old)) = |
1067 val ((fold_frees, (_, fold_def_frees)), (lthy, lthy_old)) = |
1101 lthy |
1068 lthy |
1102 |> fold_map3 (fn i => fn T => fn AT => |
1069 |> fold_map (fn i => |
1103 Specification.definition |
1070 Local_Theory.define ((fold_bind i, NoSyn), (fold_def_bind i, fold_spec i))) ks |
1104 (SOME (fold_bind i, NONE, NoSyn), (fold_def_bind i, fold_spec i T AT))) |
|
1105 ks Ts activeAs |
|
1106 |>> apsnd split_list o split_list |
1071 |>> apsnd split_list o split_list |
1107 ||> `Local_Theory.restore; |
1072 ||> `Local_Theory.restore; |
1108 |
1073 |
1109 val phi = Proof_Context.export_morphism lthy_old lthy; |
1074 val phi = Proof_Context.export_morphism lthy_old lthy; |
1110 val folds = map (Morphism.term phi) fold_frees; |
1075 val folds = map (Morphism.term phi) fold_frees; |
1114 Const (name, Library.foldr (op -->) |
1079 Const (name, Library.foldr (op -->) |
1115 (map2 (curry op -->) (mk_FTs (passives @ actives)) actives, T --> active))) |
1080 (map2 (curry op -->) (mk_FTs (passives @ actives)) actives, T --> active))) |
1116 fold_names (mk_Ts passives) actives; |
1081 fold_names (mk_Ts passives) actives; |
1117 fun mk_fold Ts ss i = Term.list_comb (Const (nth fold_names (i - 1), Library.foldr (op -->) |
1082 fun mk_fold Ts ss i = Term.list_comb (Const (nth fold_names (i - 1), Library.foldr (op -->) |
1118 (map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss); |
1083 (map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss); |
1119 val fold_defs = map (Morphism.thm phi) fold_def_frees; |
1084 val fold_defs = map (fn def => |
|
1085 mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) fold_def_frees; |
1120 |
1086 |
1121 val mor_fold_thm = |
1087 val mor_fold_thm = |
1122 let |
1088 let |
1123 val ex_mor = talg_thm RS init_ex_mor_thm; |
1089 val ex_mor = talg_thm RS init_ex_mor_thm; |
1124 val mor_cong = mor_cong_thm OF (map (mk_nth_conv n) ks); |
1090 val mor_cong = mor_cong_thm OF (map (mk_nth_conv n) ks); |
1172 val map_ctors = map2 (fn Ds => fn bnf => |
1138 val map_ctors = map2 (fn Ds => fn bnf => |
1173 Term.list_comb (mk_map_of_bnf Ds (passiveAs @ FTs) (passiveAs @ Ts) bnf, |
1139 Term.list_comb (mk_map_of_bnf Ds (passiveAs @ FTs) (passiveAs @ Ts) bnf, |
1174 map HOLogic.id_const passiveAs @ ctors)) Dss bnfs; |
1140 map HOLogic.id_const passiveAs @ ctors)) Dss bnfs; |
1175 |
1141 |
1176 fun dtor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtorN ^ "_"); |
1142 fun dtor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtorN ^ "_"); |
1177 val dtor_name = Binding.name_of o dtor_bind; |
|
1178 val dtor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o dtor_bind; |
1143 val dtor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o dtor_bind; |
1179 |
1144 |
1180 fun dtor_spec i FT T = |
1145 fun dtor_spec i = mk_fold Ts map_ctors i; |
1181 let |
|
1182 val dtorT = T --> FT; |
|
1183 |
|
1184 val lhs = Free (dtor_name i, dtorT); |
|
1185 val rhs = mk_fold Ts map_ctors i; |
|
1186 in |
|
1187 mk_Trueprop_eq (lhs, rhs) |
|
1188 end; |
|
1189 |
1146 |
1190 val ((dtor_frees, (_, dtor_def_frees)), (lthy, lthy_old)) = |
1147 val ((dtor_frees, (_, dtor_def_frees)), (lthy, lthy_old)) = |
1191 lthy |
1148 lthy |
1192 |> fold_map3 (fn i => fn FT => fn T => |
1149 |> fold_map (fn i => |
1193 Specification.definition |
1150 Local_Theory.define ((dtor_bind i, NoSyn), (dtor_def_bind i, dtor_spec i))) ks |
1194 (SOME (dtor_bind i, NONE, NoSyn), (dtor_def_bind i, dtor_spec i FT T))) ks FTs Ts |
|
1195 |>> apsnd split_list o split_list |
1151 |>> apsnd split_list o split_list |
1196 ||> `Local_Theory.restore; |
1152 ||> `Local_Theory.restore; |
1197 |
1153 |
1198 val phi = Proof_Context.export_morphism lthy_old lthy; |
1154 val phi = Proof_Context.export_morphism lthy_old lthy; |
1199 fun mk_dtors params = |
1155 fun mk_dtors params = |
1200 map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ params) o Morphism.term phi) |
1156 map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ params) o Morphism.term phi) |
1201 dtor_frees; |
1157 dtor_frees; |
1202 val dtors = mk_dtors params'; |
1158 val dtors = mk_dtors params'; |
1203 val dtor_defs = map (Morphism.thm phi) dtor_def_frees; |
1159 val dtor_defs = map (fn def => Morphism.thm phi def RS meta_eq_to_obj_eq) dtor_def_frees; |
1204 |
1160 |
1205 val ctor_o_dtor_thms = map2 (fold_thms lthy o single) dtor_defs ctor_o_fold_thms; |
1161 val ctor_o_dtor_thms = map2 (fold_thms lthy o single) dtor_defs ctor_o_fold_thms; |
1206 |
1162 |
1207 val dtor_o_ctor_thms = |
1163 val dtor_o_ctor_thms = |
1208 let |
1164 let |
1245 map2 (fn unique => fn fold_ctor => |
1201 map2 (fn unique => fn fold_ctor => |
1246 trans OF [mor RS unique, fold_ctor]) fold_unique_mor_thms fold_ctor_thms |
1202 trans OF [mor RS unique, fold_ctor]) fold_unique_mor_thms fold_ctor_thms |
1247 end; |
1203 end; |
1248 |
1204 |
1249 fun rec_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctor_recN ^ "_"); |
1205 fun rec_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctor_recN ^ "_"); |
1250 val rec_name = Binding.name_of o rec_bind; |
|
1251 val rec_def_bind = rpair [] o Binding.conceal o Thm.def_binding o rec_bind; |
1206 val rec_def_bind = rpair [] o Binding.conceal o Thm.def_binding o rec_bind; |
1252 |
1207 |
1253 val rec_strs = |
1208 val rec_strs = |
1254 map3 (fn ctor => fn prod_s => fn mapx => |
1209 map3 (fn ctor => fn prod_s => fn mapx => |
1255 mk_convol (HOLogic.mk_comp (ctor, Term.list_comb (mapx, passive_ids @ rec_fsts)), prod_s)) |
1210 mk_convol (HOLogic.mk_comp (ctor, Term.list_comb (mapx, passive_ids @ rec_fsts)), prod_s)) |
1256 ctors rec_ss rec_maps; |
1211 ctors rec_ss rec_maps; |
1257 |
1212 |
1258 fun rec_spec i T AT = |
1213 fun rec_spec i T AT = |
1259 let |
1214 fold_rev (Term.absfree o Term.dest_Free) rec_ss |
1260 val recT = Library.foldr (op -->) (rec_sTs, T --> AT); |
1215 (HOLogic.mk_comp (snd_const (HOLogic.mk_prodT (T, AT)), mk_fold Ts rec_strs i)); |
1261 |
|
1262 val lhs = Term.list_comb (Free (rec_name i, recT), rec_ss); |
|
1263 val rhs = HOLogic.mk_comp (snd_const (HOLogic.mk_prodT (T, AT)), mk_fold Ts rec_strs i); |
|
1264 in |
|
1265 mk_Trueprop_eq (lhs, rhs) |
|
1266 end; |
|
1267 |
1216 |
1268 val ((rec_frees, (_, rec_def_frees)), (lthy, lthy_old)) = |
1217 val ((rec_frees, (_, rec_def_frees)), (lthy, lthy_old)) = |
1269 lthy |
1218 lthy |
1270 |> fold_map3 (fn i => fn T => fn AT => |
1219 |> fold_map3 (fn i => fn T => fn AT => |
1271 Specification.definition |
1220 Local_Theory.define ((rec_bind i, NoSyn), (rec_def_bind i, rec_spec i T AT))) ks Ts activeAs |
1272 (SOME (rec_bind i, NONE, NoSyn), (rec_def_bind i, rec_spec i T AT))) |
|
1273 ks Ts activeAs |
|
1274 |>> apsnd split_list o split_list |
1221 |>> apsnd split_list o split_list |
1275 ||> `Local_Theory.restore; |
1222 ||> `Local_Theory.restore; |
1276 |
1223 |
1277 val phi = Proof_Context.export_morphism lthy_old lthy; |
1224 val phi = Proof_Context.export_morphism lthy_old lthy; |
1278 val recs = map (Morphism.term phi) rec_frees; |
1225 val recs = map (Morphism.term phi) rec_frees; |
1279 val rec_names = map (fst o dest_Const) recs; |
1226 val rec_names = map (fst o dest_Const) recs; |
1280 fun mk_rec ss i = Term.list_comb (Const (nth rec_names (i - 1), Library.foldr (op -->) |
1227 fun mk_rec ss i = Term.list_comb (Const (nth rec_names (i - 1), Library.foldr (op -->) |
1281 (map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss); |
1228 (map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss); |
1282 val rec_defs = map (Morphism.thm phi) rec_def_frees; |
1229 val rec_defs = map (fn def => |
|
1230 mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) rec_def_frees; |
1283 |
1231 |
1284 val convols = map2 (fn T => fn i => mk_convol (HOLogic.id_const T, mk_rec rec_ss i)) Ts ks; |
1232 val convols = map2 (fn T => fn i => mk_convol (HOLogic.id_const T, mk_rec rec_ss i)) Ts ks; |
1285 val ctor_rec_thms = |
1233 val ctor_rec_thms = |
1286 let |
1234 let |
1287 fun mk_goal i rec_s rec_map ctor x = |
1235 fun mk_goal i rec_s rec_map ctor x = |