65 atac |
65 atac |
66 else |
66 else |
67 REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN' |
67 REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN' |
68 SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac refl)) 1; |
68 SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac refl)) 1; |
69 |
69 |
70 fun mk_expand_tac ctxt |
70 fun mk_expand_tac ctxt n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss |
71 n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss disc_excludesss' = |
71 disc_excludesss' = |
72 if ms = [0] then |
72 if ms = [0] then |
73 rtac (@{thm trans_sym} OF (replicate 2 (the_single uncollapses RS sym))) 1 |
73 (rtac (@{thm trans_sym} OF (replicate 2 (the_single uncollapses))) THEN' |
|
74 TRY o EVERY' [rtac udisc_exhaust, atac, rtac vdisc_exhaust, atac]) 1 |
74 else |
75 else |
75 let |
76 let val ks = 1 upto n in |
76 val ks = 1 upto n; |
|
77 val maybe_atac = if n = 1 then K all_tac else atac; |
|
78 in |
|
79 (rtac udisc_exhaust THEN' |
77 (rtac udisc_exhaust THEN' |
80 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' => |
81 EVERY' [if m = 0 then K all_tac else rtac (uuncollapse RS trans) THEN' maybe_atac, |
79 fn uuncollapse => |
|
80 EVERY' [rtac (uuncollapse RS trans) THEN' TRY o atac, |
82 rtac sym, rtac vdisc_exhaust, |
81 rtac sym, rtac vdisc_exhaust, |
83 EVERY' (map4 (fn k' => fn disc_excludes => fn disc_excludes' => fn vuncollapse => |
82 EVERY' (map4 (fn k' => fn disc_excludes => fn disc_excludes' => fn vuncollapse => |
84 EVERY' |
83 EVERY' |
85 (if k' = k then |
84 (if k' = k then |
86 if m = 0 then |
85 [rtac (vuncollapse RS trans), TRY o atac] @ |
87 [hyp_subst_tac, rtac refl] |
86 (if m = 0 then |
88 else |
87 [rtac refl] |
89 [rtac (vuncollapse RS trans), maybe_atac, |
88 else |
90 if n = 1 then K all_tac else EVERY' [dtac meta_mp, atac, dtac meta_mp, atac], |
89 [if n = 1 then K all_tac else EVERY' [dtac meta_mp, atac, dtac meta_mp, atac], |
91 REPEAT_DETERM_N (Int.max (0, m - 1)) o etac conjE, |
90 REPEAT_DETERM_N (Int.max (0, m - 1)) o etac conjE, |
92 asm_simp_tac (ss_only [] ctxt)] |
91 asm_simp_tac (ss_only [] ctxt)]) |
93 else |
92 else |
94 [dtac (the_single (if k = n then disc_excludes else disc_excludes')), |
93 [dtac (the_single (if k = n then disc_excludes else disc_excludes')), |
95 etac (if k = n then @{thm iff_contradict(1)} else @{thm iff_contradict(2)}), |
94 etac (if k = n then @{thm iff_contradict(1)} else @{thm iff_contradict(2)}), |
96 atac, atac])) |
95 atac, atac])) |
97 ks disc_excludess disc_excludess' uncollapses)]) |
96 ks disc_excludess disc_excludess' uncollapses)]) |