--- a/src/HOL/Arith.ML Mon May 26 14:54:24 1997 +0200
+++ b/src/HOL/Arith.ML Tue May 27 13:03:41 1997 +0200
@@ -325,10 +325,10 @@
Addsimps [diff_self_eq_0];
(*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
-val [prem] = goal Arith.thy "[| ~ m<n |] ==> n+(m-n) = (m::nat)";
+val [prem] = goal Arith.thy "~ m<n ==> n+(m-n) = (m::nat)";
by (rtac (prem RS rev_mp) 1);
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS (Asm_simp_tac));
+by (ALLGOALS Asm_simp_tac);
qed "add_diff_inverse";
Delsimps [diff_Suc];
@@ -336,6 +336,12 @@
(*** More results about difference ***)
+val [prem] = goal Arith.thy "n < Suc(m) ==> Suc(m)-n = Suc(m-n)";
+by (rtac (prem RS rev_mp) 1);
+by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
+by (ALLGOALS Asm_simp_tac);
+qed "Suc_diff_n";
+
goal Arith.thy "m - n < Suc(m)";
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
by (etac less_SucE 3);
@@ -347,6 +353,30 @@
by (ALLGOALS Asm_simp_tac);
qed "diff_le_self";
+goal Arith.thy "!!i::nat. i-j-k = i - (j+k)";
+by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
+by (ALLGOALS Asm_simp_tac);
+qed "diff_diff_left";
+
+(*This and the next few suggested by Florian Kammüller*)
+goal Arith.thy "!!i::nat. i-j-k = i-k-j";
+by (simp_tac (!simpset addsimps [diff_diff_left, add_commute]) 1);
+qed "diff_commute";
+
+goal Arith.thy "!!i j k:: nat. k<=j --> j<=i --> i - (j - k) = i - j + k";
+by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
+by (ALLGOALS Asm_simp_tac);
+by (asm_simp_tac
+ (!simpset addsimps [Suc_diff_n, le_imp_less_Suc, le_Suc_eq]) 1);
+by (simp_tac
+ (!simpset addsimps [add_diff_inverse, not_less_iff_le, add_commute]) 1);
+qed_spec_mp "diff_diff_right";
+
+goal Arith.thy "!!i j k:: nat. k<=j --> (i + j) - k = i + (j - k)";
+by (res_inst_tac [("m","j"),("n","k")] diff_induct 1);
+by (ALLGOALS Asm_simp_tac);
+qed_spec_mp "diff_add_assoc";
+
goal Arith.thy "!!n::nat. (n+m) - n = m";
by (induct_tac "n" 1);
by (ALLGOALS Asm_simp_tac);
@@ -354,8 +384,7 @@
Addsimps [diff_add_inverse];
goal Arith.thy "!!n::nat.(m+n) - n = m";
-by (res_inst_tac [("m1","m")] (add_commute RS ssubst) 1);
-by (REPEAT (ares_tac [diff_add_inverse] 1));
+by (simp_tac (!simpset addsimps [diff_add_assoc]) 1);
qed "diff_add_inverse2";
Addsimps [diff_add_inverse2];
@@ -363,7 +392,7 @@
by (rtac (prem RS rev_mp) 1);
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
-by (ALLGOALS (Asm_simp_tac));
+by (ALLGOALS Asm_simp_tac);
qed "less_imp_diff_is_0";
val prems = goal Arith.thy "m-n = 0 --> n-m = 0 --> m=n";
@@ -374,15 +403,9 @@
val [prem] = goal Arith.thy "m<n ==> 0<n-m";
by (rtac (prem RS rev_mp) 1);
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS (Asm_simp_tac));
+by (ALLGOALS Asm_simp_tac);
qed "less_imp_diff_positive";
-val [prem] = goal Arith.thy "n < Suc(m) ==> Suc(m)-n = Suc(m-n)";
-by (rtac (prem RS rev_mp) 1);
-by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS (Asm_simp_tac));
-qed "Suc_diff_n";
-
goal Arith.thy "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
by (simp_tac (!simpset addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]
setloop (split_tac [expand_if])) 1);
--- a/src/HOL/Finite.ML Mon May 26 14:54:24 1997 +0200
+++ b/src/HOL/Finite.ML Tue May 27 13:03:41 1997 +0200
@@ -132,13 +132,13 @@
goalw Finite.thy [finite_def] "finite(F Un G) = (finite F & finite G)";
by (Simp_tac 1);
-qed "subset_finite";
-Addsimps[subset_finite];
+qed "finite_Un_eq";
+Addsimps[finite_Un_eq];
goalw Finite.thy [finite_def] "finite(insert a A) = finite(A)";
by (Simp_tac 1);
-qed "insert_finite";
-Addsimps[insert_finite];
+qed "finite_insert";
+Addsimps[finite_insert];
(* finite B ==> finite (B - Ba) *)
bind_thm ("finite_Diff", Diff_subset RS finite_subset);
@@ -291,11 +291,46 @@
by (etac lemma 1);
by (assume_tac 1);
qed "card_insert_disjoint";
+Addsimps [card_insert_disjoint];
+
+goal Finite.thy "!!A. finite A ==> !B. B <= A --> card(B) <= card(A)";
+by (etac finite_induct 1);
+by (Simp_tac 1);
+by (strip_tac 1);
+by (case_tac "x:B" 1);
+ by (dtac mk_disjoint_insert 1);
+ by (SELECT_GOAL(safe_tac (!claset))1);
+ by (rotate_tac ~1 1);
+ by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
+by (rotate_tac ~1 1);
+by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
+qed_spec_mp "card_mono";
+
+goal Finite.thy "!!A B. [| finite A; finite B |]\
+\ ==> A Int B = {} --> card(A Un B) = card A + card B";
+by (etac finite_induct 1);
+by (ALLGOALS
+ (asm_simp_tac (!simpset addsimps [Un_insert_left, Int_insert_left]
+ setloop split_tac [expand_if])));
+qed_spec_mp "card_Un_disjoint";
+
+goal Finite.thy "!!A. [| finite A; B<=A |] ==> card A - card B = card (A - B)";
+by (subgoal_tac "(A-B) Un B = A" 1);
+by (Blast_tac 2);
+br (add_right_cancel RS iffD1) 1;
+br (card_Un_disjoint RS subst) 1;
+be ssubst 4;
+by (Blast_tac 3);
+by (ALLGOALS
+ (asm_simp_tac
+ (!simpset addsimps [add_commute, not_less_iff_le,
+ add_diff_inverse, card_mono, finite_subset])));
+qed "card_Diff_subset";
goal Finite.thy "!!A. [| finite A; x: A |] ==> Suc(card(A-{x})) = card A";
by (res_inst_tac [("t", "A")] (insert_Diff RS subst) 1);
by (assume_tac 1);
-by (asm_simp_tac (!simpset addsimps [card_insert_disjoint]) 1);
+by (Asm_simp_tac 1);
qed "card_Suc_Diff";
goal Finite.thy "!!A. [| finite A; x: A |] ==> card(A-{x}) < card A";
@@ -332,19 +367,6 @@
qed_spec_mp "card_image";
-goal Finite.thy "!!A. finite A ==> !B. B <= A --> card(B) <= card(A)";
-by (etac finite_induct 1);
-by (Simp_tac 1);
-by (strip_tac 1);
-by (case_tac "x:B" 1);
- by (dtac mk_disjoint_insert 1);
- by (SELECT_GOAL(safe_tac (!claset))1);
- by (rotate_tac ~1 1);
- by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
-by (rotate_tac ~1 1);
-by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
-qed_spec_mp "card_mono";
-
goalw Finite.thy [psubset_def]
"!!B. finite B ==> !A. A < B --> card(A) < card(B)";
by (etac finite_induct 1);