# HG changeset patch # User nipkow # Date 937916035 -7200 # Node ID 1dcf2a7a2b5b781f9cd99c26d328311460f8b5ba # Parent 9e29a3af64ab24044ea61ac6a519764418350ead Integ/bin_simprocs.ML now loaded in Integ/Bin.ML diff -r 9e29a3af64ab -r 1dcf2a7a2b5b src/HOL/Integ/Bin.ML --- 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 = diff -r 9e29a3af64ab -r 1dcf2a7a2b5b src/HOL/Integ/IntDiv.ML --- 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);