src/HOL/Presburger.thy
changeset 26508 4cd7c4f936bb
parent 26156 420c1947511c
child 27540 dc38e79f5a1c
     1.1 --- a/src/HOL/Presburger.thy	Wed Apr 02 15:58:26 2008 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Wed Apr 02 15:58:27 2008 +0200
     1.3 @@ -489,286 +489,4 @@
     1.4    then show ?thesis by simp
     1.5  qed
     1.6  
     1.7 -
     1.8 -subsection {* Code generator setup *}
     1.9 -
    1.10 -text {*
    1.11 -  Presburger arithmetic is convenient to prove some
    1.12 -  of the following code lemmas on integer numerals:
    1.13 -*}
    1.14 -
    1.15 -lemma eq_Pls_Pls:
    1.16 -  "Int.Pls = Int.Pls \<longleftrightarrow> True" by presburger
    1.17 -
    1.18 -lemma eq_Pls_Min:
    1.19 -  "Int.Pls = Int.Min \<longleftrightarrow> False"
    1.20 -  unfolding Pls_def Int.Min_def by presburger
    1.21 -
    1.22 -lemma eq_Pls_Bit0:
    1.23 -  "Int.Pls = Int.Bit0 k \<longleftrightarrow> Int.Pls = k"
    1.24 -  unfolding Pls_def Bit0_def by presburger
    1.25 -
    1.26 -lemma eq_Pls_Bit1:
    1.27 -  "Int.Pls = Int.Bit1 k \<longleftrightarrow> False"
    1.28 -  unfolding Pls_def Bit1_def by presburger
    1.29 -
    1.30 -lemma eq_Min_Pls:
    1.31 -  "Int.Min = Int.Pls \<longleftrightarrow> False"
    1.32 -  unfolding Pls_def Int.Min_def by presburger
    1.33 -
    1.34 -lemma eq_Min_Min:
    1.35 -  "Int.Min = Int.Min \<longleftrightarrow> True" by presburger
    1.36 -
    1.37 -lemma eq_Min_Bit0:
    1.38 -  "Int.Min = Int.Bit0 k \<longleftrightarrow> False"
    1.39 -  unfolding Int.Min_def Bit0_def by presburger
    1.40 -
    1.41 -lemma eq_Min_Bit1:
    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.Bit0 k = Int.Pls \<longleftrightarrow> Int.Pls = k"
    1.47 -  unfolding Pls_def Bit0_def by presburger
    1.48 -
    1.49 -lemma eq_Bit1_Pls:
    1.50 -  "Int.Bit1 k = Int.Pls \<longleftrightarrow> False"
    1.51 -  unfolding Pls_def Bit1_def by presburger
    1.52 -
    1.53 -lemma eq_Bit0_Min:
    1.54 -  "Int.Bit0 k = Int.Min \<longleftrightarrow> False"
    1.55 -  unfolding Int.Min_def Bit0_def by presburger
    1.56 -
    1.57 -lemma eq_Bit1_Min:
    1.58 -  "Int.Bit1 k = Int.Min \<longleftrightarrow> Int.Min = k"
    1.59 -  unfolding Int.Min_def Bit1_def by presburger
    1.60 -
    1.61 -lemma eq_Bit0_Bit0:
    1.62 -  "Int.Bit0 k1 = Int.Bit0 k2 \<longleftrightarrow> k1 = k2"
    1.63 -  unfolding Bit0_def by presburger
    1.64 -
    1.65 -lemma eq_Bit0_Bit1:
    1.66 -  "Int.Bit0 k1 = Int.Bit1 k2 \<longleftrightarrow> False"
    1.67 -  unfolding Bit0_def Bit1_def by presburger
    1.68 -
    1.69 -lemma eq_Bit1_Bit0:
    1.70 -  "Int.Bit1 k1 = Int.Bit0 k2 \<longleftrightarrow> False"
    1.71 -  unfolding Bit0_def Bit1_def by presburger
    1.72 -
    1.73 -lemma eq_Bit1_Bit1:
    1.74 -  "Int.Bit1 k1 = Int.Bit1 k2 \<longleftrightarrow> k1 = k2"
    1.75 -  unfolding Bit1_def by presburger
    1.76 -
    1.77 -lemma eq_number_of:
    1.78 -  "(number_of k \<Colon> int) = number_of l \<longleftrightarrow> k = l" 
    1.79 -  unfolding number_of_is_id ..
    1.80 -
    1.81 -
    1.82 -lemma less_eq_Pls_Pls:
    1.83 -  "Int.Pls \<le> Int.Pls \<longleftrightarrow> True" by rule+
    1.84 -
    1.85 -lemma less_eq_Pls_Min:
    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_Bit0:
    1.90 -  "Int.Pls \<le> Int.Bit0 k \<longleftrightarrow> Int.Pls \<le> k"
    1.91 -  unfolding Pls_def Bit0_def by auto
    1.92 -
    1.93 -lemma less_eq_Pls_Bit1:
    1.94 -  "Int.Pls \<le> Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
    1.95 -  unfolding Pls_def Bit1_def by auto
    1.96 -
    1.97 -lemma less_eq_Min_Pls:
    1.98 -  "Int.Min \<le> Int.Pls \<longleftrightarrow> True"
    1.99 -  unfolding Pls_def Int.Min_def by presburger
   1.100 -
   1.101 -lemma less_eq_Min_Min:
   1.102 -  "Int.Min \<le> Int.Min \<longleftrightarrow> True" by rule+
   1.103 -
   1.104 -lemma less_eq_Min_Bit0:
   1.105 -  "Int.Min \<le> Int.Bit0 k \<longleftrightarrow> Int.Min < k"
   1.106 -  unfolding Int.Min_def Bit0_def by auto
   1.107 -
   1.108 -lemma less_eq_Min_Bit1:
   1.109 -  "Int.Min \<le> Int.Bit1 k \<longleftrightarrow> Int.Min \<le> k"
   1.110 -  unfolding Int.Min_def Bit1_def by auto
   1.111 -
   1.112 -lemma less_eq_Bit0_Pls:
   1.113 -  "Int.Bit0 k \<le> Int.Pls \<longleftrightarrow> k \<le> Int.Pls"
   1.114 -  unfolding Pls_def Bit0_def by simp
   1.115 -
   1.116 -lemma less_eq_Bit1_Pls:
   1.117 -  "Int.Bit1 k \<le> Int.Pls \<longleftrightarrow> k < Int.Pls"
   1.118 -  unfolding Pls_def Bit1_def by auto
   1.119 -
   1.120 -lemma less_eq_Bit0_Min:
   1.121 -  "Int.Bit0 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
   1.122 -  unfolding Int.Min_def Bit0_def by auto
   1.123 -
   1.124 -lemma less_eq_Bit1_Min:
   1.125 -  "Int.Bit1 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
   1.126 -  unfolding Int.Min_def Bit1_def by auto
   1.127 -
   1.128 -lemma less_eq_Bit0_Bit0:
   1.129 -  "Int.Bit0 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 \<le> k2"
   1.130 -  unfolding Bit0_def by auto
   1.131 -
   1.132 -lemma less_eq_Bit0_Bit1:
   1.133 -  "Int.Bit0 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
   1.134 -  unfolding Bit0_def Bit1_def by auto
   1.135 -
   1.136 -lemma less_eq_Bit1_Bit0:
   1.137 -  "Int.Bit1 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
   1.138 -  unfolding Bit0_def Bit1_def by auto
   1.139 -
   1.140 -lemma less_eq_Bit1_Bit1:
   1.141 -  "Int.Bit1 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
   1.142 -  unfolding Bit1_def by auto
   1.143 -
   1.144 -lemma less_eq_number_of:
   1.145 -  "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
   1.146 -  unfolding number_of_is_id ..
   1.147 -
   1.148 -
   1.149 -lemma less_Pls_Pls:
   1.150 -  "Int.Pls < Int.Pls \<longleftrightarrow> False" by simp 
   1.151 -
   1.152 -lemma less_Pls_Min:
   1.153 -  "Int.Pls < Int.Min \<longleftrightarrow> False"
   1.154 -  unfolding Pls_def Int.Min_def  by presburger 
   1.155 -
   1.156 -lemma less_Pls_Bit0:
   1.157 -  "Int.Pls < Int.Bit0 k \<longleftrightarrow> Int.Pls < k"
   1.158 -  unfolding Pls_def Bit0_def by auto
   1.159 -
   1.160 -lemma less_Pls_Bit1:
   1.161 -  "Int.Pls < Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
   1.162 -  unfolding Pls_def Bit1_def by auto
   1.163 -
   1.164 -lemma less_Min_Pls:
   1.165 -  "Int.Min < Int.Pls \<longleftrightarrow> True"
   1.166 -  unfolding Pls_def Int.Min_def by presburger 
   1.167 -
   1.168 -lemma less_Min_Min:
   1.169 -  "Int.Min < Int.Min \<longleftrightarrow> False"  by simp
   1.170 -
   1.171 -lemma less_Min_Bit0:
   1.172 -  "Int.Min < Int.Bit0 k \<longleftrightarrow> Int.Min < k"
   1.173 -  unfolding Int.Min_def Bit0_def by auto
   1.174 -
   1.175 -lemma less_Min_Bit1:
   1.176 -  "Int.Min < Int.Bit1 k \<longleftrightarrow> Int.Min < k"
   1.177 -  unfolding Int.Min_def Bit1_def by auto
   1.178 -
   1.179 -lemma less_Bit0_Pls:
   1.180 -  "Int.Bit0 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
   1.181 -  unfolding Pls_def Bit0_def by auto
   1.182 -
   1.183 -lemma less_Bit1_Pls:
   1.184 -  "Int.Bit1 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
   1.185 -  unfolding Pls_def Bit1_def by auto
   1.186 -
   1.187 -lemma less_Bit0_Min:
   1.188 -  "Int.Bit0 k < Int.Min \<longleftrightarrow> k \<le> Int.Min"
   1.189 -  unfolding Int.Min_def Bit0_def by auto
   1.190 -
   1.191 -lemma less_Bit1_Min:
   1.192 -  "Int.Bit1 k < Int.Min \<longleftrightarrow> k < Int.Min"
   1.193 -  unfolding Int.Min_def Bit1_def by auto
   1.194 -
   1.195 -lemma less_Bit0_Bit0:
   1.196 -  "Int.Bit0 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
   1.197 -  unfolding Bit0_def by auto
   1.198 -
   1.199 -lemma less_Bit0_Bit1:
   1.200 -  "Int.Bit0 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
   1.201 -  unfolding Bit0_def Bit1_def by auto
   1.202 -
   1.203 -lemma less_Bit1_Bit0:
   1.204 -  "Int.Bit1 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
   1.205 -  unfolding Bit0_def Bit1_def by auto
   1.206 -
   1.207 -lemma less_Bit1_Bit1:
   1.208 -  "Int.Bit1 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 < k2"
   1.209 -  unfolding Bit1_def by auto
   1.210 -
   1.211 -lemma less_number_of:
   1.212 -  "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
   1.213 -  unfolding number_of_is_id ..
   1.214 -
   1.215 -lemmas pred_succ_numeral_code [code func] =
   1.216 -  pred_bin_simps succ_bin_simps
   1.217 -
   1.218 -lemmas plus_numeral_code [code func] =
   1.219 -  add_bin_simps
   1.220 -  arith_extra_simps(1) [where 'a = int]
   1.221 -
   1.222 -lemmas minus_numeral_code [code func] =
   1.223 -  minus_bin_simps
   1.224 -  arith_extra_simps(2) [where 'a = int]
   1.225 -  arith_extra_simps(5) [where 'a = int]
   1.226 -
   1.227 -lemmas times_numeral_code [code func] =
   1.228 -  mult_bin_simps
   1.229 -  arith_extra_simps(4) [where 'a = int]
   1.230 -
   1.231 -lemmas eq_numeral_code [code func] =
   1.232 -  eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1
   1.233 -  eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
   1.234 -  eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min
   1.235 -  eq_Bit0_Bit0 eq_Bit0_Bit1 eq_Bit1_Bit0 eq_Bit1_Bit1
   1.236 -  eq_number_of
   1.237 -
   1.238 -lemmas less_eq_numeral_code [code func] =
   1.239 -  less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit0 less_eq_Pls_Bit1
   1.240 -  less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
   1.241 -  less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit0_Min less_eq_Bit1_Min
   1.242 -  less_eq_Bit0_Bit0 less_eq_Bit0_Bit1 less_eq_Bit1_Bit0 less_eq_Bit1_Bit1
   1.243 -  less_eq_number_of
   1.244 -
   1.245 -lemmas less_numeral_code [code func] =
   1.246 -  less_Pls_Pls less_Pls_Min less_Pls_Bit0 less_Pls_Bit1
   1.247 -  less_Min_Pls less_Min_Min less_Min_Bit0 less_Min_Bit1
   1.248 -  less_Bit0_Pls less_Bit1_Pls less_Bit0_Min less_Bit1_Min
   1.249 -  less_Bit0_Bit0 less_Bit0_Bit1 less_Bit1_Bit0 less_Bit1_Bit1
   1.250 -  less_number_of
   1.251 -
   1.252 -context ring_1
   1.253 -begin
   1.254 -
   1.255 -lemma of_int_num [code func]:
   1.256 -  "of_int k = (if k = 0 then 0 else if k < 0 then
   1.257 -     - of_int (- k) else let
   1.258 -       (l, m) = divAlg (k, 2);
   1.259 -       l' = of_int l
   1.260 -     in if m = 0 then l' + l' else l' + l' + 1)"
   1.261 -proof -
   1.262 -  have aux1: "k mod (2\<Colon>int) \<noteq> (0\<Colon>int) \<Longrightarrow> 
   1.263 -    of_int k = of_int (k div 2 * 2 + 1)"
   1.264 -  proof -
   1.265 -    assume "k mod 2 \<noteq> 0"
   1.266 -    then have "k mod 2 = 1" by arith
   1.267 -    moreover have "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
   1.268 -    ultimately show ?thesis by auto
   1.269 -  qed
   1.270 -  have aux2: "\<And>x. of_int 2 * x = x + x"
   1.271 -  proof -
   1.272 -    fix x
   1.273 -    have int2: "(2::int) = 1 + 1" by arith
   1.274 -    show "of_int 2 * x = x + x"
   1.275 -    unfolding int2 of_int_add left_distrib by simp
   1.276 -  qed
   1.277 -  have aux3: "\<And>x. x * of_int 2 = x + x"
   1.278 -  proof -
   1.279 -    fix x
   1.280 -    have int2: "(2::int) = 1 + 1" by arith
   1.281 -    show "x * of_int 2 = x + x" 
   1.282 -    unfolding int2 of_int_add right_distrib by simp
   1.283 -  qed
   1.284 -  from aux1 show ?thesis by (auto simp add: divAlg_mod_div Let_def aux2 aux3)
   1.285 -qed
   1.286 -
   1.287  end
   1.288 -
   1.289 -end