prefer 'definition' over low-level defs;
authorwenzelm
Wed May 17 01:23:41 2006 +0200 (2006-05-17)
changeset 196702e4a143c73c5
parent 19669 95ac857276e1
child 19671 e293e16d1442
prefer 'definition' over low-level defs;
tuned source/document;
src/HOL/NumberTheory/BijectionRel.thy
src/HOL/NumberTheory/Chinese.thy
src/HOL/NumberTheory/Euler.thy
src/HOL/NumberTheory/EulerFermat.thy
src/HOL/NumberTheory/EvenOdd.thy
src/HOL/NumberTheory/Factorization.thy
src/HOL/NumberTheory/Finite2.thy
src/HOL/NumberTheory/Int2.thy
src/HOL/NumberTheory/IntPrimes.thy
src/HOL/NumberTheory/Quadratic_Reciprocity.thy
src/HOL/NumberTheory/Residues.thy
src/HOL/NumberTheory/WilsonBij.thy
src/HOL/NumberTheory/WilsonRuss.thy
     1.1 --- a/src/HOL/NumberTheory/BijectionRel.thy	Wed May 17 01:23:40 2006 +0200
     1.2 +++ b/src/HOL/NumberTheory/BijectionRel.thy	Wed May 17 01:23:41 2006 +0200
     1.3 @@ -29,15 +29,15 @@
     1.4    (and similar for @{term A}).
     1.5  *}
     1.6  
     1.7 -constdefs
     1.8 +definition
     1.9    bijP :: "('a => 'a => bool) => 'a set => bool"
    1.10 -  "bijP P F == \<forall>a b. a \<in> F \<and> P a b --> b \<in> F"
    1.11 +  "bijP P F = (\<forall>a b. a \<in> F \<and> P a b --> b \<in> F)"
    1.12  
    1.13    uniqP :: "('a => 'a => bool) => bool"
    1.14 -  "uniqP P == \<forall>a b c d. P a b \<and> P c d --> (a = c) = (b = d)"
    1.15 +  "uniqP P = (\<forall>a b c d. P a b \<and> P c d --> (a = c) = (b = d))"
    1.16  
    1.17    symP :: "('a => 'a => bool) => bool"
    1.18 -  "symP P == \<forall>a b. P a b = P b a"
    1.19 +  "symP P = (\<forall>a b. P a b = P b a)"
    1.20  
    1.21  consts
    1.22    bijER :: "('a => 'a => bool) => 'a set set"
     2.1 --- a/src/HOL/NumberTheory/Chinese.thy	Wed May 17 01:23:40 2006 +0200
     2.2 +++ b/src/HOL/NumberTheory/Chinese.thy	Wed May 17 01:23:41 2006 +0200
     2.3 @@ -31,43 +31,34 @@
     2.4    "funsum f i 0 = f i"
     2.5    "funsum f i (Suc n) = f (Suc (i + n)) + funsum f i n"
     2.6  
     2.7 -consts
     2.8 +definition
     2.9    m_cond :: "nat => (nat => int) => bool"
    2.10 +  "m_cond n mf =
    2.11 +    ((\<forall>i. i \<le> n --> 0 < mf i) \<and>
    2.12 +      (\<forall>i j. i \<le> n \<and> j \<le> n \<and> i \<noteq> j --> zgcd (mf i, mf j) = 1))"
    2.13 +
    2.14    km_cond :: "nat => (nat => int) => (nat => int) => bool"
    2.15 +  "km_cond n kf mf = (\<forall>i. i \<le> n --> zgcd (kf i, mf i) = 1)"
    2.16 +
    2.17    lincong_sol ::
    2.18      "nat => (nat => int) => (nat => int) => (nat => int) => int => bool"
    2.19 +  "lincong_sol n kf bf mf x = (\<forall>i. i \<le> n --> zcong (kf i * x) (bf i) (mf i))"
    2.20  
    2.21    mhf :: "(nat => int) => nat => nat => int"
    2.22 +  "mhf mf n i =
    2.23 +    (if i = 0 then funprod mf (Suc 0) (n - Suc 0)
    2.24 +     else if i = n then funprod mf 0 (n - Suc 0)
    2.25 +     else funprod mf 0 (i - Suc 0) * funprod mf (Suc i) (n - Suc 0 - i))"
    2.26 +
    2.27    xilin_sol ::
    2.28      "nat => nat => (nat => int) => (nat => int) => (nat => int) => int"
    2.29 -  x_sol :: "nat => (nat => int) => (nat => int) => (nat => int) => int"
    2.30 -
    2.31 -defs
    2.32 -  m_cond_def:
    2.33 -    "m_cond n mf ==
    2.34 -      (\<forall>i. i \<le> n --> 0 < mf i) \<and>
    2.35 -      (\<forall>i j. i \<le> n \<and> j \<le> n \<and> i \<noteq> j --> zgcd (mf i, mf j) = 1)"
    2.36 -
    2.37 -  km_cond_def:
    2.38 -    "km_cond n kf mf == \<forall>i. i \<le> n --> zgcd (kf i, mf i) = 1"
    2.39 -
    2.40 -  lincong_sol_def:
    2.41 -    "lincong_sol n kf bf mf x == \<forall>i. i \<le> n --> zcong (kf i * x) (bf i) (mf i)"
    2.42 +  "xilin_sol i n kf bf mf =
    2.43 +    (if 0 < n \<and> i \<le> n \<and> m_cond n mf \<and> km_cond n kf mf then
    2.44 +        (SOME x. 0 \<le> x \<and> x < mf i \<and> zcong (kf i * mhf mf n i * x) (bf i) (mf i))
    2.45 +     else 0)"
    2.46  
    2.47 -  mhf_def:
    2.48 -    "mhf mf n i ==
    2.49 -      if i = 0 then funprod mf (Suc 0) (n - Suc 0)
    2.50 -      else if i = n then funprod mf 0 (n - Suc 0)
    2.51 -      else funprod mf 0 (i - Suc 0) * funprod mf (Suc i) (n - Suc 0 - i)"
    2.52 -
    2.53 -  xilin_sol_def:
    2.54 -    "xilin_sol i n kf bf mf ==
    2.55 -      if 0 < n \<and> i \<le> n \<and> m_cond n mf \<and> km_cond n kf mf then
    2.56 -        (SOME x. 0 \<le> x \<and> x < mf i \<and> zcong (kf i * mhf mf n i * x) (bf i) (mf i))
    2.57 -      else 0"
    2.58 -
    2.59 -  x_sol_def:
    2.60 -    "x_sol n kf bf mf == funsum (\<lambda>i. xilin_sol i n kf bf mf * mhf mf n i) 0 n"
    2.61 +  x_sol :: "nat => (nat => int) => (nat => int) => (nat => int) => int"
    2.62 +  "x_sol n kf bf mf = funsum (\<lambda>i. xilin_sol i n kf bf mf * mhf mf n i) 0 n"
    2.63  
    2.64  
    2.65  text {* \medskip @{term funprod} and @{term funsum} *}
     3.1 --- a/src/HOL/NumberTheory/Euler.thy	Wed May 17 01:23:40 2006 +0200
     3.2 +++ b/src/HOL/NumberTheory/Euler.thy	Wed May 17 01:23:41 2006 +0200
     3.3 @@ -7,22 +7,20 @@
     3.4  
     3.5  theory Euler imports Residues EvenOdd begin
     3.6  
     3.7 -constdefs
     3.8 +definition
     3.9    MultInvPair :: "int => int => int => int set"
    3.10 -  "MultInvPair a p j == {StandardRes p j, StandardRes p (a * (MultInv p j))}"
    3.11 +  "MultInvPair a p j = {StandardRes p j, StandardRes p (a * (MultInv p j))}"
    3.12 +
    3.13    SetS        :: "int => int => int set set"
    3.14 -  "SetS        a p   ==  ((MultInvPair a p) ` (SRStar p))"
    3.15 +  "SetS        a p   =  (MultInvPair a p ` SRStar p)"
    3.16  
    3.17 -(****************************************************************)
    3.18 -(*                                                              *)
    3.19 -(* Property for MultInvPair                                     *)
    3.20 -(*                                                              *)
    3.21 -(****************************************************************)
    3.22 +
    3.23 +subsection {* Property for MultInvPair *}
    3.24  
    3.25 -lemma MultInvPair_prop1a: "[| zprime p; 2 < p; ~([a = 0](mod p));
    3.26 -                              X \<in> (SetS a p); Y \<in> (SetS a p);
    3.27 -                              ~((X \<inter> Y) = {}) |] ==> 
    3.28 -                           X = Y"
    3.29 +lemma MultInvPair_prop1a:
    3.30 +  "[| zprime p; 2 < p; ~([a = 0](mod p));
    3.31 +      X \<in> (SetS a p); Y \<in> (SetS a p);
    3.32 +      ~((X \<inter> Y) = {}) |] ==> X = Y"
    3.33    apply (auto simp add: SetS_def)
    3.34    apply (drule StandardRes_SRStar_prop1a)+ defer 1
    3.35    apply (drule StandardRes_SRStar_prop1a)+
    3.36 @@ -35,16 +33,16 @@
    3.37    apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)
    3.38    apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)
    3.39    apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)
    3.40 -done
    3.41 +  done
    3.42  
    3.43 -lemma MultInvPair_prop1b: "[| zprime p; 2 < p; ~([a = 0](mod p));
    3.44 -                              X \<in> (SetS a p); Y \<in> (SetS a p);
    3.45 -                              X \<noteq> Y |] ==>
    3.46 -                              X \<inter> Y = {}"
    3.47 +lemma MultInvPair_prop1b:
    3.48 +  "[| zprime p; 2 < p; ~([a = 0](mod p));
    3.49 +      X \<in> (SetS a p); Y \<in> (SetS a p);
    3.50 +      X \<noteq> Y |] ==> X \<inter> Y = {}"
    3.51    apply (rule notnotD)
    3.52    apply (rule notI)
    3.53    apply (drule MultInvPair_prop1a, auto)
    3.54 -done
    3.55 +  done
    3.56  
    3.57  lemma MultInvPair_prop1c: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==>  
    3.58      \<forall>X \<in> SetS a p. \<forall>Y \<in> SetS a p. X \<noteq> Y --> X\<inter>Y = {}"
    3.59 @@ -56,7 +54,7 @@
    3.60      SRStar_mult_prop2)
    3.61    apply (frule StandardRes_SRStar_prop3)
    3.62    apply (rule bexI, auto)
    3.63 -done
    3.64 +  done
    3.65  
    3.66  lemma MultInvPair_distinct: "[| zprime p; 2 < p; ~([a = 0] (mod p)); 
    3.67                                  ~([j = 0] (mod p)); 
    3.68 @@ -97,11 +95,8 @@
    3.69    apply (drule MultInvPair_distinct)
    3.70  by auto
    3.71  
    3.72 -(****************************************************************)
    3.73 -(*                                                              *)
    3.74 -(* Properties of SetS                                           *)
    3.75 -(*                                                              *)
    3.76 -(****************************************************************)
    3.77 +
    3.78 +subsection {* Properties of SetS *}
    3.79  
    3.80  lemma SetS_finite: "2 < p ==> finite (SetS a p)"
    3.81    by (auto simp add: SetS_def SRStar_finite [of p] finite_imageI)
    3.82 @@ -115,7 +110,7 @@
    3.83    apply (auto simp add: SetS_def)
    3.84    apply (frule StandardRes_SRStar_prop1a)
    3.85    apply (rule MultInvPair_card_two, auto)
    3.86 -done
    3.87 +  done
    3.88  
    3.89  lemma Union_SetS_finite: "2 < p ==> finite (Union (SetS a p))"
    3.90    by (auto simp add: SetS_finite SetS_elems_finite finite_Union)
    3.91 @@ -136,10 +131,9 @@
    3.92        by (auto simp add: prems SetS_finite SetS_elems_finite
    3.93                           MultInvPair_prop1c [of p a] card_Union_disjoint)
    3.94      also have "... = int(setsum (%x.2) (SetS a p))"
    3.95 -      apply (insert prems)
    3.96 -      apply (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite 
    3.97 +      using prems
    3.98 +      by (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite 
    3.99          card_setsum_aux simp del: setsum_constant)
   3.100 -    done
   3.101      also have "... = 2 * int(card( SetS a p))"
   3.102        by (auto simp add: prems SetS_finite setsum_const2)
   3.103      finally show ?thesis .
   3.104 @@ -164,7 +158,7 @@
   3.105    apply (frule_tac p = p and x = x in MultInv_prop2, auto)
   3.106    apply (drule_tac a = "x * MultInv p x" and b = 1 in zcong_zmult_prop2)
   3.107    apply (auto simp add: zmult_ac)
   3.108 -done
   3.109 +  done
   3.110  
   3.111  lemma aux1: "[| 0 < x; (x::int) < a; x \<noteq> (a - 1) |] ==> x < a - 1"
   3.112    by arith
   3.113 @@ -237,13 +231,7 @@
   3.114    apply (auto simp add: Union_SetS_setprod_prop2)
   3.115    done
   3.116  
   3.117 -(****************************************************************)
   3.118 -(*                                                              *)
   3.119 -(*  Prove the first part of Euler's Criterion:                  *)
   3.120 -(*    ~(QuadRes p x) |] ==>                                     *)
   3.121 -(*                   [x^(nat (((p) - 1) div 2)) = -1](mod p)    *)
   3.122 -(*                                                              *)
   3.123 -(****************************************************************)
   3.124 +text {* \medskip Prove the first part of Euler's Criterion: *}
   3.125  
   3.126  lemma Euler_part1: "[| 2 < p; zprime p; ~([x = 0](mod p)); 
   3.127      ~(QuadRes p x) |] ==> 
   3.128 @@ -254,12 +242,7 @@
   3.129    apply (rule zcong_trans, auto)
   3.130    done
   3.131  
   3.132 -(********************************************************************)
   3.133 -(*                                                                  *)
   3.134 -(* Prove another part of Euler Criterion:                           *)
   3.135 -(*        [a = 0] (mod p) ==> [0 = a ^ nat ((p - 1) div 2)] (mod p) *)
   3.136 -(*                                                                  *)
   3.137 -(********************************************************************)
   3.138 +text {* \medskip Prove another part of Euler Criterion: *}
   3.139  
   3.140  lemma aux_1: "0 < p ==> (a::int) ^ nat (p) = a * a ^ (nat (p) - 1)"
   3.141  proof -
   3.142 @@ -289,20 +272,15 @@
   3.143    then show ?thesis by auto
   3.144  qed
   3.145  
   3.146 -lemma Euler_part2: "[| 2 < p; zprime p; [a = 0] (mod p) |] ==> [0 = a ^ nat ((p - 1) div 2)] (mod p)"
   3.147 +lemma Euler_part2:
   3.148 +    "[| 2 < p; zprime p; [a = 0] (mod p) |] ==> [0 = a ^ nat ((p - 1) div 2)] (mod p)"
   3.149    apply (frule zprime_zOdd_eq_grt_2)
   3.150    apply (frule aux_2, auto)
   3.151    apply (frule_tac a = a in aux_1, auto)
   3.152    apply (frule zcong_zmult_prop1, auto)
   3.153    done
   3.154  
   3.155 -(****************************************************************)
   3.156 -(*                                                              *)
   3.157 -(* Prove the final part of Euler's Criterion:                   *)
   3.158 -(*           QuadRes p x |] ==>                                 *)
   3.159 -(*                      [x^(nat (((p) - 1) div 2)) = 1](mod p)  *)
   3.160 -(*                                                              *)
   3.161 -(****************************************************************)
   3.162 +text {* \medskip Prove the final part of Euler's Criterion: *}
   3.163  
   3.164  lemma aux__1: "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==> ~(p dvd y)"
   3.165    apply (subgoal_tac "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==> 
   3.166 @@ -329,11 +307,8 @@
   3.167    apply (auto intro: Little_Fermat simp add: zprime_zOdd_eq_grt_2)
   3.168    done
   3.169  
   3.170 -(********************************************************************)
   3.171 -(*                                                                  *)
   3.172 -(* Finally show Euler's Criterion                                   *)
   3.173 -(*                                                                  *)
   3.174 -(********************************************************************)
   3.175 +
   3.176 +text {* \medskip Finally show Euler's Criterion: *}
   3.177  
   3.178  theorem Euler_Criterion: "[| 2 < p; zprime p |] ==> [(Legendre a p) =
   3.179      a^(nat (((p) - 1) div 2))] (mod p)"
     4.1 --- a/src/HOL/NumberTheory/EulerFermat.thy	Wed May 17 01:23:40 2006 +0200
     4.2 +++ b/src/HOL/NumberTheory/EulerFermat.thy	Wed May 17 01:23:41 2006 +0200
     4.3 @@ -19,12 +19,6 @@
     4.4  
     4.5  consts
     4.6    RsetR :: "int => int set set"
     4.7 -  BnorRset :: "int * int => int set"
     4.8 -  norRRset :: "int => int set"
     4.9 -  noXRRset :: "int => int => int set"
    4.10 -  phi :: "int => nat"
    4.11 -  is_RRset :: "int set => int => bool"
    4.12 -  RRset2norRR :: "int set => int => int => int"
    4.13  
    4.14  inductive "RsetR m"
    4.15    intros
    4.16 @@ -32,6 +26,9 @@
    4.17      insert: "A \<in> RsetR m ==> zgcd (a, m) = 1 ==>
    4.18        \<forall>a'. a' \<in> A --> \<not> zcong a a' m ==> insert a A \<in> RsetR m"
    4.19  
    4.20 +consts
    4.21 +  BnorRset :: "int * int => int set"
    4.22 +
    4.23  recdef BnorRset
    4.24    "measure ((\<lambda>(a, m). nat a) :: int * int => nat)"
    4.25    "BnorRset (a, m) =
    4.26 @@ -40,20 +37,27 @@
    4.27      in (if zgcd (a, m) = 1 then insert a na else na)
    4.28      else {})"
    4.29  
    4.30 -defs
    4.31 -  norRRset_def: "norRRset m == BnorRset (m - 1, m)"
    4.32 -  noXRRset_def: "noXRRset m x == (\<lambda>a. a * x) ` norRRset m"
    4.33 -  phi_def: "phi m == card (norRRset m)"
    4.34 -  is_RRset_def: "is_RRset A m == A \<in> RsetR m \<and> card A = phi m"
    4.35 -  RRset2norRR_def:
    4.36 -    "RRset2norRR A m a ==
    4.37 +definition
    4.38 +  norRRset :: "int => int set"
    4.39 +  "norRRset m = BnorRset (m - 1, m)"
    4.40 +
    4.41 +  noXRRset :: "int => int => int set"
    4.42 +  "noXRRset m x = (\<lambda>a. a * x) ` norRRset m"
    4.43 +
    4.44 +  phi :: "int => nat"
    4.45 +  "phi m = card (norRRset m)"
    4.46 +
    4.47 +  is_RRset :: "int set => int => bool"
    4.48 +  "is_RRset A m = (A \<in> RsetR m \<and> card A = phi m)"
    4.49 +
    4.50 +  RRset2norRR :: "int set => int => int => int"
    4.51 +  "RRset2norRR A m a =
    4.52       (if 1 < m \<and> is_RRset A m \<and> a \<in> A then
    4.53          SOME b. zcong a b m \<and> b \<in> norRRset m
    4.54        else 0)"
    4.55  
    4.56 -constdefs
    4.57    zcongm :: "int => int => int => bool"
    4.58 -  "zcongm m == \<lambda>a b. zcong a b m"
    4.59 +  "zcongm m = (\<lambda>a b. zcong a b m)"
    4.60  
    4.61  lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)"
    4.62    -- {* LCP: not sure why this lemma is needed now *}
     5.1 --- a/src/HOL/NumberTheory/EvenOdd.thy	Wed May 17 01:23:40 2006 +0200
     5.2 +++ b/src/HOL/NumberTheory/EvenOdd.thy	Wed May 17 01:23:41 2006 +0200
     5.3 @@ -7,20 +7,13 @@
     5.4  
     5.5  theory EvenOdd imports Int2 begin
     5.6  
     5.7 -text{*Note.  This theory is being revised.  See the web page
     5.8 -\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
     5.9 -
    5.10 -constdefs
    5.11 +definition
    5.12    zOdd    :: "int set"
    5.13 -  "zOdd == {x. \<exists>k. x = 2 * k + 1}"
    5.14 +  "zOdd = {x. \<exists>k. x = 2 * k + 1}"
    5.15    zEven   :: "int set"
    5.16 -  "zEven == {x. \<exists>k. x = 2 * k}"
    5.17 +  "zEven = {x. \<exists>k. x = 2 * k}"
    5.18  
    5.19 -(***********************************************************)
    5.20 -(*                                                         *)
    5.21 -(* Some useful properties about even and odd               *)
    5.22 -(*                                                         *)
    5.23 -(***********************************************************)
    5.24 +subsection {* Some useful properties about even and odd *}
    5.25  
    5.26  lemma zOddI [intro?]: "x = 2 * k + 1 \<Longrightarrow> x \<in> zOdd"
    5.27    and zOddE [elim?]: "x \<in> zOdd \<Longrightarrow> (!!k. x = 2 * k + 1 \<Longrightarrow> C) \<Longrightarrow> C"
     6.1 --- a/src/HOL/NumberTheory/Factorization.thy	Wed May 17 01:23:40 2006 +0200
     6.2 +++ b/src/HOL/NumberTheory/Factorization.thy	Wed May 17 01:23:41 2006 +0200
     6.3 @@ -11,16 +11,16 @@
     6.4  
     6.5  subsection {* Definitions *}
     6.6  
     6.7 +definition
     6.8 +  primel :: "nat list => bool "
     6.9 +  "primel xs = (\<forall>p \<in> set xs. prime p)"
    6.10 +
    6.11  consts
    6.12 -  primel :: "nat list => bool "
    6.13    nondec :: "nat list => bool "
    6.14    prod :: "nat list => nat"
    6.15    oinsert :: "nat => nat list => nat list"
    6.16    sort :: "nat list => nat list"
    6.17  
    6.18 -defs
    6.19 -  primel_def: "primel xs == \<forall>p \<in> set xs. prime p"
    6.20 -
    6.21  primrec
    6.22    "nondec [] = True"
    6.23    "nondec (x # xs) = (case xs of [] => True | y # ys => x \<le> y \<and> nondec xs)"
    6.24 @@ -41,12 +41,12 @@
    6.25  subsection {* Arithmetic *}
    6.26  
    6.27  lemma one_less_m: "(m::nat) \<noteq> m * k ==> m \<noteq> Suc 0 ==> Suc 0 < m"
    6.28 -  apply (case_tac m)
    6.29 +  apply (cases m)
    6.30     apply auto
    6.31    done
    6.32  
    6.33  lemma one_less_k: "(m::nat) \<noteq> m * k ==> Suc 0 < m * k ==> Suc 0 < k"
    6.34 -  apply (case_tac k)
    6.35 +  apply (cases k)
    6.36     apply auto
    6.37    done
    6.38  
    6.39 @@ -55,7 +55,7 @@
    6.40    done
    6.41  
    6.42  lemma mn_eq_m_one: "(0::nat) < m ==> m * n = m ==> n = Suc 0"
    6.43 -  apply (case_tac n)
    6.44 +  apply (cases n)
    6.45     apply auto
    6.46    done
    6.47  
    6.48 @@ -116,9 +116,8 @@
    6.49    done
    6.50  
    6.51  lemma primel_one_empty: "primel xs ==> prod xs = Suc 0 ==> xs = []"
    6.52 -  apply (unfold primel_def prime_def)
    6.53 -  apply (case_tac xs)
    6.54 -   apply simp_all
    6.55 +  apply (cases xs)
    6.56 +   apply (simp_all add: primel_def prime_def)
    6.57    done
    6.58  
    6.59  lemma prime_g_one: "prime p ==> Suc 0 < p"
    6.60 @@ -131,25 +130,25 @@
    6.61    apply auto
    6.62    done
    6.63  
    6.64 -lemma primel_nempty_g_one [rule_format]:
    6.65 -    "primel xs --> xs \<noteq> [] --> Suc 0 < prod xs"
    6.66 -  apply (unfold primel_def prime_def)
    6.67 +lemma primel_nempty_g_one:
    6.68 +    "primel xs \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> Suc 0 < prod xs"
    6.69    apply (induct xs)
    6.70 -   apply (auto elim: one_less_mult)
    6.71 +   apply simp
    6.72 +  apply (fastsimp simp: primel_def prime_def elim: one_less_mult)
    6.73    done
    6.74  
    6.75  lemma primel_prod_gz: "primel xs ==> 0 < prod xs"
    6.76 -  apply (unfold primel_def prime_def)
    6.77    apply (induct xs)
    6.78 -   apply auto
    6.79 +   apply (auto simp: primel_def prime_def)
    6.80    done
    6.81  
    6.82  
    6.83  subsection {* Sorting *}
    6.84  
    6.85 -lemma nondec_oinsert [rule_format]: "nondec xs --> nondec (oinsert x xs)"
    6.86 +lemma nondec_oinsert: "nondec xs \<Longrightarrow> nondec (oinsert x xs)"
    6.87    apply (induct xs)
    6.88 -   apply (case_tac [2] xs)
    6.89 +   apply simp
    6.90 +   apply (case_tac xs)
    6.91      apply (simp_all cong del: list.weak_case_cong)
    6.92    done
    6.93  
    6.94 @@ -163,7 +162,7 @@
    6.95    apply simp_all
    6.96    done
    6.97  
    6.98 -lemma nondec_sort_eq [rule_format]: "nondec xs --> xs = sort xs"
    6.99 +lemma nondec_sort_eq [rule_format]: "nondec xs \<longrightarrow> xs = sort xs"
   6.100    apply (induct xs)
   6.101     apply safe
   6.102      apply simp_all
   6.103 @@ -185,7 +184,7 @@
   6.104  
   6.105  lemma perm_primel [rule_format]: "xs <~~> ys ==> primel xs --> primel ys"
   6.106    apply (unfold primel_def)
   6.107 -  apply (erule perm.induct)
   6.108 +  apply (induct set: perm)
   6.109       apply simp
   6.110      apply simp
   6.111     apply (simp (no_asm))
   6.112 @@ -193,13 +192,13 @@
   6.113    apply blast
   6.114    done
   6.115  
   6.116 -lemma perm_prod [rule_format]: "xs <~~> ys ==> prod xs = prod ys"
   6.117 -  apply (erule perm.induct)
   6.118 +lemma perm_prod: "xs <~~> ys ==> prod xs = prod ys"
   6.119 +  apply (induct set: perm)
   6.120       apply (simp_all add: mult_ac)
   6.121    done
   6.122  
   6.123  lemma perm_subst_oinsert: "xs <~~> ys ==> oinsert a xs <~~> oinsert a ys"
   6.124 -  apply (erule perm.induct)
   6.125 +  apply (induct set: perm)
   6.126       apply auto
   6.127    done
   6.128  
   6.129 @@ -214,7 +213,7 @@
   6.130    done
   6.131  
   6.132  lemma perm_sort_eq: "xs <~~> ys ==> sort xs = sort ys"
   6.133 -  apply (erule perm.induct)
   6.134 +  apply (induct set: perm)
   6.135       apply (simp_all add: oinsert_x_y)
   6.136    done
   6.137  
     7.1 --- a/src/HOL/NumberTheory/Finite2.thy	Wed May 17 01:23:40 2006 +0200
     7.2 +++ b/src/HOL/NumberTheory/Finite2.thy	Wed May 17 01:23:41 2006 +0200
     7.3 @@ -9,23 +9,17 @@
     7.4  imports IntFact
     7.5  begin
     7.6  
     7.7 -text{*These are useful for combinatorial and number-theoretic counting
     7.8 -arguments.*}
     7.9 -
    7.10 -text{*Note.  This theory is being revised.  See the web page
    7.11 -\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
    7.12 +text{*
    7.13 +  These are useful for combinatorial and number-theoretic counting
    7.14 +  arguments.
    7.15 +*}
    7.16  
    7.17 -(******************************************************************)
    7.18 -(*                                                                *)
    7.19 -(* Useful properties of sums and products                         *)
    7.20 -(*                                                                *)
    7.21 -(******************************************************************)
    7.22  
    7.23  subsection {* Useful properties of sums and products *}
    7.24  
    7.25  lemma setsum_same_function_zcong:
    7.26 -assumes a: "\<forall>x \<in> S. [f x = g x](mod m)"
    7.27 -shows "[setsum f S = setsum g S] (mod m)"
    7.28 +  assumes a: "\<forall>x \<in> S. [f x = g x](mod m)"
    7.29 +  shows "[setsum f S = setsum g S] (mod m)"
    7.30  proof cases
    7.31    assume "finite S"
    7.32    thus ?thesis using a by induct (simp_all add: zcong_zadd)
    7.33 @@ -34,8 +28,8 @@
    7.34  qed
    7.35  
    7.36  lemma setprod_same_function_zcong:
    7.37 -assumes a: "\<forall>x \<in> S. [f x = g x](mod m)"
    7.38 -shows "[setprod f S = setprod g S] (mod m)"
    7.39 +  assumes a: "\<forall>x \<in> S. [f x = g x](mod m)"
    7.40 +  shows "[setprod f S = setprod g S] (mod m)"
    7.41  proof cases
    7.42    assume "finite S"
    7.43    thus ?thesis using a by induct (simp_all add: zcong_zmult)
    7.44 @@ -59,12 +53,6 @@
    7.45    by (induct set: Finites) (auto simp add: zadd_zmult_distrib2)
    7.46  
    7.47  
    7.48 -(******************************************************************)
    7.49 -(*                                                                *)
    7.50 -(* Cardinality of some explicit finite sets                       *)
    7.51 -(*                                                                *)
    7.52 -(******************************************************************)
    7.53 -
    7.54  subsection {* Cardinality of explicit finite sets *}
    7.55  
    7.56  lemma finite_surjI: "[| B \<subseteq> f ` A; finite A |] ==> finite B"
    7.57 @@ -80,19 +68,19 @@
    7.58  qed
    7.59  
    7.60  lemma  bdd_int_set_l_finite: "finite {x::int. 0 \<le> x & x < n}"
    7.61 -apply (subgoal_tac " {(x :: int). 0 \<le> x & x < n} \<subseteq>
    7.62 -    int ` {(x :: nat). x < nat n}")
    7.63 -apply (erule finite_surjI)
    7.64 -apply (auto simp add: bdd_nat_set_l_finite image_def)
    7.65 -apply (rule_tac x = "nat x" in exI, simp)
    7.66 -done
    7.67 +  apply (subgoal_tac " {(x :: int). 0 \<le> x & x < n} \<subseteq>
    7.68 +      int ` {(x :: nat). x < nat n}")
    7.69 +   apply (erule finite_surjI)
    7.70 +   apply (auto simp add: bdd_nat_set_l_finite image_def)
    7.71 +  apply (rule_tac x = "nat x" in exI, simp)
    7.72 +  done
    7.73  
    7.74  lemma bdd_int_set_le_finite: "finite {x::int. 0 \<le> x & x \<le> n}"
    7.75 -apply (subgoal_tac "{x. 0 \<le> x & x \<le> n} = {x. 0 \<le> x & x < n + 1}")
    7.76 -apply (erule ssubst)
    7.77 -apply (rule bdd_int_set_l_finite)
    7.78 -apply auto
    7.79 -done
    7.80 +  apply (subgoal_tac "{x. 0 \<le> x & x \<le> n} = {x. 0 \<le> x & x < n + 1}")
    7.81 +   apply (erule ssubst)
    7.82 +   apply (rule bdd_int_set_l_finite)
    7.83 +  apply auto
    7.84 +  done
    7.85  
    7.86  lemma bdd_int_set_l_l_finite: "finite {x::int. 0 < x & x < n}"
    7.87  proof -
    7.88 @@ -192,7 +180,7 @@
    7.89      int(card {x. 0 < x & x < n}) = n - 1"
    7.90    apply (auto simp add: card_bdd_int_set_l_l)
    7.91    apply (subgoal_tac "Suc 0 \<le> nat n")
    7.92 -  apply (auto simp add: zdiff_int [symmetric])
    7.93 +   apply (auto simp add: zdiff_int [symmetric])
    7.94    apply (subgoal_tac "0 < nat n", arith)
    7.95    apply (simp add: zero_less_nat_eq)
    7.96    done
    7.97 @@ -201,11 +189,6 @@
    7.98      int(card {x. 0 < x & x \<le> n}) = n"
    7.99    by (auto simp add: card_bdd_int_set_l_le)
   7.100  
   7.101 -(******************************************************************)
   7.102 -(*                                                                *)
   7.103 -(* Cartesian products of finite sets                              *)
   7.104 -(*                                                                *)
   7.105 -(******************************************************************)
   7.106  
   7.107  subsection {* Cardinality of finite cartesian products *}
   7.108  
   7.109 @@ -214,35 +197,29 @@
   7.110    by blast
   7.111   *)
   7.112  
   7.113 -(******************************************************************)
   7.114 -(*                                                                *)
   7.115 -(* Sums and products over finite sets                             *)
   7.116 -(*                                                                *)
   7.117 -(******************************************************************)
   7.118 -
   7.119 -subsection {* Lemmas for counting arguments *}
   7.120 +text {* Lemmas for counting arguments. *}
   7.121  
   7.122  lemma setsum_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A;
   7.123      g ` B \<subseteq> A; inj_on g B |] ==> setsum g B = setsum (g \<circ> f) A"
   7.124 -apply (frule_tac h = g and f = f in setsum_reindex)
   7.125 -apply (subgoal_tac "setsum g B = setsum g (f ` A)")
   7.126 -apply (simp add: inj_on_def)
   7.127 -apply (subgoal_tac "card A = card B")
   7.128 -apply (drule_tac A = "f ` A" and B = B in card_seteq)
   7.129 -apply (auto simp add: card_image)
   7.130 -apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
   7.131 -apply (frule_tac A = B and B = A and f = g in card_inj_on_le)
   7.132 -apply auto
   7.133 -done
   7.134 +  apply (frule_tac h = g and f = f in setsum_reindex)
   7.135 +  apply (subgoal_tac "setsum g B = setsum g (f ` A)")
   7.136 +   apply (simp add: inj_on_def)
   7.137 +  apply (subgoal_tac "card A = card B")
   7.138 +   apply (drule_tac A = "f ` A" and B = B in card_seteq)
   7.139 +     apply (auto simp add: card_image)
   7.140 +  apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
   7.141 +  apply (frule_tac A = B and B = A and f = g in card_inj_on_le)
   7.142 +    apply auto
   7.143 +  done
   7.144  
   7.145  lemma setprod_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A;
   7.146      g ` B \<subseteq> A; inj_on g B |] ==> setprod g B = setprod (g \<circ> f) A"
   7.147    apply (frule_tac h = g and f = f in setprod_reindex)
   7.148    apply (subgoal_tac "setprod g B = setprod g (f ` A)")
   7.149 -  apply (simp add: inj_on_def)
   7.150 +   apply (simp add: inj_on_def)
   7.151    apply (subgoal_tac "card A = card B")
   7.152 -  apply (drule_tac A = "f ` A" and B = B in card_seteq)
   7.153 -  apply (auto simp add: card_image)
   7.154 +   apply (drule_tac A = "f ` A" and B = B in card_seteq)
   7.155 +     apply (auto simp add: card_image)
   7.156    apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
   7.157    apply (frule_tac A = B and B = A and f = g in card_inj_on_le, auto)
   7.158    done
     8.1 --- a/src/HOL/NumberTheory/Int2.thy	Wed May 17 01:23:40 2006 +0200
     8.2 +++ b/src/HOL/NumberTheory/Int2.thy	Wed May 17 01:23:41 2006 +0200
     8.3 @@ -7,18 +7,12 @@
     8.4  
     8.5  theory Int2 imports Finite2 WilsonRuss begin
     8.6  
     8.7 -text{*Note.  This theory is being revised.  See the web page
     8.8 -\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
     8.9 +definition
    8.10 +  MultInv :: "int => int => int"
    8.11 +  "MultInv p x = x ^ nat (p - 2)"
    8.12  
    8.13 -constdefs
    8.14 -  MultInv :: "int => int => int" 
    8.15 -  "MultInv p x == x ^ nat (p - 2)"
    8.16  
    8.17 -(*****************************************************************)
    8.18 -(*                                                               *)
    8.19 -(* Useful lemmas about dvd and powers                            *)
    8.20 -(*                                                               *)
    8.21 -(*****************************************************************)
    8.22 +subsection {* Useful lemmas about dvd and powers *}
    8.23  
    8.24  lemma zpower_zdvd_prop1:
    8.25    "0 < n \<Longrightarrow> p dvd y \<Longrightarrow> p dvd ((y::int) ^ n)"
    8.26 @@ -32,7 +26,7 @@
    8.27    then show ?thesis by auto
    8.28  qed
    8.29  
    8.30 -lemma zprime_zdvd_zmult_better: "[| zprime p;  p dvd (m * n) |] ==> 
    8.31 +lemma zprime_zdvd_zmult_better: "[| zprime p;  p dvd (m * n) |] ==>
    8.32      (p dvd m) | (p dvd n)"
    8.33    apply (cases "0 \<le> m")
    8.34    apply (simp add: zprime_zdvd_zmult)
    8.35 @@ -83,11 +77,8 @@
    8.36      by arith
    8.37  qed
    8.38  
    8.39 -(*****************************************************************)
    8.40 -(*                                                               *)
    8.41 -(* Useful properties of congruences                              *)
    8.42 -(*                                                               *)
    8.43 -(*****************************************************************)
    8.44 +
    8.45 +subsection {* Useful properties of congruences *}
    8.46  
    8.47  lemma zcong_eq_zdvd_prop: "[x = 0](mod p) = (p dvd x)"
    8.48    by (auto simp add: zcong_def)
    8.49 @@ -101,7 +92,7 @@
    8.50  lemma zcong_zpower: "[x = y](mod m) ==> [x^z = y^z](mod m)"
    8.51    by (induct z) (auto simp add: zcong_zmult)
    8.52  
    8.53 -lemma zcong_eq_trans: "[| [a = b](mod m); b = c; [c = d](mod m) |] ==> 
    8.54 +lemma zcong_eq_trans: "[| [a = b](mod m); b = c; [c = d](mod m) |] ==>
    8.55      [a = d](mod m)"
    8.56    apply (erule zcong_trans)
    8.57    apply simp
    8.58 @@ -110,7 +101,7 @@
    8.59  lemma aux1: "a - b = (c::int) ==> a = c + b"
    8.60    by auto
    8.61  
    8.62 -lemma zcong_zmult_prop1: "[a = b](mod m) ==> ([c = a * d](mod m) = 
    8.63 +lemma zcong_zmult_prop1: "[a = b](mod m) ==> ([c = a * d](mod m) =
    8.64      [c = b * d] (mod m))"
    8.65    apply (auto simp add: zcong_def dvd_def)
    8.66    apply (rule_tac x = "ka + k * d" in exI)
    8.67 @@ -121,17 +112,17 @@
    8.68    apply (auto simp add: int_distrib)
    8.69    done
    8.70  
    8.71 -lemma zcong_zmult_prop2: "[a = b](mod m) ==> 
    8.72 +lemma zcong_zmult_prop2: "[a = b](mod m) ==>
    8.73      ([c = d * a](mod m) = [c = d * b] (mod m))"
    8.74    by (auto simp add: zmult_ac zcong_zmult_prop1)
    8.75  
    8.76 -lemma zcong_zmult_prop3: "[| zprime p; ~[x = 0] (mod p); 
    8.77 +lemma zcong_zmult_prop3: "[| zprime p; ~[x = 0] (mod p);
    8.78      ~[y = 0] (mod p) |] ==> ~[x * y = 0] (mod p)"
    8.79    apply (auto simp add: zcong_def)
    8.80    apply (drule zprime_zdvd_zmult_better, auto)
    8.81    done
    8.82  
    8.83 -lemma zcong_less_eq: "[| 0 < x; 0 < y; 0 < m; [x = y] (mod m); 
    8.84 +lemma zcong_less_eq: "[| 0 < x; 0 < y; 0 < m; [x = y] (mod m);
    8.85      x < m; y < m |] ==> x = y"
    8.86    apply (simp add: zcong_zmod_eq)
    8.87    apply (subgoal_tac "(x mod m) = x")
    8.88 @@ -141,7 +132,7 @@
    8.89    apply auto
    8.90    done
    8.91  
    8.92 -lemma zcong_neg_1_impl_ne_1: "[| 2 < p; [x = -1] (mod p) |] ==> 
    8.93 +lemma zcong_neg_1_impl_ne_1: "[| 2 < p; [x = -1] (mod p) |] ==>
    8.94      ~([x = 1] (mod p))"
    8.95  proof
    8.96    assume "2 < p" and "[x = 1] (mod p)" and "[x = -1] (mod p)"
    8.97 @@ -162,18 +153,18 @@
    8.98  lemma zcong_zero_equiv_div: "[a = 0] (mod m) = (m dvd a)"
    8.99    by (auto simp add: zcong_def)
   8.100  
   8.101 -lemma zcong_zprime_prod_zero: "[| zprime p; 0 < a |] ==> 
   8.102 -    [a * b = 0] (mod p) ==> [a = 0] (mod p) | [b = 0] (mod p)" 
   8.103 +lemma zcong_zprime_prod_zero: "[| zprime p; 0 < a |] ==>
   8.104 +    [a * b = 0] (mod p) ==> [a = 0] (mod p) | [b = 0] (mod p)"
   8.105    by (auto simp add: zcong_zero_equiv_div zprime_zdvd_zmult)
   8.106  
   8.107  lemma zcong_zprime_prod_zero_contra: "[| zprime p; 0 < a |] ==>
   8.108    ~[a = 0](mod p) & ~[b = 0](mod p) ==> ~[a * b = 0] (mod p)"
   8.109 -  apply auto 
   8.110 +  apply auto
   8.111    apply (frule_tac a = a and b = b and p = p in zcong_zprime_prod_zero)
   8.112    apply auto
   8.113    done
   8.114  
   8.115 -lemma zcong_not_zero: "[| 0 < x; x < m |] ==> ~[x = 0] (mod m)" 
   8.116 +lemma zcong_not_zero: "[| 0 < x; x < m |] ==> ~[x = 0] (mod m)"
   8.117    by (auto simp add: zcong_zero_equiv_div zdvd_not_zless)
   8.118  
   8.119  lemma zcong_zero: "[| 0 \<le> x; x < m; [x = 0](mod m) |] ==> x = 0"
   8.120 @@ -186,17 +177,14 @@
   8.121      ==> zgcd (setprod id A,y) = 1"
   8.122    by (induct set: Finites) (auto simp add: zgcd_zgcd_zmult)
   8.123  
   8.124 -(*****************************************************************)
   8.125 -(*                                                               *)
   8.126 -(* Some properties of MultInv                                    *)
   8.127 -(*                                                               *)
   8.128 -(*****************************************************************)
   8.129  
   8.130 -lemma MultInv_prop1: "[| 2 < p; [x = y] (mod p) |] ==> 
   8.131 +subsection {* Some properties of MultInv *}
   8.132 +
   8.133 +lemma MultInv_prop1: "[| 2 < p; [x = y] (mod p) |] ==>
   8.134      [(MultInv p x) = (MultInv p y)] (mod p)"
   8.135    by (auto simp add: MultInv_def zcong_zpower)
   8.136  
   8.137 -lemma MultInv_prop2: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> 
   8.138 +lemma MultInv_prop2: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
   8.139    [(x * (MultInv p x)) = 1] (mod p)"
   8.140  proof (simp add: MultInv_def zcong_eq_zdvd_prop)
   8.141    assume "2 < p" and "zprime p" and "~ p dvd x"
   8.142 @@ -208,11 +196,11 @@
   8.143    finally have "[x * x ^ nat (p - 2) = x ^ nat (p - 1)] (mod p)"
   8.144      by (rule ssubst, auto)
   8.145    also from prems have "[x ^ nat (p - 1) = 1] (mod p)"
   8.146 -    by (auto simp add: Little_Fermat) 
   8.147 +    by (auto simp add: Little_Fermat)
   8.148    finally (zcong_trans) show "[x * x ^ nat (p - 2) = 1] (mod p)" .
   8.149  qed
   8.150  
   8.151 -lemma MultInv_prop2a: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> 
   8.152 +lemma MultInv_prop2a: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
   8.153      [(MultInv p x) * x = 1] (mod p)"
   8.154    by (auto simp add: MultInv_prop2 zmult_ac)
   8.155  
   8.156 @@ -222,15 +210,15 @@
   8.157  lemma aux_2: "2 < p ==> 0 < nat (p - 2)"
   8.158    by auto
   8.159  
   8.160 -lemma MultInv_prop3: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> 
   8.161 +lemma MultInv_prop3: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
   8.162      ~([MultInv p x = 0](mod p))"
   8.163    apply (auto simp add: MultInv_def zcong_eq_zdvd_prop aux_1)
   8.164    apply (drule aux_2)
   8.165    apply (drule zpower_zdvd_prop2, auto)
   8.166    done
   8.167  
   8.168 -lemma aux__1: "[| 2 < p; zprime p; ~([x = 0](mod p))|] ==> 
   8.169 -    [(MultInv p (MultInv p x)) = (x * (MultInv p x) * 
   8.170 +lemma aux__1: "[| 2 < p; zprime p; ~([x = 0](mod p))|] ==>
   8.171 +    [(MultInv p (MultInv p x)) = (x * (MultInv p x) *
   8.172        (MultInv p (MultInv p x)))] (mod p)"
   8.173    apply (drule MultInv_prop2, auto)
   8.174    apply (drule_tac k = "MultInv p (MultInv p x)" in zcong_scalar, auto)
   8.175 @@ -246,17 +234,17 @@
   8.176    apply (auto simp add: zmult_ac)
   8.177    done
   8.178  
   8.179 -lemma MultInv_prop4: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> 
   8.180 +lemma MultInv_prop4: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
   8.181      [(MultInv p (MultInv p x)) = x] (mod p)"
   8.182    apply (frule aux__1, auto)
   8.183    apply (drule aux__2, auto)
   8.184    apply (drule zcong_trans, auto)
   8.185    done
   8.186  
   8.187 -lemma MultInv_prop5: "[| 2 < p; zprime p; ~([x = 0](mod p)); 
   8.188 -    ~([y = 0](mod p)); [(MultInv p x) = (MultInv p y)] (mod p) |] ==> 
   8.189 +lemma MultInv_prop5: "[| 2 < p; zprime p; ~([x = 0](mod p));
   8.190 +    ~([y = 0](mod p)); [(MultInv p x) = (MultInv p y)] (mod p) |] ==>
   8.191      [x = y] (mod p)"
   8.192 -  apply (drule_tac a = "MultInv p x" and b = "MultInv p y" and 
   8.193 +  apply (drule_tac a = "MultInv p x" and b = "MultInv p y" and
   8.194      m = p and k = x in zcong_scalar)
   8.195    apply (insert MultInv_prop2 [of p x], simp)
   8.196    apply (auto simp only: zcong_sym [of "MultInv p x * x"])
   8.197 @@ -268,43 +256,43 @@
   8.198    apply (auto simp add: zcong_sym)
   8.199    done
   8.200  
   8.201 -lemma MultInv_zcong_prop1: "[| 2 < p; [j = k] (mod p) |] ==> 
   8.202 +lemma MultInv_zcong_prop1: "[| 2 < p; [j = k] (mod p) |] ==>
   8.203      [a * MultInv p j = a * MultInv p k] (mod p)"
   8.204    by (drule MultInv_prop1, auto simp add: zcong_scalar2)
   8.205  
   8.206 -lemma aux___1: "[j = a * MultInv p k] (mod p) ==> 
   8.207 +lemma aux___1: "[j = a * MultInv p k] (mod p) ==>
   8.208      [j * k = a * MultInv p k * k] (mod p)"
   8.209    by (auto simp add: zcong_scalar)
   8.210  
   8.211 -lemma aux___2: "[|2 < p; zprime p; ~([k = 0](mod p)); 
   8.212 +lemma aux___2: "[|2 < p; zprime p; ~([k = 0](mod p));
   8.213      [j * k = a * MultInv p k * k] (mod p) |] ==> [j * k = a] (mod p)"
   8.214 -  apply (insert MultInv_prop2a [of p k] zcong_zmult_prop2 
   8.215 +  apply (insert MultInv_prop2a [of p k] zcong_zmult_prop2
   8.216      [of "MultInv p k * k" 1 p "j * k" a])
   8.217    apply (auto simp add: zmult_ac)
   8.218    done
   8.219  
   8.220 -lemma aux___3: "[j * k = a] (mod p) ==> [(MultInv p j) * j * k = 
   8.221 +lemma aux___3: "[j * k = a] (mod p) ==> [(MultInv p j) * j * k =
   8.222       (MultInv p j) * a] (mod p)"
   8.223    by (auto simp add: zmult_assoc zcong_scalar2)
   8.224  
   8.225 -lemma aux___4: "[|2 < p; zprime p; ~([j = 0](mod p)); 
   8.226 +lemma aux___4: "[|2 < p; zprime p; ~([j = 0](mod p));
   8.227      [(MultInv p j) * j * k = (MultInv p j) * a] (mod p) |]
   8.228         ==> [k = a * (MultInv p j)] (mod p)"
   8.229 -  apply (insert MultInv_prop2a [of p j] zcong_zmult_prop1 
   8.230 +  apply (insert MultInv_prop2a [of p j] zcong_zmult_prop1
   8.231      [of "MultInv p j * j" 1 p "MultInv p j * a" k])
   8.232    apply (auto simp add: zmult_ac zcong_sym)
   8.233    done
   8.234  
   8.235 -lemma MultInv_zcong_prop2: "[| 2 < p; zprime p; ~([k = 0](mod p)); 
   8.236 -    ~([j = 0](mod p)); [j = a * MultInv p k] (mod p) |] ==> 
   8.237 +lemma MultInv_zcong_prop2: "[| 2 < p; zprime p; ~([k = 0](mod p));
   8.238 +    ~([j = 0](mod p)); [j = a * MultInv p k] (mod p) |] ==>
   8.239      [k = a * MultInv p j] (mod p)"
   8.240    apply (drule aux___1)
   8.241    apply (frule aux___2, auto)
   8.242    by (drule aux___3, drule aux___4, auto)
   8.243  
   8.244 -lemma MultInv_zcong_prop3: "[| 2 < p; zprime p; ~([a = 0](mod p)); 
   8.245 +lemma MultInv_zcong_prop3: "[| 2 < p; zprime p; ~([a = 0](mod p));
   8.246      ~([k = 0](mod p)); ~([j = 0](mod p));
   8.247 -    [a * MultInv p j = a * MultInv p k] (mod p) |] ==> 
   8.248 +    [a * MultInv p j = a * MultInv p k] (mod p) |] ==>
   8.249        [j = k] (mod p)"
   8.250    apply (auto simp add: zcong_eq_zdvd_prop [of a p])
   8.251    apply (frule zprime_imp_zrelprime, auto)
     9.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Wed May 17 01:23:40 2006 +0200
     9.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Wed May 17 01:23:41 2006 +0200
     9.3 @@ -31,18 +31,18 @@
     9.4  		      s, s' - (r' div r) * s, 
     9.5  		      t, t' - (r' div r) * t))"
     9.6  
     9.7 -constdefs
     9.8 +definition
     9.9    zgcd :: "int * int => int"
    9.10 -  "zgcd == \<lambda>(x,y). int (gcd (nat (abs x), nat (abs y)))"
    9.11 +  "zgcd = (\<lambda>(x,y). int (gcd (nat (abs x), nat (abs y))))"
    9.12  
    9.13    zprime :: "int \<Rightarrow> bool"
    9.14 -  "zprime p == 1 < p \<and> (\<forall>m. 0 <= m & m dvd p --> m = 1 \<or> m = p)"
    9.15 +  "zprime p = (1 < p \<and> (\<forall>m. 0 <= m & m dvd p --> m = 1 \<or> m = p))"
    9.16  
    9.17    xzgcd :: "int => int => int * int * int"
    9.18 -  "xzgcd m n == xzgcda (m, n, m, n, 1, 0, 0, 1)"
    9.19 +  "xzgcd m n = xzgcda (m, n, m, n, 1, 0, 0, 1)"
    9.20  
    9.21    zcong :: "int => int => int => bool"    ("(1[_ = _] '(mod _'))")
    9.22 -  "[a = b] (mod m) == m dvd (a - b)"
    9.23 +  "[a = b] (mod m) = (m dvd (a - b))"
    9.24  
    9.25  
    9.26  
    10.1 --- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Wed May 17 01:23:40 2006 +0200
    10.2 +++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Wed May 17 01:23:41 2006 +0200
    10.3 @@ -9,12 +9,10 @@
    10.4  imports Gauss
    10.5  begin
    10.6  
    10.7 -(***************************************************************)
    10.8 -(*                                                             *)
    10.9 -(*  Lemmas leading up to the proof of theorem 3.3 in           *)
   10.10 -(*  Niven and Zuckerman's presentation                         *)
   10.11 -(*                                                             *)
   10.12 -(***************************************************************)
   10.13 +text {*
   10.14 +  Lemmas leading up to the proof of theorem 3.3 in Niven and
   10.15 +  Zuckerman's presentation.
   10.16 +*}
   10.17  
   10.18  lemma (in GAUSS) QRLemma1: "a * setsum id A =
   10.19    p * setsum (%x. ((x * a) div p)) A + setsum id D + setsum id E"
   10.20 @@ -149,11 +147,8 @@
   10.21    apply (auto simp add: GAUSS_def)
   10.22    done
   10.23  
   10.24 -(******************************************************************)
   10.25 -(*                                                                *)
   10.26 -(* Stuff about S, S1 and S2...                                    *)
   10.27 -(*                                                                *)
   10.28 -(******************************************************************)
   10.29 +
   10.30 +subsection {* Stuff about S, S1 and S2 *}
   10.31  
   10.32  locale QRTEMP =
   10.33    fixes p     :: "int"
    11.1 --- a/src/HOL/NumberTheory/Residues.thy	Wed May 17 01:23:40 2006 +0200
    11.2 +++ b/src/HOL/NumberTheory/Residues.thy	Wed May 17 01:23:41 2006 +0200
    11.3 @@ -7,45 +7,33 @@
    11.4  
    11.5  theory Residues imports Int2 begin
    11.6  
    11.7 -text{*Note.  This theory is being revised.  See the web page
    11.8 -\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
    11.9 +text {*
   11.10 +  \medskip Define the residue of a set, the standard residue,
   11.11 +  quadratic residues, and prove some basic properties. *}
   11.12  
   11.13 -(*****************************************************************)
   11.14 -(*                                                               *)
   11.15 -(* Define the residue of a set, the standard residue, quadratic  *)
   11.16 -(* residues, and prove some basic properties.                    *)
   11.17 -(*                                                               *)
   11.18 -(*****************************************************************)
   11.19 -
   11.20 -constdefs
   11.21 +definition
   11.22    ResSet      :: "int => int set => bool"
   11.23 -  "ResSet m X == \<forall>y1 y2. (((y1 \<in> X) & (y2 \<in> X) & [y1 = y2] (mod m)) --> 
   11.24 -    y1 = y2)"
   11.25 +  "ResSet m X = (\<forall>y1 y2. (y1 \<in> X & y2 \<in> X & [y1 = y2] (mod m) --> y1 = y2))"
   11.26  
   11.27    StandardRes :: "int => int => int"
   11.28 -  "StandardRes m x == x mod m"
   11.29 +  "StandardRes m x = x mod m"
   11.30  
   11.31    QuadRes     :: "int => int => bool"
   11.32 -  "QuadRes m x == \<exists>y. ([(y ^ 2) = x] (mod m))"
   11.33 +  "QuadRes m x = (\<exists>y. ([(y ^ 2) = x] (mod m)))"
   11.34  
   11.35    Legendre    :: "int => int => int"      
   11.36 -  "Legendre a p == (if ([a = 0] (mod p)) then 0
   11.37 +  "Legendre a p = (if ([a = 0] (mod p)) then 0
   11.38                       else if (QuadRes p a) then 1
   11.39                       else -1)"
   11.40  
   11.41    SR          :: "int => int set"
   11.42 -  "SR p == {x. (0 \<le> x) & (x < p)}"
   11.43 +  "SR p = {x. (0 \<le> x) & (x < p)}"
   11.44  
   11.45    SRStar      :: "int => int set"
   11.46 -  "SRStar p == {x. (0 < x) & (x < p)}"
   11.47 +  "SRStar p = {x. (0 < x) & (x < p)}"
   11.48  
   11.49 -(******************************************************************)
   11.50 -(*                                                                *)
   11.51 -(* Some useful properties of StandardRes                          *)
   11.52 -(*                                                                *)
   11.53 -(******************************************************************)
   11.54  
   11.55 -subsection {* Properties of StandardRes *}
   11.56 +subsection {* Some useful properties of StandardRes *}
   11.57  
   11.58  lemma StandardRes_prop1: "[x = StandardRes m x] (mod m)"
   11.59    by (auto simp add: StandardRes_def zcong_zmod)
   11.60 @@ -72,11 +60,6 @@
   11.61     "(StandardRes m x = 0) = ([x = 0](mod m))"
   11.62    by (auto simp add: StandardRes_def zcong_eq_zdvd_prop dvd_def) 
   11.63  
   11.64 -(******************************************************************)
   11.65 -(*                                                                *)
   11.66 -(* Some useful stuff relating StandardRes and SRStar and SR       *)
   11.67 -(*                                                                *)
   11.68 -(******************************************************************)
   11.69  
   11.70  subsection {* Relations between StandardRes, SRStar, and SR *}
   11.71  
   11.72 @@ -132,11 +115,6 @@
   11.73  lemma SRStar_finite: "2 < p ==> finite( SRStar p)"
   11.74    by (auto simp add: SRStar_def bdd_int_set_l_l_finite)
   11.75  
   11.76 -(******************************************************************)
   11.77 -(*                                                                *)
   11.78 -(* Some useful stuff about ResSet and StandardRes                 *)
   11.79 -(*                                                                *)
   11.80 -(******************************************************************)
   11.81  
   11.82  subsection {* Properties relating ResSets with StandardRes *}
   11.83  
   11.84 @@ -175,14 +153,13 @@
   11.85    apply (auto intro!: zcong_zmult simp add: StandardRes_prop1)
   11.86    done
   11.87  
   11.88 -lemma ResSet_image: "[| 0 < m; ResSet m A; \<forall>x \<in> A. \<forall>y \<in> A. ([f x = f y](mod m) --> x = y) |] ==> ResSet m (f ` A)"
   11.89 +lemma ResSet_image:
   11.90 +  "[| 0 < m; ResSet m A; \<forall>x \<in> A. \<forall>y \<in> A. ([f x = f y](mod m) --> x = y) |] ==>
   11.91 +    ResSet m (f ` A)"
   11.92    by (auto simp add: ResSet_def)
   11.93  
   11.94 -(****************************************************************)
   11.95 -(*                                                              *)
   11.96 -(* Property for SRStar                                          *)
   11.97 -(*                                                              *)
   11.98 -(****************************************************************)
   11.99 +
  11.100 +subsection {* Property for SRStar *}
  11.101  
  11.102  lemma ResSet_SRStar_prop: "ResSet p (SRStar p)"
  11.103    by (auto simp add: SRStar_def ResSet_def zcong_zless_imp_eq)
    12.1 --- a/src/HOL/NumberTheory/WilsonBij.thy	Wed May 17 01:23:40 2006 +0200
    12.2 +++ b/src/HOL/NumberTheory/WilsonBij.thy	Wed May 17 01:23:41 2006 +0200
    12.3 @@ -17,15 +17,14 @@
    12.4  
    12.5  subsection {* Definitions and lemmas *}
    12.6  
    12.7 -constdefs
    12.8 +definition
    12.9    reciR :: "int => int => int => bool"
   12.10 -  "reciR p ==
   12.11 -    \<lambda>a b. zcong (a * b) 1 p \<and> 1 < a \<and> a < p - 1 \<and> 1 < b \<and> b < p - 1"
   12.12 +  "reciR p = (\<lambda>a b. zcong (a * b) 1 p \<and> 1 < a \<and> a < p - 1 \<and> 1 < b \<and> b < p - 1)"
   12.13    inv :: "int => int => int"
   12.14 -  "inv p a ==
   12.15 -    if zprime p \<and> 0 < a \<and> a < p then
   12.16 +  "inv p a =
   12.17 +    (if zprime p \<and> 0 < a \<and> a < p then
   12.18        (SOME x. 0 \<le> x \<and> x < p \<and> zcong (a * x) 1 p)
   12.19 -    else 0"
   12.20 +     else 0)"
   12.21  
   12.22  
   12.23  text {* \medskip Inverse *}
    13.1 --- a/src/HOL/NumberTheory/WilsonRuss.thy	Wed May 17 01:23:40 2006 +0200
    13.2 +++ b/src/HOL/NumberTheory/WilsonRuss.thy	Wed May 17 01:23:41 2006 +0200
    13.3 @@ -15,13 +15,13 @@
    13.4  
    13.5  subsection {* Definitions and lemmas *}
    13.6  
    13.7 +definition
    13.8 +  inv :: "int => int => int"
    13.9 +  "inv p a = (a^(nat (p - 2))) mod p"
   13.10 +
   13.11  consts
   13.12 -  inv :: "int => int => int"
   13.13    wset :: "int * int => int set"
   13.14  
   13.15 -defs
   13.16 -  inv_def: "inv p a == (a^(nat (p - 2))) mod p"
   13.17 -
   13.18  recdef wset
   13.19    "measure ((\<lambda>(a, p). nat a) :: int * int => nat)"
   13.20    "wset (a, p) =
   13.21 @@ -81,7 +81,8 @@
   13.22        apply (rule_tac [2] zcong_zless_imp_eq, auto)
   13.23    done
   13.24  
   13.25 -lemma inv_not_p_minus_1_aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
   13.26 +lemma inv_not_p_minus_1_aux:
   13.27 +    "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
   13.28    apply (unfold zcong_def)
   13.29    apply (simp add: OrderedGroup.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
   13.30    apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
   13.31 @@ -163,7 +164,8 @@
   13.32  
   13.33  lemma wset_induct:
   13.34    assumes "!!a p. P {} a p"
   13.35 -    and "!!a p. 1 < (a::int) \<Longrightarrow> P (wset (a - 1, p)) (a - 1) p ==> P (wset (a, p)) a p"
   13.36 +    and "!!a p. 1 < (a::int) \<Longrightarrow>
   13.37 +      P (wset (a - 1, p)) (a - 1) p ==> P (wset (a, p)) a p"
   13.38    shows "P (wset (u, v)) u v"
   13.39    apply (rule wset.induct, safe)
   13.40     prefer 2