equal
deleted
inserted
replaced
7 |
7 |
8 theory Arith2 |
8 theory Arith2 |
9 imports Main |
9 imports Main |
10 begin |
10 begin |
11 |
11 |
12 definition "cd" :: "[nat, nat, nat] => bool" where |
12 definition "cd" :: "[nat, nat, nat] => bool" |
13 "cd x m n == x dvd m & x dvd n" |
13 where "cd x m n \<longleftrightarrow> x dvd m & x dvd n" |
14 |
14 |
15 definition gcd :: "[nat, nat] => nat" where |
15 definition gcd :: "[nat, nat] => nat" |
16 "gcd m n == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)" |
16 where "gcd m n = (SOME x. cd x m n & (!y.(cd y m n) --> y<=x))" |
17 |
17 |
18 consts fac :: "nat => nat" |
18 primrec fac :: "nat => nat" |
19 |
19 where |
20 primrec |
|
21 "fac 0 = Suc 0" |
20 "fac 0 = Suc 0" |
22 "fac(Suc n) = (Suc n)*fac(n)" |
21 | "fac (Suc n) = Suc n * fac n" |
23 |
22 |
24 |
23 |
25 subsubsection {* cd *} |
24 subsubsection {* cd *} |
26 |
25 |
27 lemma cd_nnn: "0<n ==> cd n n n" |
26 lemma cd_nnn: "0<n ==> cd n n n" |