# HG changeset patch
# User paulson
# Date 827948717 -3600
# Node ID 372880456b5bd03655558ce87b72e150f71db2a9
# Parent  f9a9d27e92785c70a639e7dc3546b9619b922a74
Library changes for mutilated checkerboard

diff -r f9a9d27e9278 -r 372880456b5b src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Tue Mar 26 17:15:54 1996 +0100
+++ b/src/HOL/Arith.ML	Wed Mar 27 18:45:17 1996 +0100
@@ -285,6 +285,36 @@
 
 (*13 July 1992: loaded in 105.7s*)
 
+
+(*** Further facts about mod (mainly for mutilated checkerboard ***)
+
+goal Arith.thy
+    "!!m n. 0<n ==> \
+\           Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))";
+by (res_inst_tac [("n","m")] less_induct 1);
+by (excluded_middle_tac "Suc(na)<n" 1);
+(* case Suc(na) < n *)
+by (forward_tac [lessI RS less_trans] 2);
+by (asm_simp_tac (!simpset addsimps [mod_less, less_not_refl2 RS not_sym]) 2);
+(* case n <= Suc(na) *)
+by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le, mod_geq]) 1);
+by (etac (le_imp_less_or_eq RS disjE) 1);
+by (asm_simp_tac (!simpset addsimps [Suc_diff_n]) 1);
+by (asm_full_simp_tac (!simpset addsimps [not_less_eq RS sym, 
+                                          diff_less, mod_geq]) 1);
+by (asm_simp_tac (!simpset addsimps [mod_less]) 1);
+qed "mod_Suc";
+
+goal Arith.thy "!!m n. 0<n ==> m mod n < n";
+by (res_inst_tac [("n","m")] less_induct 1);
+by (excluded_middle_tac "na<n" 1);
+(*case na<n*)
+by (asm_simp_tac (!simpset addsimps [mod_less]) 2);
+(*case n le na*)
+by (asm_full_simp_tac (!simpset addsimps [mod_geq, diff_less]) 1);
+qed "mod_less_divisor";
+
+
 (**** Additional theorems about "less than" ****)
 
 goal Arith.thy "!!m. m<n --> (? k. n=Suc(m+k))";
diff -r f9a9d27e9278 -r 372880456b5b src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Tue Mar 26 17:15:54 1996 +0100
+++ b/src/HOL/Finite.ML	Wed Mar 27 18:45:17 1996 +0100
@@ -139,12 +139,8 @@
 qed "insert_finite";
 Addsimps[insert_finite];
 
-goal Finite.thy "!!A. finite(A) ==> finite(A-B)";
-by (etac finite_induct 1);
-by (Simp_tac 1);
-by (asm_simp_tac (!simpset addsimps [insert_Diff_if]
-                          setloop split_tac[expand_if]) 1);
-qed "finite_Diff";
+(* finite B ==> finite (B - Ba) *)
+bind_thm ("finite_Diff", Diff_subset RS finite_subset);
 Addsimps [finite_Diff];
 
 (*The image of a finite set is finite*)
@@ -287,6 +283,17 @@
 by (assume_tac 1);
 qed "card_insert_disjoint";
 
+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);
+qed "card_Suc_Diff";
+
+goal Finite.thy "!!A. [| finite A; x: A |] ==> card(A-{x}) < card A";
+by (resolve_tac [Suc_less_SucD] 1);
+by (asm_simp_tac (!simpset addsimps [card_Suc_Diff]) 1);
+qed "card_Diff";
+
 val [major] = goal Finite.thy
   "finite A ==> card(insert x A) = Suc(card(A-{x}))";
 by (case_tac "x:A" 1);
diff -r f9a9d27e9278 -r 372880456b5b src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Tue Mar 26 17:15:54 1996 +0100
+++ b/src/HOL/Nat.ML	Wed Mar 27 18:45:17 1996 +0100
@@ -123,7 +123,7 @@
 by (ALLGOALS(asm_simp_tac (!simpset addsimps [Suc_Suc_eq])));
 qed "n_not_Suc_n";
 
-val Suc_n_not_n = n_not_Suc_n RS not_sym;
+bind_thm ("Suc_n_not_n", n_not_Suc_n RS not_sym);
 
 (*** nat_case -- the selection operator for nat ***)
 
@@ -217,7 +217,7 @@
 qed "lessI";
 Addsimps [lessI];
 
-(* i(j ==> i(Suc(j) *)
+(* i<j ==> i<Suc(j) *)
 val less_SucI = lessI RSN (2, less_trans);
 
 goal Nat.thy "0 < Suc(n)";
@@ -239,14 +239,14 @@
 
 goalw Nat.thy [less_def] "~ n<(n::nat)";
 by (rtac notI 1);
-by (etac (wf_pred_nat RS wf_trancl RS wf_anti_refl) 1);
+by (etac (wf_pred_nat RS wf_trancl RS wf_irrefl) 1);
 qed "less_not_refl";
 
 (* n(n ==> R *)
-bind_thm ("less_anti_refl", (less_not_refl RS notE));
+bind_thm ("less_irrefl", (less_not_refl RS notE));
 
 goal Nat.thy "!!m. n<m ==> m ~= (n::nat)";
-by (fast_tac (HOL_cs addEs [less_anti_refl]) 1);
+by (fast_tac (HOL_cs addEs [less_irrefl]) 1);
 qed "less_not_refl2";
 
 
@@ -335,7 +335,7 @@
 Addsimps [Suc_less_eq];
 
 goal Nat.thy "~(Suc(n) < n)";
-by (fast_tac (HOL_cs addEs [Suc_lessD RS less_anti_refl]) 1);
+by (fast_tac (HOL_cs addEs [Suc_lessD RS less_irrefl]) 1);
 qed "not_Suc_n_less_n";
 Addsimps [not_Suc_n_less_n];
 
@@ -398,23 +398,27 @@
   "m=n ==> nat_rec m a f = nat_rec n a f"
   (fn [prem] => [rtac (prem RS arg_cong) 1]);
 
-val prems = goalw Nat.thy [le_def] "~(n<m) ==> m<=(n::nat)";
+val prems = goalw Nat.thy [le_def] "~n<m ==> m<=(n::nat)";
 by (resolve_tac prems 1);
 qed "leI";
 
-val prems = goalw Nat.thy [le_def] "m<=n ==> ~(n<(m::nat))";
+val prems = goalw Nat.thy [le_def] "m<=n ==> ~ n < (m::nat)";
 by (resolve_tac prems 1);
 qed "leD";
 
 val leE = make_elim leD;
 
+goal Nat.thy "(~n<m) = (m<=(n::nat))";
+by (fast_tac (HOL_cs addIs [leI] addEs [leE]) 1);
+qed "not_less_iff_le";
+
 goalw Nat.thy [le_def] "!!m. ~ m <= n ==> n<(m::nat)";
 by (fast_tac HOL_cs 1);
 qed "not_leE";
 
 goalw Nat.thy [le_def] "!!m. m < n ==> Suc(m) <= n";
 by (Simp_tac 1);
-by (fast_tac (HOL_cs addEs [less_anti_refl,less_asym]) 1);
+by (fast_tac (HOL_cs addEs [less_irrefl,less_asym]) 1);
 qed "lessD";
 
 goalw Nat.thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
@@ -433,12 +437,12 @@
 
 goalw Nat.thy [le_def] "!!m. m <= n ==> m < n | m=(n::nat)";
 by (cut_facts_tac [less_linear] 1);
-by (fast_tac (HOL_cs addEs [less_anti_refl,less_asym]) 1);
+by (fast_tac (HOL_cs addEs [less_irrefl,less_asym]) 1);
 qed "le_imp_less_or_eq";
 
 goalw Nat.thy [le_def] "!!m. m<n | m=n ==> m <=(n::nat)";
 by (cut_facts_tac [less_linear] 1);
-by (fast_tac (HOL_cs addEs [less_anti_refl,less_asym]) 1);
+by (fast_tac (HOL_cs addEs [less_irrefl,less_asym]) 1);
 by (flexflex_tac);
 qed "less_or_eq_imp_le";
 
@@ -467,7 +471,7 @@
 
 val prems = goal Nat.thy "!!m. [| m <= n; n <= m |] ==> m = (n::nat)";
 by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq,
-          fast_tac (HOL_cs addEs [less_anti_refl,less_asym])]);
+          fast_tac (HOL_cs addEs [less_irrefl,less_asym])]);
 qed "le_anti_sym";
 
 goal Nat.thy "(Suc(n) <= Suc(m)) = (n <= m)";
diff -r f9a9d27e9278 -r 372880456b5b src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Tue Mar 26 17:15:54 1996 +0100
+++ b/src/HOL/Prod.ML	Wed Mar 27 18:45:17 1996 +0100
@@ -232,6 +232,19 @@
                      addSEs [SigmaE]) 1);
 qed "Sigma_mono";
 
+qed_goal "Sigma_empty1" Prod.thy "Sigma {} B = {}"
+ (fn _ => [ (fast_tac (eq_cs addSEs [SigmaE]) 1) ]);
+
+qed_goal "Sigma_empty2" Prod.thy "Sigma A (%x.{}) = {}"
+ (fn _ => [ (fast_tac (eq_cs addSEs [SigmaE]) 1) ]);
+
+Addsimps [Sigma_empty1,Sigma_empty2]; 
+
+goal Prod.thy "((a,b): Sigma A B) = (a:A & b:B(a))";
+by (fast_tac (eq_cs addSIs [SigmaI] addSEs [SigmaE, Pair_inject]) 1);
+qed "mem_Sigma_iff";
+Addsimps [mem_Sigma_iff]; 
+
 
 (*** Domain of a relation ***)
 
diff -r f9a9d27e9278 -r 372880456b5b src/HOL/Set.ML
--- a/src/HOL/Set.ML	Tue Mar 26 17:15:54 1996 +0100
+++ b/src/HOL/Set.ML	Wed Mar 27 18:45:17 1996 +0100
@@ -70,10 +70,10 @@
 qed "bexE";
 
 (*Trival rewrite rule;   (! x:A.P)=P holds only if A is nonempty!*)
-val prems = goal Set.thy
-    "(! x:A. True) = True";
+goal Set.thy "(! x:A. True) = True";
 by (REPEAT (ares_tac [TrueI,ballI,iffI] 1));
 qed "ball_rew";
+Addsimps [ball_rew];
 
 (** Congruence rules **)
 
diff -r f9a9d27e9278 -r 372880456b5b src/HOL/WF.ML
--- a/src/HOL/WF.ML	Tue Mar 26 17:15:54 1996 +0100
+++ b/src/HOL/WF.ML	Wed Mar 27 18:45:17 1996 +0100
@@ -46,7 +46,7 @@
 val prems = goal WF.thy "[| wf(r);  (a,a): r |] ==> P";
 by (rtac wf_asym 1);
 by (REPEAT (resolve_tac prems 1));
-qed "wf_anti_refl";
+qed "wf_irrefl";
 
 (*transitive closure of a wf relation is wf! *)
 val [prem] = goal WF.thy "wf(r) ==> wf(r^+)";
diff -r f9a9d27e9278 -r 372880456b5b src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Tue Mar 26 17:15:54 1996 +0100
+++ b/src/HOL/equalities.ML	Wed Mar 27 18:45:17 1996 +0100
@@ -120,6 +120,10 @@
 by (fast_tac eq_cs 1);
 qed "Int_Un_distrib";
 
+goal Set.thy "(B Un C) Int A =  (B Int A) Un (C Int A)";
+by (fast_tac eq_cs 1);
+qed "Int_Un_distrib2";
+
 goal Set.thy "(A<=B) = (A Int B = A)";
 by (fast_tac (eq_cs addSEs [equalityE]) 1);
 qed "subset_Int_eq";