src/HOL/Hoare/Arith2.thy
author wenzelm
Tue Oct 10 19:23:03 2017 +0200 (2017-10-10)
changeset 66831 29ea2b900a05
parent 64246 15d1ee6e847b
child 67613 ce654b0e6d69
permissions -rw-r--r--
tuned: each session has at most one defining entry;
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
wenzelm@57442
    12
definition cd :: "[nat, nat, nat] => bool"
wenzelm@38353
    13
  where "cd x m n \<longleftrightarrow> x dvd m & x dvd n"
nipkow@1335
    14
wenzelm@38353
    15
definition gcd :: "[nat, nat] => nat"
wenzelm@38353
    16
  where "gcd m n = (SOME x. cd x m n & (!y.(cd y m n) --> y<=x))"
berghofe@5183
    17
wenzelm@38353
    18
primrec fac :: "nat => nat"
wenzelm@38353
    19
where
berghofe@5183
    20
  "fac 0 = Suc 0"
wenzelm@38353
    21
| "fac (Suc n) = Suc n * fac n"
nipkow@1335
    22
wenzelm@19802
    23
wenzelm@62042
    24
subsubsection \<open>cd\<close>
wenzelm@19802
    25
wenzelm@19802
    26
lemma cd_nnn: "0<n ==> cd n n n"
wenzelm@19802
    27
  apply (simp add: cd_def)
wenzelm@19802
    28
  done
wenzelm@19802
    29
wenzelm@19802
    30
lemma cd_le: "[| cd x m n; 0<m; 0<n |] ==> x<=m & x<=n"
wenzelm@19802
    31
  apply (unfold cd_def)
wenzelm@19802
    32
  apply (blast intro: dvd_imp_le)
wenzelm@19802
    33
  done
wenzelm@19802
    34
wenzelm@19802
    35
lemma cd_swap: "cd x m n = cd x n m"
wenzelm@19802
    36
  apply (unfold cd_def)
wenzelm@19802
    37
  apply blast
wenzelm@19802
    38
  done
wenzelm@19802
    39
wenzelm@19802
    40
lemma cd_diff_l: "n<=m ==> cd x m n = cd x (m-n) n"
wenzelm@19802
    41
  apply (unfold cd_def)
nipkow@44890
    42
  apply (fastforce dest: dvd_diffD)
wenzelm@19802
    43
  done
wenzelm@19802
    44
wenzelm@19802
    45
lemma cd_diff_r: "m<=n ==> cd x m n = cd x m (n-m)"
wenzelm@19802
    46
  apply (unfold cd_def)
nipkow@44890
    47
  apply (fastforce dest: dvd_diffD)
wenzelm@19802
    48
  done
wenzelm@19802
    49
wenzelm@19802
    50
wenzelm@62042
    51
subsubsection \<open>gcd\<close>
wenzelm@19802
    52
wenzelm@19802
    53
lemma gcd_nnn: "0<n ==> n = gcd n n"
wenzelm@19802
    54
  apply (unfold gcd_def)
wenzelm@19802
    55
  apply (frule cd_nnn)
wenzelm@19802
    56
  apply (rule some_equality [symmetric])
wenzelm@19802
    57
  apply (blast dest: cd_le)
nipkow@33657
    58
  apply (blast intro: le_antisym dest: cd_le)
wenzelm@19802
    59
  done
wenzelm@19802
    60
wenzelm@19802
    61
lemma gcd_swap: "gcd m n = gcd n m"
wenzelm@19802
    62
  apply (simp add: gcd_def cd_swap)
wenzelm@19802
    63
  done
wenzelm@19802
    64
wenzelm@19802
    65
lemma gcd_diff_l: "n<=m ==> gcd m n = gcd (m-n) n"
wenzelm@19802
    66
  apply (unfold gcd_def)
wenzelm@19802
    67
  apply (subgoal_tac "n<=m ==> !x. cd x m n = cd x (m-n) n")
wenzelm@19802
    68
  apply simp
wenzelm@19802
    69
  apply (rule allI)
wenzelm@19802
    70
  apply (erule cd_diff_l)
wenzelm@19802
    71
  done
wenzelm@19802
    72
wenzelm@19802
    73
lemma gcd_diff_r: "m<=n ==> gcd m n = gcd m (n-m)"
wenzelm@19802
    74
  apply (unfold gcd_def)
wenzelm@19802
    75
  apply (subgoal_tac "m<=n ==> !x. cd x m n = cd x m (n-m) ")
wenzelm@19802
    76
  apply simp
wenzelm@19802
    77
  apply (rule allI)
wenzelm@19802
    78
  apply (erule cd_diff_r)
wenzelm@19802
    79
  done
wenzelm@19802
    80
wenzelm@19802
    81
wenzelm@62042
    82
subsubsection \<open>pow\<close>
wenzelm@19802
    83
wenzelm@19802
    84
lemma sq_pow_div2 [simp]:
wenzelm@19802
    85
    "m mod 2 = 0 ==> ((n::nat)*n)^(m div 2) = n^m"
haftmann@64246
    86
  apply (simp add: power2_eq_square [symmetric] power_mult [symmetric] minus_mod_eq_mult_div [symmetric])
wenzelm@19802
    87
  done
wenzelm@17278
    88
nipkow@1335
    89
end