<commit_before>(*  Title:      HOL/Parity.thy
    Author:     <NAME>
    Author:     <NAME>
*)

header {* Even and Odd for int and nat *}

theory Parity
imports Main
begin

class even_odd = 
  fixes even :: "'a \<Rightarrow> bool"

abbreviation
  odd :: "'a\<Colon>even_odd \<Rightarrow> bool" where
  "odd x \<equiv> \<not> even x"

instantiation nat and int  :: even_odd
begin

definition
  even_def [presburger]: "even x \<longleftrightarrow> (x\<Colon>int) mod 2 = 0"

definition
  even_nat_def [presburger]: "even x \<longleftrightarrow> even (int x)"

instance ..

end

lemma transfer_int_nat_relations:
  "even (int x) \<longleftrightarrow> even x"
  by (simp add: even_nat_def)

declare transfer_morphism_int_nat[transfer add return:
  transfer_int_nat_relations
]

lemma even_zero_int[simp]: "even (0::int)" by presburger

lemma odd_one_int[simp]: "odd (1::int)" by presburger

lemma even_zero_nat[simp]: "even (0::nat)" by presburger

lemma odd_1_nat [simp]: "odd (1::nat)" by presburger

(* TODO: proper simp rules for Num.Bit0, Num.Bit1 *)
declare even_def[of "numeral v", simp] for v
declare even_def[of "neg_numeral v", simp] for v

declare even_nat_def[of "numeral v", simp] for v

subsection {* Even and odd are mutually exclusive *}

lemma int_pos_lt_two_imp_zero_or_one:
    "0 <= x ==> (x::int) < 2 ==> x = 0 | x = 1"
  by presburger

lemma neq_one_mod_two [simp, presburger]: <commit_msg>add simp rules for eve/odd on numerals<commit_after>(*  Title:      HOL/Parity.thy
    Author:     <NAME>
    Author:     <NAME>
*)

header {* Even and Odd for int and nat *}

theory Parity
imports Main
begin

class even_odd = 
  fixes even :: "'a \<Rightarrow> bool"

abbreviation
  odd :: "'a\<Colon>even_odd \<Rightarrow> bool" where
  "odd x \<equiv> \<not> even x"

instantiation nat and int  :: even_odd
begin

definition
  even_def [presburger]: "even x \<longleftrightarrow> (x\<Colon>int) mod 2 = 0"

definition
  even_nat_def [presburger]: "even x \<longleftrightarrow> even (int x)"

instance ..

end

lemma transfer_int_nat_relations:
  "even (int x) \<longleftrightarrow> even x"
  by (simp add: even_nat_def)

declare transfer_morphism_int_nat[transfer add return:
  transfer_int_nat_relations
]

lemma even_zero_int[simp]: "even (0::int)" by presburger

lemma odd_one_int[simp]: "odd (1::int)" by presburger

lemma even_zero_nat[simp]: "even (0::nat)" by presburger

lemma odd_1_nat [simp]: "odd (1::nat)" by presburger

lemma even_numeral_int [simp]: "even (numeral (Num.Bit0 k) :: int)"
  unfolding even_def by simp

lemma odd_numeral_int [simp]: "odd (numeral (Num.Bit1 k) :: int)"
  unfolding even_def by simp

(* TODO: proper simp rules for Num.Bit0, Num.Bit1 *)
declare even_def[of "neg_numeral v", simp] for v

lemma even_numeral_nat [simp]: "even (numeral (Num.Bit0 k) :: nat)"
  unfolding even_nat_def by simp

lemma odd_numeral_nat [simp]: "odd (numeral (Num.Bit1 k) :: nat)"
  unfolding even_nat_def by simp

subsection {* Even and odd are mutually exclusive *}

lemma int_pos_lt_two_imp_zero_or_one:
    "0 <= x ==> (x::int) < 2 ==> x = 0 | x = 1"
  by presburger

lemma neq_one_mod_two [simp, presburger]: 
{'fraction_non_alphanumeric': 0.12444302991725016, 'fraction_numerical': 0.009548058561425843, 'mean_word_length': 4.391080617495712, 'pattern_counts': {'":': 0, '<': 29, '<?xml version=': 0, '>': 29, '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': '7276231', 'n_tokens_mistral': 1246, 'n_tokens_neox': 1174, 'n_words': 358}