# HG changeset patch
# User haftmann
# Date 1492952013 -7200
# Node ID 85ed070017b7465118aecf638a20314c37450fe3
# Parent  a04afc400156c3d68a91aeeeae51426ad7da25b0
include GCD as integral part of computational algebra in session HOL

diff -r a04afc400156 -r 85ed070017b7 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sun Apr 23 14:27:22 2017 +0200
+++ b/src/HOL/GCD.thy	Sun Apr 23 14:53:33 2017 +0200
@@ -31,21 +31,21 @@
 section \<open>Greatest common divisor and least common multiple\<close>
 
 theory GCD
-  imports Pre_Main
+  imports Groups_List 
 begin
 
 subsection \<open>Abstract bounded quasi semilattices as common foundation\<close>
 
 locale bounded_quasi_semilattice = abel_semigroup +
-  fixes top :: 'a  ("\<top>") and bot :: 'a  ("\<bottom>")
+  fixes top :: 'a  ("\<^bold>\<top>") and bot :: 'a  ("\<^bold>\<bottom>")
     and normalize :: "'a \<Rightarrow> 'a"
   assumes idem_normalize [simp]: "a \<^bold>* a = normalize a"
     and normalize_left_idem [simp]: "normalize a \<^bold>* b = a \<^bold>* b"
     and normalize_idem [simp]: "normalize (a \<^bold>* b) = a \<^bold>* b"
-    and normalize_top [simp]: "normalize \<top> = \<top>"
-    and normalize_bottom [simp]: "normalize \<bottom> = \<bottom>"
-    and top_left_normalize [simp]: "\<top> \<^bold>* a = normalize a"
-    and bottom_left_bottom [simp]: "\<bottom> \<^bold>* a = \<bottom>"
+    and normalize_top [simp]: "normalize \<^bold>\<top> = \<^bold>\<top>"
+    and normalize_bottom [simp]: "normalize \<^bold>\<bottom> = \<^bold>\<bottom>"
+    and top_left_normalize [simp]: "\<^bold>\<top> \<^bold>* a = normalize a"
+    and bottom_left_bottom [simp]: "\<^bold>\<bottom> \<^bold>* a = \<^bold>\<bottom>"
 begin
 
 lemma left_idem [simp]:
@@ -63,11 +63,11 @@
   by (fact comp_fun_idem)
 
 lemma top_right_normalize [simp]:
-  "a \<^bold>* \<top> = normalize a"
+  "a \<^bold>* \<^bold>\<top> = normalize a"
   using top_left_normalize [of a] by (simp add: ac_simps)
 
 lemma bottom_right_bottom [simp]:
-  "a \<^bold>* \<bottom> = \<bottom>"
+  "a \<^bold>* \<^bold>\<bottom> = \<^bold>\<bottom>"
   using bottom_left_bottom [of a] by (simp add: ac_simps)
 
 lemma normalize_right_idem [simp]:
@@ -84,18 +84,18 @@
 
 definition F :: "'a set \<Rightarrow> 'a"
 where
-  eq_fold: "F A = (if finite A then Finite_Set.fold f \<top> A else \<bottom>)"
+  eq_fold: "F A = (if finite A then Finite_Set.fold f \<^bold>\<top> A else \<^bold>\<bottom>)"
+
+lemma infinite [simp]:
+  "infinite A \<Longrightarrow> F A = \<^bold>\<bottom>"
+  by (simp add: eq_fold)
 
 lemma set_eq_fold [code]:
-  "F (set xs) = fold f xs \<top>"
+  "F (set xs) = fold f xs \<^bold>\<top>"
   by (simp add: eq_fold fold_set_fold)
 
-lemma infinite [simp]:
-  "infinite A \<Longrightarrow> F A = \<bottom>"
-  by (simp add: eq_fold)
-
 lemma empty [simp]:
-  "F {} = \<top>"
+  "F {} = \<^bold>\<top>"
   by (simp add: eq_fold)
 
 lemma insert [simp]:
@@ -908,7 +908,7 @@
   from ab'(1) have "a' dvd a"
     unfolding dvd_def by blast
   with assms have "a' dvd b * c"
-    using dvd_trans[of a' a "b*c"] by simp
+    using dvd_trans [of a' a "b * c"] by simp
   from assms ab'(1,2) have "a' * ?d dvd (b' * ?d) * c"
     by simp
   then have "?d * a' dvd ?d * (b' * c)"
@@ -2663,16 +2663,6 @@
   by (auto simp add: inj_on_def coprime_crossproduct_nat simp del: One_nat_def)
 
 
-text \<open>Nitpick:\<close>
-
-lemma gcd_eq_nitpick_gcd [nitpick_unfold]: "gcd x y = Nitpick.nat_gcd x y"
-  by (induct x y rule: nat_gcd.induct)
-    (simp add: gcd_nat.simps Nitpick.nat_gcd.simps)
-
-lemma lcm_eq_nitpick_lcm [nitpick_unfold]: "lcm x y = Nitpick.nat_lcm x y"
-  by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
-
-
 subsubsection \<open>Setwise GCD and LCM for integers\<close>
 
 instantiation int :: semiring_Gcd
diff -r a04afc400156 -r 85ed070017b7 src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Sun Apr 23 14:27:22 2017 +0200
+++ b/src/HOL/Nitpick.thy	Sun Apr 23 14:53:33 2017 +0200
@@ -8,7 +8,7 @@
 section \<open>Nitpick: Yet Another Counterexample Generator for Isabelle/HOL\<close>
 
 theory Nitpick
-imports Record
+imports Record GCD
 keywords
   "nitpick" :: diag and
   "nitpick_params" :: thy_decl
@@ -129,7 +129,7 @@
   apply (metis mod_mod_trivial mod_self nat_neq_iff xt1(10))
   done
 
-declare nat_gcd.simps[simp del]
+declare nat_gcd.simps [simp del]
 
 definition nat_lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
   "nat_lcm x y = x * y div (nat_gcd x y)"
@@ -140,6 +140,13 @@
 definition int_lcm :: "int \<Rightarrow> int \<Rightarrow> int" where
   "int_lcm x y = int (nat_lcm (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
 
+lemma gcd_eq_nitpick_gcd [nitpick_unfold]: "gcd x y = Nitpick.nat_gcd x y"
+  by (induct x y rule: nat_gcd.induct)
+    (simp add: gcd_nat.simps Nitpick.nat_gcd.simps)
+
+lemma lcm_eq_nitpick_lcm [nitpick_unfold]: "lcm x y = Nitpick.nat_lcm x y"
+  by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
+
 definition Frac :: "int \<times> int \<Rightarrow> bool" where
   "Frac \<equiv> \<lambda>(a, b). b > 0 \<and> int_gcd a b = 1"