src/HOL/Integ/simproc.ML

added is_draft;
renamed sig to PRIVATE_THEORY;

(*  Title:      HOL/Integ/simproc
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

Apply Abel_Cancel to the integers
*)


(*** Two lemmas needed for the simprocs ***)

(*Deletion of other terms in the formula, seeking the -x at the front of z*)
val zadd_cancel_21 = prove_goal IntDef.thy
    "((x::int) + (y + z) = y + u) = ((x + z) = u)"
  (fn _ => [stac zadd_left_commute 1,
	    rtac zadd_left_cancel 1]);

(*A further rule to deal with the case that
  everything gets cancelled on the right.*)
val zadd_cancel_end = prove_goal IntDef.thy
    "((x::int) + (y + z) = y) = (x = -z)"
  (fn _ => [stac zadd_left_commute 1,
	    res_inst_tac [("t", "y")] (zadd_nat0_right RS subst) 1,
	    stac zadd_left_cancel 1,
	    simp_tac (simpset() addsimps [eq_zdiff_eq RS sym]) 1]);


structure Int_Cancel_Data =
struct
  val ss		= HOL_ss
  val eq_reflection	= eq_reflection

  val thy	= IntDef.thy
  val T		= Type ("IntDef.int", [])
  val zero	= Const ("IntDef.int", HOLogic.natT --> T) $ HOLogic.zero
  val add_cancel_21	= zadd_cancel_21
  val add_cancel_end	= zadd_cancel_end
  val add_left_cancel	= zadd_left_cancel
  val add_assoc		= zadd_assoc
  val add_commute	= zadd_commute
  val add_left_commute	= zadd_left_commute
  val add_0		= zadd_nat0
  val add_0_right	= zadd_nat0_right

  val eq_diff_eq	= eq_zdiff_eq
  val eqI_rules		= [zless_eqI, zeq_eqI, zle_eqI]
  fun dest_eqI th = 
      #1 (HOLogic.dest_bin "op =" HOLogic.boolT 
	      (HOLogic.dest_Trueprop (concl_of th)))

  val diff_def		= zdiff_def
  val minus_add_distrib	= zminus_zadd_distrib
  val minus_minus	= zminus_zminus
  val minus_0		= zminus_nat0
  val add_inverses	= [zadd_zminus_inverse, zadd_zminus_inverse2];
  val cancel_simps	= [zadd_zminus_cancel, zminus_zadd_cancel]
end;

structure Int_Cancel = Abel_Cancel (Int_Cancel_Data);

Addsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv];