explicit equivalence for strict order on lattices
authorhaftmann
Sun Feb 15 17:01:22 2015 +0100 (2015-02-15)
changeset 5954512a6088ed195
parent 59544 792691e4b311
child 59546 3850a2d20f19
explicit equivalence for strict order on lattices
src/HOL/GCD.thy
src/HOL/Lattices.thy
src/HOL/Number_Theory/Gauss.thy
     1.1 --- a/src/HOL/GCD.thy	Sun Feb 15 08:17:46 2015 +0100
     1.2 +++ b/src/HOL/GCD.thy	Sun Feb 15 17:01:22 2015 +0100
     1.3 @@ -334,8 +334,7 @@
     1.4    + gcd_nat: semilattice_neutr_order "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat" 0 "op dvd" "(\<lambda>m n. m dvd n \<and> \<not> n dvd m)"
     1.5  apply default
     1.6  apply (auto intro: dvd_antisym dvd_trans)[4]
     1.7 -apply (metis dvd.dual_order.refl gcd_unique_nat)
     1.8 -apply (auto intro: dvdI elim: dvdE)
     1.9 +apply (metis dvd.dual_order.refl gcd_unique_nat)+
    1.10  done
    1.11  
    1.12  interpretation gcd_int: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int"
     2.1 --- a/src/HOL/Lattices.thy	Sun Feb 15 08:17:46 2015 +0100
     2.2 +++ b/src/HOL/Lattices.thy	Sun Feb 15 17:01:22 2015 +0100
     2.3 @@ -37,7 +37,7 @@
     2.4    fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<preceq>" 50)
     2.5      and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<prec>" 50)
     2.6    assumes order_iff: "a \<preceq> b \<longleftrightarrow> a = a * b"
     2.7 -    and semilattice_strict_iff_order: "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
     2.8 +    and strict_order_iff: "a \<prec> b \<longleftrightarrow> a = a * b \<and> a \<noteq> b"
     2.9  begin
    2.10  
    2.11  lemma orderI:
    2.12 @@ -53,7 +53,7 @@
    2.13  proof
    2.14    fix a b
    2.15    show "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
    2.16 -    by (fact semilattice_strict_iff_order)
    2.17 +    by (simp add: order_iff strict_order_iff)
    2.18  next
    2.19    fix a
    2.20    show "a \<preceq> a"
     3.1 --- a/src/HOL/Number_Theory/Gauss.thy	Sun Feb 15 08:17:46 2015 +0100
     3.2 +++ b/src/HOL/Number_Theory/Gauss.thy	Sun Feb 15 17:01:22 2015 +0100
     3.3 @@ -161,8 +161,7 @@
     3.4  
     3.5  lemma nonzero_mod_p:
     3.6    fixes x::int shows "\<lbrakk>0 < x; x < int p\<rbrakk> \<Longrightarrow> [x \<noteq> 0](mod p)"
     3.7 -by (metis Nat_Transfer.transfer_nat_int_function_closures(9) cong_less_imp_eq_int 
     3.8 -     inf.semilattice_strict_iff_order int_less_0_conv le_numeral_extra(3) zero_less_imp_eq_int)
     3.9 +  by (simp add: cong_int_def)
    3.10  
    3.11  lemma A_ncong_p: "x \<in> A \<Longrightarrow> [x \<noteq> 0](mod p)"
    3.12    by (rule nonzero_mod_p) (auto simp add: A_def)