# Theory Cancellation

theory Cancellation
imports Main
```(*  Title:      HOL/Library/Cancellation.thy
Author:     Mathias Fleury, MPII

This theory defines cancelation simprocs that work on cancel_comm_monoid_add and support the simplification of an operation
*)

theory Cancellation
imports Main
begin

named_theorems cancelation_simproc_pre ‹These theorems are here to normalise the term. Special
handling of constructors should be here. Remark that only the simproc @{term NO_MATCH} is also
included.›

named_theorems cancelation_simproc_post ‹These theorems are here to normalise the term, after the
cancelation simproc. Normalisation of ‹iterate_add› back to the normale representation
should be put here.›

named_theorems cancelation_simproc_eq_elim ‹These theorems are here to help deriving contradiction
(e.g., ‹Suc _ = 0›).›

‹iterate_add n a = (((+) a) ^^ n) 0›

unfolding iterate_add_def by (induction n) auto

by (induction n) (auto simp: ac_simps)

by (induction n) auto

‹i ≤ j ⟹ (iterate_add j u + m = iterate_add i u + n) = (iterate_add (j - i) u + m = n)›

‹i ≤ j ⟹ (iterate_add i u + m = iterate_add j u + n) = (m = iterate_add (j - i) u + n)›

"i ≤ (j::nat) ⟹ (iterate_add i (u:: 'a :: {cancel_comm_monoid_add, ordered_ab_semigroup_add_imp_le}) + m < iterate_add j u + n) = (m <iterate_add (j - i) u + n)"

"i ≤ (j::nat) ⟹ (iterate_add i (u:: 'a :: {cancel_comm_monoid_add, ordered_ab_semigroup_add_imp_le}) + m ≤ iterate_add j u + n) = (m ≤ iterate_add (j - i) u + n)"

"j ≤ (i::nat) ⟹ ((iterate_add i u + m) - (iterate_add j u + n)) = ((iterate_add (i-j) u + m) - n)"