# 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 |] ==> 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