1.1 --- a/src/HOL/Presburger.thy	Tue Jan 15 16:19:21 2008 +0100
     1.2 +++ b/src/HOL/Presburger.thy	Tue Jan 15 16:19:23 2008 +0100
     1.3 @@ -496,53 +496,53 @@
     1.4  *}
     1.5  
     1.6  lemma eq_Pls_Pls:
     1.7 -  "Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by presburger
     1.8 +  "Int.Pls = Int.Pls \<longleftrightarrow> True" by presburger
     1.9  
    1.10  lemma eq_Pls_Min:
    1.11 -  "Numeral.Pls = Numeral.Min \<longleftrightarrow> False"
    1.12 -  unfolding Pls_def Numeral.Min_def by presburger
    1.13 +  "Int.Pls = Int.Min \<longleftrightarrow> False"
    1.14 +  unfolding Pls_def Int.Min_def by presburger
    1.15  
    1.16  lemma eq_Pls_Bit0:
    1.17 -  "Numeral.Pls = Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls = k"
    1.18 +  "Int.Pls = Int.Bit k bit.B0 \<longleftrightarrow> Int.Pls = k"
    1.19    unfolding Pls_def Bit_def bit.cases by presburger
    1.20  
    1.21  lemma eq_Pls_Bit1:
    1.22 -  "Numeral.Pls = Numeral.Bit k bit.B1 \<longleftrightarrow> False"
    1.23 +  "Int.Pls = Int.Bit k bit.B1 \<longleftrightarrow> False"
    1.24    unfolding Pls_def Bit_def bit.cases by presburger
    1.25  
    1.26  lemma eq_Min_Pls:
    1.27 -  "Numeral.Min = Numeral.Pls \<longleftrightarrow> False"
    1.28 -  unfolding Pls_def Numeral.Min_def by presburger
    1.29 +  "Int.Min = Int.Pls \<longleftrightarrow> False"
    1.30 +  unfolding Pls_def Int.Min_def by presburger
    1.31  
    1.32  lemma eq_Min_Min:
    1.33 -  "Numeral.Min = Numeral.Min \<longleftrightarrow> True" by presburger
    1.34 +  "Int.Min = Int.Min \<longleftrightarrow> True" by presburger
    1.35  
    1.36  lemma eq_Min_Bit0:
    1.37 -  "Numeral.Min = Numeral.Bit k bit.B0 \<longleftrightarrow> False"
    1.38 -  unfolding Numeral.Min_def Bit_def bit.cases by presburger
    1.39 +  "Int.Min = Int.Bit k bit.B0 \<longleftrightarrow> False"
    1.40 +  unfolding Int.Min_def Bit_def bit.cases by presburger
    1.41  
    1.42  lemma eq_Min_Bit1:
    1.43 -  "Numeral.Min = Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min = k"
    1.44 -  unfolding Numeral.Min_def Bit_def bit.cases by presburger
    1.45 +  "Int.Min = Int.Bit k bit.B1 \<longleftrightarrow> Int.Min = k"
    1.46 +  unfolding Int.Min_def Bit_def bit.cases by presburger
    1.47  
    1.48  lemma eq_Bit0_Pls:
    1.49 -  "Numeral.Bit k bit.B0 = Numeral.Pls \<longleftrightarrow> Numeral.Pls = k"
    1.50 +  "Int.Bit k bit.B0 = Int.Pls \<longleftrightarrow> Int.Pls = k"
    1.51    unfolding Pls_def Bit_def bit.cases by presburger
    1.52  
    1.53  lemma eq_Bit1_Pls:
    1.54 -  "Numeral.Bit k bit.B1 = Numeral.Pls \<longleftrightarrow> False"
    1.55 +  "Int.Bit k bit.B1 = Int.Pls \<longleftrightarrow> False"
    1.56    unfolding Pls_def Bit_def bit.cases  by presburger
    1.57  
    1.58  lemma eq_Bit0_Min:
    1.59 -  "Numeral.Bit k bit.B0 = Numeral.Min \<longleftrightarrow> False"
    1.60 -  unfolding Numeral.Min_def Bit_def bit.cases  by presburger
    1.61 +  "Int.Bit k bit.B0 = Int.Min \<longleftrightarrow> False"
    1.62 +  unfolding Int.Min_def Bit_def bit.cases  by presburger
    1.63  
    1.64  lemma eq_Bit1_Min:
    1.65 -  "(Numeral.Bit k bit.B1) = Numeral.Min \<longleftrightarrow> Numeral.Min = k"
    1.66 -  unfolding Numeral.Min_def Bit_def bit.cases  by presburger
    1.67 +  "(Int.Bit k bit.B1) = Int.Min \<longleftrightarrow> Int.Min = k"
    1.68 +  unfolding Int.Min_def Bit_def bit.cases  by presburger
    1.69  
    1.70  lemma eq_Bit_Bit:
    1.71 -  "Numeral.Bit k1 v1 = Numeral.Bit k2 v2 \<longleftrightarrow>
    1.72 +  "Int.Bit k1 v1 = Int.Bit k2 v2 \<longleftrightarrow>
    1.73      v1 = v2 \<and> k1 = k2" 
    1.74    unfolding Bit_def
    1.75    apply (cases v1)
    1.76 @@ -562,53 +562,53 @@
    1.77  
    1.78  
    1.79  lemma less_eq_Pls_Pls:
    1.80 -  "Numeral.Pls \<le> Numeral.Pls \<longleftrightarrow> True" by rule+
    1.81 +  "Int.Pls \<le> Int.Pls \<longleftrightarrow> True" by rule+
    1.82  
    1.83  lemma less_eq_Pls_Min:
    1.84 -  "Numeral.Pls \<le> Numeral.Min \<longleftrightarrow> False"
    1.85 -  unfolding Pls_def Numeral.Min_def by presburger
    1.86 +  "Int.Pls \<le> Int.Min \<longleftrightarrow> False"
    1.87 +  unfolding Pls_def Int.Min_def by presburger
    1.88  
    1.89  lemma less_eq_Pls_Bit:
    1.90 -  "Numeral.Pls \<le> Numeral.Bit k v \<longleftrightarrow> Numeral.Pls \<le> k"
    1.91 +  "Int.Pls \<le> Int.Bit k v \<longleftrightarrow> Int.Pls \<le> k"
    1.92    unfolding Pls_def Bit_def by (cases v) auto
    1.93  
    1.94  lemma less_eq_Min_Pls:
    1.95 -  "Numeral.Min \<le> Numeral.Pls \<longleftrightarrow> True"
    1.96 -  unfolding Pls_def Numeral.Min_def by presburger
    1.97 +  "Int.Min \<le> Int.Pls \<longleftrightarrow> True"
    1.98 +  unfolding Pls_def Int.Min_def by presburger
    1.99  
   1.100  lemma less_eq_Min_Min:
   1.101 -  "Numeral.Min \<le> Numeral.Min \<longleftrightarrow> True" by rule+
   1.102 +  "Int.Min \<le> Int.Min \<longleftrightarrow> True" by rule+
   1.103  
   1.104  lemma less_eq_Min_Bit0:
   1.105 -  "Numeral.Min \<le> Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Min < k"
   1.106 -  unfolding Numeral.Min_def Bit_def by auto
   1.107 +  "Int.Min \<le> Int.Bit k bit.B0 \<longleftrightarrow> Int.Min < k"
   1.108 +  unfolding Int.Min_def Bit_def by auto
   1.109  
   1.110  lemma less_eq_Min_Bit1:
   1.111 -  "Numeral.Min \<le> Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min \<le> k"
   1.112 -  unfolding Numeral.Min_def Bit_def by auto
   1.113 +  "Int.Min \<le> Int.Bit k bit.B1 \<longleftrightarrow> Int.Min \<le> k"
   1.114 +  unfolding Int.Min_def Bit_def by auto
   1.115  
   1.116  lemma less_eq_Bit0_Pls:
   1.117 -  "Numeral.Bit k bit.B0 \<le> Numeral.Pls \<longleftrightarrow> k \<le> Numeral.Pls"
   1.118 +  "Int.Bit k bit.B0 \<le> Int.Pls \<longleftrightarrow> k \<le> Int.Pls"
   1.119    unfolding Pls_def Bit_def by simp
   1.120  
   1.121  lemma less_eq_Bit1_Pls:
   1.122 -  "Numeral.Bit k bit.B1 \<le> Numeral.Pls \<longleftrightarrow> k < Numeral.Pls"
   1.123 +  "Int.Bit k bit.B1 \<le> Int.Pls \<longleftrightarrow> k < Int.Pls"
   1.124    unfolding Pls_def Bit_def by auto
   1.125  
   1.126  lemma less_eq_Bit_Min:
   1.127 -  "Numeral.Bit k v \<le> Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min"
   1.128 -  unfolding Numeral.Min_def Bit_def by (cases v) auto
   1.129 +  "Int.Bit k v \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
   1.130 +  unfolding Int.Min_def Bit_def by (cases v) auto
   1.131  
   1.132  lemma less_eq_Bit0_Bit:
   1.133 -  "Numeral.Bit k1 bit.B0 \<le> Numeral.Bit k2 v \<longleftrightarrow> k1 \<le> k2"
   1.134 +  "Int.Bit k1 bit.B0 \<le> Int.Bit k2 v \<longleftrightarrow> k1 \<le> k2"
   1.135    unfolding Bit_def bit.cases by (cases v) auto
   1.136  
   1.137  lemma less_eq_Bit_Bit1:
   1.138 -  "Numeral.Bit k1 v \<le> Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
   1.139 +  "Int.Bit k1 v \<le> Int.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
   1.140    unfolding Bit_def bit.cases by (cases v) auto
   1.141  
   1.142  lemma less_eq_Bit1_Bit0:
   1.143 -  "Numeral.Bit k1 bit.B1 \<le> Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
   1.144 +  "Int.Bit k1 bit.B1 \<le> Int.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
   1.145    unfolding Bit_def by (auto split: bit.split)
   1.146  
   1.147  lemma less_eq_number_of:
   1.148 @@ -617,53 +617,53 @@
   1.149  
   1.150  
   1.151  lemma less_Pls_Pls:
   1.152 -  "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by simp 
   1.153 +  "Int.Pls < Int.Pls \<longleftrightarrow> False" by simp 
   1.154  
   1.155  lemma less_Pls_Min:
   1.156 -  "Numeral.Pls < Numeral.Min \<longleftrightarrow> False"
   1.157 -  unfolding Pls_def Numeral.Min_def  by presburger 
   1.158 +  "Int.Pls < Int.Min \<longleftrightarrow> False"
   1.159 +  unfolding Pls_def Int.Min_def  by presburger 
   1.160  
   1.161  lemma less_Pls_Bit0:
   1.162 -  "Numeral.Pls < Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls < k"
   1.163 +  "Int.Pls < Int.Bit k bit.B0 \<longleftrightarrow> Int.Pls < k"
   1.164    unfolding Pls_def Bit_def by auto
   1.165  
   1.166  lemma less_Pls_Bit1:
   1.167 -  "Numeral.Pls < Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Pls \<le> k"
   1.168 +  "Int.Pls < Int.Bit k bit.B1 \<longleftrightarrow> Int.Pls \<le> k"
   1.169    unfolding Pls_def Bit_def by auto
   1.170  
   1.171  lemma less_Min_Pls:
   1.172 -  "Numeral.Min < Numeral.Pls \<longleftrightarrow> True"
   1.173 -  unfolding Pls_def Numeral.Min_def by presburger 
   1.174 +  "Int.Min < Int.Pls \<longleftrightarrow> True"
   1.175 +  unfolding Pls_def Int.Min_def by presburger 
   1.176  
   1.177  lemma less_Min_Min:
   1.178 -  "Numeral.Min < Numeral.Min \<longleftrightarrow> False"  by simp
   1.179 +  "Int.Min < Int.Min \<longleftrightarrow> False"  by simp
   1.180  
   1.181  lemma less_Min_Bit:
   1.182 -  "Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k"
   1.183 -  unfolding Numeral.Min_def Bit_def by (auto split: bit.split)
   1.184 +  "Int.Min < Int.Bit k v \<longleftrightarrow> Int.Min < k"
   1.185 +  unfolding Int.Min_def Bit_def by (auto split: bit.split)
   1.186  
   1.187  lemma less_Bit_Pls:
   1.188 -  "Numeral.Bit k v < Numeral.Pls \<longleftrightarrow> k < Numeral.Pls"
   1.189 +  "Int.Bit k v < Int.Pls \<longleftrightarrow> k < Int.Pls"
   1.190    unfolding Pls_def Bit_def by (auto split: bit.split)
   1.191  
   1.192  lemma less_Bit0_Min:
   1.193 -  "Numeral.Bit k bit.B0 < Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min"
   1.194 -  unfolding Numeral.Min_def Bit_def by auto
   1.195 +  "Int.Bit k bit.B0 < Int.Min \<longleftrightarrow> k \<le> Int.Min"
   1.196 +  unfolding Int.Min_def Bit_def by auto
   1.197  
   1.198  lemma less_Bit1_Min:
   1.199 -  "Numeral.Bit k bit.B1 < Numeral.Min \<longleftrightarrow> k < Numeral.Min"
   1.200 -  unfolding Numeral.Min_def Bit_def by auto
   1.201 +  "Int.Bit k bit.B1 < Int.Min \<longleftrightarrow> k < Int.Min"
   1.202 +  unfolding Int.Min_def Bit_def by auto
   1.203  
   1.204  lemma less_Bit_Bit0:
   1.205 -  "Numeral.Bit k1 v < Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
   1.206 +  "Int.Bit k1 v < Int.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
   1.207    unfolding Bit_def by (auto split: bit.split)
   1.208  
   1.209  lemma less_Bit1_Bit:
   1.210 -  "Numeral.Bit k1 bit.B1 < Numeral.Bit k2 v \<longleftrightarrow> k1 < k2"
   1.211 +  "Int.Bit k1 bit.B1 < Int.Bit k2 v \<longleftrightarrow> k1 < k2"
   1.212    unfolding Bit_def by (auto split: bit.split)
   1.213  
   1.214  lemma less_Bit0_Bit1:
   1.215 -  "Numeral.Bit k1 bit.B0 < Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
   1.216 +  "Int.Bit k1 bit.B0 < Int.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
   1.217    unfolding Bit_def bit.cases  by arith
   1.218  
   1.219  lemma less_number_of: