951 val sbd = Const (fst (Term.dest_Const (Morphism.term phi sbd_free)), mk_relT (`I sbdT)); |
951 val sbd = Const (fst (Term.dest_Const (Morphism.term phi sbd_free)), mk_relT (`I sbdT)); |
952 |
952 |
953 val Abs_sbdT_inj = mk_Abs_inj_thm (#Abs_inject sbdT_loc_info); |
953 val Abs_sbdT_inj = mk_Abs_inj_thm (#Abs_inject sbdT_loc_info); |
954 val Abs_sbdT_bij = mk_Abs_bij_thm lthy Abs_sbdT_inj (#Abs_cases sbdT_loc_info); |
954 val Abs_sbdT_bij = mk_Abs_bij_thm lthy Abs_sbdT_inj (#Abs_cases sbdT_loc_info); |
955 |
955 |
956 fun mk_sum_Cinfinite [thm] = thm |
|
957 | mk_sum_Cinfinite (thm :: thms) = |
|
958 @{thm Cinfinite_csum_strong} OF [thm, mk_sum_Cinfinite thms]; |
|
959 |
|
960 val sum_Cinfinite = mk_sum_Cinfinite bd_Cinfinites; |
956 val sum_Cinfinite = mk_sum_Cinfinite bd_Cinfinites; |
961 val sum_Card_order = sum_Cinfinite RS conjunct2; |
957 val sum_Card_order = sum_Cinfinite RS conjunct2; |
962 |
|
963 fun mk_sum_card_order [thm] = thm |
|
964 | mk_sum_card_order (thm :: thms) = |
|
965 @{thm card_order_csum} OF [thm, mk_sum_card_order thms]; |
|
966 |
|
967 val sum_card_order = mk_sum_card_order bd_card_orders; |
958 val sum_card_order = mk_sum_card_order bd_card_orders; |
968 |
959 |
969 val sbd_ordIso = @{thm ssubst_Pair_rhs} OF |
960 val sbd_ordIso = @{thm ssubst_Pair_rhs} OF |
970 [@{thm dir_image} OF [Abs_sbdT_inj, sum_Card_order], sbd_def]; |
961 [@{thm dir_image} OF [Abs_sbdT_inj, sum_Card_order], sbd_def]; |
971 val sbd_card_order = @{thm iffD2[OF arg_cong[of _ _ card_order]]} OF |
962 val sbd_card_order = @{thm iffD2[OF arg_cong[of _ _ card_order]]} OF |