More arith refinements.

--- a/src/HOL/Arith.ML	Thu Jan 14 12:32:13 1999 +0100
+++ b/src/HOL/Arith.ML	Thu Jan 14 13:18:09 1999 +0100
@@ -853,8 +853,11 @@
 val notI = notI;
 val sym = sym;
 val not_lessD = linorder_not_less RS iffD1;
+val not_leD = linorder_not_le RS iffD1;
 
-val mk_Eq = mk_eq;
+
+fun mk_Eq thm = (thm RS Eq_FalseI) handle _ => (thm RS Eq_TrueI);
+
 val mk_Trueprop = HOLogic.mk_Trueprop;
 
 fun neg_prop(TP$(Const("Not",_)$t)) = TP$t
@@ -864,13 +867,18 @@
   let val _ $ t = #prop(rep_thm thm)
   in t = Const("False",HOLogic.boolT) end;
 
+fun is_nat(t) = fastype_of1 t = HOLogic.natT;
+
+fun mk_nat_thm sg t =
+  let val ct = cterm_of sg t  and cn = cterm_of sg (Var(("n",0),HOLogic.natT))
+  in instantiate ([],[(cn,ct)]) le0 end;
+
 end;
 
-structure Nat_LA_Data: LIN_ARITH_DATA =
+structure Nat_LA_Data (* : LIN_ARITH_DATA *) =
 struct
 
-val lessD = Suc_leI;
-val not_leD = not_leE RS Suc_leI;
+val lessD = [Suc_leI];
 
 (* Turn term into list of summand * multiplicity plus a constant *)
 fun poly(Const("Suc",_)$t, (p,i)) = poly(t, (p,i+1))
@@ -882,8 +890,7 @@
 
 fun nnb T = T = ([HOLogic.natT,HOLogic.natT] ---> HOLogic.boolT);
 
-fun decomp2(rel,T,lhs,rhs) =
-  if not(nnb T) then None else
+fun decomp2(rel,lhs,rhs) =
   let val (p,i) = poly(lhs,([],0)) and (q,j) = poly(rhs,([],0))
   in case rel of
        "op <"  => Some(p,i,"<",q,j)
@@ -895,9 +902,11 @@
 fun negate(Some(x,i,rel,y,j)) = Some(x,i,"~"^rel,y,j)
   | negate None = None;
 
-fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp2(rel,T,lhs,rhs)
+fun decomp1(T,xxx) = if nnb T then decomp2 xxx else None;
+
+fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp1(T,(rel,lhs,rhs))
   | decomp(_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
-      negate(decomp2(rel,T,lhs,rhs))
+      negate(decomp1(T,(rel,lhs,rhs)))
   | decomp _ = None
 
 (* reduce contradictory <= to False.
@@ -919,29 +928,27 @@
  "(i  = j) & (k  = l) ==> i + k  = j + (l::nat)"
 ];
 
-fun is_nat(t) = fastype_of1 t = HOLogic.natT;
+end;
 
-fun mk_nat_thm sg t =
-  let val ct = cterm_of sg t  and cn = cterm_of sg (Var(("n",0),HOLogic.natT))
-  in instantiate ([],[(cn,ct)]) le0 end;
-
+structure LA_Data_Ref =
+struct
+  val add_mono_thms = ref Nat_LA_Data.add_mono_thms
+  val lessD = ref Nat_LA_Data.lessD
+  val decomp = ref Nat_LA_Data.decomp
+  val simp = ref Nat_LA_Data.simp
 end;
 
-structure Fast_Nat_Arith =
-  Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=Nat_LA_Data);
+structure Fast_Arith =
+  Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=LA_Data_Ref);
 
-val fast_nat_arith_tac = Fast_Nat_Arith.lin_arith_tac;
-
-local
-fun prep_pat s = Thm.read_cterm (sign_of Arith.thy) (s, HOLogic.boolT);
+val fast_arith_tac = Fast_Arith.lin_arith_tac;
 
-val pats = map prep_pat
-  ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"]
+val nat_arith_simproc_pats =
+  map (fn s => Thm.read_cterm (sign_of Arith.thy) (s, HOLogic.boolT))
+      ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"];
 
-in
-val fast_nat_arith_simproc =
-  mk_simproc "fast_nat_arith" pats Fast_Nat_Arith.lin_arith_prover;
-end;
+val fast_nat_arith_simproc = mk_simproc "fast_nat_arith" nat_arith_simproc_pats
+                                        Fast_Arith.lin_arith_prover;
 
 Addsimprocs [fast_nat_arith_simproc];
 
@@ -951,7 +958,7 @@
 fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
 solver all the time rather than add the additional check. *)
 
-simpset_ref () := (simpset() addSolver Fast_Nat_Arith.cut_lin_arith_tac);
+simpset_ref () := (simpset() addSolver Fast_Arith.cut_lin_arith_tac);
 
 (* Elimination of `-' on nat due to John Harrison *)
 Goal "P(a - b::nat) = (!d. (b = a + d --> P 0) & (a = b + d --> P d))";
@@ -964,9 +971,9 @@
 (* FIXME: K true should be replaced by a sensible test to speed things up
    in case there are lots of irrelevant terms involved
 *)
-val nat_arith_tac =
+val arith_tac =
   refute_tac (K true) (REPEAT o split_tac[nat_diff_split])
-             ((REPEAT_DETERM o etac nat_neqE) THEN' fast_nat_arith_tac);
+             ((REPEAT_DETERM o etac nat_neqE) THEN' fast_arith_tac);
 
 (*---------------------------------------------------------------------------*)
 (* End of proof procedures. Now go and USE them!                             *)
@@ -975,75 +982,75 @@
 (*** Subtraction laws -- mostly from Clemens Ballarin ***)
 
 Goal "[| a < (b::nat); c <= a |] ==> a-c < b-c";
-by(nat_arith_tac 1);
+by(arith_tac 1);
 qed "diff_less_mono";
 
 Goal "a+b < (c::nat) ==> a < c-b";
-by(nat_arith_tac 1);
+by(arith_tac 1);
 qed "add_less_imp_less_diff";
 
 Goal "(i < j-k) = (i+k < (j::nat))";
-by(nat_arith_tac 1);
+by(arith_tac 1);
 qed "less_diff_conv";
 
 Goal "(j-k <= (i::nat)) = (j <= i+k)";
-by(nat_arith_tac 1);
+by(arith_tac 1);
 qed "le_diff_conv";
 
 Goal "k <= j ==> (i <= j-k) = (i+k <= (j::nat))";
-by(nat_arith_tac 1);
+by(arith_tac 1);
 qed "le_diff_conv2";
 
 Goal "Suc i <= n ==> Suc (n - Suc i) = n - i";
-by(nat_arith_tac 1);
+by(arith_tac 1);
 qed "Suc_diff_Suc";
 
 Goal "i <= (n::nat) ==> n - (n - i) = i";
-by(nat_arith_tac 1);
+by(arith_tac 1);
 qed "diff_diff_cancel";
 Addsimps [diff_diff_cancel];
 
 Goal "k <= (n::nat) ==> m <= n + m - k";
-by(nat_arith_tac 1);
+by(arith_tac 1);
 qed "le_add_diff";
 
 Goal "[| 0<k; j<i |] ==> j+k-i < k";
-by(nat_arith_tac 1);
+by(arith_tac 1);
 qed "add_diff_less";
 
 Goal "m-1 < n ==> m <= n";
-by(nat_arith_tac 1);
+by(arith_tac 1);
 qed "pred_less_imp_le";
 
 Goal "j<=i ==> i - j < Suc i - j";
-by(nat_arith_tac 1);
+by(arith_tac 1);
 qed "diff_less_Suc_diff";
 
 Goal "i - j <= Suc i - j";
-by(nat_arith_tac 1);
+by(arith_tac 1);
 qed "diff_le_Suc_diff";
 AddIffs [diff_le_Suc_diff];
 
 Goal "n - Suc i <= n - i";
-by(nat_arith_tac 1);
+by(arith_tac 1);
 qed "diff_Suc_le_diff";
 AddIffs [diff_Suc_le_diff];
 
 Goal "0 < n ==> (m <= n-1) = (m<n)";
-by(nat_arith_tac 1);
+by(arith_tac 1);
 qed "le_pred_eq";
 
 Goal "0 < n ==> (m-1 < n) = (m<=n)";
-by(nat_arith_tac 1);
+by(arith_tac 1);
 qed "less_pred_eq";
 
 (*In ordinary notation: if 0<n and n<=m then m-n < m *)
 Goal "[| 0<n; ~ m<n |] ==> m - n < m";
-by(nat_arith_tac 1);
+by(arith_tac 1);
 qed "diff_less";
 
 Goal "[| 0<n; n<=m |] ==> m - n < m";
-by(nat_arith_tac 1);
+by(arith_tac 1);
 qed "le_diff_less";
 
 
@@ -1052,19 +1059,19 @@
 
 (* Monotonicity of subtraction in first argument *)
 Goal "m <= (n::nat) ==> (m-l) <= (n-l)";
-by(nat_arith_tac 1);
+by(arith_tac 1);
 qed "diff_le_mono";
 
 Goal "m <= (n::nat) ==> (l-n) <= (l-m)";
-by(nat_arith_tac 1);
+by(arith_tac 1);
 qed "diff_le_mono2";
 
 
 (*This proof requires natdiff_cancel_sums*)
 Goal "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)";
-by(nat_arith_tac 1);
+by(arith_tac 1);
 qed "diff_less_mono2";
 
 Goal "[| m-n = 0; n-m = 0 |] ==>  m=n";
-by(nat_arith_tac 1);
+by(arith_tac 1);
 qed "diffs0_imp_equal";

--- a/src/HOL/Integ/Bin.ML	Thu Jan 14 12:32:13 1999 +0100
+++ b/src/HOL/Integ/Bin.ML	Thu Jan 14 13:18:09 1999 +0100
@@ -399,13 +399,10 @@
 (The latter option is very inefficient!)
 *)
 
-structure Int_LA_Data: LIN_ARITH_DATA =
+structure Int_LA_Data(*: LIN_ARITH_DATA*) =
 struct
 
-val lessD = add1_zle_eq RS iffD2;
-val not_leD = not_zleE RS lessD;
-
-val intT = Type("IntDef.int",[]);
+val lessD = Nat_LA_Data.lessD @ [add1_zle_eq RS iffD2];
 
 (* borrowed from Bin.thy: *)
 fun dest_bit (Const ("False", _)) = 0
@@ -437,10 +434,7 @@
      ((p,i + m*dest_bin t) handle Match => add_atom(all,m,(p,i)))
   | poly x  = add_atom x;
 
-fun iib T = T = ([intT,intT] ---> HOLogic.boolT);
-
-fun decomp2(rel,T,lhs,rhs) =
-  if not(iib T) then None else
+fun decomp2(rel,lhs,rhs) =
   let val (p,i) = poly(lhs,1,([],0)) and (q,j) = poly(rhs,1,([],0))
   in case rel of
        "op <"  => Some(p,i,"<",q,j)
@@ -449,80 +443,89 @@
      | _       => None
   end;
 
-fun negate(Some(x,i,rel,y,j)) = Some(x,i,"~"^rel,y,j)
-  | negate None = None;
+val intT = Type("IntDef.int",[]);
+fun iib T = T = ([intT,intT] ---> HOLogic.boolT);
 
-fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp2(rel,T,lhs,rhs)
+fun decomp1(T,xxx) =
+  if iib T then decomp2 xxx else Nat_LA_Data.decomp1(T,xxx);
+
+fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp1(T,(rel,lhs,rhs))
   | decomp(_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
-      negate(decomp2(rel,T,lhs,rhs))
+      Nat_LA_Data.negate(decomp1(T,(rel,lhs,rhs)))
   | decomp _ = None
 
 (* reduce contradictory <= to False *)
 val add_rules = simp_thms@bin_arith_simps@bin_rel_simps@[int_0];
 
-val cancel_sums_ss = HOL_basic_ss addsimps add_rules
+val cancel_sums_ss = Nat_LA_Data.cancel_sums_ss addsimps add_rules
           addsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv];
 
 val simp = simplify cancel_sums_ss;
 
-val add_mono_thms = map (fn s => prove_goal Int.thy s
- (fn prems => [cut_facts_tac prems 1,
-               asm_simp_tac (simpset() addsimps [zadd_zle_mono]) 1]))
-["(i <= j) & (k <= l) ==> i + k <= j + (l::int)",
- "(i  = j) & (k <= l) ==> i + k <= j + (l::int)",
- "(i <= j) & (k  = l) ==> i + k <= j + (l::int)",
- "(i  = j) & (k  = l) ==> i + k  = j + (l::int)"
-];
-
-fun is_nat(t) = false;
-
-fun mk_nat_thm sg t = sys_error "Int/mk_nat_thm";
+val add_mono_thms = Nat_LA_Data.add_mono_thms @
+  map (fn s => prove_goal Int.thy s
+                 (fn prems => [cut_facts_tac prems 1,
+                      asm_simp_tac (simpset() addsimps [zadd_zle_mono]) 1]))
+    ["(i <= j) & (k <= l) ==> i + k <= j + (l::int)",
+     "(i  = j) & (k <= l) ==> i + k <= j + (l::int)",
+     "(i <= j) & (k  = l) ==> i + k <= j + (l::int)",
+     "(i  = j) & (k  = l) ==> i + k  = j + (l::int)"
+    ];
 
 end;
 
-structure Fast_Int_Arith =
-  Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=Int_LA_Data);
+(* Update parameters of arithmetic prover *)
+LA_Data_Ref.add_mono_thms := Int_LA_Data.add_mono_thms;
+LA_Data_Ref.lessD :=         Int_LA_Data.lessD;
+LA_Data_Ref.decomp :=        Int_LA_Data.decomp;
+LA_Data_Ref.simp :=          Int_LA_Data.simp;
+
 
-val fast_int_arith_tac = Fast_Int_Arith.lin_arith_tac;
+val int_arith_simproc_pats =
+  map (fn s => Thm.read_cterm (sign_of Int.thy) (s, HOLogic.boolT))
+      ["(m::int) < n","(m::int) <= n", "(m::int) = n"];
 
-simpset_ref () := (simpset() addSolver Fast_Int_Arith.cut_lin_arith_tac);
+val fast_int_arith_simproc = mk_simproc "fast_int_arith" int_arith_simproc_pats
+                                        Fast_Arith.lin_arith_prover;
+
+Addsimprocs [fast_int_arith_simproc];
 
 (* FIXME: K true should be replaced by a sensible test to speed things up
    in case there are lots of irrelevant terms involved.
 *)
-val int_arith_tac =
-  refute_tac (K true) (K all_tac)
-             ((REPEAT o etac int_neqE) THEN' fast_int_arith_tac);
+val arith_tac =
+  refute_tac (K true) (REPEAT o split_tac[nat_diff_split])
+             ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac);
 
 (* Some test data
 Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
-by(fast_int_arith_tac 1);
+by(fast_arith_tac 1);
 Goal "!!a::int. [| a < b; c < d |] ==> a-d+ #2 <= b+(-c)";
-by(fast_int_arith_tac 1);
+by(fast_arith_tac 1);
 Goal "!!a::int. [| a < b; c < d |] ==> a+c+ #1 < b+d";
-by(fast_int_arith_tac 1);
+by(fast_arith_tac 1);
 Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c";
-by(fast_int_arith_tac 1);
+by(fast_arith_tac 1);
 Goal "!!a::int. [| a+b <= i+j; a<=b; i<=j |] \
 \     ==> a+a <= j+j";
-by(fast_int_arith_tac 1);
+by(fast_arith_tac 1);
 Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \
 \     ==> a+a - - #-1 < j+j - #3";
-by(fast_int_arith_tac 1);
+by(fast_arith_tac 1);
 Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
-by(int_arith_tac 1);
+by(arith_tac 1);
 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
 \     ==> a <= l";
-by(fast_int_arith_tac 1);
+by(fast_arith_tac 1);
 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
 \     ==> a+a+a+a <= l+l+l+l";
-by(fast_int_arith_tac 1);
+by(fast_arith_tac 1);
 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
 \     ==> a+a+a+a+a <= l+l+l+l+i";
-by(fast_int_arith_tac 1);
+by(fast_arith_tac 1);
 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
 \     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
-by(fast_int_arith_tac 1);
+by(fast_arith_tac 1);
 *)
 
 (*---------------------------------------------------------------------------*)
@@ -544,50 +547,50 @@
 (** Simplification of inequalities involving numerical constants **)
 
 Goal "(w <= z + #1) = (w<=z | w = z + #1)";
-by(int_arith_tac 1);
+by(arith_tac 1);
 qed "zle_add1_eq";
 
 Goal "(w <= z - #1) = (w<z)";
-by(int_arith_tac 1);
+by(arith_tac 1);
 qed "zle_diff1_eq";
 Addsimps [zle_diff1_eq];
 
 (*2nd premise can be proved automatically if v is a literal*)
 Goal "[| w <= z; #0 <= v |] ==> w <= z + v";
-by(fast_int_arith_tac 1);
+by(fast_arith_tac 1);
 qed "zle_imp_zle_zadd";
 
 Goal "w <= z ==> w <= z + #1";
-by(fast_int_arith_tac 1);
+by(fast_arith_tac 1);
 qed "zle_imp_zle_zadd1";
 
 (*2nd premise can be proved automatically if v is a literal*)
 Goal "[| w < z; #0 <= v |] ==> w < z + v";
-by(fast_int_arith_tac 1);
+by(fast_arith_tac 1);
 qed "zless_imp_zless_zadd";
 
 Goal "w < z ==> w < z + #1";
-by(fast_int_arith_tac 1);
+by(fast_arith_tac 1);
 qed "zless_imp_zless_zadd1";
 
 Goal "(w < z + #1) = (w<=z)";
-by(int_arith_tac 1);
+by(arith_tac 1);
 qed "zle_add1_eq_le";
 Addsimps [zle_add1_eq_le];
 
 Goal "(z = z + w) = (w = #0)";
-by(int_arith_tac 1);
+by(arith_tac 1);
 qed "zadd_left_cancel0";
 Addsimps [zadd_left_cancel0];
 
 (*LOOPS as a simprule!*)
 Goal "[| w + v < z; #0 <= v |] ==> w < z";
-by(fast_int_arith_tac 1);
+by(fast_arith_tac 1);
 qed "zless_zadd_imp_zless";
 
 (*LOOPS as a simprule!  Analogous to Suc_lessD*)
 Goal "w + #1 < z ==> w < z";
-by(fast_int_arith_tac 1);
+by(fast_arith_tac 1);
 qed "zless_zadd1_imp_zless";
 
 Goal "w + #-1 = w - #1";

--- a/src/HOL/Lambda/Eta.ML	Thu Jan 14 12:32:13 1999 +0100
+++ b/src/HOL/Lambda/Eta.ML	Thu Jan 14 13:18:09 1999 +0100
@@ -29,7 +29,7 @@
 Goal "!i k. free (lift t k) i = (i < k & free t i | k < i & free t (i-1))";
 by (induct_tac "t" 1);
   by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()) addcongs [conj_cong])));
- by(nat_arith_tac 1);
+ by(arith_tac 1);
 by(Auto_tac);
 qed "free_lift";
 Addsimps [free_lift];

--- a/src/HOL/Lambda/ListApplication.ML	Thu Jan 14 12:32:13 1999 +0100
+++ b/src/HOL/Lambda/ListApplication.ML	Thu Jan 14 13:18:09 1999 +0100
@@ -88,7 +88,7 @@
 Addsimps [size_apps];
 
 Goal "[| 0 < k; m <= n |] ==> m < n+k";
-by(fast_nat_arith_tac 1);
+by(fast_arith_tac 1);
 val lemma = result();
 
 (* a customized induction schema for $$ *)

--- a/src/HOL/Ord.ML	Thu Jan 14 12:32:13 1999 +0100
+++ b/src/HOL/Ord.ML	Thu Jan 14 13:18:09 1999 +0100
@@ -104,6 +104,28 @@
 by (Blast_tac 1);
 qed "linorder_less_linear";
 
+Goal "!!x::'a::linorder. (~ x < y) = (y <= x)";
+by (simp_tac (simpset() addsimps [order_less_le]) 1);
+by (cut_facts_tac [linorder_linear] 1);
+by (blast_tac (claset() addIs [order_antisym]) 1);
+qed "linorder_not_less";
+
+Goal "!!x::'a::linorder. (~ x <= y) = (y < x)";
+by (simp_tac (simpset() addsimps [order_less_le]) 1);
+by (cut_facts_tac [linorder_linear] 1);
+by (blast_tac (claset() addIs [order_antisym]) 1);
+qed "linorder_not_le";
+
+Goal "!!x::'a::linorder. (x ~= y) = (x<y | y<x)";
+by (cut_inst_tac [("x","x"),("y","y")] linorder_less_linear 1);
+by Auto_tac;
+qed "linorder_neq_iff";
+
+(* eliminates ~= in premises *)
+bind_thm("linorder_neqE", linorder_neq_iff RS iffD1 RS disjE);
+
+(** min & max **)
+
 Goalw [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)";
 by (Simp_tac 1);
 by (cut_facts_tac [linorder_linear] 1);
@@ -136,17 +158,3 @@
 by (cut_facts_tac [linorder_linear] 1);
 by (blast_tac (claset() addIs [order_trans]) 1);
 qed "min_le_iff_disj";
-
-Goal "!!x::'a::linorder. (x ~= y) = (x<y | y<x)";
-by (cut_inst_tac [("x","x"),("y","y")] linorder_less_linear 1);
-by Auto_tac;
-qed "linorder_neq_iff";
-
-(*** eliminates ~= in premises ***)
-bind_thm("linorder_neqE", linorder_neq_iff RS iffD1 RS disjE);
-
-Goal "!!x::'a::linorder. (~ x < y) = (y <= x)";
-by (simp_tac (simpset() addsimps [order_less_le]) 1);
-by (cut_facts_tac [linorder_linear] 1);
-by (blast_tac (claset() addIs [order_antisym]) 1);
-qed "linorder_not_less";

--- a/src/HOL/UNITY/LessThan.ML	Thu Jan 14 12:32:13 1999 +0100
+++ b/src/HOL/UNITY/LessThan.ML	Thu Jan 14 13:18:09 1999 +0100
@@ -7,10 +7,6 @@
 *)
 
 
-(*Make Auto_tac and Force_tac try lin_arith_tac!*)
-claset_ref() := claset() addaltern ("lin_arith_tac",Fast_Nat_Arith.lin_arith_tac);
-
-
 (*** lessThan ***)
 
 Goalw [lessThan_def] "(i: lessThan k) = (i<k)";

--- a/src/HOL/UNITY/Lift.ML	Thu Jan 14 12:32:13 1999 +0100
+++ b/src/HOL/UNITY/Lift.ML	Thu Jan 14 13:18:09 1999 +0100
@@ -275,8 +275,7 @@
     (asm_simp_tac (simpset() addsimps [zle_def]@metric_simps @ zcompare_rls)));
 (** LEVEL 5 **)
 by (dres_inst_tac [("w1","Min")] (zle_iff_zadd RS iffD1) 1);
-by Auto_tac;
-by (full_simp_tac (simpset() addsimps [zadd_int_left]) 1);
+by (Blast_tac 1);
 qed "E_thm16a";
 
 (*lem_lift_5_1 has ~goingup instead of goingdown*)
@@ -292,10 +291,7 @@
 		                      metric_simps @ zcompare_rls)));
 (** LEVEL 5 **)
 by (dres_inst_tac [("z1","Max")] (zle_iff_zadd RS iffD1) 1);
-by (etac exE 1);  
-by (etac ssubst 1);
-by Auto_tac;
-by (full_simp_tac (simpset() addsimps [zadd_int_left]) 1);
+by (Blast_tac 1);
 qed "E_thm16b";
 
 

--- a/src/HOL/simpdata.ML	Thu Jan 14 12:32:13 1999 +0100
+++ b/src/HOL/simpdata.ML	Thu Jan 14 13:18:09 1999 +0100
@@ -64,31 +64,28 @@
 
   fun prover s = prove_goal HOL.thy s (K [Blast_tac 1]);
 
-  val P_imp_P_iff_True = prover "P --> (P = True)" RS mp;
-  val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;
-
-  val not_P_imp_P_iff_F = prover "~P --> (P = False)" RS mp;
-  val not_P_imp_P_eq_False = not_P_imp_P_iff_F RS eq_reflection;
-
 in
 
 (*Make meta-equalities.  The operator below is Trueprop*)
 
-  fun mk_meta_eq r = r RS eq_reflection;
+fun mk_meta_eq r = r RS eq_reflection;
+
+val Eq_TrueI  = mk_meta_eq(prover  "P --> (P = True)"  RS mp);
+val Eq_FalseI = mk_meta_eq(prover "~P --> (P = False)" RS mp);
 
-  fun mk_eq th = case concl_of th of
-          Const("==",_)$_$_       => th
-      |   _$(Const("op =",_)$_$_) => mk_meta_eq th
-      |   _$(Const("Not",_)$_)    => th RS not_P_imp_P_eq_False
-      |   _                       => th RS P_imp_P_eq_True;
-  (* last 2 lines requires all formulae to be of the from Trueprop(.) *)
+fun mk_eq th = case concl_of th of
+        Const("==",_)$_$_       => th
+    |   _$(Const("op =",_)$_$_) => mk_meta_eq th
+    |   _$(Const("Not",_)$_)    => th RS Eq_FalseI
+    |   _                       => th RS Eq_TrueI;
+(* last 2 lines requires all formulae to be of the from Trueprop(.) *)
 
-  fun mk_eq_True r = Some(r RS meta_eq_to_obj_eq RS P_imp_P_eq_True);
+fun mk_eq_True r = Some(r RS meta_eq_to_obj_eq RS Eq_TrueI);
 
-  fun mk_meta_cong rl =
-    standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
-    handle THM _ =>
-    error("Premises and conclusion of congruence rules must be =-equalities");
+fun mk_meta_cong rl =
+  standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
+  handle THM _ =>
+  error("Premises and conclusion of congruence rules must be =-equalities");
 
 val not_not = prover "(~ ~ P) = P";
 
@@ -505,6 +502,6 @@
                eresolve_tac [disjE] 1) THEN
         ref_tac 1;
   in EVERY'[TRY o filter_prems_tac test,
-            REPEAT o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac,
+            DETERM o REPEAT o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac,
             SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]
   end;

--- a/src/Provers/Arith/fast_lin_arith.ML	Thu Jan 14 12:32:13 1999 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Thu Jan 14 13:18:09 1999 +0100
@@ -26,11 +26,14 @@
   val neqE:             thm (* [| m ~= n; m < n ==> P; n < m ==> P |] ==> P *)
   val notI:             thm (* (P ==> False) ==> ~ P *)
   val not_lessD:        thm (* ~(m < n) ==> n <= m *)
+  val not_leD:          thm (* ~(m <= n) ==> n < m *)
   val sym:		thm (* x = y ==> y = x *)
   val mk_Eq: thm -> thm
   val mk_Trueprop: term -> term
   val neg_prop: term -> term
   val is_False: thm -> bool
+  val is_nat: typ list * term -> bool
+  val mk_nat_thm: Sign.sg -> term -> thm
 end;
 (*
 mk_Eq(~in) = `in == False'
@@ -40,19 +43,20 @@
 neg_prop(t) = neg if t is wrapped up in Trueprop and
   nt is the (logically) negated version of t, where the negation
   of a negative term is the term itself (no double negation!);
+
+is_nat(parameter-types,t) =  t:nat
+mk_nat_thm(t) = "0 <= t"
 *)
 
 signature LIN_ARITH_DATA =
 sig
-  val add_mono_thms:    thm list
+  val add_mono_thms:    thm list ref
                             (* [| i rel1 j; m rel2 n |] ==> i + m rel3 j + n *)
-  val lessD:            thm (* m < n ==> Suc m <= n *)
-  val not_leD:          thm (* ~(m <= n) ==> Suc n <= m *)
-  val decomp: term ->
-             ((term * int)list * int * string * (term * int)list * int)option
-  val simp: thm -> thm
-  val is_nat: typ list * term -> bool
-  val mk_nat_thm: Sign.sg -> term -> thm
+  val lessD:            thm list ref (* m < n ==> m+1 <= n *)
+  val decomp:
+    (term -> ((term * int)list * int * string * (term * int)list * int)option)
+    ref
+  val simp: (thm -> thm) ref
 end;
 (*
 decomp(`x Rel y') should yield (p,i,Rel,q,j)
@@ -63,9 +67,6 @@
 simp must reduce contradictory <= to False.
    It should also cancel common summands to keep <= reduced;
    otherwise <= can grow to massive proportions.
-
-is_nat(parameter-types,t) =  t:nat
-mk_nat_thm(t) = "0 <= t"
 *)
 
 signature FAST_LIN_ARITH =
@@ -90,7 +91,9 @@
 
 datatype injust = Asm of int
                 | Nat of int (* index of atom *)
-                | Fwd of injust * thm
+                | LessD of injust
+                | NotLessD of injust
+                | NotLeD of injust
                 | Multiplied of int * injust
                 | Added of injust * injust;
 
@@ -250,12 +253,12 @@
 fun mkthm sg asms just =
   let val atoms = foldl (fn (ats,(lhs,_,_,rhs,_)) =>
                             map fst lhs  union  (map fst rhs  union  ats))
-                        ([], mapfilter (LA_Data.decomp o concl_of) asms)
+                        ([], mapfilter (!LA_Data.decomp o concl_of) asms)
 
       fun addthms thm1 thm2 =
         let val conj = thm1 RS (thm2 RS LA_Logic.conjI)
         in the(get_first (fn th => Some(conj RS th) handle _ => None)
-                         LA_Data.add_mono_thms)
+                         (!LA_Data.add_mono_thms))
         end;
 
       fun multn(n,thm) =
@@ -263,16 +266,18 @@
         in if n < 0 then mul(~n,thm) RS LA_Logic.sym else mul(n,thm) end;
 
       fun simp thm =
-        let val thm' = LA_Data.simp thm
+        let val thm' = !LA_Data.simp thm
         in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end
 
       fun mk(Asm i) = nth_elem(i,asms)
-        | mk(Nat(i)) = LA_Data.mk_nat_thm sg (nth_elem(i,atoms))
-        | mk(Fwd(j,thm)) = mk j RS thm
+        | mk(Nat(i)) = LA_Logic.mk_nat_thm sg (nth_elem(i,atoms))
+        | mk(LessD(j)) = hd([mk j] RL !LA_Data.lessD)
+        | mk(NotLeD(j)) = hd([mk j RS LA_Logic.not_leD] RL !LA_Data.lessD)
+        | mk(NotLessD(j)) = mk j RS LA_Logic.not_lessD
         | mk(Added(j1,j2)) = simp(addthms (mk j1) (mk j2))
         | mk(Multiplied(n,j)) = multn(n,mk j)
 
-  in LA_Data.simp(mk just) handle FalseE thm => thm end
+  in !LA_Data.simp(mk just) handle FalseE thm => thm end
 end;
 
 fun coeff poly atom = case assoc(poly,atom) of None => 0 | Some i => i;
@@ -287,9 +292,9 @@
         val just = Asm k
     in case rel of
         "<="   => Some(Lineq(c,Le,diff,just))
-       | "~<=" => Some(Lineq(1-c,Le,map (op ~) diff,Fwd(just,LA_Data.not_leD)))
-       | "<"   => Some(Lineq(c+1,Le,diff,Fwd(just,LA_Data.lessD)))
-       | "~<"  => Some(Lineq(~c,Le,map (op~) diff,Fwd(just,LA_Logic.not_lessD)))
+       | "~<=" => Some(Lineq(1-c,Le,map (op ~) diff,NotLeD(just)))
+       | "<"   => Some(Lineq(c+1,Le,diff,LessD(just)))
+       | "~<"  => Some(Lineq(~c,Le,map (op~) diff,NotLessD(just)))
        | "="   => Some(Lineq(c,Eq,diff,just))
        | "~="  => None
        | _     => sys_error("mklineq" ^ rel)   
@@ -297,7 +302,7 @@
   end;
 
 fun mknat pTs ixs (atom,i) =
-  if LA_Data.is_nat(pTs,atom)
+  if LA_Logic.is_nat(pTs,atom)
   then let val l = map (fn j => if j=i then 1 else 0) ixs
        in Some(Lineq(0,Le,l,Nat(i))) end
   else None
@@ -345,9 +350,9 @@
 fun prove(pTs,Hs,concl) =
 let val nHs = length Hs
     val ixHs = Hs ~~ (0 upto (nHs-1))
-    val Hitems = mapfilter (fn (h,i) => case LA_Data.decomp h of
+    val Hitems = mapfilter (fn (h,i) => case !LA_Data.decomp h of
                                  None => None | Some(it) => Some(it,i)) ixHs
-in case LA_Data.decomp concl of
+in case !LA_Data.decomp concl of
      None => if null Hitems then [] else refute1(pTs,Hitems)
    | Some(citem as (r,i,rel,l,j)) =>
        if rel = "="