More arith refinements.
authornipkow
Thu Jan 14 13:18:09 1999 +0100 (1999-01-14)
changeset 61282acc5d36610c
parent 6127 ece970eb5850
child 6129 0f5ecd633c2f
More arith refinements.
src/HOL/Arith.ML
src/HOL/Integ/Bin.ML
src/HOL/Lambda/Eta.ML
src/HOL/Lambda/ListApplication.ML
src/HOL/Ord.ML
src/HOL/UNITY/LessThan.ML
src/HOL/UNITY/Lift.ML
src/HOL/simpdata.ML
src/Provers/Arith/fast_lin_arith.ML
     1.1 --- a/src/HOL/Arith.ML	Thu Jan 14 12:32:13 1999 +0100
     1.2 +++ b/src/HOL/Arith.ML	Thu Jan 14 13:18:09 1999 +0100
     1.3 @@ -853,8 +853,11 @@
     1.4  val notI = notI;
     1.5  val sym = sym;
     1.6  val not_lessD = linorder_not_less RS iffD1;
     1.7 +val not_leD = linorder_not_le RS iffD1;
     1.8  
     1.9 -val mk_Eq = mk_eq;
    1.10 +
    1.11 +fun mk_Eq thm = (thm RS Eq_FalseI) handle _ => (thm RS Eq_TrueI);
    1.12 +
    1.13  val mk_Trueprop = HOLogic.mk_Trueprop;
    1.14  
    1.15  fun neg_prop(TP$(Const("Not",_)$t)) = TP$t
    1.16 @@ -864,13 +867,18 @@
    1.17    let val _ $ t = #prop(rep_thm thm)
    1.18    in t = Const("False",HOLogic.boolT) end;
    1.19  
    1.20 +fun is_nat(t) = fastype_of1 t = HOLogic.natT;
    1.21 +
    1.22 +fun mk_nat_thm sg t =
    1.23 +  let val ct = cterm_of sg t  and cn = cterm_of sg (Var(("n",0),HOLogic.natT))
    1.24 +  in instantiate ([],[(cn,ct)]) le0 end;
    1.25 +
    1.26  end;
    1.27  
    1.28 -structure Nat_LA_Data: LIN_ARITH_DATA =
    1.29 +structure Nat_LA_Data (* : LIN_ARITH_DATA *) =
    1.30  struct
    1.31  
    1.32 -val lessD = Suc_leI;
    1.33 -val not_leD = not_leE RS Suc_leI;
    1.34 +val lessD = [Suc_leI];
    1.35  
    1.36  (* Turn term into list of summand * multiplicity plus a constant *)
    1.37  fun poly(Const("Suc",_)$t, (p,i)) = poly(t, (p,i+1))
    1.38 @@ -882,8 +890,7 @@
    1.39  
    1.40  fun nnb T = T = ([HOLogic.natT,HOLogic.natT] ---> HOLogic.boolT);
    1.41  
    1.42 -fun decomp2(rel,T,lhs,rhs) =
    1.43 -  if not(nnb T) then None else
    1.44 +fun decomp2(rel,lhs,rhs) =
    1.45    let val (p,i) = poly(lhs,([],0)) and (q,j) = poly(rhs,([],0))
    1.46    in case rel of
    1.47         "op <"  => Some(p,i,"<",q,j)
    1.48 @@ -895,9 +902,11 @@
    1.49  fun negate(Some(x,i,rel,y,j)) = Some(x,i,"~"^rel,y,j)
    1.50    | negate None = None;
    1.51  
    1.52 -fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp2(rel,T,lhs,rhs)
    1.53 +fun decomp1(T,xxx) = if nnb T then decomp2 xxx else None;
    1.54 +
    1.55 +fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp1(T,(rel,lhs,rhs))
    1.56    | decomp(_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
    1.57 -      negate(decomp2(rel,T,lhs,rhs))
    1.58 +      negate(decomp1(T,(rel,lhs,rhs)))
    1.59    | decomp _ = None
    1.60  
    1.61  (* reduce contradictory <= to False.
    1.62 @@ -919,29 +928,27 @@
    1.63   "(i  = j) & (k  = l) ==> i + k  = j + (l::nat)"
    1.64  ];
    1.65  
    1.66 -fun is_nat(t) = fastype_of1 t = HOLogic.natT;
    1.67 +end;
    1.68  
    1.69 -fun mk_nat_thm sg t =
    1.70 -  let val ct = cterm_of sg t  and cn = cterm_of sg (Var(("n",0),HOLogic.natT))
    1.71 -  in instantiate ([],[(cn,ct)]) le0 end;
    1.72 -
    1.73 +structure LA_Data_Ref =
    1.74 +struct
    1.75 +  val add_mono_thms = ref Nat_LA_Data.add_mono_thms
    1.76 +  val lessD = ref Nat_LA_Data.lessD
    1.77 +  val decomp = ref Nat_LA_Data.decomp
    1.78 +  val simp = ref Nat_LA_Data.simp
    1.79  end;
    1.80  
    1.81 -structure Fast_Nat_Arith =
    1.82 -  Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=Nat_LA_Data);
    1.83 +structure Fast_Arith =
    1.84 +  Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=LA_Data_Ref);
    1.85  
    1.86 -val fast_nat_arith_tac = Fast_Nat_Arith.lin_arith_tac;
    1.87 -
    1.88 -local
    1.89 -fun prep_pat s = Thm.read_cterm (sign_of Arith.thy) (s, HOLogic.boolT);
    1.90 +val fast_arith_tac = Fast_Arith.lin_arith_tac;
    1.91  
    1.92 -val pats = map prep_pat
    1.93 -  ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"]
    1.94 +val nat_arith_simproc_pats =
    1.95 +  map (fn s => Thm.read_cterm (sign_of Arith.thy) (s, HOLogic.boolT))
    1.96 +      ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"];
    1.97  
    1.98 -in
    1.99 -val fast_nat_arith_simproc =
   1.100 -  mk_simproc "fast_nat_arith" pats Fast_Nat_Arith.lin_arith_prover;
   1.101 -end;
   1.102 +val fast_nat_arith_simproc = mk_simproc "fast_nat_arith" nat_arith_simproc_pats
   1.103 +                                        Fast_Arith.lin_arith_prover;
   1.104  
   1.105  Addsimprocs [fast_nat_arith_simproc];
   1.106  
   1.107 @@ -951,7 +958,7 @@
   1.108  fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
   1.109  solver all the time rather than add the additional check. *)
   1.110  
   1.111 -simpset_ref () := (simpset() addSolver Fast_Nat_Arith.cut_lin_arith_tac);
   1.112 +simpset_ref () := (simpset() addSolver Fast_Arith.cut_lin_arith_tac);
   1.113  
   1.114  (* Elimination of `-' on nat due to John Harrison *)
   1.115  Goal "P(a - b::nat) = (!d. (b = a + d --> P 0) & (a = b + d --> P d))";
   1.116 @@ -964,9 +971,9 @@
   1.117  (* FIXME: K true should be replaced by a sensible test to speed things up
   1.118     in case there are lots of irrelevant terms involved
   1.119  *)
   1.120 -val nat_arith_tac =
   1.121 +val arith_tac =
   1.122    refute_tac (K true) (REPEAT o split_tac[nat_diff_split])
   1.123 -             ((REPEAT_DETERM o etac nat_neqE) THEN' fast_nat_arith_tac);
   1.124 +             ((REPEAT_DETERM o etac nat_neqE) THEN' fast_arith_tac);
   1.125  
   1.126  (*---------------------------------------------------------------------------*)
   1.127  (* End of proof procedures. Now go and USE them!                             *)
   1.128 @@ -975,75 +982,75 @@
   1.129  (*** Subtraction laws -- mostly from Clemens Ballarin ***)
   1.130  
   1.131  Goal "[| a < (b::nat); c <= a |] ==> a-c < b-c";
   1.132 -by(nat_arith_tac 1);
   1.133 +by(arith_tac 1);
   1.134  qed "diff_less_mono";
   1.135  
   1.136  Goal "a+b < (c::nat) ==> a < c-b";
   1.137 -by(nat_arith_tac 1);
   1.138 +by(arith_tac 1);
   1.139  qed "add_less_imp_less_diff";
   1.140  
   1.141  Goal "(i < j-k) = (i+k < (j::nat))";
   1.142 -by(nat_arith_tac 1);
   1.143 +by(arith_tac 1);
   1.144  qed "less_diff_conv";
   1.145  
   1.146  Goal "(j-k <= (i::nat)) = (j <= i+k)";
   1.147 -by(nat_arith_tac 1);
   1.148 +by(arith_tac 1);
   1.149  qed "le_diff_conv";
   1.150  
   1.151  Goal "k <= j ==> (i <= j-k) = (i+k <= (j::nat))";
   1.152 -by(nat_arith_tac 1);
   1.153 +by(arith_tac 1);
   1.154  qed "le_diff_conv2";
   1.155  
   1.156  Goal "Suc i <= n ==> Suc (n - Suc i) = n - i";
   1.157 -by(nat_arith_tac 1);
   1.158 +by(arith_tac 1);
   1.159  qed "Suc_diff_Suc";
   1.160  
   1.161  Goal "i <= (n::nat) ==> n - (n - i) = i";
   1.162 -by(nat_arith_tac 1);
   1.163 +by(arith_tac 1);
   1.164  qed "diff_diff_cancel";
   1.165  Addsimps [diff_diff_cancel];
   1.166  
   1.167  Goal "k <= (n::nat) ==> m <= n + m - k";
   1.168 -by(nat_arith_tac 1);
   1.169 +by(arith_tac 1);
   1.170  qed "le_add_diff";
   1.171  
   1.172  Goal "[| 0<k; j<i |] ==> j+k-i < k";
   1.173 -by(nat_arith_tac 1);
   1.174 +by(arith_tac 1);
   1.175  qed "add_diff_less";
   1.176  
   1.177  Goal "m-1 < n ==> m <= n";
   1.178 -by(nat_arith_tac 1);
   1.179 +by(arith_tac 1);
   1.180  qed "pred_less_imp_le";
   1.181  
   1.182  Goal "j<=i ==> i - j < Suc i - j";
   1.183 -by(nat_arith_tac 1);
   1.184 +by(arith_tac 1);
   1.185  qed "diff_less_Suc_diff";
   1.186  
   1.187  Goal "i - j <= Suc i - j";
   1.188 -by(nat_arith_tac 1);
   1.189 +by(arith_tac 1);
   1.190  qed "diff_le_Suc_diff";
   1.191  AddIffs [diff_le_Suc_diff];
   1.192  
   1.193  Goal "n - Suc i <= n - i";
   1.194 -by(nat_arith_tac 1);
   1.195 +by(arith_tac 1);
   1.196  qed "diff_Suc_le_diff";
   1.197  AddIffs [diff_Suc_le_diff];
   1.198  
   1.199  Goal "0 < n ==> (m <= n-1) = (m<n)";
   1.200 -by(nat_arith_tac 1);
   1.201 +by(arith_tac 1);
   1.202  qed "le_pred_eq";
   1.203  
   1.204  Goal "0 < n ==> (m-1 < n) = (m<=n)";
   1.205 -by(nat_arith_tac 1);
   1.206 +by(arith_tac 1);
   1.207  qed "less_pred_eq";
   1.208  
   1.209  (*In ordinary notation: if 0<n and n<=m then m-n < m *)
   1.210  Goal "[| 0<n; ~ m<n |] ==> m - n < m";
   1.211 -by(nat_arith_tac 1);
   1.212 +by(arith_tac 1);
   1.213  qed "diff_less";
   1.214  
   1.215  Goal "[| 0<n; n<=m |] ==> m - n < m";
   1.216 -by(nat_arith_tac 1);
   1.217 +by(arith_tac 1);
   1.218  qed "le_diff_less";
   1.219  
   1.220  
   1.221 @@ -1052,19 +1059,19 @@
   1.222  
   1.223  (* Monotonicity of subtraction in first argument *)
   1.224  Goal "m <= (n::nat) ==> (m-l) <= (n-l)";
   1.225 -by(nat_arith_tac 1);
   1.226 +by(arith_tac 1);
   1.227  qed "diff_le_mono";
   1.228  
   1.229  Goal "m <= (n::nat) ==> (l-n) <= (l-m)";
   1.230 -by(nat_arith_tac 1);
   1.231 +by(arith_tac 1);
   1.232  qed "diff_le_mono2";
   1.233  
   1.234  
   1.235  (*This proof requires natdiff_cancel_sums*)
   1.236  Goal "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)";
   1.237 -by(nat_arith_tac 1);
   1.238 +by(arith_tac 1);
   1.239  qed "diff_less_mono2";
   1.240  
   1.241  Goal "[| m-n = 0; n-m = 0 |] ==>  m=n";
   1.242 -by(nat_arith_tac 1);
   1.243 +by(arith_tac 1);
   1.244  qed "diffs0_imp_equal";
     2.1 --- a/src/HOL/Integ/Bin.ML	Thu Jan 14 12:32:13 1999 +0100
     2.2 +++ b/src/HOL/Integ/Bin.ML	Thu Jan 14 13:18:09 1999 +0100
     2.3 @@ -399,13 +399,10 @@
     2.4  (The latter option is very inefficient!)
     2.5  *)
     2.6  
     2.7 -structure Int_LA_Data: LIN_ARITH_DATA =
     2.8 +structure Int_LA_Data(*: LIN_ARITH_DATA*) =
     2.9  struct
    2.10  
    2.11 -val lessD = add1_zle_eq RS iffD2;
    2.12 -val not_leD = not_zleE RS lessD;
    2.13 -
    2.14 -val intT = Type("IntDef.int",[]);
    2.15 +val lessD = Nat_LA_Data.lessD @ [add1_zle_eq RS iffD2];
    2.16  
    2.17  (* borrowed from Bin.thy: *)
    2.18  fun dest_bit (Const ("False", _)) = 0
    2.19 @@ -437,10 +434,7 @@
    2.20       ((p,i + m*dest_bin t) handle Match => add_atom(all,m,(p,i)))
    2.21    | poly x  = add_atom x;
    2.22  
    2.23 -fun iib T = T = ([intT,intT] ---> HOLogic.boolT);
    2.24 -
    2.25 -fun decomp2(rel,T,lhs,rhs) =
    2.26 -  if not(iib T) then None else
    2.27 +fun decomp2(rel,lhs,rhs) =
    2.28    let val (p,i) = poly(lhs,1,([],0)) and (q,j) = poly(rhs,1,([],0))
    2.29    in case rel of
    2.30         "op <"  => Some(p,i,"<",q,j)
    2.31 @@ -449,80 +443,89 @@
    2.32       | _       => None
    2.33    end;
    2.34  
    2.35 -fun negate(Some(x,i,rel,y,j)) = Some(x,i,"~"^rel,y,j)
    2.36 -  | negate None = None;
    2.37 +val intT = Type("IntDef.int",[]);
    2.38 +fun iib T = T = ([intT,intT] ---> HOLogic.boolT);
    2.39  
    2.40 -fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp2(rel,T,lhs,rhs)
    2.41 +fun decomp1(T,xxx) =
    2.42 +  if iib T then decomp2 xxx else Nat_LA_Data.decomp1(T,xxx);
    2.43 +
    2.44 +fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp1(T,(rel,lhs,rhs))
    2.45    | decomp(_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
    2.46 -      negate(decomp2(rel,T,lhs,rhs))
    2.47 +      Nat_LA_Data.negate(decomp1(T,(rel,lhs,rhs)))
    2.48    | decomp _ = None
    2.49  
    2.50  (* reduce contradictory <= to False *)
    2.51  val add_rules = simp_thms@bin_arith_simps@bin_rel_simps@[int_0];
    2.52  
    2.53 -val cancel_sums_ss = HOL_basic_ss addsimps add_rules
    2.54 +val cancel_sums_ss = Nat_LA_Data.cancel_sums_ss addsimps add_rules
    2.55            addsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv];
    2.56  
    2.57  val simp = simplify cancel_sums_ss;
    2.58  
    2.59 -val add_mono_thms = map (fn s => prove_goal Int.thy s
    2.60 - (fn prems => [cut_facts_tac prems 1,
    2.61 -               asm_simp_tac (simpset() addsimps [zadd_zle_mono]) 1]))
    2.62 -["(i <= j) & (k <= l) ==> i + k <= j + (l::int)",
    2.63 - "(i  = j) & (k <= l) ==> i + k <= j + (l::int)",
    2.64 - "(i <= j) & (k  = l) ==> i + k <= j + (l::int)",
    2.65 - "(i  = j) & (k  = l) ==> i + k  = j + (l::int)"
    2.66 -];
    2.67 -
    2.68 -fun is_nat(t) = false;
    2.69 -
    2.70 -fun mk_nat_thm sg t = sys_error "Int/mk_nat_thm";
    2.71 +val add_mono_thms = Nat_LA_Data.add_mono_thms @
    2.72 +  map (fn s => prove_goal Int.thy s
    2.73 +                 (fn prems => [cut_facts_tac prems 1,
    2.74 +                      asm_simp_tac (simpset() addsimps [zadd_zle_mono]) 1]))
    2.75 +    ["(i <= j) & (k <= l) ==> i + k <= j + (l::int)",
    2.76 +     "(i  = j) & (k <= l) ==> i + k <= j + (l::int)",
    2.77 +     "(i <= j) & (k  = l) ==> i + k <= j + (l::int)",
    2.78 +     "(i  = j) & (k  = l) ==> i + k  = j + (l::int)"
    2.79 +    ];
    2.80  
    2.81  end;
    2.82  
    2.83 -structure Fast_Int_Arith =
    2.84 -  Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=Int_LA_Data);
    2.85 +(* Update parameters of arithmetic prover *)
    2.86 +LA_Data_Ref.add_mono_thms := Int_LA_Data.add_mono_thms;
    2.87 +LA_Data_Ref.lessD :=         Int_LA_Data.lessD;
    2.88 +LA_Data_Ref.decomp :=        Int_LA_Data.decomp;
    2.89 +LA_Data_Ref.simp :=          Int_LA_Data.simp;
    2.90 +
    2.91  
    2.92 -val fast_int_arith_tac = Fast_Int_Arith.lin_arith_tac;
    2.93 +val int_arith_simproc_pats =
    2.94 +  map (fn s => Thm.read_cterm (sign_of Int.thy) (s, HOLogic.boolT))
    2.95 +      ["(m::int) < n","(m::int) <= n", "(m::int) = n"];
    2.96  
    2.97 -simpset_ref () := (simpset() addSolver Fast_Int_Arith.cut_lin_arith_tac);
    2.98 +val fast_int_arith_simproc = mk_simproc "fast_int_arith" int_arith_simproc_pats
    2.99 +                                        Fast_Arith.lin_arith_prover;
   2.100 +
   2.101 +Addsimprocs [fast_int_arith_simproc];
   2.102  
   2.103  (* FIXME: K true should be replaced by a sensible test to speed things up
   2.104     in case there are lots of irrelevant terms involved.
   2.105  *)
   2.106 -val int_arith_tac =
   2.107 -  refute_tac (K true) (K all_tac)
   2.108 -             ((REPEAT o etac int_neqE) THEN' fast_int_arith_tac);
   2.109 +val arith_tac =
   2.110 +  refute_tac (K true) (REPEAT o split_tac[nat_diff_split])
   2.111 +             ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac);
   2.112  
   2.113  (* Some test data
   2.114  Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
   2.115 -by(fast_int_arith_tac 1);
   2.116 +by(fast_arith_tac 1);
   2.117  Goal "!!a::int. [| a < b; c < d |] ==> a-d+ #2 <= b+(-c)";
   2.118 -by(fast_int_arith_tac 1);
   2.119 +by(fast_arith_tac 1);
   2.120  Goal "!!a::int. [| a < b; c < d |] ==> a+c+ #1 < b+d";
   2.121 -by(fast_int_arith_tac 1);
   2.122 +by(fast_arith_tac 1);
   2.123  Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c";
   2.124 -by(fast_int_arith_tac 1);
   2.125 +by(fast_arith_tac 1);
   2.126  Goal "!!a::int. [| a+b <= i+j; a<=b; i<=j |] \
   2.127  \     ==> a+a <= j+j";
   2.128 -by(fast_int_arith_tac 1);
   2.129 +by(fast_arith_tac 1);
   2.130  Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \
   2.131  \     ==> a+a - - #-1 < j+j - #3";
   2.132 -by(fast_int_arith_tac 1);
   2.133 +by(fast_arith_tac 1);
   2.134  Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
   2.135 -by(int_arith_tac 1);
   2.136 +by(arith_tac 1);
   2.137  Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   2.138  \     ==> a <= l";
   2.139 -by(fast_int_arith_tac 1);
   2.140 +by(fast_arith_tac 1);
   2.141  Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   2.142  \     ==> a+a+a+a <= l+l+l+l";
   2.143 -by(fast_int_arith_tac 1);
   2.144 +by(fast_arith_tac 1);
   2.145  Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   2.146  \     ==> a+a+a+a+a <= l+l+l+l+i";
   2.147 -by(fast_int_arith_tac 1);
   2.148 +by(fast_arith_tac 1);
   2.149  Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   2.150  \     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
   2.151 -by(fast_int_arith_tac 1);
   2.152 +by(fast_arith_tac 1);
   2.153  *)
   2.154  
   2.155  (*---------------------------------------------------------------------------*)
   2.156 @@ -544,50 +547,50 @@
   2.157  (** Simplification of inequalities involving numerical constants **)
   2.158  
   2.159  Goal "(w <= z + #1) = (w<=z | w = z + #1)";
   2.160 -by(int_arith_tac 1);
   2.161 +by(arith_tac 1);
   2.162  qed "zle_add1_eq";
   2.163  
   2.164  Goal "(w <= z - #1) = (w<z)";
   2.165 -by(int_arith_tac 1);
   2.166 +by(arith_tac 1);
   2.167  qed "zle_diff1_eq";
   2.168  Addsimps [zle_diff1_eq];
   2.169  
   2.170  (*2nd premise can be proved automatically if v is a literal*)
   2.171  Goal "[| w <= z; #0 <= v |] ==> w <= z + v";
   2.172 -by(fast_int_arith_tac 1);
   2.173 +by(fast_arith_tac 1);
   2.174  qed "zle_imp_zle_zadd";
   2.175  
   2.176  Goal "w <= z ==> w <= z + #1";
   2.177 -by(fast_int_arith_tac 1);
   2.178 +by(fast_arith_tac 1);
   2.179  qed "zle_imp_zle_zadd1";
   2.180  
   2.181  (*2nd premise can be proved automatically if v is a literal*)
   2.182  Goal "[| w < z; #0 <= v |] ==> w < z + v";
   2.183 -by(fast_int_arith_tac 1);
   2.184 +by(fast_arith_tac 1);
   2.185  qed "zless_imp_zless_zadd";
   2.186  
   2.187  Goal "w < z ==> w < z + #1";
   2.188 -by(fast_int_arith_tac 1);
   2.189 +by(fast_arith_tac 1);
   2.190  qed "zless_imp_zless_zadd1";
   2.191  
   2.192  Goal "(w < z + #1) = (w<=z)";
   2.193 -by(int_arith_tac 1);
   2.194 +by(arith_tac 1);
   2.195  qed "zle_add1_eq_le";
   2.196  Addsimps [zle_add1_eq_le];
   2.197  
   2.198  Goal "(z = z + w) = (w = #0)";
   2.199 -by(int_arith_tac 1);
   2.200 +by(arith_tac 1);
   2.201  qed "zadd_left_cancel0";
   2.202  Addsimps [zadd_left_cancel0];
   2.203  
   2.204  (*LOOPS as a simprule!*)
   2.205  Goal "[| w + v < z; #0 <= v |] ==> w < z";
   2.206 -by(fast_int_arith_tac 1);
   2.207 +by(fast_arith_tac 1);
   2.208  qed "zless_zadd_imp_zless";
   2.209  
   2.210  (*LOOPS as a simprule!  Analogous to Suc_lessD*)
   2.211  Goal "w + #1 < z ==> w < z";
   2.212 -by(fast_int_arith_tac 1);
   2.213 +by(fast_arith_tac 1);
   2.214  qed "zless_zadd1_imp_zless";
   2.215  
   2.216  Goal "w + #-1 = w - #1";
     3.1 --- a/src/HOL/Lambda/Eta.ML	Thu Jan 14 12:32:13 1999 +0100
     3.2 +++ b/src/HOL/Lambda/Eta.ML	Thu Jan 14 13:18:09 1999 +0100
     3.3 @@ -29,7 +29,7 @@
     3.4  Goal "!i k. free (lift t k) i = (i < k & free t i | k < i & free t (i-1))";
     3.5  by (induct_tac "t" 1);
     3.6    by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()) addcongs [conj_cong])));
     3.7 - by(nat_arith_tac 1);
     3.8 + by(arith_tac 1);
     3.9  by(Auto_tac);
    3.10  qed "free_lift";
    3.11  Addsimps [free_lift];
     4.1 --- a/src/HOL/Lambda/ListApplication.ML	Thu Jan 14 12:32:13 1999 +0100
     4.2 +++ b/src/HOL/Lambda/ListApplication.ML	Thu Jan 14 13:18:09 1999 +0100
     4.3 @@ -88,7 +88,7 @@
     4.4  Addsimps [size_apps];
     4.5  
     4.6  Goal "[| 0 < k; m <= n |] ==> m < n+k";
     4.7 -by(fast_nat_arith_tac 1);
     4.8 +by(fast_arith_tac 1);
     4.9  val lemma = result();
    4.10  
    4.11  (* a customized induction schema for $$ *)
     5.1 --- a/src/HOL/Ord.ML	Thu Jan 14 12:32:13 1999 +0100
     5.2 +++ b/src/HOL/Ord.ML	Thu Jan 14 13:18:09 1999 +0100
     5.3 @@ -104,6 +104,28 @@
     5.4  by (Blast_tac 1);
     5.5  qed "linorder_less_linear";
     5.6  
     5.7 +Goal "!!x::'a::linorder. (~ x < y) = (y <= x)";
     5.8 +by (simp_tac (simpset() addsimps [order_less_le]) 1);
     5.9 +by (cut_facts_tac [linorder_linear] 1);
    5.10 +by (blast_tac (claset() addIs [order_antisym]) 1);
    5.11 +qed "linorder_not_less";
    5.12 +
    5.13 +Goal "!!x::'a::linorder. (~ x <= y) = (y < x)";
    5.14 +by (simp_tac (simpset() addsimps [order_less_le]) 1);
    5.15 +by (cut_facts_tac [linorder_linear] 1);
    5.16 +by (blast_tac (claset() addIs [order_antisym]) 1);
    5.17 +qed "linorder_not_le";
    5.18 +
    5.19 +Goal "!!x::'a::linorder. (x ~= y) = (x<y | y<x)";
    5.20 +by (cut_inst_tac [("x","x"),("y","y")] linorder_less_linear 1);
    5.21 +by Auto_tac;
    5.22 +qed "linorder_neq_iff";
    5.23 +
    5.24 +(* eliminates ~= in premises *)
    5.25 +bind_thm("linorder_neqE", linorder_neq_iff RS iffD1 RS disjE);
    5.26 +
    5.27 +(** min & max **)
    5.28 +
    5.29  Goalw [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)";
    5.30  by (Simp_tac 1);
    5.31  by (cut_facts_tac [linorder_linear] 1);
    5.32 @@ -136,17 +158,3 @@
    5.33  by (cut_facts_tac [linorder_linear] 1);
    5.34  by (blast_tac (claset() addIs [order_trans]) 1);
    5.35  qed "min_le_iff_disj";
    5.36 -
    5.37 -Goal "!!x::'a::linorder. (x ~= y) = (x<y | y<x)";
    5.38 -by (cut_inst_tac [("x","x"),("y","y")] linorder_less_linear 1);
    5.39 -by Auto_tac;
    5.40 -qed "linorder_neq_iff";
    5.41 -
    5.42 -(*** eliminates ~= in premises ***)
    5.43 -bind_thm("linorder_neqE", linorder_neq_iff RS iffD1 RS disjE);
    5.44 -
    5.45 -Goal "!!x::'a::linorder. (~ x < y) = (y <= x)";
    5.46 -by (simp_tac (simpset() addsimps [order_less_le]) 1);
    5.47 -by (cut_facts_tac [linorder_linear] 1);
    5.48 -by (blast_tac (claset() addIs [order_antisym]) 1);
    5.49 -qed "linorder_not_less";
     6.1 --- a/src/HOL/UNITY/LessThan.ML	Thu Jan 14 12:32:13 1999 +0100
     6.2 +++ b/src/HOL/UNITY/LessThan.ML	Thu Jan 14 13:18:09 1999 +0100
     6.3 @@ -7,10 +7,6 @@
     6.4  *)
     6.5  
     6.6  
     6.7 -(*Make Auto_tac and Force_tac try lin_arith_tac!*)
     6.8 -claset_ref() := claset() addaltern ("lin_arith_tac",Fast_Nat_Arith.lin_arith_tac);
     6.9 -
    6.10 -
    6.11  (*** lessThan ***)
    6.12  
    6.13  Goalw [lessThan_def] "(i: lessThan k) = (i<k)";
     7.1 --- a/src/HOL/UNITY/Lift.ML	Thu Jan 14 12:32:13 1999 +0100
     7.2 +++ b/src/HOL/UNITY/Lift.ML	Thu Jan 14 13:18:09 1999 +0100
     7.3 @@ -275,8 +275,7 @@
     7.4      (asm_simp_tac (simpset() addsimps [zle_def]@metric_simps @ zcompare_rls)));
     7.5  (** LEVEL 5 **)
     7.6  by (dres_inst_tac [("w1","Min")] (zle_iff_zadd RS iffD1) 1);
     7.7 -by Auto_tac;
     7.8 -by (full_simp_tac (simpset() addsimps [zadd_int_left]) 1);
     7.9 +by (Blast_tac 1);
    7.10  qed "E_thm16a";
    7.11  
    7.12  (*lem_lift_5_1 has ~goingup instead of goingdown*)
    7.13 @@ -292,10 +291,7 @@
    7.14  		                      metric_simps @ zcompare_rls)));
    7.15  (** LEVEL 5 **)
    7.16  by (dres_inst_tac [("z1","Max")] (zle_iff_zadd RS iffD1) 1);
    7.17 -by (etac exE 1);  
    7.18 -by (etac ssubst 1);
    7.19 -by Auto_tac;
    7.20 -by (full_simp_tac (simpset() addsimps [zadd_int_left]) 1);
    7.21 +by (Blast_tac 1);
    7.22  qed "E_thm16b";
    7.23  
    7.24  
     8.1 --- a/src/HOL/simpdata.ML	Thu Jan 14 12:32:13 1999 +0100
     8.2 +++ b/src/HOL/simpdata.ML	Thu Jan 14 13:18:09 1999 +0100
     8.3 @@ -64,31 +64,28 @@
     8.4  
     8.5    fun prover s = prove_goal HOL.thy s (K [Blast_tac 1]);
     8.6  
     8.7 -  val P_imp_P_iff_True = prover "P --> (P = True)" RS mp;
     8.8 -  val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;
     8.9 -
    8.10 -  val not_P_imp_P_iff_F = prover "~P --> (P = False)" RS mp;
    8.11 -  val not_P_imp_P_eq_False = not_P_imp_P_iff_F RS eq_reflection;
    8.12 -
    8.13  in
    8.14  
    8.15  (*Make meta-equalities.  The operator below is Trueprop*)
    8.16  
    8.17 -  fun mk_meta_eq r = r RS eq_reflection;
    8.18 +fun mk_meta_eq r = r RS eq_reflection;
    8.19 +
    8.20 +val Eq_TrueI  = mk_meta_eq(prover  "P --> (P = True)"  RS mp);
    8.21 +val Eq_FalseI = mk_meta_eq(prover "~P --> (P = False)" RS mp);
    8.22  
    8.23 -  fun mk_eq th = case concl_of th of
    8.24 -          Const("==",_)$_$_       => th
    8.25 -      |   _$(Const("op =",_)$_$_) => mk_meta_eq th
    8.26 -      |   _$(Const("Not",_)$_)    => th RS not_P_imp_P_eq_False
    8.27 -      |   _                       => th RS P_imp_P_eq_True;
    8.28 -  (* last 2 lines requires all formulae to be of the from Trueprop(.) *)
    8.29 +fun mk_eq th = case concl_of th of
    8.30 +        Const("==",_)$_$_       => th
    8.31 +    |   _$(Const("op =",_)$_$_) => mk_meta_eq th
    8.32 +    |   _$(Const("Not",_)$_)    => th RS Eq_FalseI
    8.33 +    |   _                       => th RS Eq_TrueI;
    8.34 +(* last 2 lines requires all formulae to be of the from Trueprop(.) *)
    8.35  
    8.36 -  fun mk_eq_True r = Some(r RS meta_eq_to_obj_eq RS P_imp_P_eq_True);
    8.37 +fun mk_eq_True r = Some(r RS meta_eq_to_obj_eq RS Eq_TrueI);
    8.38  
    8.39 -  fun mk_meta_cong rl =
    8.40 -    standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
    8.41 -    handle THM _ =>
    8.42 -    error("Premises and conclusion of congruence rules must be =-equalities");
    8.43 +fun mk_meta_cong rl =
    8.44 +  standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
    8.45 +  handle THM _ =>
    8.46 +  error("Premises and conclusion of congruence rules must be =-equalities");
    8.47  
    8.48  val not_not = prover "(~ ~ P) = P";
    8.49  
    8.50 @@ -505,6 +502,6 @@
    8.51                 eresolve_tac [disjE] 1) THEN
    8.52          ref_tac 1;
    8.53    in EVERY'[TRY o filter_prems_tac test,
    8.54 -            REPEAT o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac,
    8.55 +            DETERM o REPEAT o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac,
    8.56              SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]
    8.57    end;
     9.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Thu Jan 14 12:32:13 1999 +0100
     9.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Thu Jan 14 13:18:09 1999 +0100
     9.3 @@ -26,11 +26,14 @@
     9.4    val neqE:             thm (* [| m ~= n; m < n ==> P; n < m ==> P |] ==> P *)
     9.5    val notI:             thm (* (P ==> False) ==> ~ P *)
     9.6    val not_lessD:        thm (* ~(m < n) ==> n <= m *)
     9.7 +  val not_leD:          thm (* ~(m <= n) ==> n < m *)
     9.8    val sym:		thm (* x = y ==> y = x *)
     9.9    val mk_Eq: thm -> thm
    9.10    val mk_Trueprop: term -> term
    9.11    val neg_prop: term -> term
    9.12    val is_False: thm -> bool
    9.13 +  val is_nat: typ list * term -> bool
    9.14 +  val mk_nat_thm: Sign.sg -> term -> thm
    9.15  end;
    9.16  (*
    9.17  mk_Eq(~in) = `in == False'
    9.18 @@ -40,19 +43,20 @@
    9.19  neg_prop(t) = neg if t is wrapped up in Trueprop and
    9.20    nt is the (logically) negated version of t, where the negation
    9.21    of a negative term is the term itself (no double negation!);
    9.22 +
    9.23 +is_nat(parameter-types,t) =  t:nat
    9.24 +mk_nat_thm(t) = "0 <= t"
    9.25  *)
    9.26  
    9.27  signature LIN_ARITH_DATA =
    9.28  sig
    9.29 -  val add_mono_thms:    thm list
    9.30 +  val add_mono_thms:    thm list ref
    9.31                              (* [| i rel1 j; m rel2 n |] ==> i + m rel3 j + n *)
    9.32 -  val lessD:            thm (* m < n ==> Suc m <= n *)
    9.33 -  val not_leD:          thm (* ~(m <= n) ==> Suc n <= m *)
    9.34 -  val decomp: term ->
    9.35 -             ((term * int)list * int * string * (term * int)list * int)option
    9.36 -  val simp: thm -> thm
    9.37 -  val is_nat: typ list * term -> bool
    9.38 -  val mk_nat_thm: Sign.sg -> term -> thm
    9.39 +  val lessD:            thm list ref (* m < n ==> m+1 <= n *)
    9.40 +  val decomp:
    9.41 +    (term -> ((term * int)list * int * string * (term * int)list * int)option)
    9.42 +    ref
    9.43 +  val simp: (thm -> thm) ref
    9.44  end;
    9.45  (*
    9.46  decomp(`x Rel y') should yield (p,i,Rel,q,j)
    9.47 @@ -63,9 +67,6 @@
    9.48  simp must reduce contradictory <= to False.
    9.49     It should also cancel common summands to keep <= reduced;
    9.50     otherwise <= can grow to massive proportions.
    9.51 -
    9.52 -is_nat(parameter-types,t) =  t:nat
    9.53 -mk_nat_thm(t) = "0 <= t"
    9.54  *)
    9.55  
    9.56  signature FAST_LIN_ARITH =
    9.57 @@ -90,7 +91,9 @@
    9.58  
    9.59  datatype injust = Asm of int
    9.60                  | Nat of int (* index of atom *)
    9.61 -                | Fwd of injust * thm
    9.62 +                | LessD of injust
    9.63 +                | NotLessD of injust
    9.64 +                | NotLeD of injust
    9.65                  | Multiplied of int * injust
    9.66                  | Added of injust * injust;
    9.67  
    9.68 @@ -250,12 +253,12 @@
    9.69  fun mkthm sg asms just =
    9.70    let val atoms = foldl (fn (ats,(lhs,_,_,rhs,_)) =>
    9.71                              map fst lhs  union  (map fst rhs  union  ats))
    9.72 -                        ([], mapfilter (LA_Data.decomp o concl_of) asms)
    9.73 +                        ([], mapfilter (!LA_Data.decomp o concl_of) asms)
    9.74  
    9.75        fun addthms thm1 thm2 =
    9.76          let val conj = thm1 RS (thm2 RS LA_Logic.conjI)
    9.77          in the(get_first (fn th => Some(conj RS th) handle _ => None)
    9.78 -                         LA_Data.add_mono_thms)
    9.79 +                         (!LA_Data.add_mono_thms))
    9.80          end;
    9.81  
    9.82        fun multn(n,thm) =
    9.83 @@ -263,16 +266,18 @@
    9.84          in if n < 0 then mul(~n,thm) RS LA_Logic.sym else mul(n,thm) end;
    9.85  
    9.86        fun simp thm =
    9.87 -        let val thm' = LA_Data.simp thm
    9.88 +        let val thm' = !LA_Data.simp thm
    9.89          in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end
    9.90  
    9.91        fun mk(Asm i) = nth_elem(i,asms)
    9.92 -        | mk(Nat(i)) = LA_Data.mk_nat_thm sg (nth_elem(i,atoms))
    9.93 -        | mk(Fwd(j,thm)) = mk j RS thm
    9.94 +        | mk(Nat(i)) = LA_Logic.mk_nat_thm sg (nth_elem(i,atoms))
    9.95 +        | mk(LessD(j)) = hd([mk j] RL !LA_Data.lessD)
    9.96 +        | mk(NotLeD(j)) = hd([mk j RS LA_Logic.not_leD] RL !LA_Data.lessD)
    9.97 +        | mk(NotLessD(j)) = mk j RS LA_Logic.not_lessD
    9.98          | mk(Added(j1,j2)) = simp(addthms (mk j1) (mk j2))
    9.99          | mk(Multiplied(n,j)) = multn(n,mk j)
   9.100  
   9.101 -  in LA_Data.simp(mk just) handle FalseE thm => thm end
   9.102 +  in !LA_Data.simp(mk just) handle FalseE thm => thm end
   9.103  end;
   9.104  
   9.105  fun coeff poly atom = case assoc(poly,atom) of None => 0 | Some i => i;
   9.106 @@ -287,9 +292,9 @@
   9.107          val just = Asm k
   9.108      in case rel of
   9.109          "<="   => Some(Lineq(c,Le,diff,just))
   9.110 -       | "~<=" => Some(Lineq(1-c,Le,map (op ~) diff,Fwd(just,LA_Data.not_leD)))
   9.111 -       | "<"   => Some(Lineq(c+1,Le,diff,Fwd(just,LA_Data.lessD)))
   9.112 -       | "~<"  => Some(Lineq(~c,Le,map (op~) diff,Fwd(just,LA_Logic.not_lessD)))
   9.113 +       | "~<=" => Some(Lineq(1-c,Le,map (op ~) diff,NotLeD(just)))
   9.114 +       | "<"   => Some(Lineq(c+1,Le,diff,LessD(just)))
   9.115 +       | "~<"  => Some(Lineq(~c,Le,map (op~) diff,NotLessD(just)))
   9.116         | "="   => Some(Lineq(c,Eq,diff,just))
   9.117         | "~="  => None
   9.118         | _     => sys_error("mklineq" ^ rel)   
   9.119 @@ -297,7 +302,7 @@
   9.120    end;
   9.121  
   9.122  fun mknat pTs ixs (atom,i) =
   9.123 -  if LA_Data.is_nat(pTs,atom)
   9.124 +  if LA_Logic.is_nat(pTs,atom)
   9.125    then let val l = map (fn j => if j=i then 1 else 0) ixs
   9.126         in Some(Lineq(0,Le,l,Nat(i))) end
   9.127    else None
   9.128 @@ -345,9 +350,9 @@
   9.129  fun prove(pTs,Hs,concl) =
   9.130  let val nHs = length Hs
   9.131      val ixHs = Hs ~~ (0 upto (nHs-1))
   9.132 -    val Hitems = mapfilter (fn (h,i) => case LA_Data.decomp h of
   9.133 +    val Hitems = mapfilter (fn (h,i) => case !LA_Data.decomp h of
   9.134                                   None => None | Some(it) => Some(it,i)) ixHs
   9.135 -in case LA_Data.decomp concl of
   9.136 +in case !LA_Data.decomp concl of
   9.137       None => if null Hitems then [] else refute1(pTs,Hitems)
   9.138     | Some(citem as (r,i,rel,l,j)) =>
   9.139         if rel = "="