if_splits and split_if_asm
authorpaulson
Mon May 21 14:53:30 2001 +0200 (2001-05-21 ago)
changeset 1132392eddd0914a9
parent 11322 6a20952757b2
child 11324 82406bd816a5
if_splits and split_if_asm
src/ZF/simpdata.ML
     1.1 --- a/src/ZF/simpdata.ML	Mon May 21 14:53:11 2001 +0200
     1.2 +++ b/src/ZF/simpdata.ML	Mon May 21 14:53:30 2001 +0200
     1.3 @@ -117,6 +117,14 @@
     1.4  		           addsplits [split_if]
     1.5                             setSolver (mk_solver "types" Type_solver_tac);
     1.6  
     1.7 +(** Splitting IFs in the assumptions **)
     1.8 +
     1.9 +Goal "P(if Q then x else y) <-> (~((Q & ~P(x)) | (~Q & ~P(y))))";
    1.10 +by (Simp_tac 1); 
    1.11 +qed "split_if_asm";   
    1.12 +
    1.13 +bind_thms ("if_splits", [split_if, split_if_asm]);
    1.14 +
    1.15  (** One-point rule for bounded quantifiers: see HOL/Set.ML **)
    1.16  
    1.17  Goal "(EX x:A. x=a) <-> (a:A)";