added split_sum_case_asm
authoroheimb
Tue Jun 02 15:07:00 1998 +0200 (1998-06-02)
changeset 49888f4dc836a2ea
parent 4987 257aeccdefc3
child 4989 857dabe71d72
added split_sum_case_asm
src/HOL/Sum.ML
     1.1 --- a/src/HOL/Sum.ML	Fri May 29 13:50:21 1998 +0200
     1.2 +++ b/src/HOL/Sum.ML	Tue Jun 02 15:07:00 1998 +0200
     1.3 @@ -152,6 +152,11 @@
     1.4  by Auto_tac;
     1.5  qed "split_sum_case";
     1.6  
     1.7 +qed_goal "split_sum_case_asm" Sum.thy "P (sum_case f g s) = \
     1.8 +\ (~((? x. s = Inl x & ~P (f x)) | (? y. s = Inr y & ~P (g y))))"
     1.9 +    (K [stac split_sum_case 1,
    1.10 +	Blast_tac 1]);
    1.11 +
    1.12  (*Prevents simplification of f and g: much faster*)
    1.13  qed_goal "sum_case_weak_cong" Sum.thy
    1.14    "s=t ==> sum_case f g s = sum_case f g t"