author paulson Tue, 27 May 1997 13:03:41 +0200 changeset 3352 04502e5431fb parent 3351 ed64b6799303 child 3353 9112a2efb9a3
New theorems suggested by Florian Kammueller
 src/HOL/Arith.ML file | annotate | diff | comparison | revisions src/HOL/Finite.ML file | annotate | diff | comparison | revisions
```--- 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 @@

(*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);

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";
+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
+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);
+
goal Arith.thy "!!n::nat. (n+m) - n = m";
by (induct_tac "n" 1);
by (ALLGOALS Asm_simp_tac);
@@ -354,8 +384,7 @@

goal Arith.thy "!!n::nat.(m+n) - n = m";
-by (res_inst_tac [("m1","m")] (add_commute RS ssubst) 1);

@@ -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";
+qed "finite_Un_eq";

goalw Finite.thy [finite_def] "finite(insert a A) = finite(A)";
by (Simp_tac 1);
-qed "insert_finite";
+qed "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";
+
+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 (card_Un_disjoint RS subst) 1;
+be ssubst 4;
+by (Blast_tac 3);
+by (ALLGOALS
+    (asm_simp_tac
+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);```