# HG changeset patch
# User nipkow
# Date 1187112207 -7200
# Node ID bdb48fd8fbdd9ed61f0f44b9f23eb7e18758fcd0
# Parent  4d5917cc60c4da92a9b715ef3985ede82907999d
extended linear arith capabilities with code by Amine

diff -r 4d5917cc60c4 -r bdb48fd8fbdd src/HOL/int_arith1.ML
--- a/src/HOL/int_arith1.ML	Tue Aug 14 15:09:33 2007 +0200
+++ b/src/HOL/int_arith1.ML	Tue Aug 14 19:23:27 2007 +0200
@@ -570,7 +570,66 @@
 (* Update parameters of arithmetic prover *)
 local
 
-(* reduce contradictory <= to False *)
+(* reduce contradictory =/</<= to False *)
+
+(* Evaluation of terms of the form "m R n" where R is one of "=", "<=" or "<",
+   and m and n are ground terms over rings (roughly speaking).
+   That is, m and n consist only of 1s combined with "+", "-" and "*".
+*)
+local
+val zeroth = (symmetric o mk_meta_eq) @{thm of_int_0};
+val lhss0 = [@{cpat "0::?'a::ring"}];
+fun proc0 phi ss ct =
+  let val T = ctyp_of_term ct
+  in if typ_of T = @{typ int} then NONE else
+     SOME (instantiate' [SOME T] [] zeroth)
+  end;
+val zero_to_of_int_zero_simproc =
+  make_simproc {lhss = lhss0, name = "zero_to_of_int_zero_simproc",
+  proc = proc0, identifier = []};
+
+val oneth = (symmetric o mk_meta_eq) @{thm of_int_1};
+val lhss1 = [@{cpat "1::?'a::ring_1"}];
+fun proc1 phi ss ct =
+  let val T = ctyp_of_term ct
+  in if typ_of T = @{typ int} then NONE else
+     SOME (instantiate' [SOME T] [] oneth)
+  end;
+val one_to_of_int_one_simproc =
+  make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
+  proc = proc1, identifier = []};
+
+val allowed_consts =
+  [@{const_name "op ="}, @{const_name "HOL.times"}, @{const_name "HOL.uminus"},
+   @{const_name "HOL.minus"}, @{const_name "HOL.plus"},
+   @{const_name "HOL.zero"}, @{const_name "HOL.one"}, @{const_name "HOL.less"},
+   @{const_name "HOL.less_eq"}];
+
+fun check t = case t of
+   Const(s,t) => if s = @{const_name "HOL.one"} then not (t = @{typ int})
+                else s mem_string allowed_consts
+ | a$b => check a andalso check b
+ | _ => false;
+
+val conv =
+  Simplifier.rewrite
+   (HOL_basic_ss addsimps
+     ((map (fn th => th RS sym) [@{thm of_int_add}, @{thm of_int_mult},
+             @{thm of_int_diff},  @{thm of_int_minus}])@
+      [@{thm of_int_less_iff}, @{thm of_int_le_iff}, @{thm of_int_eq_iff}])
+     addsimprocs [zero_to_of_int_zero_simproc,one_to_of_int_one_simproc]);
+
+fun sproc phi ss ct = if check (term_of ct) then SOME (conv ct) else NONE
+val lhss' =
+  [@{cpat "(?x::?'a::ring_char_0) = (?y::?'a)"},
+   @{cpat "(?x::?'a::ordered_idom) < (?y::?'a)"},
+   @{cpat "(?x::?'a::ordered_idom) <= (?y::?'a)"}]
+in
+val zero_one_idom_simproc =
+  make_simproc {lhss = lhss' , name = "zero_one_idom_simproc",
+  proc = sproc, identifier = []}
+end;
+
 val add_rules =
     simp_thms @ arith_simps @ rel_simps @ arith_special @
     [@{thm neg_le_iff_le}, @{thm numeral_0_eq_0}, @{thm numeral_1_eq_1},
@@ -584,7 +643,7 @@
 
 val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
 
-val Int_Numeral_Base_Simprocs = assoc_fold_simproc
+val Int_Numeral_Base_Simprocs = assoc_fold_simproc :: zero_one_idom_simproc
   :: Int_Numeral_Simprocs.combine_numerals
   :: Int_Numeral_Simprocs.cancel_numerals;