(* Title: HOL/Hoare/Arith2.thy ID: $Id: Arith2.thy,v 1.11 2005/09/06 14:59:53 wenzelm Exp $ Author: Norbert Galm Copyright 1995 TUM More arithmetic. Much of this duplicates ex/Primes. *) theory Arith2 imports Main begin constdefs "cd" :: "[nat, nat, nat] => bool" "cd x m n == x dvd m & x dvd n" gcd :: "[nat, nat] => nat" "gcd m n == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)" consts fac :: "nat => nat" primrec "fac 0 = Suc 0" "fac(Suc n) = (Suc n)*fac(n)" ML {* use_legacy_bindings (the_context ()) *} end
theorem cd_nnn:
0 < n ==> cd n n n
theorem cd_le:
[| cd x m n; 0 < m; 0 < n |] ==> x ≤ m ∧ x ≤ n
theorem cd_swap:
cd x m n = cd x n m
theorem cd_diff_l:
n ≤ m ==> cd x m n = cd x (m - n) n
theorem cd_diff_r:
m ≤ n ==> cd x m n = cd x m (n - m)
theorem gcd_nnn:
0 < n ==> n = Arith2.gcd n n
theorem gcd_swap:
Arith2.gcd m n = Arith2.gcd n m
theorem gcd_diff_l:
n ≤ m ==> Arith2.gcd m n = Arith2.gcd (m - n) n
theorem gcd_diff_r:
m ≤ n ==> Arith2.gcd m n = Arith2.gcd m (n - m)
theorem sq_pow_div2:
m mod 2 = 0 ==> (n * n) ^ (m div 2) = n ^ m