equal
deleted
inserted
replaced
28 (rtac (BNF_FP_Util.mk_sum_casesN n k RS ssubst) THEN' |
28 (rtac (BNF_FP_Util.mk_sum_casesN n k RS ssubst) THEN' |
29 REPEAT_DETERM_N (Int.max (0, m - 1)) o rtac (@{thm split} RS ssubst) THEN' |
29 REPEAT_DETERM_N (Int.max (0, m - 1)) o rtac (@{thm split} RS ssubst) THEN' |
30 rtac refl) 1; |
30 rtac refl) 1; |
31 |
31 |
32 fun mk_exhaust_tac ctxt n ctr_defs fld_iff_unf sumEN' = |
32 fun mk_exhaust_tac ctxt n ctr_defs fld_iff_unf sumEN' = |
33 print_tac "A1" THEN(*###*) |
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 |
|
35 print_tac ("A2: " ^ Display.string_of_thm ctxt sumEN') THEN(*###*) |
|
36 rtac sumEN' 1 THEN |
|
37 print_tac "A3" THEN(*###*) |
|
38 Local_Defs.unfold_tac ctxt @{thms all_prod_eq} THEN |
34 Local_Defs.unfold_tac ctxt @{thms all_prod_eq} THEN |
39 EVERY' (maps (fn k => [select_prem_tac n (rotate_tac 1) k, REPEAT_DETERM o dtac @{thm meta_spec}, |
35 EVERY' (maps (fn k => [select_prem_tac n (rotate_tac 1) k, REPEAT_DETERM o dtac @{thm meta_spec}, |
40 etac @{thm meta_mp}, atac]) (1 upto n)) 1; |
36 etac @{thm meta_mp}, atac]) (1 upto n)) 1; |
41 |
37 |
42 fun mk_fld_iff_unf_tac ctxt cTs cfld cunf fld_unf unf_fld = |
38 fun mk_fld_iff_unf_tac ctxt cTs cfld cunf fld_unf unf_fld = |