equal
deleted
inserted
replaced
141 sum.cases} @ mapsx @ map_comps @ map_idents))))); |
141 sum.cases} @ mapsx @ map_comps @ map_idents))))); |
142 |
142 |
143 fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs = |
143 fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs = |
144 HEADGOAL (rtac ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN' |
144 HEADGOAL (rtac ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN' |
145 (the_default (K all_tac) (Option.map rtac disc_fun_opt)) THEN' REPEAT_DETERM_N m o atac) THEN |
145 (the_default (K all_tac) (Option.map rtac disc_fun_opt)) THEN' REPEAT_DETERM_N m o atac) THEN |
146 unfold_thms_tac ctxt (unfold_lets @ sel_funs) THEN HEADGOAL (rtac refl); |
146 unfold_thms_tac ctxt (@{thm split_def} :: unfold_lets @ sel_funs) THEN HEADGOAL (rtac refl); |
147 |
147 |
148 fun inst_split_eq ctxt split = |
148 fun inst_split_eq ctxt split = |
149 (case prop_of split of |
149 (case prop_of split of |
150 @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ (Var (_, Type (_, [T, _])) $ _) $ _) => |
150 @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ (Var (_, Type (_, [T, _])) $ _) $ _) => |
151 let |
151 let |