40 |
40 |
41 val deads = fold (union (op =)) Dss resDs; |
41 val deads = fold (union (op =)) Dss resDs; |
42 val names_lthy = fold Variable.declare_typ deads lthy; |
42 val names_lthy = fold Variable.declare_typ deads lthy; |
43 |
43 |
44 (* tvars *) |
44 (* tvars *) |
45 val (((((((passiveAs, activeAs), allAs)), (passiveBs, activeBs)), |
45 val (((((((passiveAs, activeAs), allAs)), ((passiveBs, activeBs), allBs')), |
46 activeCs), passiveXs), passiveYs) = names_lthy |
46 activeCs), passiveXs), passiveYs) = names_lthy |
47 |> mk_TFrees live |
47 |> mk_TFrees live |
48 |> apfst (`(chop m)) |
48 |> apfst (`(chop m)) |
49 ||> mk_TFrees live |
49 ||> mk_TFrees live |
50 ||>> apfst (chop m) |
50 ||>> apfst (`(chop m)) |
51 ||>> mk_TFrees n |
51 ||>> mk_TFrees n |
52 ||>> mk_TFrees m |
52 ||>> mk_TFrees m |
53 ||> fst o mk_TFrees m; |
53 ||> fst o mk_TFrees m; |
54 |
54 |
55 val Ass = replicate n allAs; |
55 val Ass = replicate n allAs; |
1089 ||> `Local_Theory.restore; |
1089 ||> `Local_Theory.restore; |
1090 |
1090 |
1091 val phi = Proof_Context.export_morphism lthy_old lthy; |
1091 val phi = Proof_Context.export_morphism lthy_old lthy; |
1092 val folds = map (Morphism.term phi) fold_frees; |
1092 val folds = map (Morphism.term phi) fold_frees; |
1093 val fold_names = map (fst o dest_Const) folds; |
1093 val fold_names = map (fst o dest_Const) folds; |
|
1094 fun mk_folds passives actives = |
|
1095 map3 (fn name => fn T => fn active => |
|
1096 Const (name, Library.foldr (op -->) |
|
1097 (map2 (curry (op -->)) (mk_FTs (passives @ actives)) actives, T --> active))) |
|
1098 fold_names (mk_Ts passives) actives; |
1094 fun mk_fold Ts ss i = Term.list_comb (Const (nth fold_names (i - 1), Library.foldr (op -->) |
1099 fun mk_fold Ts ss i = Term.list_comb (Const (nth fold_names (i - 1), Library.foldr (op -->) |
1095 (map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss); |
1100 (map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss); |
1096 val fold_defs = map (Morphism.thm phi) fold_def_frees; |
1101 val fold_defs = map (Morphism.thm phi) fold_def_frees; |
1097 |
1102 |
1098 val mor_fold_thm = |
1103 val mor_fold_thm = |
1380 |
1385 |
1381 fun mk_ctor_Irel_DEADID_thm ctor_inject bnf = |
1386 fun mk_ctor_Irel_DEADID_thm ctor_inject bnf = |
1382 trans OF [ctor_inject, rel_eq_of_bnf bnf RS @{thm predicate2_eqD} RS sym]; |
1387 trans OF [ctor_inject, rel_eq_of_bnf bnf RS @{thm predicate2_eqD} RS sym]; |
1383 |
1388 |
1384 val IphiTs = map2 mk_pred2T passiveAs passiveBs; |
1389 val IphiTs = map2 mk_pred2T passiveAs passiveBs; |
|
1390 val activephiTs = map2 mk_pred2T activeAs activeBs; |
1385 val activeIphiTs = map2 mk_pred2T Ts Ts'; |
1391 val activeIphiTs = map2 mk_pred2T Ts Ts'; |
1386 val ((Iphis, activeIphis), names_lthy) = names_lthy |
1392 val (((Iphis, activephis), activeIphis), names_lthy) = names_lthy |
1387 |> mk_Frees "R" IphiTs |
1393 |> mk_Frees "R" IphiTs |
|
1394 ||>> mk_Frees "S" activephiTs |
1388 ||>> mk_Frees "IR" activeIphiTs; |
1395 ||>> mk_Frees "IR" activeIphiTs; |
1389 val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; |
1396 val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; |
1390 |
1397 |
1391 (*register new datatypes as BNFs*) |
1398 (*register new datatypes as BNFs*) |
1392 val (timer, Ibnfs, folded_ctor_map_thms, folded_ctor_set_thmss', ctor_Irel_thms, lthy) = |
1399 val (timer, Ibnfs, folded_ctor_map_thms, folded_ctor_set_thmss', ctor_Irel_thms, lthy) = |
1799 val Irel_induct_thm = |
1806 val Irel_induct_thm = |
1800 mk_rel_co_induct_thm Least_FP rels activeIphis Irels Iphis xFs yFs ctors ctor's |
1807 mk_rel_co_induct_thm Least_FP rels activeIphis Irels Iphis xFs yFs ctors ctor's |
1801 (mk_rel_induct_tac m ctor_induct2_thm ks ctor_Irel_thms (map rel_mono_strong_of_bnf bnfs)) |
1808 (mk_rel_induct_tac m ctor_induct2_thm ks ctor_Irel_thms (map rel_mono_strong_of_bnf bnfs)) |
1802 lthy; |
1809 lthy; |
1803 |
1810 |
|
1811 val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs; |
|
1812 val ctor_fold_transfer_thms = |
|
1813 mk_un_fold_transfer_thms Least_FP rels activephis Irels Iphis |
|
1814 (mk_folds passiveAs activeAs) (mk_folds passiveBs activeBs) |
|
1815 (mk_fold_transfer_tac m Irel_induct_thm (map map_transfer_of_bnf bnfs) ctor_fold_thms) |
|
1816 lthy; |
|
1817 |
1804 val timer = time (timer "relator induction"); |
1818 val timer = time (timer "relator induction"); |
1805 |
1819 |
1806 val common_notes = |
1820 val common_notes = |
1807 [(ctor_inductN, [ctor_induct_thm]), |
1821 [(ctor_inductN, [ctor_induct_thm]), |
1808 (ctor_induct2N, [ctor_induct2_thm]), |
1822 (ctor_induct2N, [ctor_induct2_thm]), |
1809 (rel_inductN, [Irel_induct_thm])] |
1823 (rel_inductN, [Irel_induct_thm]), |
|
1824 (ctor_fold_transferN, ctor_fold_transfer_thms)] |
1810 |> map (fn (thmN, thms) => |
1825 |> map (fn (thmN, thms) => |
1811 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); |
1826 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); |
1812 |
1827 |
1813 val notes = |
1828 val notes = |
1814 [(ctor_dtorN, ctor_dtor_thms), |
1829 [(ctor_dtorN, ctor_dtor_thms), |