40 fun mk_unique_disc_def_tac m uexhaust = |
40 fun mk_unique_disc_def_tac m uexhaust = |
41 EVERY' [rtac iffI, rtac uexhaust, REPEAT_DETERM_N m o rtac exI, atac, rtac refl] 1; |
41 EVERY' [rtac iffI, rtac uexhaust, REPEAT_DETERM_N m o rtac exI, atac, rtac refl] 1; |
42 |
42 |
43 fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct uexhaust = |
43 fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct uexhaust = |
44 EVERY' ([subst_tac ctxt [other_disc_def], rtac @{thm iffI_np}, REPEAT_DETERM o etac exE, |
44 EVERY' ([subst_tac ctxt [other_disc_def], rtac @{thm iffI_np}, REPEAT_DETERM o etac exE, |
45 hyp_subst_tac, SELECT_GOAL (unfold_defs_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI, |
45 hyp_subst_tac, SELECT_GOAL (unfold_thms_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI, |
46 rtac distinct, rtac uexhaust] @ |
46 rtac distinct, rtac uexhaust] @ |
47 (([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac]) |
47 (([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac]) |
48 |> k = 1 ? swap |> op @)) 1; |
48 |> k = 1 ? swap |> op @)) 1; |
49 |
49 |
50 fun mk_half_disc_exclude_tac m discD disc' = |
50 fun mk_half_disc_exclude_tac m discD disc' = |
61 (dtac discD THEN' |
61 (dtac discD THEN' |
62 (if m = 0 then |
62 (if m = 0 then |
63 atac |
63 atac |
64 else |
64 else |
65 REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN' |
65 REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN' |
66 SELECT_GOAL (unfold_defs_tac ctxt sels) THEN' rtac refl)) 1; |
66 SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac refl)) 1; |
67 |
67 |
68 fun mk_expand_tac ctxt n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss |
68 fun mk_expand_tac ctxt n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss |
69 disc_excludesss' = |
69 disc_excludesss' = |
70 if ms = [0] then |
70 if ms = [0] then |
71 rtac (@{thm trans_sym} OF (replicate 2 (the_single uncollapses RS sym))) 1 |
71 rtac (@{thm trans_sym} OF (replicate 2 (the_single uncollapses RS sym))) 1 |
96 end; |
96 end; |
97 |
97 |
98 fun mk_case_eq_tac ctxt n uexhaust cases discss' selss = |
98 fun mk_case_eq_tac ctxt n uexhaust cases discss' selss = |
99 (rtac uexhaust THEN' |
99 (rtac uexhaust THEN' |
100 EVERY' (map3 (fn casex => fn if_discs => fn sels => |
100 EVERY' (map3 (fn casex => fn if_discs => fn sels => |
101 EVERY' [hyp_subst_tac, SELECT_GOAL (unfold_defs_tac ctxt (if_discs @ sels)), rtac casex]) |
101 EVERY' [hyp_subst_tac, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)), rtac casex]) |
102 cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss)) 1; |
102 cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss)) 1; |
103 |
103 |
104 fun mk_case_cong_tac uexhaust cases = |
104 fun mk_case_cong_tac uexhaust cases = |
105 (rtac uexhaust THEN' |
105 (rtac uexhaust THEN' |
106 EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex])]) cases)) 1; |
106 EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex])]) cases)) 1; |