src/HOL/Presburger.thy
changeset 26086 3c243098b64a
parent 26075 815f3ccc0b45
child 26156 420c1947511c
     1.1 --- a/src/HOL/Presburger.thy	Sat Feb 16 16:52:09 2008 +0100
     1.2 +++ b/src/HOL/Presburger.thy	Sun Feb 17 06:49:53 2008 +0100
     1.3 @@ -394,7 +394,8 @@
     1.4    ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
     1.5    by (case_tac "y \<le> x", simp_all add: zdiff_int)
     1.6  
     1.7 -lemma number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)" by simp
     1.8 +lemma number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (Int.Bit0 n) \<and> (0::int) <= number_of (Int.Bit1 n)"
     1.9 +by simp
    1.10  lemma number_of2: "(0::int) <= Numeral0" by simp
    1.11  lemma Suc_plus1: "Suc n = n + 1" by simp
    1.12  
    1.13 @@ -503,12 +504,12 @@
    1.14    unfolding Pls_def Int.Min_def by presburger
    1.15  
    1.16  lemma eq_Pls_Bit0:
    1.17 -  "Int.Pls = Int.Bit k bit.B0 \<longleftrightarrow> Int.Pls = k"
    1.18 -  unfolding Pls_def Bit_def bit.cases by presburger
    1.19 +  "Int.Pls = Int.Bit0 k \<longleftrightarrow> Int.Pls = k"
    1.20 +  unfolding Pls_def Bit0_def by presburger
    1.21  
    1.22  lemma eq_Pls_Bit1:
    1.23 -  "Int.Pls = Int.Bit k bit.B1 \<longleftrightarrow> False"
    1.24 -  unfolding Pls_def Bit_def bit.cases by presburger
    1.25 +  "Int.Pls = Int.Bit1 k \<longleftrightarrow> False"
    1.26 +  unfolding Pls_def Bit1_def by presburger
    1.27  
    1.28  lemma eq_Min_Pls:
    1.29    "Int.Min = Int.Pls \<longleftrightarrow> False"
    1.30 @@ -518,43 +519,44 @@
    1.31    "Int.Min = Int.Min \<longleftrightarrow> True" by presburger
    1.32  
    1.33  lemma eq_Min_Bit0:
    1.34 -  "Int.Min = Int.Bit k bit.B0 \<longleftrightarrow> False"
    1.35 -  unfolding Int.Min_def Bit_def bit.cases by presburger
    1.36 +  "Int.Min = Int.Bit0 k \<longleftrightarrow> False"
    1.37 +  unfolding Int.Min_def Bit0_def by presburger
    1.38  
    1.39  lemma eq_Min_Bit1:
    1.40 -  "Int.Min = Int.Bit k bit.B1 \<longleftrightarrow> Int.Min = k"
    1.41 -  unfolding Int.Min_def Bit_def bit.cases by presburger
    1.42 +  "Int.Min = Int.Bit1 k \<longleftrightarrow> Int.Min = k"
    1.43 +  unfolding Int.Min_def Bit1_def by presburger
    1.44  
    1.45  lemma eq_Bit0_Pls:
    1.46 -  "Int.Bit k bit.B0 = Int.Pls \<longleftrightarrow> Int.Pls = k"
    1.47 -  unfolding Pls_def Bit_def bit.cases by presburger
    1.48 +  "Int.Bit0 k = Int.Pls \<longleftrightarrow> Int.Pls = k"
    1.49 +  unfolding Pls_def Bit0_def by presburger
    1.50  
    1.51  lemma eq_Bit1_Pls:
    1.52 -  "Int.Bit k bit.B1 = Int.Pls \<longleftrightarrow> False"
    1.53 -  unfolding Pls_def Bit_def bit.cases  by presburger
    1.54 +  "Int.Bit1 k = Int.Pls \<longleftrightarrow> False"
    1.55 +  unfolding Pls_def Bit1_def by presburger
    1.56  
    1.57  lemma eq_Bit0_Min:
    1.58 -  "Int.Bit k bit.B0 = Int.Min \<longleftrightarrow> False"
    1.59 -  unfolding Int.Min_def Bit_def bit.cases  by presburger
    1.60 +  "Int.Bit0 k = Int.Min \<longleftrightarrow> False"
    1.61 +  unfolding Int.Min_def Bit0_def by presburger
    1.62  
    1.63  lemma eq_Bit1_Min:
    1.64 -  "(Int.Bit k bit.B1) = Int.Min \<longleftrightarrow> Int.Min = k"
    1.65 -  unfolding Int.Min_def Bit_def bit.cases  by presburger
    1.66 +  "Int.Bit1 k = Int.Min \<longleftrightarrow> Int.Min = k"
    1.67 +  unfolding Int.Min_def Bit1_def by presburger
    1.68 +
    1.69 +lemma eq_Bit0_Bit0:
    1.70 +  "Int.Bit0 k1 = Int.Bit0 k2 \<longleftrightarrow> k1 = k2"
    1.71 +  unfolding Bit0_def by presburger
    1.72  
    1.73 -lemma eq_Bit_Bit:
    1.74 -  "Int.Bit k1 v1 = Int.Bit k2 v2 \<longleftrightarrow>
    1.75 -    v1 = v2 \<and> k1 = k2" 
    1.76 -  unfolding Bit_def
    1.77 -  apply (cases v1)
    1.78 -  apply (cases v2)
    1.79 -  apply auto
    1.80 -  apply presburger
    1.81 -  apply (cases v2)
    1.82 -  apply auto
    1.83 -  apply presburger
    1.84 -  apply (cases v2)
    1.85 -  apply auto
    1.86 -  done
    1.87 +lemma eq_Bit0_Bit1:
    1.88 +  "Int.Bit0 k1 = Int.Bit1 k2 \<longleftrightarrow> False"
    1.89 +  unfolding Bit0_def Bit1_def by presburger
    1.90 +
    1.91 +lemma eq_Bit1_Bit0:
    1.92 +  "Int.Bit1 k1 = Int.Bit0 k2 \<longleftrightarrow> False"
    1.93 +  unfolding Bit0_def Bit1_def by presburger
    1.94 +
    1.95 +lemma eq_Bit1_Bit1:
    1.96 +  "Int.Bit1 k1 = Int.Bit1 k2 \<longleftrightarrow> k1 = k2"
    1.97 +  unfolding Bit1_def by presburger
    1.98  
    1.99  lemma eq_number_of:
   1.100    "(number_of k \<Colon> int) = number_of l \<longleftrightarrow> k = l" 
   1.101 @@ -568,9 +570,13 @@
   1.102    "Int.Pls \<le> Int.Min \<longleftrightarrow> False"
   1.103    unfolding Pls_def Int.Min_def by presburger
   1.104  
   1.105 -lemma less_eq_Pls_Bit:
   1.106 -  "Int.Pls \<le> Int.Bit k v \<longleftrightarrow> Int.Pls \<le> k"
   1.107 -  unfolding Pls_def Bit_def by (cases v) auto
   1.108 +lemma less_eq_Pls_Bit0:
   1.109 +  "Int.Pls \<le> Int.Bit0 k \<longleftrightarrow> Int.Pls \<le> k"
   1.110 +  unfolding Pls_def Bit0_def by auto
   1.111 +
   1.112 +lemma less_eq_Pls_Bit1:
   1.113 +  "Int.Pls \<le> Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
   1.114 +  unfolding Pls_def Bit1_def by auto
   1.115  
   1.116  lemma less_eq_Min_Pls:
   1.117    "Int.Min \<le> Int.Pls \<longleftrightarrow> True"
   1.118 @@ -580,36 +586,44 @@
   1.119    "Int.Min \<le> Int.Min \<longleftrightarrow> True" by rule+
   1.120  
   1.121  lemma less_eq_Min_Bit0:
   1.122 -  "Int.Min \<le> Int.Bit k bit.B0 \<longleftrightarrow> Int.Min < k"
   1.123 -  unfolding Int.Min_def Bit_def by auto
   1.124 +  "Int.Min \<le> Int.Bit0 k \<longleftrightarrow> Int.Min < k"
   1.125 +  unfolding Int.Min_def Bit0_def by auto
   1.126  
   1.127  lemma less_eq_Min_Bit1:
   1.128 -  "Int.Min \<le> Int.Bit k bit.B1 \<longleftrightarrow> Int.Min \<le> k"
   1.129 -  unfolding Int.Min_def Bit_def by auto
   1.130 +  "Int.Min \<le> Int.Bit1 k \<longleftrightarrow> Int.Min \<le> k"
   1.131 +  unfolding Int.Min_def Bit1_def by auto
   1.132  
   1.133  lemma less_eq_Bit0_Pls:
   1.134 -  "Int.Bit k bit.B0 \<le> Int.Pls \<longleftrightarrow> k \<le> Int.Pls"
   1.135 -  unfolding Pls_def Bit_def by simp
   1.136 +  "Int.Bit0 k \<le> Int.Pls \<longleftrightarrow> k \<le> Int.Pls"
   1.137 +  unfolding Pls_def Bit0_def by simp
   1.138  
   1.139  lemma less_eq_Bit1_Pls:
   1.140 -  "Int.Bit k bit.B1 \<le> Int.Pls \<longleftrightarrow> k < Int.Pls"
   1.141 -  unfolding Pls_def Bit_def by auto
   1.142 +  "Int.Bit1 k \<le> Int.Pls \<longleftrightarrow> k < Int.Pls"
   1.143 +  unfolding Pls_def Bit1_def by auto
   1.144  
   1.145 -lemma less_eq_Bit_Min:
   1.146 -  "Int.Bit k v \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
   1.147 -  unfolding Int.Min_def Bit_def by (cases v) auto
   1.148 +lemma less_eq_Bit0_Min:
   1.149 +  "Int.Bit0 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
   1.150 +  unfolding Int.Min_def Bit0_def by auto
   1.151  
   1.152 -lemma less_eq_Bit0_Bit:
   1.153 -  "Int.Bit k1 bit.B0 \<le> Int.Bit k2 v \<longleftrightarrow> k1 \<le> k2"
   1.154 -  unfolding Bit_def bit.cases by (cases v) auto
   1.155 +lemma less_eq_Bit1_Min:
   1.156 +  "Int.Bit1 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
   1.157 +  unfolding Int.Min_def Bit1_def by auto
   1.158  
   1.159 -lemma less_eq_Bit_Bit1:
   1.160 -  "Int.Bit k1 v \<le> Int.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
   1.161 -  unfolding Bit_def bit.cases by (cases v) auto
   1.162 +lemma less_eq_Bit0_Bit0:
   1.163 +  "Int.Bit0 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 \<le> k2"
   1.164 +  unfolding Bit0_def by auto
   1.165 +
   1.166 +lemma less_eq_Bit0_Bit1:
   1.167 +  "Int.Bit0 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
   1.168 +  unfolding Bit0_def Bit1_def by auto
   1.169  
   1.170  lemma less_eq_Bit1_Bit0:
   1.171 -  "Int.Bit k1 bit.B1 \<le> Int.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
   1.172 -  unfolding Bit_def by (auto split: bit.split)
   1.173 +  "Int.Bit1 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
   1.174 +  unfolding Bit0_def Bit1_def by auto
   1.175 +
   1.176 +lemma less_eq_Bit1_Bit1:
   1.177 +  "Int.Bit1 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
   1.178 +  unfolding Bit1_def by auto
   1.179  
   1.180  lemma less_eq_number_of:
   1.181    "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
   1.182 @@ -624,12 +638,12 @@
   1.183    unfolding Pls_def Int.Min_def  by presburger 
   1.184  
   1.185  lemma less_Pls_Bit0:
   1.186 -  "Int.Pls < Int.Bit k bit.B0 \<longleftrightarrow> Int.Pls < k"
   1.187 -  unfolding Pls_def Bit_def by auto
   1.188 +  "Int.Pls < Int.Bit0 k \<longleftrightarrow> Int.Pls < k"
   1.189 +  unfolding Pls_def Bit0_def by auto
   1.190  
   1.191  lemma less_Pls_Bit1:
   1.192 -  "Int.Pls < Int.Bit k bit.B1 \<longleftrightarrow> Int.Pls \<le> k"
   1.193 -  unfolding Pls_def Bit_def by auto
   1.194 +  "Int.Pls < Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
   1.195 +  unfolding Pls_def Bit1_def by auto
   1.196  
   1.197  lemma less_Min_Pls:
   1.198    "Int.Min < Int.Pls \<longleftrightarrow> True"
   1.199 @@ -638,33 +652,45 @@
   1.200  lemma less_Min_Min:
   1.201    "Int.Min < Int.Min \<longleftrightarrow> False"  by simp
   1.202  
   1.203 -lemma less_Min_Bit:
   1.204 -  "Int.Min < Int.Bit k v \<longleftrightarrow> Int.Min < k"
   1.205 -  unfolding Int.Min_def Bit_def by (auto split: bit.split)
   1.206 +lemma less_Min_Bit0:
   1.207 +  "Int.Min < Int.Bit0 k \<longleftrightarrow> Int.Min < k"
   1.208 +  unfolding Int.Min_def Bit0_def by auto
   1.209 +
   1.210 +lemma less_Min_Bit1:
   1.211 +  "Int.Min < Int.Bit1 k \<longleftrightarrow> Int.Min < k"
   1.212 +  unfolding Int.Min_def Bit1_def by auto
   1.213  
   1.214 -lemma less_Bit_Pls:
   1.215 -  "Int.Bit k v < Int.Pls \<longleftrightarrow> k < Int.Pls"
   1.216 -  unfolding Pls_def Bit_def by (auto split: bit.split)
   1.217 +lemma less_Bit0_Pls:
   1.218 +  "Int.Bit0 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
   1.219 +  unfolding Pls_def Bit0_def by auto
   1.220 +
   1.221 +lemma less_Bit1_Pls:
   1.222 +  "Int.Bit1 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
   1.223 +  unfolding Pls_def Bit1_def by auto
   1.224  
   1.225  lemma less_Bit0_Min:
   1.226 -  "Int.Bit k bit.B0 < Int.Min \<longleftrightarrow> k \<le> Int.Min"
   1.227 -  unfolding Int.Min_def Bit_def by auto
   1.228 +  "Int.Bit0 k < Int.Min \<longleftrightarrow> k \<le> Int.Min"
   1.229 +  unfolding Int.Min_def Bit0_def by auto
   1.230  
   1.231  lemma less_Bit1_Min:
   1.232 -  "Int.Bit k bit.B1 < Int.Min \<longleftrightarrow> k < Int.Min"
   1.233 -  unfolding Int.Min_def Bit_def by auto
   1.234 +  "Int.Bit1 k < Int.Min \<longleftrightarrow> k < Int.Min"
   1.235 +  unfolding Int.Min_def Bit1_def by auto
   1.236  
   1.237 -lemma less_Bit_Bit0:
   1.238 -  "Int.Bit k1 v < Int.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
   1.239 -  unfolding Bit_def by (auto split: bit.split)
   1.240 -
   1.241 -lemma less_Bit1_Bit:
   1.242 -  "Int.Bit k1 bit.B1 < Int.Bit k2 v \<longleftrightarrow> k1 < k2"
   1.243 -  unfolding Bit_def by (auto split: bit.split)
   1.244 +lemma less_Bit0_Bit0:
   1.245 +  "Int.Bit0 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
   1.246 +  unfolding Bit0_def by auto
   1.247  
   1.248  lemma less_Bit0_Bit1:
   1.249 -  "Int.Bit k1 bit.B0 < Int.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
   1.250 -  unfolding Bit_def bit.cases  by arith
   1.251 +  "Int.Bit0 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
   1.252 +  unfolding Bit0_def Bit1_def by auto
   1.253 +
   1.254 +lemma less_Bit1_Bit0:
   1.255 +  "Int.Bit1 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
   1.256 +  unfolding Bit0_def Bit1_def by auto
   1.257 +
   1.258 +lemma less_Bit1_Bit1:
   1.259 +  "Int.Bit1 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 < k2"
   1.260 +  unfolding Bit1_def by auto
   1.261  
   1.262  lemma less_number_of:
   1.263    "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
   1.264 @@ -689,17 +715,22 @@
   1.265  lemmas eq_numeral_code [code func] =
   1.266    eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1
   1.267    eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
   1.268 -  eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit
   1.269 +  eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min
   1.270 +  eq_Bit0_Bit0 eq_Bit0_Bit1 eq_Bit1_Bit0 eq_Bit1_Bit1
   1.271    eq_number_of
   1.272  
   1.273 -lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit
   1.274 +lemmas less_eq_numeral_code [code func] =
   1.275 +  less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit0 less_eq_Pls_Bit1
   1.276    less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
   1.277 -  less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1 less_eq_Bit1_Bit0
   1.278 +  less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit0_Min less_eq_Bit1_Min
   1.279 +  less_eq_Bit0_Bit0 less_eq_Bit0_Bit1 less_eq_Bit1_Bit0 less_eq_Bit1_Bit1
   1.280    less_eq_number_of
   1.281  
   1.282 -lemmas less_numeral_code [code func] = less_Pls_Pls less_Pls_Min less_Pls_Bit0
   1.283 -  less_Pls_Bit1 less_Min_Pls less_Min_Min less_Min_Bit less_Bit_Pls
   1.284 -  less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1
   1.285 +lemmas less_numeral_code [code func] =
   1.286 +  less_Pls_Pls less_Pls_Min less_Pls_Bit0 less_Pls_Bit1
   1.287 +  less_Min_Pls less_Min_Min less_Min_Bit0 less_Min_Bit1
   1.288 +  less_Bit0_Pls less_Bit1_Pls less_Bit0_Min less_Bit1_Min
   1.289 +  less_Bit0_Bit0 less_Bit0_Bit1 less_Bit1_Bit0 less_Bit1_Bit1
   1.290    less_number_of
   1.291  
   1.292  context ring_1