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