(* Title: HOL/Real/simproc.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
Apply Abel_Cancel to the reals
*)
(*** Two lemmas needed for the simprocs ***)
(*Deletion of other terms in the formula, seeking the -x at the front of z*)
val real_add_cancel_21 = prove_goal RealDef.thy
"((x::real) + (y + z) = y + u) = ((x + z) = u)"
(fn _ => [stac real_add_left_commute 1,
rtac real_add_left_cancel 1]);
(*A further rule to deal with the case that
everything gets cancelled on the right.*)
val real_add_cancel_end = prove_goal RealDef.thy
"((x::real) + (y + z) = y) = (x = -z)"
(fn _ => [stac real_add_left_commute 1,
res_inst_tac [("t", "y")] (real_add_zero_right RS subst) 1,
stac real_add_left_cancel 1,
simp_tac (simpset() addsimps [real_eq_diff_eq RS sym]) 1]);
structure Real_Cancel_Data =
struct
val ss = HOL_ss
val eq_reflection = eq_reflection
val thy = RealDef.thy
val T = Type ("RealDef.real", [])
val zero = Const ("RealDef.0r", T)
val add_cancel_21 = real_add_cancel_21
val add_cancel_end = real_add_cancel_end
val add_left_cancel = real_add_left_cancel
val add_assoc = real_add_assoc
val add_commute = real_add_commute
val add_left_commute = real_add_left_commute
val add_0 = real_add_zero_left
val add_0_right = real_add_zero_right
val eq_diff_eq = real_eq_diff_eq
val eqI_rules = [real_less_eqI, real_eq_eqI, real_le_eqI]
fun dest_eqI th =
#1 (HOLogic.dest_bin "op =" HOLogic.boolT
(HOLogic.dest_Trueprop (concl_of th)))
val diff_def = real_diff_def
val minus_add_distrib = real_minus_add_distrib
val minus_minus = real_minus_minus
val minus_0 = real_minus_zero
val add_inverses = [real_add_minus, real_add_minus_left];
val cancel_simps = [real_add_minus_cancel, real_minus_add_cancel]
end;
structure Real_Cancel = Abel_Cancel (Real_Cancel_Data);
Addsimprocs [Real_Cancel.sum_conv, Real_Cancel.rel_conv];