# HG changeset patch
# User wenzelm
# Date 880559065 -3600
# Node ID 81132a38996a1100d4f1f9a2dabaee978e0d207c
# Parent  7fe9723d579bb4d6a38e6f8349bdbfb9e1178d3f
Setup various arithmetic proof procedures.

diff -r 7fe9723d579b -r 81132a38996a src/HOL/arith_data.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/arith_data.ML	Wed Nov 26 16:44:25 1997 +0100
@@ -0,0 +1,194 @@
+(*  Title:      HOL/arith_data.ML
+    ID:         $Id$
+    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
+
+Setup various arithmetic proof procedures.
+*)
+
+signature ARITH_DATA =
+sig
+  val nat_cancel: simproc list
+end;
+
+structure ArithData (* FIXME :ARITH_DATA *) =
+struct
+
+
+(** abstract syntax of structure nat: 0, Suc, + **)
+
+(* mk_sum *)
+
+val mk_plus = HOLogic.mk_binop "op +";
+
+fun mk_sum [] = HOLogic.zero
+  | mk_sum [t] = t
+  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
+
+
+(* dest_sum *)
+
+val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
+val one = HOLogic.mk_nat 1;
+
+fun dest_sum tm =
+  if HOLogic.is_zero tm then []
+  else
+    (case try HOLogic.dest_Suc tm of
+      Some t => one :: dest_sum t
+    | None =>
+        (case try dest_plus tm of
+          Some (t, u) => dest_sum t @ dest_sum u
+        | None => [tm]));
+
+
+(** generic proof tools **)
+
+(* prove conversions *)
+
+val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
+
+fun prove_conv expand_tac norm_tac sg (t, u) =
+  mk_meta_eq (prove_goalw_cterm [] (cterm_of sg (mk_eqv (t, u)))
+    (K [expand_tac, norm_tac]))
+  handle ERROR => error ("The error(s) above occurred while trying to prove " ^
+    (string_of_cterm (cterm_of sg (mk_eqv (t, u)))));
+
+val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s"
+  (fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]);
+
+
+(* rewriting *)
+
+fun simp_all rules = ALLGOALS (simp_tac (HOL_ss addsimps rules));
+
+val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right];
+val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right];
+
+
+
+(** cancel common summands **)
+
+structure Sum =
+struct
+  val mk_sum = mk_sum;
+  val dest_sum = dest_sum;
+  val prove_conv = prove_conv;
+  val norm_tac = simp_all add_rules THEN simp_all add_ac;
+end;
+
+fun gen_uncancel_tac rule ct =
+  rtac (instantiate' [] [None, Some ct] (rule RS subst_equals)) 1;
+
+
+(* nat eq *)
+
+structure EqCancelSums = CancelSumsFun
+(struct
+  open Sum;
+  val mk_bal = HOLogic.mk_eq;
+  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
+  val uncancel_tac = gen_uncancel_tac add_left_cancel;
+end);
+
+
+(* nat less *)
+
+structure LessCancelSums = CancelSumsFun
+(struct
+  open Sum;
+  val mk_bal = HOLogic.mk_binrel "op <";
+  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;
+  val uncancel_tac = gen_uncancel_tac add_left_cancel_less;
+end);
+
+
+(* nat le *)
+
+structure LeCancelSums = CancelSumsFun
+(struct
+  open Sum;
+  val mk_bal = HOLogic.mk_binrel "op <=";
+  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;
+  val uncancel_tac = gen_uncancel_tac add_left_cancel_le;
+end);
+
+
+(* nat diff *)
+
+(* FIXME *)
+
+
+
+(** cancel common factor **)
+
+structure Factor =
+struct
+  val mk_sum = mk_sum;
+  val dest_sum = dest_sum;
+  val prove_conv = prove_conv;
+  val norm_tac = simp_all (add_rules @ mult_rules) THEN simp_all add_ac;
+end;
+
+fun mk_cnat n = cterm_of (sign_of Nat.thy) (HOLogic.mk_nat n);
+
+fun gen_multiply_tac rule k =
+  if k > 0 then
+    rtac (instantiate' [] [None, Some (mk_cnat (k - 1))] (rule RS subst_equals)) 1
+  else no_tac;
+
+
+(* nat eq *)
+
+structure EqCancelFactor = CancelFactorFun
+(struct
+  open Factor;
+  val mk_bal = HOLogic.mk_eq;
+  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
+  val multiply_tac = gen_multiply_tac Suc_mult_cancel1;
+end);
+
+
+(* nat less *)
+
+structure LessCancelFactor = CancelFactorFun
+(struct
+  open Factor;
+  val mk_bal = HOLogic.mk_binrel "op <";
+  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;
+  val multiply_tac = gen_multiply_tac Suc_mult_less_cancel1;
+end);
+
+
+(* nat le *)
+
+structure LeCancelFactor = CancelFactorFun
+(struct
+  open Factor;
+  val mk_bal = HOLogic.mk_binrel "op <=";
+  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;
+  val multiply_tac = gen_multiply_tac Suc_mult_le_cancel1;
+end);
+
+
+
+(** prepare nat_cancel simprocs **)
+
+fun prep_pat s = Thm.read_cterm (sign_of Arith.thy) (s, HOLogic.termTVar);
+val prep_pats = map prep_pat;
+
+fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
+
+val eq_pats = prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"];
+val less_pats = prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"];
+val le_pats = prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"];
+
+val nat_cancel = map prep_simproc
+  [("nateq_cancel_factor", eq_pats, EqCancelFactor.proc),
+   ("natless_cancel_factor", less_pats, LessCancelFactor.proc),
+   ("natle_cancel_factor", le_pats, LeCancelFactor.proc),
+   ("nateq_cancel_sums", eq_pats, EqCancelSums.proc),
+   ("natless_cancel_sums", less_pats, LessCancelSums.proc),
+   ("natle_cancel_sums", le_pats, LeCancelSums.proc)];
+
+
+end;