--- 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:
--- 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
--- 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
--- 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:
--- 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
--- 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"
--- 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
--- 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"
--- 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";
--- 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)
--- 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
--- 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
--- 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