120 \<close> |
120 \<close> |
121 |
121 |
122 function nat_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
122 function nat_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
123 "nat_gcd x y = (if y = 0 then x else nat_gcd y (x mod y))" |
123 "nat_gcd x y = (if y = 0 then x else nat_gcd y (x mod y))" |
124 by auto |
124 by auto |
125 termination |
125 termination |
126 apply (relation "measure (\<lambda>(x, y). x + y + (if y > x then 1 else 0))") |
126 apply (relation "measure (\<lambda>(x, y). x + y + (if y > x then 1 else 0))") |
127 apply auto |
127 apply auto |
128 apply (metis mod_less_divisor xt1(9)) |
128 apply (metis mod_less_divisor xt1(9)) |
129 by (metis mod_mod_trivial mod_self nat_neq_iff xt1(10)) |
129 apply (metis mod_mod_trivial mod_self nat_neq_iff xt1(10)) |
|
130 done |
130 |
131 |
131 declare nat_gcd.simps[simp del] |
132 declare nat_gcd.simps[simp del] |
132 |
133 |
133 definition nat_lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
134 definition nat_lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
134 "nat_lcm x y = x * y div (nat_gcd x y)" |
135 "nat_lcm x y = x * y div (nat_gcd x y)" |
135 |
136 |
136 definition int_gcd :: "int \<Rightarrow> int \<Rightarrow> int" where |
137 definition int_gcd :: "int \<Rightarrow> int \<Rightarrow> int" where |
137 "int_gcd x y = int (nat_gcd (nat (abs x)) (nat (abs y)))" |
138 "int_gcd x y = int (nat_gcd (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))" |
138 |
139 |
139 definition int_lcm :: "int \<Rightarrow> int \<Rightarrow> int" where |
140 definition int_lcm :: "int \<Rightarrow> int \<Rightarrow> int" where |
140 "int_lcm x y = int (nat_lcm (nat (abs x)) (nat (abs y)))" |
141 "int_lcm x y = int (nat_lcm (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))" |
141 |
142 |
142 definition Frac :: "int \<times> int \<Rightarrow> bool" where |
143 definition Frac :: "int \<times> int \<Rightarrow> bool" where |
143 "Frac \<equiv> \<lambda>(a, b). b > 0 \<and> int_gcd a b = 1" |
144 "Frac \<equiv> \<lambda>(a, b). b > 0 \<and> int_gcd a b = 1" |
144 |
145 |
145 consts |
146 consts |