typeclass formalising bounded subtraction
authorhaftmann
Sat Sep 15 20:14:29 2012 +0200 (2012-09-15)
changeset 493881ffd5a055acf
parent 49387 167708456269
child 49389 da621dc65146
typeclass formalising bounded subtraction
NEWS
src/HOL/Groups.thy
src/HOL/Library/Multiset.thy
src/HOL/Nat.thy
     1.1 --- a/NEWS	Sat Sep 15 20:13:25 2012 +0200
     1.2 +++ b/NEWS	Sat Sep 15 20:14:29 2012 +0200
     1.3 @@ -47,6 +47,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Class "comm_monoid_diff" formalised properties of bounded
     1.8 +subtraction, with natural numbers and multisets as typical instances.
     1.9 +
    1.10  * Theory "Library/Option_ord" provides instantiation of option type
    1.11  to lattice type classes.
    1.12  
     2.1 --- a/src/HOL/Groups.thy	Sat Sep 15 20:13:25 2012 +0200
     2.2 +++ b/src/HOL/Groups.thy	Sat Sep 15 20:14:29 2012 +0200
     2.3 @@ -213,6 +213,57 @@
     2.4  subclass (in comm_monoid_add) monoid_add proof
     2.5  qed (fact add.left_neutral add.right_neutral)+
     2.6  
     2.7 +class comm_monoid_diff = comm_monoid_add + minus +
     2.8 +  assumes diff_zero [simp]: "a - 0 = a"
     2.9 +    and zero_diff [simp]: "0 - a = 0"
    2.10 +    and add_diff_cancel_left [simp]: "(c + a) - (c + b) = a - b"
    2.11 +    and diff_diff_add: "a - b - c = a - (b + c)"
    2.12 +begin
    2.13 +
    2.14 +lemma add_diff_cancel_right [simp]:
    2.15 +  "(a + c) - (b + c) = a - b"
    2.16 +  using add_diff_cancel_left [symmetric] by (simp add: add.commute)
    2.17 +
    2.18 +lemma add_diff_cancel_left' [simp]:
    2.19 +  "(b + a) - b = a"
    2.20 +proof -
    2.21 +  have "(b + a) - (b + 0) = a" by (simp only: add_diff_cancel_left diff_zero)
    2.22 +  then show ?thesis by simp
    2.23 +qed
    2.24 +
    2.25 +lemma add_diff_cancel_right' [simp]:
    2.26 +  "(a + b) - b = a"
    2.27 +  using add_diff_cancel_left' [symmetric] by (simp add: add.commute)
    2.28 +
    2.29 +lemma diff_add_zero [simp]:
    2.30 +  "a - (a + b) = 0"
    2.31 +proof -
    2.32 +  have "a - (a + b) = (a + 0) - (a + b)" by simp
    2.33 +  also have "\<dots> = 0" by (simp only: add_diff_cancel_left zero_diff)
    2.34 +  finally show ?thesis .
    2.35 +qed
    2.36 +
    2.37 +lemma diff_cancel [simp]:
    2.38 +  "a - a = 0"
    2.39 +proof -
    2.40 +  have "(a + 0) - (a + 0) = 0" by (simp only: add_diff_cancel_left diff_zero)
    2.41 +  then show ?thesis by simp
    2.42 +qed
    2.43 +
    2.44 +lemma diff_right_commute:
    2.45 +  "a - c - b = a - b - c"
    2.46 +  by (simp add: diff_diff_add add.commute)
    2.47 +
    2.48 +lemma add_implies_diff:
    2.49 +  assumes "c + b = a"
    2.50 +  shows "c = a - b"
    2.51 +proof -
    2.52 +  from assms have "(b + c) - (b + 0) = a - b" by (simp add: add.commute)
    2.53 +  then show "c = a - b" by simp
    2.54 +qed
    2.55 +
    2.56 +end
    2.57 +
    2.58  class monoid_mult = one + semigroup_mult +
    2.59    assumes mult_1_left: "1 * a  = a"
    2.60      and mult_1_right: "a * 1 = a"
    2.61 @@ -1263,3 +1314,4 @@
    2.62  lemmas diff_def = diff_minus
    2.63  
    2.64  end
    2.65 +
     3.1 --- a/src/HOL/Library/Multiset.thy	Sat Sep 15 20:13:25 2012 +0200
     3.2 +++ b/src/HOL/Library/Multiset.thy	Sat Sep 15 20:14:29 2012 +0200
     3.3 @@ -122,13 +122,14 @@
     3.4  
     3.5  subsubsection {* Difference *}
     3.6  
     3.7 -instantiation multiset :: (type) minus
     3.8 +instantiation multiset :: (type) comm_monoid_diff
     3.9  begin
    3.10  
    3.11  lift_definition minus_multiset :: "'a multiset => 'a multiset => 'a multiset" is "\<lambda> M N. \<lambda>a. M a - N a"
    3.12  by (rule diff_preserves_multiset)
    3.13   
    3.14 -instance ..
    3.15 +instance
    3.16 +by default (transfer, simp add: fun_eq_iff)+
    3.17  
    3.18  end
    3.19  
    3.20 @@ -161,6 +162,7 @@
    3.21  
    3.22  lemma diff_add:
    3.23    "(M::'a multiset) - (N + Q) = M - N - Q"
    3.24 +  find_theorems solves
    3.25  by (simp add: multiset_eq_iff)
    3.26  
    3.27  lemma diff_union_swap:
    3.28 @@ -1913,3 +1915,4 @@
    3.29  *}
    3.30  
    3.31  end
    3.32 +
     4.1 --- a/src/HOL/Nat.thy	Sat Sep 15 20:13:25 2012 +0200
     4.2 +++ b/src/HOL/Nat.thy	Sat Sep 15 20:14:29 2012 +0200
     4.3 @@ -134,7 +134,7 @@
     4.4  
     4.5  subsection {* Arithmetic operators *}
     4.6  
     4.7 -instantiation nat :: "{minus, comm_monoid_add}"
     4.8 +instantiation nat :: comm_monoid_diff
     4.9  begin
    4.10  
    4.11  primrec plus_nat where
    4.12 @@ -169,6 +169,10 @@
    4.13    show "(n + m) + q = n + (m + q)" by (induct n) simp_all
    4.14    show "n + m = m + n" by (induct n) simp_all
    4.15    show "0 + n = n" by simp
    4.16 +  show "n - 0 = n" by simp
    4.17 +  show "0 - n = 0" by simp
    4.18 +  show "(q + n) - (q + m) = n - m" by (induct q) simp_all
    4.19 +  show "n - m - q = n - (m + q)" by (induct q) (simp_all add: diff_Suc)
    4.20  qed
    4.21  
    4.22  end
    4.23 @@ -1814,3 +1818,4 @@
    4.24  hide_const (open) of_nat_aux
    4.25  
    4.26  end
    4.27 +