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