Library changes for mutilated checkerboard
authorpaulson
Wed Mar 27 18:45:17 1996 +0100 (1996-03-27)
changeset 1618372880456b5b
parent 1617 f9a9d27e9278
child 1619 cb62d89b7adb
Library changes for mutilated checkerboard
src/HOL/Arith.ML
src/HOL/Finite.ML
src/HOL/Nat.ML
src/HOL/Prod.ML
src/HOL/Set.ML
src/HOL/WF.ML
src/HOL/equalities.ML
     1.1 --- a/src/HOL/Arith.ML	Tue Mar 26 17:15:54 1996 +0100
     1.2 +++ b/src/HOL/Arith.ML	Wed Mar 27 18:45:17 1996 +0100
     1.3 @@ -285,6 +285,36 @@
     1.4  
     1.5  (*13 July 1992: loaded in 105.7s*)
     1.6  
     1.7 +
     1.8 +(*** Further facts about mod (mainly for mutilated checkerboard ***)
     1.9 +
    1.10 +goal Arith.thy
    1.11 +    "!!m n. 0<n ==> \
    1.12 +\           Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))";
    1.13 +by (res_inst_tac [("n","m")] less_induct 1);
    1.14 +by (excluded_middle_tac "Suc(na)<n" 1);
    1.15 +(* case Suc(na) < n *)
    1.16 +by (forward_tac [lessI RS less_trans] 2);
    1.17 +by (asm_simp_tac (!simpset addsimps [mod_less, less_not_refl2 RS not_sym]) 2);
    1.18 +(* case n <= Suc(na) *)
    1.19 +by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le, mod_geq]) 1);
    1.20 +by (etac (le_imp_less_or_eq RS disjE) 1);
    1.21 +by (asm_simp_tac (!simpset addsimps [Suc_diff_n]) 1);
    1.22 +by (asm_full_simp_tac (!simpset addsimps [not_less_eq RS sym, 
    1.23 +                                          diff_less, mod_geq]) 1);
    1.24 +by (asm_simp_tac (!simpset addsimps [mod_less]) 1);
    1.25 +qed "mod_Suc";
    1.26 +
    1.27 +goal Arith.thy "!!m n. 0<n ==> m mod n < n";
    1.28 +by (res_inst_tac [("n","m")] less_induct 1);
    1.29 +by (excluded_middle_tac "na<n" 1);
    1.30 +(*case na<n*)
    1.31 +by (asm_simp_tac (!simpset addsimps [mod_less]) 2);
    1.32 +(*case n le na*)
    1.33 +by (asm_full_simp_tac (!simpset addsimps [mod_geq, diff_less]) 1);
    1.34 +qed "mod_less_divisor";
    1.35 +
    1.36 +
    1.37  (**** Additional theorems about "less than" ****)
    1.38  
    1.39  goal Arith.thy "!!m. m<n --> (? k. n=Suc(m+k))";
     2.1 --- a/src/HOL/Finite.ML	Tue Mar 26 17:15:54 1996 +0100
     2.2 +++ b/src/HOL/Finite.ML	Wed Mar 27 18:45:17 1996 +0100
     2.3 @@ -139,12 +139,8 @@
     2.4  qed "insert_finite";
     2.5  Addsimps[insert_finite];
     2.6  
     2.7 -goal Finite.thy "!!A. finite(A) ==> finite(A-B)";
     2.8 -by (etac finite_induct 1);
     2.9 -by (Simp_tac 1);
    2.10 -by (asm_simp_tac (!simpset addsimps [insert_Diff_if]
    2.11 -                          setloop split_tac[expand_if]) 1);
    2.12 -qed "finite_Diff";
    2.13 +(* finite B ==> finite (B - Ba) *)
    2.14 +bind_thm ("finite_Diff", Diff_subset RS finite_subset);
    2.15  Addsimps [finite_Diff];
    2.16  
    2.17  (*The image of a finite set is finite*)
    2.18 @@ -287,6 +283,17 @@
    2.19  by (assume_tac 1);
    2.20  qed "card_insert_disjoint";
    2.21  
    2.22 +goal Finite.thy "!!A. [| finite A; x: A |] ==> Suc(card(A-{x})) = card A";
    2.23 +by (res_inst_tac [("t", "A")] (insert_Diff RS subst) 1);
    2.24 +by (assume_tac 1);
    2.25 +by (asm_simp_tac (!simpset addsimps [card_insert_disjoint]) 1);
    2.26 +qed "card_Suc_Diff";
    2.27 +
    2.28 +goal Finite.thy "!!A. [| finite A; x: A |] ==> card(A-{x}) < card A";
    2.29 +by (resolve_tac [Suc_less_SucD] 1);
    2.30 +by (asm_simp_tac (!simpset addsimps [card_Suc_Diff]) 1);
    2.31 +qed "card_Diff";
    2.32 +
    2.33  val [major] = goal Finite.thy
    2.34    "finite A ==> card(insert x A) = Suc(card(A-{x}))";
    2.35  by (case_tac "x:A" 1);
     3.1 --- a/src/HOL/Nat.ML	Tue Mar 26 17:15:54 1996 +0100
     3.2 +++ b/src/HOL/Nat.ML	Wed Mar 27 18:45:17 1996 +0100
     3.3 @@ -123,7 +123,7 @@
     3.4  by (ALLGOALS(asm_simp_tac (!simpset addsimps [Suc_Suc_eq])));
     3.5  qed "n_not_Suc_n";
     3.6  
     3.7 -val Suc_n_not_n = n_not_Suc_n RS not_sym;
     3.8 +bind_thm ("Suc_n_not_n", n_not_Suc_n RS not_sym);
     3.9  
    3.10  (*** nat_case -- the selection operator for nat ***)
    3.11  
    3.12 @@ -217,7 +217,7 @@
    3.13  qed "lessI";
    3.14  Addsimps [lessI];
    3.15  
    3.16 -(* i(j ==> i(Suc(j) *)
    3.17 +(* i<j ==> i<Suc(j) *)
    3.18  val less_SucI = lessI RSN (2, less_trans);
    3.19  
    3.20  goal Nat.thy "0 < Suc(n)";
    3.21 @@ -239,14 +239,14 @@
    3.22  
    3.23  goalw Nat.thy [less_def] "~ n<(n::nat)";
    3.24  by (rtac notI 1);
    3.25 -by (etac (wf_pred_nat RS wf_trancl RS wf_anti_refl) 1);
    3.26 +by (etac (wf_pred_nat RS wf_trancl RS wf_irrefl) 1);
    3.27  qed "less_not_refl";
    3.28  
    3.29  (* n(n ==> R *)
    3.30 -bind_thm ("less_anti_refl", (less_not_refl RS notE));
    3.31 +bind_thm ("less_irrefl", (less_not_refl RS notE));
    3.32  
    3.33  goal Nat.thy "!!m. n<m ==> m ~= (n::nat)";
    3.34 -by (fast_tac (HOL_cs addEs [less_anti_refl]) 1);
    3.35 +by (fast_tac (HOL_cs addEs [less_irrefl]) 1);
    3.36  qed "less_not_refl2";
    3.37  
    3.38  
    3.39 @@ -335,7 +335,7 @@
    3.40  Addsimps [Suc_less_eq];
    3.41  
    3.42  goal Nat.thy "~(Suc(n) < n)";
    3.43 -by (fast_tac (HOL_cs addEs [Suc_lessD RS less_anti_refl]) 1);
    3.44 +by (fast_tac (HOL_cs addEs [Suc_lessD RS less_irrefl]) 1);
    3.45  qed "not_Suc_n_less_n";
    3.46  Addsimps [not_Suc_n_less_n];
    3.47  
    3.48 @@ -398,23 +398,27 @@
    3.49    "m=n ==> nat_rec m a f = nat_rec n a f"
    3.50    (fn [prem] => [rtac (prem RS arg_cong) 1]);
    3.51  
    3.52 -val prems = goalw Nat.thy [le_def] "~(n<m) ==> m<=(n::nat)";
    3.53 +val prems = goalw Nat.thy [le_def] "~n<m ==> m<=(n::nat)";
    3.54  by (resolve_tac prems 1);
    3.55  qed "leI";
    3.56  
    3.57 -val prems = goalw Nat.thy [le_def] "m<=n ==> ~(n<(m::nat))";
    3.58 +val prems = goalw Nat.thy [le_def] "m<=n ==> ~ n < (m::nat)";
    3.59  by (resolve_tac prems 1);
    3.60  qed "leD";
    3.61  
    3.62  val leE = make_elim leD;
    3.63  
    3.64 +goal Nat.thy "(~n<m) = (m<=(n::nat))";
    3.65 +by (fast_tac (HOL_cs addIs [leI] addEs [leE]) 1);
    3.66 +qed "not_less_iff_le";
    3.67 +
    3.68  goalw Nat.thy [le_def] "!!m. ~ m <= n ==> n<(m::nat)";
    3.69  by (fast_tac HOL_cs 1);
    3.70  qed "not_leE";
    3.71  
    3.72  goalw Nat.thy [le_def] "!!m. m < n ==> Suc(m) <= n";
    3.73  by (Simp_tac 1);
    3.74 -by (fast_tac (HOL_cs addEs [less_anti_refl,less_asym]) 1);
    3.75 +by (fast_tac (HOL_cs addEs [less_irrefl,less_asym]) 1);
    3.76  qed "lessD";
    3.77  
    3.78  goalw Nat.thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
    3.79 @@ -433,12 +437,12 @@
    3.80  
    3.81  goalw Nat.thy [le_def] "!!m. m <= n ==> m < n | m=(n::nat)";
    3.82  by (cut_facts_tac [less_linear] 1);
    3.83 -by (fast_tac (HOL_cs addEs [less_anti_refl,less_asym]) 1);
    3.84 +by (fast_tac (HOL_cs addEs [less_irrefl,less_asym]) 1);
    3.85  qed "le_imp_less_or_eq";
    3.86  
    3.87  goalw Nat.thy [le_def] "!!m. m<n | m=n ==> m <=(n::nat)";
    3.88  by (cut_facts_tac [less_linear] 1);
    3.89 -by (fast_tac (HOL_cs addEs [less_anti_refl,less_asym]) 1);
    3.90 +by (fast_tac (HOL_cs addEs [less_irrefl,less_asym]) 1);
    3.91  by (flexflex_tac);
    3.92  qed "less_or_eq_imp_le";
    3.93  
    3.94 @@ -467,7 +471,7 @@
    3.95  
    3.96  val prems = goal Nat.thy "!!m. [| m <= n; n <= m |] ==> m = (n::nat)";
    3.97  by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq,
    3.98 -          fast_tac (HOL_cs addEs [less_anti_refl,less_asym])]);
    3.99 +          fast_tac (HOL_cs addEs [less_irrefl,less_asym])]);
   3.100  qed "le_anti_sym";
   3.101  
   3.102  goal Nat.thy "(Suc(n) <= Suc(m)) = (n <= m)";
     4.1 --- a/src/HOL/Prod.ML	Tue Mar 26 17:15:54 1996 +0100
     4.2 +++ b/src/HOL/Prod.ML	Wed Mar 27 18:45:17 1996 +0100
     4.3 @@ -232,6 +232,19 @@
     4.4                       addSEs [SigmaE]) 1);
     4.5  qed "Sigma_mono";
     4.6  
     4.7 +qed_goal "Sigma_empty1" Prod.thy "Sigma {} B = {}"
     4.8 + (fn _ => [ (fast_tac (eq_cs addSEs [SigmaE]) 1) ]);
     4.9 +
    4.10 +qed_goal "Sigma_empty2" Prod.thy "Sigma A (%x.{}) = {}"
    4.11 + (fn _ => [ (fast_tac (eq_cs addSEs [SigmaE]) 1) ]);
    4.12 +
    4.13 +Addsimps [Sigma_empty1,Sigma_empty2]; 
    4.14 +
    4.15 +goal Prod.thy "((a,b): Sigma A B) = (a:A & b:B(a))";
    4.16 +by (fast_tac (eq_cs addSIs [SigmaI] addSEs [SigmaE, Pair_inject]) 1);
    4.17 +qed "mem_Sigma_iff";
    4.18 +Addsimps [mem_Sigma_iff]; 
    4.19 +
    4.20  
    4.21  (*** Domain of a relation ***)
    4.22  
     5.1 --- a/src/HOL/Set.ML	Tue Mar 26 17:15:54 1996 +0100
     5.2 +++ b/src/HOL/Set.ML	Wed Mar 27 18:45:17 1996 +0100
     5.3 @@ -70,10 +70,10 @@
     5.4  qed "bexE";
     5.5  
     5.6  (*Trival rewrite rule;   (! x:A.P)=P holds only if A is nonempty!*)
     5.7 -val prems = goal Set.thy
     5.8 -    "(! x:A. True) = True";
     5.9 +goal Set.thy "(! x:A. True) = True";
    5.10  by (REPEAT (ares_tac [TrueI,ballI,iffI] 1));
    5.11  qed "ball_rew";
    5.12 +Addsimps [ball_rew];
    5.13  
    5.14  (** Congruence rules **)
    5.15  
     6.1 --- a/src/HOL/WF.ML	Tue Mar 26 17:15:54 1996 +0100
     6.2 +++ b/src/HOL/WF.ML	Wed Mar 27 18:45:17 1996 +0100
     6.3 @@ -46,7 +46,7 @@
     6.4  val prems = goal WF.thy "[| wf(r);  (a,a): r |] ==> P";
     6.5  by (rtac wf_asym 1);
     6.6  by (REPEAT (resolve_tac prems 1));
     6.7 -qed "wf_anti_refl";
     6.8 +qed "wf_irrefl";
     6.9  
    6.10  (*transitive closure of a wf relation is wf! *)
    6.11  val [prem] = goal WF.thy "wf(r) ==> wf(r^+)";
     7.1 --- a/src/HOL/equalities.ML	Tue Mar 26 17:15:54 1996 +0100
     7.2 +++ b/src/HOL/equalities.ML	Wed Mar 27 18:45:17 1996 +0100
     7.3 @@ -120,6 +120,10 @@
     7.4  by (fast_tac eq_cs 1);
     7.5  qed "Int_Un_distrib";
     7.6  
     7.7 +goal Set.thy "(B Un C) Int A =  (B Int A) Un (C Int A)";
     7.8 +by (fast_tac eq_cs 1);
     7.9 +qed "Int_Un_distrib2";
    7.10 +
    7.11  goal Set.thy "(A<=B) = (A Int B = A)";
    7.12  by (fast_tac (eq_cs addSEs [equalityE]) 1);
    7.13  qed "subset_Int_eq";