generlization of some "nat" theorems
authorpaulson
Wed Jul 13 15:06:20 2005 +0200 (2005-07-13)
changeset 16796140f1e0ea846
parent 16795 b400b53d8f7d
child 16797 6109d4020420
generlization of some "nat" theorems
src/HOL/Auth/KerberosIV.thy
src/HOL/Auth/Message.thy
src/HOL/Divides.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Hoare/Examples.thy
src/HOL/Import/HOL/arithmetic.imp
src/HOL/Infinite_Set.thy
src/HOL/Library/Word.thy
src/HOL/Nat.ML
src/HOL/Nat.thy
src/HOL/Orderings.thy
src/HOL/Power.thy
src/HOL/UNITY/Simple/Reach.thy
     1.1 --- a/src/HOL/Auth/KerberosIV.thy	Wed Jul 13 15:06:04 2005 +0200
     1.2 +++ b/src/HOL/Auth/KerberosIV.thy	Wed Jul 13 15:06:20 2005 +0200
     1.3 @@ -1218,7 +1218,7 @@
     1.4  lemma NotExpirServ_NotExpirAuth_refined:
     1.5       "[| ~ ExpirServ Tt evs; ServLife + Tt <= AuthLife + Tk |]
     1.6        ==> ~ ExpirAuth Tk evs"
     1.7 -by (blast dest: leI le_trans elim: leE)
     1.8 +by (blast dest: leI le_trans dest: leD)
     1.9  
    1.10  
    1.11  lemma Confidentiality_B:
     2.1 --- a/src/HOL/Auth/Message.thy	Wed Jul 13 15:06:04 2005 +0200
     2.2 +++ b/src/HOL/Auth/Message.thy	Wed Jul 13 15:06:20 2005 +0200
     2.3 @@ -84,11 +84,11 @@
     2.4  lemma parts_mono: "G\<subseteq>H ==> parts(G) \<subseteq> parts(H)"
     2.5  apply auto
     2.6  apply (erule parts.induct) 
     2.7 -apply (auto dest: Fst Snd Body) 
     2.8 +apply (blast dest: Fst Snd Body)+
     2.9  done
    2.10  
    2.11  
    2.12 -(*Equations hold because constructors are injective; cannot prove for all f*)
    2.13 +text{*Equations hold because constructors are injective; cannot prove for all f*}
    2.14  lemma Friend_image_eq [simp]: "(Friend x \<in> Friend`A) = (x:A)"
    2.15  by auto
    2.16  
     3.1 --- a/src/HOL/Divides.thy	Wed Jul 13 15:06:04 2005 +0200
     3.2 +++ b/src/HOL/Divides.thy	Wed Jul 13 15:06:20 2005 +0200
     3.3 @@ -82,7 +82,7 @@
     3.4  
     3.5  (*Avoids the ugly ~m<n above*)
     3.6  lemma le_mod_geq: "(n::nat) \<le> m ==> m mod n = (m-n) mod n"
     3.7 -by (simp add: mod_geq not_less_iff_le)
     3.8 +by (simp add: mod_geq linorder_not_less)
     3.9  
    3.10  lemma mod_if: "m mod (n::nat) = (if m<n then m else (m-n) mod n)"
    3.11  by (simp add: mod_geq)
    3.12 @@ -149,7 +149,7 @@
    3.13  
    3.14  (*Avoids the ugly ~m<n above*)
    3.15  lemma le_div_geq: "[| 0<n;  n\<le>m |] ==> m div n = Suc((m-n) div n)"
    3.16 -by (simp add: div_geq not_less_iff_le)
    3.17 +by (simp add: div_geq linorder_not_less)
    3.18  
    3.19  lemma div_if: "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))"
    3.20  by (simp add: div_geq)
    3.21 @@ -483,7 +483,7 @@
    3.22  (* case Suc(na) < n *)
    3.23  apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
    3.24  (* case n \<le> Suc(na) *)
    3.25 -apply (simp add: not_less_iff_le le_Suc_eq mod_geq)
    3.26 +apply (simp add: linorder_not_less le_Suc_eq mod_geq)
    3.27  apply (auto simp add: Suc_diff_le le_mod_geq)
    3.28  done
    3.29  
    3.30 @@ -545,7 +545,7 @@
    3.31  done
    3.32  
    3.33  lemma dvd_diffD: "[| k dvd m-n; k dvd n; n\<le>m |] ==> k dvd (m::nat)"
    3.34 -apply (erule not_less_iff_le [THEN iffD2, THEN add_diff_inverse, THEN subst])
    3.35 +apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
    3.36  apply (blast intro: dvd_add)
    3.37  done
    3.38  
     4.1 --- a/src/HOL/Hilbert_Choice.thy	Wed Jul 13 15:06:04 2005 +0200
     4.2 +++ b/src/HOL/Hilbert_Choice.thy	Wed Jul 13 15:06:20 2005 +0200
     4.3 @@ -336,7 +336,7 @@
     4.4      "P k ==> \<exists>x. P x & (\<forall>y. P y --> m x <= (m y::nat))"
     4.5    apply (simp only: pred_nat_trancl_eq_le [symmetric])
     4.6    apply (rule wf_pred_nat [THEN wf_linord_ex_has_least])
     4.7 -   apply (simp add: less_eq not_le_iff_less pred_nat_trancl_eq_le, assumption)
     4.8 +   apply (simp add: less_eq linorder_not_le pred_nat_trancl_eq_le, assumption)
     4.9    done
    4.10  
    4.11  lemma LeastM_nat_lemma:
     5.1 --- a/src/HOL/Hoare/Examples.thy	Wed Jul 13 15:06:04 2005 +0200
     5.2 +++ b/src/HOL/Hoare/Examples.thy	Wed Jul 13 15:06:20 2005 +0200
     5.3 @@ -50,7 +50,7 @@
     5.4  (*Now prove the verification conditions*)
     5.5    apply auto
     5.6    apply(simp add: gcd_diff_r less_imp_le)
     5.7 - apply(simp add: not_less_iff_le gcd_diff_l)
     5.8 + apply(simp add: linorder_not_less gcd_diff_l)
     5.9  apply(erule gcd_nnn)
    5.10  done
    5.11  
    5.12 @@ -72,7 +72,7 @@
    5.13   {a = gcd A B & 2*A*B = a*(x+y)}"
    5.14  apply vcg
    5.15    apply simp
    5.16 - apply(simp add: distribs gcd_diff_r not_less_iff_le gcd_diff_l)
    5.17 + apply(simp add: distribs gcd_diff_r linorder_not_less gcd_diff_l)
    5.18  apply(simp add: distribs gcd_nnn)
    5.19  done
    5.20  
     6.1 --- a/src/HOL/Import/HOL/arithmetic.imp	Wed Jul 13 15:06:04 2005 +0200
     6.2 +++ b/src/HOL/Import/HOL/arithmetic.imp	Wed Jul 13 15:06:20 2005 +0200
     6.3 @@ -101,11 +101,11 @@
     6.4    "NOT_SUC_ADD_LESS_EQ" > "HOL4Base.arithmetic.NOT_SUC_ADD_LESS_EQ"
     6.5    "NOT_ODD_EQ_EVEN" > "HOL4Base.arithmetic.NOT_ODD_EQ_EVEN"
     6.6    "NOT_NUM_EQ" > "HOL4Base.arithmetic.NOT_NUM_EQ"
     6.7 -  "NOT_LESS_EQUAL" > "Nat.not_le_iff_less"
     6.8 -  "NOT_LESS" > "Nat.not_less_iff_le"
     6.9 +  "NOT_LESS_EQUAL" > "Orderings.linorder_not_le"
    6.10 +  "NOT_LESS" > "Orderings.linorder_not_less"
    6.11    "NOT_LEQ" > "HOL4Base.arithmetic.NOT_LEQ"
    6.12    "NOT_GREATER_EQ" > "HOL4Base.arithmetic.NOT_GREATER_EQ"
    6.13 -  "NOT_GREATER" > "Nat.not_less_iff_le"
    6.14 +  "NOT_GREATER" > "Orderings.linorder_not_less"
    6.15    "NOT_EXP_0" > "HOL4Base.arithmetic.NOT_EXP_0"
    6.16    "NORM_0" > "HOL4Base.arithmetic.NORM_0"
    6.17    "MULT_SYM" > "Nat.nat_mult_commute"
     7.1 --- a/src/HOL/Infinite_Set.thy	Wed Jul 13 15:06:04 2005 +0200
     7.2 +++ b/src/HOL/Infinite_Set.thy	Wed Jul 13 15:06:20 2005 +0200
     7.3 @@ -127,7 +127,7 @@
     7.4      assume "\<not> ?rhs"
     7.5      then obtain m where m: "\<forall>n. m<n \<longrightarrow> n\<notin>S" by blast
     7.6      hence "S \<subseteq> {..m}"
     7.7 -      by (auto simp add: sym[OF not_less_iff_le])
     7.8 +      by (auto simp add: sym[OF linorder_not_less])
     7.9      with inf show "False" 
    7.10        by (simp add: finite_nat_iff_bounded_le)
    7.11    qed
     8.1 --- a/src/HOL/Library/Word.thy	Wed Jul 13 15:06:04 2005 +0200
     8.2 +++ b/src/HOL/Library/Word.thy	Wed Jul 13 15:06:20 2005 +0200
     8.3 @@ -2248,7 +2248,7 @@
     8.4  	hence "ys ! (length ys - Suc n) = rev ys ! n"
     8.5  	  ..
     8.6  	thus "(y # ys) ! (length ys - n) = rev ys ! n"
     8.7 -	  by (simp add: nth_Cons' noty not_less_iff_le [symmetric])
     8.8 +	  by (simp add: nth_Cons' noty linorder_not_less [symmetric])
     8.9        next
    8.10  	assume "~ n < length ys"
    8.11  	hence x: "length ys \<le> n"
     9.1 --- a/src/HOL/Nat.ML	Wed Jul 13 15:06:04 2005 +0200
     9.2 +++ b/src/HOL/Nat.ML	Wed Jul 13 15:06:20 2005 +0200
     9.3 @@ -25,6 +25,9 @@
     9.4  bind_thm ("nat_case_0", nat_case_0);
     9.5  bind_thm ("nat_case_Suc", nat_case_Suc);
     9.6  
     9.7 +val leD = thm "leD";  (*Now defined in Orderings.thy*)
     9.8 +val leI = thm "leI";
     9.9 +
    9.10  val Least_Suc = thm "Least_Suc";
    9.11  val Least_Suc2 = thm "Least_Suc2";
    9.12  val One_nat_def = thm "One_nat_def";
    9.13 @@ -112,9 +115,6 @@
    9.14  val gr_implies_not0 = thm "gr_implies_not0";
    9.15  val inj_Suc = thm "inj_Suc";
    9.16  val le0 = thm "le0";
    9.17 -val leD = thm "leD";
    9.18 -val leE = thm "leE";
    9.19 -val leI = thm "leI";
    9.20  val le_0_eq = thm "le_0_eq";
    9.21  val le_SucE = thm "le_SucE";
    9.22  val le_SucI = thm "le_SucI";
    9.23 @@ -212,10 +212,8 @@
    9.24  val not_add_less2 = thm "not_add_less2";
    9.25  val not_gr0 = thm "not_gr0";
    9.26  val not_leE = thm "not_leE";
    9.27 -val not_le_iff_less = thm "not_le_iff_less";
    9.28  val not_less0 = thm "not_less0";
    9.29  val not_less_eq = thm "not_less_eq";
    9.30 -val not_less_iff_le = thm "not_less_iff_le";
    9.31  val not_less_less_Suc_eq = thm "not_less_less_Suc_eq";
    9.32  val not_less_simps = thms "not_less_simps";
    9.33  val one_eq_mult_iff = thm "one_eq_mult_iff";
    10.1 --- a/src/HOL/Nat.thy	Wed Jul 13 15:06:04 2005 +0200
    10.2 +++ b/src/HOL/Nat.thy	Wed Jul 13 15:06:20 2005 +0200
    10.3 @@ -342,22 +342,6 @@
    10.4  lemma le_SucE: "m \<le> Suc n ==> (m \<le> n ==> R) ==> (m = Suc n ==> R) ==> R"
    10.5    by (drule le_Suc_eq [THEN iffD1], rules+)
    10.6  
    10.7 -lemma leI: "~ n < m ==> m \<le> (n::nat)" by (simp add: le_def)
    10.8 -
    10.9 -lemma leD: "m \<le> n ==> ~ n < (m::nat)"
   10.10 -  by (simp add: le_def)
   10.11 -
   10.12 -lemmas leE = leD [elim_format]
   10.13 -
   10.14 -lemma not_less_iff_le: "(~ n < m) = (m \<le> (n::nat))"
   10.15 -  by (blast intro: leI elim: leE)
   10.16 -
   10.17 -lemma not_leE: "~ m \<le> n ==> n<(m::nat)"
   10.18 -  by (simp add: le_def)
   10.19 -
   10.20 -lemma not_le_iff_less: "(~ n \<le> m) = (m < (n::nat))"
   10.21 -  by (simp add: le_def)
   10.22 -
   10.23  lemma Suc_leI: "m < n ==> Suc(m) \<le> n"
   10.24    apply (simp add: le_def less_Suc_eq)
   10.25    apply (blast elim!: less_irrefl less_asym)
   10.26 @@ -853,7 +837,7 @@
   10.27    by (induct m n rule: diff_induct) simp_all
   10.28  
   10.29  lemma le_add_diff_inverse [simp]: "n \<le> m ==> n + (m - n) = (m::nat)"
   10.30 -  by (simp add: add_diff_inverse not_less_iff_le)
   10.31 +  by (simp add: add_diff_inverse linorder_not_less)
   10.32  
   10.33  lemma le_add_diff_inverse2 [simp]: "n \<le> m ==> (m - n) + n = (m::nat)"
   10.34    by (simp add: le_add_diff_inverse add_commute)
    11.1 --- a/src/HOL/Orderings.thy	Wed Jul 13 15:06:04 2005 +0200
    11.2 +++ b/src/HOL/Orderings.thy	Wed Jul 13 15:06:20 2005 +0200
    11.3 @@ -269,6 +269,17 @@
    11.4  lemma linorder_antisym_conv3: "~ (y::'a::linorder) < x ==> (~ x < y) = (x = y)"
    11.5  by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1])
    11.6  
    11.7 +text{*Replacing the old Nat.leI*}
    11.8 +lemma leI: "~ x < y ==> y <= (x::'a::linorder)"
    11.9 +  by (simp only: linorder_not_less)
   11.10 +
   11.11 +lemma leD: "y <= (x::'a::linorder) ==> ~ x < y"
   11.12 +  by (simp only: linorder_not_less)
   11.13 +
   11.14 +(*FIXME inappropriate name (or delete altogether)*)
   11.15 +lemma not_leE: "~ y <= (x::'a::linorder) ==> x < y"
   11.16 +  by (simp only: linorder_not_le)
   11.17 +
   11.18  use "antisym_setup.ML";
   11.19  setup antisym_setup
   11.20  
    12.1 --- a/src/HOL/Power.thy	Wed Jul 13 15:06:04 2005 +0200
    12.2 +++ b/src/HOL/Power.thy	Wed Jul 13 15:06:20 2005 +0200
    12.3 @@ -324,7 +324,7 @@
    12.4  
    12.5  lemma le_imp_power_dvd: "!!i::nat. m \<le> n ==> i^m dvd i^n"
    12.6  apply (unfold dvd_def)
    12.7 -apply (erule not_less_iff_le [THEN iffD2, THEN add_diff_inverse, THEN subst])
    12.8 +apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
    12.9  apply (simp add: power_add)
   12.10  done
   12.11  
    13.1 --- a/src/HOL/UNITY/Simple/Reach.thy	Wed Jul 13 15:06:04 2005 +0200
    13.2 +++ b/src/HOL/UNITY/Simple/Reach.thy	Wed Jul 13 15:06:20 2005 +0200
    13.3 @@ -138,7 +138,7 @@
    13.4  apply (rule LeadsTo_UN, auto)
    13.5  apply (ensures_tac "asgt a b")
    13.6   prefer 2 apply blast
    13.7 -apply (simp (no_asm_use) add: not_less_iff_le)
    13.8 +apply (simp (no_asm_use) add: linorder_not_less)
    13.9  apply (drule metric_le [THEN order_antisym]) 
   13.10  apply (auto elim: less_not_refl3 [THEN [2] rev_notE])
   13.11  done