--- 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
--- 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"