<commit_before>(* 
  ID:      $Id$
  Author:  <NAME>, NICTA
*) 

header {* Useful Numerical Lemmas *}

theory Num_Lemmas
imports Main Parity
begin

datatype bit = B0 | B1

definition
  Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
  [code func del]: "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"

lemma BIT_B0_eq_Bit0 [simp]: "w BIT B0 = Int.Bit0 w"
  unfolding Bit_def Bit0_def by simp

lemma BIT_B1_eq_Bit1 [simp]: "w BIT B1 = Int.Bit1 w"
  unfolding Bit_def Bit1_def by simp

lemmas BIT_simps = BIT_B0_eq_Bit0 BIT_B1_eq_Bit1

hide (open) const B0 B1

lemma contentsI: "y = {x} ==> contents y = x" 
  unfolding contents_def by auto

lemma prod_case_split: "prod_case = split"
  by (rule ext)+ auto
 
lemmas split_split = prod.split [unfolded prod_case_split] 
lemmas split_split_asm = prod.split_asm [unfolded prod_case_split]
lemmas "split.splits" = split_split split_split_asm 

lemmas funpow_0 = funpow.simps(1)
lemmas funpow_Suc = funpow.simps(2)

lemma nonemptyE: "S ~= {} ==> (!!x. x : S ==> R) ==> R"
  apply (erule contrapos_np)
  apply (rule equals0I)
  apply auto
  done

lemma gt_or_eq_0: "0 < y \<or> 0 = (y::nat)" by auto

constdefs
  mod_alt :: "'a => 'a => 'a :: Divides.div"
  "mod_alt n m == n mod m" 

  -- "alternative way of defining @{text bin_last}, @{text bin_rest}"
  bin_rl :: "int => int * bit" 
  "bin_rl w == SOME (r, l). w = r BIT l"

declare iszero_0 [iff]

lemmas xtr1 = xtrans(1)
lemmas xtr2 = xtrans(2)
lemmas xtr3 = xtrans(3)
lemmas xtr4 = xtrans(4)
lemmas xtr5 = xtrans(5)
lemmas xtr6 = xtrans(6)
lemmas xtr7 = xtrans(7)
lemmas xtr8 = xtrans(8)

lemma Min_ne_Pls [iff]:  
  "Int.Min ~= Int.Pls"
  unfolding Min_def Pls_def by auto

lemmas Pls_ne_Min [iff] = Min_ne_Pls [symmetric]

lemmas PlsMin_defs [intro!] = 
  Pls_def Min_def Pls_def [symmetric] Min_def [symmetric]

lemmas PlsMin_simps [simp] = PlsMin_defs [THEN Eq_TrueI]

lemma number_of_False_cong: 
  "False \<Longrightarrow> number_of x = number_of y"
  by (rule FalseE)

lemmas nat_simps = diff_add_inverse2 diff_add_inverse
lemmas nat_iffs = le_add1 le_add2

lemma sum_imp_diff: "j = k + i ==> j - i = (k :: nat)"
  by (clarsimp simp add: nat_simps)

lemma nobm1:
  "0 < (number_of w :: nat) ==> 
   number_of w - (1 :: nat) = number_of (Int.pred w)"
  apply (unfold nat_number_of_def One_nat_def nat_1 [symmetric] pred_def)
  apply (simp add: number_of_eq nat_diff_distrib [symmetric])
  done

lemma of_int_power:
  "of_int (a ^ n) = (of_int a ^ n :: 'a :: {recpower, comm_ring_1})" 
  by (induct n) (auto simp add: power_Suc)

lemma zless2: "0 < (2 :: int)" 
  by auto

lemmas zless2p [simp] = zless2 [THEN zero_less_power]
lemmas zle2p [simp] = zless2p [THEN order_less_imp_le]

lemmas pos_mod_sign2 = zless2 [THEN pos_mod_sign [where b = "2::int"]]
lemmas pos_mod_bound2 = zless2 [THEN pos_mod_bound [where b = "2::int"]]

-- "the inverse(s) of @{text number_of}"
lemma nmod2: "n mod (2::int) = 0 | n mod 2 = 1"
  using pos_mod_sign2 [of n] pos_mod_bound2 [of n]
  unfolding mod_alt_def [symmetric] by auto

lemma emep1:
  "even n ==> even d ==> 0 <= d ==> (n + 1) mod (d :: int) = (n mod d) + 1"
  apply (simp add: add_commute)
  apply (safe dest!: even_equiv_def [THEN iffD1])
  apply (subst pos_zmod_mult_2)
   apply arith
  apply (simp add: zmod_zmult_zmult1)
 done

lemmas eme1p = emep1 [simplified add_commute]

lemma le_diff_eq': "(a \<le> c - b) = (b + a \<le> (c::int))"
  by (simp add: le_diff_eq add_commute)

lemma less_diff_eq': "(a < c - b) = (b + a < (c::int))"
  by (simp add: less_diff_eq add_commute)

lemma diff_le_eq': "(a - b \<le> c) = (a \<le> b + (c::int))"
  by (simp add: diff_le_eq add_commute)

lemma diff_less_eq': "(a - b < c) = (a < b + (c::int))"
  by (simp add: diff_less_eq add_commute)


lemmas m1mod2k = zless2p [THEN zmod_minus1]<commit_msg>remove unneeded constant mod_alt<commit_after>(* 
  ID:      $Id$
  Author:  <NAME>, NICTA
*) 

header {* Useful Numerical Lemmas *}

theory Num_Lemmas
imports Main Parity
begin

datatype bit = B0 | B1

definition
  Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
  [code func del]: "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"

lemma BIT_B0_eq_Bit0 [simp]: "w BIT B0 = Int.Bit0 w"
  unfolding Bit_def Bit0_def by simp

lemma BIT_B1_eq_Bit1 [simp]: "w BIT B1 = Int.Bit1 w"
  unfolding Bit_def Bit1_def by simp

lemmas BIT_simps = BIT_B0_eq_Bit0 BIT_B1_eq_Bit1

hide (open) const B0 B1

lemma contentsI: "y = {x} ==> contents y = x" 
  unfolding contents_def by auto

lemma prod_case_split: "prod_case = split"
  by (rule ext)+ auto
 
lemmas split_split = prod.split [unfolded prod_case_split] 
lemmas split_split_asm = prod.split_asm [unfolded prod_case_split]
lemmas "split.splits" = split_split split_split_asm 

lemmas funpow_0 = funpow.simps(1)
lemmas funpow_Suc = funpow.simps(2)

lemma nonemptyE: "S ~= {} ==> (!!x. x : S ==> R) ==> R"
  apply (erule contrapos_np)
  apply (rule equals0I)
  apply auto
  done

lemma gt_or_eq_0: "0 < y \<or> 0 = (y::nat)" by auto

constdefs
  -- "alternative way of defining @{text bin_last}, @{text bin_rest}"
  bin_rl :: "int => int * bit" 
  "bin_rl w == SOME (r, l). w = r BIT l"

declare iszero_0 [iff]

lemmas xtr1 = xtrans(1)
lemmas xtr2 = xtrans(2)
lemmas xtr3 = xtrans(3)
lemmas xtr4 = xtrans(4)
lemmas xtr5 = xtrans(5)
lemmas xtr6 = xtrans(6)
lemmas xtr7 = xtrans(7)
lemmas xtr8 = xtrans(8)

lemma Min_ne_Pls [iff]:  
  "Int.Min ~= Int.Pls"
  unfolding Min_def Pls_def by auto

lemmas Pls_ne_Min [iff] = Min_ne_Pls [symmetric]

lemmas PlsMin_defs [intro!] = 
  Pls_def Min_def Pls_def [symmetric] Min_def [symmetric]

lemmas PlsMin_simps [simp] = PlsMin_defs [THEN Eq_TrueI]

lemma number_of_False_cong: 
  "False \<Longrightarrow> number_of x = number_of y"
  by (rule FalseE)

lemmas nat_simps = diff_add_inverse2 diff_add_inverse
lemmas nat_iffs = le_add1 le_add2

lemma sum_imp_diff: "j = k + i ==> j - i = (k :: nat)"
  by (clarsimp simp add: nat_simps)

lemma nobm1:
  "0 < (number_of w :: nat) ==> 
   number_of w - (1 :: nat) = number_of (Int.pred w)"
  apply (unfold nat_number_of_def One_nat_def nat_1 [symmetric] pred_def)
  apply (simp add: number_of_eq nat_diff_distrib [symmetric])
  done

lemma of_int_power:
  "of_int (a ^ n) = (of_int a ^ n :: 'a :: {recpower, comm_ring_1})" 
  by (induct n) (auto simp add: power_Suc)

lemma zless2: "0 < (2 :: int)" 
  by auto

lemmas zless2p [simp] = zless2 [THEN zero_less_power]
lemmas zle2p [simp] = zless2p [THEN order_less_imp_le]

lemmas pos_mod_sign2 = zless2 [THEN pos_mod_sign [where b = "2::int"]]
lemmas pos_mod_bound2 = zless2 [THEN pos_mod_bound [where b = "2::int"]]

-- "the inverse(s) of @{text number_of}"
lemma nmod2: "n mod (2::int) = 0 | n mod 2 = 1"
  by (cases "n mod 2 = 0", simp_all)

lemma emep1:
  "even n ==> even d ==> 0 <= d ==> (n + 1) mod (d :: int) = (n mod d) + 1"
  apply (simp add: add_commute)
  apply (safe dest!: even_equiv_def [THEN iffD1])
  apply (subst pos_zmod_mult_2)
   apply arith
  apply (simp add: zmod_zmult_zmult1)
 done

lemmas eme1p = emep1 [simplified add_commute]

lemma le_diff_eq': "(a \<le> c - b) = (b + a \<le> (c::int))"
  by (simp add: le_diff_eq add_commute)

lemma less_diff_eq': "(a < c - b) = (b + a < (c::int))"
  by (simp add: less_diff_eq add_commute)

lemma diff_le_eq': "(a - b \<le> c) = (a \<le> b + (c::int))"
  by (simp add: diff_le_eq add_commute)

lemma diff_less_eq': "(a - b < c) = (a < b + (c::int))"
  by (simp add: diff_less_eq add_commute)


lemmas m1mod2k = zless2p [THEN zmod_minus1]
{'fraction_non_alphanumeric': 0.1344448855365886, 'fraction_numerical': 0.023554320497551937, 'mean_word_length': 3.9690992767915847, 'pattern_counts': {'":': 0, '<': 41, '<?xml version=': 0, '>': 47, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3280230', 'n_tokens_mistral': 3345, 'n_tokens_neox': 3297, 'n_words': 948}