# HG changeset patch
# User haftmann
# Date 1424016082 -3600
# Node ID 12a6088ed195b3e7f1e092119314ec3f050ee82d
# Parent  792691e4b311bb425560a399e14710903972d4f9
explicit equivalence for strict order on lattices

diff -r 792691e4b311 -r 12a6088ed195 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sun Feb 15 08:17:46 2015 +0100
+++ b/src/HOL/GCD.thy	Sun Feb 15 17:01:22 2015 +0100
@@ -334,8 +334,7 @@
   + 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)"
 apply default
 apply (auto intro: dvd_antisym dvd_trans)[4]
-apply (metis dvd.dual_order.refl gcd_unique_nat)
-apply (auto intro: dvdI elim: dvdE)
+apply (metis dvd.dual_order.refl gcd_unique_nat)+
 done
 
 interpretation gcd_int: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int"
diff -r 792691e4b311 -r 12a6088ed195 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Sun Feb 15 08:17:46 2015 +0100
+++ b/src/HOL/Lattices.thy	Sun Feb 15 17:01:22 2015 +0100
@@ -37,7 +37,7 @@
   fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<preceq>" 50)
     and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<prec>" 50)
   assumes order_iff: "a \<preceq> b \<longleftrightarrow> a = a * b"
-    and semilattice_strict_iff_order: "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
+    and strict_order_iff: "a \<prec> b \<longleftrightarrow> a = a * b \<and> a \<noteq> b"
 begin
 
 lemma orderI:
@@ -53,7 +53,7 @@
 proof
   fix a b
   show "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
-    by (fact semilattice_strict_iff_order)
+    by (simp add: order_iff strict_order_iff)
 next
   fix a
   show "a \<preceq> a"
diff -r 792691e4b311 -r 12a6088ed195 src/HOL/Number_Theory/Gauss.thy
--- a/src/HOL/Number_Theory/Gauss.thy	Sun Feb 15 08:17:46 2015 +0100
+++ b/src/HOL/Number_Theory/Gauss.thy	Sun Feb 15 17:01:22 2015 +0100
@@ -161,8 +161,7 @@
 
 lemma nonzero_mod_p:
   fixes x::int shows "\<lbrakk>0 < x; x < int p\<rbrakk> \<Longrightarrow> [x \<noteq> 0](mod p)"
-by (metis Nat_Transfer.transfer_nat_int_function_closures(9) cong_less_imp_eq_int 
-     inf.semilattice_strict_iff_order int_less_0_conv le_numeral_extra(3) zero_less_imp_eq_int)
+  by (simp add: cong_int_def)
 
 lemma A_ncong_p: "x \<in> A \<Longrightarrow> [x \<noteq> 0](mod p)"
   by (rule nonzero_mod_p) (auto simp add: A_def)