45 val (_, big_case_args) = strip_comb big_case_tm; |
45 val (_, big_case_args) = strip_comb big_case_tm; |
46 |
46 |
47 (*Each equation has the form |
47 (*Each equation has the form |
48 rec_case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *) |
48 rec_case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *) |
49 fun mk_case_equation (((id,T,syn), name, args, prems), case_free) = |
49 fun mk_case_equation (((id,T,syn), name, args, prems), case_free) = |
50 Ind_Syntax.mk_tprop |
50 FOLogic.mk_Trueprop |
51 (Ind_Syntax.eq_const $ |
51 (FOLogic.mk_eq |
52 (big_case_tm $ |
52 (big_case_tm $ |
53 (list_comb (Const (Sign.intern_const (sign_of Const.thy) name,T), args))) $ |
53 (list_comb (Const (Sign.intern_const (sign_of Const.thy) name,T), |
54 (list_comb (case_free, args))); |
54 args)), |
|
55 list_comb (case_free, args))); |
55 |
56 |
56 val case_trans = hd con_defs RS Ind_Syntax.def_trans |
57 val case_trans = hd con_defs RS Ind_Syntax.def_trans |
57 and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS trans; |
58 and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS trans; |
58 |
59 |
59 (*Proves a single case equation. Could use simp_tac, but it's slower!*) |
60 (*Proves a single case equation. Could use simp_tac, but it's slower!*) |