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
```