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