type class for confined subtraction
authorhaftmann
Sun Jun 02 20:44:55 2013 +0200 (2013-06-02)
changeset 5228983ce5d2841e7
parent 52288 ca4932dad084
child 52290 9be30aa5a39b
type class for confined subtraction
src/HOL/Groups.thy
src/HOL/Library/Multiset.thy
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Groups.thy	Sun Jun 02 10:57:21 2013 +0200
     1.2 +++ b/src/HOL/Groups.thy	Sun Jun 02 20:44:55 2013 +0200
     1.3 @@ -658,6 +658,68 @@
     1.4  
     1.5  end
     1.6  
     1.7 +class ordered_cancel_comm_monoid_diff = comm_monoid_diff + ordered_ab_semigroup_add_imp_le +
     1.8 +  assumes le_iff_add: "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)"
     1.9 +begin
    1.10 +
    1.11 +context
    1.12 +  fixes a b
    1.13 +  assumes "a \<le> b"
    1.14 +begin
    1.15 +
    1.16 +lemma add_diff_inverse:
    1.17 +  "a + (b - a) = b"
    1.18 +  using `a \<le> b` by (auto simp add: le_iff_add)
    1.19 +
    1.20 +lemma add_diff_assoc:
    1.21 +  "c + (b - a) = c + b - a"
    1.22 +  using `a \<le> b` by (auto simp add: le_iff_add add_left_commute [of c])
    1.23 +
    1.24 +lemma add_diff_assoc2:
    1.25 +  "b - a + c = b + c - a"
    1.26 +  using `a \<le> b` by (auto simp add: le_iff_add add_assoc)
    1.27 +
    1.28 +lemma diff_add_assoc:
    1.29 +  "c + b - a = c + (b - a)"
    1.30 +  using `a \<le> b` by (simp add: add_commute add_diff_assoc)
    1.31 +
    1.32 +lemma diff_add_assoc2:
    1.33 +  "b + c - a = b - a + c"
    1.34 +  using `a \<le> b`by (simp add: add_commute add_diff_assoc)
    1.35 +
    1.36 +lemma diff_diff_right:
    1.37 +  "c - (b - a) = c + a - b"
    1.38 +  by (simp add: add_diff_inverse add_diff_cancel_left [of a c "b - a", symmetric] add_commute)
    1.39 +
    1.40 +lemma diff_add:
    1.41 +  "b - a + a = b"
    1.42 +  by (simp add: add_commute add_diff_inverse)
    1.43 +
    1.44 +lemma le_add_diff:
    1.45 +  "c \<le> b + c - a"
    1.46 +  by (auto simp add: add_commute diff_add_assoc2 le_iff_add)
    1.47 +
    1.48 +lemma le_imp_diff_is_add:
    1.49 +  "a \<le> b \<Longrightarrow> b - a = c \<longleftrightarrow> b = c + a"
    1.50 +  by (auto simp add: add_commute add_diff_inverse)
    1.51 +
    1.52 +lemma le_diff_conv2:
    1.53 +  "c \<le> b - a \<longleftrightarrow> c + a \<le> b" (is "?P \<longleftrightarrow> ?Q")
    1.54 +proof
    1.55 +  assume ?P
    1.56 +  then have "c + a \<le> b - a + a" by (rule add_right_mono)
    1.57 +  then show ?Q by (simp add: add_diff_inverse add_commute)
    1.58 +next
    1.59 +  assume ?Q
    1.60 +  then have "a + c \<le> a + (b - a)" by (simp add: add_diff_inverse add_commute)
    1.61 +  then show ?P by simp
    1.62 +qed
    1.63 +
    1.64 +end
    1.65 +
    1.66 +end
    1.67 +
    1.68 +
    1.69  subsection {* Support for reasoning about signs *}
    1.70  
    1.71  class ordered_comm_monoid_add =
     2.1 --- a/src/HOL/Library/Multiset.thy	Sun Jun 02 10:57:21 2013 +0200
     2.2 +++ b/src/HOL/Library/Multiset.thy	Sun Jun 02 20:44:55 2013 +0200
     2.3 @@ -137,17 +137,25 @@
     2.4    by (simp add: minus_multiset.rep_eq)
     2.5  
     2.6  lemma diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}"
     2.7 -by(simp add: multiset_eq_iff)
     2.8 +  by rule (fact Groups.diff_zero, fact Groups.zero_diff)
     2.9  
    2.10  lemma diff_cancel[simp]: "A - A = {#}"
    2.11 -by (rule multiset_eqI) simp
    2.12 +  by (fact Groups.diff_cancel)
    2.13  
    2.14  lemma diff_union_cancelR [simp]: "M + N - N = (M::'a multiset)"
    2.15 -by(simp add: multiset_eq_iff)
    2.16 +  by (fact add_diff_cancel_right')
    2.17  
    2.18  lemma diff_union_cancelL [simp]: "N + M - N = (M::'a multiset)"
    2.19 -by(simp add: multiset_eq_iff)
    2.20 +  by (fact add_diff_cancel_left')
    2.21  
    2.22 +lemma diff_right_commute:
    2.23 +  "(M::'a multiset) - N - Q = M - Q - N"
    2.24 +  by (fact diff_right_commute)
    2.25 +
    2.26 +lemma diff_add:
    2.27 +  "(M::'a multiset) - (N + Q) = M - N - Q"
    2.28 +  by (rule sym) (fact diff_diff_add)
    2.29 +  
    2.30  lemma insert_DiffM:
    2.31    "x \<in># M \<Longrightarrow> {#x#} + (M - {#x#}) = M"
    2.32    by (clarsimp simp: multiset_eq_iff)
    2.33 @@ -156,14 +164,6 @@
    2.34    "x \<in># M \<Longrightarrow> M - {#x#} + {#x#} = M"
    2.35    by (clarsimp simp: multiset_eq_iff)
    2.36  
    2.37 -lemma diff_right_commute:
    2.38 -  "(M::'a multiset) - N - Q = M - Q - N"
    2.39 -  by (auto simp add: multiset_eq_iff)
    2.40 -
    2.41 -lemma diff_add:
    2.42 -  "(M::'a multiset) - (N + Q) = M - N - Q"
    2.43 -by (simp add: multiset_eq_iff)
    2.44 -
    2.45  lemma diff_union_swap:
    2.46    "a \<noteq> b \<Longrightarrow> M - {#a#} + {#b#} = M + {#b#} - {#a#}"
    2.47    by (auto simp add: multiset_eq_iff)
    2.48 @@ -289,6 +289,9 @@
    2.49  apply (auto intro: multiset_eq_iff [THEN iffD2])
    2.50  done
    2.51  
    2.52 +instance multiset :: (type) ordered_cancel_comm_monoid_diff
    2.53 +  by default (simp, fact mset_le_exists_conv)
    2.54 +
    2.55  lemma mset_le_mono_add_right_cancel [simp]:
    2.56    "(A::'a multiset) + C \<le> B + C \<longleftrightarrow> A \<le> B"
    2.57    by (fact add_le_cancel_right)
     3.1 --- a/src/HOL/Nat.thy	Sun Jun 02 10:57:21 2013 +0200
     3.2 +++ b/src/HOL/Nat.thy	Sun Jun 02 20:44:55 2013 +0200
     3.3 @@ -456,7 +456,8 @@
     3.4  end
     3.5  
     3.6  instance nat :: no_top
     3.7 -  by default (auto intro: less_Suc_eq_le[THEN iffD2])
     3.8 +  by default (auto intro: less_Suc_eq_le [THEN iffD2])
     3.9 +
    3.10  
    3.11  subsubsection {* Introduction properties *}
    3.12  
    3.13 @@ -714,10 +715,9 @@
    3.14  text{*The naturals form an ordered @{text comm_semiring_1_cancel}*}
    3.15  instance nat :: linordered_semidom
    3.16  proof
    3.17 -  fix i j k :: nat
    3.18    show "0 < (1::nat)" by simp
    3.19 -  show "i \<le> j ==> k + i \<le> k + j" by simp
    3.20 -  show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2)
    3.21 +  show "\<And>m n q :: nat. m \<le> n \<Longrightarrow> q + m \<le> q + n" by simp
    3.22 +  show "\<And>m n q :: nat. m < n \<Longrightarrow> 0 < q \<Longrightarrow> q * m < q * n" by (simp add: mult_less_mono2)
    3.23  qed
    3.24  
    3.25  instance nat :: no_zero_divisors
    3.26 @@ -1067,6 +1067,11 @@
    3.27  lemma le_iff_add: "(m::nat) \<le> n = (\<exists>k. n = m + k)"
    3.28    by (auto simp: le_add1 dest!: le_add_diff_inverse sym [of _ n])
    3.29  
    3.30 +instance nat :: ordered_cancel_comm_monoid_diff
    3.31 +proof
    3.32 +  show "\<And>m n :: nat. m \<le> n \<longleftrightarrow> (\<exists>q. n = m + q)" by (fact le_iff_add)
    3.33 +qed
    3.34 +
    3.35  lemma less_imp_diff_less: "(j::nat) < k ==> j - n < k"
    3.36  by (rule le_less_trans, rule diff_le_self)
    3.37