56 (* replace parameters of product type by individual component parameters *) |
56 (* replace parameters of product type by individual component parameters *) |
57 local |
57 local |
58 fun is_pair (_,Type("*",_)) = true |
58 fun is_pair (_,Type("*",_)) = true |
59 | is_pair _ = false; |
59 | is_pair _ = false; |
60 |
60 |
61 fun find_pair_param t = |
61 fun find_pair_param prem = |
62 let val params = Logic.strip_params t |
62 let val params = Logic.strip_params prem |
63 in if exists is_pair params |
63 in if exists is_pair params |
64 then let val params = rev(rename_wrt_term t params) |
64 then let val params = rev(rename_wrt_term prem params) |
65 (*as they are printed*) |
65 (*as they are printed*) |
66 in apsome fst (find_first is_pair params) end |
66 in apsome fst (find_first is_pair params) end |
67 else None |
67 else None |
68 end; |
68 end; |
69 |
69 |
70 in |
70 in |
71 |
71 |
72 val split_all_tac = REPEAT o SUBGOAL (fn (t,_) => |
72 val split_all_tac = REPEAT o SUBGOAL (fn (prem,i) => |
73 case find_pair_param t of |
73 case find_pair_param prem of |
74 None => no_tac |
74 None => no_tac |
75 | Some x => EVERY[res_inst_tac[("p",x)] PairE 1, |
75 | Some x => EVERY[res_inst_tac[("p",x)] PairE i, |
76 REPEAT(hyp_subst_tac 1), prune_params_tac]); |
76 REPEAT(hyp_subst_tac i), prune_params_tac]); |
77 |
77 |
78 end; |
78 end; |
79 |
79 |
80 goal Prod.thy "(!x. P x) = (!a b. P(a,b))"; |
80 goal Prod.thy "(!x. P x) = (!a b. P(a,b))"; |
81 by (fast_tac (HOL_cs addbefore split_all_tac 1) 1); |
81 by (fast_tac (HOL_cs addbefore split_all_tac 1) 1); |