New theorems suggested by Florian Kammueller
authorpaulson
Tue May 27 13:03:41 1997 +0200 (1997-05-27)
changeset 335204502e5431fb
parent 3351 ed64b6799303
child 3353 9112a2efb9a3
New theorems suggested by Florian Kammueller
src/HOL/Arith.ML
src/HOL/Finite.ML
     1.1 --- a/src/HOL/Arith.ML	Mon May 26 14:54:24 1997 +0200
     1.2 +++ b/src/HOL/Arith.ML	Tue May 27 13:03:41 1997 +0200
     1.3 @@ -325,10 +325,10 @@
     1.4  Addsimps [diff_self_eq_0];
     1.5  
     1.6  (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
     1.7 -val [prem] = goal Arith.thy "[| ~ m<n |] ==> n+(m-n) = (m::nat)";
     1.8 +val [prem] = goal Arith.thy "~ m<n ==> n+(m-n) = (m::nat)";
     1.9  by (rtac (prem RS rev_mp) 1);
    1.10  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.11 -by (ALLGOALS (Asm_simp_tac));
    1.12 +by (ALLGOALS Asm_simp_tac);
    1.13  qed "add_diff_inverse";
    1.14  
    1.15  Delsimps  [diff_Suc];
    1.16 @@ -336,6 +336,12 @@
    1.17  
    1.18  (*** More results about difference ***)
    1.19  
    1.20 +val [prem] = goal Arith.thy "n < Suc(m) ==> Suc(m)-n = Suc(m-n)";
    1.21 +by (rtac (prem RS rev_mp) 1);
    1.22 +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.23 +by (ALLGOALS Asm_simp_tac);
    1.24 +qed "Suc_diff_n";
    1.25 +
    1.26  goal Arith.thy "m - n < Suc(m)";
    1.27  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.28  by (etac less_SucE 3);
    1.29 @@ -347,6 +353,30 @@
    1.30  by (ALLGOALS Asm_simp_tac);
    1.31  qed "diff_le_self";
    1.32  
    1.33 +goal Arith.thy "!!i::nat. i-j-k = i - (j+k)";
    1.34 +by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
    1.35 +by (ALLGOALS Asm_simp_tac);
    1.36 +qed "diff_diff_left";
    1.37 +
    1.38 +(*This and the next few suggested by Florian Kammüller*)
    1.39 +goal Arith.thy "!!i::nat. i-j-k = i-k-j";
    1.40 +by (simp_tac (!simpset addsimps [diff_diff_left, add_commute]) 1);
    1.41 +qed "diff_commute";
    1.42 +
    1.43 +goal Arith.thy "!!i j k:: nat. k<=j --> j<=i --> i - (j - k) = i - j + k";
    1.44 +by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
    1.45 +by (ALLGOALS Asm_simp_tac);
    1.46 +by (asm_simp_tac
    1.47 +    (!simpset addsimps [Suc_diff_n, le_imp_less_Suc, le_Suc_eq]) 1);
    1.48 +by (simp_tac
    1.49 +    (!simpset addsimps [add_diff_inverse, not_less_iff_le, add_commute]) 1);
    1.50 +qed_spec_mp "diff_diff_right";
    1.51 +
    1.52 +goal Arith.thy "!!i j k:: nat. k<=j --> (i + j) - k = i + (j - k)";
    1.53 +by (res_inst_tac [("m","j"),("n","k")] diff_induct 1);
    1.54 +by (ALLGOALS Asm_simp_tac);
    1.55 +qed_spec_mp "diff_add_assoc";
    1.56 +
    1.57  goal Arith.thy "!!n::nat. (n+m) - n = m";
    1.58  by (induct_tac "n" 1);
    1.59  by (ALLGOALS Asm_simp_tac);
    1.60 @@ -354,8 +384,7 @@
    1.61  Addsimps [diff_add_inverse];
    1.62  
    1.63  goal Arith.thy "!!n::nat.(m+n) - n = m";
    1.64 -by (res_inst_tac [("m1","m")] (add_commute RS ssubst) 1);
    1.65 -by (REPEAT (ares_tac [diff_add_inverse] 1));
    1.66 +by (simp_tac (!simpset addsimps [diff_add_assoc]) 1);
    1.67  qed "diff_add_inverse2";
    1.68  Addsimps [diff_add_inverse2];
    1.69  
    1.70 @@ -363,7 +392,7 @@
    1.71  by (rtac (prem RS rev_mp) 1);
    1.72  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.73  by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
    1.74 -by (ALLGOALS (Asm_simp_tac));
    1.75 +by (ALLGOALS Asm_simp_tac);
    1.76  qed "less_imp_diff_is_0";
    1.77  
    1.78  val prems = goal Arith.thy "m-n = 0  -->  n-m = 0  -->  m=n";
    1.79 @@ -374,15 +403,9 @@
    1.80  val [prem] = goal Arith.thy "m<n ==> 0<n-m";
    1.81  by (rtac (prem RS rev_mp) 1);
    1.82  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.83 -by (ALLGOALS (Asm_simp_tac));
    1.84 +by (ALLGOALS Asm_simp_tac);
    1.85  qed "less_imp_diff_positive";
    1.86  
    1.87 -val [prem] = goal Arith.thy "n < Suc(m) ==> Suc(m)-n = Suc(m-n)";
    1.88 -by (rtac (prem RS rev_mp) 1);
    1.89 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.90 -by (ALLGOALS (Asm_simp_tac));
    1.91 -qed "Suc_diff_n";
    1.92 -
    1.93  goal Arith.thy "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
    1.94  by (simp_tac (!simpset addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]
    1.95                      setloop (split_tac [expand_if])) 1);
     2.1 --- a/src/HOL/Finite.ML	Mon May 26 14:54:24 1997 +0200
     2.2 +++ b/src/HOL/Finite.ML	Tue May 27 13:03:41 1997 +0200
     2.3 @@ -132,13 +132,13 @@
     2.4  
     2.5  goalw Finite.thy [finite_def] "finite(F Un G) = (finite F & finite G)";
     2.6  by (Simp_tac 1);
     2.7 -qed "subset_finite";
     2.8 -Addsimps[subset_finite];
     2.9 +qed "finite_Un_eq";
    2.10 +Addsimps[finite_Un_eq];
    2.11  
    2.12  goalw Finite.thy [finite_def] "finite(insert a A) = finite(A)";
    2.13  by (Simp_tac 1);
    2.14 -qed "insert_finite";
    2.15 -Addsimps[insert_finite];
    2.16 +qed "finite_insert";
    2.17 +Addsimps[finite_insert];
    2.18  
    2.19  (* finite B ==> finite (B - Ba) *)
    2.20  bind_thm ("finite_Diff", Diff_subset RS finite_subset);
    2.21 @@ -291,11 +291,46 @@
    2.22  by (etac lemma 1);
    2.23  by (assume_tac 1);
    2.24  qed "card_insert_disjoint";
    2.25 +Addsimps [card_insert_disjoint];
    2.26 +
    2.27 +goal Finite.thy  "!!A. finite A ==> !B. B <= A --> card(B) <= card(A)";
    2.28 +by (etac finite_induct 1);
    2.29 +by (Simp_tac 1);
    2.30 +by (strip_tac 1);
    2.31 +by (case_tac "x:B" 1);
    2.32 + by (dtac mk_disjoint_insert 1);
    2.33 + by (SELECT_GOAL(safe_tac (!claset))1);
    2.34 + by (rotate_tac ~1 1);
    2.35 + by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
    2.36 +by (rotate_tac ~1 1);
    2.37 +by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
    2.38 +qed_spec_mp "card_mono";
    2.39 +
    2.40 +goal Finite.thy "!!A B. [| finite A; finite B |]\
    2.41 +\                       ==> A Int B = {} --> card(A Un B) = card A + card B";
    2.42 +by (etac finite_induct 1);
    2.43 +by (ALLGOALS 
    2.44 +    (asm_simp_tac (!simpset addsimps [Un_insert_left, Int_insert_left]
    2.45 +		            setloop split_tac [expand_if])));
    2.46 +qed_spec_mp "card_Un_disjoint";
    2.47 +
    2.48 +goal Finite.thy "!!A. [| finite A; B<=A |] ==> card A - card B = card (A - B)";
    2.49 +by (subgoal_tac "(A-B) Un B = A" 1);
    2.50 +by (Blast_tac 2);
    2.51 +br (add_right_cancel RS iffD1) 1;
    2.52 +br (card_Un_disjoint RS subst) 1;
    2.53 +be ssubst 4;
    2.54 +by (Blast_tac 3);
    2.55 +by (ALLGOALS 
    2.56 +    (asm_simp_tac
    2.57 +     (!simpset addsimps [add_commute, not_less_iff_le, 
    2.58 +			 add_diff_inverse, card_mono, finite_subset])));
    2.59 +qed "card_Diff_subset";
    2.60  
    2.61  goal Finite.thy "!!A. [| finite A; x: A |] ==> Suc(card(A-{x})) = card A";
    2.62  by (res_inst_tac [("t", "A")] (insert_Diff RS subst) 1);
    2.63  by (assume_tac 1);
    2.64 -by (asm_simp_tac (!simpset addsimps [card_insert_disjoint]) 1);
    2.65 +by (Asm_simp_tac 1);
    2.66  qed "card_Suc_Diff";
    2.67  
    2.68  goal Finite.thy "!!A. [| finite A; x: A |] ==> card(A-{x}) < card A";
    2.69 @@ -332,19 +367,6 @@
    2.70  qed_spec_mp "card_image";
    2.71  
    2.72  
    2.73 -goal Finite.thy  "!!A. finite A ==> !B. B <= A --> card(B) <= card(A)";
    2.74 -by (etac finite_induct 1);
    2.75 -by (Simp_tac 1);
    2.76 -by (strip_tac 1);
    2.77 -by (case_tac "x:B" 1);
    2.78 - by (dtac mk_disjoint_insert 1);
    2.79 - by (SELECT_GOAL(safe_tac (!claset))1);
    2.80 - by (rotate_tac ~1 1);
    2.81 - by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
    2.82 -by (rotate_tac ~1 1);
    2.83 -by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
    2.84 -qed_spec_mp "card_mono";
    2.85 -
    2.86  goalw Finite.thy [psubset_def]
    2.87  "!!B. finite B ==> !A. A < B --> card(A) < card(B)";
    2.88  by (etac finite_induct 1);