author  wenzelm 
Tue, 31 Jul 2007 00:56:26 +0200  
changeset 24075  366d4d234814 
parent 23856  ebec38420a85 
child 24094  6db35c14146d 
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 

21 
lemma minf: 

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

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

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

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

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

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

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

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

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

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

32 
"\<exists>z.\<forall>(x::'a::{linorder,plus,times})<z. (d dvd x + s) = (d dvd x + s)" 

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

34 
"\<exists>z.\<forall>x<z. F = F" 

35 
by ((erule exE, erule exE,rule_tac x="min z za" in exI,simp)+, (rule_tac x="t" in exI,fastsimp)+) simp_all 

36 

37 
lemma pinf: 

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

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

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

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

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

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

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

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

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

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

48 
"\<exists>z.\<forall>(x::'a::{linorder,plus,times})>z. (d dvd x + s) = (d dvd x + s)" 

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

50 
"\<exists>z.\<forall>x>z. F = F" 

51 
by ((erule exE, erule exE,rule_tac x="max z za" in exI,simp)+,(rule_tac x="t" in exI,fastsimp)+) simp_all 

52 

53 
lemma inf_period: 

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

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

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

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

58 
"(d::'a::{comm_ring}) dvd D \<Longrightarrow> \<forall>x k. (d dvd x + t) = (d dvd (x  k*D) + t)" 

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

60 
"\<forall>x k. F = F" 

61 
by simp_all 

62 
(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

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

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

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

69 
\<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))" 

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

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

72 
\<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))" 

73 
"\<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))" 

74 
"\<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))" 

75 
"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))" 

76 
"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))" 

77 
"\<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))" 

78 
"\<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))" 

79 
"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))" 

80 
"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))" 

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

82 
proof (blast, blast) 

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

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

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

86 
using dp tB by simp_all 

87 
next 

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

89 
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))" 

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

91 
using dp tB by simp_all 

92 
next 

93 
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 

94 
next 

95 
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 

96 
next 

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

98 
{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" 

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

100 
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

101 
hence "\<exists>j \<in> {1 .. D}. x = t + j" by (simp add: ring_simps) 
23465  102 
with nob tB have "False" by simp} 
103 
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 

104 
next 

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

106 
{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" 

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

108 
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

109 
hence "\<exists>j \<in> {1 .. D}. x = (t  1) + j" by (simp add: ring_simps) 
23465  110 
with nob tB have "False" by simp} 
111 
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 

112 
next 

113 
assume d: "d dvd D" 

114 
{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

115 
by (clarsimp simp add: dvd_def,rule_tac x= "ka  k" in exI,simp add: ring_simps)} 
23465  116 
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 
117 
next 

118 
assume d: "d dvd D" 

119 
{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

120 
by (clarsimp simp add: dvd_def,erule_tac x= "ka + k" in allE,simp add: ring_simps)} 
23465  121 
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 
122 
qed blast 

123 

124 
lemma aset: 

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

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

127 
\<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))" 

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

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

130 
\<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))" 

131 
"\<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))" 

132 
"\<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))" 

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 < t) \<longrightarrow> (x + D < t))" 

134 
"\<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))" 

135 
"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))" 

136 
"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))" 

137 
"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))" 

138 
"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))" 

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

140 
proof (blast, blast) 

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

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

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

144 
using dp tA by simp_all 

145 
next 

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

147 
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))" 

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

149 
using dp tA by simp_all 

150 
next 

151 
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 

152 
next 

153 
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 

154 
next 

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

156 
{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" 

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

158 
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

159 
hence "\<exists>j \<in> {1 .. D}. x = t  j" by (auto simp add: ring_simps) 
23465  160 
with nob tA have "False" by simp} 
161 
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 

162 
next 

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

164 
{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

165 
hence "(t + 1)  x \<le> D" and "1 \<le> (t + 1)  x" by (simp_all add: ring_simps) 
23465  166 
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

167 
hence "\<exists>j \<in> {1 .. D}. x = (t + 1)  j" by (auto simp add: ring_simps) 
23465  168 
with nob tA have "False" by simp} 
169 
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 

170 
next 

171 
assume d: "d dvd D" 

172 
{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

173 
by (clarsimp simp add: dvd_def,rule_tac x= "ka + k" in exI,simp add: ring_simps)} 
23465  174 
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 
175 
next 

176 
assume d: "d dvd D" 

177 
{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

178 
by (clarsimp simp add: dvd_def,erule_tac x= "ka  k" in allE,simp add: ring_simps)} 
23465  179 
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 
180 
qed blast 

181 

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

183 

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

185 
lemma periodic_finite_ex: 

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

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

188 
(is "?LHS = ?RHS") 

189 
proof 

190 
assume ?LHS 

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

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

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

194 
show ?RHS 

195 
proof (cases) 

196 
assume "x mod d = 0" 

197 
hence "P 0" using P Pmod by simp 

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

199 
ultimately have "P d" by simp 

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

201 
ultimately show ?RHS .. 

202 
next 

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

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

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

206 
proof  

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

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

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

210 
qed 

211 
ultimately show ?RHS .. 

212 
qed 

213 
qed auto 

214 

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

216 

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

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

219 

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

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

222 

223 
theorem int_induct[case_names base step1 step2]: 

224 
assumes 

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

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

227 
shows "P i" 

228 
proof  

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

230 
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 

231 
qed 

232 

233 
lemma decr_mult_lemma: 

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

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

236 
using knneg 

237 
proof (induct rule:int_ge_induct) 

238 
case base thus ?case by simp 

239 
next 

240 
case (step i) 

241 
{fix x 

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

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

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

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

246 
thus ?case .. 

247 
qed 

248 

249 
lemma minusinfinity: 

250 
assumes dpos: "0 < d" and 

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

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

253 
proof 

254 
assume eP1: "EX x. P1 x" 

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

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

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

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

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

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

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

262 
thus "EX x. P x" .. 

263 
qed 

264 

265 
lemma cpmi: 

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

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

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

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

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

271 
proof 

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

273 
moreover 

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

275 
moreover 

276 
{ fix x 

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

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

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

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

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

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

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

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

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

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

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

288 
with periodic_finite_ex[OF dp pd] 

289 
have "?R1" by blast} 

290 
ultimately show ?thesis by blast 

291 
qed 

292 

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

294 

295 
lemma plusinfinity: 

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

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

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

299 
proof 

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

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

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

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

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

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

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

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

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

310 
thus "EX x. P x" .. 

311 
qed 

312 

313 
lemma incr_mult_lemma: 

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

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

316 
using knneg 

317 
proof (induct rule:int_ge_induct) 

318 
case base thus ?case by simp 

319 
next 

320 
case (step i) 

321 
{fix x 

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

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

324 
by (simp add:int_distrib zadd_ac) 

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

326 
thus ?case .. 

327 
qed 

328 

329 
lemma cppi: 

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

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

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

333 
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)") 

334 
proof 

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

336 
moreover 

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

338 
moreover 

339 
{ fix x 

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

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

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

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

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

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

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

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

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

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

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

351 
with periodic_finite_ex[OF dp pd] 

352 
have "?R1" by blast} 

353 
ultimately show ?thesis by blast 

354 
qed 

355 

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

357 
apply(simp add:atLeastAtMost_def atLeast_def atMost_def) 

358 
apply(fastsimp) 

359 
done 

360 

361 
theorem unity_coeff_ex: "(\<exists>(x::'a::{semiring_0}). P (l * x)) \<equiv> (\<exists>x. l dvd (x + 0) \<and> P x)" 

362 
apply (rule eq_reflection[symmetric]) 

363 
apply (rule iffI) 

364 
defer 

365 
apply (erule exE) 

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

367 
apply (simp add: dvd_def) 

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

369 
apply (erule exE) 

370 
apply (erule conjE) 

371 
apply (erule dvdE) 

372 
apply (rule_tac x = k in exI) 

373 
apply simp 

374 
done 

375 

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

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

378 
using not0 by (simp add: dvd_def) 

379 

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

381 
by simp_all 

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

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

384 
by (simp split add: split_nat) 

385 

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

387 
apply (auto split add: split_nat) 

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

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

390 
done 

391 

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

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

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

395 

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

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

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

399 

400 
text {* 

401 
\medskip Specific instances of congruence rules, to prevent 

402 
simplifier from looping. *} 

403 

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

405 

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

407 
by (simp cong: conj_cong) 

408 
lemma int_eq_number_of_eq: 

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

410 
by simp 

411 

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

413 
unfolding dvd_eq_mod_eq_0[symmetric] .. 

414 

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

416 
unfolding zdvd_iff_zmod_eq_0[symmetric] .. 

417 
declare mod_1[presburger] 

418 
declare mod_0[presburger] 

419 
declare zmod_1[presburger] 

420 
declare zmod_zero[presburger] 

421 
declare zmod_self[presburger] 

422 
declare mod_self[presburger] 

423 
declare DIVISION_BY_ZERO_MOD[presburger] 

424 
declare nat_mod_div_trivial[presburger] 

425 
declare div_mod_equality2[presburger] 

426 
declare div_mod_equality[presburger] 

427 
declare mod_div_equality2[presburger] 

428 
declare mod_div_equality[presburger] 

429 
declare mod_mult_self1[presburger] 

430 
declare mod_mult_self2[presburger] 

431 
declare zdiv_zmod_equality2[presburger] 

432 
declare zdiv_zmod_equality[presburger] 

433 
declare mod2_Suc_Suc[presburger] 

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

435 
using IntDiv.DIVISION_BY_ZERO by blast+ 

436 

437 
use "Tools/Qelim/cooper.ML" 

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

439 

440 
use "Tools/Qelim/presburger.ML" 

441 

24075  442 
declaration {* fn _ => 
443 
arith_tactic_add 

23465  444 
(mk_arith_tactic "presburger" (fn i => fn st => 
445 
(warning "Trying Presburger arithmetic ..."; 

446 
Presburger.cooper_tac true [] [] ((ProofContext.init o theory_of_thm) st) i st))) 

447 
(* FIXME!!!!!!! get the right context!!*) 

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: 

499 
"Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by presburger 

500 

501 
lemma eq_Pls_Min: 

502 
"Numeral.Pls = Numeral.Min \<longleftrightarrow> False" 

503 
unfolding Pls_def Numeral.Min_def by presburger 

504 

505 
lemma eq_Pls_Bit0: 

506 
"Numeral.Pls = Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls = k" 

507 
unfolding Pls_def Bit_def bit.cases by presburger 

508 

509 
lemma eq_Pls_Bit1: 

510 
"Numeral.Pls = Numeral.Bit k bit.B1 \<longleftrightarrow> False" 

511 
unfolding Pls_def Bit_def bit.cases by presburger 

512 

513 
lemma eq_Min_Pls: 

514 
"Numeral.Min = Numeral.Pls \<longleftrightarrow> False" 

515 
unfolding Pls_def Numeral.Min_def by presburger 

516 

517 
lemma eq_Min_Min: 

518 
"Numeral.Min = Numeral.Min \<longleftrightarrow> True" by presburger 

519 

520 
lemma eq_Min_Bit0: 

521 
"Numeral.Min = Numeral.Bit k bit.B0 \<longleftrightarrow> False" 

522 
unfolding Numeral.Min_def Bit_def bit.cases by presburger 

523 

524 
lemma eq_Min_Bit1: 

525 
"Numeral.Min = Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min = k" 

526 
unfolding Numeral.Min_def Bit_def bit.cases by presburger 

527 

528 
lemma eq_Bit0_Pls: 

529 
"Numeral.Bit k bit.B0 = Numeral.Pls \<longleftrightarrow> Numeral.Pls = k" 

530 
unfolding Pls_def Bit_def bit.cases by presburger 

531 

532 
lemma eq_Bit1_Pls: 

533 
"Numeral.Bit k bit.B1 = Numeral.Pls \<longleftrightarrow> False" 

534 
unfolding Pls_def Bit_def bit.cases by presburger 

535 

536 
lemma eq_Bit0_Min: 

537 
"Numeral.Bit k bit.B0 = Numeral.Min \<longleftrightarrow> False" 

538 
unfolding Numeral.Min_def Bit_def bit.cases by presburger 

539 

540 
lemma eq_Bit1_Min: 

541 
"(Numeral.Bit k bit.B1) = Numeral.Min \<longleftrightarrow> Numeral.Min = k" 

542 
unfolding Numeral.Min_def Bit_def bit.cases by presburger 

543 

544 
lemma eq_Bit_Bit: 

545 
"Numeral.Bit k1 v1 = Numeral.Bit k2 v2 \<longleftrightarrow> 

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: 

565 
"Numeral.Pls \<le> Numeral.Pls \<longleftrightarrow> True" by rule+ 

566 

567 
lemma less_eq_Pls_Min: 

568 
"Numeral.Pls \<le> Numeral.Min \<longleftrightarrow> False" 

569 
unfolding Pls_def Numeral.Min_def by presburger 

570 

571 
lemma less_eq_Pls_Bit: 

572 
"Numeral.Pls \<le> Numeral.Bit k v \<longleftrightarrow> Numeral.Pls \<le> k" 

573 
unfolding Pls_def Bit_def by (cases v) auto 

574 

575 
lemma less_eq_Min_Pls: 

576 
"Numeral.Min \<le> Numeral.Pls \<longleftrightarrow> True" 

577 
unfolding Pls_def Numeral.Min_def by presburger 

578 

579 
lemma less_eq_Min_Min: 

580 
"Numeral.Min \<le> Numeral.Min \<longleftrightarrow> True" by rule+ 

581 

582 
lemma less_eq_Min_Bit0: 

583 
"Numeral.Min \<le> Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Min < k" 

584 
unfolding Numeral.Min_def Bit_def by auto 

585 

586 
lemma less_eq_Min_Bit1: 

587 
"Numeral.Min \<le> Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min \<le> k" 

588 
unfolding Numeral.Min_def Bit_def by auto 

589 

590 
lemma less_eq_Bit0_Pls: 

591 
"Numeral.Bit k bit.B0 \<le> Numeral.Pls \<longleftrightarrow> k \<le> Numeral.Pls" 

592 
unfolding Pls_def Bit_def by simp 

593 

594 
lemma less_eq_Bit1_Pls: 

595 
"Numeral.Bit k bit.B1 \<le> Numeral.Pls \<longleftrightarrow> k < Numeral.Pls" 

596 
unfolding Pls_def Bit_def by auto 

597 

598 
lemma less_eq_Bit_Min: 

599 
"Numeral.Bit k v \<le> Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min" 

600 
unfolding Numeral.Min_def Bit_def by (cases v) auto 

601 

602 
lemma less_eq_Bit0_Bit: 

603 
"Numeral.Bit k1 bit.B0 \<le> Numeral.Bit k2 v \<longleftrightarrow> k1 \<le> k2" 

604 
unfolding Bit_def bit.cases by (cases v) auto 

605 

606 
lemma less_eq_Bit_Bit1: 

607 
"Numeral.Bit k1 v \<le> Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2" 

608 
unfolding Bit_def bit.cases by (cases v) auto 

609 

610 
lemma less_eq_Bit1_Bit0: 

611 
"Numeral.Bit k1 bit.B1 \<le> Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2" 

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: 

620 
"Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by simp 

621 

622 
lemma less_Pls_Min: 

623 
"Numeral.Pls < Numeral.Min \<longleftrightarrow> False" 

624 
unfolding Pls_def Numeral.Min_def by presburger 

625 

626 
lemma less_Pls_Bit0: 

627 
"Numeral.Pls < Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls < k" 

628 
unfolding Pls_def Bit_def by auto 

629 

630 
lemma less_Pls_Bit1: 

631 
"Numeral.Pls < Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Pls \<le> k" 

632 
unfolding Pls_def Bit_def by auto 

633 

634 
lemma less_Min_Pls: 

635 
"Numeral.Min < Numeral.Pls \<longleftrightarrow> True" 

636 
unfolding Pls_def Numeral.Min_def by presburger 

637 

638 
lemma less_Min_Min: 

639 
"Numeral.Min < Numeral.Min \<longleftrightarrow> False" by simp 

640 

641 
lemma less_Min_Bit: 

642 
"Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k" 

643 
unfolding Numeral.Min_def Bit_def by (auto split: bit.split) 

644 

645 
lemma less_Bit_Pls: 

646 
"Numeral.Bit k v < Numeral.Pls \<longleftrightarrow> k < Numeral.Pls" 

647 
unfolding Pls_def Bit_def by (auto split: bit.split) 

648 

649 
lemma less_Bit0_Min: 

650 
"Numeral.Bit k bit.B0 < Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min" 

651 
unfolding Numeral.Min_def Bit_def by auto 

652 

653 
lemma less_Bit1_Min: 

654 
"Numeral.Bit k bit.B1 < Numeral.Min \<longleftrightarrow> k < Numeral.Min" 

655 
unfolding Numeral.Min_def Bit_def by auto 

656 

657 
lemma less_Bit_Bit0: 

658 
"Numeral.Bit k1 v < Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2" 

659 
unfolding Bit_def by (auto split: bit.split) 

660 

661 
lemma less_Bit1_Bit: 

662 
"Numeral.Bit k1 bit.B1 < Numeral.Bit k2 v \<longleftrightarrow> k1 < k2" 

663 
unfolding Bit_def by (auto split: bit.split) 

664 

665 
lemma less_Bit0_Bit1: 

666 
"Numeral.Bit k1 bit.B0 < Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2" 

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 

23856  706 

707 
lemma of_int_num [code func]: 

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

709 
 of_int ( k) else let 

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

711 
l' = of_int l 

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

713 
proof  

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

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

716 
proof  

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

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

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

720 
ultimately show ?thesis by auto 

721 
qed 

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

723 
proof  

724 
fix x 

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

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

727 
unfolding int2 of_int_add left_distrib by simp 

728 
qed 

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

730 
proof  

731 
fix x 

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

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

734 
unfolding int2 of_int_add right_distrib by simp 

735 
qed 

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

737 
qed 

738 

23465  739 
end 