src/HOL/Library/Extended_Nat.thy
changeset 45775 6c340de26a0d
parent 45539 787a1a097465
child 45934 9321cd2572fe
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Wed Dec 07 11:24:45 2011 +0100
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Wed Dec 07 10:50:30 2011 +0100
     1.3 @@ -489,6 +489,78 @@
     1.4  qed
     1.5  
     1.6  
     1.7 +subsection {* Cancellation simprocs *}
     1.8 +
     1.9 +lemma enat_add_left_cancel: "a + b = a + c \<longleftrightarrow> a = (\<infinity>::enat) \<or> b = c"
    1.10 +  unfolding plus_enat_def by (simp split: enat.split)
    1.11 +
    1.12 +lemma enat_add_left_cancel_le: "a + b \<le> a + c \<longleftrightarrow> a = (\<infinity>::enat) \<or> b \<le> c"
    1.13 +  unfolding plus_enat_def by (simp split: enat.split)
    1.14 +
    1.15 +lemma enat_add_left_cancel_less: "a + b < a + c \<longleftrightarrow> a \<noteq> (\<infinity>::enat) \<and> b < c"
    1.16 +  unfolding plus_enat_def by (simp split: enat.split)
    1.17 +
    1.18 +ML {*
    1.19 +structure Cancel_Enat_Common =
    1.20 +struct
    1.21 +  (* copied from src/HOL/Tools/nat_numeral_simprocs.ML *)
    1.22 +  fun find_first_t _    _ []         = raise TERM("find_first_t", [])
    1.23 +    | find_first_t past u (t::terms) =
    1.24 +          if u aconv t then (rev past @ terms)
    1.25 +          else find_first_t (t::past) u terms
    1.26 +
    1.27 +  val mk_sum = Arith_Data.long_mk_sum
    1.28 +  val dest_sum = Arith_Data.dest_sum
    1.29 +  val find_first = find_first_t []
    1.30 +  val trans_tac = Numeral_Simprocs.trans_tac
    1.31 +  val norm_ss = HOL_basic_ss addsimps
    1.32 +    @{thms add_ac semiring_numeral_0_eq_0 add_0_left add_0_right}
    1.33 +  fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
    1.34 +  fun simplify_meta_eq ss cancel_th th =
    1.35 +    Arith_Data.simplify_meta_eq @{thms semiring_numeral_0_eq_0} ss
    1.36 +      ([th, cancel_th] MRS trans)
    1.37 +  fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
    1.38 +end
    1.39 +
    1.40 +structure Eq_Enat_Cancel = ExtractCommonTermFun
    1.41 +(open Cancel_Enat_Common
    1.42 +  val mk_bal = HOLogic.mk_eq
    1.43 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} @{typ enat}
    1.44 +  fun simp_conv _ _ = SOME @{thm enat_add_left_cancel}
    1.45 +)
    1.46 +
    1.47 +structure Le_Enat_Cancel = ExtractCommonTermFun
    1.48 +(open Cancel_Enat_Common
    1.49 +  val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}
    1.50 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} @{typ enat}
    1.51 +  fun simp_conv _ _ = SOME @{thm enat_add_left_cancel_le}
    1.52 +)
    1.53 +
    1.54 +structure Less_Enat_Cancel = ExtractCommonTermFun
    1.55 +(open Cancel_Enat_Common
    1.56 +  val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}
    1.57 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} @{typ enat}
    1.58 +  fun simp_conv _ _ = SOME @{thm enat_add_left_cancel_less}
    1.59 +)
    1.60 +*}
    1.61 +
    1.62 +simproc_setup enat_eq_cancel
    1.63 +  ("(l::enat) + m = n" | "(l::enat) = m + n") =
    1.64 +  {* fn phi => fn ss => fn ct => Eq_Enat_Cancel.proc ss (term_of ct) *}
    1.65 +
    1.66 +simproc_setup enat_le_cancel
    1.67 +  ("(l::enat) + m \<le> n" | "(l::enat) \<le> m + n") =
    1.68 +  {* fn phi => fn ss => fn ct => Le_Enat_Cancel.proc ss (term_of ct) *}
    1.69 +
    1.70 +simproc_setup enat_less_cancel
    1.71 +  ("(l::enat) + m < n" | "(l::enat) < m + n") =
    1.72 +  {* fn phi => fn ss => fn ct => Less_Enat_Cancel.proc ss (term_of ct) *}
    1.73 +
    1.74 +text {* TODO: add regression tests for these simprocs *}
    1.75 +
    1.76 +text {* TODO: add simprocs for combining and cancelling numerals *}
    1.77 +
    1.78 +
    1.79  subsection {* Well-ordering *}
    1.80  
    1.81  lemma less_enatE: