847 infer_instantiate' lthy [NONE, NONE, SOME (Thm.cterm_of lthy ctorB)] arg_cong; |
847 infer_instantiate' lthy [NONE, NONE, SOME (Thm.cterm_of lthy ctorB)] arg_cong; |
848 val fp_map_thm' = fp_map_thm |
848 val fp_map_thm' = fp_map_thm |
849 |> infer_instantiate' lthy (replicate live NONE @ |
849 |> infer_instantiate' lthy (replicate live NONE @ |
850 [SOME (Thm.cterm_of lthy (ctorA $ y))]) |
850 [SOME (Thm.cterm_of lthy (ctorA $ y))]) |
851 |> unfold_thms lthy [dtor_ctor]; |
851 |> unfold_thms lthy [dtor_ctor]; |
852 |
|
853 val map_ctor_thm0 = fp_map_thm' RS ctor_cong RS (ctor_dtor RS sym RS trans); |
|
854 in |
852 in |
855 Thm.generalize ([], [y_s]) (Thm.maxidx_of map_ctor_thm0 + 1) map_ctor_thm0 |
853 (fp_map_thm' RS ctor_cong RS (ctor_dtor RS sym RS trans)) |
|
854 |> Drule.generalize ([], [y_s]) |
856 end; |
855 end; |
857 |
856 |
858 val map_thms = |
857 val map_thms = |
859 let |
858 let |
860 fun mk_goal ctrA ctrB xs ys = |
859 fun mk_goal ctrA ctrB xs ys = |
924 val y_T = domain_type (fastype_of ctorA); |
923 val y_T = domain_type (fastype_of ctorA); |
925 val z_T = domain_type (fastype_of ctorB); |
924 val z_T = domain_type (fastype_of ctorB); |
926 val ((y as Free (y_s, _), z as Free (z_s, _)), _) = lthy |
925 val ((y as Free (y_s, _), z as Free (z_s, _)), _) = lthy |
927 |> yield_singleton (mk_Frees "y") y_T |
926 |> yield_singleton (mk_Frees "y") y_T |
928 ||>> yield_singleton (mk_Frees "z") z_T; |
927 ||>> yield_singleton (mk_Frees "z") z_T; |
929 |
|
930 val rel_ctor_thm0 = fp_rel_thm |
|
931 |> infer_instantiate' lthy (replicate live NONE @ |
|
932 [SOME (Thm.cterm_of lthy (ctorA $ y)), SOME (Thm.cterm_of lthy (ctorB $ z))]) |
|
933 |> unfold_thms lthy [dtor_ctor]; |
|
934 in |
928 in |
935 Thm.generalize ([], [y_s, z_s]) (Thm.maxidx_of rel_ctor_thm0 + 1) rel_ctor_thm0 |
929 fp_rel_thm |
|
930 |> infer_instantiate' lthy (replicate live NONE @ |
|
931 [SOME (Thm.cterm_of lthy (ctorA $ y)), SOME (Thm.cterm_of lthy (ctorB $ z))]) |
|
932 |> unfold_thms lthy [dtor_ctor] |
|
933 |> Drule.generalize ([], [y_s, z_s]) |
936 end; |
934 end; |
937 |
935 |
938 val rel_inject_thms = |
936 val rel_inject_thms = |
939 let |
937 let |
940 fun mk_goal ctrA ctrB xs ys = |
938 fun mk_goal ctrA ctrB xs ys = |