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