Sets new component "restrict_to_left"
authorpaulson
Thu Sep 23 13:07:25 1999 +0200 (1999-09-23 ago)
changeset 7585dca904d4ce4c
parent 7584 5be4bb8e4e3f
child 7586 ae28545cd104
Sets new component "restrict_to_left"
src/HOL/Integ/simproc.ML
src/HOL/Real/simproc.ML
     1.1 --- a/src/HOL/Integ/simproc.ML	Thu Sep 23 13:06:31 1999 +0200
     1.2 +++ b/src/HOL/Integ/simproc.ML	Thu Sep 23 13:07:25 1999 +0200
     1.3 @@ -7,22 +7,24 @@
     1.4  *)
     1.5  
     1.6  
     1.7 -(*** Two lemmas needed for the simprocs ***)
     1.8 +(*** Lemmas needed for the simprocs ***)
     1.9  
    1.10  (*Deletion of other terms in the formula, seeking the -x at the front of z*)
    1.11 -val zadd_cancel_21 = prove_goal IntDef.thy
    1.12 -    "((x::int) + (y + z) = y + u) = ((x + z) = u)"
    1.13 -  (fn _ => [stac zadd_left_commute 1,
    1.14 -	    rtac zadd_left_cancel 1]);
    1.15 +Goal "((x::int) + (y + z) = y + u) = ((x + z) = u)";
    1.16 +by (stac zadd_left_commute 1);
    1.17 +by (rtac zadd_left_cancel 1);
    1.18 +qed "zadd_cancel_21";
    1.19  
    1.20  (*A further rule to deal with the case that
    1.21    everything gets cancelled on the right.*)
    1.22 -val zadd_cancel_end = prove_goal IntDef.thy
    1.23 -    "((x::int) + (y + z) = y) = (x = -z)"
    1.24 -  (fn _ => [stac zadd_left_commute 1,
    1.25 -	    res_inst_tac [("t", "y")] (zadd_int0_right RS subst) 1,
    1.26 -	    stac zadd_left_cancel 1,
    1.27 -	    simp_tac (simpset() addsimps [eq_zdiff_eq RS sym]) 1]);
    1.28 +Goal "((x::int) + (y + z) = y) = (x = -z)";
    1.29 +by (stac zadd_left_commute 1);
    1.30 +by (res_inst_tac [("t", "y")] (zadd_int0_right RS subst) 1
    1.31 +    THEN stac zadd_left_cancel 1);
    1.32 +by (simp_tac (simpset() addsimps [eq_zdiff_eq RS sym]) 1);
    1.33 +qed "zadd_cancel_end";
    1.34 +
    1.35 +
    1.36  
    1.37  
    1.38  structure Int_Cancel_Data =
    1.39 @@ -33,6 +35,7 @@
    1.40    val thy	= IntDef.thy
    1.41    val T		= HOLogic.intT
    1.42    val zero	= Const ("IntDef.int", HOLogic.natT --> T) $ HOLogic.zero
    1.43 +  val restrict_to_left  = restrict_to_left
    1.44    val add_cancel_21	= zadd_cancel_21
    1.45    val add_cancel_end	= zadd_cancel_end
    1.46    val add_left_cancel	= zadd_left_cancel
     2.1 --- a/src/HOL/Real/simproc.ML	Thu Sep 23 13:06:31 1999 +0200
     2.2 +++ b/src/HOL/Real/simproc.ML	Thu Sep 23 13:07:25 1999 +0200
     2.3 @@ -9,19 +9,19 @@
     2.4  (*** Two lemmas needed for the simprocs ***)
     2.5  
     2.6  (*Deletion of other terms in the formula, seeking the -x at the front of z*)
     2.7 -val real_add_cancel_21 = prove_goal RealDef.thy
     2.8 -    "((x::real) + (y + z) = y + u) = ((x + z) = u)"
     2.9 -  (fn _ => [stac real_add_left_commute 1,
    2.10 -	    rtac real_add_left_cancel 1]);
    2.11 +Goal "((x::real) + (y + z) = y + u) = ((x + z) = u)";
    2.12 +by (stac real_add_left_commute 1);
    2.13 +by (rtac real_add_left_cancel 1);
    2.14 +qed "real_add_cancel_21";
    2.15  
    2.16  (*A further rule to deal with the case that
    2.17    everything gets cancelled on the right.*)
    2.18 -val real_add_cancel_end = prove_goal RealDef.thy
    2.19 -    "((x::real) + (y + z) = y) = (x = -z)"
    2.20 -  (fn _ => [stac real_add_left_commute 1,
    2.21 -	    res_inst_tac [("t", "y")] (real_add_zero_right RS subst) 1,
    2.22 -	    stac real_add_left_cancel 1,
    2.23 -	    simp_tac (simpset() addsimps [real_eq_diff_eq RS sym]) 1]);
    2.24 +Goal "((x::real) + (y + z) = y) = (x = -z)";
    2.25 +by (stac real_add_left_commute 1);
    2.26 +by (res_inst_tac [("t", "y")] (real_add_zero_right RS subst) 1
    2.27 +    THEN stac real_add_left_cancel 1);
    2.28 +by (simp_tac (simpset() addsimps [real_eq_diff_eq RS sym]) 1);
    2.29 +qed "real_add_cancel_end";
    2.30  
    2.31  
    2.32  structure Real_Cancel_Data =
    2.33 @@ -32,6 +32,7 @@
    2.34    val thy		= RealDef.thy
    2.35    val T			= Type ("RealDef.real", [])
    2.36    val zero		= Const ("RealDef.0r", T)
    2.37 +  val restrict_to_left  = restrict_to_left
    2.38    val add_cancel_21	= real_add_cancel_21
    2.39    val add_cancel_end	= real_add_cancel_end
    2.40    val add_left_cancel	= real_add_left_cancel