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.5  
     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.15  
    1.16 -declare nat_gcd.simps[simp del]
    1.17 +declare nat_gcd.simps [simp del]
    1.18  
    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.24  
    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"
    1.34