# HG changeset patch
# User paulson
# Date 1121259980 -7200
# Node ID 140f1e0ea846852970f4a065933b885556835fb3
# Parent  b400b53d8f7dd06910879bfc1de61ce4e947e555
generlization of some "nat" theorems

diff -r b400b53d8f7d -r 140f1e0ea846 src/HOL/Auth/KerberosIV.thy
--- a/src/HOL/Auth/KerberosIV.thy	Wed Jul 13 15:06:04 2005 +0200
+++ b/src/HOL/Auth/KerberosIV.thy	Wed Jul 13 15:06:20 2005 +0200
@@ -1218,7 +1218,7 @@
 lemma NotExpirServ_NotExpirAuth_refined:
      "[| ~ ExpirServ Tt evs; ServLife + Tt <= AuthLife + Tk |]
       ==> ~ ExpirAuth Tk evs"
-by (blast dest: leI le_trans elim: leE)
+by (blast dest: leI le_trans dest: leD)
 
 
 lemma Confidentiality_B:
diff -r b400b53d8f7d -r 140f1e0ea846 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Wed Jul 13 15:06:04 2005 +0200
+++ b/src/HOL/Auth/Message.thy	Wed Jul 13 15:06:20 2005 +0200
@@ -84,11 +84,11 @@
 lemma parts_mono: "G\<subseteq>H ==> parts(G) \<subseteq> parts(H)"
 apply auto
 apply (erule parts.induct) 
-apply (auto dest: Fst Snd Body) 
+apply (blast dest: Fst Snd Body)+
 done
 
 
-(*Equations hold because constructors are injective; cannot prove for all f*)
+text{*Equations hold because constructors are injective; cannot prove for all f*}
 lemma Friend_image_eq [simp]: "(Friend x \<in> Friend`A) = (x:A)"
 by auto
 
diff -r b400b53d8f7d -r 140f1e0ea846 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Wed Jul 13 15:06:04 2005 +0200
+++ b/src/HOL/Divides.thy	Wed Jul 13 15:06:20 2005 +0200
@@ -82,7 +82,7 @@
 
 (*Avoids the ugly ~m<n above*)
 lemma le_mod_geq: "(n::nat) \<le> m ==> m mod n = (m-n) mod n"
-by (simp add: mod_geq not_less_iff_le)
+by (simp add: mod_geq linorder_not_less)
 
 lemma mod_if: "m mod (n::nat) = (if m<n then m else (m-n) mod n)"
 by (simp add: mod_geq)
@@ -149,7 +149,7 @@
 
 (*Avoids the ugly ~m<n above*)
 lemma le_div_geq: "[| 0<n;  n\<le>m |] ==> m div n = Suc((m-n) div n)"
-by (simp add: div_geq not_less_iff_le)
+by (simp add: div_geq linorder_not_less)
 
 lemma div_if: "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))"
 by (simp add: div_geq)
@@ -483,7 +483,7 @@
 (* case Suc(na) < n *)
 apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
 (* case n \<le> Suc(na) *)
-apply (simp add: not_less_iff_le le_Suc_eq mod_geq)
+apply (simp add: linorder_not_less le_Suc_eq mod_geq)
 apply (auto simp add: Suc_diff_le le_mod_geq)
 done
 
@@ -545,7 +545,7 @@
 done
 
 lemma dvd_diffD: "[| k dvd m-n; k dvd n; n\<le>m |] ==> k dvd (m::nat)"
-apply (erule not_less_iff_le [THEN iffD2, THEN add_diff_inverse, THEN subst])
+apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
 apply (blast intro: dvd_add)
 done
 
diff -r b400b53d8f7d -r 140f1e0ea846 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Wed Jul 13 15:06:04 2005 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Wed Jul 13 15:06:20 2005 +0200
@@ -336,7 +336,7 @@
     "P k ==> \<exists>x. P x & (\<forall>y. P y --> m x <= (m y::nat))"
   apply (simp only: pred_nat_trancl_eq_le [symmetric])
   apply (rule wf_pred_nat [THEN wf_linord_ex_has_least])
-   apply (simp add: less_eq not_le_iff_less pred_nat_trancl_eq_le, assumption)
+   apply (simp add: less_eq linorder_not_le pred_nat_trancl_eq_le, assumption)
   done
 
 lemma LeastM_nat_lemma:
diff -r b400b53d8f7d -r 140f1e0ea846 src/HOL/Hoare/Examples.thy
--- a/src/HOL/Hoare/Examples.thy	Wed Jul 13 15:06:04 2005 +0200
+++ b/src/HOL/Hoare/Examples.thy	Wed Jul 13 15:06:20 2005 +0200
@@ -50,7 +50,7 @@
 (*Now prove the verification conditions*)
   apply auto
   apply(simp add: gcd_diff_r less_imp_le)
- apply(simp add: not_less_iff_le gcd_diff_l)
+ apply(simp add: linorder_not_less gcd_diff_l)
 apply(erule gcd_nnn)
 done
 
@@ -72,7 +72,7 @@
  {a = gcd A B & 2*A*B = a*(x+y)}"
 apply vcg
   apply simp
- apply(simp add: distribs gcd_diff_r not_less_iff_le gcd_diff_l)
+ apply(simp add: distribs gcd_diff_r linorder_not_less gcd_diff_l)
 apply(simp add: distribs gcd_nnn)
 done
 
diff -r b400b53d8f7d -r 140f1e0ea846 src/HOL/Import/HOL/arithmetic.imp
--- a/src/HOL/Import/HOL/arithmetic.imp	Wed Jul 13 15:06:04 2005 +0200
+++ b/src/HOL/Import/HOL/arithmetic.imp	Wed Jul 13 15:06:20 2005 +0200
@@ -101,11 +101,11 @@
   "NOT_SUC_ADD_LESS_EQ" > "HOL4Base.arithmetic.NOT_SUC_ADD_LESS_EQ"
   "NOT_ODD_EQ_EVEN" > "HOL4Base.arithmetic.NOT_ODD_EQ_EVEN"
   "NOT_NUM_EQ" > "HOL4Base.arithmetic.NOT_NUM_EQ"
-  "NOT_LESS_EQUAL" > "Nat.not_le_iff_less"
-  "NOT_LESS" > "Nat.not_less_iff_le"
+  "NOT_LESS_EQUAL" > "Orderings.linorder_not_le"
+  "NOT_LESS" > "Orderings.linorder_not_less"
   "NOT_LEQ" > "HOL4Base.arithmetic.NOT_LEQ"
   "NOT_GREATER_EQ" > "HOL4Base.arithmetic.NOT_GREATER_EQ"
-  "NOT_GREATER" > "Nat.not_less_iff_le"
+  "NOT_GREATER" > "Orderings.linorder_not_less"
   "NOT_EXP_0" > "HOL4Base.arithmetic.NOT_EXP_0"
   "NORM_0" > "HOL4Base.arithmetic.NORM_0"
   "MULT_SYM" > "Nat.nat_mult_commute"
diff -r b400b53d8f7d -r 140f1e0ea846 src/HOL/Infinite_Set.thy
--- a/src/HOL/Infinite_Set.thy	Wed Jul 13 15:06:04 2005 +0200
+++ b/src/HOL/Infinite_Set.thy	Wed Jul 13 15:06:20 2005 +0200
@@ -127,7 +127,7 @@
     assume "\<not> ?rhs"
     then obtain m where m: "\<forall>n. m<n \<longrightarrow> n\<notin>S" by blast
     hence "S \<subseteq> {..m}"
-      by (auto simp add: sym[OF not_less_iff_le])
+      by (auto simp add: sym[OF linorder_not_less])
     with inf show "False" 
       by (simp add: finite_nat_iff_bounded_le)
   qed
diff -r b400b53d8f7d -r 140f1e0ea846 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Wed Jul 13 15:06:04 2005 +0200
+++ b/src/HOL/Library/Word.thy	Wed Jul 13 15:06:20 2005 +0200
@@ -2248,7 +2248,7 @@
 	hence "ys ! (length ys - Suc n) = rev ys ! n"
 	  ..
 	thus "(y # ys) ! (length ys - n) = rev ys ! n"
-	  by (simp add: nth_Cons' noty not_less_iff_le [symmetric])
+	  by (simp add: nth_Cons' noty linorder_not_less [symmetric])
       next
 	assume "~ n < length ys"
 	hence x: "length ys \<le> n"
diff -r b400b53d8f7d -r 140f1e0ea846 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Wed Jul 13 15:06:04 2005 +0200
+++ b/src/HOL/Nat.ML	Wed Jul 13 15:06:20 2005 +0200
@@ -25,6 +25,9 @@
 bind_thm ("nat_case_0", nat_case_0);
 bind_thm ("nat_case_Suc", nat_case_Suc);
 
+val leD = thm "leD";  (*Now defined in Orderings.thy*)
+val leI = thm "leI";
+
 val Least_Suc = thm "Least_Suc";
 val Least_Suc2 = thm "Least_Suc2";
 val One_nat_def = thm "One_nat_def";
@@ -112,9 +115,6 @@
 val gr_implies_not0 = thm "gr_implies_not0";
 val inj_Suc = thm "inj_Suc";
 val le0 = thm "le0";
-val leD = thm "leD";
-val leE = thm "leE";
-val leI = thm "leI";
 val le_0_eq = thm "le_0_eq";
 val le_SucE = thm "le_SucE";
 val le_SucI = thm "le_SucI";
@@ -212,10 +212,8 @@
 val not_add_less2 = thm "not_add_less2";
 val not_gr0 = thm "not_gr0";
 val not_leE = thm "not_leE";
-val not_le_iff_less = thm "not_le_iff_less";
 val not_less0 = thm "not_less0";
 val not_less_eq = thm "not_less_eq";
-val not_less_iff_le = thm "not_less_iff_le";
 val not_less_less_Suc_eq = thm "not_less_less_Suc_eq";
 val not_less_simps = thms "not_less_simps";
 val one_eq_mult_iff = thm "one_eq_mult_iff";
diff -r b400b53d8f7d -r 140f1e0ea846 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed Jul 13 15:06:04 2005 +0200
+++ b/src/HOL/Nat.thy	Wed Jul 13 15:06:20 2005 +0200
@@ -342,22 +342,6 @@
 lemma le_SucE: "m \<le> Suc n ==> (m \<le> n ==> R) ==> (m = Suc n ==> R) ==> R"
   by (drule le_Suc_eq [THEN iffD1], rules+)
 
-lemma leI: "~ n < m ==> m \<le> (n::nat)" by (simp add: le_def)
-
-lemma leD: "m \<le> n ==> ~ n < (m::nat)"
-  by (simp add: le_def)
-
-lemmas leE = leD [elim_format]
-
-lemma not_less_iff_le: "(~ n < m) = (m \<le> (n::nat))"
-  by (blast intro: leI elim: leE)
-
-lemma not_leE: "~ m \<le> n ==> n<(m::nat)"
-  by (simp add: le_def)
-
-lemma not_le_iff_less: "(~ n \<le> m) = (m < (n::nat))"
-  by (simp add: le_def)
-
 lemma Suc_leI: "m < n ==> Suc(m) \<le> n"
   apply (simp add: le_def less_Suc_eq)
   apply (blast elim!: less_irrefl less_asym)
@@ -853,7 +837,7 @@
   by (induct m n rule: diff_induct) simp_all
 
 lemma le_add_diff_inverse [simp]: "n \<le> m ==> n + (m - n) = (m::nat)"
-  by (simp add: add_diff_inverse not_less_iff_le)
+  by (simp add: add_diff_inverse linorder_not_less)
 
 lemma le_add_diff_inverse2 [simp]: "n \<le> m ==> (m - n) + n = (m::nat)"
   by (simp add: le_add_diff_inverse add_commute)
diff -r b400b53d8f7d -r 140f1e0ea846 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Wed Jul 13 15:06:04 2005 +0200
+++ b/src/HOL/Orderings.thy	Wed Jul 13 15:06:20 2005 +0200
@@ -269,6 +269,17 @@
 lemma linorder_antisym_conv3: "~ (y::'a::linorder) < x ==> (~ x < y) = (x = y)"
 by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1])
 
+text{*Replacing the old Nat.leI*}
+lemma leI: "~ x < y ==> y <= (x::'a::linorder)"
+  by (simp only: linorder_not_less)
+
+lemma leD: "y <= (x::'a::linorder) ==> ~ x < y"
+  by (simp only: linorder_not_less)
+
+(*FIXME inappropriate name (or delete altogether)*)
+lemma not_leE: "~ y <= (x::'a::linorder) ==> x < y"
+  by (simp only: linorder_not_le)
+
 use "antisym_setup.ML";
 setup antisym_setup
 
diff -r b400b53d8f7d -r 140f1e0ea846 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Wed Jul 13 15:06:04 2005 +0200
+++ b/src/HOL/Power.thy	Wed Jul 13 15:06:20 2005 +0200
@@ -324,7 +324,7 @@
 
 lemma le_imp_power_dvd: "!!i::nat. m \<le> n ==> i^m dvd i^n"
 apply (unfold dvd_def)
-apply (erule not_less_iff_le [THEN iffD2, THEN add_diff_inverse, THEN subst])
+apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
 apply (simp add: power_add)
 done
 
diff -r b400b53d8f7d -r 140f1e0ea846 src/HOL/UNITY/Simple/Reach.thy
--- a/src/HOL/UNITY/Simple/Reach.thy	Wed Jul 13 15:06:04 2005 +0200
+++ b/src/HOL/UNITY/Simple/Reach.thy	Wed Jul 13 15:06:20 2005 +0200
@@ -138,7 +138,7 @@
 apply (rule LeadsTo_UN, auto)
 apply (ensures_tac "asgt a b")
  prefer 2 apply blast
-apply (simp (no_asm_use) add: not_less_iff_le)
+apply (simp (no_asm_use) add: linorder_not_less)
 apply (drule metric_le [THEN order_antisym]) 
 apply (auto elim: less_not_refl3 [THEN [2] rev_notE])
 done