131 which cannot be solved by reflexivity. |
131 which cannot be solved by reflexivity. |
132 *) |
132 *) |
133 |
133 |
134 (* replace parameters of product type by individual component parameters *) |
134 (* replace parameters of product type by individual component parameters *) |
135 local |
135 local |
136 fun exists_paired_all prem = (* FIXME check deeper nesting of params!?! *) |
136 fun exists_paired_all (Const ("all", _) $ Abs (_, T, t)) = |
137 Library.exists (can HOLogic.dest_prodT o #2) (Logic.strip_params prem); |
137 can HOLogic.dest_prodT T orelse exists_paired_all t |
138 val ss = HOL_basic_ss |
138 | exists_paired_all (t $ u) = exists_paired_all t orelse exists_paired_all u |
139 addsimps [split_paired_all, unit_all_eq2, unit_abs_eta_conv] |
139 | exists_paired_all (Abs (_, _, t)) = exists_paired_all t |
140 addsimprocs [unit_eq_proc]; |
140 | exists_paired_all _ = false; |
141 val split_tac = full_simp_tac ss; |
141 val split_tac = full_simp_tac |
|
142 (HOL_basic_ss |
|
143 addsimps [split_paired_all, unit_all_eq2, unit_abs_eta_conv] |
|
144 addsimprocs [unit_eq_proc]); |
142 in |
145 in |
143 val split_all_tac = SUBGOAL (fn (prem,i) => |
146 val split_all_tac = SUBGOAL (fn (t, i) => |
144 if exists_paired_all prem then split_tac i else no_tac); |
147 if exists_paired_all t then split_tac i else no_tac); |
145 end; |
148 end; |
146 |
149 |
147 claset_ref() := claset() |
150 claset_ref() := claset() |
148 addSWrapper ("split_all_tac", fn tac2 => split_all_tac ORELSE' tac2); |
151 addSWrapper ("split_all_tac", fn tac2 => split_all_tac ORELSE' tac2); |
149 |
152 |