# HG changeset patch # User chaieb # Date 1132294438 -3600 # Node ID 46af82efd3113b858274a4d14f99c430fa43f3db # Parent 6c63f0eb16d7bd61e16d68b88fa4e8d1e2717061 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy diff -r 6c63f0eb16d7 -r 46af82efd311 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Fri Nov 18 07:10:37 2005 +0100 +++ b/src/HOL/Divides.thy Fri Nov 18 07:13:58 2005 +0100 @@ -858,6 +858,18 @@ qed +lemma mod_add_left_eq: "((a::nat) + b) mod c = (a mod c + b) mod c" + apply (rule trans [symmetric]) + apply (rule mod_add1_eq, simp) + apply (rule mod_add1_eq [symmetric]) + done + +lemma mod_add_right_eq: "(a+b) mod (c::nat) = (a + (b mod c)) mod c" +apply (rule trans [symmetric]) +apply (rule mod_add1_eq, simp) +apply (rule mod_add1_eq [symmetric]) +done + ML {* val div_def = thm "div_def" @@ -907,6 +919,8 @@ val mod_mult_distrib_mod = thm "mod_mult_distrib_mod"; val div_add1_eq = thm "div_add1_eq"; val mod_add1_eq = thm "mod_add1_eq"; +val mod_add_left_eq = thm "mod_add_left_eq"; + val mod_add_right_eq = thm "mod_add_right_eq"; val mod_lemma = thm "mod_lemma"; val div_mult2_eq = thm "div_mult2_eq"; val mod_mult2_eq = thm "mod_mult2_eq"; diff -r 6c63f0eb16d7 -r 46af82efd311 src/HOL/Integ/Presburger.thy --- a/src/HOL/Integ/Presburger.thy Fri Nov 18 07:10:37 2005 +0100 +++ b/src/HOL/Integ/Presburger.thy Fri Nov 18 07:13:58 2005 +0100 @@ -982,6 +982,99 @@ theorem conj_le_cong: "(0 <= x \ P = P') \ (0 <= (x::int) \ P) = (0 <= x \ P')" by (simp cong: conj_cong) + (* Theorems used in presburger.ML for the computation simpset*) + (* FIXME: They are present in Float.thy, so may be Float.thy should be lightened.*) + +lemma lift_bool: "x \ x=True" + by simp + +lemma nlift_bool: "~x \ x=False" + by simp + +lemma not_false_eq_true: "(~ False) = True" by simp + +lemma not_true_eq_false: "(~ True) = False" by simp + + +lemma int_eq_number_of_eq: "(((number_of v)::int)=(number_of w)) = iszero ((number_of (bin_add v (bin_minus w)))::int)" + by simp +lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)" + by (simp only: iszero_number_of_Pls) + +lemma int_nonzero_number_of_Min: "~(iszero ((-1)::int))" + by simp + +lemma int_iszero_number_of_0: "iszero ((number_of (w BIT bit.B0))::int) = iszero ((number_of w)::int)" + by simp + +lemma int_iszero_number_of_1: "\ iszero ((number_of (w BIT bit.B1))::int)" + by simp + +lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (bin_add x (bin_minus y)))::int)" + by simp + +lemma int_not_neg_number_of_Pls: "\ (neg (Numeral0::int))" + by simp + +lemma int_neg_number_of_Min: "neg (-1::int)" + by simp + +lemma int_neg_number_of_BIT: "neg ((number_of (w BIT x))::int) = neg ((number_of w)::int)" + by simp + +lemma int_le_number_of_eq: "(((number_of x)::int) \ number_of y) = (\ neg ((number_of (bin_add y (bin_minus x)))::int))" + by simp +lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (bin_add v w)" + by simp + +lemma int_number_of_diff_sym: "((number_of v)::int) - number_of w = number_of (bin_add v (bin_minus w))" + by simp + +lemma int_number_of_mult_sym: "((number_of v)::int) * number_of w = number_of (bin_mult v w)" + by simp + +lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (bin_minus v)" + by simp +lemma add_left_zero: "0 + a = (a::'a::comm_monoid_add)" + by simp + +lemma add_right_zero: "a + 0 = (a::'a::comm_monoid_add)" + by simp + +lemma mult_left_one: "1 * a = (a::'a::semiring_1)" + by simp + +lemma mult_right_one: "a * 1 = (a::'a::semiring_1)" + by simp + +lemma int_pow_0: "(a::int)^(Numeral0) = 1" + by simp + +lemma int_pow_1: "(a::int)^(Numeral1) = a" + by simp + +lemma zero_eq_Numeral0_nring: "(0::'a::number_ring) = Numeral0" + by simp + +lemma one_eq_Numeral1_nring: "(1::'a::number_ring) = Numeral1" + by simp + +lemma zero_eq_Numeral0_nat: "(0::nat) = Numeral0" + by simp + +lemma one_eq_Numeral1_nat: "(1::nat) = Numeral1" + by simp + +lemma zpower_Pls: "(z::int)^Numeral0 = Numeral1" + by simp + +lemma zpower_Min: "(z::int)^((-1)::nat) = Numeral1" +proof - + have 1:"((-1)::nat) = 0" + by simp + show ?thesis by (simp add: 1) +qed + use "cooper_dec.ML" use "reflected_presburger.ML" use "reflected_cooper.ML" diff -r 6c63f0eb16d7 -r 46af82efd311 src/HOL/Integ/presburger.ML --- a/src/HOL/Integ/presburger.ML Fri Nov 18 07:10:37 2005 +0100 +++ b/src/HOL/Integ/presburger.ML Fri Nov 18 07:13:58 2005 +0100 @@ -31,6 +31,38 @@ val presburger_ss = simpset_of (theory "Presburger"); +val binarith = map thm + ["Pls_0_eq", "Min_1_eq", + "bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0", + "bin_succ_Pls", "bin_succ_Min", "bin_succ_1", "bin_succ_0", + "bin_add_Pls", "bin_add_Min", "bin_add_BIT_0", "bin_add_BIT_10", + "bin_add_BIT_11", "bin_minus_Pls", "bin_minus_Min", "bin_minus_1", + "bin_minus_0", "bin_mult_Pls", "bin_mult_Min", "bin_mult_1", "bin_mult_0", + "bin_add_Pls_right", "bin_add_Min_right"]; + val intarithrel = + (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT", + "int_le_number_of_eq","int_iszero_number_of_0", + "int_less_number_of_eq_neg"]) @ + (map (fn s => thm s RS thm "lift_bool") + ["int_iszero_number_of_Pls","int_iszero_number_of_1", + "int_neg_number_of_Min"])@ + (map (fn s => thm s RS thm "nlift_bool") + ["int_nonzero_number_of_Min","int_not_neg_number_of_Pls"]); + +val intarith = map thm ["int_number_of_add_sym", "int_number_of_minus_sym", + "int_number_of_diff_sym", "int_number_of_mult_sym"]; +val natarith = map thm ["add_nat_number_of", "diff_nat_number_of", + "mult_nat_number_of", "eq_nat_number_of", + "less_nat_number_of"] +val powerarith = + (map thm ["nat_number_of", "zpower_number_of_even", + "zpower_Pls", "zpower_Min"]) @ + [(Tactic.simplify true [thm "zero_eq_Numeral0_nring", + thm "one_eq_Numeral1_nring"] + (thm "zpower_number_of_odd"))] + +val arith = binarith @ intarith @ intarithrel @ natarith + @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"]; fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = let val (xn1,p1) = variant_abs (xn,xT,p) @@ -59,6 +91,17 @@ val Suc_plus1 = thm "Suc_plus1"; val imp_le_cong = thm "imp_le_cong"; val conj_le_cong = thm "conj_le_cong"; +val nat_mod_add_eq = mod_add1_eq RS sym; +val nat_mod_add_left_eq = mod_add_left_eq RS sym; +val nat_mod_add_right_eq = mod_add_right_eq RS sym; +val int_mod_add_eq = zmod_zadd1_eq RS sym; +val int_mod_add_left_eq = zmod_zadd_left_eq RS sym; +val int_mod_add_right_eq = zmod_zadd_right_eq RS sym; +val nat_div_add_eq = div_add1_eq RS sym; +val int_div_add_eq = zdiv_zadd1_eq RS sym; +val ZDIVISION_BY_ZERO_MOD = DIVISION_BY_ZERO RS conjunct2; +val ZDIVISION_BY_ZERO_DIV = DIVISION_BY_ZERO RS conjunct1; + (* extract all the constants in a term*) fun add_term_typed_consts (Const (c, T), cs) = (c,T) ins cs @@ -246,8 +289,21 @@ (* Transform the term*) val (t,np,nh) = prepare_for_presburger sg q g' (* Some simpsets for dealing with mod div abs and nat*) + val mod_div_simpset = HOL_basic_ss + addsimps [refl,nat_mod_add_eq, nat_mod_add_left_eq, + nat_mod_add_right_eq, int_mod_add_eq, + int_mod_add_right_eq, int_mod_add_left_eq, + nat_div_add_eq, int_div_add_eq, + mod_self, zmod_self, + DIVISION_BY_ZERO_MOD,DIVISION_BY_ZERO_DIV, + ZDIVISION_BY_ZERO_MOD,ZDIVISION_BY_ZERO_DIV, + zdiv_zero,zmod_zero,div_0,mod_0, + zdiv_1,zmod_1,div_1,mod_1] + addsimps add_ac + addsimprocs [cancel_div_mod_proc] val simpset0 = HOL_basic_ss addsimps [mod_div_equality', Suc_plus1] + addsimps arith addsplits [split_zdiv, split_zmod, split_div', split_min, split_max] (* Simp rules for changing (n::int) to int n *) val simpset1 = HOL_basic_ss @@ -264,7 +320,7 @@ val ct = cterm_of sg (HOLogic.mk_Trueprop t) (* Theorem for the nat --> int transformation *) val pre_thm = Seq.hd (EVERY - [simp_tac simpset0 1, + [simp_tac mod_div_simpset 1, simp_tac simpset0 1, TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1), TRY (simp_tac simpset3 1), TRY (simp_tac presburger_ss 1)] (trivial ct)) diff -r 6c63f0eb16d7 -r 46af82efd311 src/HOL/Presburger.thy --- a/src/HOL/Presburger.thy Fri Nov 18 07:10:37 2005 +0100 +++ b/src/HOL/Presburger.thy Fri Nov 18 07:13:58 2005 +0100 @@ -982,6 +982,99 @@ theorem conj_le_cong: "(0 <= x \ P = P') \ (0 <= (x::int) \ P) = (0 <= x \ P')" by (simp cong: conj_cong) + (* Theorems used in presburger.ML for the computation simpset*) + (* FIXME: They are present in Float.thy, so may be Float.thy should be lightened.*) + +lemma lift_bool: "x \ x=True" + by simp + +lemma nlift_bool: "~x \ x=False" + by simp + +lemma not_false_eq_true: "(~ False) = True" by simp + +lemma not_true_eq_false: "(~ True) = False" by simp + + +lemma int_eq_number_of_eq: "(((number_of v)::int)=(number_of w)) = iszero ((number_of (bin_add v (bin_minus w)))::int)" + by simp +lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)" + by (simp only: iszero_number_of_Pls) + +lemma int_nonzero_number_of_Min: "~(iszero ((-1)::int))" + by simp + +lemma int_iszero_number_of_0: "iszero ((number_of (w BIT bit.B0))::int) = iszero ((number_of w)::int)" + by simp + +lemma int_iszero_number_of_1: "\ iszero ((number_of (w BIT bit.B1))::int)" + by simp + +lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (bin_add x (bin_minus y)))::int)" + by simp + +lemma int_not_neg_number_of_Pls: "\ (neg (Numeral0::int))" + by simp + +lemma int_neg_number_of_Min: "neg (-1::int)" + by simp + +lemma int_neg_number_of_BIT: "neg ((number_of (w BIT x))::int) = neg ((number_of w)::int)" + by simp + +lemma int_le_number_of_eq: "(((number_of x)::int) \ number_of y) = (\ neg ((number_of (bin_add y (bin_minus x)))::int))" + by simp +lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (bin_add v w)" + by simp + +lemma int_number_of_diff_sym: "((number_of v)::int) - number_of w = number_of (bin_add v (bin_minus w))" + by simp + +lemma int_number_of_mult_sym: "((number_of v)::int) * number_of w = number_of (bin_mult v w)" + by simp + +lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (bin_minus v)" + by simp +lemma add_left_zero: "0 + a = (a::'a::comm_monoid_add)" + by simp + +lemma add_right_zero: "a + 0 = (a::'a::comm_monoid_add)" + by simp + +lemma mult_left_one: "1 * a = (a::'a::semiring_1)" + by simp + +lemma mult_right_one: "a * 1 = (a::'a::semiring_1)" + by simp + +lemma int_pow_0: "(a::int)^(Numeral0) = 1" + by simp + +lemma int_pow_1: "(a::int)^(Numeral1) = a" + by simp + +lemma zero_eq_Numeral0_nring: "(0::'a::number_ring) = Numeral0" + by simp + +lemma one_eq_Numeral1_nring: "(1::'a::number_ring) = Numeral1" + by simp + +lemma zero_eq_Numeral0_nat: "(0::nat) = Numeral0" + by simp + +lemma one_eq_Numeral1_nat: "(1::nat) = Numeral1" + by simp + +lemma zpower_Pls: "(z::int)^Numeral0 = Numeral1" + by simp + +lemma zpower_Min: "(z::int)^((-1)::nat) = Numeral1" +proof - + have 1:"((-1)::nat) = 0" + by simp + show ?thesis by (simp add: 1) +qed + use "cooper_dec.ML" use "reflected_presburger.ML" use "reflected_cooper.ML" diff -r 6c63f0eb16d7 -r 46af82efd311 src/HOL/Tools/Presburger/presburger.ML --- a/src/HOL/Tools/Presburger/presburger.ML Fri Nov 18 07:10:37 2005 +0100 +++ b/src/HOL/Tools/Presburger/presburger.ML Fri Nov 18 07:13:58 2005 +0100 @@ -31,6 +31,38 @@ val presburger_ss = simpset_of (theory "Presburger"); +val binarith = map thm + ["Pls_0_eq", "Min_1_eq", + "bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0", + "bin_succ_Pls", "bin_succ_Min", "bin_succ_1", "bin_succ_0", + "bin_add_Pls", "bin_add_Min", "bin_add_BIT_0", "bin_add_BIT_10", + "bin_add_BIT_11", "bin_minus_Pls", "bin_minus_Min", "bin_minus_1", + "bin_minus_0", "bin_mult_Pls", "bin_mult_Min", "bin_mult_1", "bin_mult_0", + "bin_add_Pls_right", "bin_add_Min_right"]; + val intarithrel = + (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT", + "int_le_number_of_eq","int_iszero_number_of_0", + "int_less_number_of_eq_neg"]) @ + (map (fn s => thm s RS thm "lift_bool") + ["int_iszero_number_of_Pls","int_iszero_number_of_1", + "int_neg_number_of_Min"])@ + (map (fn s => thm s RS thm "nlift_bool") + ["int_nonzero_number_of_Min","int_not_neg_number_of_Pls"]); + +val intarith = map thm ["int_number_of_add_sym", "int_number_of_minus_sym", + "int_number_of_diff_sym", "int_number_of_mult_sym"]; +val natarith = map thm ["add_nat_number_of", "diff_nat_number_of", + "mult_nat_number_of", "eq_nat_number_of", + "less_nat_number_of"] +val powerarith = + (map thm ["nat_number_of", "zpower_number_of_even", + "zpower_Pls", "zpower_Min"]) @ + [(Tactic.simplify true [thm "zero_eq_Numeral0_nring", + thm "one_eq_Numeral1_nring"] + (thm "zpower_number_of_odd"))] + +val arith = binarith @ intarith @ intarithrel @ natarith + @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"]; fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = let val (xn1,p1) = variant_abs (xn,xT,p) @@ -59,6 +91,17 @@ val Suc_plus1 = thm "Suc_plus1"; val imp_le_cong = thm "imp_le_cong"; val conj_le_cong = thm "conj_le_cong"; +val nat_mod_add_eq = mod_add1_eq RS sym; +val nat_mod_add_left_eq = mod_add_left_eq RS sym; +val nat_mod_add_right_eq = mod_add_right_eq RS sym; +val int_mod_add_eq = zmod_zadd1_eq RS sym; +val int_mod_add_left_eq = zmod_zadd_left_eq RS sym; +val int_mod_add_right_eq = zmod_zadd_right_eq RS sym; +val nat_div_add_eq = div_add1_eq RS sym; +val int_div_add_eq = zdiv_zadd1_eq RS sym; +val ZDIVISION_BY_ZERO_MOD = DIVISION_BY_ZERO RS conjunct2; +val ZDIVISION_BY_ZERO_DIV = DIVISION_BY_ZERO RS conjunct1; + (* extract all the constants in a term*) fun add_term_typed_consts (Const (c, T), cs) = (c,T) ins cs @@ -246,8 +289,21 @@ (* Transform the term*) val (t,np,nh) = prepare_for_presburger sg q g' (* Some simpsets for dealing with mod div abs and nat*) + val mod_div_simpset = HOL_basic_ss + addsimps [refl,nat_mod_add_eq, nat_mod_add_left_eq, + nat_mod_add_right_eq, int_mod_add_eq, + int_mod_add_right_eq, int_mod_add_left_eq, + nat_div_add_eq, int_div_add_eq, + mod_self, zmod_self, + DIVISION_BY_ZERO_MOD,DIVISION_BY_ZERO_DIV, + ZDIVISION_BY_ZERO_MOD,ZDIVISION_BY_ZERO_DIV, + zdiv_zero,zmod_zero,div_0,mod_0, + zdiv_1,zmod_1,div_1,mod_1] + addsimps add_ac + addsimprocs [cancel_div_mod_proc] val simpset0 = HOL_basic_ss addsimps [mod_div_equality', Suc_plus1] + addsimps arith addsplits [split_zdiv, split_zmod, split_div', split_min, split_max] (* Simp rules for changing (n::int) to int n *) val simpset1 = HOL_basic_ss @@ -264,7 +320,7 @@ val ct = cterm_of sg (HOLogic.mk_Trueprop t) (* Theorem for the nat --> int transformation *) val pre_thm = Seq.hd (EVERY - [simp_tac simpset0 1, + [simp_tac mod_div_simpset 1, simp_tac simpset0 1, TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1), TRY (simp_tac simpset3 1), TRY (simp_tac presburger_ss 1)] (trivial ct))