Theory Arith2

Up to index of Isabelle/HOL/Hoare

theory Arith2
imports Main
uses [Arith2.ML]
begin

(*  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 |] ==> xmxn

theorem cd_swap:

  cd x m n = cd x n m

theorem cd_diff_l:

  nm ==> cd x m n = cd x (m - n) n

theorem cd_diff_r:

  mn ==> 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:

  nm ==> Arith2.gcd m n = Arith2.gcd (m - n) n

theorem gcd_diff_r:

  mn ==> Arith2.gcd m n = Arith2.gcd m (n - m)

theorem sq_pow_div2:

  m mod 2 = 0 ==> (n * n) ^ (m div 2) = n ^ m