96 atac, atac])) |
96 atac, atac])) |
97 ks disc_excludess disc_excludess' uncollapses)]) |
97 ks disc_excludess disc_excludess' uncollapses)]) |
98 ks ms disc_excludesss disc_excludesss' uncollapses)) |
98 ks ms disc_excludesss disc_excludesss' uncollapses)) |
99 end; |
99 end; |
100 |
100 |
|
101 fun mk_case_same_ctr_tac ctxt injects = |
|
102 REPEAT_DETERM o etac exE THEN' etac conjE THEN' |
|
103 (case injects of |
|
104 [] => atac |
|
105 | [inject] => dtac (inject RS iffD1) THEN' REPEAT_DETERM o etac conjE THEN' |
|
106 hyp_subst_tac ctxt THEN' rtac refl); |
|
107 |
|
108 fun mk_case_distinct_ctrs_tac ctxt distincts = |
|
109 REPEAT_DETERM o etac exE THEN' etac conjE THEN' full_simp_tac (ss_only distincts ctxt); |
|
110 |
|
111 fun mk_case_tac ctxt n k def injects distinctss = |
|
112 let val ks = 1 upto n in |
|
113 HEADGOAL (rtac (def RS trans) THEN' rtac @{thm the_equality} THEN' rtac (mk_disjIN n k) THEN' |
|
114 REPEAT_DETERM o rtac exI THEN' rtac conjI THEN' rtac refl THEN' rtac refl THEN' |
|
115 EVERY' (map2 (fn k' => fn distincts => |
|
116 (if k' < n then etac disjE else K all_tac) THEN' |
|
117 (if k' = k then mk_case_same_ctr_tac ctxt injects |
|
118 else mk_case_distinct_ctrs_tac ctxt distincts)) ks distinctss)) |
|
119 end; |
|
120 |
101 fun mk_case_conv_tac ctxt n uexhaust cases discss' selss = |
121 fun mk_case_conv_tac ctxt n uexhaust cases discss' selss = |
102 HEADGOAL (rtac uexhaust THEN' |
122 HEADGOAL (rtac uexhaust THEN' |
103 EVERY' (map3 (fn casex => fn if_discs => fn sels => |
123 EVERY' (map3 (fn casex => fn if_discs => fn sels => |
104 EVERY' [hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)), |
124 EVERY' [hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)), |
105 rtac casex]) |
125 rtac casex]) |