tuned sources and proofs
authorwenzelm
Thu Dec 08 12:50:04 2005 +0100 (2005-12-08)
changeset 18369694ea14ab4f2
parent 18368 2f9b2539c5bb
child 18370 db5900e7c6c9
tuned sources and proofs
src/HOL/NumberTheory/BijectionRel.thy
src/HOL/NumberTheory/Euler.thy
src/HOL/NumberTheory/EulerFermat.thy
src/HOL/NumberTheory/EvenOdd.thy
src/HOL/NumberTheory/Finite2.thy
src/HOL/NumberTheory/Gauss.thy
src/HOL/NumberTheory/Int2.thy
src/HOL/NumberTheory/IntFact.thy
src/HOL/NumberTheory/IntPrimes.thy
src/HOL/NumberTheory/Quadratic_Reciprocity.thy
src/HOL/NumberTheory/Residues.thy
src/HOL/NumberTheory/WilsonRuss.thy
     1.1 --- a/src/HOL/NumberTheory/BijectionRel.thy	Thu Dec 08 12:50:03 2005 +0100
     1.2 +++ b/src/HOL/NumberTheory/BijectionRel.thy	Thu Dec 08 12:50:04 2005 +0100
     1.3 @@ -63,19 +63,16 @@
     1.4    done
     1.5  
     1.6  lemma aux_induct:
     1.7 -  "finite F ==> F \<subseteq> A ==> P {} ==>
     1.8 -    (!!F a. F \<subseteq> A ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F))
     1.9 -  ==> P F"
    1.10 -proof -
    1.11 -  case rule_context
    1.12 -  assume major: "finite F"
    1.13 +  assumes major: "finite F"
    1.14      and subs: "F \<subseteq> A"
    1.15 -  show ?thesis
    1.16 -    apply (rule subs [THEN rev_mp])
    1.17 -    apply (rule major [THEN finite_induct])
    1.18 -     apply (blast intro: rule_context)+
    1.19 -    done
    1.20 -qed
    1.21 +    and cases: "P {}"
    1.22 +      "!!F a. F \<subseteq> A ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
    1.23 +  shows "P F"
    1.24 +  using major subs
    1.25 +  apply (induct set: Finites)
    1.26 +   apply (blast intro: cases)+
    1.27 +  done
    1.28 +
    1.29  
    1.30  lemma inj_func_bijR_aux1:
    1.31      "A \<subseteq> B ==> a \<notin> A ==> a \<in> B ==> inj_on f B ==> f a \<notin> f ` A"
     2.1 --- a/src/HOL/NumberTheory/Euler.thy	Thu Dec 08 12:50:03 2005 +0100
     2.2 +++ b/src/HOL/NumberTheory/Euler.thy	Thu Dec 08 12:50:04 2005 +0100
     2.3 @@ -122,7 +122,7 @@
     2.4  
     2.5  lemma card_setsum_aux: "[| finite S; \<forall>X \<in> S. finite (X::int set); 
     2.6      \<forall>X \<in> S. card X = n |] ==> setsum card S = setsum (%x. n) S"
     2.7 -by (induct set: Finites, auto)
     2.8 +  by (induct set: Finites) auto
     2.9  
    2.10  lemma SetS_card: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==> 
    2.11                    int(card(SetS a p)) = (p - 1) div 2"
    2.12 @@ -172,9 +172,9 @@
    2.13  lemma aux2: "[| (a::int) < c; b < c |] ==> (a \<le> b | b \<le> a)"
    2.14    by auto
    2.15  
    2.16 -lemma SRStar_d22set_prop [rule_format]: "2 < p --> (SRStar p) = {1} \<union> 
    2.17 -    (d22set (p - 1))"
    2.18 -  apply (induct p rule: d22set.induct, auto)
    2.19 +lemma SRStar_d22set_prop: "2 < p \<Longrightarrow> (SRStar p) = {1} \<union> (d22set (p - 1))"
    2.20 +  apply (induct p rule: d22set.induct)
    2.21 +  apply auto
    2.22    apply (simp add: SRStar_def d22set.simps)
    2.23    apply (simp add: SRStar_def d22set.simps, clarify)
    2.24    apply (frule aux1)
    2.25 @@ -183,7 +183,7 @@
    2.26    apply (simp add: d22set.simps)
    2.27    apply (frule d22set_le)
    2.28    apply (frule d22set_g_1, auto)
    2.29 -done
    2.30 +  done
    2.31  
    2.32  lemma Union_SetS_setprod_prop1: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
    2.33                                   [\<Prod>(Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)"
    2.34 @@ -195,8 +195,8 @@
    2.35                         MultInvPair_prop1c setprod_Union_disjoint)
    2.36    also have "[setprod (setprod (%x. x)) (SetS a p) = 
    2.37        setprod (%x. a) (SetS a p)] (mod p)"
    2.38 -    apply (rule setprod_same_function_zcong)
    2.39 -    by (auto simp add: prems SetS_setprod_prop SetS_finite)
    2.40 +    by (rule setprod_same_function_zcong)
    2.41 +      (auto simp add: prems SetS_setprod_prop SetS_finite)
    2.42    also (zcong_trans) have "[setprod (%x. a) (SetS a p) = 
    2.43        a^(card (SetS a p))] (mod p)"
    2.44      by (auto simp add: prems SetS_finite setprod_constant)
    2.45 @@ -205,7 +205,7 @@
    2.46      apply (subgoal_tac "card(SetS a p) = nat((p - 1) div 2)", auto)
    2.47      apply (subgoal_tac "nat(int(card(SetS a p))) = nat((p - 1) div 2)", force)
    2.48      apply (auto simp add: prems SetS_card)
    2.49 -  done
    2.50 +    done
    2.51  qed
    2.52  
    2.53  lemma Union_SetS_setprod_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==> 
    2.54 @@ -218,15 +218,15 @@
    2.55      by (auto simp add: prems SRStar_d22set_prop)
    2.56    also have "... = zfact(p - 1)"
    2.57    proof -
    2.58 -     have "~(1 \<in> d22set (p - 1)) & finite( d22set (p - 1))"
    2.59 +    have "~(1 \<in> d22set (p - 1)) & finite( d22set (p - 1))"
    2.60        apply (insert prems, auto)
    2.61        apply (drule d22set_g_1)
    2.62        apply (auto simp add: d22set_fin)
    2.63 -     done
    2.64 -     then have "\<Prod>({1} \<union> (d22set (p - 1))) = \<Prod>(d22set (p - 1))"
    2.65 -       by auto
    2.66 -     then show ?thesis
    2.67 -       by (auto simp add: d22set_prod_zfact)
    2.68 +      done
    2.69 +    then have "\<Prod>({1} \<union> (d22set (p - 1))) = \<Prod>(d22set (p - 1))"
    2.70 +      by auto
    2.71 +    then show ?thesis
    2.72 +      by (auto simp add: d22set_prod_zfact)
    2.73    qed
    2.74    finally show ?thesis .
    2.75  qed
    2.76 @@ -235,7 +235,7 @@
    2.77                     [zfact (p - 1) = a ^ nat ((p - 1) div 2)] (mod p)"
    2.78    apply (frule Union_SetS_setprod_prop1) 
    2.79    apply (auto simp add: Union_SetS_setprod_prop2)
    2.80 -done
    2.81 +  done
    2.82  
    2.83  (****************************************************************)
    2.84  (*                                                              *)
    2.85 @@ -252,7 +252,7 @@
    2.86    apply (frule Wilson_Russ)
    2.87    apply (auto simp add: zcong_sym)
    2.88    apply (rule zcong_trans, auto)
    2.89 -done
    2.90 +  done
    2.91  
    2.92  (********************************************************************)
    2.93  (*                                                                  *)
    2.94 @@ -294,7 +294,7 @@
    2.95    apply (frule aux_2, auto)
    2.96    apply (frule_tac a = a in aux_1, auto)
    2.97    apply (frule zcong_zmult_prop1, auto)
    2.98 -done
    2.99 +  done
   2.100  
   2.101  (****************************************************************)
   2.102  (*                                                              *)
   2.103 @@ -309,7 +309,7 @@
   2.104      ~([y ^ 2 = 0] (mod p))")
   2.105    apply (auto simp add: zcong_sym [of "y^2" x p] intro: zcong_trans)
   2.106    apply (auto simp add: zcong_eq_zdvd_prop intro: zpower_zdvd_prop1)
   2.107 -done
   2.108 +  done
   2.109  
   2.110  lemma aux__2: "2 * nat((p - 1) div 2) =  nat (2 * ((p - 1) div 2))"
   2.111    by (auto simp add: nat_mult_distrib)
   2.112 @@ -327,7 +327,7 @@
   2.113    apply (frule odd_minus_one_even)
   2.114    apply (frule even_div_2_prop2)
   2.115    apply (auto intro: Little_Fermat simp add: zprime_zOdd_eq_grt_2)
   2.116 -done
   2.117 +  done
   2.118  
   2.119  (********************************************************************)
   2.120  (*                                                                  *)
   2.121 @@ -340,6 +340,6 @@
   2.122    apply (auto simp add: Legendre_def Euler_part2)
   2.123    apply (frule Euler_part3, auto simp add: zcong_sym)
   2.124    apply (frule Euler_part1, auto simp add: zcong_sym)
   2.125 -done
   2.126 +  done
   2.127  
   2.128 -end
   2.129 \ No newline at end of file
   2.130 +end
     3.1 --- a/src/HOL/NumberTheory/EulerFermat.thy	Thu Dec 08 12:50:03 2005 +0100
     3.2 +++ b/src/HOL/NumberTheory/EulerFermat.thy	Thu Dec 08 12:50:04 2005 +0100
     3.3 @@ -2,9 +2,6 @@
     3.4      ID:         $Id$
     3.5      Author:     Thomas M. Rasmussen
     3.6      Copyright   2000  University of Cambridge
     3.7 -
     3.8 -Changes by Jeremy Avigad, 2003/02/21:
     3.9 -   repaired proof of Bnor_prime (removed use of zprime_def)
    3.10  *)
    3.11  
    3.12  header {* Fermat's Little Theorem extended to Euler's Totient function *}
    3.13 @@ -60,7 +57,7 @@
    3.14  
    3.15  lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)"
    3.16    -- {* LCP: not sure why this lemma is needed now *}
    3.17 -by (auto simp add: abs_if)
    3.18 +  by (auto simp add: abs_if)
    3.19  
    3.20  
    3.21  text {* \medskip @{text norRRset} *}
    3.22 @@ -68,29 +65,27 @@
    3.23  declare BnorRset.simps [simp del]
    3.24  
    3.25  lemma BnorRset_induct:
    3.26 -  "(!!a m. P {} a m) ==>
    3.27 -    (!!a m. 0 < (a::int) ==> P (BnorRset (a - 1, m::int)) (a - 1) m
    3.28 -      ==> P (BnorRset(a,m)) a m)
    3.29 -    ==> P (BnorRset(u,v)) u v"
    3.30 -proof -
    3.31 -  case rule_context
    3.32 -  show ?thesis
    3.33 -    apply (rule BnorRset.induct, safe)
    3.34 -     apply (case_tac [2] "0 < a")
    3.35 -      apply (rule_tac [2] rule_context, simp_all)
    3.36 -     apply (simp_all add: BnorRset.simps rule_context)
    3.37 +  assumes "!!a m. P {} a m"
    3.38 +    and "!!a m. 0 < (a::int) ==> P (BnorRset (a - 1, m::int)) (a - 1) m
    3.39 +      ==> P (BnorRset(a,m)) a m"
    3.40 +  shows "P (BnorRset(u,v)) u v"
    3.41 +  apply (rule BnorRset.induct)
    3.42 +  apply safe
    3.43 +   apply (case_tac [2] "0 < a")
    3.44 +    apply (rule_tac [2] prems)
    3.45 +     apply simp_all
    3.46 +   apply (simp_all add: BnorRset.simps prems)
    3.47    done
    3.48 -qed
    3.49  
    3.50 -lemma Bnor_mem_zle [rule_format]: "b \<in> BnorRset (a, m) --> b \<le> a"
    3.51 +lemma Bnor_mem_zle [rule_format]: "b \<in> BnorRset (a, m) \<longrightarrow> b \<le> a"
    3.52    apply (induct a m rule: BnorRset_induct)
    3.53 -   prefer 2
    3.54 -   apply (subst BnorRset.simps)
    3.55 +   apply simp
    3.56 +  apply (subst BnorRset.simps)
    3.57     apply (unfold Let_def, auto)
    3.58    done
    3.59  
    3.60  lemma Bnor_mem_zle_swap: "a < b ==> b \<notin> BnorRset (a, m)"
    3.61 -by (auto dest: Bnor_mem_zle)
    3.62 +  by (auto dest: Bnor_mem_zle)
    3.63  
    3.64  lemma Bnor_mem_zg [rule_format]: "b \<in> BnorRset (a, m) --> 0 < b"
    3.65    apply (induct a m rule: BnorRset_induct)
    3.66 @@ -210,7 +205,7 @@
    3.67    RRset2norRR_correct [THEN conjunct2, standard]
    3.68  
    3.69  lemma RsetR_fin: "A \<in> RsetR m ==> finite A"
    3.70 -by (erule RsetR.induct, auto)
    3.71 +  by (induct set: RsetR) auto
    3.72  
    3.73  lemma RRset_zcong_eq [rule_format]:
    3.74    "1 < m ==>
     4.1 --- a/src/HOL/NumberTheory/EvenOdd.thy	Thu Dec 08 12:50:03 2005 +0100
     4.2 +++ b/src/HOL/NumberTheory/EvenOdd.thy	Thu Dec 08 12:50:04 2005 +0100
     4.3 @@ -5,14 +5,14 @@
     4.4  
     4.5  header {*Parity: Even and Odd Integers*}
     4.6  
     4.7 -theory EvenOdd imports Int2 begin;
     4.8 +theory EvenOdd imports Int2 begin
     4.9  
    4.10  text{*Note.  This theory is being revised.  See the web page
    4.11  \url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
    4.12  
    4.13  constdefs
    4.14    zOdd    :: "int set"
    4.15 -  "zOdd == {x. \<exists>k. x = 2*k + 1}"
    4.16 +  "zOdd == {x. \<exists>k. x = 2 * k + 1}"
    4.17    zEven   :: "int set"
    4.18    "zEven == {x. \<exists>k. x = 2 * k}"
    4.19  
    4.20 @@ -22,223 +22,239 @@
    4.21  (*                                                         *)
    4.22  (***********************************************************)
    4.23  
    4.24 -lemma one_not_even: "~(1 \<in> zEven)";
    4.25 -  apply (simp add: zEven_def)
    4.26 -  apply (rule allI, case_tac "k \<le> 0", auto)
    4.27 -done
    4.28 +lemma zOddI [intro?]: "x = 2 * k + 1 \<Longrightarrow> x \<in> zOdd"
    4.29 +  and zOddE [elim?]: "x \<in> zOdd \<Longrightarrow> (!!k. x = 2 * k + 1 \<Longrightarrow> C) \<Longrightarrow> C"
    4.30 +  by (auto simp add: zOdd_def)
    4.31  
    4.32 -lemma even_odd_conj: "~(x \<in> zOdd & x \<in> zEven)";
    4.33 -  apply (auto simp add: zOdd_def zEven_def)
    4.34 -  proof -;
    4.35 -    fix a b;
    4.36 -    assume "2 * (a::int) = 2 * (b::int) + 1"; 
    4.37 -    then have "2 * (a::int) - 2 * (b :: int) = 1";
    4.38 -       by arith
    4.39 -    then have "2 * (a - b) = 1";
    4.40 -       by (auto simp add: zdiff_zmult_distrib)
    4.41 -    moreover have "(2 * (a - b)):zEven";
    4.42 -       by (auto simp only: zEven_def)
    4.43 -    ultimately show "False";
    4.44 -       by (auto simp add: one_not_even)
    4.45 -  qed;
    4.46 +lemma zEvenI [intro?]: "x = 2 * k \<Longrightarrow> x \<in> zEven"
    4.47 +  and zEvenE [elim?]: "x \<in> zEven \<Longrightarrow> (!!k. x = 2 * k \<Longrightarrow> C) \<Longrightarrow> C"
    4.48 +  by (auto simp add: zEven_def)
    4.49 +
    4.50 +lemma one_not_even: "~(1 \<in> zEven)"
    4.51 +proof
    4.52 +  assume "1 \<in> zEven"
    4.53 +  then obtain k :: int where "1 = 2 * k" ..
    4.54 +  then show False by arith
    4.55 +qed
    4.56  
    4.57 -lemma even_odd_disj: "(x \<in> zOdd | x \<in> zEven)";
    4.58 -  by (simp add: zOdd_def zEven_def, presburger)
    4.59 +lemma even_odd_conj: "~(x \<in> zOdd & x \<in> zEven)"
    4.60 +proof -
    4.61 +  {
    4.62 +    fix a b
    4.63 +    assume "2 * (a::int) = 2 * (b::int) + 1"
    4.64 +    then have "2 * (a::int) - 2 * (b :: int) = 1"
    4.65 +      by arith
    4.66 +    then have "2 * (a - b) = 1"
    4.67 +      by (auto simp add: zdiff_zmult_distrib)
    4.68 +    moreover have "(2 * (a - b)):zEven"
    4.69 +      by (auto simp only: zEven_def)
    4.70 +    ultimately have False
    4.71 +      by (auto simp add: one_not_even)
    4.72 +  }
    4.73 +  then show ?thesis
    4.74 +    by (auto simp add: zOdd_def zEven_def)
    4.75 +qed
    4.76  
    4.77 -lemma not_odd_impl_even: "~(x \<in> zOdd) ==> x \<in> zEven";
    4.78 -  by (insert even_odd_disj, auto)
    4.79 +lemma even_odd_disj: "(x \<in> zOdd | x \<in> zEven)"
    4.80 +  by (simp add: zOdd_def zEven_def) arith
    4.81  
    4.82 -lemma odd_mult_odd_prop: "(x*y):zOdd ==> x \<in> zOdd";
    4.83 -  apply (case_tac "x \<in> zOdd", auto)
    4.84 -  apply (drule not_odd_impl_even)
    4.85 -  apply (auto simp add: zEven_def zOdd_def)
    4.86 -  proof -;
    4.87 -    fix a b; 
    4.88 -    assume "2 * a * y = 2 * b + 1";
    4.89 -    then have "2 * a * y - 2 * b = 1";
    4.90 -      by arith
    4.91 -    then have "2 * (a * y - b) = 1";
    4.92 -      by (auto simp add: zdiff_zmult_distrib)
    4.93 -    moreover have "(2 * (a * y - b)):zEven";
    4.94 -       by (auto simp only: zEven_def)
    4.95 -    ultimately show "False";
    4.96 -       by (auto simp add: one_not_even)
    4.97 -  qed;
    4.98 +lemma not_odd_impl_even: "~(x \<in> zOdd) ==> x \<in> zEven"
    4.99 +  using even_odd_disj by auto
   4.100  
   4.101 -lemma odd_minus_one_even: "x \<in> zOdd ==> (x - 1):zEven";
   4.102 +lemma odd_mult_odd_prop: "(x*y):zOdd ==> x \<in> zOdd"
   4.103 +proof (rule classical)
   4.104 +  assume "\<not> ?thesis"
   4.105 +  then have "x \<in> zEven" by (rule not_odd_impl_even)
   4.106 +  then obtain a where a: "x = 2 * a" ..
   4.107 +  assume "x * y : zOdd"
   4.108 +  then obtain b where "x * y = 2 * b + 1" ..
   4.109 +  with a have "2 * a * y = 2 * b + 1" by simp
   4.110 +  then have "2 * a * y - 2 * b = 1"
   4.111 +    by arith
   4.112 +  then have "2 * (a * y - b) = 1"
   4.113 +    by (auto simp add: zdiff_zmult_distrib)
   4.114 +  moreover have "(2 * (a * y - b)):zEven"
   4.115 +    by (auto simp only: zEven_def)
   4.116 +  ultimately have False
   4.117 +    by (auto simp add: one_not_even)
   4.118 +  then show ?thesis ..
   4.119 +qed
   4.120 +
   4.121 +lemma odd_minus_one_even: "x \<in> zOdd ==> (x - 1):zEven"
   4.122    by (auto simp add: zOdd_def zEven_def)
   4.123  
   4.124 -lemma even_div_2_prop1: "x \<in> zEven ==> (x mod 2) = 0";
   4.125 +lemma even_div_2_prop1: "x \<in> zEven ==> (x mod 2) = 0"
   4.126    by (auto simp add: zEven_def)
   4.127  
   4.128 -lemma even_div_2_prop2: "x \<in> zEven ==> (2 * (x div 2)) = x";
   4.129 +lemma even_div_2_prop2: "x \<in> zEven ==> (2 * (x div 2)) = x"
   4.130    by (auto simp add: zEven_def)
   4.131  
   4.132 -lemma even_plus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x + y \<in> zEven";
   4.133 +lemma even_plus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x + y \<in> zEven"
   4.134    apply (auto simp add: zEven_def)
   4.135 -  by (auto simp only: zadd_zmult_distrib2 [THEN sym])
   4.136 +  apply (auto simp only: zadd_zmult_distrib2 [symmetric])
   4.137 +  done
   4.138  
   4.139 -lemma even_times_either: "x \<in> zEven ==> x * y \<in> zEven";
   4.140 +lemma even_times_either: "x \<in> zEven ==> x * y \<in> zEven"
   4.141    by (auto simp add: zEven_def)
   4.142  
   4.143 -lemma even_minus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x - y \<in> zEven";
   4.144 +lemma even_minus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x - y \<in> zEven"
   4.145    apply (auto simp add: zEven_def)
   4.146 -  by (auto simp only: zdiff_zmult_distrib2 [THEN sym])
   4.147 +  apply (auto simp only: zdiff_zmult_distrib2 [symmetric])
   4.148 +  done
   4.149  
   4.150 -lemma odd_minus_odd: "[| x \<in> zOdd; y \<in> zOdd |] ==> x - y \<in> zEven";
   4.151 +lemma odd_minus_odd: "[| x \<in> zOdd; y \<in> zOdd |] ==> x - y \<in> zEven"
   4.152    apply (auto simp add: zOdd_def zEven_def)
   4.153 -  by (auto simp only: zdiff_zmult_distrib2 [THEN sym])
   4.154 +  apply (auto simp only: zdiff_zmult_distrib2 [symmetric])
   4.155 +  done
   4.156  
   4.157 -lemma even_minus_odd: "[| x \<in> zEven; y \<in> zOdd |] ==> x - y \<in> zOdd";
   4.158 +lemma even_minus_odd: "[| x \<in> zEven; y \<in> zOdd |] ==> x - y \<in> zOdd"
   4.159    apply (auto simp add: zOdd_def zEven_def)
   4.160    apply (rule_tac x = "k - ka - 1" in exI)
   4.161 -  by auto
   4.162 +  apply auto
   4.163 +  done
   4.164  
   4.165 -lemma odd_minus_even: "[| x \<in> zOdd; y \<in> zEven |] ==> x - y \<in> zOdd";
   4.166 +lemma odd_minus_even: "[| x \<in> zOdd; y \<in> zEven |] ==> x - y \<in> zOdd"
   4.167    apply (auto simp add: zOdd_def zEven_def)
   4.168 -  by (auto simp only: zdiff_zmult_distrib2 [THEN sym])
   4.169 +  apply (auto simp only: zdiff_zmult_distrib2 [symmetric])
   4.170 +  done
   4.171  
   4.172 -lemma odd_times_odd: "[| x \<in> zOdd;  y \<in> zOdd |] ==> x * y \<in> zOdd";
   4.173 +lemma odd_times_odd: "[| x \<in> zOdd;  y \<in> zOdd |] ==> x * y \<in> zOdd"
   4.174    apply (auto simp add: zOdd_def zadd_zmult_distrib zadd_zmult_distrib2)
   4.175    apply (rule_tac x = "2 * ka * k + ka + k" in exI)
   4.176 -  by (auto simp add: zadd_zmult_distrib)
   4.177 -
   4.178 -lemma odd_iff_not_even: "(x \<in> zOdd) = (~ (x \<in> zEven))";
   4.179 -  by (insert even_odd_conj even_odd_disj, auto)
   4.180 -
   4.181 -lemma even_product: "x * y \<in> zEven ==> x \<in> zEven | y \<in> zEven"; 
   4.182 -  by (insert odd_iff_not_even odd_times_odd, auto)
   4.183 +  apply (auto simp add: zadd_zmult_distrib)
   4.184 +  done
   4.185  
   4.186 -lemma even_diff: "x - y \<in> zEven = ((x \<in> zEven) = (y \<in> zEven))";
   4.187 -  apply (auto simp add: odd_iff_not_even even_minus_even odd_minus_odd
   4.188 -     even_minus_odd odd_minus_even)
   4.189 -  proof -;
   4.190 -    assume "x - y \<in> zEven" and "x \<in> zEven";
   4.191 -    show "y \<in> zEven";
   4.192 -    proof (rule classical);
   4.193 -      assume "~(y \<in> zEven)"; 
   4.194 -      then have "y \<in> zOdd" 
   4.195 -        by (auto simp add: odd_iff_not_even)
   4.196 -      with prems have "x - y \<in> zOdd";
   4.197 -        by (simp add: even_minus_odd)
   4.198 -      with prems have "False"; 
   4.199 -        by (auto simp add: odd_iff_not_even)
   4.200 -      thus ?thesis;
   4.201 -        by auto
   4.202 -    qed;
   4.203 -    next assume "x - y \<in> zEven" and "y \<in> zEven"; 
   4.204 -    show "x \<in> zEven";
   4.205 -    proof (rule classical);
   4.206 -      assume "~(x \<in> zEven)"; 
   4.207 -      then have "x \<in> zOdd" 
   4.208 -        by (auto simp add: odd_iff_not_even)
   4.209 -      with prems have "x - y \<in> zOdd";
   4.210 -        by (simp add: odd_minus_even)
   4.211 -      with prems have "False"; 
   4.212 -        by (auto simp add: odd_iff_not_even)
   4.213 -      thus ?thesis;
   4.214 -        by auto
   4.215 -    qed;
   4.216 -  qed;
   4.217 +lemma odd_iff_not_even: "(x \<in> zOdd) = (~ (x \<in> zEven))"
   4.218 +  using even_odd_conj even_odd_disj by auto
   4.219 +
   4.220 +lemma even_product: "x * y \<in> zEven ==> x \<in> zEven | y \<in> zEven"
   4.221 +  using odd_iff_not_even odd_times_odd by auto
   4.222  
   4.223 -lemma neg_one_even_power: "[| x \<in> zEven; 0 \<le> x |] ==> (-1::int)^(nat x) = 1";
   4.224 -proof -;
   4.225 -  assume "x \<in> zEven" and "0 \<le> x";
   4.226 -  then have "\<exists>k. x = 2 * k";
   4.227 -    by (auto simp only: zEven_def)
   4.228 -  then show ?thesis;
   4.229 -    proof;
   4.230 -      fix a;
   4.231 -      assume "x = 2 * a";
   4.232 -      from prems have a: "0 \<le> a";
   4.233 -        by arith
   4.234 -      from prems have "nat x = nat(2 * a)";
   4.235 -        by auto
   4.236 -      also from a have "nat (2 * a) = 2 * nat a";
   4.237 -        by (auto simp add: nat_mult_distrib)
   4.238 -      finally have "(-1::int)^nat x = (-1)^(2 * nat a)";
   4.239 -        by auto
   4.240 -      also have "... = ((-1::int)^2)^ (nat a)";
   4.241 -        by (auto simp add: zpower_zpower [THEN sym])
   4.242 -      also have "(-1::int)^2 = 1";
   4.243 -        by auto
   4.244 -      finally; show ?thesis;
   4.245 -        by auto
   4.246 -    qed;
   4.247 -qed;
   4.248 +lemma even_diff: "x - y \<in> zEven = ((x \<in> zEven) = (y \<in> zEven))"
   4.249 +proof
   4.250 +  assume xy: "x - y \<in> zEven"
   4.251 +  {
   4.252 +    assume x: "x \<in> zEven"
   4.253 +    have "y \<in> zEven"
   4.254 +    proof (rule classical)
   4.255 +      assume "\<not> ?thesis"
   4.256 +      then have "y \<in> zOdd"
   4.257 +        by (simp add: odd_iff_not_even)
   4.258 +      with x have "x - y \<in> zOdd"
   4.259 +        by (simp add: even_minus_odd)
   4.260 +      with xy have False
   4.261 +        by (auto simp add: odd_iff_not_even)
   4.262 +      then show ?thesis ..
   4.263 +    qed
   4.264 +  } moreover {
   4.265 +    assume y: "y \<in> zEven"
   4.266 +    have "x \<in> zEven"
   4.267 +    proof (rule classical)
   4.268 +      assume "\<not> ?thesis"
   4.269 +      then have "x \<in> zOdd"
   4.270 +        by (auto simp add: odd_iff_not_even)
   4.271 +      with y have "x - y \<in> zOdd"
   4.272 +        by (simp add: odd_minus_even)
   4.273 +      with xy have False
   4.274 +        by (auto simp add: odd_iff_not_even)
   4.275 +      then show ?thesis ..
   4.276 +    qed
   4.277 +  }
   4.278 +  ultimately show "(x \<in> zEven) = (y \<in> zEven)"
   4.279 +    by (auto simp add: odd_iff_not_even even_minus_even odd_minus_odd
   4.280 +      even_minus_odd odd_minus_even)
   4.281 +next
   4.282 +  assume "(x \<in> zEven) = (y \<in> zEven)"
   4.283 +  then show "x - y \<in> zEven"
   4.284 +    by (auto simp add: odd_iff_not_even even_minus_even odd_minus_odd
   4.285 +      even_minus_odd odd_minus_even)
   4.286 +qed
   4.287  
   4.288 -lemma neg_one_odd_power: "[| x \<in> zOdd; 0 \<le> x |] ==> (-1::int)^(nat x) = -1";
   4.289 -proof -;
   4.290 -  assume "x \<in> zOdd" and "0 \<le> x";
   4.291 -  then have "\<exists>k. x = 2 * k + 1";
   4.292 -    by (auto simp only: zOdd_def)
   4.293 -  then show ?thesis;
   4.294 -    proof;
   4.295 -      fix a;
   4.296 -      assume "x = 2 * a + 1";
   4.297 -      from prems have a: "0 \<le> a";
   4.298 -        by arith
   4.299 -      from prems have "nat x = nat(2 * a + 1)";
   4.300 -        by auto
   4.301 -      also from a have "nat (2 * a + 1) = 2 * nat a + 1";
   4.302 -        by (auto simp add: nat_mult_distrib nat_add_distrib)
   4.303 -      finally have "(-1::int)^nat x = (-1)^(2 * nat a + 1)";
   4.304 -        by auto
   4.305 -      also have "... = ((-1::int)^2)^ (nat a) * (-1)^1";
   4.306 -        by (auto simp add: zpower_zpower [THEN sym] zpower_zadd_distrib)
   4.307 -      also have "(-1::int)^2 = 1";
   4.308 -        by auto
   4.309 -      finally; show ?thesis;
   4.310 -        by auto
   4.311 -    qed;
   4.312 -qed;
   4.313 +lemma neg_one_even_power: "[| x \<in> zEven; 0 \<le> x |] ==> (-1::int)^(nat x) = 1"
   4.314 +proof -
   4.315 +  assume 1: "x \<in> zEven" and 2: "0 \<le> x"
   4.316 +  from 1 obtain a where 3: "x = 2 * a" ..
   4.317 +  with 2 have "0 \<le> a" by simp
   4.318 +  from 2 3 have "nat x = nat (2 * a)"
   4.319 +    by simp
   4.320 +  also from 3 have "nat (2 * a) = 2 * nat a"
   4.321 +    by (simp add: nat_mult_distrib)
   4.322 +  finally have "(-1::int)^nat x = (-1)^(2 * nat a)"
   4.323 +    by simp
   4.324 +  also have "... = ((-1::int)^2)^ (nat a)"
   4.325 +    by (simp add: zpower_zpower [symmetric])
   4.326 +  also have "(-1::int)^2 = 1"
   4.327 +    by simp
   4.328 +  finally show ?thesis
   4.329 +    by simp
   4.330 +qed
   4.331  
   4.332 -lemma neg_one_power_parity: "[| 0 \<le> x; 0 \<le> y; (x \<in> zEven) = (y \<in> zEven) |] ==> 
   4.333 -  (-1::int)^(nat x) = (-1::int)^(nat y)";
   4.334 -  apply (insert even_odd_disj [of x])
   4.335 -  apply (insert even_odd_disj [of y])
   4.336 +lemma neg_one_odd_power: "[| x \<in> zOdd; 0 \<le> x |] ==> (-1::int)^(nat x) = -1"
   4.337 +proof -
   4.338 +  assume 1: "x \<in> zOdd" and 2: "0 \<le> x"
   4.339 +  from 1 obtain a where 3: "x = 2 * a + 1" ..
   4.340 +  with 2 have a: "0 \<le> a" by simp
   4.341 +  with 2 3 have "nat x = nat (2 * a + 1)"
   4.342 +    by simp
   4.343 +  also from a have "nat (2 * a + 1) = 2 * nat a + 1"
   4.344 +    by (auto simp add: nat_mult_distrib nat_add_distrib)
   4.345 +  finally have "(-1::int)^nat x = (-1)^(2 * nat a + 1)"
   4.346 +    by simp
   4.347 +  also have "... = ((-1::int)^2)^ (nat a) * (-1)^1"
   4.348 +    by (auto simp add: zpower_zpower [symmetric] zpower_zadd_distrib)
   4.349 +  also have "(-1::int)^2 = 1"
   4.350 +    by simp
   4.351 +  finally show ?thesis
   4.352 +    by simp
   4.353 +qed
   4.354 +
   4.355 +lemma neg_one_power_parity: "[| 0 \<le> x; 0 \<le> y; (x \<in> zEven) = (y \<in> zEven) |] ==>
   4.356 +  (-1::int)^(nat x) = (-1::int)^(nat y)"
   4.357 +  using even_odd_disj [of x] even_odd_disj [of y]
   4.358    by (auto simp add: neg_one_even_power neg_one_odd_power)
   4.359  
   4.360 -lemma one_not_neg_one_mod_m: "2 < m ==> ~([1 = -1] (mod m))";
   4.361 +
   4.362 +lemma one_not_neg_one_mod_m: "2 < m ==> ~([1 = -1] (mod m))"
   4.363    by (auto simp add: zcong_def zdvd_not_zless)
   4.364  
   4.365 -lemma even_div_2_l: "[| y \<in> zEven; x < y |] ==> x div 2 < y div 2";
   4.366 -  apply (auto simp only: zEven_def)
   4.367 -  proof -;
   4.368 -    fix k assume "x < 2 * k";
   4.369 -    then have "x div 2 < k" by (auto simp add: div_prop1)
   4.370 -    also have "k = (2 * k) div 2"; by auto
   4.371 -    finally show "x div 2 < 2 * k div 2" by auto
   4.372 -  qed;
   4.373 +lemma even_div_2_l: "[| y \<in> zEven; x < y |] ==> x div 2 < y div 2"
   4.374 +proof -
   4.375 +  assume 1: "y \<in> zEven" and 2: "x < y"
   4.376 +  from 1 obtain k where k: "y = 2 * k" ..
   4.377 +  with 2 have "x < 2 * k" by simp
   4.378 +  then have "x div 2 < k" by (auto simp add: div_prop1)
   4.379 +  also have "k = (2 * k) div 2" by simp
   4.380 +  finally have "x div 2 < 2 * k div 2" by simp
   4.381 +  with k show ?thesis by simp
   4.382 +qed
   4.383  
   4.384 -lemma even_sum_div_2: "[| x \<in> zEven; y \<in> zEven |] ==> (x + y) div 2 = x div 2 + y div 2";
   4.385 +lemma even_sum_div_2: "[| x \<in> zEven; y \<in> zEven |] ==> (x + y) div 2 = x div 2 + y div 2"
   4.386    by (auto simp add: zEven_def, auto simp add: zdiv_zadd1_eq)
   4.387  
   4.388 -lemma even_prod_div_2: "[| x \<in> zEven |] ==> (x * y) div 2 = (x div 2) * y";
   4.389 +lemma even_prod_div_2: "[| x \<in> zEven |] ==> (x * y) div 2 = (x div 2) * y"
   4.390    by (auto simp add: zEven_def)
   4.391  
   4.392  (* An odd prime is greater than 2 *)
   4.393  
   4.394 -lemma zprime_zOdd_eq_grt_2: "zprime p ==> (p \<in> zOdd) = (2 < p)";
   4.395 +lemma zprime_zOdd_eq_grt_2: "zprime p ==> (p \<in> zOdd) = (2 < p)"
   4.396    apply (auto simp add: zOdd_def zprime_def)
   4.397    apply (drule_tac x = 2 in allE)
   4.398 -  apply (insert odd_iff_not_even [of p])  
   4.399 -by (auto simp add: zOdd_def zEven_def)
   4.400 +  using odd_iff_not_even [of p]
   4.401 +  apply (auto simp add: zOdd_def zEven_def)
   4.402 +  done
   4.403  
   4.404  (* Powers of -1 and parity *)
   4.405  
   4.406 -lemma neg_one_special: "finite A ==> 
   4.407 -    ((-1 :: int) ^ card A) * (-1 ^ card A) = 1";
   4.408 -  by (induct set: Finites, auto)
   4.409 +lemma neg_one_special: "finite A ==>
   4.410 +    ((-1 :: int) ^ card A) * (-1 ^ card A) = 1"
   4.411 +  by (induct set: Finites) auto
   4.412  
   4.413 -lemma neg_one_power: "(-1::int)^n = 1 | (-1::int)^n = -1";
   4.414 -  apply (induct_tac n)
   4.415 -  by auto
   4.416 +lemma neg_one_power: "(-1::int)^n = 1 | (-1::int)^n = -1"
   4.417 +  by (induct n) auto
   4.418  
   4.419  lemma neg_one_power_eq_mod_m: "[| 2 < m; [(-1::int)^j = (-1::int)^k] (mod m) |]
   4.420 -  ==> ((-1::int)^j = (-1::int)^k)";
   4.421 -  apply (insert neg_one_power [of j])
   4.422 -  apply (insert neg_one_power [of k])
   4.423 +    ==> ((-1::int)^j = (-1::int)^k)"
   4.424 +  using neg_one_power [of j] and insert neg_one_power [of k]
   4.425    by (auto simp add: one_not_neg_one_mod_m zcong_sym)
   4.426  
   4.427 -end;
   4.428 +end
     5.1 --- a/src/HOL/NumberTheory/Finite2.thy	Thu Dec 08 12:50:03 2005 +0100
     5.2 +++ b/src/HOL/NumberTheory/Finite2.thy	Thu Dec 08 12:50:04 2005 +0100
     5.3 @@ -23,7 +23,7 @@
     5.4  
     5.5  subsection {* Useful properties of sums and products *}
     5.6  
     5.7 -lemma setsum_same_function_zcong: 
     5.8 +lemma setsum_same_function_zcong:
     5.9  assumes a: "\<forall>x \<in> S. [f x = g x](mod m)"
    5.10  shows "[setsum f S = setsum g S] (mod m)"
    5.11  proof cases
    5.12 @@ -48,16 +48,16 @@
    5.13    apply (auto simp add: left_distrib right_distrib int_eq_of_nat)
    5.14    done
    5.15  
    5.16 -lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) = 
    5.17 +lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) =
    5.18      int(c) * int(card X)"
    5.19    apply (induct set: Finites)
    5.20    apply (auto simp add: zadd_zmult_distrib2)
    5.21 -done
    5.22 +  done
    5.23  
    5.24 -lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A = 
    5.25 +lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A =
    5.26      c * setsum f A"
    5.27 -  apply (induct set: Finites, auto)
    5.28 -  by (auto simp only: zadd_zmult_distrib2)
    5.29 +  by (induct set: Finites) (auto simp add: zadd_zmult_distrib2)
    5.30 +
    5.31  
    5.32  (******************************************************************)
    5.33  (*                                                                *)
    5.34 @@ -68,61 +68,71 @@
    5.35  subsection {* Cardinality of explicit finite sets *}
    5.36  
    5.37  lemma finite_surjI: "[| B \<subseteq> f ` A; finite A |] ==> finite B"
    5.38 -by (simp add: finite_subset finite_imageI)
    5.39 +  by (simp add: finite_subset finite_imageI)
    5.40  
    5.41 -lemma bdd_nat_set_l_finite: "finite { y::nat . y < x}"
    5.42 -apply (rule_tac N = "{y. y < x}" and n = x in bounded_nat_set_is_finite)
    5.43 -by auto
    5.44 +lemma bdd_nat_set_l_finite: "finite {y::nat . y < x}"
    5.45 +  by (rule bounded_nat_set_is_finite) blast
    5.46  
    5.47 -lemma bdd_nat_set_le_finite: "finite { y::nat . y \<le> x  }"
    5.48 -apply (subgoal_tac "{ y::nat . y \<le> x  } = { y::nat . y < Suc x}")
    5.49 -by (auto simp add: bdd_nat_set_l_finite)
    5.50 +lemma bdd_nat_set_le_finite: "finite {y::nat . y \<le> x}"
    5.51 +proof -
    5.52 +  have "{y::nat . y \<le> x} = {y::nat . y < Suc x}" by auto
    5.53 +  then show ?thesis by (auto simp add: bdd_nat_set_l_finite)
    5.54 +qed
    5.55  
    5.56 -lemma  bdd_int_set_l_finite: "finite { x::int . 0 \<le> x & x < n}"
    5.57 -apply (subgoal_tac " {(x :: int). 0 \<le> x & x < n} \<subseteq> 
    5.58 +lemma  bdd_int_set_l_finite: "finite {x::int. 0 \<le> x & x < n}"
    5.59 +apply (subgoal_tac " {(x :: int). 0 \<le> x & x < n} \<subseteq>
    5.60      int ` {(x :: nat). x < nat n}")
    5.61  apply (erule finite_surjI)
    5.62  apply (auto simp add: bdd_nat_set_l_finite image_def)
    5.63 -apply (rule_tac x = "nat x" in exI, simp) 
    5.64 +apply (rule_tac x = "nat x" in exI, simp)
    5.65  done
    5.66  
    5.67  lemma bdd_int_set_le_finite: "finite {x::int. 0 \<le> x & x \<le> n}"
    5.68  apply (subgoal_tac "{x. 0 \<le> x & x \<le> n} = {x. 0 \<le> x & x < n + 1}")
    5.69  apply (erule ssubst)
    5.70  apply (rule bdd_int_set_l_finite)
    5.71 -by auto
    5.72 +apply auto
    5.73 +done
    5.74  
    5.75  lemma bdd_int_set_l_l_finite: "finite {x::int. 0 < x & x < n}"
    5.76 -apply (subgoal_tac "{x::int. 0 < x & x < n} \<subseteq> {x::int. 0 \<le> x & x < n}")
    5.77 -by (auto simp add: bdd_int_set_l_finite finite_subset)
    5.78 +proof -
    5.79 +  have "{x::int. 0 < x & x < n} \<subseteq> {x::int. 0 \<le> x & x < n}"
    5.80 +    by auto
    5.81 +  then show ?thesis by (auto simp add: bdd_int_set_l_finite finite_subset)
    5.82 +qed
    5.83  
    5.84  lemma bdd_int_set_l_le_finite: "finite {x::int. 0 < x & x \<le> n}"
    5.85 -apply (subgoal_tac "{x::int. 0 < x & x \<le> n} \<subseteq> {x::int. 0 \<le> x & x \<le> n}")
    5.86 -by (auto simp add: bdd_int_set_le_finite finite_subset)
    5.87 +proof -
    5.88 +  have "{x::int. 0 < x & x \<le> n} \<subseteq> {x::int. 0 \<le> x & x \<le> n}"
    5.89 +    by auto
    5.90 +  then show ?thesis by (auto simp add: bdd_int_set_le_finite finite_subset)
    5.91 +qed
    5.92  
    5.93  lemma card_bdd_nat_set_l: "card {y::nat . y < x} = x"
    5.94 -apply (induct_tac x, force)
    5.95 -proof -
    5.96 +proof (induct x)
    5.97 +  show "card {y::nat . y < 0} = 0" by simp
    5.98 +next
    5.99    fix n::nat
   5.100 -  assume "card {y. y < n} = n" 
   5.101 +  assume "card {y. y < n} = n"
   5.102    have "{y. y < Suc n} = insert n {y. y < n}"
   5.103      by auto
   5.104    then have "card {y. y < Suc n} = card (insert n {y. y < n})"
   5.105      by auto
   5.106    also have "... = Suc (card {y. y < n})"
   5.107 -    apply (rule card_insert_disjoint)
   5.108 -    by (auto simp add: bdd_nat_set_l_finite)
   5.109 -  finally show "card {y. y < Suc n} = Suc n" 
   5.110 +    by (rule card_insert_disjoint) (auto simp add: bdd_nat_set_l_finite)
   5.111 +  finally show "card {y. y < Suc n} = Suc n"
   5.112      by (simp add: prems)
   5.113  qed
   5.114  
   5.115  lemma card_bdd_nat_set_le: "card { y::nat. y \<le> x} = Suc x"
   5.116 -apply (subgoal_tac "{ y::nat. y \<le> x} = { y::nat. y < Suc x}")
   5.117 -by (auto simp add: card_bdd_nat_set_l)
   5.118 +proof -
   5.119 +  have "{y::nat. y \<le> x} = { y::nat. y < Suc x}"
   5.120 +    by auto
   5.121 +  then show ?thesis by (auto simp add: card_bdd_nat_set_l)
   5.122 +qed
   5.123  
   5.124  lemma card_bdd_int_set_l: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y < n} = nat n"
   5.125  proof -
   5.126 -  fix n::int
   5.127    assume "0 \<le> n"
   5.128    have "inj_on (%y. int y) {y. y < nat n}"
   5.129      by (auto simp add: inj_on_def)
   5.130 @@ -131,52 +141,63 @@
   5.131    also from prems have "int ` {y. y < nat n} = {y. 0 \<le> y & y < n}"
   5.132      apply (auto simp add: zless_nat_eq_int_zless image_def)
   5.133      apply (rule_tac x = "nat x" in exI)
   5.134 -    by (auto simp add: nat_0_le)
   5.135 -  also have "card {y. y < nat n} = nat n" 
   5.136 +    apply (auto simp add: nat_0_le)
   5.137 +    done
   5.138 +  also have "card {y. y < nat n} = nat n"
   5.139      by (rule card_bdd_nat_set_l)
   5.140    finally show "card {y. 0 \<le> y & y < n} = nat n" .
   5.141  qed
   5.142  
   5.143 -lemma card_bdd_int_set_le: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y \<le> n} = 
   5.144 +lemma card_bdd_int_set_le: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y \<le> n} =
   5.145    nat n + 1"
   5.146 -apply (subgoal_tac "{y. 0 \<le> y & y \<le> n} = {y. 0 \<le> y & y < n+1}")
   5.147 -apply (insert card_bdd_int_set_l [of "n+1"])
   5.148 -by (auto simp add: nat_add_distrib)
   5.149 +proof -
   5.150 +  assume "0 \<le> n"
   5.151 +  moreover have "{y. 0 \<le> y & y \<le> n} = {y. 0 \<le> y & y < n+1}" by auto
   5.152 +  ultimately show ?thesis
   5.153 +    using card_bdd_int_set_l [of "n + 1"]
   5.154 +    by (auto simp add: nat_add_distrib)
   5.155 +qed
   5.156  
   5.157 -lemma card_bdd_int_set_l_le: "0 \<le> (n::int) ==> 
   5.158 +lemma card_bdd_int_set_l_le: "0 \<le> (n::int) ==>
   5.159      card {x. 0 < x & x \<le> n} = nat n"
   5.160  proof -
   5.161 -  fix n::int
   5.162    assume "0 \<le> n"
   5.163    have "inj_on (%x. x+1) {x. 0 \<le> x & x < n}"
   5.164      by (auto simp add: inj_on_def)
   5.165 -  hence "card ((%x. x+1) ` {x. 0 \<le> x & x < n}) = 
   5.166 +  hence "card ((%x. x+1) ` {x. 0 \<le> x & x < n}) =
   5.167       card {x. 0 \<le> x & x < n}"
   5.168      by (rule card_image)
   5.169 -  also from prems have "... = nat n"
   5.170 +  also from `0 \<le> n` have "... = nat n"
   5.171      by (rule card_bdd_int_set_l)
   5.172    also have "(%x. x + 1) ` {x. 0 \<le> x & x < n} = {x. 0 < x & x<= n}"
   5.173      apply (auto simp add: image_def)
   5.174      apply (rule_tac x = "x - 1" in exI)
   5.175 -    by arith
   5.176 -  finally show "card {x. 0 < x & x \<le> n} = nat n".
   5.177 +    apply arith
   5.178 +    done
   5.179 +  finally show "card {x. 0 < x & x \<le> n} = nat n" .
   5.180  qed
   5.181  
   5.182 -lemma card_bdd_int_set_l_l: "0 < (n::int) ==> 
   5.183 -    card {x. 0 < x & x < n} = nat n - 1"
   5.184 -  apply (subgoal_tac "{x. 0 < x & x < n} = {x. 0 < x & x \<le> n - 1}")
   5.185 -  apply (insert card_bdd_int_set_l_le [of "n - 1"])
   5.186 -  by (auto simp add: nat_diff_distrib)
   5.187 +lemma card_bdd_int_set_l_l: "0 < (n::int) ==>
   5.188 +  card {x. 0 < x & x < n} = nat n - 1"
   5.189 +proof -
   5.190 +  assume "0 < n"
   5.191 +  moreover have "{x. 0 < x & x < n} = {x. 0 < x & x \<le> n - 1}"
   5.192 +    by simp
   5.193 +  ultimately show ?thesis
   5.194 +    using insert card_bdd_int_set_l_le [of "n - 1"]
   5.195 +    by (auto simp add: nat_diff_distrib)
   5.196 +qed
   5.197  
   5.198 -lemma int_card_bdd_int_set_l_l: "0 < n ==> 
   5.199 +lemma int_card_bdd_int_set_l_l: "0 < n ==>
   5.200      int(card {x. 0 < x & x < n}) = n - 1"
   5.201    apply (auto simp add: card_bdd_int_set_l_l)
   5.202    apply (subgoal_tac "Suc 0 \<le> nat n")
   5.203 -  apply (auto simp add: zdiff_int [THEN sym])
   5.204 +  apply (auto simp add: zdiff_int [symmetric])
   5.205    apply (subgoal_tac "0 < nat n", arith)
   5.206 -  by (simp add: zero_less_nat_eq)
   5.207 +  apply (simp add: zero_less_nat_eq)
   5.208 +  done
   5.209  
   5.210 -lemma int_card_bdd_int_set_l_le: "0 \<le> n ==> 
   5.211 +lemma int_card_bdd_int_set_l_le: "0 \<le> n ==>
   5.212      int(card {x. 0 < x & x \<le> n}) = n"
   5.213    by (auto simp add: card_bdd_int_set_l_le)
   5.214  
   5.215 @@ -201,7 +222,7 @@
   5.216  
   5.217  subsection {* Lemmas for counting arguments *}
   5.218  
   5.219 -lemma setsum_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A; 
   5.220 +lemma setsum_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A;
   5.221      g ` B \<subseteq> A; inj_on g B |] ==> setsum g B = setsum (g \<circ> f) A"
   5.222  apply (frule_tac h = g and f = f in setsum_reindex)
   5.223  apply (subgoal_tac "setsum g B = setsum g (f ` A)")
   5.224 @@ -211,17 +232,19 @@
   5.225  apply (auto simp add: card_image)
   5.226  apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
   5.227  apply (frule_tac A = B and B = A and f = g in card_inj_on_le)
   5.228 -by auto
   5.229 +apply auto
   5.230 +done
   5.231  
   5.232 -lemma setprod_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A; 
   5.233 +lemma setprod_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A;
   5.234      g ` B \<subseteq> A; inj_on g B |] ==> setprod g B = setprod (g \<circ> f) A"
   5.235    apply (frule_tac h = g and f = f in setprod_reindex)
   5.236 -  apply (subgoal_tac "setprod g B = setprod g (f ` A)") 
   5.237 +  apply (subgoal_tac "setprod g B = setprod g (f ` A)")
   5.238    apply (simp add: inj_on_def)
   5.239    apply (subgoal_tac "card A = card B")
   5.240    apply (drule_tac A = "f ` A" and B = B in card_seteq)
   5.241    apply (auto simp add: card_image)
   5.242    apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
   5.243 -by (frule_tac A = B and B = A and f = g in card_inj_on_le, auto)
   5.244 +  apply (frule_tac A = B and B = A and f = g in card_inj_on_le, auto)
   5.245 +  done
   5.246  
   5.247 -end
   5.248 \ No newline at end of file
   5.249 +end
     6.1 --- a/src/HOL/NumberTheory/Gauss.thy	Thu Dec 08 12:50:03 2005 +0100
     6.2 +++ b/src/HOL/NumberTheory/Gauss.thy	Thu Dec 08 12:50:04 2005 +0100
     6.3 @@ -5,7 +5,7 @@
     6.4  
     6.5  header {* Gauss' Lemma *}
     6.6  
     6.7 -theory Gauss imports Euler begin;
     6.8 +theory Gauss imports Euler begin
     6.9  
    6.10  locale GAUSS =
    6.11    fixes p :: "int"
    6.12 @@ -27,410 +27,417 @@
    6.13    defines C_def: "C == (StandardRes p) ` B"
    6.14    defines D_def: "D == C \<inter> {x. x \<le> ((p - 1) div 2)}"
    6.15    defines E_def: "E == C \<inter> {x. ((p - 1) div 2) < x}"
    6.16 -  defines F_def: "F == (%x. (p - x)) ` E";
    6.17 +  defines F_def: "F == (%x. (p - x)) ` E"
    6.18  
    6.19  subsection {* Basic properties of p *}
    6.20  
    6.21 -lemma (in GAUSS) p_odd: "p \<in> zOdd";
    6.22 +lemma (in GAUSS) p_odd: "p \<in> zOdd"
    6.23    by (auto simp add: p_prime p_g_2 zprime_zOdd_eq_grt_2)
    6.24  
    6.25 -lemma (in GAUSS) p_g_0: "0 < p";
    6.26 -  by (insert p_g_2, auto)
    6.27 +lemma (in GAUSS) p_g_0: "0 < p"
    6.28 +  using p_g_2 by auto
    6.29  
    6.30 -lemma (in GAUSS) int_nat: "int (nat ((p - 1) div 2)) = (p - 1) div 2";
    6.31 -  by (insert p_g_2, auto simp add: pos_imp_zdiv_nonneg_iff)
    6.32 +lemma (in GAUSS) int_nat: "int (nat ((p - 1) div 2)) = (p - 1) div 2"
    6.33 +  using insert p_g_2 by (auto simp add: pos_imp_zdiv_nonneg_iff)
    6.34  
    6.35 -lemma (in GAUSS) p_minus_one_l: "(p - 1) div 2 < p";
    6.36 -  proof -;
    6.37 -    have "p - 1 = (p - 1) div 1" by auto
    6.38 -    then have "(p - 1) div 2 \<le> p - 1"
    6.39 -      apply (rule ssubst) back;
    6.40 -      apply (rule zdiv_mono2)
    6.41 -      by (auto simp add: p_g_0)
    6.42 -    then have "(p - 1) div 2 \<le> p - 1";
    6.43 -      by auto
    6.44 -    then show ?thesis by simp
    6.45 -qed;
    6.46 +lemma (in GAUSS) p_minus_one_l: "(p - 1) div 2 < p"
    6.47 +proof -
    6.48 +  have "(p - 1) div 2 \<le> (p - 1) div 1"
    6.49 +    by (rule zdiv_mono2) (auto simp add: p_g_0)
    6.50 +  also have "\<dots> = p - 1" by simp
    6.51 +  finally show ?thesis by simp
    6.52 +qed
    6.53  
    6.54 -lemma (in GAUSS) p_eq: "p = (2 * (p - 1) div 2) + 1";
    6.55 -  apply (insert zdiv_zmult_self2 [of 2 "p - 1"])
    6.56 -by auto
    6.57 +lemma (in GAUSS) p_eq: "p = (2 * (p - 1) div 2) + 1"
    6.58 +  using zdiv_zmult_self2 [of 2 "p - 1"] by auto
    6.59  
    6.60 -lemma zodd_imp_zdiv_eq: "x \<in> zOdd ==> 2 * (x - 1) div 2 = 2 * ((x - 1) div 2)";
    6.61 +lemma zodd_imp_zdiv_eq: "x \<in> zOdd ==> 2 * (x - 1) div 2 = 2 * ((x - 1) div 2)"
    6.62    apply (frule odd_minus_one_even)
    6.63    apply (simp add: zEven_def)
    6.64    apply (subgoal_tac "2 \<noteq> 0")
    6.65 -  apply (frule_tac b = "2 :: int" and a = "x - 1" in zdiv_zmult_self2)  
    6.66 -by (auto simp add: even_div_2_prop2)
    6.67 +  apply (frule_tac b = "2 :: int" and a = "x - 1" in zdiv_zmult_self2)
    6.68 +  apply (auto simp add: even_div_2_prop2)
    6.69 +  done
    6.70  
    6.71 -lemma (in GAUSS) p_eq2: "p = (2 * ((p - 1) div 2)) + 1";
    6.72 +lemma (in GAUSS) p_eq2: "p = (2 * ((p - 1) div 2)) + 1"
    6.73    apply (insert p_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 [of p], auto)
    6.74 -by (frule zodd_imp_zdiv_eq, auto)
    6.75 +  apply (frule zodd_imp_zdiv_eq, auto)
    6.76 +  done
    6.77  
    6.78  subsection {* Basic Properties of the Gauss Sets *}
    6.79  
    6.80 -lemma (in GAUSS) finite_A: "finite (A)";
    6.81 -  apply (auto simp add: A_def) 
    6.82 -thm bdd_int_set_l_finite;
    6.83 -  apply (subgoal_tac "{x. 0 < x & x \<le> (p - 1) div 2} \<subseteq> {x. 0 \<le> x & x < 1 + (p - 1) div 2}"); 
    6.84 -by (auto simp add: bdd_int_set_l_finite finite_subset)
    6.85 +lemma (in GAUSS) finite_A: "finite (A)"
    6.86 +  apply (auto simp add: A_def)
    6.87 +  apply (subgoal_tac "{x. 0 < x & x \<le> (p - 1) div 2} \<subseteq> {x. 0 \<le> x & x < 1 + (p - 1) div 2}")
    6.88 +  apply (auto simp add: bdd_int_set_l_finite finite_subset)
    6.89 +  done
    6.90  
    6.91 -lemma (in GAUSS) finite_B: "finite (B)";
    6.92 +lemma (in GAUSS) finite_B: "finite (B)"
    6.93    by (auto simp add: B_def finite_A finite_imageI)
    6.94  
    6.95 -lemma (in GAUSS) finite_C: "finite (C)";
    6.96 +lemma (in GAUSS) finite_C: "finite (C)"
    6.97    by (auto simp add: C_def finite_B finite_imageI)
    6.98  
    6.99 -lemma (in GAUSS) finite_D: "finite (D)";
   6.100 +lemma (in GAUSS) finite_D: "finite (D)"
   6.101    by (auto simp add: D_def finite_Int finite_C)
   6.102  
   6.103 -lemma (in GAUSS) finite_E: "finite (E)";
   6.104 +lemma (in GAUSS) finite_E: "finite (E)"
   6.105    by (auto simp add: E_def finite_Int finite_C)
   6.106  
   6.107 -lemma (in GAUSS) finite_F: "finite (F)";
   6.108 +lemma (in GAUSS) finite_F: "finite (F)"
   6.109    by (auto simp add: F_def finite_E finite_imageI)
   6.110  
   6.111 -lemma (in GAUSS) C_eq: "C = D \<union> E";
   6.112 +lemma (in GAUSS) C_eq: "C = D \<union> E"
   6.113    by (auto simp add: C_def D_def E_def)
   6.114  
   6.115 -lemma (in GAUSS) A_card_eq: "card A = nat ((p - 1) div 2)";
   6.116 -  apply (auto simp add: A_def) 
   6.117 +lemma (in GAUSS) A_card_eq: "card A = nat ((p - 1) div 2)"
   6.118 +  apply (auto simp add: A_def)
   6.119    apply (insert int_nat)
   6.120    apply (erule subst)
   6.121 -  by (auto simp add: card_bdd_int_set_l_le)
   6.122 +  apply (auto simp add: card_bdd_int_set_l_le)
   6.123 +  done
   6.124  
   6.125 -lemma (in GAUSS) inj_on_xa_A: "inj_on (%x. x * a) A";
   6.126 -  apply (insert a_nonzero)
   6.127 -by (simp add: A_def inj_on_def)
   6.128 +lemma (in GAUSS) inj_on_xa_A: "inj_on (%x. x * a) A"
   6.129 +  using a_nonzero by (simp add: A_def inj_on_def)
   6.130  
   6.131 -lemma (in GAUSS) A_res: "ResSet p A";
   6.132 -  apply (auto simp add: A_def ResSet_def) 
   6.133 -  apply (rule_tac m = p in zcong_less_eq) 
   6.134 -  apply (insert p_g_2, auto) 
   6.135 -  apply (subgoal_tac [1-2] "(p - 1) div 2 < p");
   6.136 -by (auto, auto simp add: p_minus_one_l)
   6.137 +lemma (in GAUSS) A_res: "ResSet p A"
   6.138 +  apply (auto simp add: A_def ResSet_def)
   6.139 +  apply (rule_tac m = p in zcong_less_eq)
   6.140 +  apply (insert p_g_2, auto)
   6.141 +  apply (subgoal_tac [1-2] "(p - 1) div 2 < p")
   6.142 +  apply (auto, auto simp add: p_minus_one_l)
   6.143 +  done
   6.144  
   6.145 -lemma (in GAUSS) B_res: "ResSet p B";
   6.146 +lemma (in GAUSS) B_res: "ResSet p B"
   6.147    apply (insert p_g_2 p_a_relprime p_minus_one_l)
   6.148 -  apply (auto simp add: B_def) 
   6.149 +  apply (auto simp add: B_def)
   6.150    apply (rule ResSet_image)
   6.151 -  apply (auto simp add: A_res) 
   6.152 +  apply (auto simp add: A_res)
   6.153    apply (auto simp add: A_def)
   6.154 -  proof -;
   6.155 -    fix x fix y
   6.156 -    assume a: "[x * a = y * a] (mod p)"
   6.157 -    assume b: "0 < x"
   6.158 -    assume c: "x \<le> (p - 1) div 2"
   6.159 -    assume d: "0 < y"
   6.160 -    assume e: "y \<le> (p - 1) div 2"
   6.161 -    from a p_a_relprime p_prime a_nonzero zcong_cancel [of p a x y] 
   6.162 -        have "[x = y](mod p)";
   6.163 -      by (simp add: zprime_imp_zrelprime zcong_def p_g_0 order_le_less) 
   6.164 -    with zcong_less_eq [of x y p] p_minus_one_l 
   6.165 -         order_le_less_trans [of x "(p - 1) div 2" p]
   6.166 -         order_le_less_trans [of y "(p - 1) div 2" p] show "x = y";
   6.167 -      by (simp add: prems p_minus_one_l p_g_0)
   6.168 -qed;
   6.169 +proof -
   6.170 +  fix x fix y
   6.171 +  assume a: "[x * a = y * a] (mod p)"
   6.172 +  assume b: "0 < x"
   6.173 +  assume c: "x \<le> (p - 1) div 2"
   6.174 +  assume d: "0 < y"
   6.175 +  assume e: "y \<le> (p - 1) div 2"
   6.176 +  from a p_a_relprime p_prime a_nonzero zcong_cancel [of p a x y]
   6.177 +  have "[x = y](mod p)"
   6.178 +    by (simp add: zprime_imp_zrelprime zcong_def p_g_0 order_le_less)
   6.179 +  with zcong_less_eq [of x y p] p_minus_one_l
   6.180 +      order_le_less_trans [of x "(p - 1) div 2" p]
   6.181 +      order_le_less_trans [of y "(p - 1) div 2" p] show "x = y"
   6.182 +    by (simp add: prems p_minus_one_l p_g_0)
   6.183 +qed
   6.184  
   6.185 -lemma (in GAUSS) SR_B_inj: "inj_on (StandardRes p) B";
   6.186 +lemma (in GAUSS) SR_B_inj: "inj_on (StandardRes p) B"
   6.187    apply (auto simp add: B_def StandardRes_def inj_on_def A_def prems)
   6.188 -  proof -;
   6.189 -    fix x fix y
   6.190 -    assume a: "x * a mod p = y * a mod p"
   6.191 -    assume b: "0 < x"
   6.192 -    assume c: "x \<le> (p - 1) div 2"
   6.193 -    assume d: "0 < y"
   6.194 -    assume e: "y \<le> (p - 1) div 2"
   6.195 -    assume f: "x \<noteq> y"
   6.196 -    from a have "[x * a = y * a](mod p)";
   6.197 -      by (simp add: zcong_zmod_eq p_g_0)
   6.198 -    with p_a_relprime p_prime a_nonzero zcong_cancel [of p a x y] 
   6.199 -        have "[x = y](mod p)";
   6.200 -      by (simp add: zprime_imp_zrelprime zcong_def p_g_0 order_le_less) 
   6.201 -    with zcong_less_eq [of x y p] p_minus_one_l 
   6.202 -         order_le_less_trans [of x "(p - 1) div 2" p]
   6.203 -         order_le_less_trans [of y "(p - 1) div 2" p] have "x = y";
   6.204 -      by (simp add: prems p_minus_one_l p_g_0)
   6.205 -    then have False;
   6.206 -      by (simp add: f)
   6.207 -    then show "a = 0";
   6.208 -      by simp
   6.209 -qed;
   6.210 +proof -
   6.211 +  fix x fix y
   6.212 +  assume a: "x * a mod p = y * a mod p"
   6.213 +  assume b: "0 < x"
   6.214 +  assume c: "x \<le> (p - 1) div 2"
   6.215 +  assume d: "0 < y"
   6.216 +  assume e: "y \<le> (p - 1) div 2"
   6.217 +  assume f: "x \<noteq> y"
   6.218 +  from a have "[x * a = y * a](mod p)"
   6.219 +    by (simp add: zcong_zmod_eq p_g_0)
   6.220 +  with p_a_relprime p_prime a_nonzero zcong_cancel [of p a x y]
   6.221 +  have "[x = y](mod p)"
   6.222 +    by (simp add: zprime_imp_zrelprime zcong_def p_g_0 order_le_less)
   6.223 +  with zcong_less_eq [of x y p] p_minus_one_l
   6.224 +    order_le_less_trans [of x "(p - 1) div 2" p]
   6.225 +    order_le_less_trans [of y "(p - 1) div 2" p] have "x = y"
   6.226 +    by (simp add: prems p_minus_one_l p_g_0)
   6.227 +  then have False
   6.228 +    by (simp add: f)
   6.229 +  then show "a = 0"
   6.230 +    by simp
   6.231 +qed
   6.232  
   6.233 -lemma (in GAUSS) inj_on_pminusx_E: "inj_on (%x. p - x) E";
   6.234 +lemma (in GAUSS) inj_on_pminusx_E: "inj_on (%x. p - x) E"
   6.235    apply (auto simp add: E_def C_def B_def A_def)
   6.236 -  apply (rule_tac g = "%x. -1 * (x - p)" in inj_on_inverseI);
   6.237 -by auto
   6.238 +  apply (rule_tac g = "%x. -1 * (x - p)" in inj_on_inverseI)
   6.239 +  apply auto
   6.240 +  done
   6.241  
   6.242 -lemma (in GAUSS) A_ncong_p: "x \<in> A ==> ~[x = 0](mod p)";
   6.243 +lemma (in GAUSS) A_ncong_p: "x \<in> A ==> ~[x = 0](mod p)"
   6.244    apply (auto simp add: A_def)
   6.245    apply (frule_tac m = p in zcong_not_zero)
   6.246    apply (insert p_minus_one_l)
   6.247 -by auto
   6.248 +  apply auto
   6.249 +  done
   6.250  
   6.251 -lemma (in GAUSS) A_greater_zero: "x \<in> A ==> 0 < x";
   6.252 +lemma (in GAUSS) A_greater_zero: "x \<in> A ==> 0 < x"
   6.253    by (auto simp add: A_def)
   6.254  
   6.255 -lemma (in GAUSS) B_ncong_p: "x \<in> B ==> ~[x = 0](mod p)";
   6.256 +lemma (in GAUSS) B_ncong_p: "x \<in> B ==> ~[x = 0](mod p)"
   6.257    apply (auto simp add: B_def)
   6.258 -  apply (frule A_ncong_p) 
   6.259 +  apply (frule A_ncong_p)
   6.260    apply (insert p_a_relprime p_prime a_nonzero)
   6.261    apply (frule_tac a = x and b = a in zcong_zprime_prod_zero_contra)
   6.262 -by (auto simp add: A_greater_zero)
   6.263 +  apply (auto simp add: A_greater_zero)
   6.264 +  done
   6.265  
   6.266 -lemma (in GAUSS) B_greater_zero: "x \<in> B ==> 0 < x";
   6.267 -  apply (insert a_nonzero)
   6.268 -by (auto simp add: B_def mult_pos_pos A_greater_zero)
   6.269 +lemma (in GAUSS) B_greater_zero: "x \<in> B ==> 0 < x"
   6.270 +  using a_nonzero by (auto simp add: B_def mult_pos_pos A_greater_zero)
   6.271  
   6.272 -lemma (in GAUSS) C_ncong_p: "x \<in> C ==>  ~[x = 0](mod p)";
   6.273 +lemma (in GAUSS) C_ncong_p: "x \<in> C ==>  ~[x = 0](mod p)"
   6.274    apply (auto simp add: C_def)
   6.275    apply (frule B_ncong_p)
   6.276 -  apply (subgoal_tac "[x = StandardRes p x](mod p)");
   6.277 -  defer; apply (simp add: StandardRes_prop1)
   6.278 +  apply (subgoal_tac "[x = StandardRes p x](mod p)")
   6.279 +  defer apply (simp add: StandardRes_prop1)
   6.280    apply (frule_tac a = x and b = "StandardRes p x" and c = 0 in zcong_trans)
   6.281 -by auto
   6.282 +  apply auto
   6.283 +  done
   6.284  
   6.285 -lemma (in GAUSS) C_greater_zero: "y \<in> C ==> 0 < y";
   6.286 +lemma (in GAUSS) C_greater_zero: "y \<in> C ==> 0 < y"
   6.287    apply (auto simp add: C_def)
   6.288 -  proof -;
   6.289 -    fix x;
   6.290 -    assume a: "x \<in> B";
   6.291 -    from p_g_0 have "0 \<le> StandardRes p x";
   6.292 -      by (simp add: StandardRes_lbound)
   6.293 -    moreover have "~[x = 0] (mod p)";
   6.294 -      by (simp add: a B_ncong_p)
   6.295 -    then have "StandardRes p x \<noteq> 0";
   6.296 -      by (simp add: StandardRes_prop3)
   6.297 -    ultimately show "0 < StandardRes p x";
   6.298 -      by (simp add: order_le_less)
   6.299 -qed;
   6.300 +proof -
   6.301 +  fix x
   6.302 +  assume a: "x \<in> B"
   6.303 +  from p_g_0 have "0 \<le> StandardRes p x"
   6.304 +    by (simp add: StandardRes_lbound)
   6.305 +  moreover have "~[x = 0] (mod p)"
   6.306 +    by (simp add: a B_ncong_p)
   6.307 +  then have "StandardRes p x \<noteq> 0"
   6.308 +    by (simp add: StandardRes_prop3)
   6.309 +  ultimately show "0 < StandardRes p x"
   6.310 +    by (simp add: order_le_less)
   6.311 +qed
   6.312  
   6.313 -lemma (in GAUSS) D_ncong_p: "x \<in> D ==> ~[x = 0](mod p)";
   6.314 +lemma (in GAUSS) D_ncong_p: "x \<in> D ==> ~[x = 0](mod p)"
   6.315    by (auto simp add: D_def C_ncong_p)
   6.316  
   6.317 -lemma (in GAUSS) E_ncong_p: "x \<in> E ==> ~[x = 0](mod p)";
   6.318 +lemma (in GAUSS) E_ncong_p: "x \<in> E ==> ~[x = 0](mod p)"
   6.319    by (auto simp add: E_def C_ncong_p)
   6.320  
   6.321 -lemma (in GAUSS) F_ncong_p: "x \<in> F ==> ~[x = 0](mod p)";
   6.322 -  apply (auto simp add: F_def) 
   6.323 -  proof -;
   6.324 -    fix x assume a: "x \<in> E" assume b: "[p - x = 0] (mod p)"
   6.325 -    from E_ncong_p have "~[x = 0] (mod p)";
   6.326 -      by (simp add: a)
   6.327 -    moreover from a have "0 < x";
   6.328 -      by (simp add: a E_def C_greater_zero)
   6.329 -    moreover from a have "x < p";
   6.330 -      by (auto simp add: E_def C_def p_g_0 StandardRes_ubound)
   6.331 -    ultimately have "~[p - x = 0] (mod p)";
   6.332 -      by (simp add: zcong_not_zero)
   6.333 -    from this show False by (simp add: b)
   6.334 -qed;
   6.335 +lemma (in GAUSS) F_ncong_p: "x \<in> F ==> ~[x = 0](mod p)"
   6.336 +  apply (auto simp add: F_def)
   6.337 +proof -
   6.338 +  fix x assume a: "x \<in> E" assume b: "[p - x = 0] (mod p)"
   6.339 +  from E_ncong_p have "~[x = 0] (mod p)"
   6.340 +    by (simp add: a)
   6.341 +  moreover from a have "0 < x"
   6.342 +    by (simp add: a E_def C_greater_zero)
   6.343 +  moreover from a have "x < p"
   6.344 +    by (auto simp add: E_def C_def p_g_0 StandardRes_ubound)
   6.345 +  ultimately have "~[p - x = 0] (mod p)"
   6.346 +    by (simp add: zcong_not_zero)
   6.347 +  from this show False by (simp add: b)
   6.348 +qed
   6.349  
   6.350 -lemma (in GAUSS) F_subset: "F \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}";
   6.351 -  apply (auto simp add: F_def E_def) 
   6.352 +lemma (in GAUSS) F_subset: "F \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}"
   6.353 +  apply (auto simp add: F_def E_def)
   6.354    apply (insert p_g_0)
   6.355    apply (frule_tac x = xa in StandardRes_ubound)
   6.356    apply (frule_tac x = x in StandardRes_ubound)
   6.357    apply (subgoal_tac "xa = StandardRes p xa")
   6.358    apply (auto simp add: C_def StandardRes_prop2 StandardRes_prop1)
   6.359 -  proof -;
   6.360 -    from zodd_imp_zdiv_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 have 
   6.361 -        "2 * (p - 1) div 2 = 2 * ((p - 1) div 2)";
   6.362 -      by simp
   6.363 -    with p_eq2 show " !!x. [| (p - 1) div 2 < StandardRes p x; x \<in> B |]
   6.364 -         ==> p - StandardRes p x \<le> (p - 1) div 2";
   6.365 -      by simp
   6.366 -qed;
   6.367 +proof -
   6.368 +  from zodd_imp_zdiv_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 have
   6.369 +    "2 * (p - 1) div 2 = 2 * ((p - 1) div 2)"
   6.370 +    by simp
   6.371 +  with p_eq2 show " !!x. [| (p - 1) div 2 < StandardRes p x; x \<in> B |]
   6.372 +      ==> p - StandardRes p x \<le> (p - 1) div 2"
   6.373 +    by simp
   6.374 +qed
   6.375  
   6.376 -lemma (in GAUSS) D_subset: "D \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}";
   6.377 +lemma (in GAUSS) D_subset: "D \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}"
   6.378    by (auto simp add: D_def C_greater_zero)
   6.379  
   6.380 -lemma (in GAUSS) F_eq: "F = {x. \<exists>y \<in> A. ( x = p - (StandardRes p (y*a)) & (p - 1) div 2 < StandardRes p (y*a))}";
   6.381 +lemma (in GAUSS) F_eq: "F = {x. \<exists>y \<in> A. ( x = p - (StandardRes p (y*a)) & (p - 1) div 2 < StandardRes p (y*a))}"
   6.382    by (auto simp add: F_def E_def D_def C_def B_def A_def)
   6.383  
   6.384 -lemma (in GAUSS) D_eq: "D = {x. \<exists>y \<in> A. ( x = StandardRes p (y*a) & StandardRes p (y*a) \<le> (p - 1) div 2)}";
   6.385 +lemma (in GAUSS) D_eq: "D = {x. \<exists>y \<in> A. ( x = StandardRes p (y*a) & StandardRes p (y*a) \<le> (p - 1) div 2)}"
   6.386    by (auto simp add: D_def C_def B_def A_def)
   6.387  
   6.388 -lemma (in GAUSS) D_leq: "x \<in> D ==> x \<le> (p - 1) div 2";
   6.389 +lemma (in GAUSS) D_leq: "x \<in> D ==> x \<le> (p - 1) div 2"
   6.390    by (auto simp add: D_eq)
   6.391  
   6.392 -lemma (in GAUSS) F_ge: "x \<in> F ==> x \<le> (p - 1) div 2";
   6.393 +lemma (in GAUSS) F_ge: "x \<in> F ==> x \<le> (p - 1) div 2"
   6.394    apply (auto simp add: F_eq A_def)
   6.395 -  proof -;
   6.396 -    fix y;
   6.397 -    assume "(p - 1) div 2 < StandardRes p (y * a)";
   6.398 -    then have "p - StandardRes p (y * a) < p - ((p - 1) div 2)";
   6.399 -      by arith
   6.400 -    also from p_eq2 have "... = 2 * ((p - 1) div 2) + 1 - ((p - 1) div 2)"; 
   6.401 -      by (rule subst, auto)
   6.402 -    also; have "2 * ((p - 1) div 2) + 1 - (p - 1) div 2 = (p - 1) div 2 + 1";
   6.403 -      by arith
   6.404 -    finally show "p - StandardRes p (y * a) \<le> (p - 1) div 2";
   6.405 -      by (insert zless_add1_eq [of "p - StandardRes p (y * a)" 
   6.406 -          "(p - 1) div 2"],auto);
   6.407 -qed;
   6.408 +proof -
   6.409 +  fix y
   6.410 +  assume "(p - 1) div 2 < StandardRes p (y * a)"
   6.411 +  then have "p - StandardRes p (y * a) < p - ((p - 1) div 2)"
   6.412 +    by arith
   6.413 +  also from p_eq2 have "... = 2 * ((p - 1) div 2) + 1 - ((p - 1) div 2)"
   6.414 +    by auto
   6.415 +  also have "2 * ((p - 1) div 2) + 1 - (p - 1) div 2 = (p - 1) div 2 + 1"
   6.416 +    by arith
   6.417 +  finally show "p - StandardRes p (y * a) \<le> (p - 1) div 2"
   6.418 +    using zless_add1_eq [of "p - StandardRes p (y * a)" "(p - 1) div 2"] by auto
   6.419 +qed
   6.420  
   6.421 -lemma (in GAUSS) all_A_relprime: "\<forall>x \<in> A. zgcd(x,p) = 1";
   6.422 -  apply (insert p_prime p_minus_one_l)
   6.423 -by (auto simp add: A_def zless_zprime_imp_zrelprime)
   6.424 +lemma (in GAUSS) all_A_relprime: "\<forall>x \<in> A. zgcd(x, p) = 1"
   6.425 +  using p_prime p_minus_one_l by (auto simp add: A_def zless_zprime_imp_zrelprime)
   6.426  
   6.427 -lemma (in GAUSS) A_prod_relprime: "zgcd((setprod id A),p) = 1";
   6.428 -  by (insert all_A_relprime finite_A, simp add: all_relprime_prod_relprime)
   6.429 +lemma (in GAUSS) A_prod_relprime: "zgcd((setprod id A),p) = 1"
   6.430 +  using all_A_relprime finite_A by (simp add: all_relprime_prod_relprime)
   6.431  
   6.432  subsection {* Relationships Between Gauss Sets *}
   6.433  
   6.434 -lemma (in GAUSS) B_card_eq_A: "card B = card A";
   6.435 -  apply (insert finite_A)
   6.436 -by (simp add: finite_A B_def inj_on_xa_A card_image)
   6.437 +lemma (in GAUSS) B_card_eq_A: "card B = card A"
   6.438 +  using finite_A by (simp add: finite_A B_def inj_on_xa_A card_image)
   6.439  
   6.440 -lemma (in GAUSS) B_card_eq: "card B = nat ((p - 1) div 2)";
   6.441 -  by (auto simp add: B_card_eq_A A_card_eq)
   6.442 +lemma (in GAUSS) B_card_eq: "card B = nat ((p - 1) div 2)"
   6.443 +  by (simp add: B_card_eq_A A_card_eq)
   6.444  
   6.445 -lemma (in GAUSS) F_card_eq_E: "card F = card E";
   6.446 -  apply (insert finite_E)
   6.447 -by (simp add: F_def inj_on_pminusx_E card_image)
   6.448 +lemma (in GAUSS) F_card_eq_E: "card F = card E"
   6.449 +  using finite_E by (simp add: F_def inj_on_pminusx_E card_image)
   6.450  
   6.451 -lemma (in GAUSS) C_card_eq_B: "card C = card B";
   6.452 +lemma (in GAUSS) C_card_eq_B: "card C = card B"
   6.453    apply (insert finite_B)
   6.454 -  apply (subgoal_tac "inj_on (StandardRes p) B");
   6.455 +  apply (subgoal_tac "inj_on (StandardRes p) B")
   6.456    apply (simp add: B_def C_def card_image)
   6.457    apply (rule StandardRes_inj_on_ResSet)
   6.458 -by (simp add: B_res)
   6.459 +  apply (simp add: B_res)
   6.460 +  done
   6.461  
   6.462 -lemma (in GAUSS) D_E_disj: "D \<inter> E = {}";
   6.463 +lemma (in GAUSS) D_E_disj: "D \<inter> E = {}"
   6.464    by (auto simp add: D_def E_def)
   6.465  
   6.466 -lemma (in GAUSS) C_card_eq_D_plus_E: "card C = card D + card E";
   6.467 +lemma (in GAUSS) C_card_eq_D_plus_E: "card C = card D + card E"
   6.468    by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E)
   6.469  
   6.470 -lemma (in GAUSS) C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C";
   6.471 +lemma (in GAUSS) C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C"
   6.472    apply (insert D_E_disj finite_D finite_E C_eq)
   6.473    apply (frule setprod_Un_disjoint [of D E id])
   6.474 -by auto
   6.475 +  apply auto
   6.476 +  done
   6.477  
   6.478 -lemma (in GAUSS) C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)";
   6.479 +lemma (in GAUSS) C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)"
   6.480    apply (auto simp add: C_def)
   6.481 -  apply (insert finite_B SR_B_inj) 
   6.482 -  apply (frule_tac f1 = "StandardRes p" in setprod_reindex_id[THEN sym], auto)
   6.483 +  apply (insert finite_B SR_B_inj)
   6.484 +  apply (frule_tac f1 = "StandardRes p" in setprod_reindex_id [symmetric], auto)
   6.485    apply (rule setprod_same_function_zcong)
   6.486 -by (auto simp add: StandardRes_prop1 zcong_sym p_g_0)
   6.487 +  apply (auto simp add: StandardRes_prop1 zcong_sym p_g_0)
   6.488 +  done
   6.489  
   6.490 -lemma (in GAUSS) F_Un_D_subset: "(F \<union> D) \<subseteq> A";
   6.491 +lemma (in GAUSS) F_Un_D_subset: "(F \<union> D) \<subseteq> A"
   6.492    apply (rule Un_least)
   6.493 -by (auto simp add: A_def F_subset D_subset)
   6.494 +  apply (auto simp add: A_def F_subset D_subset)
   6.495 +  done
   6.496  
   6.497 -lemma two_eq: "2 * (x::int) = x + x";
   6.498 +lemma two_eq: "2 * (x::int) = x + x"
   6.499    by arith
   6.500  
   6.501 -lemma (in GAUSS) F_D_disj: "(F \<inter> D) = {}";
   6.502 +lemma (in GAUSS) F_D_disj: "(F \<inter> D) = {}"
   6.503    apply (simp add: F_eq D_eq)
   6.504    apply (auto simp add: F_eq D_eq)
   6.505 -  proof -;
   6.506 -    fix y; fix ya;
   6.507 -    assume "p - StandardRes p (y * a) = StandardRes p (ya * a)";
   6.508 -    then have "p = StandardRes p (y * a) + StandardRes p (ya * a)";
   6.509 -      by arith
   6.510 -    moreover have "p dvd p";
   6.511 -      by auto
   6.512 -    ultimately have "p dvd (StandardRes p (y * a) + StandardRes p (ya * a))";
   6.513 -      by auto
   6.514 -    then have a: "[StandardRes p (y * a) + StandardRes p (ya * a) = 0] (mod p)";
   6.515 -      by (auto simp add: zcong_def)
   6.516 -    have "[y * a = StandardRes p (y * a)] (mod p)";
   6.517 -      by (simp only: zcong_sym StandardRes_prop1)
   6.518 -    moreover have "[ya * a = StandardRes p (ya * a)] (mod p)";
   6.519 -      by (simp only: zcong_sym StandardRes_prop1)
   6.520 -    ultimately have "[y * a + ya * a = 
   6.521 -        StandardRes p (y * a) + StandardRes p (ya * a)] (mod p)";
   6.522 -      by (rule zcong_zadd)
   6.523 -    with a have "[y * a + ya * a = 0] (mod p)";
   6.524 -      apply (elim zcong_trans)
   6.525 -      by (simp only: zcong_refl)
   6.526 -    also have "y * a + ya * a = a * (y + ya)";
   6.527 -      by (simp add: zadd_zmult_distrib2 zmult_commute)
   6.528 -    finally have "[a * (y + ya) = 0] (mod p)";.;
   6.529 -    with p_prime a_nonzero zcong_zprime_prod_zero [of p a "y + ya"]
   6.530 -        p_a_relprime
   6.531 -        have a: "[y + ya = 0] (mod p)";
   6.532 -      by auto
   6.533 -    assume b: "y \<in> A" and c: "ya: A";
   6.534 -    with A_def have "0 < y + ya";
   6.535 -      by auto
   6.536 -    moreover from b c A_def have "y + ya \<le> (p - 1) div 2 + (p - 1) div 2";
   6.537 -      by auto 
   6.538 -    moreover from b c p_eq2 A_def have "y + ya < p";
   6.539 -      by auto
   6.540 -    ultimately show False;
   6.541 -      apply simp
   6.542 -      apply (frule_tac m = p in zcong_not_zero)
   6.543 -      by (auto simp add: a)
   6.544 -qed;
   6.545 +proof -
   6.546 +  fix y fix ya
   6.547 +  assume "p - StandardRes p (y * a) = StandardRes p (ya * a)"
   6.548 +  then have "p = StandardRes p (y * a) + StandardRes p (ya * a)"
   6.549 +    by arith
   6.550 +  moreover have "p dvd p"
   6.551 +    by auto
   6.552 +  ultimately have "p dvd (StandardRes p (y * a) + StandardRes p (ya * a))"
   6.553 +    by auto
   6.554 +  then have a: "[StandardRes p (y * a) + StandardRes p (ya * a) = 0] (mod p)"
   6.555 +    by (auto simp add: zcong_def)
   6.556 +  have "[y * a = StandardRes p (y * a)] (mod p)"
   6.557 +    by (simp only: zcong_sym StandardRes_prop1)
   6.558 +  moreover have "[ya * a = StandardRes p (ya * a)] (mod p)"
   6.559 +    by (simp only: zcong_sym StandardRes_prop1)
   6.560 +  ultimately have "[y * a + ya * a =
   6.561 +    StandardRes p (y * a) + StandardRes p (ya * a)] (mod p)"
   6.562 +    by (rule zcong_zadd)
   6.563 +  with a have "[y * a + ya * a = 0] (mod p)"
   6.564 +    apply (elim zcong_trans)
   6.565 +    by (simp only: zcong_refl)
   6.566 +  also have "y * a + ya * a = a * (y + ya)"
   6.567 +    by (simp add: zadd_zmult_distrib2 zmult_commute)
   6.568 +  finally have "[a * (y + ya) = 0] (mod p)" .
   6.569 +  with p_prime a_nonzero zcong_zprime_prod_zero [of p a "y + ya"]
   6.570 +    p_a_relprime
   6.571 +  have a: "[y + ya = 0] (mod p)"
   6.572 +    by auto
   6.573 +  assume b: "y \<in> A" and c: "ya: A"
   6.574 +  with A_def have "0 < y + ya"
   6.575 +    by auto
   6.576 +  moreover from b c A_def have "y + ya \<le> (p - 1) div 2 + (p - 1) div 2"
   6.577 +    by auto
   6.578 +  moreover from b c p_eq2 A_def have "y + ya < p"
   6.579 +    by auto
   6.580 +  ultimately show False
   6.581 +    apply simp
   6.582 +    apply (frule_tac m = p in zcong_not_zero)
   6.583 +    apply (auto simp add: a)
   6.584 +    done
   6.585 +qed
   6.586  
   6.587 -lemma (in GAUSS) F_Un_D_card: "card (F \<union> D) = nat ((p - 1) div 2)";
   6.588 +lemma (in GAUSS) F_Un_D_card: "card (F \<union> D) = nat ((p - 1) div 2)"
   6.589    apply (insert F_D_disj finite_F finite_D)
   6.590 -  proof -;
   6.591 -    have "card (F \<union> D) = card E + card D";
   6.592 -      by (auto simp add: finite_F finite_D F_D_disj 
   6.593 -                         card_Un_disjoint F_card_eq_E)
   6.594 -    then have "card (F \<union> D) = card C";
   6.595 -      by (simp add: C_card_eq_D_plus_E)
   6.596 -    from this show "card (F \<union> D) = nat ((p - 1) div 2)"; 
   6.597 -      by (simp add: C_card_eq_B B_card_eq)
   6.598 -qed;
   6.599 +proof -
   6.600 +  have "card (F \<union> D) = card E + card D"
   6.601 +    by (auto simp add: finite_F finite_D F_D_disj
   6.602 +      card_Un_disjoint F_card_eq_E)
   6.603 +  then have "card (F \<union> D) = card C"
   6.604 +    by (simp add: C_card_eq_D_plus_E)
   6.605 +  from this show "card (F \<union> D) = nat ((p - 1) div 2)"
   6.606 +    by (simp add: C_card_eq_B B_card_eq)
   6.607 +qed
   6.608  
   6.609 -lemma (in GAUSS) F_Un_D_eq_A: "F \<union> D = A";
   6.610 -  apply (insert finite_A F_Un_D_subset A_card_eq F_Un_D_card) 
   6.611 -by (auto simp add: card_seteq)
   6.612 +lemma (in GAUSS) F_Un_D_eq_A: "F \<union> D = A"
   6.613 +  using finite_A F_Un_D_subset A_card_eq F_Un_D_card by (auto simp add: card_seteq)
   6.614  
   6.615 -lemma (in GAUSS) prod_D_F_eq_prod_A: 
   6.616 -    "(setprod id D) * (setprod id F) = setprod id A";
   6.617 +lemma (in GAUSS) prod_D_F_eq_prod_A:
   6.618 +    "(setprod id D) * (setprod id F) = setprod id A"
   6.619    apply (insert F_D_disj finite_D finite_F)
   6.620    apply (frule setprod_Un_disjoint [of F D id])
   6.621 -by (auto simp add: F_Un_D_eq_A)
   6.622 +  apply (auto simp add: F_Un_D_eq_A)
   6.623 +  done
   6.624  
   6.625  lemma (in GAUSS) prod_F_zcong:
   6.626 -    "[setprod id F = ((-1) ^ (card E)) * (setprod id E)] (mod p)"
   6.627 -  proof -
   6.628 -    have "setprod id F = setprod id (op - p ` E)"
   6.629 -      by (auto simp add: F_def)
   6.630 -    then have "setprod id F = setprod (op - p) E"
   6.631 -      apply simp
   6.632 -      apply (insert finite_E inj_on_pminusx_E)
   6.633 -      by (frule_tac f = "op - p" in setprod_reindex_id, auto)
   6.634 -    then have one: 
   6.635 -      "[setprod id F = setprod (StandardRes p o (op - p)) E] (mod p)"
   6.636 -      apply simp
   6.637 -      apply (insert p_g_0 finite_E)
   6.638 -      by (auto simp add: StandardRes_prod)
   6.639 -    moreover have a: "\<forall>x \<in> E. [p - x = 0 - x] (mod p)"
   6.640 -      apply clarify
   6.641 -      apply (insert zcong_id [of p])
   6.642 -      by (rule_tac a = p and m = p and c = x and d = x in zcong_zdiff, auto)
   6.643 -    moreover have b: "\<forall>x \<in> E. [StandardRes p (p - x) = p - x](mod p)"
   6.644 -      apply clarify
   6.645 -      by (simp add: StandardRes_prop1 zcong_sym)
   6.646 -    moreover have "\<forall>x \<in> E. [StandardRes p (p - x) = - x](mod p)"
   6.647 -      apply clarify
   6.648 -      apply (insert a b)
   6.649 -      by (rule_tac b = "p - x" in zcong_trans, auto)
   6.650 -    ultimately have c:
   6.651 -      "[setprod (StandardRes p o (op - p)) E = setprod (uminus) E](mod p)"
   6.652 -      apply simp
   6.653 -      apply (insert finite_E p_g_0)
   6.654 -      by (rule setprod_same_function_zcong [of E "StandardRes p o (op - p)"
   6.655 -                                                     uminus p], auto)
   6.656 -    then have two: "[setprod id F = setprod (uminus) E](mod p)"
   6.657 -      apply (insert one c)
   6.658 -      by (rule zcong_trans [of "setprod id F" 
   6.659 +  "[setprod id F = ((-1) ^ (card E)) * (setprod id E)] (mod p)"
   6.660 +proof -
   6.661 +  have "setprod id F = setprod id (op - p ` E)"
   6.662 +    by (auto simp add: F_def)
   6.663 +  then have "setprod id F = setprod (op - p) E"
   6.664 +    apply simp
   6.665 +    apply (insert finite_E inj_on_pminusx_E)
   6.666 +    apply (frule_tac f = "op - p" in setprod_reindex_id, auto)
   6.667 +    done
   6.668 +  then have one:
   6.669 +    "[setprod id F = setprod (StandardRes p o (op - p)) E] (mod p)"
   6.670 +    apply simp
   6.671 +    apply (insert p_g_0 finite_E)
   6.672 +    by (auto simp add: StandardRes_prod)
   6.673 +  moreover have a: "\<forall>x \<in> E. [p - x = 0 - x] (mod p)"
   6.674 +    apply clarify
   6.675 +    apply (insert zcong_id [of p])
   6.676 +    apply (rule_tac a = p and m = p and c = x and d = x in zcong_zdiff, auto)
   6.677 +    done
   6.678 +  moreover have b: "\<forall>x \<in> E. [StandardRes p (p - x) = p - x](mod p)"
   6.679 +    apply clarify
   6.680 +    apply (simp add: StandardRes_prop1 zcong_sym)
   6.681 +    done
   6.682 +  moreover have "\<forall>x \<in> E. [StandardRes p (p - x) = - x](mod p)"
   6.683 +    apply clarify
   6.684 +    apply (insert a b)
   6.685 +    apply (rule_tac b = "p - x" in zcong_trans, auto)
   6.686 +    done
   6.687 +  ultimately have c:
   6.688 +    "[setprod (StandardRes p o (op - p)) E = setprod (uminus) E](mod p)"
   6.689 +    apply simp
   6.690 +    apply (insert finite_E p_g_0)
   6.691 +    apply (rule setprod_same_function_zcong
   6.692 +      [of E "StandardRes p o (op - p)" uminus p], auto)
   6.693 +    done
   6.694 +  then have two: "[setprod id F = setprod (uminus) E](mod p)"
   6.695 +    apply (insert one c)
   6.696 +    apply (rule zcong_trans [of "setprod id F"
   6.697                                 "setprod (StandardRes p o op - p) E" p
   6.698 -                               "setprod uminus E"], auto) 
   6.699 -    also have "setprod uminus E = (setprod id E) * (-1)^(card E)" 
   6.700 -      apply (insert finite_E)
   6.701 -      by (induct set: Finites, auto)
   6.702 -    then have "setprod uminus E = (-1) ^ (card E) * (setprod id E)"
   6.703 -      by (simp add: zmult_commute)
   6.704 -    with two show ?thesis
   6.705 -      by simp
   6.706 +                               "setprod uminus E"], auto)
   6.707 +    done
   6.708 +  also have "setprod uminus E = (setprod id E) * (-1)^(card E)"
   6.709 +    using finite_E by (induct set: Finites) auto
   6.710 +  then have "setprod uminus E = (-1) ^ (card E) * (setprod id E)"
   6.711 +    by (simp add: zmult_commute)
   6.712 +  with two show ?thesis
   6.713 +    by simp
   6.714  qed
   6.715  
   6.716  subsection {* Gauss' Lemma *}
   6.717 @@ -439,60 +446,65 @@
   6.718    by (auto simp add: finite_E neg_one_special)
   6.719  
   6.720  theorem (in GAUSS) pre_gauss_lemma:
   6.721 -    "[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)"
   6.722 -  proof -
   6.723 -    have "[setprod id A = setprod id F * setprod id D](mod p)"
   6.724 -      by (auto simp add: prod_D_F_eq_prod_A zmult_commute)
   6.725 -    then have "[setprod id A = ((-1)^(card E) * setprod id E) * 
   6.726 -        setprod id D] (mod p)"
   6.727 -      apply (rule zcong_trans)
   6.728 -      by (auto simp add: prod_F_zcong zcong_scalar)
   6.729 -    then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
   6.730 -      apply (rule zcong_trans)
   6.731 -      apply (insert C_prod_eq_D_times_E, erule subst)
   6.732 -      by (subst zmult_assoc, auto)
   6.733 -    then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
   6.734 -      apply (rule zcong_trans)
   6.735 -      by (simp add: C_B_zcong_prod zcong_scalar2)
   6.736 -    then have "[setprod id A = ((-1)^(card E) *
   6.737 -        (setprod id ((%x. x * a) ` A)))] (mod p)"
   6.738 -      by (simp add: B_def)
   6.739 -    then have "[setprod id A = ((-1)^(card E) * (setprod (%x. x * a) A))] 
   6.740 -        (mod p)"
   6.741 -      by(simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric])
   6.742 -    moreover have "setprod (%x. x * a) A = 
   6.743 -        setprod (%x. a) A * setprod id A"
   6.744 -      by (insert finite_A, induct set: Finites, auto)
   6.745 -    ultimately have "[setprod id A = ((-1)^(card E) * (setprod (%x. a) A * 
   6.746 -        setprod id A))] (mod p)"
   6.747 -      by simp 
   6.748 -    then have "[setprod id A = ((-1)^(card E) * a^(card A) * 
   6.749 -        setprod id A)](mod p)"
   6.750 -      apply (rule zcong_trans)
   6.751 -      by (simp add: zcong_scalar2 zcong_scalar finite_A setprod_constant
   6.752 -        zmult_assoc)
   6.753 -    then have a: "[setprod id A * (-1)^(card E) = 
   6.754 -        ((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)"
   6.755 -      by (rule zcong_scalar)
   6.756 -    then have "[setprod id A * (-1)^(card E) = setprod id A * 
   6.757 -        (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
   6.758 -      apply (rule zcong_trans)
   6.759 -      by (simp add: a mult_commute mult_left_commute)
   6.760 -    then have "[setprod id A * (-1)^(card E) = setprod id A * 
   6.761 -        a^(card A)](mod p)"
   6.762 -      apply (rule zcong_trans)
   6.763 -      by (simp add: aux)
   6.764 -    with this zcong_cancel2 [of p "setprod id A" "-1 ^ card E" "a ^ card A"]
   6.765 -         p_g_0 A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)"
   6.766 -       by (simp add: order_less_imp_le)
   6.767 -    from this show ?thesis
   6.768 -      by (simp add: A_card_eq zcong_sym)
   6.769 +  "[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)"
   6.770 +proof -
   6.771 +  have "[setprod id A = setprod id F * setprod id D](mod p)"
   6.772 +    by (auto simp add: prod_D_F_eq_prod_A zmult_commute)
   6.773 +  then have "[setprod id A = ((-1)^(card E) * setprod id E) *
   6.774 +      setprod id D] (mod p)"
   6.775 +    apply (rule zcong_trans)
   6.776 +    apply (auto simp add: prod_F_zcong zcong_scalar)
   6.777 +    done
   6.778 +  then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
   6.779 +    apply (rule zcong_trans)
   6.780 +    apply (insert C_prod_eq_D_times_E, erule subst)
   6.781 +    apply (subst zmult_assoc, auto)
   6.782 +    done
   6.783 +  then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
   6.784 +    apply (rule zcong_trans)
   6.785 +    apply (simp add: C_B_zcong_prod zcong_scalar2)
   6.786 +    done
   6.787 +  then have "[setprod id A = ((-1)^(card E) *
   6.788 +    (setprod id ((%x. x * a) ` A)))] (mod p)"
   6.789 +    by (simp add: B_def)
   6.790 +  then have "[setprod id A = ((-1)^(card E) * (setprod (%x. x * a) A))]
   6.791 +    (mod p)"
   6.792 +    by (simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric])
   6.793 +  moreover have "setprod (%x. x * a) A =
   6.794 +    setprod (%x. a) A * setprod id A"
   6.795 +    using finite_A by (induct set: Finites) auto
   6.796 +  ultimately have "[setprod id A = ((-1)^(card E) * (setprod (%x. a) A *
   6.797 +    setprod id A))] (mod p)"
   6.798 +    by simp
   6.799 +  then have "[setprod id A = ((-1)^(card E) * a^(card A) *
   6.800 +      setprod id A)](mod p)"
   6.801 +    apply (rule zcong_trans)
   6.802 +    apply (simp add: zcong_scalar2 zcong_scalar finite_A setprod_constant zmult_assoc)
   6.803 +    done
   6.804 +  then have a: "[setprod id A * (-1)^(card E) =
   6.805 +      ((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)"
   6.806 +    by (rule zcong_scalar)
   6.807 +  then have "[setprod id A * (-1)^(card E) = setprod id A *
   6.808 +      (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
   6.809 +    apply (rule zcong_trans)
   6.810 +    apply (simp add: a mult_commute mult_left_commute)
   6.811 +    done
   6.812 +  then have "[setprod id A * (-1)^(card E) = setprod id A *
   6.813 +      a^(card A)](mod p)"
   6.814 +    apply (rule zcong_trans)
   6.815 +    apply (simp add: aux)
   6.816 +    done
   6.817 +  with this zcong_cancel2 [of p "setprod id A" "-1 ^ card E" "a ^ card A"]
   6.818 +      p_g_0 A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)"
   6.819 +    by (simp add: order_less_imp_le)
   6.820 +  from this show ?thesis
   6.821 +    by (simp add: A_card_eq zcong_sym)
   6.822  qed
   6.823  
   6.824  theorem (in GAUSS) gauss_lemma: "(Legendre a p) = (-1) ^ (card E)"
   6.825  proof -
   6.826    from Euler_Criterion p_prime p_g_2 have
   6.827 -    "[(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)"
   6.828 +      "[(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)"
   6.829      by auto
   6.830    moreover note pre_gauss_lemma
   6.831    ultimately have "[(Legendre a p) = (-1) ^ (card E)] (mod p)"
     7.1 --- a/src/HOL/NumberTheory/Int2.thy	Thu Dec 08 12:50:03 2005 +0100
     7.2 +++ b/src/HOL/NumberTheory/Int2.thy	Thu Dec 08 12:50:04 2005 +0100
     7.3 @@ -5,14 +5,14 @@
     7.4  
     7.5  header {*Integers: Divisibility and Congruences*}
     7.6  
     7.7 -theory Int2 imports Finite2 WilsonRuss begin;
     7.8 +theory Int2 imports Finite2 WilsonRuss begin
     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  
    7.13  constdefs
    7.14    MultInv :: "int => int => int" 
    7.15 -  "MultInv p x == x ^ nat (p - 2)";
    7.16 +  "MultInv p x == x ^ nat (p - 2)"
    7.17  
    7.18  (*****************************************************************)
    7.19  (*                                                               *)
    7.20 @@ -20,69 +20,68 @@
    7.21  (*                                                               *)
    7.22  (*****************************************************************)
    7.23  
    7.24 -lemma zpower_zdvd_prop1 [rule_format]: "((0 < n) & (p dvd y)) --> 
    7.25 -    p dvd ((y::int) ^ n)";
    7.26 -  by (induct_tac n, auto simp add: zdvd_zmult zdvd_zmult2 [of p y])
    7.27 +lemma zpower_zdvd_prop1:
    7.28 +  "0 < n \<Longrightarrow> p dvd y \<Longrightarrow> p dvd ((y::int) ^ n)"
    7.29 +  by (induct n) (auto simp add: zdvd_zmult zdvd_zmult2 [of p y])
    7.30  
    7.31 -lemma zdvd_bounds: "n dvd m ==> (m \<le> (0::int) | n \<le> m)";
    7.32 -proof -;
    7.33 -  assume "n dvd m";
    7.34 -  then have "~(0 < m & m < n)";
    7.35 -    apply (insert zdvd_not_zless [of m n])
    7.36 -    by (rule contrapos_pn, auto)
    7.37 -  then have "(~0 < m | ~m < n)"  by auto
    7.38 +lemma zdvd_bounds: "n dvd m ==> m \<le> (0::int) | n \<le> m"
    7.39 +proof -
    7.40 +  assume "n dvd m"
    7.41 +  then have "~(0 < m & m < n)"
    7.42 +    using zdvd_not_zless [of m n] by auto
    7.43    then show ?thesis by auto
    7.44 -qed;
    7.45 -
    7.46 -lemma aux4: " -(m * n) = (-m) * (n::int)";
    7.47 -  by auto
    7.48 +qed
    7.49  
    7.50  lemma zprime_zdvd_zmult_better: "[| zprime p;  p dvd (m * n) |] ==> 
    7.51 -    (p dvd m) | (p dvd n)";
    7.52 -  apply (case_tac "0 \<le> m")
    7.53 +    (p dvd m) | (p dvd n)"
    7.54 +  apply (cases "0 \<le> m")
    7.55    apply (simp add: zprime_zdvd_zmult)
    7.56 -  by (insert zprime_zdvd_zmult [of "-m" p n], auto)
    7.57 +  apply (insert zprime_zdvd_zmult [of "-m" p n])
    7.58 +  apply auto
    7.59 +  done
    7.60  
    7.61 -lemma zpower_zdvd_prop2 [rule_format]: "zprime p --> p dvd ((y::int) ^ n) 
    7.62 -    --> 0 < n --> p dvd y";
    7.63 -  apply (induct_tac n, auto)
    7.64 -  apply (frule zprime_zdvd_zmult_better, auto)
    7.65 -done
    7.66 -
    7.67 -lemma stupid: "(0 :: int) \<le> y ==> x \<le> x + y";
    7.68 -  by arith
    7.69 +lemma zpower_zdvd_prop2:
    7.70 +    "zprime p \<Longrightarrow> p dvd ((y::int) ^ n) \<Longrightarrow> 0 < n \<Longrightarrow> p dvd y"
    7.71 +  apply (induct n)
    7.72 +   apply simp
    7.73 +  apply (frule zprime_zdvd_zmult_better)
    7.74 +   apply simp
    7.75 +  apply force
    7.76 +  done
    7.77  
    7.78 -lemma div_prop1: "[| 0 < z; (x::int) < y * z |] ==> x div z < y";
    7.79 -proof -;
    7.80 -  assume "0 < z";
    7.81 -  then have "(x div z) * z \<le> (x div z) * z + x mod z";
    7.82 -  apply (rule_tac x = "x div z * z" in stupid)
    7.83 -  by (simp add: pos_mod_sign)
    7.84 -  also have "... = x";
    7.85 -    by (auto simp add: zmod_zdiv_equality [THEN sym] zmult_ac)
    7.86 -  also assume  "x < y * z";
    7.87 -  finally show ?thesis;
    7.88 +lemma div_prop1: "[| 0 < z; (x::int) < y * z |] ==> x div z < y"
    7.89 +proof -
    7.90 +  assume "0 < z"
    7.91 +  then have "(x div z) * z \<le> (x div z) * z + x mod z"
    7.92 +    by arith
    7.93 +  also have "... = x"
    7.94 +    by (auto simp add: zmod_zdiv_equality [symmetric] zmult_ac)
    7.95 +  also assume  "x < y * z"
    7.96 +  finally show ?thesis
    7.97      by (auto simp add: prems mult_less_cancel_right, insert prems, arith)
    7.98 -qed;
    7.99 +qed
   7.100  
   7.101 -lemma div_prop2: "[| 0 < z; (x::int) < (y * z) + z |] ==> x div z \<le> y";
   7.102 -proof -;
   7.103 -  assume "0 < z" and "x < (y * z) + z";
   7.104 +lemma div_prop2: "[| 0 < z; (x::int) < (y * z) + z |] ==> x div z \<le> y"
   7.105 +proof -
   7.106 +  assume "0 < z" and "x < (y * z) + z"
   7.107    then have "x < (y + 1) * z" by (auto simp add: int_distrib)
   7.108 -  then have "x div z < y + 1";
   7.109 -    by (rule_tac y = "y + 1" in div_prop1, auto simp add: prems)
   7.110 +  then have "x div z < y + 1"
   7.111 +    apply -
   7.112 +    apply (rule_tac y = "y + 1" in div_prop1)
   7.113 +    apply (auto simp add: prems)
   7.114 +    done
   7.115    then show ?thesis by auto
   7.116 -qed;
   7.117 +qed
   7.118  
   7.119 -lemma zdiv_leq_prop: "[| 0 < y |] ==> y * (x div y) \<le> (x::int)";
   7.120 -proof-;
   7.121 -  assume "0 < y";
   7.122 +lemma zdiv_leq_prop: "[| 0 < y |] ==> y * (x div y) \<le> (x::int)"
   7.123 +proof-
   7.124 +  assume "0 < y"
   7.125    from zmod_zdiv_equality have "x = y * (x div y) + x mod y" by auto
   7.126 -  moreover have "0 \<le> x mod y";
   7.127 +  moreover have "0 \<le> x mod y"
   7.128      by (auto simp add: prems pos_mod_sign)
   7.129 -  ultimately show ?thesis;
   7.130 +  ultimately show ?thesis
   7.131      by arith
   7.132 -qed;
   7.133 +qed
   7.134  
   7.135  (*****************************************************************)
   7.136  (*                                                               *)
   7.137 @@ -90,96 +89,102 @@
   7.138  (*                                                               *)
   7.139  (*****************************************************************)
   7.140  
   7.141 -lemma zcong_eq_zdvd_prop: "[x = 0](mod p) = (p dvd x)";
   7.142 +lemma zcong_eq_zdvd_prop: "[x = 0](mod p) = (p dvd x)"
   7.143    by (auto simp add: zcong_def)
   7.144  
   7.145 -lemma zcong_id: "[m = 0] (mod m)";
   7.146 +lemma zcong_id: "[m = 0] (mod m)"
   7.147    by (auto simp add: zcong_def zdvd_0_right)
   7.148  
   7.149 -lemma zcong_shift: "[a = b] (mod m) ==> [a + c = b + c] (mod m)";
   7.150 +lemma zcong_shift: "[a = b] (mod m) ==> [a + c = b + c] (mod m)"
   7.151    by (auto simp add: zcong_refl zcong_zadd)
   7.152  
   7.153 -lemma zcong_zpower: "[x = y](mod m) ==> [x^z = y^z](mod m)";
   7.154 -  by (induct_tac z, auto simp add: zcong_zmult)
   7.155 +lemma zcong_zpower: "[x = y](mod m) ==> [x^z = y^z](mod m)"
   7.156 +  by (induct z) (auto simp add: zcong_zmult)
   7.157  
   7.158  lemma zcong_eq_trans: "[| [a = b](mod m); b = c; [c = d](mod m) |] ==> 
   7.159 -    [a = d](mod m)";
   7.160 -  by (auto, rule_tac b = c in zcong_trans)
   7.161 +    [a = d](mod m)"
   7.162 +  apply (erule zcong_trans)
   7.163 +  apply simp
   7.164 +  done
   7.165  
   7.166 -lemma aux1: "a - b = (c::int) ==> a = c + b";
   7.167 +lemma aux1: "a - b = (c::int) ==> a = c + b"
   7.168    by auto
   7.169  
   7.170  lemma zcong_zmult_prop1: "[a = b](mod m) ==> ([c = a * d](mod m) = 
   7.171 -    [c = b * d] (mod m))";
   7.172 +    [c = b * d] (mod m))"
   7.173    apply (auto simp add: zcong_def dvd_def)
   7.174    apply (rule_tac x = "ka + k * d" in exI)
   7.175 -  apply (drule aux1)+;
   7.176 +  apply (drule aux1)+
   7.177    apply (auto simp add: int_distrib)
   7.178    apply (rule_tac x = "ka - k * d" in exI)
   7.179 -  apply (drule aux1)+;
   7.180 +  apply (drule aux1)+
   7.181    apply (auto simp add: int_distrib)
   7.182 -done
   7.183 +  done
   7.184  
   7.185  lemma zcong_zmult_prop2: "[a = b](mod m) ==> 
   7.186 -    ([c = d * a](mod m) = [c = d * b] (mod m))";
   7.187 +    ([c = d * a](mod m) = [c = d * b] (mod m))"
   7.188    by (auto simp add: zmult_ac zcong_zmult_prop1)
   7.189  
   7.190  lemma zcong_zmult_prop3: "[| zprime p; ~[x = 0] (mod p); 
   7.191 -    ~[y = 0] (mod p) |] ==> ~[x * y = 0] (mod p)";
   7.192 +    ~[y = 0] (mod p) |] ==> ~[x * y = 0] (mod p)"
   7.193    apply (auto simp add: zcong_def)
   7.194    apply (drule zprime_zdvd_zmult_better, auto)
   7.195 -done
   7.196 +  done
   7.197  
   7.198  lemma zcong_less_eq: "[| 0 < x; 0 < y; 0 < m; [x = y] (mod m); 
   7.199 -    x < m; y < m |] ==> x = y";
   7.200 +    x < m; y < m |] ==> x = y"
   7.201    apply (simp add: zcong_zmod_eq)
   7.202 -  apply (subgoal_tac "(x mod m) = x");
   7.203 -  apply (subgoal_tac "(y mod m) = y");
   7.204 +  apply (subgoal_tac "(x mod m) = x")
   7.205 +  apply (subgoal_tac "(y mod m) = y")
   7.206    apply simp
   7.207    apply (rule_tac [1-2] mod_pos_pos_trivial)
   7.208 -by auto
   7.209 +  apply auto
   7.210 +  done
   7.211  
   7.212  lemma zcong_neg_1_impl_ne_1: "[| 2 < p; [x = -1] (mod p) |] ==> 
   7.213 -    ~([x = 1] (mod p))";
   7.214 -proof;
   7.215 +    ~([x = 1] (mod p))"
   7.216 +proof
   7.217    assume "2 < p" and "[x = 1] (mod p)" and "[x = -1] (mod p)"
   7.218 -  then have "[1 = -1] (mod p)";
   7.219 +  then have "[1 = -1] (mod p)"
   7.220      apply (auto simp add: zcong_sym)
   7.221      apply (drule zcong_trans, auto)
   7.222 -  done
   7.223 -  then have "[1 + 1 = -1 + 1] (mod p)";
   7.224 +    done
   7.225 +  then have "[1 + 1 = -1 + 1] (mod p)"
   7.226      by (simp only: zcong_shift)
   7.227 -  then have "[2 = 0] (mod p)";
   7.228 +  then have "[2 = 0] (mod p)"
   7.229      by auto
   7.230 -  then have "p dvd 2";
   7.231 +  then have "p dvd 2"
   7.232      by (auto simp add: dvd_def zcong_def)
   7.233 -  with prems show False;
   7.234 +  with prems show False
   7.235      by (auto simp add: zdvd_not_zless)
   7.236 -qed;
   7.237 +qed
   7.238  
   7.239 -lemma zcong_zero_equiv_div: "[a = 0] (mod m) = (m dvd a)";
   7.240 +lemma zcong_zero_equiv_div: "[a = 0] (mod m) = (m dvd a)"
   7.241    by (auto simp add: zcong_def)
   7.242  
   7.243  lemma zcong_zprime_prod_zero: "[| zprime p; 0 < a |] ==> 
   7.244 -  [a * b = 0] (mod p) ==> [a = 0] (mod p) | [b = 0] (mod p)"; 
   7.245 +    [a * b = 0] (mod p) ==> [a = 0] (mod p) | [b = 0] (mod p)" 
   7.246    by (auto simp add: zcong_zero_equiv_div zprime_zdvd_zmult)
   7.247  
   7.248  lemma zcong_zprime_prod_zero_contra: "[| zprime p; 0 < a |] ==>
   7.249 -  ~[a = 0](mod p) & ~[b = 0](mod p) ==> ~[a * b = 0] (mod p)";
   7.250 +  ~[a = 0](mod p) & ~[b = 0](mod p) ==> ~[a * b = 0] (mod p)"
   7.251    apply auto 
   7.252    apply (frule_tac a = a and b = b and p = p in zcong_zprime_prod_zero)
   7.253 -by auto
   7.254 +  apply auto
   7.255 +  done
   7.256  
   7.257 -lemma zcong_not_zero: "[| 0 < x; x < m |] ==> ~[x = 0] (mod m)"; 
   7.258 +lemma zcong_not_zero: "[| 0 < x; x < m |] ==> ~[x = 0] (mod m)" 
   7.259    by (auto simp add: zcong_zero_equiv_div zdvd_not_zless)
   7.260  
   7.261 -lemma zcong_zero: "[| 0 \<le> x; x < m; [x = 0](mod m) |] ==> x = 0";
   7.262 +lemma zcong_zero: "[| 0 \<le> x; x < m; [x = 0](mod m) |] ==> x = 0"
   7.263    apply (drule order_le_imp_less_or_eq, auto)
   7.264 -by (frule_tac m = m in zcong_not_zero, auto)
   7.265 +  apply (frule_tac m = m in zcong_not_zero)
   7.266 +  apply auto
   7.267 +  done
   7.268  
   7.269  lemma all_relprime_prod_relprime: "[| finite A; \<forall>x \<in> A. (zgcd(x,y) = 1) |]
   7.270 -    ==> zgcd (setprod id A,y) = 1";
   7.271 -  by (induct set: Finites, auto simp add: zgcd_zgcd_zmult)
   7.272 +    ==> zgcd (setprod id A,y) = 1"
   7.273 +  by (induct set: Finites) (auto simp add: zgcd_zgcd_zmult)
   7.274  
   7.275  (*****************************************************************)
   7.276  (*                                                               *)
   7.277 @@ -188,69 +193,69 @@
   7.278  (*****************************************************************)
   7.279  
   7.280  lemma MultInv_prop1: "[| 2 < p; [x = y] (mod p) |] ==> 
   7.281 -    [(MultInv p x) = (MultInv p y)] (mod p)";
   7.282 +    [(MultInv p x) = (MultInv p y)] (mod p)"
   7.283    by (auto simp add: MultInv_def zcong_zpower)
   7.284  
   7.285  lemma MultInv_prop2: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> 
   7.286 -  [(x * (MultInv p x)) = 1] (mod p)";
   7.287 -proof (simp add: MultInv_def zcong_eq_zdvd_prop);
   7.288 -  assume "2 < p" and "zprime p" and "~ p dvd x";
   7.289 -  have "x * x ^ nat (p - 2) = x ^ (nat (p - 2) + 1)";
   7.290 +  [(x * (MultInv p x)) = 1] (mod p)"
   7.291 +proof (simp add: MultInv_def zcong_eq_zdvd_prop)
   7.292 +  assume "2 < p" and "zprime p" and "~ p dvd x"
   7.293 +  have "x * x ^ nat (p - 2) = x ^ (nat (p - 2) + 1)"
   7.294      by auto
   7.295 -  also from prems have "nat (p - 2) + 1 = nat (p - 2 + 1)";
   7.296 +  also from prems have "nat (p - 2) + 1 = nat (p - 2 + 1)"
   7.297      by (simp only: nat_add_distrib, auto)
   7.298    also have "p - 2 + 1 = p - 1" by arith
   7.299 -  finally have "[x * x ^ nat (p - 2) = x ^ nat (p - 1)] (mod p)";
   7.300 +  finally have "[x * x ^ nat (p - 2) = x ^ nat (p - 1)] (mod p)"
   7.301      by (rule ssubst, auto)
   7.302 -  also from prems have "[x ^ nat (p - 1) = 1] (mod p)";
   7.303 +  also from prems have "[x ^ nat (p - 1) = 1] (mod p)"
   7.304      by (auto simp add: Little_Fermat) 
   7.305 -  finally (zcong_trans) show "[x * x ^ nat (p - 2) = 1] (mod p)";.;
   7.306 -qed;
   7.307 +  finally (zcong_trans) show "[x * x ^ nat (p - 2) = 1] (mod p)" .
   7.308 +qed
   7.309  
   7.310  lemma MultInv_prop2a: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> 
   7.311 -    [(MultInv p x) * x = 1] (mod p)";
   7.312 +    [(MultInv p x) * x = 1] (mod p)"
   7.313    by (auto simp add: MultInv_prop2 zmult_ac)
   7.314  
   7.315 -lemma aux_1: "2 < p ==> ((nat p) - 2) = (nat (p - 2))";
   7.316 +lemma aux_1: "2 < p ==> ((nat p) - 2) = (nat (p - 2))"
   7.317    by (simp add: nat_diff_distrib)
   7.318  
   7.319 -lemma aux_2: "2 < p ==> 0 < nat (p - 2)";
   7.320 +lemma aux_2: "2 < p ==> 0 < nat (p - 2)"
   7.321    by auto
   7.322  
   7.323  lemma MultInv_prop3: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> 
   7.324 -    ~([MultInv p x = 0](mod p))";
   7.325 +    ~([MultInv p x = 0](mod p))"
   7.326    apply (auto simp add: MultInv_def zcong_eq_zdvd_prop aux_1)
   7.327    apply (drule aux_2)
   7.328    apply (drule zpower_zdvd_prop2, auto)
   7.329 -done
   7.330 +  done
   7.331  
   7.332  lemma aux__1: "[| 2 < p; zprime p; ~([x = 0](mod p))|] ==> 
   7.333      [(MultInv p (MultInv p x)) = (x * (MultInv p x) * 
   7.334 -      (MultInv p (MultInv p x)))] (mod p)";
   7.335 +      (MultInv p (MultInv p x)))] (mod p)"
   7.336    apply (drule MultInv_prop2, auto)
   7.337 -  apply (drule_tac k = "MultInv p (MultInv p x)" in zcong_scalar, auto);
   7.338 +  apply (drule_tac k = "MultInv p (MultInv p x)" in zcong_scalar, auto)
   7.339    apply (auto simp add: zcong_sym)
   7.340 -done
   7.341 +  done
   7.342  
   7.343  lemma aux__2: "[| 2 < p; zprime p; ~([x = 0](mod p))|] ==>
   7.344 -    [(x * (MultInv p x) * (MultInv p (MultInv p x))) = x] (mod p)";
   7.345 +    [(x * (MultInv p x) * (MultInv p (MultInv p x))) = x] (mod p)"
   7.346    apply (frule MultInv_prop3, auto)
   7.347    apply (insert MultInv_prop2 [of p "MultInv p x"], auto)
   7.348    apply (drule MultInv_prop2, auto)
   7.349    apply (drule_tac k = x in zcong_scalar2, auto)
   7.350    apply (auto simp add: zmult_ac)
   7.351 -done
   7.352 +  done
   7.353  
   7.354  lemma MultInv_prop4: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> 
   7.355 -    [(MultInv p (MultInv p x)) = x] (mod p)";
   7.356 +    [(MultInv p (MultInv p x)) = x] (mod p)"
   7.357    apply (frule aux__1, auto)
   7.358    apply (drule aux__2, auto)
   7.359    apply (drule zcong_trans, auto)
   7.360 -done
   7.361 +  done
   7.362  
   7.363  lemma MultInv_prop5: "[| 2 < p; zprime p; ~([x = 0](mod p)); 
   7.364      ~([y = 0](mod p)); [(MultInv p x) = (MultInv p y)] (mod p) |] ==> 
   7.365 -    [x = y] (mod p)";
   7.366 +    [x = y] (mod p)"
   7.367    apply (drule_tac a = "MultInv p x" and b = "MultInv p y" and 
   7.368      m = p and k = x in zcong_scalar)
   7.369    apply (insert MultInv_prop2 [of p x], simp)
   7.370 @@ -261,38 +266,38 @@
   7.371    apply (insert MultInv_prop2a [of p y], auto simp add: zmult_ac)
   7.372    apply (insert zcong_zmult_prop2 [of "y * MultInv p y" 1 p y x])
   7.373    apply (auto simp add: zcong_sym)
   7.374 -done
   7.375 +  done
   7.376  
   7.377  lemma MultInv_zcong_prop1: "[| 2 < p; [j = k] (mod p) |] ==> 
   7.378 -    [a * MultInv p j = a * MultInv p k] (mod p)";
   7.379 +    [a * MultInv p j = a * MultInv p k] (mod p)"
   7.380    by (drule MultInv_prop1, auto simp add: zcong_scalar2)
   7.381  
   7.382  lemma aux___1: "[j = a * MultInv p k] (mod p) ==> 
   7.383 -    [j * k = a * MultInv p k * k] (mod p)";
   7.384 +    [j * k = a * MultInv p k * k] (mod p)"
   7.385    by (auto simp add: zcong_scalar)
   7.386  
   7.387  lemma aux___2: "[|2 < p; zprime p; ~([k = 0](mod p)); 
   7.388 -    [j * k = a * MultInv p k * k] (mod p) |] ==> [j * k = a] (mod p)";
   7.389 +    [j * k = a * MultInv p k * k] (mod p) |] ==> [j * k = a] (mod p)"
   7.390    apply (insert MultInv_prop2a [of p k] zcong_zmult_prop2 
   7.391      [of "MultInv p k * k" 1 p "j * k" a])
   7.392    apply (auto simp add: zmult_ac)
   7.393 -done
   7.394 +  done
   7.395  
   7.396  lemma aux___3: "[j * k = a] (mod p) ==> [(MultInv p j) * j * k = 
   7.397 -     (MultInv p j) * a] (mod p)";
   7.398 +     (MultInv p j) * a] (mod p)"
   7.399    by (auto simp add: zmult_assoc zcong_scalar2)
   7.400  
   7.401  lemma aux___4: "[|2 < p; zprime p; ~([j = 0](mod p)); 
   7.402      [(MultInv p j) * j * k = (MultInv p j) * a] (mod p) |]
   7.403 -       ==> [k = a * (MultInv p j)] (mod p)";
   7.404 +       ==> [k = a * (MultInv p j)] (mod p)"
   7.405    apply (insert MultInv_prop2a [of p j] zcong_zmult_prop1 
   7.406      [of "MultInv p j * j" 1 p "MultInv p j * a" k])
   7.407    apply (auto simp add: zmult_ac zcong_sym)
   7.408 -done
   7.409 +  done
   7.410  
   7.411  lemma MultInv_zcong_prop2: "[| 2 < p; zprime p; ~([k = 0](mod p)); 
   7.412      ~([j = 0](mod p)); [j = a * MultInv p k] (mod p) |] ==> 
   7.413 -    [k = a * MultInv p j] (mod p)";
   7.414 +    [k = a * MultInv p j] (mod p)"
   7.415    apply (drule aux___1)
   7.416    apply (frule aux___2, auto)
   7.417    by (drule aux___3, drule aux___4, auto)
   7.418 @@ -300,11 +305,11 @@
   7.419  lemma MultInv_zcong_prop3: "[| 2 < p; zprime p; ~([a = 0](mod p)); 
   7.420      ~([k = 0](mod p)); ~([j = 0](mod p));
   7.421      [a * MultInv p j = a * MultInv p k] (mod p) |] ==> 
   7.422 -      [j = k] (mod p)";
   7.423 +      [j = k] (mod p)"
   7.424    apply (auto simp add: zcong_eq_zdvd_prop [of a p])
   7.425    apply (frule zprime_imp_zrelprime, auto)
   7.426    apply (insert zcong_cancel2 [of p a "MultInv p j" "MultInv p k"], auto)
   7.427    apply (drule MultInv_prop5, auto)
   7.428 -done
   7.429 +  done
   7.430  
   7.431  end
     8.1 --- a/src/HOL/NumberTheory/IntFact.thy	Thu Dec 08 12:50:03 2005 +0100
     8.2 +++ b/src/HOL/NumberTheory/IntFact.thy	Thu Dec 08 12:50:04 2005 +0100
     8.3 @@ -36,41 +36,36 @@
     8.4  
     8.5  
     8.6  lemma d22set_induct:
     8.7 -  "(!!a. P {} a) ==>
     8.8 -    (!!a. 1 < (a::int) ==> P (d22set (a - 1)) (a - 1)
     8.9 -      ==> P (d22set a) a)
    8.10 -    ==> P (d22set u) u"
    8.11 -proof -
    8.12 -  case rule_context
    8.13 -  show ?thesis
    8.14 -    apply (rule d22set.induct)
    8.15 -    apply safe
    8.16 -     apply (case_tac [2] "1 < a")
    8.17 -      apply (rule_tac [2] rule_context)
    8.18 -       apply (simp_all (no_asm_simp))
    8.19 -     apply (simp_all (no_asm_simp) add: d22set.simps rule_context)
    8.20 -    done
    8.21 -qed
    8.22 +  assumes "!!a. P {} a"
    8.23 +    and "!!a. 1 < (a::int) ==> P (d22set (a - 1)) (a - 1) ==> P (d22set a) a"
    8.24 +  shows "P (d22set u) u"
    8.25 +  apply (rule d22set.induct)
    8.26 +  apply safe
    8.27 +   prefer 2
    8.28 +   apply (case_tac "1 < a")
    8.29 +    apply (rule_tac prems)
    8.30 +     apply (simp_all (no_asm_simp))
    8.31 +   apply (simp_all (no_asm_simp) add: d22set.simps prems)
    8.32 +  done
    8.33  
    8.34  lemma d22set_g_1 [rule_format]: "b \<in> d22set a --> 1 < b"
    8.35    apply (induct a rule: d22set_induct)
    8.36 -   prefer 2
    8.37 -   apply (subst d22set.simps)
    8.38 -   apply auto
    8.39 +   apply simp
    8.40 +  apply (subst d22set.simps)
    8.41 +  apply auto
    8.42    done
    8.43  
    8.44  lemma d22set_le [rule_format]: "b \<in> d22set a --> b \<le> a"
    8.45    apply (induct a rule: d22set_induct)
    8.46 -   prefer 2
    8.47 +  apply simp
    8.48     apply (subst d22set.simps)
    8.49     apply auto
    8.50    done
    8.51  
    8.52  lemma d22set_le_swap: "a < b ==> b \<notin> d22set a"
    8.53 -  apply (auto dest: d22set_le)
    8.54 -  done
    8.55 +  by (auto dest: d22set_le)
    8.56  
    8.57 -lemma d22set_mem [rule_format]: "1 < b --> b \<le> a --> b \<in> d22set a"
    8.58 +lemma d22set_mem: "1 < b \<Longrightarrow> b \<le> a \<Longrightarrow> b \<in> d22set a"
    8.59    apply (induct a rule: d22set.induct)
    8.60    apply auto
    8.61     apply (simp_all add: d22set.simps)
     9.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Thu Dec 08 12:50:03 2005 +0100
     9.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Thu Dec 08 12:50:04 2005 +0100
     9.3 @@ -2,11 +2,6 @@
     9.4      ID:         $Id$
     9.5      Author:     Thomas M. Rasmussen
     9.6      Copyright   2000  University of Cambridge
     9.7 -
     9.8 -Changes by Jeremy Avigad, 2003/02/21:
     9.9 -   Repaired definition of zprime_def, added "0 <= m &"
    9.10 -   Added lemma zgcd_geq_zero
    9.11 -   Repaired proof of zprime_imp_zrelprime
    9.12  *)
    9.13  
    9.14  header {* Divisibility and prime numbers (on integers) *}
    10.1 --- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Thu Dec 08 12:50:03 2005 +0100
    10.2 +++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Thu Dec 08 12:50:04 2005 +0100
    10.3 @@ -16,12 +16,12 @@
    10.4  (*                                                             *)
    10.5  (***************************************************************)
    10.6  
    10.7 -lemma (in GAUSS) QRLemma1: "a * setsum id A = 
    10.8 +lemma (in GAUSS) QRLemma1: "a * setsum id A =
    10.9    p * setsum (%x. ((x * a) div p)) A + setsum id D + setsum id E"
   10.10  proof -
   10.11 -  from finite_A have "a * setsum id A = setsum (%x. a * x) A" 
   10.12 +  from finite_A have "a * setsum id A = setsum (%x. a * x) A"
   10.13      by (auto simp add: setsum_const_mult id_def)
   10.14 -  also have "setsum (%x. a * x) = setsum (%x. x * a)" 
   10.15 +  also have "setsum (%x. a * x) = setsum (%x. x * a)"
   10.16      by (auto simp add: zmult_commute)
   10.17    also have "setsum (%x. x * a) A = setsum id B"
   10.18      by (simp add: B_def setsum_reindex_id[OF inj_on_xa_A])
   10.19 @@ -34,28 +34,26 @@
   10.20    also from C_eq have "... = setsum id (D \<union> E)"
   10.21      by auto
   10.22    also from finite_D finite_E have "... = setsum id D + setsum id E"
   10.23 -    apply (rule setsum_Un_disjoint)
   10.24 -    by (auto simp add: D_def E_def)
   10.25 -  also have "setsum (%x. p * (x div p)) B = 
   10.26 +    by (rule setsum_Un_disjoint) (auto simp add: D_def E_def)
   10.27 +  also have "setsum (%x. p * (x div p)) B =
   10.28        setsum ((%x. p * (x div p)) o (%x. (x * a))) A"
   10.29      by (auto simp add: B_def setsum_reindex inj_on_xa_A)
   10.30    also have "... = setsum (%x. p * ((x * a) div p)) A"
   10.31      by (auto simp add: o_def)
   10.32 -  also from finite_A have "setsum (%x. p * ((x * a) div p)) A = 
   10.33 +  also from finite_A have "setsum (%x. p * ((x * a) div p)) A =
   10.34      p * setsum (%x. ((x * a) div p)) A"
   10.35      by (auto simp add: setsum_const_mult)
   10.36    finally show ?thesis by arith
   10.37  qed
   10.38  
   10.39 -lemma (in GAUSS) QRLemma2: "setsum id A = p * int (card E) - setsum id E + 
   10.40 -  setsum id D" 
   10.41 +lemma (in GAUSS) QRLemma2: "setsum id A = p * int (card E) - setsum id E +
   10.42 +  setsum id D"
   10.43  proof -
   10.44    from F_Un_D_eq_A have "setsum id A = setsum id (D \<union> F)"
   10.45      by (simp add: Un_commute)
   10.46 -  also from F_D_disj finite_D finite_F have 
   10.47 -      "... = setsum id D + setsum id F"
   10.48 -    apply (simp add: Int_commute)
   10.49 -    by (intro setsum_Un_disjoint) 
   10.50 +  also from F_D_disj finite_D finite_F
   10.51 +  have "... = setsum id D + setsum id F"
   10.52 +    by (auto simp add: Int_commute intro: setsum_Un_disjoint)
   10.53    also from F_def have "F = (%x. (p - x)) ` E"
   10.54      by auto
   10.55    also from finite_E inj_on_pminusx_E have "setsum id ((%x. (p - x)) ` E) =
   10.56 @@ -69,30 +67,30 @@
   10.57      by arith
   10.58  qed
   10.59  
   10.60 -lemma (in GAUSS) QRLemma3: "(a - 1) * setsum id A = 
   10.61 +lemma (in GAUSS) QRLemma3: "(a - 1) * setsum id A =
   10.62      p * (setsum (%x. ((x * a) div p)) A - int(card E)) + 2 * setsum id E"
   10.63  proof -
   10.64    have "(a - 1) * setsum id A = a * setsum id A - setsum id A"
   10.65 -    by (auto simp add: zdiff_zmult_distrib)  
   10.66 +    by (auto simp add: zdiff_zmult_distrib)
   10.67    also note QRLemma1
   10.68 -  also from QRLemma2 have "p * (\<Sum>x \<in> A. x * a div p) + setsum id D + 
   10.69 -     setsum id E - setsum id A = 
   10.70 -      p * (\<Sum>x \<in> A. x * a div p) + setsum id D + 
   10.71 +  also from QRLemma2 have "p * (\<Sum>x \<in> A. x * a div p) + setsum id D +
   10.72 +     setsum id E - setsum id A =
   10.73 +      p * (\<Sum>x \<in> A. x * a div p) + setsum id D +
   10.74        setsum id E - (p * int (card E) - setsum id E + setsum id D)"
   10.75      by auto
   10.76 -  also have "... = p * (\<Sum>x \<in> A. x * a div p) - 
   10.77 -      p * int (card E) + 2 * setsum id E" 
   10.78 +  also have "... = p * (\<Sum>x \<in> A. x * a div p) -
   10.79 +      p * int (card E) + 2 * setsum id E"
   10.80      by arith
   10.81    finally show ?thesis
   10.82      by (auto simp only: zdiff_zmult_distrib2)
   10.83  qed
   10.84  
   10.85 -lemma (in GAUSS) QRLemma4: "a \<in> zOdd ==> 
   10.86 +lemma (in GAUSS) QRLemma4: "a \<in> zOdd ==>
   10.87      (setsum (%x. ((x * a) div p)) A \<in> zEven) = (int(card E): zEven)"
   10.88  proof -
   10.89    assume a_odd: "a \<in> zOdd"
   10.90    from QRLemma3 have a: "p * (setsum (%x. ((x * a) div p)) A - int(card E)) =
   10.91 -      (a - 1) * setsum id A - 2 * setsum id E" 
   10.92 +      (a - 1) * setsum id A - 2 * setsum id E"
   10.93      by arith
   10.94    from a_odd have "a - 1 \<in> zEven"
   10.95      by (rule odd_minus_one_even)
   10.96 @@ -109,10 +107,10 @@
   10.97    with p_odd have "(setsum (%x. ((x * a) div p)) A - int(card E)): zEven"
   10.98      by (auto simp add: odd_iff_not_even)
   10.99    thus ?thesis
  10.100 -    by (auto simp only: even_diff [THEN sym])
  10.101 +    by (auto simp only: even_diff [symmetric])
  10.102  qed
  10.103  
  10.104 -lemma (in GAUSS) QRLemma5: "a \<in> zOdd ==> 
  10.105 +lemma (in GAUSS) QRLemma5: "a \<in> zOdd ==>
  10.106     (-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))"
  10.107  proof -
  10.108    assume "a \<in> zOdd"
  10.109 @@ -130,7 +128,7 @@
  10.110            by (auto simp add: A_def)
  10.111          with a_nonzero have "0 \<le> x * a"
  10.112            by (auto simp add: zero_le_mult_iff)
  10.113 -        with p_g_2 show "0 \<le> x * a div p" 
  10.114 +        with p_g_2 show "0 \<le> x * a div p"
  10.115            by (auto simp add: pos_imp_zdiv_nonneg_iff)
  10.116        qed
  10.117      qed
  10.118 @@ -143,12 +141,13 @@
  10.119  qed
  10.120  
  10.121  lemma MainQRLemma: "[| a \<in> zOdd; 0 < a; ~([a = 0] (mod p)); zprime p; 2 < p;
  10.122 -  A = {x. 0 < x & x \<le> (p - 1) div 2} |] ==> 
  10.123 +  A = {x. 0 < x & x \<le> (p - 1) div 2} |] ==>
  10.124    (Legendre a p) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))"
  10.125    apply (subst GAUSS.gauss_lemma)
  10.126    apply (auto simp add: GAUSS_def)
  10.127    apply (subst GAUSS.QRLemma5)
  10.128 -by (auto simp add: GAUSS_def)
  10.129 +  apply (auto simp add: GAUSS_def)
  10.130 +  done
  10.131  
  10.132  (******************************************************************)
  10.133  (*                                                                *)
  10.134 @@ -178,9 +177,9 @@
  10.135    defines S_def:     "S     == P_set <*> Q_set"
  10.136    defines S1_def:    "S1    == { (x, y). (x, y):S & ((p * y) < (q * x)) }"
  10.137    defines S2_def:    "S2    == { (x, y). (x, y):S & ((q * x) < (p * y)) }"
  10.138 -  defines f1_def:    "f1 j  == { (j1, y). (j1, y):S & j1 = j & 
  10.139 +  defines f1_def:    "f1 j  == { (j1, y). (j1, y):S & j1 = j &
  10.140                                   (y \<le> (q * j) div p) }"
  10.141 -  defines f2_def:    "f2 j  == { (x, j1). (x, j1):S & j1 = j & 
  10.142 +  defines f2_def:    "f2 j  == { (x, j1). (x, j1):S & j1 = j &
  10.143                                   (x \<le> (p * j) div q) }"
  10.144  
  10.145  lemma (in QRTEMP) p_fact: "0 < (p - 1) div 2"
  10.146 @@ -199,7 +198,7 @@
  10.147    then show ?thesis by auto
  10.148  qed
  10.149  
  10.150 -lemma (in QRTEMP) pb_neq_qa: "[|1 \<le> b; b \<le> (q - 1) div 2 |] ==> 
  10.151 +lemma (in QRTEMP) pb_neq_qa: "[|1 \<le> b; b \<le> (q - 1) div 2 |] ==>
  10.152      (p * b \<noteq> q * a)"
  10.153  proof
  10.154    assume "p * b = q * a" and "1 \<le> b" and "b \<le> (q - 1) div 2"
  10.155 @@ -212,10 +211,11 @@
  10.156      with p_prime have "q = 1 | q = p"
  10.157        apply (auto simp add: zprime_def QRTEMP_def)
  10.158        apply (drule_tac x = q and R = False in allE)
  10.159 -      apply (simp add: QRTEMP_def)    
  10.160 +      apply (simp add: QRTEMP_def)
  10.161        apply (subgoal_tac "0 \<le> q", simp add: QRTEMP_def)
  10.162        apply (insert prems)
  10.163 -    by (auto simp add: QRTEMP_def)
  10.164 +      apply (auto simp add: QRTEMP_def)
  10.165 +      done
  10.166      with q_g_2 p_neq_q show False by auto
  10.167    qed
  10.168    ultimately have "q dvd b" by auto
  10.169 @@ -223,7 +223,7 @@
  10.170    proof -
  10.171      assume "q dvd b"
  10.172      moreover from prems have "0 < b" by auto
  10.173 -    ultimately show ?thesis by (insert zdvd_bounds [of q b], auto)
  10.174 +    ultimately show ?thesis using zdvd_bounds [of q b] by auto
  10.175    qed
  10.176    with prems have "q \<le> (q - 1) div 2" by auto
  10.177    then have "2 * q \<le> 2 * ((q - 1) div 2)" by arith
  10.178 @@ -240,10 +240,10 @@
  10.179  qed
  10.180  
  10.181  lemma (in QRTEMP) P_set_finite: "finite (P_set)"
  10.182 -  by (insert p_fact, auto simp add: P_set_def bdd_int_set_l_le_finite)
  10.183 +  using p_fact by (auto simp add: P_set_def bdd_int_set_l_le_finite)
  10.184  
  10.185  lemma (in QRTEMP) Q_set_finite: "finite (Q_set)"
  10.186 -  by (insert q_fact, auto simp add: Q_set_def bdd_int_set_l_le_finite)
  10.187 +  using q_fact by (auto simp add: Q_set_def bdd_int_set_l_le_finite)
  10.188  
  10.189  lemma (in QRTEMP) S_finite: "finite S"
  10.190    by (auto simp add: S_def  P_set_finite Q_set_finite finite_cartesian_product)
  10.191 @@ -263,43 +263,42 @@
  10.192  qed
  10.193  
  10.194  lemma (in QRTEMP) P_set_card: "(p - 1) div 2 = int (card (P_set))"
  10.195 -  by (insert p_fact, auto simp add: P_set_def card_bdd_int_set_l_le)
  10.196 +  using p_fact by (auto simp add: P_set_def card_bdd_int_set_l_le)
  10.197  
  10.198  lemma (in QRTEMP) Q_set_card: "(q - 1) div 2 = int (card (Q_set))"
  10.199 -  by (insert q_fact, auto simp add: Q_set_def card_bdd_int_set_l_le)
  10.200 +  using q_fact by (auto simp add: Q_set_def card_bdd_int_set_l_le)
  10.201  
  10.202  lemma (in QRTEMP) S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))"
  10.203 -  apply (insert P_set_card Q_set_card P_set_finite Q_set_finite)
  10.204 -  apply (auto simp add: S_def zmult_int setsum_constant)
  10.205 -done
  10.206 +  using P_set_card Q_set_card P_set_finite Q_set_finite
  10.207 +  by (auto simp add: S_def zmult_int setsum_constant)
  10.208  
  10.209  lemma (in QRTEMP) S1_Int_S2_prop: "S1 \<inter> S2 = {}"
  10.210    by (auto simp add: S1_def S2_def)
  10.211  
  10.212  lemma (in QRTEMP) S1_Union_S2_prop: "S = S1 \<union> S2"
  10.213    apply (auto simp add: S_def P_set_def Q_set_def S1_def S2_def)
  10.214 -  proof -
  10.215 -    fix a and b
  10.216 -    assume "~ q * a < p * b" and b1: "0 < b" and b2: "b \<le> (q - 1) div 2"
  10.217 -    with zless_linear have "(p * b < q * a) | (p * b = q * a)" by auto
  10.218 -    moreover from pb_neq_qa b1 b2 have "(p * b \<noteq> q * a)" by auto
  10.219 -    ultimately show "p * b < q * a" by auto
  10.220 -  qed
  10.221 +proof -
  10.222 +  fix a and b
  10.223 +  assume "~ q * a < p * b" and b1: "0 < b" and b2: "b \<le> (q - 1) div 2"
  10.224 +  with zless_linear have "(p * b < q * a) | (p * b = q * a)" by auto
  10.225 +  moreover from pb_neq_qa b1 b2 have "(p * b \<noteq> q * a)" by auto
  10.226 +  ultimately show "p * b < q * a" by auto
  10.227 +qed
  10.228  
  10.229 -lemma (in QRTEMP) card_sum_S1_S2: "((p - 1) div 2) * ((q - 1) div 2) = 
  10.230 +lemma (in QRTEMP) card_sum_S1_S2: "((p - 1) div 2) * ((q - 1) div 2) =
  10.231      int(card(S1)) + int(card(S2))"
  10.232 -proof-
  10.233 +proof -
  10.234    have "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))"
  10.235      by (auto simp add: S_card)
  10.236    also have "... = int( card(S1) + card(S2))"
  10.237      apply (insert S1_finite S2_finite S1_Int_S2_prop S1_Union_S2_prop)
  10.238      apply (drule card_Un_disjoint, auto)
  10.239 -  done
  10.240 +    done
  10.241    also have "... = int(card(S1)) + int(card(S2))" by auto
  10.242    finally show ?thesis .
  10.243  qed
  10.244  
  10.245 -lemma (in QRTEMP) aux1a: "[| 0 < a; a \<le> (p - 1) div 2; 
  10.246 +lemma (in QRTEMP) aux1a: "[| 0 < a; a \<le> (p - 1) div 2;
  10.247                               0 < b; b \<le> (q - 1) div 2 |] ==>
  10.248                            (p * b < q * a) = (b \<le> q * a div p)"
  10.249  proof -
  10.250 @@ -309,30 +308,31 @@
  10.251      assume "p * b < q * a"
  10.252      then have "p * b \<le> q * a" by auto
  10.253      then have "(p * b) div p \<le> (q * a) div p"
  10.254 -      by (rule zdiv_mono1, insert p_g_2, auto)
  10.255 +      by (rule zdiv_mono1) (insert p_g_2, auto)
  10.256      then show "b \<le> (q * a) div p"
  10.257        apply (subgoal_tac "p \<noteq> 0")
  10.258        apply (frule zdiv_zmult_self2, force)
  10.259 -      by (insert p_g_2, auto)
  10.260 +      apply (insert p_g_2, auto)
  10.261 +      done
  10.262    qed
  10.263    moreover have "b \<le> q * a div p ==> p * b < q * a"
  10.264    proof -
  10.265      assume "b \<le> q * a div p"
  10.266      then have "p * b \<le> p * ((q * a) div p)"
  10.267 -      by (insert p_g_2, auto simp add: mult_le_cancel_left)
  10.268 +      using p_g_2 by (auto simp add: mult_le_cancel_left)
  10.269      also have "... \<le> q * a"
  10.270 -      by (rule zdiv_leq_prop, insert p_g_2, auto)
  10.271 +      by (rule zdiv_leq_prop) (insert p_g_2, auto)
  10.272      finally have "p * b \<le> q * a" .
  10.273      then have "p * b < q * a | p * b = q * a"
  10.274        by (simp only: order_le_imp_less_or_eq)
  10.275      moreover have "p * b \<noteq> q * a"
  10.276 -      by (rule  pb_neq_qa, insert prems, auto)
  10.277 +      by (rule  pb_neq_qa) (insert prems, auto)
  10.278      ultimately show ?thesis by auto
  10.279    qed
  10.280    ultimately show ?thesis ..
  10.281  qed
  10.282  
  10.283 -lemma (in QRTEMP) aux1b: "[| 0 < a; a \<le> (p - 1) div 2; 
  10.284 +lemma (in QRTEMP) aux1b: "[| 0 < a; a \<le> (p - 1) div 2;
  10.285                               0 < b; b \<le> (q - 1) div 2 |] ==>
  10.286                            (q * a < p * b) = (a \<le> p * b div q)"
  10.287  proof -
  10.288 @@ -342,30 +342,31 @@
  10.289      assume "q * a < p * b"
  10.290      then have "q * a \<le> p * b" by auto
  10.291      then have "(q * a) div q \<le> (p * b) div q"
  10.292 -      by (rule zdiv_mono1, insert q_g_2, auto)
  10.293 +      by (rule zdiv_mono1) (insert q_g_2, auto)
  10.294      then show "a \<le> (p * b) div q"
  10.295        apply (subgoal_tac "q \<noteq> 0")
  10.296        apply (frule zdiv_zmult_self2, force)
  10.297 -      by (insert q_g_2, auto)
  10.298 +      apply (insert q_g_2, auto)
  10.299 +      done
  10.300    qed
  10.301    moreover have "a \<le> p * b div q ==> q * a < p * b"
  10.302    proof -
  10.303      assume "a \<le> p * b div q"
  10.304      then have "q * a \<le> q * ((p * b) div q)"
  10.305 -      by (insert q_g_2, auto simp add: mult_le_cancel_left)
  10.306 +      using q_g_2 by (auto simp add: mult_le_cancel_left)
  10.307      also have "... \<le> p * b"
  10.308 -      by (rule zdiv_leq_prop, insert q_g_2, auto)
  10.309 +      by (rule zdiv_leq_prop) (insert q_g_2, auto)
  10.310      finally have "q * a \<le> p * b" .
  10.311      then have "q * a < p * b | q * a = p * b"
  10.312        by (simp only: order_le_imp_less_or_eq)
  10.313      moreover have "p * b \<noteq> q * a"
  10.314 -      by (rule  pb_neq_qa, insert prems, auto)
  10.315 +      by (rule  pb_neq_qa) (insert prems, auto)
  10.316      ultimately show ?thesis by auto
  10.317    qed
  10.318    ultimately show ?thesis ..
  10.319  qed
  10.320  
  10.321 -lemma aux2: "[| zprime p; zprime q; 2 < p; 2 < q |] ==> 
  10.322 +lemma aux2: "[| zprime p; zprime q; 2 < p; 2 < q |] ==>
  10.323               (q * ((p - 1) div 2)) div p \<le> (q - 1) div 2"
  10.324  proof-
  10.325    assume "zprime p" and "zprime q" and "2 < p" and "2 < q"
  10.326 @@ -388,10 +389,10 @@
  10.327      by (auto simp add: even1 even_prod_div_2)
  10.328    also have "(((q - 1) * p) + (2 * p)) div 2 = (((q - 1) div 2) * p) + p"
  10.329      by (auto simp add: even1 even2 even_prod_div_2 even_sum_div_2)
  10.330 -  finally show ?thesis 
  10.331 -    apply (rule_tac x = " q * ((p - 1) div 2)" and 
  10.332 +  finally show ?thesis
  10.333 +    apply (rule_tac x = " q * ((p - 1) div 2)" and
  10.334                      y = "(q - 1) div 2" in div_prop2)
  10.335 -    by (insert prems, auto)
  10.336 +    using prems by auto
  10.337  qed
  10.338  
  10.339  lemma (in QRTEMP) aux3a: "\<forall>j \<in> P_set. int (card (f1 j)) = (q * j) div p"
  10.340 @@ -410,27 +411,29 @@
  10.341      ultimately have "card ((%(x,y). y) ` (f1 j)) = card  (f1 j)"
  10.342        by (auto simp add: f1_def card_image)
  10.343      moreover have "((%(x,y). y) ` (f1 j)) = {y. y \<in> Q_set & y \<le> (q * j) div p}"
  10.344 -      by (insert prems, auto simp add: f1_def S_def Q_set_def P_set_def 
  10.345 -        image_def)
  10.346 +      using prems by (auto simp add: f1_def S_def Q_set_def P_set_def image_def)
  10.347      ultimately show ?thesis by (auto simp add: f1_def)
  10.348    qed
  10.349    also have "... = int (card {y. 0 < y & y \<le> (q * j) div p})"
  10.350    proof -
  10.351 -    have "{y. y \<in> Q_set & y \<le> (q * j) div p} = 
  10.352 +    have "{y. y \<in> Q_set & y \<le> (q * j) div p} =
  10.353          {y. 0 < y & y \<le> (q * j) div p}"
  10.354        apply (auto simp add: Q_set_def)
  10.355 -      proof -
  10.356 -        fix x
  10.357 -        assume "0 < x" and "x \<le> q * j div p"
  10.358 -        with j_fact P_set_def  have "j \<le> (p - 1) div 2" by auto
  10.359 -        with q_g_2 have "q * j \<le> q * ((p - 1) div 2)"
  10.360 -          by (auto simp add: mult_le_cancel_left)
  10.361 -        with p_g_2 have "q * j div p \<le> q * ((p - 1) div 2) div p"
  10.362 -          by (auto simp add: zdiv_mono1)
  10.363 -        also from prems have "... \<le> (q - 1) div 2"
  10.364 -          apply simp apply (insert aux2) by (simp add: QRTEMP_def)
  10.365 -        finally show "x \<le> (q - 1) div 2" by (insert prems, auto)
  10.366 -      qed
  10.367 +    proof -
  10.368 +      fix x
  10.369 +      assume "0 < x" and "x \<le> q * j div p"
  10.370 +      with j_fact P_set_def  have "j \<le> (p - 1) div 2" by auto
  10.371 +      with q_g_2 have "q * j \<le> q * ((p - 1) div 2)"
  10.372 +        by (auto simp add: mult_le_cancel_left)
  10.373 +      with p_g_2 have "q * j div p \<le> q * ((p - 1) div 2) div p"
  10.374 +        by (auto simp add: zdiv_mono1)
  10.375 +      also from prems have "... \<le> (q - 1) div 2"
  10.376 +        apply simp
  10.377 +        apply (insert aux2)
  10.378 +        apply (simp add: QRTEMP_def)
  10.379 +        done
  10.380 +      finally show "x \<le> (q - 1) div 2" using prems by auto
  10.381 +    qed
  10.382      then show ?thesis by auto
  10.383    qed
  10.384    also have "... = (q * j) div p"
  10.385 @@ -440,7 +443,8 @@
  10.386      then have "0 \<le> q * j" by auto
  10.387      then have "0 div p \<le> (q * j) div p"
  10.388        apply (rule_tac a = 0 in zdiv_mono1)
  10.389 -      by (insert p_g_2, auto)
  10.390 +      apply (insert p_g_2, auto)
  10.391 +      done
  10.392      also have "0 div p = 0" by auto
  10.393      finally show ?thesis by (auto simp add: card_bdd_int_set_l_le)
  10.394    qed
  10.395 @@ -463,26 +467,25 @@
  10.396      ultimately have "card ((%(x,y). x) ` (f2 j)) = card  (f2 j)"
  10.397        by (auto simp add: f2_def card_image)
  10.398      moreover have "((%(x,y). x) ` (f2 j)) = {y. y \<in> P_set & y \<le> (p * j) div q}"
  10.399 -      by (insert prems, auto simp add: f2_def S_def Q_set_def 
  10.400 -        P_set_def image_def)
  10.401 +      using prems by (auto simp add: f2_def S_def Q_set_def P_set_def image_def)
  10.402      ultimately show ?thesis by (auto simp add: f2_def)
  10.403    qed
  10.404    also have "... = int (card {y. 0 < y & y \<le> (p * j) div q})"
  10.405    proof -
  10.406 -    have "{y. y \<in> P_set & y \<le> (p * j) div q} = 
  10.407 +    have "{y. y \<in> P_set & y \<le> (p * j) div q} =
  10.408          {y. 0 < y & y \<le> (p * j) div q}"
  10.409        apply (auto simp add: P_set_def)
  10.410 -      proof -
  10.411 -        fix x
  10.412 -        assume "0 < x" and "x \<le> p * j div q"
  10.413 -        with j_fact Q_set_def  have "j \<le> (q - 1) div 2" by auto
  10.414 -        with p_g_2 have "p * j \<le> p * ((q - 1) div 2)"
  10.415 -          by (auto simp add: mult_le_cancel_left)
  10.416 -        with q_g_2 have "p * j div q \<le> p * ((q - 1) div 2) div q"
  10.417 -          by (auto simp add: zdiv_mono1)
  10.418 -        also from prems have "... \<le> (p - 1) div 2"
  10.419 -          by (auto simp add: aux2 QRTEMP_def)
  10.420 -        finally show "x \<le> (p - 1) div 2" by (insert prems, auto)
  10.421 +    proof -
  10.422 +      fix x
  10.423 +      assume "0 < x" and "x \<le> p * j div q"
  10.424 +      with j_fact Q_set_def  have "j \<le> (q - 1) div 2" by auto
  10.425 +      with p_g_2 have "p * j \<le> p * ((q - 1) div 2)"
  10.426 +        by (auto simp add: mult_le_cancel_left)
  10.427 +      with q_g_2 have "p * j div q \<le> p * ((q - 1) div 2) div q"
  10.428 +        by (auto simp add: zdiv_mono1)
  10.429 +      also from prems have "... \<le> (p - 1) div 2"
  10.430 +        by (auto simp add: aux2 QRTEMP_def)
  10.431 +      finally show "x \<le> (p - 1) div 2" using prems by auto
  10.432        qed
  10.433      then show ?thesis by auto
  10.434    qed
  10.435 @@ -493,7 +496,8 @@
  10.436      then have "0 \<le> p * j" by auto
  10.437      then have "0 div q \<le> (p * j) div q"
  10.438        apply (rule_tac a = 0 in zdiv_mono1)
  10.439 -      by (insert q_g_2, auto)
  10.440 +      apply (insert q_g_2, auto)
  10.441 +      done
  10.442      also have "0 div q = 0" by auto
  10.443      finally show ?thesis by (auto simp add: card_bdd_int_set_l_le)
  10.444    qed
  10.445 @@ -511,12 +515,12 @@
  10.446    moreover have "(\<forall>x \<in> P_set. \<forall>y \<in> P_set. x \<noteq> y --> (f1 x) \<inter> (f1 y) = {})"
  10.447      by (auto simp add: f1_def)
  10.448    moreover note P_set_finite
  10.449 -  ultimately have "int(card (UNION P_set f1)) = 
  10.450 +  ultimately have "int(card (UNION P_set f1)) =
  10.451        setsum (%x. int(card (f1 x))) P_set"
  10.452      by(simp add:card_UN_disjoint int_setsum o_def)
  10.453    moreover have "S1 = UNION P_set f1"
  10.454      by (auto simp add: f1_def S_def S1_def S2_def P_set_def Q_set_def aux1a)
  10.455 -  ultimately have "int(card (S1)) = setsum (%j. int(card (f1 j))) P_set" 
  10.456 +  ultimately have "int(card (S1)) = setsum (%j. int(card (f1 j))) P_set"
  10.457      by auto
  10.458    also have "... = setsum (%j. q * j div p) P_set"
  10.459      using aux3a by(fastsimp intro: setsum_cong)
  10.460 @@ -531,34 +535,34 @@
  10.461      have "f2 x \<subseteq> S" by (auto simp add: f2_def)
  10.462      with S_finite show "finite (f2 x)" by (auto simp add: finite_subset)
  10.463    qed
  10.464 -  moreover have "(\<forall>x \<in> Q_set. \<forall>y \<in> Q_set. x \<noteq> y --> 
  10.465 +  moreover have "(\<forall>x \<in> Q_set. \<forall>y \<in> Q_set. x \<noteq> y -->
  10.466        (f2 x) \<inter> (f2 y) = {})"
  10.467      by (auto simp add: f2_def)
  10.468    moreover note Q_set_finite
  10.469 -  ultimately have "int(card (UNION Q_set f2)) = 
  10.470 +  ultimately have "int(card (UNION Q_set f2)) =
  10.471        setsum (%x. int(card (f2 x))) Q_set"
  10.472      by(simp add:card_UN_disjoint int_setsum o_def)
  10.473    moreover have "S2 = UNION Q_set f2"
  10.474      by (auto simp add: f2_def S_def S1_def S2_def P_set_def Q_set_def aux1b)
  10.475 -  ultimately have "int(card (S2)) = setsum (%j. int(card (f2 j))) Q_set" 
  10.476 +  ultimately have "int(card (S2)) = setsum (%j. int(card (f2 j))) Q_set"
  10.477      by auto
  10.478    also have "... = setsum (%j. p * j div q) Q_set"
  10.479      using aux3b by(fastsimp intro: setsum_cong)
  10.480    finally show ?thesis .
  10.481  qed
  10.482  
  10.483 -lemma (in QRTEMP) S1_carda: "int (card(S1)) = 
  10.484 +lemma (in QRTEMP) S1_carda: "int (card(S1)) =
  10.485      setsum (%j. (j * q) div p) P_set"
  10.486    by (auto simp add: S1_card zmult_ac)
  10.487  
  10.488 -lemma (in QRTEMP) S2_carda: "int (card(S2)) = 
  10.489 +lemma (in QRTEMP) S2_carda: "int (card(S2)) =
  10.490      setsum (%j. (j * p) div q) Q_set"
  10.491    by (auto simp add: S2_card zmult_ac)
  10.492  
  10.493 -lemma (in QRTEMP) pq_sum_prop: "(setsum (%j. (j * p) div q) Q_set) + 
  10.494 +lemma (in QRTEMP) pq_sum_prop: "(setsum (%j. (j * p) div q) Q_set) +
  10.495      (setsum (%j. (j * q) div p) P_set) = ((p - 1) div 2) * ((q - 1) div 2)"
  10.496  proof -
  10.497 -  have "(setsum (%j. (j * p) div q) Q_set) + 
  10.498 +  have "(setsum (%j. (j * p) div q) Q_set) +
  10.499        (setsum (%j. (j * q) div p) P_set) = int (card S2) + int (card S1)"
  10.500      by (auto simp add: S1_carda S2_carda)
  10.501    also have "... = int (card S1) + int (card S2)"
  10.502 @@ -572,50 +576,54 @@
  10.503    apply (auto simp add: zcong_eq_zdvd_prop zprime_def)
  10.504    apply (drule_tac x = q in allE)
  10.505    apply (drule_tac x = p in allE)
  10.506 -by auto
  10.507 +  apply auto
  10.508 +  done
  10.509  
  10.510 -lemma (in QRTEMP) QR_short: "(Legendre p q) * (Legendre q p) = 
  10.511 +lemma (in QRTEMP) QR_short: "(Legendre p q) * (Legendre q p) =
  10.512      (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))"
  10.513  proof -
  10.514    from prems have "~([p = 0] (mod q))"
  10.515      by (auto simp add: pq_prime_neq QRTEMP_def)
  10.516 -  with prems have a1: "(Legendre p q) = (-1::int) ^ 
  10.517 +  with prems have a1: "(Legendre p q) = (-1::int) ^
  10.518        nat(setsum (%x. ((x * p) div q)) Q_set)"
  10.519      apply (rule_tac p = q in  MainQRLemma)
  10.520 -    by (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
  10.521 +    apply (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
  10.522 +    done
  10.523    from prems have "~([q = 0] (mod p))"
  10.524      apply (rule_tac p = q and q = p in pq_prime_neq)
  10.525      apply (simp add: QRTEMP_def)+
  10.526      done
  10.527 -  with prems have a2: "(Legendre q p) = 
  10.528 +  with prems have a2: "(Legendre q p) =
  10.529        (-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)"
  10.530      apply (rule_tac p = p in  MainQRLemma)
  10.531 -    by (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
  10.532 -  from a1 a2 have "(Legendre p q) * (Legendre q p) = 
  10.533 +    apply (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
  10.534 +    done
  10.535 +  from a1 a2 have "(Legendre p q) * (Legendre q p) =
  10.536        (-1::int) ^ nat(setsum (%x. ((x * p) div q)) Q_set) *
  10.537          (-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)"
  10.538      by auto
  10.539 -  also have "... = (-1::int) ^ (nat(setsum (%x. ((x * p) div q)) Q_set) + 
  10.540 +  also have "... = (-1::int) ^ (nat(setsum (%x. ((x * p) div q)) Q_set) +
  10.541                     nat(setsum (%x. ((x * q) div p)) P_set))"
  10.542      by (auto simp add: zpower_zadd_distrib)
  10.543 -  also have "nat(setsum (%x. ((x * p) div q)) Q_set) + 
  10.544 +  also have "nat(setsum (%x. ((x * p) div q)) Q_set) +
  10.545        nat(setsum (%x. ((x * q) div p)) P_set) =
  10.546 -        nat((setsum (%x. ((x * p) div q)) Q_set) + 
  10.547 +        nat((setsum (%x. ((x * p) div q)) Q_set) +
  10.548            (setsum (%x. ((x * q) div p)) P_set))"
  10.549 -    apply (rule_tac z1 = "setsum (%x. ((x * p) div q)) Q_set" in 
  10.550 -      nat_add_distrib [THEN sym])
  10.551 -    by (auto simp add: S1_carda [THEN sym] S2_carda [THEN sym])
  10.552 +    apply (rule_tac z1 = "setsum (%x. ((x * p) div q)) Q_set" in
  10.553 +      nat_add_distrib [symmetric])
  10.554 +    apply (auto simp add: S1_carda [symmetric] S2_carda [symmetric])
  10.555 +    done
  10.556    also have "... = nat(((p - 1) div 2) * ((q - 1) div 2))"
  10.557      by (auto simp add: pq_sum_prop)
  10.558    finally show ?thesis .
  10.559  qed
  10.560  
  10.561  theorem Quadratic_Reciprocity:
  10.562 -     "[| p \<in> zOdd; zprime p; q \<in> zOdd; zprime q; 
  10.563 -         p \<noteq> q |] 
  10.564 -      ==> (Legendre p q) * (Legendre q p) = 
  10.565 +     "[| p \<in> zOdd; zprime p; q \<in> zOdd; zprime q;
  10.566 +         p \<noteq> q |]
  10.567 +      ==> (Legendre p q) * (Legendre q p) =
  10.568            (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))"
  10.569 -  by (auto simp add: QRTEMP.QR_short zprime_zOdd_eq_grt_2 [THEN sym] 
  10.570 +  by (auto simp add: QRTEMP.QR_short zprime_zOdd_eq_grt_2 [symmetric]
  10.571                       QRTEMP_def)
  10.572  
  10.573  end
    11.1 --- a/src/HOL/NumberTheory/Residues.thy	Thu Dec 08 12:50:03 2005 +0100
    11.2 +++ b/src/HOL/NumberTheory/Residues.thy	Thu Dec 08 12:50:04 2005 +0100
    11.3 @@ -5,7 +5,7 @@
    11.4  
    11.5  header {* Residue Sets *}
    11.6  
    11.7 -theory Residues imports Int2 begin;
    11.8 +theory Residues imports Int2 begin
    11.9  
   11.10  text{*Note.  This theory is being revised.  See the web page
   11.11  \url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
   11.12 @@ -37,7 +37,7 @@
   11.13    "SR p == {x. (0 \<le> x) & (x < p)}"
   11.14  
   11.15    SRStar      :: "int => int set"
   11.16 -  "SRStar p == {x. (0 < x) & (x < p)}";
   11.17 +  "SRStar p == {x. (0 < x) & (x < p)}"
   11.18  
   11.19  (******************************************************************)
   11.20  (*                                                                *)
   11.21 @@ -47,29 +47,29 @@
   11.22  
   11.23  subsection {* Properties of StandardRes *}
   11.24  
   11.25 -lemma StandardRes_prop1: "[x = StandardRes m x] (mod m)";
   11.26 +lemma StandardRes_prop1: "[x = StandardRes m x] (mod m)"
   11.27    by (auto simp add: StandardRes_def zcong_zmod)
   11.28  
   11.29  lemma StandardRes_prop2: "0 < m ==> (StandardRes m x1 = StandardRes m x2)
   11.30 -      = ([x1 = x2] (mod m))";
   11.31 +      = ([x1 = x2] (mod m))"
   11.32    by (auto simp add: StandardRes_def zcong_zmod_eq)
   11.33  
   11.34 -lemma StandardRes_prop3: "(~[x = 0] (mod p)) = (~(StandardRes p x = 0))";
   11.35 +lemma StandardRes_prop3: "(~[x = 0] (mod p)) = (~(StandardRes p x = 0))"
   11.36    by (auto simp add: StandardRes_def zcong_def zdvd_iff_zmod_eq_0)
   11.37  
   11.38  lemma StandardRes_prop4: "2 < m 
   11.39 -     ==> [StandardRes m x * StandardRes m y = (x * y)] (mod m)";
   11.40 +     ==> [StandardRes m x * StandardRes m y = (x * y)] (mod m)"
   11.41    by (auto simp add: StandardRes_def zcong_zmod_eq 
   11.42                       zmod_zmult_distrib [of x y m])
   11.43  
   11.44 -lemma StandardRes_lbound: "0 < p ==> 0 \<le> StandardRes p x";
   11.45 +lemma StandardRes_lbound: "0 < p ==> 0 \<le> StandardRes p x"
   11.46    by (auto simp add: StandardRes_def pos_mod_sign)
   11.47  
   11.48 -lemma StandardRes_ubound: "0 < p ==> StandardRes p x < p";
   11.49 +lemma StandardRes_ubound: "0 < p ==> StandardRes p x < p"
   11.50    by (auto simp add: StandardRes_def pos_mod_bound)
   11.51  
   11.52  lemma StandardRes_eq_zcong: 
   11.53 -   "(StandardRes m x = 0) = ([x = 0](mod m))";
   11.54 +   "(StandardRes m x = 0) = ([x = 0](mod m))"
   11.55    by (auto simp add: StandardRes_def zcong_eq_zdvd_prop dvd_def) 
   11.56  
   11.57  (******************************************************************)
   11.58 @@ -80,55 +80,56 @@
   11.59  
   11.60  subsection {* Relations between StandardRes, SRStar, and SR *}
   11.61  
   11.62 -lemma SRStar_SR_prop: "x \<in> SRStar p ==> x \<in> SR p";
   11.63 +lemma SRStar_SR_prop: "x \<in> SRStar p ==> x \<in> SR p"
   11.64    by (auto simp add: SRStar_def SR_def)
   11.65  
   11.66 -lemma StandardRes_SR_prop: "x \<in> SR p ==> StandardRes p x = x";
   11.67 +lemma StandardRes_SR_prop: "x \<in> SR p ==> StandardRes p x = x"
   11.68    by (auto simp add: SR_def StandardRes_def mod_pos_pos_trivial)
   11.69  
   11.70  lemma StandardRes_SRStar_prop1: "2 < p ==> (StandardRes p x \<in> SRStar p) 
   11.71 -     = (~[x = 0] (mod p))";
   11.72 +     = (~[x = 0] (mod p))"
   11.73    apply (auto simp add: StandardRes_prop3 StandardRes_def
   11.74                          SRStar_def pos_mod_bound)
   11.75    apply (subgoal_tac "0 < p")
   11.76 -by (drule_tac a = x in pos_mod_sign, arith, simp)
   11.77 +  apply (drule_tac a = x in pos_mod_sign, arith, simp)
   11.78 +  done
   11.79  
   11.80 -lemma StandardRes_SRStar_prop1a: "x \<in> SRStar p ==> ~([x = 0] (mod p))";
   11.81 +lemma StandardRes_SRStar_prop1a: "x \<in> SRStar p ==> ~([x = 0] (mod p))"
   11.82    by (auto simp add: SRStar_def zcong_def zdvd_not_zless)
   11.83  
   11.84  lemma StandardRes_SRStar_prop2: "[| 2 < p; zprime p; x \<in> SRStar p |] 
   11.85 -     ==> StandardRes p (MultInv p x) \<in> SRStar p";
   11.86 -  apply (frule_tac x = "(MultInv p x)" in StandardRes_SRStar_prop1, simp);
   11.87 +     ==> StandardRes p (MultInv p x) \<in> SRStar p"
   11.88 +  apply (frule_tac x = "(MultInv p x)" in StandardRes_SRStar_prop1, simp)
   11.89    apply (rule MultInv_prop3)
   11.90    apply (auto simp add: SRStar_def zcong_def zdvd_not_zless)
   11.91 -done
   11.92 +  done
   11.93  
   11.94 -lemma StandardRes_SRStar_prop3: "x \<in> SRStar p ==> StandardRes p x = x";
   11.95 +lemma StandardRes_SRStar_prop3: "x \<in> SRStar p ==> StandardRes p x = x"
   11.96    by (auto simp add: SRStar_SR_prop StandardRes_SR_prop)
   11.97  
   11.98  lemma StandardRes_SRStar_prop4: "[| zprime p; 2 < p; x \<in> SRStar p |] 
   11.99 -     ==> StandardRes p x \<in> SRStar p";
  11.100 +     ==> StandardRes p x \<in> SRStar p"
  11.101    by (frule StandardRes_SRStar_prop3, auto)
  11.102  
  11.103  lemma SRStar_mult_prop1: "[| zprime p; 2 < p; x \<in> SRStar p; y \<in> SRStar p|] 
  11.104 -     ==> (StandardRes p (x * y)):SRStar p";
  11.105 +     ==> (StandardRes p (x * y)):SRStar p"
  11.106    apply (frule_tac x = x in StandardRes_SRStar_prop4, auto)
  11.107    apply (frule_tac x = y in StandardRes_SRStar_prop4, auto)
  11.108    apply (auto simp add: StandardRes_SRStar_prop1 zcong_zmult_prop3)
  11.109 -done
  11.110 +  done
  11.111  
  11.112  lemma SRStar_mult_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)); 
  11.113       x \<in> SRStar p |] 
  11.114 -     ==> StandardRes p (a * MultInv p x) \<in> SRStar p";
  11.115 +     ==> StandardRes p (a * MultInv p x) \<in> SRStar p"
  11.116    apply (frule_tac x = x in StandardRes_SRStar_prop2, auto)
  11.117    apply (frule_tac x = "MultInv p x" in StandardRes_SRStar_prop1)
  11.118    apply (auto simp add: StandardRes_SRStar_prop1 zcong_zmult_prop3)
  11.119 -done
  11.120 +  done
  11.121  
  11.122 -lemma SRStar_card: "2 < p ==> int(card(SRStar p)) = p - 1";
  11.123 +lemma SRStar_card: "2 < p ==> int(card(SRStar p)) = p - 1"
  11.124    by (auto simp add: SRStar_def int_card_bdd_int_set_l_l)
  11.125  
  11.126 -lemma SRStar_finite: "2 < p ==> finite( SRStar p)";
  11.127 +lemma SRStar_finite: "2 < p ==> finite( SRStar p)"
  11.128    by (auto simp add: SRStar_def bdd_int_set_l_l_finite)
  11.129  
  11.130  (******************************************************************)
  11.131 @@ -139,40 +140,42 @@
  11.132  
  11.133  subsection {* Properties relating ResSets with StandardRes *}
  11.134  
  11.135 -lemma aux: "x mod m = y mod m ==> [x = y] (mod m)";
  11.136 -  apply (subgoal_tac "x = y ==> [x = y](mod m)");
  11.137 -  apply (subgoal_tac "[x mod m = y mod m] (mod m) ==> [x = y] (mod m)");
  11.138 +lemma aux: "x mod m = y mod m ==> [x = y] (mod m)"
  11.139 +  apply (subgoal_tac "x = y ==> [x = y](mod m)")
  11.140 +  apply (subgoal_tac "[x mod m = y mod m] (mod m) ==> [x = y] (mod m)")
  11.141    apply (auto simp add: zcong_zmod [of x y m])
  11.142 -done
  11.143 +  done
  11.144  
  11.145 -lemma StandardRes_inj_on_ResSet: "ResSet m X ==> (inj_on (StandardRes m) X)";
  11.146 +lemma StandardRes_inj_on_ResSet: "ResSet m X ==> (inj_on (StandardRes m) X)"
  11.147    apply (auto simp add: ResSet_def StandardRes_def inj_on_def)
  11.148    apply (drule_tac m = m in aux, auto)
  11.149 -done
  11.150 +  done
  11.151  
  11.152  lemma StandardRes_Sum: "[| finite X; 0 < m |] 
  11.153 -     ==> [setsum f X = setsum (StandardRes m o f) X](mod m)"; 
  11.154 +     ==> [setsum f X = setsum (StandardRes m o f) X](mod m)" 
  11.155    apply (rule_tac F = X in finite_induct)
  11.156    apply (auto intro!: zcong_zadd simp add: StandardRes_prop1)
  11.157 -done
  11.158 +  done
  11.159  
  11.160 -lemma SR_pos: "0 < m ==> (StandardRes m ` X) \<subseteq> {x. 0 \<le> x & x < m}";
  11.161 +lemma SR_pos: "0 < m ==> (StandardRes m ` X) \<subseteq> {x. 0 \<le> x & x < m}"
  11.162    by (auto simp add: StandardRes_ubound StandardRes_lbound)
  11.163  
  11.164 -lemma ResSet_finite: "0 < m ==> ResSet m X ==> finite X";
  11.165 +lemma ResSet_finite: "0 < m ==> ResSet m X ==> finite X"
  11.166    apply (rule_tac f = "StandardRes m" in finite_imageD) 
  11.167 -  apply (rule_tac B = "{x. (0 :: int) \<le> x & x < m}" in finite_subset);
  11.168 -by (auto simp add: StandardRes_inj_on_ResSet bdd_int_set_l_finite SR_pos)
  11.169 +  apply (rule_tac B = "{x. (0 :: int) \<le> x & x < m}" in finite_subset)
  11.170 +  apply (auto simp add: StandardRes_inj_on_ResSet bdd_int_set_l_finite SR_pos)
  11.171 +  done
  11.172  
  11.173 -lemma mod_mod_is_mod: "[x = x mod m](mod m)";
  11.174 +lemma mod_mod_is_mod: "[x = x mod m](mod m)"
  11.175    by (auto simp add: zcong_zmod)
  11.176  
  11.177  lemma StandardRes_prod: "[| finite X; 0 < m |] 
  11.178 -     ==> [setprod f X = setprod (StandardRes m o f) X] (mod m)";
  11.179 +     ==> [setprod f X = setprod (StandardRes m o f) X] (mod m)"
  11.180    apply (rule_tac F = X in finite_induct)
  11.181 -by (auto intro!: zcong_zmult simp add: StandardRes_prop1)
  11.182 +  apply (auto intro!: zcong_zmult simp add: StandardRes_prop1)
  11.183 +  done
  11.184  
  11.185 -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.186 +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.187    by (auto simp add: ResSet_def)
  11.188  
  11.189  (****************************************************************)
  11.190 @@ -181,7 +184,7 @@
  11.191  (*                                                              *)
  11.192  (****************************************************************)
  11.193  
  11.194 -lemma ResSet_SRStar_prop: "ResSet p (SRStar p)";
  11.195 +lemma ResSet_SRStar_prop: "ResSet p (SRStar p)"
  11.196    by (auto simp add: SRStar_def ResSet_def zcong_zless_imp_eq)
  11.197  
  11.198 -end;
  11.199 \ No newline at end of file
  11.200 +end
    12.1 --- a/src/HOL/NumberTheory/WilsonRuss.thy	Thu Dec 08 12:50:03 2005 +0100
    12.2 +++ b/src/HOL/NumberTheory/WilsonRuss.thy	Thu Dec 08 12:50:04 2005 +0100
    12.3 @@ -2,9 +2,6 @@
    12.4      ID:         $Id$
    12.5      Author:     Thomas M. Rasmussen
    12.6      Copyright   2000  University of Cambridge
    12.7 -
    12.8 -Changes by Jeremy Avigad, 2003/02/21:
    12.9 -    repaired proof of prime_g_5
   12.10  *)
   12.11  
   12.12  header {* Wilson's Theorem according to Russinoff *}
   12.13 @@ -165,19 +162,16 @@
   12.14  declare wset.simps [simp del]
   12.15  
   12.16  lemma wset_induct:
   12.17 -  "(!!a p. P {} a p) \<Longrightarrow>
   12.18 -    (!!a p. 1 < (a::int) \<Longrightarrow> P (wset (a - 1, p)) (a - 1) p
   12.19 -      ==> P (wset (a, p)) a p)
   12.20 -    ==> P (wset (u, v)) u v"
   12.21 -proof -
   12.22 -  case rule_context
   12.23 -  show ?thesis
   12.24 -    apply (rule wset.induct, safe)
   12.25 -     apply (case_tac [2] "1 < a")
   12.26 -      apply (rule_tac [2] rule_context, simp_all)
   12.27 -      apply (simp_all add: wset.simps rule_context)
   12.28 -    done
   12.29 -qed
   12.30 +  assumes "!!a p. P {} a p"
   12.31 +    and "!!a p. 1 < (a::int) \<Longrightarrow> P (wset (a - 1, p)) (a - 1) p ==> P (wset (a, p)) a p"
   12.32 +  shows "P (wset (u, v)) u v"
   12.33 +  apply (rule wset.induct, safe)
   12.34 +   prefer 2
   12.35 +   apply (case_tac "1 < a")
   12.36 +    apply (rule prems)
   12.37 +     apply simp_all
   12.38 +   apply (simp_all add: wset.simps prems)
   12.39 +  done
   12.40  
   12.41  lemma wset_mem_imp_or [rule_format]:
   12.42    "1 < a \<Longrightarrow> b \<notin> wset (a - 1, p)