src/HOL/Library/Cancellation.thy
 author wenzelm Tue May 15 13:57:39 2018 +0200 (16 months ago) changeset 68189 6163c90694ef parent 67399 eab6ce8368fa child 69605 a96320074298 permissions -rw-r--r--
```     1 (*  Title:      HOL/Library/Cancellation.thy
```
```     2     Author:     Mathias Fleury, MPII
```
```     3     Copyright   2017
```
```     4
```
```     5 This theory defines cancelation simprocs that work on cancel_comm_monoid_add and support the simplification of an operation
```
```     6 that repeats the additions.
```
```     7 *)
```
```     8
```
```     9 theory Cancellation
```
```    10 imports Main
```
```    11 begin
```
```    12
```
```    13 named_theorems cancelation_simproc_pre \<open>These theorems are here to normalise the term. Special
```
```    14   handling of constructors should be here. Remark that only the simproc @{term NO_MATCH} is also
```
```    15   included.\<close>
```
```    16
```
```    17 named_theorems cancelation_simproc_post \<open>These theorems are here to normalise the term, after the
```
```    18   cancelation simproc. Normalisation of \<open>iterate_add\<close> back to the normale representation
```
```    19   should be put here.\<close>
```
```    20
```
```    21 named_theorems cancelation_simproc_eq_elim \<open>These theorems are here to help deriving contradiction
```
```    22   (e.g., \<open>Suc _ = 0\<close>).\<close>
```
```    23
```
```    24 definition iterate_add :: \<open>nat \<Rightarrow> 'a::cancel_comm_monoid_add \<Rightarrow> 'a\<close> where
```
```    25   \<open>iterate_add n a = (((+) a) ^^ n) 0\<close>
```
```    26
```
```    27 lemma iterate_add_simps[simp]:
```
```    28   \<open>iterate_add 0 a = 0\<close>
```
```    29   \<open>iterate_add (Suc n) a = a + iterate_add n a\<close>
```
```    30   unfolding iterate_add_def by auto
```
```    31
```
```    32 lemma iterate_add_empty[simp]: \<open>iterate_add n 0 = 0\<close>
```
```    33   unfolding iterate_add_def by (induction n) auto
```
```    34
```
```    35 lemma iterate_add_distrib[simp]: \<open>iterate_add (m+n) a = iterate_add m a + iterate_add n a\<close>
```
```    36   by (induction n) (auto simp: ac_simps)
```
```    37
```
```    38 lemma iterate_add_Numeral1: \<open>iterate_add n Numeral1 = of_nat n\<close>
```
```    39   by (induction n) auto
```
```    40
```
```    41 lemma iterate_add_1: \<open>iterate_add n 1 = of_nat n\<close>
```
```    42   using iterate_add_Numeral1 by auto
```
```    43
```
```    44 lemma iterate_add_eq_add_iff1:
```
```    45   \<open>i \<le> j \<Longrightarrow> (iterate_add j u + m = iterate_add i u + n) = (iterate_add (j - i) u + m = n)\<close>
```
```    46   by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
```
```    47
```
```    48 lemma iterate_add_eq_add_iff2:
```
```    49    \<open>i \<le> j \<Longrightarrow> (iterate_add i u + m = iterate_add j u + n) = (m = iterate_add (j - i) u + n)\<close>
```
```    50   by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
```
```    51
```
```    52 lemma iterate_add_less_iff1:
```
```    53   "j \<le> (i::nat) \<Longrightarrow> (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)"
```
```    54   by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
```
```    55
```
```    56 lemma iterate_add_less_iff2:
```
```    57   "i \<le> (j::nat) \<Longrightarrow> (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)"
```
```    58   by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
```
```    59
```
```    60 lemma iterate_add_less_eq_iff1:
```
```    61   "j \<le> (i::nat) \<Longrightarrow> (iterate_add i (u:: 'a :: {cancel_comm_monoid_add, ordered_ab_semigroup_add_imp_le}) + m \<le> iterate_add j u + n) = (iterate_add (i-j) u + m \<le> n)"
```
```    62   by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
```
```    63
```
```    64 lemma iterate_add_less_eq_iff2:
```
```    65   "i \<le> (j::nat) \<Longrightarrow> (iterate_add i (u:: 'a :: {cancel_comm_monoid_add, ordered_ab_semigroup_add_imp_le}) + m \<le> iterate_add j u + n) = (m \<le> iterate_add (j - i) u + n)"
```
```    66   by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
```
```    67
```
```    68 lemma iterate_add_add_eq1:
```
```    69   "j \<le> (i::nat) \<Longrightarrow> ((iterate_add i u + m) - (iterate_add j u + n)) = ((iterate_add (i-j) u + m) - n)"
```
```    70   by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
```
```    71
```
```    72 lemma iterate_add_diff_add_eq2:
```
```    73   "i \<le> (j::nat) \<Longrightarrow> ((iterate_add i u + m) - (iterate_add j u + n)) = (m - (iterate_add (j-i) u + n))"
```
```    74   by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
```
```    75
```
```    76
```
```    77 subsection \<open>Simproc Set-Up\<close>
```
```    78
```
```    79 ML_file "Cancellation/cancel.ML"
```
```    80 ML_file "Cancellation/cancel_data.ML"
```
```    81 ML_file "Cancellation/cancel_simprocs.ML"
```
```    82
```
```    83 end
```
```    84
```