# HG changeset patch
# User haftmann
# Date 1207144707 -7200
# Node ID 4cd7c4f936bb1314de3d7cd7ce23e27ce8d2b0b9
# Parent  6da615cef733f19780a791443e4e41bc01d840e5
moved some code lemmas for Numerals to other theories

diff -r 6da615cef733 -r 4cd7c4f936bb src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Wed Apr 02 15:58:26 2008 +0200
+++ b/src/HOL/Presburger.thy	Wed Apr 02 15:58:27 2008 +0200
@@ -489,286 +489,4 @@
   then show ?thesis by simp
 qed
 
-
-subsection {* Code generator setup *}
-
-text {*
-  Presburger arithmetic is convenient to prove some
-  of the following code lemmas on integer numerals:
-*}
-
-lemma eq_Pls_Pls:
-  "Int.Pls = Int.Pls \<longleftrightarrow> True" by presburger
-
-lemma eq_Pls_Min:
-  "Int.Pls = Int.Min \<longleftrightarrow> False"
-  unfolding Pls_def Int.Min_def by presburger
-
-lemma eq_Pls_Bit0:
-  "Int.Pls = Int.Bit0 k \<longleftrightarrow> Int.Pls = k"
-  unfolding Pls_def Bit0_def by presburger
-
-lemma eq_Pls_Bit1:
-  "Int.Pls = Int.Bit1 k \<longleftrightarrow> False"
-  unfolding Pls_def Bit1_def by presburger
-
-lemma eq_Min_Pls:
-  "Int.Min = Int.Pls \<longleftrightarrow> False"
-  unfolding Pls_def Int.Min_def by presburger
-
-lemma eq_Min_Min:
-  "Int.Min = Int.Min \<longleftrightarrow> True" by presburger
-
-lemma eq_Min_Bit0:
-  "Int.Min = Int.Bit0 k \<longleftrightarrow> False"
-  unfolding Int.Min_def Bit0_def by presburger
-
-lemma eq_Min_Bit1:
-  "Int.Min = Int.Bit1 k \<longleftrightarrow> Int.Min = k"
-  unfolding Int.Min_def Bit1_def by presburger
-
-lemma eq_Bit0_Pls:
-  "Int.Bit0 k = Int.Pls \<longleftrightarrow> Int.Pls = k"
-  unfolding Pls_def Bit0_def by presburger
-
-lemma eq_Bit1_Pls:
-  "Int.Bit1 k = Int.Pls \<longleftrightarrow> False"
-  unfolding Pls_def Bit1_def by presburger
-
-lemma eq_Bit0_Min:
-  "Int.Bit0 k = Int.Min \<longleftrightarrow> False"
-  unfolding Int.Min_def Bit0_def by presburger
-
-lemma eq_Bit1_Min:
-  "Int.Bit1 k = Int.Min \<longleftrightarrow> Int.Min = k"
-  unfolding Int.Min_def Bit1_def by presburger
-
-lemma eq_Bit0_Bit0:
-  "Int.Bit0 k1 = Int.Bit0 k2 \<longleftrightarrow> k1 = k2"
-  unfolding Bit0_def by presburger
-
-lemma eq_Bit0_Bit1:
-  "Int.Bit0 k1 = Int.Bit1 k2 \<longleftrightarrow> False"
-  unfolding Bit0_def Bit1_def by presburger
-
-lemma eq_Bit1_Bit0:
-  "Int.Bit1 k1 = Int.Bit0 k2 \<longleftrightarrow> False"
-  unfolding Bit0_def Bit1_def by presburger
-
-lemma eq_Bit1_Bit1:
-  "Int.Bit1 k1 = Int.Bit1 k2 \<longleftrightarrow> k1 = k2"
-  unfolding Bit1_def by presburger
-
-lemma eq_number_of:
-  "(number_of k \<Colon> int) = number_of l \<longleftrightarrow> k = l" 
-  unfolding number_of_is_id ..
-
-
-lemma less_eq_Pls_Pls:
-  "Int.Pls \<le> Int.Pls \<longleftrightarrow> True" by rule+
-
-lemma less_eq_Pls_Min:
-  "Int.Pls \<le> Int.Min \<longleftrightarrow> False"
-  unfolding Pls_def Int.Min_def by presburger
-
-lemma less_eq_Pls_Bit0:
-  "Int.Pls \<le> Int.Bit0 k \<longleftrightarrow> Int.Pls \<le> k"
-  unfolding Pls_def Bit0_def by auto
-
-lemma less_eq_Pls_Bit1:
-  "Int.Pls \<le> Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
-  unfolding Pls_def Bit1_def by auto
-
-lemma less_eq_Min_Pls:
-  "Int.Min \<le> Int.Pls \<longleftrightarrow> True"
-  unfolding Pls_def Int.Min_def by presburger
-
-lemma less_eq_Min_Min:
-  "Int.Min \<le> Int.Min \<longleftrightarrow> True" by rule+
-
-lemma less_eq_Min_Bit0:
-  "Int.Min \<le> Int.Bit0 k \<longleftrightarrow> Int.Min < k"
-  unfolding Int.Min_def Bit0_def by auto
-
-lemma less_eq_Min_Bit1:
-  "Int.Min \<le> Int.Bit1 k \<longleftrightarrow> Int.Min \<le> k"
-  unfolding Int.Min_def Bit1_def by auto
-
-lemma less_eq_Bit0_Pls:
-  "Int.Bit0 k \<le> Int.Pls \<longleftrightarrow> k \<le> Int.Pls"
-  unfolding Pls_def Bit0_def by simp
-
-lemma less_eq_Bit1_Pls:
-  "Int.Bit1 k \<le> Int.Pls \<longleftrightarrow> k < Int.Pls"
-  unfolding Pls_def Bit1_def by auto
-
-lemma less_eq_Bit0_Min:
-  "Int.Bit0 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
-  unfolding Int.Min_def Bit0_def by auto
-
-lemma less_eq_Bit1_Min:
-  "Int.Bit1 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
-  unfolding Int.Min_def Bit1_def by auto
-
-lemma less_eq_Bit0_Bit0:
-  "Int.Bit0 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 \<le> k2"
-  unfolding Bit0_def by auto
-
-lemma less_eq_Bit0_Bit1:
-  "Int.Bit0 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
-  unfolding Bit0_def Bit1_def by auto
-
-lemma less_eq_Bit1_Bit0:
-  "Int.Bit1 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
-  unfolding Bit0_def Bit1_def by auto
-
-lemma less_eq_Bit1_Bit1:
-  "Int.Bit1 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
-  unfolding Bit1_def by auto
-
-lemma less_eq_number_of:
-  "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
-  unfolding number_of_is_id ..
-
-
-lemma less_Pls_Pls:
-  "Int.Pls < Int.Pls \<longleftrightarrow> False" by simp 
-
-lemma less_Pls_Min:
-  "Int.Pls < Int.Min \<longleftrightarrow> False"
-  unfolding Pls_def Int.Min_def  by presburger 
-
-lemma less_Pls_Bit0:
-  "Int.Pls < Int.Bit0 k \<longleftrightarrow> Int.Pls < k"
-  unfolding Pls_def Bit0_def by auto
-
-lemma less_Pls_Bit1:
-  "Int.Pls < Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
-  unfolding Pls_def Bit1_def by auto
-
-lemma less_Min_Pls:
-  "Int.Min < Int.Pls \<longleftrightarrow> True"
-  unfolding Pls_def Int.Min_def by presburger 
-
-lemma less_Min_Min:
-  "Int.Min < Int.Min \<longleftrightarrow> False"  by simp
-
-lemma less_Min_Bit0:
-  "Int.Min < Int.Bit0 k \<longleftrightarrow> Int.Min < k"
-  unfolding Int.Min_def Bit0_def by auto
-
-lemma less_Min_Bit1:
-  "Int.Min < Int.Bit1 k \<longleftrightarrow> Int.Min < k"
-  unfolding Int.Min_def Bit1_def by auto
-
-lemma less_Bit0_Pls:
-  "Int.Bit0 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
-  unfolding Pls_def Bit0_def by auto
-
-lemma less_Bit1_Pls:
-  "Int.Bit1 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
-  unfolding Pls_def Bit1_def by auto
-
-lemma less_Bit0_Min:
-  "Int.Bit0 k < Int.Min \<longleftrightarrow> k \<le> Int.Min"
-  unfolding Int.Min_def Bit0_def by auto
-
-lemma less_Bit1_Min:
-  "Int.Bit1 k < Int.Min \<longleftrightarrow> k < Int.Min"
-  unfolding Int.Min_def Bit1_def by auto
-
-lemma less_Bit0_Bit0:
-  "Int.Bit0 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
-  unfolding Bit0_def by auto
-
-lemma less_Bit0_Bit1:
-  "Int.Bit0 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
-  unfolding Bit0_def Bit1_def by auto
-
-lemma less_Bit1_Bit0:
-  "Int.Bit1 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
-  unfolding Bit0_def Bit1_def by auto
-
-lemma less_Bit1_Bit1:
-  "Int.Bit1 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 < k2"
-  unfolding Bit1_def by auto
-
-lemma less_number_of:
-  "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
-  unfolding number_of_is_id ..
-
-lemmas pred_succ_numeral_code [code func] =
-  pred_bin_simps succ_bin_simps
-
-lemmas plus_numeral_code [code func] =
-  add_bin_simps
-  arith_extra_simps(1) [where 'a = int]
-
-lemmas minus_numeral_code [code func] =
-  minus_bin_simps
-  arith_extra_simps(2) [where 'a = int]
-  arith_extra_simps(5) [where 'a = int]
-
-lemmas times_numeral_code [code func] =
-  mult_bin_simps
-  arith_extra_simps(4) [where 'a = int]
-
-lemmas eq_numeral_code [code func] =
-  eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1
-  eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
-  eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min
-  eq_Bit0_Bit0 eq_Bit0_Bit1 eq_Bit1_Bit0 eq_Bit1_Bit1
-  eq_number_of
-
-lemmas less_eq_numeral_code [code func] =
-  less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit0 less_eq_Pls_Bit1
-  less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
-  less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit0_Min less_eq_Bit1_Min
-  less_eq_Bit0_Bit0 less_eq_Bit0_Bit1 less_eq_Bit1_Bit0 less_eq_Bit1_Bit1
-  less_eq_number_of
-
-lemmas less_numeral_code [code func] =
-  less_Pls_Pls less_Pls_Min less_Pls_Bit0 less_Pls_Bit1
-  less_Min_Pls less_Min_Min less_Min_Bit0 less_Min_Bit1
-  less_Bit0_Pls less_Bit1_Pls less_Bit0_Min less_Bit1_Min
-  less_Bit0_Bit0 less_Bit0_Bit1 less_Bit1_Bit0 less_Bit1_Bit1
-  less_number_of
-
-context ring_1
-begin
-
-lemma of_int_num [code func]:
-  "of_int k = (if k = 0 then 0 else if k < 0 then
-     - of_int (- k) else let
-       (l, m) = divAlg (k, 2);
-       l' = of_int l
-     in if m = 0 then l' + l' else l' + l' + 1)"
-proof -
-  have aux1: "k mod (2\<Colon>int) \<noteq> (0\<Colon>int) \<Longrightarrow> 
-    of_int k = of_int (k div 2 * 2 + 1)"
-  proof -
-    assume "k mod 2 \<noteq> 0"
-    then have "k mod 2 = 1" by arith
-    moreover have "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
-    ultimately show ?thesis by auto
-  qed
-  have aux2: "\<And>x. of_int 2 * x = x + x"
-  proof -
-    fix x
-    have int2: "(2::int) = 1 + 1" by arith
-    show "of_int 2 * x = x + x"
-    unfolding int2 of_int_add left_distrib by simp
-  qed
-  have aux3: "\<And>x. x * of_int 2 = x + x"
-  proof -
-    fix x
-    have int2: "(2::int) = 1 + 1" by arith
-    show "x * of_int 2 = x + x" 
-    unfolding int2 of_int_add right_distrib by simp
-  qed
-  from aux1 show ?thesis by (auto simp add: divAlg_mod_div Let_def aux2 aux3)
-qed
-
 end
-
-end