author haftmann Sat Sep 15 20:14:29 2012 +0200 (2012-09-15) changeset 49388 1ffd5a055acf parent 49387 167708456269 child 49389 da621dc65146
typeclass formalising bounded subtraction
 NEWS file | annotate | diff | revisions src/HOL/Groups.thy file | annotate | diff | revisions src/HOL/Library/Multiset.thy file | annotate | diff | revisions src/HOL/Nat.thy file | annotate | diff | revisions
```     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.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.15 +  "(a + c) - (b + c) = a - b"
2.17 +
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.26 +  "(a + b) - b = a"
2.28 +
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.47 +
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.23    "(M::'a multiset) - (N + Q) = M - N - Q"
3.24 +  find_theorems solves
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 +
```