author  haftmann 
Tue, 15 Jan 2008 16:19:23 +0100  
changeset 25919  8b1c0d434824 
parent 25230  022029099a83 
child 26075  815f3ccc0b45 
permissions  rwrr 
23465  1 
(* Title: HOL/Presburger.thy 
2 
ID: $Id$ 

3 
Author: Amine Chaieb, TU Muenchen 

4 
*) 

5 

23472  6 
header {* Decision Procedure for Presburger Arithmetic *} 
7 

23465  8 
theory Presburger 
9 
imports Arith_Tools SetInterval 

10 
uses 

11 
"Tools/Qelim/cooper_data.ML" 

12 
"Tools/Qelim/generated_cooper.ML" 

13 
("Tools/Qelim/cooper.ML") 

14 
("Tools/Qelim/presburger.ML") 

15 
begin 

16 

17 
setup CooperData.setup 

18 

19 
subsection{* The @{text "\<infinity>"} and @{text "+\<infinity>"} Properties *} 

20 

24404  21 

23465  22 
lemma minf: 
23 
"\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x<z. P x = P' x; \<exists>z.\<forall>x<z. Q x = Q' x\<rbrakk> 

24 
\<Longrightarrow> \<exists>z.\<forall>x<z. (P x \<and> Q x) = (P' x \<and> Q' x)" 

25 
"\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x<z. P x = P' x; \<exists>z.\<forall>x<z. Q x = Q' x\<rbrakk> 

26 
\<Longrightarrow> \<exists>z.\<forall>x<z. (P x \<or> Q x) = (P' x \<or> Q' x)" 

27 
"\<exists>(z ::'a::{linorder}).\<forall>x<z.(x = t) = False" 

28 
"\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<noteq> t) = True" 

29 
"\<exists>(z ::'a::{linorder}).\<forall>x<z.(x < t) = True" 

30 
"\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<le> t) = True" 

31 
"\<exists>(z ::'a::{linorder}).\<forall>x<z.(x > t) = False" 

32 
"\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<ge> t) = False" 

24993  33 
"\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.div})<z. (d dvd x + s) = (d dvd x + s)" 
34 
"\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.div})<z. (\<not> d dvd x + s) = (\<not> d dvd x + s)" 

23465  35 
"\<exists>z.\<forall>x<z. F = F" 
36 
by ((erule exE, erule exE,rule_tac x="min z za" in exI,simp)+, (rule_tac x="t" in exI,fastsimp)+) simp_all 

37 

38 
lemma pinf: 

39 
"\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x>z. P x = P' x; \<exists>z.\<forall>x>z. Q x = Q' x\<rbrakk> 

40 
\<Longrightarrow> \<exists>z.\<forall>x>z. (P x \<and> Q x) = (P' x \<and> Q' x)" 

41 
"\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x>z. P x = P' x; \<exists>z.\<forall>x>z. Q x = Q' x\<rbrakk> 

42 
\<Longrightarrow> \<exists>z.\<forall>x>z. (P x \<or> Q x) = (P' x \<or> Q' x)" 

43 
"\<exists>(z ::'a::{linorder}).\<forall>x>z.(x = t) = False" 

44 
"\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<noteq> t) = True" 

45 
"\<exists>(z ::'a::{linorder}).\<forall>x>z.(x < t) = False" 

46 
"\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<le> t) = False" 

47 
"\<exists>(z ::'a::{linorder}).\<forall>x>z.(x > t) = True" 

48 
"\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<ge> t) = True" 

24993  49 
"\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.div})>z. (d dvd x + s) = (d dvd x + s)" 
50 
"\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.div})>z. (\<not> d dvd x + s) = (\<not> d dvd x + s)" 

23465  51 
"\<exists>z.\<forall>x>z. F = F" 
52 
by ((erule exE, erule exE,rule_tac x="max z za" in exI,simp)+,(rule_tac x="t" in exI,fastsimp)+) simp_all 

53 

54 
lemma inf_period: 

55 
"\<lbrakk>\<forall>x k. P x = P (x  k*D); \<forall>x k. Q x = Q (x  k*D)\<rbrakk> 

56 
\<Longrightarrow> \<forall>x k. (P x \<and> Q x) = (P (x  k*D) \<and> Q (x  k*D))" 

57 
"\<lbrakk>\<forall>x k. P x = P (x  k*D); \<forall>x k. Q x = Q (x  k*D)\<rbrakk> 

58 
\<Longrightarrow> \<forall>x k. (P x \<or> Q x) = (P (x  k*D) \<or> Q (x  k*D))" 

24993  59 
"(d::'a::{comm_ring,Divides.div}) dvd D \<Longrightarrow> \<forall>x k. (d dvd x + t) = (d dvd (x  k*D) + t)" 
60 
"(d::'a::{comm_ring,Divides.div}) dvd D \<Longrightarrow> \<forall>x k. (\<not>d dvd x + t) = (\<not>d dvd (x  k*D) + t)" 

23465  61 
"\<forall>x k. F = F" 
62 
by simp_all 

63 
(clarsimp simp add: dvd_def, rule iffI, clarsimp,rule_tac x = "kb  ka*k" in exI, 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23472
diff
changeset

64 
simp add: ring_simps, clarsimp,rule_tac x = "kb + ka*k" in exI,simp add: ring_simps)+ 
23465  65 

23472  66 
subsection{* The A and B sets *} 
23465  67 
lemma bset: 
68 
"\<lbrakk>\<forall>x.(\<forall>j \<in> {1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> P x \<longrightarrow> P(x  D) ; 

69 
\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> Q x \<longrightarrow> Q(x  D)\<rbrakk> \<Longrightarrow> 

70 
\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j) \<longrightarrow> (P x \<and> Q x) \<longrightarrow> (P(x  D) \<and> Q (x  D))" 

71 
"\<lbrakk>\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> P x \<longrightarrow> P(x  D) ; 

72 
\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> Q x \<longrightarrow> Q(x  D)\<rbrakk> \<Longrightarrow> 

73 
\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (P x \<or> Q x) \<longrightarrow> (P(x  D) \<or> Q (x  D))" 

74 
"\<lbrakk>D>0; t  1\<in> B\<rbrakk> \<Longrightarrow> (\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x = t) \<longrightarrow> (x  D = t))" 

75 
"\<lbrakk>D>0 ; t \<in> B\<rbrakk> \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<noteq> t) \<longrightarrow> (x  D \<noteq> t))" 

76 
"D>0 \<Longrightarrow> (\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x < t) \<longrightarrow> (x  D < t))" 

77 
"D>0 \<Longrightarrow> (\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<le> t) \<longrightarrow> (x  D \<le> t))" 

78 
"\<lbrakk>D>0 ; t \<in> B\<rbrakk> \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x > t) \<longrightarrow> (x  D > t))" 

79 
"\<lbrakk>D>0 ; t  1 \<in> B\<rbrakk> \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<ge> t) \<longrightarrow> (x  D \<ge> t))" 

80 
"d dvd D \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (d dvd x+t) \<longrightarrow> (d dvd (x  D) + t))" 

81 
"d dvd D \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (\<not>d dvd x+t) \<longrightarrow> (\<not> d dvd (x  D) + t))" 

82 
"\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j) \<longrightarrow> F \<longrightarrow> F" 

83 
proof (blast, blast) 

84 
assume dp: "D > 0" and tB: "t  1\<in> B" 

85 
show "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x = t) \<longrightarrow> (x  D = t))" 

86 
apply (rule allI, rule impI,erule ballE[where x="1"],erule ballE[where x="t  1"]) 

87 
using dp tB by simp_all 

88 
next 

89 
assume dp: "D > 0" and tB: "t \<in> B" 

90 
show "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<noteq> t) \<longrightarrow> (x  D \<noteq> t))" 

91 
apply (rule allI, rule impI,erule ballE[where x="D"],erule ballE[where x="t"]) 

92 
using dp tB by simp_all 

93 
next 

94 
assume dp: "D > 0" thus "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x < t) \<longrightarrow> (x  D < t))" by arith 

95 
next 

96 
assume dp: "D > 0" thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<le> t) \<longrightarrow> (x  D \<le> t)" by arith 

97 
next 

98 
assume dp: "D > 0" and tB:"t \<in> B" 

99 
{fix x assume nob: "\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j" and g: "x > t" and ng: "\<not> (x  D) > t" 

100 
hence "x t \<le> D" and "1 \<le> x  t" by simp+ 

101 
hence "\<exists>j \<in> {1 .. D}. x  t = j" by auto 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23472
diff
changeset

102 
hence "\<exists>j \<in> {1 .. D}. x = t + j" by (simp add: ring_simps) 
23465  103 
with nob tB have "False" by simp} 
104 
thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x > t) \<longrightarrow> (x  D > t)" by blast 

105 
next 

106 
assume dp: "D > 0" and tB:"t  1\<in> B" 

107 
{fix x assume nob: "\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j" and g: "x \<ge> t" and ng: "\<not> (x  D) \<ge> t" 

108 
hence "x  (t  1) \<le> D" and "1 \<le> x  (t  1)" by simp+ 

109 
hence "\<exists>j \<in> {1 .. D}. x  (t  1) = j" by auto 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23472
diff
changeset

110 
hence "\<exists>j \<in> {1 .. D}. x = (t  1) + j" by (simp add: ring_simps) 
23465  111 
with nob tB have "False" by simp} 
112 
thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<ge> t) \<longrightarrow> (x  D \<ge> t)" by blast 

113 
next 

114 
assume d: "d dvd D" 

115 
{fix x assume H: "d dvd x + t" with d have "d dvd (x  D) + t" 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23472
diff
changeset

116 
by (clarsimp simp add: dvd_def,rule_tac x= "ka  k" in exI,simp add: ring_simps)} 
23465  117 
thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (d dvd x+t) \<longrightarrow> (d dvd (x  D) + t)" by simp 
118 
next 

119 
assume d: "d dvd D" 

120 
{fix x assume H: "\<not>(d dvd x + t)" with d have "\<not>d dvd (x  D) + t" 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23472
diff
changeset

121 
by (clarsimp simp add: dvd_def,erule_tac x= "ka + k" in allE,simp add: ring_simps)} 
23465  122 
thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (\<not>d dvd x+t) \<longrightarrow> (\<not>d dvd (x  D) + t)" by auto 
123 
qed blast 

124 

125 
lemma aset: 

126 
"\<lbrakk>\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b  j)\<longrightarrow> P x \<longrightarrow> P(x + D) ; 

127 
\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b  j)\<longrightarrow> Q x \<longrightarrow> Q(x + D)\<rbrakk> \<Longrightarrow> 

128 
\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b  j) \<longrightarrow> (P x \<and> Q x) \<longrightarrow> (P(x + D) \<and> Q (x + D))" 

129 
"\<lbrakk>\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b  j)\<longrightarrow> P x \<longrightarrow> P(x + D) ; 

130 
\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b  j)\<longrightarrow> Q x \<longrightarrow> Q(x + D)\<rbrakk> \<Longrightarrow> 

131 
\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b  j)\<longrightarrow> (P x \<or> Q x) \<longrightarrow> (P(x + D) \<or> Q (x + D))" 

132 
"\<lbrakk>D>0; t + 1\<in> A\<rbrakk> \<Longrightarrow> (\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b  j)\<longrightarrow> (x = t) \<longrightarrow> (x + D = t))" 

133 
"\<lbrakk>D>0 ; t \<in> A\<rbrakk> \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b  j)\<longrightarrow> (x \<noteq> t) \<longrightarrow> (x + D \<noteq> t))" 

134 
"\<lbrakk>D>0; t\<in> A\<rbrakk> \<Longrightarrow>(\<forall>(x::int). (\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b  j)\<longrightarrow> (x < t) \<longrightarrow> (x + D < t))" 

135 
"\<lbrakk>D>0; t + 1 \<in> A\<rbrakk> \<Longrightarrow> (\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b  j)\<longrightarrow> (x \<le> t) \<longrightarrow> (x + D \<le> t))" 

136 
"D>0 \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b  j)\<longrightarrow> (x > t) \<longrightarrow> (x + D > t))" 

137 
"D>0 \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b  j)\<longrightarrow> (x \<ge> t) \<longrightarrow> (x + D \<ge> t))" 

138 
"d dvd D \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b  j)\<longrightarrow> (d dvd x+t) \<longrightarrow> (d dvd (x + D) + t))" 

139 
"d dvd D \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b  j)\<longrightarrow> (\<not>d dvd x+t) \<longrightarrow> (\<not> d dvd (x + D) + t))" 

140 
"\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b  j) \<longrightarrow> F \<longrightarrow> F" 

141 
proof (blast, blast) 

142 
assume dp: "D > 0" and tA: "t + 1 \<in> A" 

143 
show "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b  j)\<longrightarrow> (x = t) \<longrightarrow> (x + D = t))" 

144 
apply (rule allI, rule impI,erule ballE[where x="1"],erule ballE[where x="t + 1"]) 

145 
using dp tA by simp_all 

146 
next 

147 
assume dp: "D > 0" and tA: "t \<in> A" 

148 
show "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b  j)\<longrightarrow> (x \<noteq> t) \<longrightarrow> (x + D \<noteq> t))" 

149 
apply (rule allI, rule impI,erule ballE[where x="D"],erule ballE[where x="t"]) 

150 
using dp tA by simp_all 

151 
next 

152 
assume dp: "D > 0" thus "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b  j)\<longrightarrow> (x > t) \<longrightarrow> (x + D > t))" by arith 

153 
next 

154 
assume dp: "D > 0" thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b  j)\<longrightarrow> (x \<ge> t) \<longrightarrow> (x + D \<ge> t)" by arith 

155 
next 

156 
assume dp: "D > 0" and tA:"t \<in> A" 

157 
{fix x assume nob: "\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b  j" and g: "x < t" and ng: "\<not> (x + D) < t" 

158 
hence "t  x \<le> D" and "1 \<le> t  x" by simp+ 

159 
hence "\<exists>j \<in> {1 .. D}. t  x = j" by auto 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23472
diff
changeset

160 
hence "\<exists>j \<in> {1 .. D}. x = t  j" by (auto simp add: ring_simps) 
23465  161 
with nob tA have "False" by simp} 
162 
thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b  j)\<longrightarrow> (x < t) \<longrightarrow> (x + D < t)" by blast 

163 
next 

164 
assume dp: "D > 0" and tA:"t + 1\<in> A" 

165 
{fix x assume nob: "\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b  j" and g: "x \<le> t" and ng: "\<not> (x + D) \<le> t" 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23472
diff
changeset

166 
hence "(t + 1)  x \<le> D" and "1 \<le> (t + 1)  x" by (simp_all add: ring_simps) 
23465  167 
hence "\<exists>j \<in> {1 .. D}. (t + 1)  x = j" by auto 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23472
diff
changeset

168 
hence "\<exists>j \<in> {1 .. D}. x = (t + 1)  j" by (auto simp add: ring_simps) 
23465  169 
with nob tA have "False" by simp} 
170 
thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b  j)\<longrightarrow> (x \<le> t) \<longrightarrow> (x + D \<le> t)" by blast 

171 
next 

172 
assume d: "d dvd D" 

173 
{fix x assume H: "d dvd x + t" with d have "d dvd (x + D) + t" 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23472
diff
changeset

174 
by (clarsimp simp add: dvd_def,rule_tac x= "ka + k" in exI,simp add: ring_simps)} 
23465  175 
thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b  j)\<longrightarrow> (d dvd x+t) \<longrightarrow> (d dvd (x + D) + t)" by simp 
176 
next 

177 
assume d: "d dvd D" 

178 
{fix x assume H: "\<not>(d dvd x + t)" with d have "\<not>d dvd (x + D) + t" 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23472
diff
changeset

179 
by (clarsimp simp add: dvd_def,erule_tac x= "ka  k" in allE,simp add: ring_simps)} 
23465  180 
thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b  j)\<longrightarrow> (\<not>d dvd x+t) \<longrightarrow> (\<not>d dvd (x + D) + t)" by auto 
181 
qed blast 

182 

183 
subsection{* Cooper's Theorem @{text "\<infinity>"} and @{text "+\<infinity>"} Version *} 

184 

185 
subsubsection{* First some trivial facts about periodic sets or predicates *} 

186 
lemma periodic_finite_ex: 

187 
assumes dpos: "(0::int) < d" and modd: "ALL x k. P x = P(x  k*d)" 

188 
shows "(EX x. P x) = (EX j : {1..d}. P j)" 

189 
(is "?LHS = ?RHS") 

190 
proof 

191 
assume ?LHS 

192 
then obtain x where P: "P x" .. 

193 
have "x mod d = x  (x div d)*d" by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq) 

194 
hence Pmod: "P x = P(x mod d)" using modd by simp 

195 
show ?RHS 

196 
proof (cases) 

197 
assume "x mod d = 0" 

198 
hence "P 0" using P Pmod by simp 

199 
moreover have "P 0 = P(0  (1)*d)" using modd by blast 

200 
ultimately have "P d" by simp 

201 
moreover have "d : {1..d}" using dpos by(simp add:atLeastAtMost_iff) 

202 
ultimately show ?RHS .. 

203 
next 

204 
assume not0: "x mod d \<noteq> 0" 

205 
have "P(x mod d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound) 

206 
moreover have "x mod d : {1..d}" 

207 
proof  

208 
from dpos have "0 \<le> x mod d" by(rule pos_mod_sign) 

209 
moreover from dpos have "x mod d < d" by(rule pos_mod_bound) 

210 
ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff) 

211 
qed 

212 
ultimately show ?RHS .. 

213 
qed 

214 
qed auto 

215 

216 
subsubsection{* The @{text "\<infinity>"} Version*} 

217 

218 
lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x  (abs(xz)+1) * d < z" 

219 
by(induct rule: int_gr_induct,simp_all add:int_distrib) 

220 

221 
lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(xz)+1) * d" 

222 
by(induct rule: int_gr_induct, simp_all add:int_distrib) 

223 

224 
theorem int_induct[case_names base step1 step2]: 

225 
assumes 

226 
base: "P(k::int)" and step1: "\<And>i. \<lbrakk>k \<le> i; P i\<rbrakk> \<Longrightarrow> P(i+1)" and 

227 
step2: "\<And>i. \<lbrakk>k \<ge> i; P i\<rbrakk> \<Longrightarrow> P(i  1)" 

228 
shows "P i" 

229 
proof  

230 
have "i \<le> k \<or> i\<ge> k" by arith 

231 
thus ?thesis using prems int_ge_induct[where P="P" and k="k" and i="i"] int_le_induct[where P="P" and k="k" and i="i"] by blast 

232 
qed 

233 

234 
lemma decr_mult_lemma: 

235 
assumes dpos: "(0::int) < d" and minus: "\<forall>x. P x \<longrightarrow> P(x  d)" and knneg: "0 <= k" 

236 
shows "ALL x. P x \<longrightarrow> P(x  k*d)" 

237 
using knneg 

238 
proof (induct rule:int_ge_induct) 

239 
case base thus ?case by simp 

240 
next 

241 
case (step i) 

242 
{fix x 

243 
have "P x \<longrightarrow> P (x  i * d)" using step.hyps by blast 

244 
also have "\<dots> \<longrightarrow> P(x  (i + 1) * d)" using minus[THEN spec, of "x  i * d"] 

245 
by (simp add:int_distrib OrderedGroup.diff_diff_eq[symmetric]) 

246 
ultimately have "P x \<longrightarrow> P(x  (i + 1) * d)" by blast} 

247 
thus ?case .. 

248 
qed 

249 

250 
lemma minusinfinity: 

251 
assumes dpos: "0 < d" and 

252 
P1eqP1: "ALL x k. P1 x = P1(x  k*d)" and ePeqP1: "EX z::int. ALL x. x < z \<longrightarrow> (P x = P1 x)" 

253 
shows "(EX x. P1 x) \<longrightarrow> (EX x. P x)" 

254 
proof 

255 
assume eP1: "EX x. P1 x" 

256 
then obtain x where P1: "P1 x" .. 

257 
from ePeqP1 obtain z where P1eqP: "ALL x. x < z \<longrightarrow> (P x = P1 x)" .. 

258 
let ?w = "x  (abs(xz)+1) * d" 

259 
from dpos have w: "?w < z" by(rule decr_lemma) 

260 
have "P1 x = P1 ?w" using P1eqP1 by blast 

261 
also have "\<dots> = P(?w)" using w P1eqP by blast 

262 
finally have "P ?w" using P1 by blast 

263 
thus "EX x. P x" .. 

264 
qed 

265 

266 
lemma cpmi: 

267 
assumes dp: "0 < D" and p1:"\<exists>z. \<forall> x< z. P x = P' x" 

268 
and nb:"\<forall>x.(\<forall> j\<in> {1..D}. \<forall>(b::int) \<in> B. x \<noteq> b+j) > P (x) > P (x  D)" 

269 
and pd: "\<forall> x k. P' x = P' (xk*D)" 

270 
shows "(\<exists>x. P x) = ((\<exists> j\<in> {1..D} . P' j)  (\<exists> j \<in> {1..D}.\<exists> b\<in> B. P (b+j)))" 

271 
(is "?L = (?R1 \<or> ?R2)") 

272 
proof 

273 
{assume "?R2" hence "?L" by blast} 

274 
moreover 

275 
{assume H:"?R1" hence "?L" using minusinfinity[OF dp pd p1] periodic_finite_ex[OF dp pd] by simp} 

276 
moreover 

277 
{ fix x 

278 
assume P: "P x" and H: "\<not> ?R2" 

279 
{fix y assume "\<not> (\<exists>j\<in>{1..D}. \<exists>b\<in>B. P (b + j))" and P: "P y" 

280 
hence "~(EX (j::int) : {1..D}. EX (b::int) : B. y = b+j)" by auto 

281 
with nb P have "P (y  D)" by auto } 

282 
hence "ALL x.~(EX (j::int) : {1..D}. EX (b::int) : B. P(b+j)) > P (x) > P (x  D)" by blast 

283 
with H P have th: " \<forall>x. P x \<longrightarrow> P (x  D)" by auto 

284 
from p1 obtain z where z: "ALL x. x < z > (P x = P' x)" by blast 

285 
let ?y = "x  (\<bar>x  z\<bar> + 1)*D" 

286 
have zp: "0 <= (\<bar>x  z\<bar> + 1)" by arith 

287 
from dp have yz: "?y < z" using decr_lemma[OF dp] by simp 

288 
from z[rule_format, OF yz] decr_mult_lemma[OF dp th zp, rule_format, OF P] have th2: " P' ?y" by auto 

289 
with periodic_finite_ex[OF dp pd] 

290 
have "?R1" by blast} 

291 
ultimately show ?thesis by blast 

292 
qed 

293 

294 
subsubsection {* The @{text "+\<infinity>"} Version*} 

295 

296 
lemma plusinfinity: 

297 
assumes dpos: "(0::int) < d" and 

298 
P1eqP1: "\<forall>x k. P' x = P'(x  k*d)" and ePeqP1: "\<exists> z. \<forall> x>z. P x = P' x" 

299 
shows "(\<exists> x. P' x) \<longrightarrow> (\<exists> x. P x)" 

300 
proof 

301 
assume eP1: "EX x. P' x" 

302 
then obtain x where P1: "P' x" .. 

303 
from ePeqP1 obtain z where P1eqP: "\<forall>x>z. P x = P' x" .. 

304 
let ?w' = "x + (abs(xz)+1) * d" 

305 
let ?w = "x  ((abs(xz) + 1))*d" 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23472
diff
changeset

306 
have ww'[simp]: "?w = ?w'" by (simp add: ring_simps) 
23465  307 
from dpos have w: "?w > z" by(simp only: ww' incr_lemma) 
308 
hence "P' x = P' ?w" using P1eqP1 by blast 

309 
also have "\<dots> = P(?w)" using w P1eqP by blast 

310 
finally have "P ?w" using P1 by blast 

311 
thus "EX x. P x" .. 

312 
qed 

313 

314 
lemma incr_mult_lemma: 

315 
assumes dpos: "(0::int) < d" and plus: "ALL x::int. P x \<longrightarrow> P(x + d)" and knneg: "0 <= k" 

316 
shows "ALL x. P x \<longrightarrow> P(x + k*d)" 

317 
using knneg 

318 
proof (induct rule:int_ge_induct) 

319 
case base thus ?case by simp 

320 
next 

321 
case (step i) 

322 
{fix x 

323 
have "P x \<longrightarrow> P (x + i * d)" using step.hyps by blast 

324 
also have "\<dots> \<longrightarrow> P(x + (i + 1) * d)" using plus[THEN spec, of "x + i * d"] 

325 
by (simp add:int_distrib zadd_ac) 

326 
ultimately have "P x \<longrightarrow> P(x + (i + 1) * d)" by blast} 

327 
thus ?case .. 

328 
qed 

329 

330 
lemma cppi: 

331 
assumes dp: "0 < D" and p1:"\<exists>z. \<forall> x> z. P x = P' x" 

332 
and nb:"\<forall>x.(\<forall> j\<in> {1..D}. \<forall>(b::int) \<in> A. x \<noteq> b  j) > P (x) > P (x + D)" 

333 
and pd: "\<forall> x k. P' x= P' (xk*D)" 

334 
shows "(\<exists>x. P x) = ((\<exists> j\<in> {1..D} . P' j)  (\<exists> j \<in> {1..D}.\<exists> b\<in> A. P (b  j)))" (is "?L = (?R1 \<or> ?R2)") 

335 
proof 

336 
{assume "?R2" hence "?L" by blast} 

337 
moreover 

338 
{assume H:"?R1" hence "?L" using plusinfinity[OF dp pd p1] periodic_finite_ex[OF dp pd] by simp} 

339 
moreover 

340 
{ fix x 

341 
assume P: "P x" and H: "\<not> ?R2" 

342 
{fix y assume "\<not> (\<exists>j\<in>{1..D}. \<exists>b\<in>A. P (b  j))" and P: "P y" 

343 
hence "~(EX (j::int) : {1..D}. EX (b::int) : A. y = b  j)" by auto 

344 
with nb P have "P (y + D)" by auto } 

345 
hence "ALL x.~(EX (j::int) : {1..D}. EX (b::int) : A. P(bj)) > P (x) > P (x + D)" by blast 

346 
with H P have th: " \<forall>x. P x \<longrightarrow> P (x + D)" by auto 

347 
from p1 obtain z where z: "ALL x. x > z > (P x = P' x)" by blast 

348 
let ?y = "x + (\<bar>x  z\<bar> + 1)*D" 

349 
have zp: "0 <= (\<bar>x  z\<bar> + 1)" by arith 

350 
from dp have yz: "?y > z" using incr_lemma[OF dp] by simp 

351 
from z[rule_format, OF yz] incr_mult_lemma[OF dp th zp, rule_format, OF P] have th2: " P' ?y" by auto 

352 
with periodic_finite_ex[OF dp pd] 

353 
have "?R1" by blast} 

354 
ultimately show ?thesis by blast 

355 
qed 

356 

357 
lemma simp_from_to: "{i..j::int} = (if j < i then {} else insert i {i+1..j})" 

358 
apply(simp add:atLeastAtMost_def atLeast_def atMost_def) 

359 
apply(fastsimp) 

360 
done 

361 

24993  362 
theorem unity_coeff_ex: "(\<exists>(x::'a::{semiring_0,Divides.div}). P (l * x)) \<equiv> (\<exists>x. l dvd (x + 0) \<and> P x)" 
23465  363 
apply (rule eq_reflection[symmetric]) 
364 
apply (rule iffI) 

365 
defer 

366 
apply (erule exE) 

367 
apply (rule_tac x = "l * x" in exI) 

368 
apply (simp add: dvd_def) 

369 
apply (rule_tac x="x" in exI, simp) 

370 
apply (erule exE) 

371 
apply (erule conjE) 

372 
apply (erule dvdE) 

373 
apply (rule_tac x = k in exI) 

374 
apply simp 

375 
done 

376 

377 
lemma zdvd_mono: assumes not0: "(k::int) \<noteq> 0" 

378 
shows "((m::int) dvd t) \<equiv> (k*m dvd k*t)" 

379 
using not0 by (simp add: dvd_def) 

380 

381 
lemma uminus_dvd_conv: "(d dvd (t::int)) \<equiv> (d dvd t)" "(d dvd (t::int)) \<equiv> (d dvd t)" 

382 
by simp_all 

383 
text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*} 

384 
lemma all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))" 

385 
by (simp split add: split_nat) 

386 

387 
lemma ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))" 

388 
apply (auto split add: split_nat) 

389 
apply (rule_tac x="int x" in exI, simp) 

390 
apply (rule_tac x = "nat x" in exI,erule_tac x = "nat x" in allE, simp) 

391 
done 

392 

393 
lemma zdiff_int_split: "P (int (x  y)) = 

394 
((y \<le> x \<longrightarrow> P (int x  int y)) \<and> (x < y \<longrightarrow> P 0))" 

395 
by (case_tac "y \<le> x", simp_all add: zdiff_int) 

396 

397 
lemma number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)" by simp 

398 
lemma number_of2: "(0::int) <= Numeral0" by simp 

399 
lemma Suc_plus1: "Suc n = n + 1" by simp 

400 

401 
text {* 

402 
\medskip Specific instances of congruence rules, to prevent 

403 
simplifier from looping. *} 

404 

405 
theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')" by simp 

406 

407 
theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> P')" 

408 
by (simp cong: conj_cong) 

409 
lemma int_eq_number_of_eq: 

410 
"(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)" 

411 
by simp 

412 

413 
lemma mod_eq0_dvd_iff[presburger]: "(m::nat) mod n = 0 \<longleftrightarrow> n dvd m" 

414 
unfolding dvd_eq_mod_eq_0[symmetric] .. 

415 

416 
lemma zmod_eq0_zdvd_iff[presburger]: "(m::int) mod n = 0 \<longleftrightarrow> n dvd m" 

417 
unfolding zdvd_iff_zmod_eq_0[symmetric] .. 

418 
declare mod_1[presburger] 

419 
declare mod_0[presburger] 

420 
declare zmod_1[presburger] 

421 
declare zmod_zero[presburger] 

422 
declare zmod_self[presburger] 

423 
declare mod_self[presburger] 

424 
declare DIVISION_BY_ZERO_MOD[presburger] 

425 
declare nat_mod_div_trivial[presburger] 

426 
declare div_mod_equality2[presburger] 

427 
declare div_mod_equality[presburger] 

428 
declare mod_div_equality2[presburger] 

429 
declare mod_div_equality[presburger] 

430 
declare mod_mult_self1[presburger] 

431 
declare mod_mult_self2[presburger] 

432 
declare zdiv_zmod_equality2[presburger] 

433 
declare zdiv_zmod_equality[presburger] 

434 
declare mod2_Suc_Suc[presburger] 

435 
lemma [presburger]: "(a::int) div 0 = 0" and [presburger]: "a mod 0 = a" 

436 
using IntDiv.DIVISION_BY_ZERO by blast+ 

437 

438 
use "Tools/Qelim/cooper.ML" 

439 
oracle linzqe_oracle ("term") = Coopereif.cooper_oracle 

440 

441 
use "Tools/Qelim/presburger.ML" 

442 

24075  443 
declaration {* fn _ => 
444 
arith_tactic_add 

24094  445 
(mk_arith_tactic "presburger" (fn ctxt => fn i => fn st => 
23465  446 
(warning "Trying Presburger arithmetic ..."; 
24094  447 
Presburger.cooper_tac true [] [] ctxt i st))) 
23465  448 
*} 
449 

450 
method_setup presburger = {* 

451 
let 

452 
fun keyword k = Scan.lift (Args.$$$ k  Args.colon) >> K () 

453 
fun simple_keyword k = Scan.lift (Args.$$$ k) >> K () 

454 
val addN = "add" 

455 
val delN = "del" 

456 
val elimN = "elim" 

457 
val any_keyword = keyword addN  keyword delN  simple_keyword elimN 

458 
val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; 

459 
in 

460 
fn src => Method.syntax 

461 
((Scan.optional (simple_keyword elimN >> K false) true)  

462 
(Scan.optional (keyword addN  thms) [])  

463 
(Scan.optional (keyword delN  thms) [])) src 

464 
#> (fn (((elim, add_ths), del_ths),ctxt) => 

465 
Method.SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt)) 

466 
end 

467 
*} "Cooper's algorithm for Presburger arithmetic" 

468 

469 
lemma [presburger]: "m mod 2 = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger 

470 
lemma [presburger]: "m mod 2 = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger 

471 
lemma [presburger]: "m mod (Suc (Suc 0)) = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger 

472 
lemma [presburger]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger 

473 
lemma [presburger]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger 

474 

475 

23685  476 
lemma zdvd_period: 
477 
fixes a d :: int 

478 
assumes advdd: "a dvd d" 

479 
shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)" 

480 
proof 

481 
{ 

482 
fix x k 

483 
from inf_period(3) [OF advdd, rule_format, where x=x and k="k"] 

484 
have "a dvd (x + t) \<longleftrightarrow> a dvd (x + k * d + t)" by simp 

485 
} 

486 
hence "\<forall>x.\<forall>k. ((a::int) dvd (x + t)) = (a dvd (x+k*d + t))" by simp 

487 
then show ?thesis by simp 

488 
qed 

489 

490 

23465  491 
subsection {* Code generator setup *} 
492 

493 
text {* 

494 
Presburger arithmetic is convenient to prove some 

495 
of the following code lemmas on integer numerals: 

496 
*} 

497 

498 
lemma eq_Pls_Pls: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

499 
"Int.Pls = Int.Pls \<longleftrightarrow> True" by presburger 
23465  500 

501 
lemma eq_Pls_Min: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

502 
"Int.Pls = Int.Min \<longleftrightarrow> False" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

503 
unfolding Pls_def Int.Min_def by presburger 
23465  504 

505 
lemma eq_Pls_Bit0: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

506 
"Int.Pls = Int.Bit k bit.B0 \<longleftrightarrow> Int.Pls = k" 
23465  507 
unfolding Pls_def Bit_def bit.cases by presburger 
508 

509 
lemma eq_Pls_Bit1: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

510 
"Int.Pls = Int.Bit k bit.B1 \<longleftrightarrow> False" 
23465  511 
unfolding Pls_def Bit_def bit.cases by presburger 
512 

513 
lemma eq_Min_Pls: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

514 
"Int.Min = Int.Pls \<longleftrightarrow> False" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

515 
unfolding Pls_def Int.Min_def by presburger 
23465  516 

517 
lemma eq_Min_Min: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

518 
"Int.Min = Int.Min \<longleftrightarrow> True" by presburger 
23465  519 

520 
lemma eq_Min_Bit0: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

521 
"Int.Min = Int.Bit k bit.B0 \<longleftrightarrow> False" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

522 
unfolding Int.Min_def Bit_def bit.cases by presburger 
23465  523 

524 
lemma eq_Min_Bit1: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

525 
"Int.Min = Int.Bit k bit.B1 \<longleftrightarrow> Int.Min = k" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

526 
unfolding Int.Min_def Bit_def bit.cases by presburger 
23465  527 

528 
lemma eq_Bit0_Pls: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

529 
"Int.Bit k bit.B0 = Int.Pls \<longleftrightarrow> Int.Pls = k" 
23465  530 
unfolding Pls_def Bit_def bit.cases by presburger 
531 

532 
lemma eq_Bit1_Pls: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

533 
"Int.Bit k bit.B1 = Int.Pls \<longleftrightarrow> False" 
23465  534 
unfolding Pls_def Bit_def bit.cases by presburger 
535 

536 
lemma eq_Bit0_Min: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

537 
"Int.Bit k bit.B0 = Int.Min \<longleftrightarrow> False" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

538 
unfolding Int.Min_def Bit_def bit.cases by presburger 
23465  539 

540 
lemma eq_Bit1_Min: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

541 
"(Int.Bit k bit.B1) = Int.Min \<longleftrightarrow> Int.Min = k" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

542 
unfolding Int.Min_def Bit_def bit.cases by presburger 
23465  543 

544 
lemma eq_Bit_Bit: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

545 
"Int.Bit k1 v1 = Int.Bit k2 v2 \<longleftrightarrow> 
23465  546 
v1 = v2 \<and> k1 = k2" 
547 
unfolding Bit_def 

548 
apply (cases v1) 

549 
apply (cases v2) 

550 
apply auto 

551 
apply presburger 

552 
apply (cases v2) 

553 
apply auto 

554 
apply presburger 

555 
apply (cases v2) 

556 
apply auto 

557 
done 

558 

559 
lemma eq_number_of: 

560 
"(number_of k \<Colon> int) = number_of l \<longleftrightarrow> k = l" 

561 
unfolding number_of_is_id .. 

562 

563 

564 
lemma less_eq_Pls_Pls: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

565 
"Int.Pls \<le> Int.Pls \<longleftrightarrow> True" by rule+ 
23465  566 

567 
lemma less_eq_Pls_Min: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

568 
"Int.Pls \<le> Int.Min \<longleftrightarrow> False" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

569 
unfolding Pls_def Int.Min_def by presburger 
23465  570 

571 
lemma less_eq_Pls_Bit: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

572 
"Int.Pls \<le> Int.Bit k v \<longleftrightarrow> Int.Pls \<le> k" 
23465  573 
unfolding Pls_def Bit_def by (cases v) auto 
574 

575 
lemma less_eq_Min_Pls: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

576 
"Int.Min \<le> Int.Pls \<longleftrightarrow> True" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

577 
unfolding Pls_def Int.Min_def by presburger 
23465  578 

579 
lemma less_eq_Min_Min: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

580 
"Int.Min \<le> Int.Min \<longleftrightarrow> True" by rule+ 
23465  581 

582 
lemma less_eq_Min_Bit0: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

583 
"Int.Min \<le> Int.Bit k bit.B0 \<longleftrightarrow> Int.Min < k" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

584 
unfolding Int.Min_def Bit_def by auto 
23465  585 

586 
lemma less_eq_Min_Bit1: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

587 
"Int.Min \<le> Int.Bit k bit.B1 \<longleftrightarrow> Int.Min \<le> k" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

588 
unfolding Int.Min_def Bit_def by auto 
23465  589 

590 
lemma less_eq_Bit0_Pls: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

591 
"Int.Bit k bit.B0 \<le> Int.Pls \<longleftrightarrow> k \<le> Int.Pls" 
23465  592 
unfolding Pls_def Bit_def by simp 
593 

594 
lemma less_eq_Bit1_Pls: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

595 
"Int.Bit k bit.B1 \<le> Int.Pls \<longleftrightarrow> k < Int.Pls" 
23465  596 
unfolding Pls_def Bit_def by auto 
597 

598 
lemma less_eq_Bit_Min: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

599 
"Int.Bit k v \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

600 
unfolding Int.Min_def Bit_def by (cases v) auto 
23465  601 

602 
lemma less_eq_Bit0_Bit: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

603 
"Int.Bit k1 bit.B0 \<le> Int.Bit k2 v \<longleftrightarrow> k1 \<le> k2" 
23465  604 
unfolding Bit_def bit.cases by (cases v) auto 
605 

606 
lemma less_eq_Bit_Bit1: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

607 
"Int.Bit k1 v \<le> Int.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2" 
23465  608 
unfolding Bit_def bit.cases by (cases v) auto 
609 

610 
lemma less_eq_Bit1_Bit0: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

611 
"Int.Bit k1 bit.B1 \<le> Int.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2" 
23465  612 
unfolding Bit_def by (auto split: bit.split) 
613 

614 
lemma less_eq_number_of: 

615 
"(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l" 

616 
unfolding number_of_is_id .. 

617 

618 

619 
lemma less_Pls_Pls: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

620 
"Int.Pls < Int.Pls \<longleftrightarrow> False" by simp 
23465  621 

622 
lemma less_Pls_Min: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

623 
"Int.Pls < Int.Min \<longleftrightarrow> False" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

624 
unfolding Pls_def Int.Min_def by presburger 
23465  625 

626 
lemma less_Pls_Bit0: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

627 
"Int.Pls < Int.Bit k bit.B0 \<longleftrightarrow> Int.Pls < k" 
23465  628 
unfolding Pls_def Bit_def by auto 
629 

630 
lemma less_Pls_Bit1: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

631 
"Int.Pls < Int.Bit k bit.B1 \<longleftrightarrow> Int.Pls \<le> k" 
23465  632 
unfolding Pls_def Bit_def by auto 
633 

634 
lemma less_Min_Pls: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

635 
"Int.Min < Int.Pls \<longleftrightarrow> True" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

636 
unfolding Pls_def Int.Min_def by presburger 
23465  637 

638 
lemma less_Min_Min: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

639 
"Int.Min < Int.Min \<longleftrightarrow> False" by simp 
23465  640 

641 
lemma less_Min_Bit: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

642 
"Int.Min < Int.Bit k v \<longleftrightarrow> Int.Min < k" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

643 
unfolding Int.Min_def Bit_def by (auto split: bit.split) 
23465  644 

645 
lemma less_Bit_Pls: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

646 
"Int.Bit k v < Int.Pls \<longleftrightarrow> k < Int.Pls" 
23465  647 
unfolding Pls_def Bit_def by (auto split: bit.split) 
648 

649 
lemma less_Bit0_Min: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

650 
"Int.Bit k bit.B0 < Int.Min \<longleftrightarrow> k \<le> Int.Min" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

651 
unfolding Int.Min_def Bit_def by auto 
23465  652 

653 
lemma less_Bit1_Min: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

654 
"Int.Bit k bit.B1 < Int.Min \<longleftrightarrow> k < Int.Min" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

655 
unfolding Int.Min_def Bit_def by auto 
23465  656 

657 
lemma less_Bit_Bit0: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

658 
"Int.Bit k1 v < Int.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2" 
23465  659 
unfolding Bit_def by (auto split: bit.split) 
660 

661 
lemma less_Bit1_Bit: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

662 
"Int.Bit k1 bit.B1 < Int.Bit k2 v \<longleftrightarrow> k1 < k2" 
23465  663 
unfolding Bit_def by (auto split: bit.split) 
664 

665 
lemma less_Bit0_Bit1: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25230
diff
changeset

666 
"Int.Bit k1 bit.B0 < Int.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2" 
23465  667 
unfolding Bit_def bit.cases by arith 
668 

669 
lemma less_number_of: 

670 
"(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l" 

671 
unfolding number_of_is_id .. 

672 

673 
lemmas pred_succ_numeral_code [code func] = 

674 
arith_simps(512) 

675 

676 
lemmas plus_numeral_code [code func] = 

677 
arith_simps(1317) 

678 
arith_simps(2627) 

679 
arith_extra_simps(1) [where 'a = int] 

680 

681 
lemmas minus_numeral_code [code func] = 

682 
arith_simps(1821) 

683 
arith_extra_simps(2) [where 'a = int] 

684 
arith_extra_simps(5) [where 'a = int] 

685 

686 
lemmas times_numeral_code [code func] = 

687 
arith_simps(2225) 

688 
arith_extra_simps(4) [where 'a = int] 

689 

690 
lemmas eq_numeral_code [code func] = 

691 
eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1 

692 
eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1 

693 
eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit 

694 
eq_number_of 

695 

696 
lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit 

697 
less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1 

698 
less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1 less_eq_Bit1_Bit0 

699 
less_eq_number_of 

700 

701 
lemmas less_numeral_code [code func] = less_Pls_Pls less_Pls_Min less_Pls_Bit0 

702 
less_Pls_Bit1 less_Min_Pls less_Min_Min less_Min_Bit less_Bit_Pls 

703 
less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1 

704 
less_number_of 

705 

25230  706 
context ring_1 
707 
begin 

23856  708 

709 
lemma of_int_num [code func]: 

710 
"of_int k = (if k = 0 then 0 else if k < 0 then 

711 
 of_int ( k) else let 

712 
(l, m) = divAlg (k, 2); 

713 
l' = of_int l 

714 
in if m = 0 then l' + l' else l' + l' + 1)" 

715 
proof  

716 
have aux1: "k mod (2\<Colon>int) \<noteq> (0\<Colon>int) \<Longrightarrow> 

717 
of_int k = of_int (k div 2 * 2 + 1)" 

718 
proof  

719 
assume "k mod 2 \<noteq> 0" 

720 
then have "k mod 2 = 1" by arith 

721 
moreover have "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp 

722 
ultimately show ?thesis by auto 

723 
qed 

724 
have aux2: "\<And>x. of_int 2 * x = x + x" 

725 
proof  

726 
fix x 

727 
have int2: "(2::int) = 1 + 1" by arith 

728 
show "of_int 2 * x = x + x" 

729 
unfolding int2 of_int_add left_distrib by simp 

730 
qed 

731 
have aux3: "\<And>x. x * of_int 2 = x + x" 

732 
proof  

733 
fix x 

734 
have int2: "(2::int) = 1 + 1" by arith 

735 
show "x * of_int 2 = x + x" 

736 
unfolding int2 of_int_add right_distrib by simp 

737 
qed 

738 
from aux1 show ?thesis by (auto simp add: divAlg_mod_div Let_def aux2 aux3) 

739 
qed 

740 

23465  741 
end 
25230  742 

743 
end 