src/HOL/Nitpick.thy
 changeset 65555 85ed070017b7 parent 64267 b9a1486e79be child 66011 f10bbfe07c41
1.1 --- a/src/HOL/Nitpick.thy	Sun Apr 23 14:27:22 2017 +0200
1.2 +++ b/src/HOL/Nitpick.thy	Sun Apr 23 14:53:33 2017 +0200
1.3 @@ -8,7 +8,7 @@
1.4  section \<open>Nitpick: Yet Another Counterexample Generator for Isabelle/HOL\<close>
1.6  theory Nitpick
1.7 -imports Record
1.8 +imports Record GCD
1.9  keywords
1.10    "nitpick" :: diag and
1.11    "nitpick_params" :: thy_decl
1.12 @@ -129,7 +129,7 @@
1.13    apply (metis mod_mod_trivial mod_self nat_neq_iff xt1(10))
1.14    done
1.16 -declare nat_gcd.simps[simp del]
1.17 +declare nat_gcd.simps [simp del]
1.19  definition nat_lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
1.20    "nat_lcm x y = x * y div (nat_gcd x y)"
1.21 @@ -140,6 +140,13 @@
1.22  definition int_lcm :: "int \<Rightarrow> int \<Rightarrow> int" where
1.23    "int_lcm x y = int (nat_lcm (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
1.25 +lemma gcd_eq_nitpick_gcd [nitpick_unfold]: "gcd x y = Nitpick.nat_gcd x y"
1.26 +  by (induct x y rule: nat_gcd.induct)
1.27 +    (simp add: gcd_nat.simps Nitpick.nat_gcd.simps)
1.28 +
1.29 +lemma lcm_eq_nitpick_lcm [nitpick_unfold]: "lcm x y = Nitpick.nat_lcm x y"
1.30 +  by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
1.31 +
1.32  definition Frac :: "int \<times> int \<Rightarrow> bool" where
1.33    "Frac \<equiv> \<lambda>(a, b). b > 0 \<and> int_gcd a b = 1"