equal
deleted
inserted
replaced
138 ORELSE EVERY1 [resolve_tac prems, |
138 ORELSE EVERY1 [resolve_tac prems, |
139 etac subst, |
139 etac subst, |
140 rtac (Rep_Sum_inverse RS sym)])); |
140 rtac (Rep_Sum_inverse RS sym)])); |
141 qed "sumE"; |
141 qed "sumE"; |
142 |
142 |
|
143 val prems = goal thy "[| !!x. P (Inl x); !!x. P (Inr x) |] ==> P x"; |
|
144 by (res_inst_tac [("s","x")] sumE 1); |
|
145 by (ALLGOALS (hyp_subst_tac THEN' (resolve_tac prems))); |
|
146 qed "sum_induct"; |
|
147 |
143 Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)"; |
148 Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)"; |
144 by (EVERY1 [res_inst_tac [("s","s")] sumE, |
149 by (EVERY1 [res_inst_tac [("s","s")] sumE, |
145 etac ssubst, rtac sum_case_Inl, |
150 etac ssubst, rtac sum_case_Inl, |
146 etac ssubst, rtac sum_case_Inr]); |
151 etac ssubst, rtac sum_case_Inr]); |
147 qed "surjective_sum"; |
152 qed "surjective_sum"; |