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