src/HOL/Real/simproc.ML
author paulson
Thu Oct 01 18:18:01 1998 +0200 (1998-10-01)
changeset 5588 a3ab526bb891
child 5610 377acd99d74c
permissions -rw-r--r--
Revised version with Abelian group simprocs
     1 (*  Title:      HOL/Real/simproc.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Apply Abel_Cancel to the reals
     7 *)
     8 
     9 (*** Two lemmas needed for the simprocs ***)
    10 
    11 (*Deletion of other terms in the formula, seeking the -x at the front of z*)
    12 val real_add_cancel_21 = prove_goal RealDef.thy
    13     "((x::real) + (y + z) = y + u) = ((x + z) = u)"
    14   (fn _ => [stac real_add_left_commute 1,
    15 	    rtac real_add_left_cancel 1]);
    16 
    17 (*A further rule to deal with the case that
    18   everything gets cancelled on the right.*)
    19 val real_add_cancel_end = prove_goal RealDef.thy
    20     "((x::real) + (y + z) = y) = (x = -z)"
    21   (fn _ => [stac real_add_left_commute 1,
    22 	    res_inst_tac [("t", "y")] (real_add_zero_right RS subst) 1,
    23 	    stac real_add_left_cancel 1,
    24 	    simp_tac (simpset() addsimps [real_eq_diff_eq RS sym]) 1]);
    25 
    26 
    27 structure Real_Cancel_Data =
    28 struct
    29   val ss		= HOL_ss
    30   val mk_eq		= HOLogic.mk_Trueprop o HOLogic.mk_eq
    31   fun mk_meta_eq r	= r RS eq_reflection
    32 
    33   val thy		= RealDef.thy
    34   val T			= Type ("RealDef.real", [])
    35   val zero		= Const ("RealDef.0r", T)
    36   val add_cancel_21	= real_add_cancel_21
    37   val add_cancel_end	= real_add_cancel_end
    38   val add_left_cancel	= real_add_left_cancel
    39   val add_assoc		= real_add_assoc
    40   val add_commute	= real_add_commute
    41   val add_left_commute	= real_add_left_commute
    42   val add_0		= real_add_zero_left
    43   val add_0_right	= real_add_zero_right
    44 
    45   val eq_diff_eq	= real_eq_diff_eq
    46   val eqI_rules		= [real_less_eqI, real_eq_eqI, real_le_eqI]
    47   fun dest_eqI th = 
    48       #1 (HOLogic.dest_bin "op =" HOLogic.boolT 
    49 	      (HOLogic.dest_Trueprop (concl_of th)))
    50 
    51   val diff_def		= real_diff_def
    52   val minus_add_distrib	= real_minus_add_distrib
    53   val minus_minus	= real_minus_minus
    54   val minus_0		= real_minus_zero
    55   val add_inverses	= [real_add_minus, real_add_minus_left];
    56   val cancel_simps	= [real_add_minus_cancel, real_minus_add_cancel]
    57 end;
    58 
    59 structure Real_Cancel = Abel_Cancel (Real_Cancel_Data);
    60 
    61 Addsimprocs [Real_Cancel.sum_conv, Real_Cancel.rel_conv];
    62