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