Theory HOL-Library.Cancellation
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›).›
definition iterate_add :: ‹nat ⇒ 'a::cancel_comm_monoid_add ⇒ 'a› where
‹iterate_add n a = (((+) a) ^^ n) 0›
lemma iterate_add_simps[simp]:
‹iterate_add 0 a = 0›
‹iterate_add (Suc n) a = a + iterate_add n a›
unfolding iterate_add_def by auto
lemma iterate_add_empty[simp]: ‹iterate_add n 0 = 0›
unfolding iterate_add_def by (induction n) auto
lemma iterate_add_distrib[simp]: ‹iterate_add (m+n) a = iterate_add m a + iterate_add n a›
by (induction n) (auto simp: ac_simps)
lemma iterate_add_Numeral1: ‹iterate_add n Numeral1 = of_nat n›
by (induction n) auto
lemma iterate_add_1: ‹iterate_add n 1 = of_nat n›
using iterate_add_Numeral1 by auto
lemma iterate_add_eq_add_iff1:
‹i ≤ j ⟹ (iterate_add j u + m = iterate_add i u + n) = (iterate_add (j - i) u + m = n)›
by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
lemma iterate_add_eq_add_iff2:
‹i ≤ j ⟹ (iterate_add i u + m = iterate_add j u + n) = (m = iterate_add (j - i) u + n)›
by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
lemma iterate_add_less_iff1:
"j ≤ (i::nat) ⟹ (iterate_add i (u:: 'a :: {cancel_comm_monoid_add, ordered_ab_semigroup_add_imp_le}) + m < iterate_add j u + n) = (iterate_add (i-j) u + m < n)"
by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
lemma iterate_add_less_iff2:
"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)"
by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
lemma iterate_add_less_eq_iff1:
"j ≤ (i::nat) ⟹ (iterate_add i (u:: 'a :: {cancel_comm_monoid_add, ordered_ab_semigroup_add_imp_le}) + m ≤ iterate_add j u + n) = (iterate_add (i-j) u + m ≤ n)"
by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
lemma iterate_add_less_eq_iff2:
"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)"
by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
lemma iterate_add_add_eq1:
"j ≤ (i::nat) ⟹ ((iterate_add i u + m) - (iterate_add j u + n)) = ((iterate_add (i-j) u + m) - n)"
by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
lemma iterate_add_diff_add_eq2:
"i ≤ (j::nat) ⟹ ((iterate_add i u + m) - (iterate_add j u + n)) = (m - (iterate_add (j-i) u + n))"
by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
text ‹Simproc Set-Up›
ML_file ‹Cancellation/cancel.ML›
ML_file ‹Cancellation/cancel_data.ML›
ML_file ‹Cancellation/cancel_simprocs.ML›
end