--- a/src/HOL/Integ/Bin.ML Tue Sep 21 14:13:45 1999 +0200
+++ b/src/HOL/Integ/Bin.ML Tue Sep 21 14:13:55 1999 +0200
@@ -465,7 +465,7 @@
Addsimps [nested_number_of_add, nested_diff1_number_of_add,
nested_diff2_number_of_add, nested_number_of_mult];
-
+use "bin_simprocs";
(*---------------------------------------------------------------------------*)
(* Linear arithmetic *)
@@ -485,44 +485,13 @@
val lessD = Nat_LA_Data.lessD @ [add1_zle_eq RS iffD2];
-fun add_atom(t,m,(p,i)) = (case assoc(p,t) of None => ((t,m)::p,i)
- | Some n => (overwrite(p,(t,n+m:int)), i));
-
-(* Turn term into list of summand * multiplicity plus a constant *)
-fun poly(Const("op +",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi))
- | poly(Const("op -",_) $ s $ t, m, pi) = poly(s,m,poly(t,~1*m,pi))
- | poly(Const("uminus",_) $ t, m, pi) = poly(t,~1*m,pi)
- | poly(all as Const("op *",_) $ (Const("Numeral.number_of",_)$c) $ t, m, pi) =
- (poly(t,m*NumeralSyntax.dest_bin c,pi) handle Match => add_atom(all,m,pi))
- | poly(all as Const("Numeral.number_of",_)$t,m,(p,i)) =
- ((p,i + m*NumeralSyntax.dest_bin t) handle Match => add_atom(all,m,(p,i)))
- | poly x = add_atom x;
-
-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)
- | "op <=" => Some(p,i,"<=",q,j)
- | "op =" => Some(p,i,"=",q,j)
- | _ => None
- end;
-
-val intT = Type("IntDef.int",[]);
-fun iib T = T = ([intT,intT] ---> HOLogic.boolT);
-
-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))) =
- 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 add_rules = simp_thms @ bin_arith_simps @ bin_rel_simps @
+ [int_0,zmult_0,zmult_0_right];
val cancel_sums_ss = Nat_LA_Data.cancel_sums_ss addsimps add_rules
- addsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv];
+ addsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv,
+ Int_CC.sum_conv, Int_CC.rel_conv];
val simp = simplify cancel_sums_ss;
@@ -541,8 +510,8 @@
(* 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;
+LA_Data_Ref.discrete := !LA_Data_Ref.discrete @ [("IntDef.int",true)];
val int_arith_simproc_pats =
--- a/src/HOL/Integ/IntDiv.ML Tue Sep 21 14:13:45 1999 +0200
+++ b/src/HOL/Integ/IntDiv.ML Tue Sep 21 14:13:55 1999 +0200
@@ -131,8 +131,6 @@
by (etac splitE 1);
by (auto_tac (claset(),
simpset() addsimps zmult_ac@[zadd_zmult_distrib2, Let_def]));
-(*the "just double" case*)
-by (asm_full_simp_tac (simpset() addsimps zcompare_rls@[zmult_2_right]) 1);
qed_spec_mp "posDivAlg_correct";
@@ -175,8 +173,6 @@
by (etac splitE 1);
by (auto_tac (claset(),
simpset() addsimps zmult_ac@[zadd_zmult_distrib2, Let_def]));
-(*the "just double" case*)
-by (asm_full_simp_tac (simpset() addsimps zcompare_rls@[zmult_2_right]) 1);
qed_spec_mp "negDivAlg_correct";
@@ -344,7 +340,6 @@
by (subgoal_tac "#0 <= a*(#1-q)" 1);
by (asm_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 2);
by (asm_full_simp_tac (simpset() addsimps [pos_imp_zmult_nonneg_iff]) 1);
-by (full_simp_tac (simpset() addsimps zcompare_rls) 1);
val lemma2 = result();
Goal "[| quorem((a,a),(q,r)); a ~= (#0::int) |] ==> q = #1";
@@ -566,14 +561,13 @@
\ ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))";
by (auto_tac
(claset(),
- simpset() addsimps split_ifs@zmult_ac@
+ simpset() delsimprocs [Int_CC.sum_conv, Int_CC.rel_conv]
+ addsimps split_ifs@zmult_ac@
[quorem_def, linorder_neq_iff,
zadd_zmult_distrib2,
pos_mod_sign,pos_mod_bound,
neg_mod_sign, neg_mod_bound]));
-by (rtac (zmod_zdiv_equality RS trans) 2);
-by (rtac (zmod_zdiv_equality RS trans) 1);
-by Auto_tac;
+by (ALLGOALS(rtac zmod_zdiv_equality));
val lemma = result();
Goal "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)";
@@ -613,14 +607,13 @@
\ ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))";
by (auto_tac
(claset(),
- simpset() addsimps split_ifs@zmult_ac@
+ simpset() delsimprocs [Int_CC.sum_conv, Int_CC.rel_conv]
+ addsimps split_ifs@zmult_ac@
[quorem_def, linorder_neq_iff,
zadd_zmult_distrib2,
pos_mod_sign,pos_mod_bound,
neg_mod_sign, neg_mod_bound]));
-by (rtac (zmod_zdiv_equality RS trans) 2);
-by (rtac (zmod_zdiv_equality RS trans) 1);
-by Auto_tac;
+by (ALLGOALS(rtac zmod_zdiv_equality));
val lemma = result();
(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
@@ -727,15 +720,14 @@
\ ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))";
by (auto_tac (*SLOW*)
(claset(),
- simpset() addsimps split_ifs@zmult_ac@
+ simpset() delsimprocs [Int_CC.sum_conv, Int_CC.rel_conv]
+ addsimps split_ifs@zmult_ac@
[quorem_def, linorder_neq_iff,
pos_imp_zmult_pos_iff,
neg_imp_zmult_pos_iff,
zadd_zmult_distrib2 RS sym,
lemma1, lemma2, lemma3, lemma4]));
-by (rtac (zmod_zdiv_equality RS trans) 2);
-by (rtac (zmod_zdiv_equality RS trans) 1);
-by Auto_tac;
+by (ALLGOALS(rtac zmod_zdiv_equality));
val lemma = result();
Goal "(#0::int) < c ==> a div (b*c) = (a div b) div c";
@@ -829,9 +821,9 @@
by (asm_simp_tac (simpset() addsimps [zdiv_zmult_zmult2, zmod_zmult_zmult2,
div_pos_pos_trivial]) 1);
by (stac div_pos_pos_trivial 1);
-by (asm_simp_tac (simpset() addsimps zadd_ac@
- [zmult_2_right, mod_pos_pos_trivial,
- pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1);
+by (asm_simp_tac (simpset() delsimprocs [Int_CC.sum_conv, Int_CC.rel_conv]
+ addsimps zadd_ac@ [zmult_2_right, mod_pos_pos_trivial,
+ pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1);
by (auto_tac (claset(),
simpset() addsimps [mod_pos_pos_trivial]));
qed "pos_zdiv_times_2";
@@ -863,7 +855,8 @@
by (simp_tac (simpset_of Int.thy
addsimps [zadd_assoc, number_of_BIT]) 1);
by (asm_simp_tac (simpset()
- delsimps bin_arith_extra_simps@bin_rel_simps
+ delsimprocs [Int_CC.sum_conv, Int_CC.rel_conv]
+ delsimps bin_arith_extra_simps@bin_rel_simps
addsimps [zmult_2 RS sym, zdiv_zmult_zmult1,
pos_zdiv_times_2, lemma, neg_zdiv_times_2]) 1);
qed "zdiv_number_of_BIT";
@@ -888,9 +881,9 @@
by (asm_simp_tac (simpset() addsimps [zmod_zmult_zmult2,
mod_pos_pos_trivial]) 1);
by (rtac mod_pos_pos_trivial 1);
-by (asm_simp_tac (simpset() addsimps zadd_ac@
- [zmult_2_right, mod_pos_pos_trivial,
- pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1);
+by (asm_simp_tac (simpset() delsimprocs [Int_CC.sum_conv, Int_CC.rel_conv]
+ addsimps zadd_ac@ [zmult_2_right, mod_pos_pos_trivial,
+ pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1);
by (auto_tac (claset(),
simpset() addsimps [mod_pos_pos_trivial]));
qed "pos_zmod_times_2";
@@ -921,6 +914,7 @@
by (simp_tac (simpset_of Int.thy
addsimps [zadd_assoc, number_of_BIT]) 1);
by (asm_simp_tac (simpset()
+ delsimprocs [Int_CC.sum_conv, Int_CC.rel_conv]
delsimps bin_arith_extra_simps@bin_rel_simps
addsimps [zmult_2 RS sym, zmod_zmult_zmult1,
pos_zmod_times_2, lemma, neg_zmod_times_2]) 1);