Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
authorchaieb
Fri, 18 Nov 2005 07:13:58 +0100
changeset 18202 46af82efd311
parent 18201 6c63f0eb16d7
child 18203 9bd26bda96ef
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
src/HOL/Divides.thy file | annotate | diff | comparison | revisions
src/HOL/Integ/Presburger.thy file | annotate | diff | comparison | revisions
src/HOL/Integ/presburger.ML file | annotate | diff | comparison | revisions
src/HOL/Presburger.thy file | annotate | diff | comparison | revisions
src/HOL/Tools/Presburger/presburger.ML file | annotate | diff | comparison | revisions 
--- 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";
--- 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 \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> 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 \<Longrightarrow> x=True"
+  by simp
+
+lemma nlift_bool: "~x \<Longrightarrow> 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: "\<not> 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: "\<not> (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) \<le> number_of y) = (\<not> 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"
--- 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))
--- 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 \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> 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 \<Longrightarrow> x=True"
+  by simp
+
+lemma nlift_bool: "~x \<Longrightarrow> 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: "\<not> 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: "\<not> (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) \<le> number_of y) = (\<not> 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"
--- 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))
isabelle