# 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 \ True" by presburger - -lemma eq_Pls_Min: - "Int.Pls = Int.Min \ False" - unfolding Pls_def Int.Min_def by presburger - -lemma eq_Pls_Bit0: - "Int.Pls = Int.Bit0 k \ Int.Pls = k" - unfolding Pls_def Bit0_def by presburger - -lemma eq_Pls_Bit1: - "Int.Pls = Int.Bit1 k \ False" - unfolding Pls_def Bit1_def by presburger - -lemma eq_Min_Pls: - "Int.Min = Int.Pls \ False" - unfolding Pls_def Int.Min_def by presburger - -lemma eq_Min_Min: - "Int.Min = Int.Min \ True" by presburger - -lemma eq_Min_Bit0: - "Int.Min = Int.Bit0 k \ False" - unfolding Int.Min_def Bit0_def by presburger - -lemma eq_Min_Bit1: - "Int.Min = Int.Bit1 k \ Int.Min = k" - unfolding Int.Min_def Bit1_def by presburger - -lemma eq_Bit0_Pls: - "Int.Bit0 k = Int.Pls \ Int.Pls = k" - unfolding Pls_def Bit0_def by presburger - -lemma eq_Bit1_Pls: - "Int.Bit1 k = Int.Pls \ False" - unfolding Pls_def Bit1_def by presburger - -lemma eq_Bit0_Min: - "Int.Bit0 k = Int.Min \ False" - unfolding Int.Min_def Bit0_def by presburger - -lemma eq_Bit1_Min: - "Int.Bit1 k = Int.Min \ Int.Min = k" - unfolding Int.Min_def Bit1_def by presburger - -lemma eq_Bit0_Bit0: - "Int.Bit0 k1 = Int.Bit0 k2 \ k1 = k2" - unfolding Bit0_def by presburger - -lemma eq_Bit0_Bit1: - "Int.Bit0 k1 = Int.Bit1 k2 \ False" - unfolding Bit0_def Bit1_def by presburger - -lemma eq_Bit1_Bit0: - "Int.Bit1 k1 = Int.Bit0 k2 \ False" - unfolding Bit0_def Bit1_def by presburger - -lemma eq_Bit1_Bit1: - "Int.Bit1 k1 = Int.Bit1 k2 \ k1 = k2" - unfolding Bit1_def by presburger - -lemma eq_number_of: - "(number_of k \ int) = number_of l \ k = l" - unfolding number_of_is_id .. - - -lemma less_eq_Pls_Pls: - "Int.Pls \ Int.Pls \ True" by rule+ - -lemma less_eq_Pls_Min: - "Int.Pls \ Int.Min \ False" - unfolding Pls_def Int.Min_def by presburger - -lemma less_eq_Pls_Bit0: - "Int.Pls \ Int.Bit0 k \ Int.Pls \ k" - unfolding Pls_def Bit0_def by auto - -lemma less_eq_Pls_Bit1: - "Int.Pls \ Int.Bit1 k \ Int.Pls \ k" - unfolding Pls_def Bit1_def by auto - -lemma less_eq_Min_Pls: - "Int.Min \ Int.Pls \ True" - unfolding Pls_def Int.Min_def by presburger - -lemma less_eq_Min_Min: - "Int.Min \ Int.Min \ True" by rule+ - -lemma less_eq_Min_Bit0: - "Int.Min \ Int.Bit0 k \ Int.Min < k" - unfolding Int.Min_def Bit0_def by auto - -lemma less_eq_Min_Bit1: - "Int.Min \ Int.Bit1 k \ Int.Min \ k" - unfolding Int.Min_def Bit1_def by auto - -lemma less_eq_Bit0_Pls: - "Int.Bit0 k \ Int.Pls \ k \ Int.Pls" - unfolding Pls_def Bit0_def by simp - -lemma less_eq_Bit1_Pls: - "Int.Bit1 k \ Int.Pls \ k < Int.Pls" - unfolding Pls_def Bit1_def by auto - -lemma less_eq_Bit0_Min: - "Int.Bit0 k \ Int.Min \ k \ Int.Min" - unfolding Int.Min_def Bit0_def by auto - -lemma less_eq_Bit1_Min: - "Int.Bit1 k \ Int.Min \ k \ Int.Min" - unfolding Int.Min_def Bit1_def by auto - -lemma less_eq_Bit0_Bit0: - "Int.Bit0 k1 \ Int.Bit0 k2 \ k1 \ k2" - unfolding Bit0_def by auto - -lemma less_eq_Bit0_Bit1: - "Int.Bit0 k1 \ Int.Bit1 k2 \ k1 \ k2" - unfolding Bit0_def Bit1_def by auto - -lemma less_eq_Bit1_Bit0: - "Int.Bit1 k1 \ Int.Bit0 k2 \ k1 < k2" - unfolding Bit0_def Bit1_def by auto - -lemma less_eq_Bit1_Bit1: - "Int.Bit1 k1 \ Int.Bit1 k2 \ k1 \ k2" - unfolding Bit1_def by auto - -lemma less_eq_number_of: - "(number_of k \ int) \ number_of l \ k \ l" - unfolding number_of_is_id .. - - -lemma less_Pls_Pls: - "Int.Pls < Int.Pls \ False" by simp - -lemma less_Pls_Min: - "Int.Pls < Int.Min \ False" - unfolding Pls_def Int.Min_def by presburger - -lemma less_Pls_Bit0: - "Int.Pls < Int.Bit0 k \ Int.Pls < k" - unfolding Pls_def Bit0_def by auto - -lemma less_Pls_Bit1: - "Int.Pls < Int.Bit1 k \ Int.Pls \ k" - unfolding Pls_def Bit1_def by auto - -lemma less_Min_Pls: - "Int.Min < Int.Pls \ True" - unfolding Pls_def Int.Min_def by presburger - -lemma less_Min_Min: - "Int.Min < Int.Min \ False" by simp - -lemma less_Min_Bit0: - "Int.Min < Int.Bit0 k \ Int.Min < k" - unfolding Int.Min_def Bit0_def by auto - -lemma less_Min_Bit1: - "Int.Min < Int.Bit1 k \ Int.Min < k" - unfolding Int.Min_def Bit1_def by auto - -lemma less_Bit0_Pls: - "Int.Bit0 k < Int.Pls \ k < Int.Pls" - unfolding Pls_def Bit0_def by auto - -lemma less_Bit1_Pls: - "Int.Bit1 k < Int.Pls \ k < Int.Pls" - unfolding Pls_def Bit1_def by auto - -lemma less_Bit0_Min: - "Int.Bit0 k < Int.Min \ k \ Int.Min" - unfolding Int.Min_def Bit0_def by auto - -lemma less_Bit1_Min: - "Int.Bit1 k < Int.Min \ k < Int.Min" - unfolding Int.Min_def Bit1_def by auto - -lemma less_Bit0_Bit0: - "Int.Bit0 k1 < Int.Bit0 k2 \ k1 < k2" - unfolding Bit0_def by auto - -lemma less_Bit0_Bit1: - "Int.Bit0 k1 < Int.Bit1 k2 \ k1 \ k2" - unfolding Bit0_def Bit1_def by auto - -lemma less_Bit1_Bit0: - "Int.Bit1 k1 < Int.Bit0 k2 \ k1 < k2" - unfolding Bit0_def Bit1_def by auto - -lemma less_Bit1_Bit1: - "Int.Bit1 k1 < Int.Bit1 k2 \ k1 < k2" - unfolding Bit1_def by auto - -lemma less_number_of: - "(number_of k \ int) < number_of l \ 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\int) \ (0\int) \ - of_int k = of_int (k div 2 * 2 + 1)" - proof - - assume "k mod 2 \ 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: "\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: "\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