<commit_before>(*  Title:      HOL/Integ/IntArith.thy
    ID:         $Id$
    Authors:    <NAME> and <NAME>
*)

header {* Integer arithmetic *}

theory IntArith
imports Numeral "../Wellfounded_Relations"
uses "~~/src/Provers/Arith/assoc_fold.ML" ("int_arith1.ML")
begin

text{*Duplicate: can't understand why it's necessary*}
declare numeral_0_eq_0 [simp]


subsection{*Inequality Reasoning for the Arithmetic Simproc*}

lemma add_numeral_0: "Numeral0 + a = (a::'a::number_ring)"
by simp 

lemma add_numeral_0_right: "a + Numeral0 = (a::'a::number_ring)"
by simp

lemma mult_numeral_1: "Numeral1 * a = (a::'a::number_ring)"
by simp 

lemma mult_numeral_1_right: "a * Numeral1 = (a::'a::number_ring)"
by simp

text{*Theorem lists for the cancellation simprocs. The use of binary numerals
for 0 and 1 reduces the number of special cases.*}

lemmas add_0s = add_numeral_0 add_numeral_0_right
lemmas mult_1s = mult_numeral_1 mult_numeral_1_right 
                 mult_minus1 mult_minus1_right
<commit_msg>add lemmas divide_numeral_1 and inverse_numeral_1<commit_after>(*  Title:      HOL/Integ/IntArith.thy
    ID:         $Id$
    Authors:    <NAME> and <NAME>
*)

header {* Integer arithmetic *}

theory IntArith
imports Numeral "../Wellfounded_Relations"
uses "~~/src/Provers/Arith/assoc_fold.ML" ("int_arith1.ML")
begin

text{*Duplicate: can't understand why it's necessary*}
declare numeral_0_eq_0 [simp]


subsection{*Inequality Reasoning for the Arithmetic Simproc*}

lemma add_numeral_0: "Numeral0 + a = (a::'a::number_ring)"
by simp 

lemma add_numeral_0_right: "a + Numeral0 = (a::'a::number_ring)"
by simp

lemma mult_numeral_1: "Numeral1 * a = (a::'a::number_ring)"
by simp 

lemma mult_numeral_1_right: "a * Numeral1 = (a::'a::number_ring)"
by simp

lemma divide_numeral_1: "a / Numeral1 = (a::'a::{number_ring,field})"
by simp

lemma inverse_numeral_1:
  "inverse Numeral1 = (Numeral1::'a::{number_ring,field})"
by simp

text{*Theorem lists for the cancellation simprocs. The use of binary numerals
for 0 and 1 reduces the number of special cases.*}

lemmas add_0s = add_numeral_0 add_numeral_0_right
lemmas mult_1s = mult_numeral_1 mult_numeral_1_right 
                 mult_minus1 mult_minus1_right

{'fraction_non_alphanumeric': 0.11336946702800361, 'fraction_numerical': 0.022131887985546522, 'mean_word_length': 4.783289817232376, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 7, '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': '4793053', 'n_tokens_mistral': 874, 'n_tokens_neox': 828, 'n_words': 208}