# HG changeset patch
# User nipkow
# Date 867837550 -7200
# Node ID 1e93eb09ebb9c173780776a6c457a03e4b1c6ac3
# Parent  6988394a600871ecec151e5bc6977e6d2a25cb3b
Added the following lemmas tp Divides and a few others to Arith and NatDef:

div_le_mono, div_le_mono2, div_le_dividend, div_less_dividend

Fixed a broken proof in WF_Rel.ML. No idea what caused this.

diff -r 6988394a6008 -r 1e93eb09ebb9 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Tue Jul 01 17:59:36 1997 +0200
+++ b/src/HOL/Arith.ML	Wed Jul 02 11:59:10 1997 +0200
@@ -7,8 +7,6 @@
 Some from the Hoare example from Norbert Galm
 *)
 
-open Arith;
-
 (*** Basic rewrite rules for the arithmetic operators ***)
 
 goalw Arith.thy [pred_def] "pred 0 = 0";
@@ -30,6 +28,16 @@
 qed "Suc_pred";
 Addsimps [Suc_pred];
 
+goal Arith.thy "pred(n) <= (n::nat)";
+by (res_inst_tac [("n","n")] natE 1);
+by (ALLGOALS Asm_simp_tac);
+qed "pred_le";
+AddIffs [pred_le];
+
+goalw Arith.thy [pred_def] "m<=n --> pred(m) <= pred(n)";
+by(simp_tac (!simpset setloop (split_tac[expand_nat_case])) 1);
+qed_spec_mp "pred_le_mono";
+
 (** Difference **)
 
 qed_goalw "diff_0_eq_0" Arith.thy [pred_def]
@@ -605,3 +613,28 @@
 qed "le_add_diff";
 
 
+(** (Anti)Monotonicity of subtraction -- by Stefan Merz **)
+
+(* Monotonicity of subtraction in first argument *)
+goal Arith.thy "!!n::nat. m<=n --> (m-l) <= (n-l)";
+by (induct_tac "n" 1);
+by (Simp_tac 1);
+by (simp_tac (!simpset addsimps [le_Suc_eq]) 1);
+by (rtac impI 1);
+by (etac impE 1);
+by (atac 1);
+by (etac le_trans 1);
+by (res_inst_tac [("m1","n")] (pred_Suc_diff RS subst) 1);
+by (rtac pred_le 1);
+qed_spec_mp "diff_le_mono";
+
+goal Arith.thy "!!n::nat. m<=n ==> (l-n) <= (l-m)";
+by (induct_tac "l" 1);
+by (Simp_tac 1);
+by (case_tac "n <= l" 1);
+by (subgoal_tac "m <= l" 1);
+by (asm_simp_tac (!simpset addsimps [Suc_diff_le]) 1);
+by (fast_tac (!claset addEs [le_trans]) 1);
+by (dtac not_leE 1);
+by (asm_simp_tac (!simpset addsimps [if_Suc_diff_n]) 1);
+qed_spec_mp "diff_le_mono2";
diff -r 6988394a6008 -r 1e93eb09ebb9 src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Tue Jul 01 17:59:36 1997 +0200
+++ b/src/HOL/Divides.ML	Wed Jul 02 11:59:10 1997 +0200
@@ -118,6 +118,80 @@
 by (asm_simp_tac (!simpset addsimps [div_less, div_geq]) 1);
 qed "div_self";
 
+(* Monotonicity of div in first argument *)
+goal thy "!!n. 0<k ==> ALL m. m <= n --> (m div k) <= (n div k)";
+by (res_inst_tac [("n","n")] less_induct 1);
+by (strip_tac 1);
+by (case_tac "na<k" 1);
+(* 1  case n<k *)
+by (subgoal_tac "m<k" 1);
+by (asm_simp_tac (!simpset addsimps [div_less]) 1);
+by (etac le_less_trans 1);
+by (atac 1);
+(* 2  case n >= k *)
+by (case_tac "m<k" 1);
+(* 2.1  case m<k *)
+by (asm_simp_tac (!simpset addsimps [div_less]) 1);
+(* 2.2  case m>=k *)
+by (asm_simp_tac (!simpset addsimps [div_geq]) 1);
+by (REPEAT (eresolve_tac [allE,impE] 1));
+by (REPEAT (eresolve_tac [allE,impE] 2));
+by (atac 3);
+by (asm_simp_tac (!simpset addsimps [diff_less]) 1);
+by (etac diff_le_mono 1);
+qed_spec_mp "div_le_mono";
+
+
+(* Antimonotonicity of div in second argument *)
+goal thy "!!k m n. [| 0<m; m<=n |] ==> (k div n) <= (k div m)";
+by (subgoal_tac "0<n" 1);
+ by(trans_tac 2);
+by (res_inst_tac [("n","k")] less_induct 1);
+by(Simp_tac 1);
+by(rename_tac "k" 1);
+by (case_tac "k<n" 1);
+ by (asm_simp_tac (!simpset addsimps [div_less]) 1);
+by (subgoal_tac "~(k<m)" 1);
+ by(trans_tac 2);
+by (asm_simp_tac (!simpset addsimps [div_geq]) 1);
+by (subgoal_tac "(k-n) div n <= (k-m) div n" 1);
+ by (etac le_trans 1);
+ by (REPEAT (eresolve_tac [allE,impE] 1));
+  by (atac 2);
+ by (asm_simp_tac (!simpset addsimps [diff_less]) 1);
+by (REPEAT (eresolve_tac [div_le_mono,diff_le_mono2] 1));
+qed "div_le_mono2";
+
+goal thy "!!m n. 0<n ==> m div n <= m";
+by (subgoal_tac "m div n <= m div 1" 1);
+by (Asm_full_simp_tac 1);
+by (rtac div_le_mono2 1);
+by (ALLGOALS trans_tac);
+qed "div_le_dividend";
+Addsimps [div_le_dividend];
+
+(* Similar for "less than" *)
+goal thy "!!m n. 1<n ==> (0 < m) --> (m div n < m)";
+by (res_inst_tac [("n","m")] less_induct 1);
+by(Simp_tac 1);
+by(rename_tac "m" 1);
+by (case_tac "m<n" 1);
+ by (asm_full_simp_tac (!simpset addsimps [div_less]) 1);
+by (subgoal_tac "0<n" 1);
+ by(trans_tac 2);
+by (asm_full_simp_tac (!simpset addsimps [div_geq]) 1);
+by (case_tac "n<m" 1);
+ by (subgoal_tac "(m-n) div n < (m-n)" 1);
+  by (REPEAT (ares_tac [impI,less_trans_Suc] 1));
+  by (asm_full_simp_tac (!simpset addsimps [diff_less]) 1);
+ by (dres_inst_tac [("m","n")] less_imp_diff_positive 1);
+ by (asm_full_simp_tac (!simpset addsimps [diff_less]) 1);
+(* case n=m *)
+by (subgoal_tac "m=n" 1);
+ by(trans_tac 2);
+by (asm_simp_tac (!simpset addsimps [div_less]) 1);
+qed_spec_mp "div_less_dividend";
+Addsimps [div_less_dividend];
 
 (*** Further facts about mod (mainly for the mutilated chess board ***)
 
diff -r 6988394a6008 -r 1e93eb09ebb9 src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Tue Jul 01 17:59:36 1997 +0200
+++ b/src/HOL/NatDef.ML	Wed Jul 02 11:59:10 1997 +0200
@@ -289,6 +289,11 @@
 by (blast_tac (!claset addSEs [less_SucE] addIs [less_trans]) 1);
 qed "less_Suc_eq";
 
+goal thy "(n<1) = (n=0)";
+by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
+qed "less_one";
+AddIffs [less_one];
+
 val prems = goal thy "m<n ==> n ~= 0";
 by (res_inst_tac [("n","n")] natE 1);
 by (cut_facts_tac prems 1);
diff -r 6988394a6008 -r 1e93eb09ebb9 src/HOL/WF_Rel.ML
--- a/src/HOL/WF_Rel.ML	Tue Jul 01 17:59:36 1997 +0200
+++ b/src/HOL/WF_Rel.ML	Wed Jul 02 11:59:10 1997 +0200
@@ -92,7 +92,7 @@
 by (rtac (wf_measure RS wf_subset) 1);
 by (simp_tac (!simpset addsimps [measure_def, inv_image_def, less_than_def,
 				 symmetric less_def])1);
-by (fast_tac (!claset addIs [psubset_card]) 1);
+by (fast_tac (!claset addSIs [psubset_card]) 1);
 qed "wf_finite_psubset";
 
 goalw thy [finite_psubset_def, trans_def] "trans finite_psubset";