src/HOL/Arith.ML
changeset 6128 2acc5d36610c
parent 6115 c70bce7deb0f
child 6151 5892fdda22c9
     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";