176 in |
176 in |
177 flatten' f (names, prems) |
177 flatten' f (names, prems) |
178 |> maps (fn (res, (names, prems)) => |
178 |> maps (fn (res, (names, prems)) => |
179 flatten' (betapply (g, res)) (names, prems)) |
179 flatten' (betapply (g, res)) (names, prems)) |
180 end) |
180 end) |
181 | Const (@{const_name prod_case}, _) => |
|
182 (let |
|
183 val (_, g :: res :: args) = strip_comb t |
|
184 val [res1, res2] = Name.variant_list names ["res1", "res2"] |
|
185 val (T1, T2) = HOLogic.dest_prodT (fastype_of res) |
|
186 val (resv1, resv2) = (Free (res1, T1), Free (res2, T2)) |
|
187 in |
|
188 flatten' (betapplys (g, (resv1 :: resv2 :: args))) |
|
189 (res1 :: res2 :: names, |
|
190 HOLogic.mk_Trueprop (HOLogic.mk_eq (res, HOLogic.mk_prod (resv1, resv2))) :: prems) |
|
191 end) |
|
192 | _ => |
181 | _ => |
193 case find_split_thm thy (fst (strip_comb t)) of |
182 case find_split_thm thy (fst (strip_comb t)) of |
194 SOME raw_split_thm => |
183 SOME raw_split_thm => |
195 let |
184 let |
196 val (f, args) = strip_comb t |
185 val (f, args) = strip_comb t |