author  nipkow 
Sat, 23 Jun 2007 19:33:22 +0200  
changeset 23477  f4b83f03cac9 
parent 23472  02099ea56555 
child 23685  1b0f4071946c 
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 

442 
setup {* 

443 
arith_tactic_add 

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 

476 
subsection {* Code generator setup *} 

477 

478 
text {* 

479 
Presburger arithmetic is convenient to prove some 

480 
of the following code lemmas on integer numerals: 

481 
*} 

482 

483 
lemma eq_Pls_Pls: 

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

485 

486 
lemma eq_Pls_Min: 

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

488 
unfolding Pls_def Numeral.Min_def by presburger 

489 

490 
lemma eq_Pls_Bit0: 

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

492 
unfolding Pls_def Bit_def bit.cases by presburger 

493 

494 
lemma eq_Pls_Bit1: 

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

496 
unfolding Pls_def Bit_def bit.cases by presburger 

497 

498 
lemma eq_Min_Pls: 

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

500 
unfolding Pls_def Numeral.Min_def by presburger 

501 

502 
lemma eq_Min_Min: 

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

504 

505 
lemma eq_Min_Bit0: 

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

507 
unfolding Numeral.Min_def Bit_def bit.cases by presburger 

508 

509 
lemma eq_Min_Bit1: 

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

511 
unfolding Numeral.Min_def Bit_def bit.cases by presburger 

512 

513 
lemma eq_Bit0_Pls: 

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

515 
unfolding Pls_def Bit_def bit.cases by presburger 

516 

517 
lemma eq_Bit1_Pls: 

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

519 
unfolding Pls_def Bit_def bit.cases by presburger 

520 

521 
lemma eq_Bit0_Min: 

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

523 
unfolding Numeral.Min_def Bit_def bit.cases by presburger 

524 

525 
lemma eq_Bit1_Min: 

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

527 
unfolding Numeral.Min_def Bit_def bit.cases by presburger 

528 

529 
lemma eq_Bit_Bit: 

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

531 
v1 = v2 \<and> k1 = k2" 

532 
unfolding Bit_def 

533 
apply (cases v1) 

534 
apply (cases v2) 

535 
apply auto 

536 
apply presburger 

537 
apply (cases v2) 

538 
apply auto 

539 
apply presburger 

540 
apply (cases v2) 

541 
apply auto 

542 
done 

543 

544 
lemma eq_number_of: 

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

546 
unfolding number_of_is_id .. 

547 

548 

549 
lemma less_eq_Pls_Pls: 

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

551 

552 
lemma less_eq_Pls_Min: 

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

554 
unfolding Pls_def Numeral.Min_def by presburger 

555 

556 
lemma less_eq_Pls_Bit: 

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

558 
unfolding Pls_def Bit_def by (cases v) auto 

559 

560 
lemma less_eq_Min_Pls: 

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

562 
unfolding Pls_def Numeral.Min_def by presburger 

563 

564 
lemma less_eq_Min_Min: 

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

566 

567 
lemma less_eq_Min_Bit0: 

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

569 
unfolding Numeral.Min_def Bit_def by auto 

570 

571 
lemma less_eq_Min_Bit1: 

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

573 
unfolding Numeral.Min_def Bit_def by auto 

574 

575 
lemma less_eq_Bit0_Pls: 

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

577 
unfolding Pls_def Bit_def by simp 

578 

579 
lemma less_eq_Bit1_Pls: 

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

581 
unfolding Pls_def Bit_def by auto 

582 

583 
lemma less_eq_Bit_Min: 

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

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

586 

587 
lemma less_eq_Bit0_Bit: 

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

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

590 

591 
lemma less_eq_Bit_Bit1: 

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

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

594 

595 
lemma less_eq_Bit1_Bit0: 

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

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

598 

599 
lemma less_eq_number_of: 

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

601 
unfolding number_of_is_id .. 

602 

603 

604 
lemma less_Pls_Pls: 

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

606 

607 
lemma less_Pls_Min: 

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

609 
unfolding Pls_def Numeral.Min_def by presburger 

610 

611 
lemma less_Pls_Bit0: 

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

613 
unfolding Pls_def Bit_def by auto 

614 

615 
lemma less_Pls_Bit1: 

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

617 
unfolding Pls_def Bit_def by auto 

618 

619 
lemma less_Min_Pls: 

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

621 
unfolding Pls_def Numeral.Min_def by presburger 

622 

623 
lemma less_Min_Min: 

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

625 

626 
lemma less_Min_Bit: 

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

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

629 

630 
lemma less_Bit_Pls: 

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

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

633 

634 
lemma less_Bit0_Min: 

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

636 
unfolding Numeral.Min_def Bit_def by auto 

637 

638 
lemma less_Bit1_Min: 

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

640 
unfolding Numeral.Min_def Bit_def by auto 

641 

642 
lemma less_Bit_Bit0: 

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

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

645 

646 
lemma less_Bit1_Bit: 

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

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

649 

650 
lemma less_Bit0_Bit1: 

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

652 
unfolding Bit_def bit.cases by arith 

653 

654 
lemma less_number_of: 

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

656 
unfolding number_of_is_id .. 

657 

658 
lemmas pred_succ_numeral_code [code func] = 

659 
arith_simps(512) 

660 

661 
lemmas plus_numeral_code [code func] = 

662 
arith_simps(1317) 

663 
arith_simps(2627) 

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

665 

666 
lemmas minus_numeral_code [code func] = 

667 
arith_simps(1821) 

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

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

670 

671 
lemmas times_numeral_code [code func] = 

672 
arith_simps(2225) 

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

674 

675 
lemmas eq_numeral_code [code func] = 

676 
eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1 

677 
eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1 

678 
eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit 

679 
eq_number_of 

680 

681 
lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit 

682 
less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1 

683 
less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1 less_eq_Bit1_Bit0 

684 
less_eq_number_of 

685 

686 
lemmas less_numeral_code [code func] = less_Pls_Pls less_Pls_Min less_Pls_Bit0 

687 
less_Pls_Bit1 less_Min_Pls less_Min_Min less_Min_Bit less_Bit_Pls 

688 
less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1 

689 
less_number_of 

690 

691 
end 