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