# HG changeset patch
# User paulson
# Date 864731021 -7200
# Node ID 04502e5431fb44768c0fda654030afd426f1d0bf
# Parent  ed64b6799303c5f9a2be129142e9a1af945fc14e
New theorems suggested by Florian Kammueller

diff -r ed64b6799303 -r 04502e5431fb src/HOL/Arith.ML
--- 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);
diff -r ed64b6799303 -r 04502e5431fb src/HOL/Finite.ML
--- 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);