src/HOL/Hyperreal/EvenOdd.thy
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 15131 c69542757a4d
child 15251 bb6f072c8d10
permissions -rw-r--r--
import -> imports
paulson@12196
     1
(*  Title       : EvenOdd.thy
paulson@14435
     2
    ID:         $Id$
paulson@12196
     3
    Author      : Jacques D. Fleuriot  
paulson@12196
     4
    Copyright   : 1999  University of Edinburgh
paulson@12196
     5
*)
paulson@12196
     6
paulson@14435
     7
header{*Even and Odd Numbers: Compatibility file for Parity*}
paulson@14430
     8
nipkow@15131
     9
theory EvenOdd
nipkow@15140
    10
imports NthRoot
nipkow@15131
    11
begin
paulson@14430
    12
paulson@14430
    13
subsection{*General Lemmas About Division*}
paulson@14430
    14
paulson@14435
    15
lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1" 
paulson@14435
    16
apply (induct_tac "m")
paulson@14435
    17
apply (simp_all add: mod_Suc)
paulson@14435
    18
done
paulson@14430
    19
paulson@14435
    20
declare Suc_times_mod_eq [of "number_of w", standard, simp]
paulson@14430
    21
paulson@14435
    22
lemma [simp]: "n div k \<le> (Suc n) div k"
paulson@14435
    23
by (simp add: div_le_mono) 
paulson@14430
    24
paulson@14435
    25
lemma Suc_n_div_2_gt_zero [simp]: "(0::nat) < n ==> 0 < (n + 1) div 2"
paulson@14430
    26
by arith
paulson@14430
    27
paulson@14435
    28
lemma div_2_gt_zero [simp]: "(1::nat) < n ==> 0 < n div 2" 
paulson@14430
    29
by arith
paulson@14430
    30
paulson@14435
    31
lemma mod_mult_self3 [simp]: "(k*n + m) mod n = m mod (n::nat)"
paulson@14430
    32
by (simp add: mult_ac add_ac)
paulson@14430
    33
paulson@14435
    34
lemma mod_mult_self4 [simp]: "Suc (k*n + m) mod n = Suc m mod n"
paulson@14430
    35
proof -
paulson@14430
    36
  have "Suc (k * n + m) mod n = (k * n + Suc m) mod n" by simp
paulson@14430
    37
  also have "... = Suc m mod n" by (rule mod_mult_self3) 
paulson@14430
    38
  finally show ?thesis .
paulson@14430
    39
qed
paulson@14430
    40
paulson@14430
    41
lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n"
paulson@14430
    42
apply (subst mod_Suc [of m]) 
paulson@14430
    43
apply (subst mod_Suc [of "m mod n"], simp) 
paulson@14430
    44
done
paulson@14430
    45
paulson@12196
    46
paulson@14430
    47
subsection{*More Even/Odd Results*}
paulson@14430
    48
 
paulson@14435
    49
lemma even_mult_two_ex: "even(n) = (\<exists>m::nat. n = 2*m)"
paulson@14430
    50
by (simp add: even_nat_equiv_def2 numeral_2_eq_2)
paulson@14430
    51
paulson@14435
    52
lemma odd_Suc_mult_two_ex: "odd(n) = (\<exists>m. n = Suc (2*m))"
paulson@14430
    53
by (simp add: odd_nat_equiv_def2 numeral_2_eq_2)
paulson@14430
    54
paulson@14435
    55
lemma even_add [simp]: "even(m + n::nat) = (even m = even n)" 
paulson@14430
    56
by auto
paulson@14430
    57
paulson@14435
    58
lemma odd_add [simp]: "odd(m + n::nat) = (odd m \<noteq> odd n)"
paulson@14430
    59
by auto
paulson@14430
    60
paulson@14435
    61
lemma lemma_even_div2 [simp]: "even (n::nat) ==> (n + 1) div 2 = n div 2"
paulson@14430
    62
apply (simp add: numeral_2_eq_2) 
paulson@14430
    63
apply (subst div_Suc)  
paulson@14430
    64
apply (simp add: even_nat_mod_two_eq_zero) 
paulson@14430
    65
done
paulson@14430
    66
paulson@14435
    67
lemma lemma_not_even_div2 [simp]: "~even n ==> (n + 1) div 2 = Suc (n div 2)"
paulson@14430
    68
apply (simp add: numeral_2_eq_2) 
paulson@14430
    69
apply (subst div_Suc)  
paulson@14430
    70
apply (simp add: odd_nat_mod_two_eq_one) 
paulson@14430
    71
done
paulson@14430
    72
paulson@14430
    73
lemma even_num_iff: "0 < n ==> even n = (~ even(n - 1 :: nat))" 
paulson@14430
    74
by (case_tac "n", auto)
paulson@14430
    75
paulson@14430
    76
lemma even_even_mod_4_iff: "even (n::nat) = even (n mod 4)"
paulson@14430
    77
apply (induct n, simp)
paulson@14430
    78
apply (subst mod_Suc, simp) 
paulson@14430
    79
done
paulson@12196
    80
paulson@14430
    81
lemma lemma_odd_mod_4_div_2: "n mod 4 = (3::nat) ==> odd((n - 1) div 2)"
paulson@14430
    82
apply (rule_tac t = n and n1 = 4 in mod_div_equality [THEN subst])
paulson@14430
    83
apply (simp add: even_num_iff)
paulson@14430
    84
done
paulson@14430
    85
paulson@14430
    86
lemma lemma_even_mod_4_div_2: "n mod 4 = (1::nat) ==> even ((n - 1) div 2)"
paulson@14430
    87
by (rule_tac t = n and n1 = 4 in mod_div_equality [THEN subst], simp)
paulson@14430
    88
paulson@14430
    89
ML
paulson@14430
    90
{*
paulson@14435
    91
val even_nat_Suc = thm"Parity.even_nat_Suc";
paulson@14430
    92
paulson@14430
    93
val even_mult_two_ex = thm "even_mult_two_ex";
paulson@14430
    94
val odd_Suc_mult_two_ex = thm "odd_Suc_mult_two_ex";
paulson@14430
    95
val even_add = thm "even_add";
paulson@14430
    96
val odd_add = thm "odd_add";
paulson@14430
    97
val Suc_n_div_2_gt_zero = thm "Suc_n_div_2_gt_zero";
paulson@14430
    98
val div_2_gt_zero = thm "div_2_gt_zero";
paulson@14430
    99
val even_num_iff = thm "even_num_iff";
paulson@14435
   100
val nat_mod_div_trivial = thm "nat_mod_div_trivial";
paulson@14435
   101
val nat_mod_mod_trivial = thm "nat_mod_mod_trivial";
paulson@14430
   102
val mod_Suc_eq_Suc_mod = thm "mod_Suc_eq_Suc_mod";
paulson@14430
   103
val even_even_mod_4_iff = thm "even_even_mod_4_iff";
paulson@14430
   104
val lemma_odd_mod_4_div_2 = thm "lemma_odd_mod_4_div_2";
paulson@14430
   105
val lemma_even_mod_4_div_2 = thm "lemma_even_mod_4_div_2";
paulson@14430
   106
*}
paulson@12196
   107
paulson@12196
   108
end
paulson@12196
   109