equal
deleted
inserted
replaced
20 structure BNF_FP_Sugar_Tactics : BNF_FP_SUGAR_TACTICS = |
20 structure BNF_FP_Sugar_Tactics : BNF_FP_SUGAR_TACTICS = |
21 struct |
21 struct |
22 |
22 |
23 open BNF_Tactics |
23 open BNF_Tactics |
24 open BNF_Util |
24 open BNF_Util |
|
25 open BNF_FP_Util |
25 |
26 |
26 fun mk_case_tac ctxt n k m case_def ctr_def unf_fld = |
27 fun mk_case_tac ctxt n k m case_def ctr_def unf_fld = |
27 Local_Defs.unfold_tac ctxt [case_def, ctr_def, unf_fld] THEN |
28 Local_Defs.unfold_tac ctxt [case_def, ctr_def, unf_fld] THEN |
28 (rtac (BNF_FP_Util.mk_sum_casesN n k RS ssubst) THEN' |
29 (rtac (mk_sum_casesN_balanced n k RS ssubst) THEN' |
29 REPEAT_DETERM_N (Int.max (0, m - 1)) o rtac (@{thm split} RS ssubst) THEN' |
30 REPEAT_DETERM_N (Int.max (0, m - 1)) o rtac (@{thm split} RS ssubst) THEN' |
30 rtac refl) 1; |
31 rtac refl) 1; |
31 |
32 |
32 fun mk_exhaust_tac ctxt n ctr_defs fld_iff_unf sumEN' = |
33 fun mk_exhaust_tac ctxt n ctr_defs fld_iff_unf sumEN' = |
33 Local_Defs.unfold_tac ctxt (fld_iff_unf :: ctr_defs) THEN rtac sumEN' 1 THEN |
34 Local_Defs.unfold_tac ctxt (fld_iff_unf :: ctr_defs) THEN rtac sumEN' 1 THEN |