equal
deleted
inserted
replaced
150 \ ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y))))"; |
150 \ ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y))))"; |
151 by (res_inst_tac [("s","s")] sumE 1); |
151 by (res_inst_tac [("s","s")] sumE 1); |
152 by Auto_tac; |
152 by Auto_tac; |
153 qed "split_sum_case"; |
153 qed "split_sum_case"; |
154 |
154 |
|
155 qed_goal "split_sum_case_asm" Sum.thy "P (sum_case f g s) = \ |
|
156 \ (~((? x. s = Inl x & ~P (f x)) | (? y. s = Inr y & ~P (g y))))" |
|
157 (K [stac split_sum_case 1, |
|
158 Blast_tac 1]); |
|
159 |
155 (*Prevents simplification of f and g: much faster*) |
160 (*Prevents simplification of f and g: much faster*) |
156 qed_goal "sum_case_weak_cong" Sum.thy |
161 qed_goal "sum_case_weak_cong" Sum.thy |
157 "s=t ==> sum_case f g s = sum_case f g t" |
162 "s=t ==> sum_case f g s = sum_case f g t" |
158 (fn [prem] => [rtac (prem RS arg_cong) 1]); |
163 (fn [prem] => [rtac (prem RS arg_cong) 1]); |
159 |
164 |