39 |
39 |
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 NONE [other_disc_def], rtac @{thm iffI_np}, REPEAT_DETERM o etac exE, |
45 hyp_subst_tac, SELECT_GOAL (unfold_thms_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 |
74 val ks = 1 upto n; |
74 val ks = 1 upto n; |
75 val maybe_atac = if n = 1 then K all_tac else atac; |
75 val maybe_atac = if n = 1 then K all_tac else atac; |
76 in |
76 in |
77 (rtac udisc_exhaust THEN' |
77 (rtac udisc_exhaust THEN' |
78 EVERY' (map5 (fn k => fn m => fn disc_excludess => fn disc_excludess' => fn uuncollapse => |
78 EVERY' (map5 (fn k => fn m => fn disc_excludess => fn disc_excludess' => fn uuncollapse => |
79 EVERY' [if m = 0 then K all_tac else subst_tac ctxt [uuncollapse] THEN' maybe_atac, |
79 EVERY' [if m = 0 then K all_tac else subst_tac ctxt NONE [uuncollapse] THEN' maybe_atac, |
80 rtac sym, rtac vdisc_exhaust, |
80 rtac sym, rtac vdisc_exhaust, |
81 EVERY' (map4 (fn k' => fn disc_excludes => fn disc_excludes' => fn vuncollapse => |
81 EVERY' (map4 (fn k' => fn disc_excludes => fn disc_excludes' => fn vuncollapse => |
82 EVERY' |
82 EVERY' |
83 (if k' = k then |
83 (if k' = k then |
84 if m = 0 then |
84 if m = 0 then |
85 [hyp_subst_tac, rtac refl] |
85 [hyp_subst_tac, rtac refl] |
86 else |
86 else |
87 [subst_tac ctxt [vuncollapse], maybe_atac, |
87 [subst_tac ctxt NONE [vuncollapse], maybe_atac, |
88 if n = 1 then K all_tac else EVERY' [dtac meta_mp, atac, dtac meta_mp, atac], |
88 if n = 1 then K all_tac else EVERY' [dtac meta_mp, atac, dtac meta_mp, atac], |
89 REPEAT_DETERM_N (Int.max (0, m - 1)) o etac conjE, asm_simp_tac (ss_only [])] |
89 REPEAT_DETERM_N (Int.max (0, m - 1)) o etac conjE, asm_simp_tac (ss_only [])] |
90 else |
90 else |
91 [dtac (the_single (if k = n then disc_excludes else disc_excludes')), |
91 [dtac (the_single (if k = n then disc_excludes else disc_excludes')), |
92 etac (if k = n then @{thm iff_contradict(1)} else @{thm iff_contradict(2)}), |
92 etac (if k = n then @{thm iff_contradict(1)} else @{thm iff_contradict(2)}), |
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; |
107 |
107 |
108 val naked_ctxt = Proof_Context.init_global @{theory HOL}; |
108 val naked_ctxt = Proof_Context.init_global @{theory HOL}; |
109 |
109 |
|
110 (* TODO: More precise "simp_thms"; get rid of "blast_tac" *) |
110 fun mk_split_tac uexhaust cases injectss distinctsss = |
111 fun mk_split_tac uexhaust cases injectss distinctsss = |
111 rtac uexhaust 1 THEN |
112 rtac uexhaust 1 THEN |
112 ALLGOALS (fn k => (hyp_subst_tac THEN' |
113 ALLGOALS (fn k => (hyp_subst_tac THEN' |
113 simp_tac (ss_only (@{thms simp_thms} @ cases @ nth injectss (k - 1) @ |
114 simp_tac (ss_only (@{thms simp_thms} @ cases @ nth injectss (k - 1) @ |
114 flat (nth distinctsss (k - 1))))) k) THEN |
115 flat (nth distinctsss (k - 1))))) k) THEN |