addsplits now in FOL, ZF too
authorpaulson
Fri Nov 28 10:54:13 1997 +0100 (1997-11-28 ago)
changeset 4325e72cba5af6c5
parent 4324 9bfac4684f2f
child 4326 7211ea5f29e2
addsplits now in FOL, ZF too
NEWS
src/FOL/simpdata.ML
     1.1 --- a/NEWS	Fri Nov 28 10:52:32 1997 +0100
     1.2 +++ b/NEWS	Fri Nov 28 10:54:13 1997 +0100
     1.3 @@ -89,6 +89,10 @@
     1.4  
     1.5  * added prems argument to simplification procedures;
     1.6  
     1.7 +* HOL, FOL, ZF: added infix function `addsplits':
     1.8 +  instead of `<simpset> setloop (split_tac <thms>)'
     1.9 +  you can simply write `<simpset> addsplits <thms>'
    1.10 +
    1.11  
    1.12  *** Syntax ***
    1.13  
    1.14 @@ -113,16 +117,12 @@
    1.15  
    1.16  * HOL/Map: new theory of `maps' a la VDM;
    1.17  
    1.18 -* HOL/simplifier: added infix function `addsplits':
    1.19 -  instead of `<simpset> setloop (split_tac <thms>)'
    1.20 -  you can simply write `<simpset> addsplits <thms>'
    1.21 -
    1.22  * HOL/simplifier: terms of the form
    1.23 -  `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)' (or t=x)
    1.24 +  `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)'  (or t=x)
    1.25    are rewritten to
    1.26    `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t)',
    1.27    and those of the form
    1.28 -  `! x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x) --> R(x)' (or t=x)
    1.29 +  `! x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x) --> R(x)'  (or t=x)
    1.30    are rewritten to
    1.31    `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t) --> R(t)',
    1.32  
     2.1 --- a/src/FOL/simpdata.ML	Fri Nov 28 10:52:32 1997 +0100
     2.2 +++ b/src/FOL/simpdata.ML	Fri Nov 28 10:54:13 1997 +0100
     2.3 @@ -186,6 +186,8 @@
     2.4  val split_asm_tac = mk_case_split_asm_tac split_tac 
     2.5  			(disjE,conjE,exE,contrapos,contrapos2,notnotD);
     2.6  
     2.7 +
     2.8 +
     2.9  (*** Standard simpsets ***)
    2.10  
    2.11  structure Induction = InductionFun(struct val spec=IFOL.spec end);
    2.12 @@ -202,6 +204,9 @@
    2.13  fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
    2.14  fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
    2.15  
    2.16 +infix 4 addsplits;
    2.17 +fun ss addsplits splits = ss addloop (split_tac splits);
    2.18 +
    2.19  val IFOL_simps =
    2.20     [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
    2.21      imp_simps @ iff_simps @ quant_simps;