src/HOL/Hoare/Arith2.thy
author haftmann
Mon Mar 01 13:40:23 2010 +0100 (2010-03-01)
changeset 35416 d8d7d1b785af
parent 33657 a4179bf442d1
child 38353 d98baa2cf589
permissions -rw-r--r--
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
     1 (*  Title:      HOL/Hoare/Arith2.thy
     2     Author:     Norbert Galm
     3     Copyright   1995 TUM
     4 
     5 More arithmetic.  Much of this duplicates ex/Primes.
     6 *)
     7 
     8 theory Arith2
     9 imports Main
    10 begin
    11 
    12 definition "cd" :: "[nat, nat, nat] => bool" where
    13   "cd x m n  == x dvd m & x dvd n"
    14 
    15 definition gcd     :: "[nat, nat] => nat" where
    16   "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
    17 
    18 consts fac     :: "nat => nat"
    19 
    20 primrec
    21   "fac 0 = Suc 0"
    22   "fac(Suc n) = (Suc n)*fac(n)"
    23 
    24 
    25 subsubsection {* cd *}
    26 
    27 lemma cd_nnn: "0<n ==> cd n n n"
    28   apply (simp add: cd_def)
    29   done
    30 
    31 lemma cd_le: "[| cd x m n; 0<m; 0<n |] ==> x<=m & x<=n"
    32   apply (unfold cd_def)
    33   apply (blast intro: dvd_imp_le)
    34   done
    35 
    36 lemma cd_swap: "cd x m n = cd x n m"
    37   apply (unfold cd_def)
    38   apply blast
    39   done
    40 
    41 lemma cd_diff_l: "n<=m ==> cd x m n = cd x (m-n) n"
    42   apply (unfold cd_def)
    43   apply (fastsimp dest: dvd_diffD)
    44   done
    45 
    46 lemma cd_diff_r: "m<=n ==> cd x m n = cd x m (n-m)"
    47   apply (unfold cd_def)
    48   apply (fastsimp dest: dvd_diffD)
    49   done
    50 
    51 
    52 subsubsection {* gcd *}
    53 
    54 lemma gcd_nnn: "0<n ==> n = gcd n n"
    55   apply (unfold gcd_def)
    56   apply (frule cd_nnn)
    57   apply (rule some_equality [symmetric])
    58   apply (blast dest: cd_le)
    59   apply (blast intro: le_antisym dest: cd_le)
    60   done
    61 
    62 lemma gcd_swap: "gcd m n = gcd n m"
    63   apply (simp add: gcd_def cd_swap)
    64   done
    65 
    66 lemma gcd_diff_l: "n<=m ==> gcd m n = gcd (m-n) n"
    67   apply (unfold gcd_def)
    68   apply (subgoal_tac "n<=m ==> !x. cd x m n = cd x (m-n) n")
    69   apply simp
    70   apply (rule allI)
    71   apply (erule cd_diff_l)
    72   done
    73 
    74 lemma gcd_diff_r: "m<=n ==> gcd m n = gcd m (n-m)"
    75   apply (unfold gcd_def)
    76   apply (subgoal_tac "m<=n ==> !x. cd x m n = cd x m (n-m) ")
    77   apply simp
    78   apply (rule allI)
    79   apply (erule cd_diff_r)
    80   done
    81 
    82 
    83 subsubsection {* pow *}
    84 
    85 lemma sq_pow_div2 [simp]:
    86     "m mod 2 = 0 ==> ((n::nat)*n)^(m div 2) = n^m"
    87   apply (simp add: power2_eq_square [symmetric] power_mult [symmetric] mult_div_cancel)
    88   done
    89 
    90 end