src/HOL/Nitpick.thy
changeset 61944 5d06ecfdb472
parent 61799 4cf66f21b764
child 63882 018998c00003
     1.1 --- a/src/HOL/Nitpick.thy	Sun Dec 27 22:07:17 2015 +0100
     1.2 +++ b/src/HOL/Nitpick.thy	Mon Dec 28 01:26:34 2015 +0100
     1.3 @@ -122,11 +122,12 @@
     1.4  function nat_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
     1.5    "nat_gcd x y = (if y = 0 then x else nat_gcd y (x mod y))"
     1.6    by auto
     1.7 -  termination
     1.8 +termination
     1.9    apply (relation "measure (\<lambda>(x, y). x + y + (if y > x then 1 else 0))")
    1.10     apply auto
    1.11     apply (metis mod_less_divisor xt1(9))
    1.12 -  by (metis mod_mod_trivial mod_self nat_neq_iff xt1(10))
    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  
    1.18 @@ -134,10 +135,10 @@
    1.19    "nat_lcm x y = x * y div (nat_gcd x y)"
    1.20  
    1.21  definition int_gcd :: "int \<Rightarrow> int \<Rightarrow> int" where
    1.22 -  "int_gcd x y = int (nat_gcd (nat (abs x)) (nat (abs y)))"
    1.23 +  "int_gcd x y = int (nat_gcd (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
    1.24  
    1.25  definition int_lcm :: "int \<Rightarrow> int \<Rightarrow> int" where
    1.26 -  "int_lcm x y = int (nat_lcm (nat (abs x)) (nat (abs y)))"
    1.27 +  "int_lcm x y = int (nat_lcm (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
    1.28  
    1.29  definition Frac :: "int \<times> int \<Rightarrow> bool" where
    1.30    "Frac \<equiv> \<lambda>(a, b). b > 0 \<and> int_gcd a b = 1"