First step in reorganizing Finite_Set
authornipkow
Thu Dec 09 18:30:59 2004 +0100 (2004-12-09)
changeset 15392290bc97038c7
parent 15391 797ed46d724b
child 15393 2e6a9146caca
First step in reorganizing Finite_Set
src/HOL/Equiv_Relations.thy
src/HOL/Finite_Set.ML
src/HOL/Finite_Set.thy
src/HOL/List.thy
src/HOL/Matrix/MatrixGeneral.thy
src/HOL/NumberTheory/Euler.thy
src/HOL/NumberTheory/EulerFermat.thy
src/HOL/NumberTheory/Finite2.thy
src/HOL/NumberTheory/Gauss.thy
src/HOL/NumberTheory/Int2.thy
src/HOL/NumberTheory/IntFact.thy
src/HOL/NumberTheory/Quadratic_Reciprocity.thy
src/HOL/NumberTheory/Residues.thy
src/HOL/NumberTheory/WilsonBij.thy
src/HOL/NumberTheory/WilsonRuss.thy
     1.1 --- a/src/HOL/Equiv_Relations.thy	Thu Dec 09 16:45:46 2004 +0100
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Thu Dec 09 18:30:59 2004 +0100
     1.3 @@ -316,8 +316,8 @@
     1.4    apply (rule Union_quotient [THEN subst])
     1.5     apply assumption
     1.6    apply (rule dvd_partition)
     1.7 -     prefer 4 apply (blast dest: quotient_disj)
     1.8 -    apply (simp_all add: Union_quotient equiv_type finite_quotient)
     1.9 +     prefer 3 apply (blast dest: quotient_disj)
    1.10 +    apply (simp_all add: Union_quotient equiv_type)
    1.11    done
    1.12  
    1.13  lemma card_quotient_disjoint:
     2.1 --- a/src/HOL/Finite_Set.ML	Thu Dec 09 16:45:46 2004 +0100
     2.2 +++ b/src/HOL/Finite_Set.ML	Thu Dec 09 18:30:59 2004 +0100
     2.3 @@ -31,7 +31,6 @@
     2.4    val [emptyI, insertI] = thms "foldSet.intros";
     2.5  end;
     2.6  
     2.7 -val Diff1_foldSet = thm "Diff1_foldSet";
     2.8  val cardR_SucD = thm "cardR_SucD";
     2.9  val cardR_determ = thm "cardR_determ";
    2.10  val cardR_emptyE = thm "cardR_emptyE";
    2.11 @@ -51,8 +50,8 @@
    2.12  val card_bij_eq = thm "card_bij_eq";
    2.13  val card_def = thm "card_def";
    2.14  val card_empty = thm "card_empty";
    2.15 +val card_equality = thm "card_equality";
    2.16  val card_eq_setsum = thm "card_eq_setsum";
    2.17 -val card_equality = thm "card_equality";
    2.18  val card_image = thm "card_image";
    2.19  val card_image_le = thm "card_image_le";
    2.20  val card_inj_on_le = thm "card_inj_on_le";
    2.21 @@ -66,6 +65,7 @@
    2.22  val card_seteq = thm "card_seteq";
    2.23  val choose_deconstruct = thm "choose_deconstruct";
    2.24  val constr_bij = thm "constr_bij";
    2.25 +val Diff1_foldSet = thm "Diff1_foldSet";
    2.26  val dvd_partition = thm "dvd_partition";
    2.27  val empty_foldSetE = thm "empty_foldSetE";
    2.28  val endo_inj_surj = thm "endo_inj_surj";
    2.29 @@ -74,6 +74,7 @@
    2.30  val finite_Diff = thm "finite_Diff";
    2.31  val finite_Diff_insert = thm "finite_Diff_insert";
    2.32  val finite_Field = thm "finite_Field";
    2.33 +val finite_imp_foldSet = thm "finite_imp_foldSet";
    2.34  val finite_Int = thm "finite_Int";
    2.35  val finite_Pow_iff = thm "finite_Pow_iff";
    2.36  val finite_Prod_UNIV = thm "finite_Prod_UNIV";
    2.37 @@ -87,25 +88,24 @@
    2.38  val finite_imageD = thm "finite_imageD";
    2.39  val finite_imageI = thm "finite_imageI";
    2.40  val finite_imp_cardR = thm "finite_imp_cardR";
    2.41 -val finite_imp_foldSet = thm "finite_imp_foldSet";
    2.42  val finite_induct = thm "finite_induct";
    2.43  val finite_insert = thm "finite_insert";
    2.44  val finite_range_imageI = thm "finite_range_imageI";
    2.45  val finite_subset = thm "finite_subset";
    2.46  val finite_subset_induct = thm "finite_subset_induct";
    2.47  val finite_trancl = thm "finite_trancl";
    2.48 -val foldSet_determ = thm "LC.foldSet_determ";
    2.49 +val foldSet_determ = thm "ACf.foldSet_determ";
    2.50  val foldSet_imp_finite = thm "foldSet_imp_finite";
    2.51  val fold_Un_Int = thm "ACe.fold_Un_Int";
    2.52  val fold_Un_disjoint = thm "ACe.fold_Un_disjoint";
    2.53 -val fold_Un_disjoint2 = thm "ACe.fold_o_Un_disjoint";
    2.54 -val fold_commute = thm "LC.fold_commute";
    2.55 +val fold_Un_disjoint2 = thm "ACe.fold_Un_disjoint";
    2.56 +val fold_commute = thm "ACf.fold_commute";
    2.57  val fold_def = thm "fold_def";
    2.58  val fold_empty = thm "fold_empty";
    2.59 -val fold_equality = thm "LC.fold_equality";
    2.60 -val fold_insert = thm "LC.fold_insert";
    2.61 -val fold_nest_Un_Int = thm "LC.fold_nest_Un_Int";
    2.62 -val fold_nest_Un_disjoint = thm "LC.fold_nest_Un_disjoint";
    2.63 +val fold_equality = thm "ACf.fold_equality";
    2.64 +val fold_insert = thm "ACf.fold_insert";
    2.65 +val fold_nest_Un_Int = thm "ACf.fold_nest_Un_Int";
    2.66 +val fold_nest_Un_disjoint = thm "ACf.fold_nest_Un_disjoint";
    2.67  val n_sub_lemma = thm "n_sub_lemma";
    2.68  val n_subsets = thm "n_subsets";
    2.69  val psubset_card_mono = thm "psubset_card_mono";
     3.1 --- a/src/HOL/Finite_Set.thy	Thu Dec 09 16:45:46 2004 +0100
     3.2 +++ b/src/HOL/Finite_Set.thy	Thu Dec 09 18:30:59 2004 +0100
     3.3 @@ -3,12 +3,7 @@
     3.4      Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
     3.5                  Additions by Jeremy Avigad in Feb 2004
     3.6  
     3.7 -FIXME split up, get rid of LC, define foldSet f g e (instead of just f)
     3.8 -
     3.9 -Possible improvements: simplify card lemmas using the card_eq_setsum.
    3.10 -Unfortunately it appears necessary to define card before foldSet
    3.11 -because the uniqueness proof of foldSet uses card (but only very
    3.12 -elementary properties).
    3.13 +FIXME: define card via fold and derive as many lemmas as possible from fold.
    3.14  *)
    3.15  
    3.16  header {* Finite sets *}
    3.17 @@ -17,7 +12,7 @@
    3.18  imports Divides Power Inductive
    3.19  begin
    3.20  
    3.21 -subsection {* Collection of finite sets *}
    3.22 +subsection {* Definition and basic properties *}
    3.23  
    3.24  consts Finites :: "'a set set"
    3.25  syntax
    3.26 @@ -87,6 +82,49 @@
    3.27    qed
    3.28  qed
    3.29  
    3.30 +text{* Finite sets are the images of initial segments of natural numbers: *}
    3.31 +
    3.32 +lemma finite_imp_nat_seg_image:
    3.33 +assumes fin: "finite A" shows "\<exists> (n::nat) f. A = f ` {i::nat. i<n}"
    3.34 +using fin
    3.35 +proof induct
    3.36 +  case empty
    3.37 +  show ?case
    3.38 +  proof show "\<exists>f. {} = f ` {i::nat. i < 0}" by(simp add:image_def) qed
    3.39 +next
    3.40 +  case (insert a A)
    3.41 +  from insert.hyps obtain n f where "A = f ` {i::nat. i < n}" by blast
    3.42 +  hence "insert a A = (%i. if i<n then f i else a) ` {i. i < n+1}"
    3.43 +    by (auto simp add:image_def Ball_def)
    3.44 +  thus ?case by blast
    3.45 +qed
    3.46 +
    3.47 +lemma nat_seg_image_imp_finite:
    3.48 +  "!!f A. A = f ` {i::nat. i<n} \<Longrightarrow> finite A"
    3.49 +proof (induct n)
    3.50 +  case 0 thus ?case by simp
    3.51 +next
    3.52 +  case (Suc n)
    3.53 +  let ?B = "f ` {i. i < n}"
    3.54 +  have finB: "finite ?B" by(rule Suc.hyps[OF refl])
    3.55 +  show ?case
    3.56 +  proof cases
    3.57 +    assume "\<exists>k<n. f n = f k"
    3.58 +    hence "A = ?B" using Suc.prems by(auto simp:less_Suc_eq)
    3.59 +    thus ?thesis using finB by simp
    3.60 +  next
    3.61 +    assume "\<not>(\<exists> k<n. f n = f k)"
    3.62 +    hence "A = insert (f n) ?B" using Suc.prems by(auto simp:less_Suc_eq)
    3.63 +    thus ?thesis using finB by simp
    3.64 +  qed
    3.65 +qed
    3.66 +
    3.67 +lemma finite_conv_nat_seg_image:
    3.68 +  "finite A = (\<exists> (n::nat) f. A = f ` {i::nat. i<n})"
    3.69 +by(blast intro: finite_imp_nat_seg_image nat_seg_image_imp_finite)
    3.70 +
    3.71 +subsubsection{* Finiteness and set theoretic constructions *}
    3.72 +
    3.73  lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)"
    3.74    -- {* The union of two finite sets is finite. *}
    3.75    by (induct set: Finites) simp_all
    3.76 @@ -177,7 +215,7 @@
    3.77    done
    3.78  
    3.79  
    3.80 -subsubsection {* Image and Inverse Image over Finite Sets *}
    3.81 +text {* Image and Inverse Image over Finite Sets *}
    3.82  
    3.83  lemma finite_imageI[simp]: "finite F ==> finite (h ` F)"
    3.84    -- {* The image of a finite set is finite. *}
    3.85 @@ -229,7 +267,7 @@
    3.86    done
    3.87  
    3.88  
    3.89 -subsubsection {* The finite UNION of finite sets *}
    3.90 +text {* The finite UNION of finite sets *}
    3.91  
    3.92  lemma finite_UN_I: "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)"
    3.93    by (induct set: Finites) simp_all
    3.94 @@ -246,7 +284,7 @@
    3.95    by (blast intro: finite_UN_I finite_subset)
    3.96  
    3.97  
    3.98 -subsubsection {* Sigma of finite sets *}
    3.99 +text {* Sigma of finite sets *}
   3.100  
   3.101  lemma finite_SigmaI [simp]:
   3.102      "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (SIGMA a:A. B a)"
   3.103 @@ -276,7 +314,7 @@
   3.104  qed
   3.105  
   3.106  
   3.107 -subsubsection {* The powerset of a finite set *}
   3.108 +text {* The powerset of a finite set *}
   3.109  
   3.110  lemma finite_Pow_iff [iff]: "finite (Pow A) = finite A"
   3.111  proof
   3.112 @@ -289,6 +327,11 @@
   3.113      by induct (simp_all add: finite_UnI finite_imageI Pow_insert)
   3.114  qed
   3.115  
   3.116 +
   3.117 +lemma finite_UnionD: "finite(\<Union>A) \<Longrightarrow> finite A"
   3.118 +by(blast intro: finite_subset[OF subset_Pow_Union])
   3.119 +
   3.120 +
   3.121  lemma finite_converse [iff]: "finite (r^-1) = finite r"
   3.122    apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
   3.123     apply simp
   3.124 @@ -303,9 +346,8 @@
   3.125    done
   3.126  
   3.127  
   3.128 -subsubsection {* Finiteness of transitive closure *}
   3.129 -
   3.130 -text {* (Thanks to Sidi Ehmety) *}
   3.131 +text {* \paragraph{Finiteness of transitive closure} (Thanks to Sidi
   3.132 +Ehmety) *}
   3.133  
   3.134  lemma finite_Field: "finite r ==> finite (Field r)"
   3.135    -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
   3.136 @@ -334,6 +376,442 @@
   3.137    by (rule finite_SigmaI)
   3.138  
   3.139  
   3.140 +subsection {* A fold functional for finite sets *}
   3.141 +
   3.142 +text {* The intended behaviour is
   3.143 +@{text "fold f g e {x\<^isub>1, ..., x\<^isub>n} = f (g x\<^isub>1) (\<dots> (f (g x\<^isub>n) e)\<dots>)"}
   3.144 +if @{text f} is associative-commutative. For an application of @{text fold}
   3.145 +se the definitions of sums and products over finite sets.
   3.146 +*}
   3.147 +
   3.148 +consts
   3.149 +  foldSet :: "('a => 'a => 'a) => ('b => 'a) => 'a => ('b set \<times> 'a) set"
   3.150 +
   3.151 +inductive "foldSet f g e"
   3.152 +intros
   3.153 +emptyI [intro]: "({}, e) : foldSet f g e"
   3.154 +insertI [intro]: "\<lbrakk> x \<notin> A; (A, y) : foldSet f g e \<rbrakk>
   3.155 + \<Longrightarrow> (insert x A, f (g x) y) : foldSet f g e"
   3.156 +
   3.157 +inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f g e"
   3.158 +
   3.159 +constdefs
   3.160 +  fold :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a"
   3.161 +  "fold f g e A == THE x. (A, x) : foldSet f g e"
   3.162 +
   3.163 +lemma Diff1_foldSet:
   3.164 +  "(A - {x}, y) : foldSet f g e ==> x: A ==> (A, f (g x) y) : foldSet f g e"
   3.165 +by (erule insert_Diff [THEN subst], rule foldSet.intros, auto)
   3.166 +
   3.167 +lemma foldSet_imp_finite: "(A, x) : foldSet f g e ==> finite A"
   3.168 +  by (induct set: foldSet) auto
   3.169 +
   3.170 +lemma finite_imp_foldSet: "finite A ==> EX x. (A, x) : foldSet f g e"
   3.171 +  by (induct set: Finites) auto
   3.172 +
   3.173 +
   3.174 +subsubsection {* Commutative monoids *}
   3.175 +
   3.176 +locale ACf =
   3.177 +  fixes f :: "'a => 'a => 'a"    (infixl "\<cdot>" 70)
   3.178 +  assumes commute: "x \<cdot> y = y \<cdot> x"
   3.179 +    and assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
   3.180 +
   3.181 +locale ACe = ACf +
   3.182 +  fixes e :: 'a
   3.183 +  assumes ident [simp]: "x \<cdot> e = x"
   3.184 +
   3.185 +lemma (in ACf) left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
   3.186 +proof -
   3.187 +  have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp only: commute)
   3.188 +  also have "... = y \<cdot> (z \<cdot> x)" by (simp only: assoc)
   3.189 +  also have "z \<cdot> x = x \<cdot> z" by (simp only: commute)
   3.190 +  finally show ?thesis .
   3.191 +qed
   3.192 +
   3.193 +lemmas (in ACf) AC = assoc commute left_commute
   3.194 +
   3.195 +lemma (in ACe) left_ident [simp]: "e \<cdot> x = x"
   3.196 +proof -
   3.197 +  have "x \<cdot> e = x" by (rule ident)
   3.198 +  thus ?thesis by (subst commute)
   3.199 +qed
   3.200 +
   3.201 +subsubsection{*From @{term foldSet} to @{term fold}*}
   3.202 +
   3.203 +lemma (in ACf) foldSet_determ_aux:
   3.204 +  "!!A x x' h. \<lbrakk> A = h`{i::nat. i<n}; (A,x) : foldSet f g e; (A,x') : foldSet f g e \<rbrakk>
   3.205 +   \<Longrightarrow> x' = x"
   3.206 +proof (induct n)
   3.207 +  case 0 thus ?case by auto
   3.208 +next
   3.209 +  case (Suc n)
   3.210 +  have IH: "!!A x x' h. \<lbrakk>A = h`{i::nat. i<n}; (A,x) \<in> foldSet f g e; (A,x') \<in> foldSet f g e\<rbrakk>
   3.211 +           \<Longrightarrow> x' = x" and card: "A = h`{i. i<Suc n}"
   3.212 +  and Afoldx: "(A, x) \<in> foldSet f g e" and Afoldy: "(A,x') \<in> foldSet f g e" .
   3.213 +  show ?case
   3.214 +  proof cases
   3.215 +    assume "EX k<n. h n = h k"
   3.216 +    hence card': "A = h ` {i. i < n}"
   3.217 +      using card by (auto simp:image_def less_Suc_eq)
   3.218 +    show ?thesis by(rule IH[OF card' Afoldx Afoldy])
   3.219 +  next
   3.220 +    assume new: "\<not>(EX k<n. h n = h k)"
   3.221 +    show ?thesis
   3.222 +    proof (rule foldSet.cases[OF Afoldx])
   3.223 +      assume "(A, x) = ({}, e)"
   3.224 +      thus "x' = x" using Afoldy by (auto)
   3.225 +    next
   3.226 +      fix B b y
   3.227 +      assume eq1: "(A, x) = (insert b B, g b \<cdot> y)"
   3.228 +	and y: "(B,y) \<in> foldSet f g e" and notinB: "b \<notin> B"
   3.229 +      hence A1: "A = insert b B" and x: "x = g b \<cdot> y" by auto
   3.230 +      show ?thesis
   3.231 +      proof (rule foldSet.cases[OF Afoldy])
   3.232 +	assume "(A,x') = ({}, e)"
   3.233 +	thus ?thesis using A1 by auto
   3.234 +      next
   3.235 +	fix C c z
   3.236 +	assume eq2: "(A,x') = (insert c C, g c \<cdot> z)"
   3.237 +	  and z: "(C,z) \<in> foldSet f g e" and notinC: "c \<notin> C"
   3.238 +	hence A2: "A = insert c C" and x': "x' = g c \<cdot> z" by auto
   3.239 +	let ?h = "%i. if h i = b then h n else h i"
   3.240 +	have finA: "finite A" by(rule foldSet_imp_finite[OF Afoldx])
   3.241 +(* move down? *)
   3.242 +	have less: "B = ?h`{i. i<n}" (is "_ = ?r")
   3.243 +	proof
   3.244 +	  show "B \<subseteq> ?r"
   3.245 +	  proof
   3.246 +	    fix u assume "u \<in> B"
   3.247 +	    hence uinA: "u \<in> A" and unotb: "u \<noteq> b" using A1 notinB by blast+
   3.248 +	    then obtain i\<^isub>u where below: "i\<^isub>u < Suc n" and [simp]: "u = h i\<^isub>u"
   3.249 +	      using card by(auto simp:image_def)
   3.250 +	    show "u \<in> ?r"
   3.251 +	    proof cases
   3.252 +	      assume "i\<^isub>u < n"
   3.253 +	      thus ?thesis using unotb by(fastsimp)
   3.254 +	    next
   3.255 +	      assume "\<not> i\<^isub>u < n"
   3.256 +	      with below have [simp]: "i\<^isub>u = n" by arith
   3.257 +	      obtain i\<^isub>k where i\<^isub>k: "i\<^isub>k < Suc n" and [simp]: "b = h i\<^isub>k"
   3.258 +		using A1 card by blast
   3.259 +	      have "i\<^isub>k < n"
   3.260 +	      proof (rule ccontr)
   3.261 +		assume "\<not> i\<^isub>k < n"
   3.262 +		hence "i\<^isub>k = n" using i\<^isub>k by arith
   3.263 +		thus False using unotb by simp
   3.264 +	      qed
   3.265 +	      thus ?thesis by(auto simp add:image_def)
   3.266 +	    qed
   3.267 +	  qed
   3.268 +	next
   3.269 +	  show "?r \<subseteq> B"
   3.270 +	  proof
   3.271 +	    fix u assume "u \<in> ?r"
   3.272 +	    then obtain i\<^isub>u where below: "i\<^isub>u < n" and
   3.273 +              or: "b = h i\<^isub>u \<and> u = h n \<or> h i\<^isub>u \<noteq> b \<and> h i\<^isub>u = u"
   3.274 +	      by(auto simp:image_def)
   3.275 +	    from or show "u \<in> B"
   3.276 +	    proof
   3.277 +	      assume [simp]: "b = h i\<^isub>u \<and> u = h n"
   3.278 +	      have "u \<in> A" using card by auto
   3.279 +              moreover have "u \<noteq> b" using new below by auto
   3.280 +	      ultimately show "u \<in> B" using A1 by blast
   3.281 +	    next
   3.282 +	      assume "h i\<^isub>u \<noteq> b \<and> h i\<^isub>u = u"
   3.283 +	      moreover hence "u \<in> A" using card below by auto
   3.284 +	      ultimately show "u \<in> B" using A1 by blast
   3.285 +	    qed
   3.286 +	  qed
   3.287 +	qed
   3.288 +	show ?thesis
   3.289 +	proof cases
   3.290 +	  assume "b = c"
   3.291 +	  then moreover have "B = C" using A1 A2 notinB notinC by auto
   3.292 +	  ultimately show ?thesis using IH[OF less] y z x x' by auto
   3.293 +	next
   3.294 +	  assume diff: "b \<noteq> c"
   3.295 +	  let ?D = "B - {c}"
   3.296 +	  have B: "B = insert c ?D" and C: "C = insert b ?D"
   3.297 +	    using A1 A2 notinB notinC diff by(blast elim!:equalityE)+
   3.298 +	  have "finite ?D" using finA A1 by simp
   3.299 +	  then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g e"
   3.300 +	    using finite_imp_foldSet by rules
   3.301 +	  moreover have cinB: "c \<in> B" using B by(auto)
   3.302 +	  ultimately have "(B,g c \<cdot> d) \<in> foldSet f g e"
   3.303 +	    by(rule Diff1_foldSet)
   3.304 +	  hence "g c \<cdot> d = y" by(rule IH[OF less y])
   3.305 +          moreover have "g b \<cdot> d = z"
   3.306 +	  proof (rule IH[OF _ z])
   3.307 +	    let ?h = "%i. if h i = c then h n else h i"
   3.308 +	    show "C = ?h`{i. i<n}" (is "_ = ?r")
   3.309 +	    proof
   3.310 +	      show "C \<subseteq> ?r"
   3.311 +	      proof
   3.312 +		fix u assume "u \<in> C"
   3.313 +		hence uinA: "u \<in> A" and unotc: "u \<noteq> c"
   3.314 +		  using A2 notinC by blast+
   3.315 +		then obtain i\<^isub>u where below: "i\<^isub>u < Suc n" and [simp]: "u = h i\<^isub>u"
   3.316 +		  using card by(auto simp:image_def)
   3.317 +		show "u \<in> ?r"
   3.318 +		proof cases
   3.319 +		  assume "i\<^isub>u < n"
   3.320 +		  thus ?thesis using unotc by(fastsimp)
   3.321 +		next
   3.322 +		  assume "\<not> i\<^isub>u < n"
   3.323 +		  with below have [simp]: "i\<^isub>u = n" by arith
   3.324 +		  obtain i\<^isub>k where i\<^isub>k: "i\<^isub>k < Suc n" and [simp]: "c = h i\<^isub>k"
   3.325 +		    using A2 card by blast
   3.326 +		  have "i\<^isub>k < n"
   3.327 +		  proof (rule ccontr)
   3.328 +		    assume "\<not> i\<^isub>k < n"
   3.329 +		    hence "i\<^isub>k = n" using i\<^isub>k by arith
   3.330 +		    thus False using unotc by simp
   3.331 +		  qed
   3.332 +		  thus ?thesis by(auto simp add:image_def)
   3.333 +		qed
   3.334 +	      qed
   3.335 +	    next
   3.336 +	      show "?r \<subseteq> C"
   3.337 +	      proof
   3.338 +		fix u assume "u \<in> ?r"
   3.339 +		then obtain i\<^isub>u where below: "i\<^isub>u < n" and
   3.340 +		  or: "c = h i\<^isub>u \<and> u = h n \<or> h i\<^isub>u \<noteq> c \<and> h i\<^isub>u = u"
   3.341 +		  by(auto simp:image_def)
   3.342 +		from or show "u \<in> C"
   3.343 +		proof
   3.344 +		  assume [simp]: "c = h i\<^isub>u \<and> u = h n"
   3.345 +		  have "u \<in> A" using card by auto
   3.346 +		  moreover have "u \<noteq> c" using new below by auto
   3.347 +		  ultimately show "u \<in> C" using A2 by blast
   3.348 +		next
   3.349 +		  assume "h i\<^isub>u \<noteq> c \<and> h i\<^isub>u = u"
   3.350 +		  moreover hence "u \<in> A" using card below by auto
   3.351 +		  ultimately show "u \<in> C" using A2 by blast
   3.352 +		qed
   3.353 +	      qed
   3.354 +	    qed
   3.355 +	  next
   3.356 +	    show "(C,g b \<cdot> d) \<in> foldSet f g e" using C notinB Dfoldd
   3.357 +	      by fastsimp
   3.358 +	  qed
   3.359 +	  ultimately show ?thesis using x x' by(auto simp:AC)
   3.360 +	qed
   3.361 +      qed
   3.362 +    qed
   3.363 +  qed
   3.364 +qed
   3.365 +
   3.366 +(* The same proof, but using card 
   3.367 +lemma (in ACf) foldSet_determ_aux:
   3.368 +  "!!A x x'. \<lbrakk> card A < n; (A,x) : foldSet f g e; (A,x') : foldSet f g e \<rbrakk>
   3.369 +   \<Longrightarrow> x' = x"
   3.370 +proof (induct n)
   3.371 +  case 0 thus ?case by simp
   3.372 +next
   3.373 +  case (Suc n)
   3.374 +  have IH: "!!A x x'. \<lbrakk>card A < n; (A,x) \<in> foldSet f g e; (A,x') \<in> foldSet f g e\<rbrakk>
   3.375 +           \<Longrightarrow> x' = x" and card: "card A < Suc n"
   3.376 +  and Afoldx: "(A, x) \<in> foldSet f g e" and Afoldy: "(A,x') \<in> foldSet f g e" .
   3.377 +  from card have "card A < n \<or> card A = n" by arith
   3.378 +  thus ?case
   3.379 +  proof
   3.380 +    assume less: "card A < n"
   3.381 +    show ?thesis by(rule IH[OF less Afoldx Afoldy])
   3.382 +  next
   3.383 +    assume cardA: "card A = n"
   3.384 +    show ?thesis
   3.385 +    proof (rule foldSet.cases[OF Afoldx])
   3.386 +      assume "(A, x) = ({}, e)"
   3.387 +      thus "x' = x" using Afoldy by (auto)
   3.388 +    next
   3.389 +      fix B b y
   3.390 +      assume eq1: "(A, x) = (insert b B, g b \<cdot> y)"
   3.391 +	and y: "(B,y) \<in> foldSet f g e" and notinB: "b \<notin> B"
   3.392 +      hence A1: "A = insert b B" and x: "x = g b \<cdot> y" by auto
   3.393 +      show ?thesis
   3.394 +      proof (rule foldSet.cases[OF Afoldy])
   3.395 +	assume "(A,x') = ({}, e)"
   3.396 +	thus ?thesis using A1 by auto
   3.397 +      next
   3.398 +	fix C c z
   3.399 +	assume eq2: "(A,x') = (insert c C, g c \<cdot> z)"
   3.400 +	  and z: "(C,z) \<in> foldSet f g e" and notinC: "c \<notin> C"
   3.401 +	hence A2: "A = insert c C" and x': "x' = g c \<cdot> z" by auto
   3.402 +	have finA: "finite A" by(rule foldSet_imp_finite[OF Afoldx])
   3.403 +	with cardA A1 notinB have less: "card B < n" by simp
   3.404 +	show ?thesis
   3.405 +	proof cases
   3.406 +	  assume "b = c"
   3.407 +	  then moreover have "B = C" using A1 A2 notinB notinC by auto
   3.408 +	  ultimately show ?thesis using IH[OF less] y z x x' by auto
   3.409 +	next
   3.410 +	  assume diff: "b \<noteq> c"
   3.411 +	  let ?D = "B - {c}"
   3.412 +	  have B: "B = insert c ?D" and C: "C = insert b ?D"
   3.413 +	    using A1 A2 notinB notinC diff by(blast elim!:equalityE)+
   3.414 +	  have "finite ?D" using finA A1 by simp
   3.415 +	  then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g e"
   3.416 +	    using finite_imp_foldSet by rules
   3.417 +	  moreover have cinB: "c \<in> B" using B by(auto)
   3.418 +	  ultimately have "(B,g c \<cdot> d) \<in> foldSet f g e"
   3.419 +	    by(rule Diff1_foldSet)
   3.420 +	  hence "g c \<cdot> d = y" by(rule IH[OF less y])
   3.421 +          moreover have "g b \<cdot> d = z"
   3.422 +	  proof (rule IH[OF _ z])
   3.423 +	    show "card C < n" using C cardA A1 notinB finA cinB
   3.424 +	      by(auto simp:card_Diff1_less)
   3.425 +	  next
   3.426 +	    show "(C,g b \<cdot> d) \<in> foldSet f g e" using C notinB Dfoldd
   3.427 +	      by fastsimp
   3.428 +	  qed
   3.429 +	  ultimately show ?thesis using x x' by(auto simp:AC)
   3.430 +	qed
   3.431 +      qed
   3.432 +    qed
   3.433 +  qed
   3.434 +qed
   3.435 +*)
   3.436 +
   3.437 +lemma (in ACf) foldSet_determ:
   3.438 +  "(A, x) : foldSet f g e ==> (A, y) : foldSet f g e ==> y = x"
   3.439 +apply(frule foldSet_imp_finite)
   3.440 +apply(simp add:finite_conv_nat_seg_image)
   3.441 +apply(blast intro: foldSet_determ_aux [rule_format])
   3.442 +done
   3.443 +
   3.444 +lemma (in ACf) fold_equality: "(A, y) : foldSet f g e ==> fold f g e A = y"
   3.445 +  by (unfold fold_def) (blast intro: foldSet_determ)
   3.446 +
   3.447 +text{* The base case for @{text fold}: *}
   3.448 +
   3.449 +lemma fold_empty [simp]: "fold f g e {} = e"
   3.450 +  by (unfold fold_def) blast
   3.451 +
   3.452 +lemma (in ACf) fold_insert_aux: "x \<notin> A ==>
   3.453 +    ((insert x A, v) : foldSet f g e) =
   3.454 +    (EX y. (A, y) : foldSet f g e & v = f (g x) y)"
   3.455 +  apply auto
   3.456 +  apply (rule_tac A1 = A and f1 = f in finite_imp_foldSet [THEN exE])
   3.457 +   apply (fastsimp dest: foldSet_imp_finite)
   3.458 +  apply (blast intro: foldSet_determ)
   3.459 +  done
   3.460 +
   3.461 +text{* The recursion equation for @{text fold}: *}
   3.462 +
   3.463 +lemma (in ACf) fold_insert[simp]:
   3.464 +    "finite A ==> x \<notin> A ==> fold f g e (insert x A) = f (g x) (fold f g e A)"
   3.465 +  apply (unfold fold_def)
   3.466 +  apply (simp add: fold_insert_aux)
   3.467 +  apply (rule the_equality)
   3.468 +  apply (auto intro: finite_imp_foldSet
   3.469 +    cong add: conj_cong simp add: fold_def [symmetric] fold_equality)
   3.470 +  done
   3.471 +
   3.472 +text{* Its definitional form: *}
   3.473 +
   3.474 +corollary (in ACf) fold_insert_def:
   3.475 +    "\<lbrakk> F \<equiv> fold f g e; finite A; x \<notin> A \<rbrakk> \<Longrightarrow> F (insert x A) = f (g x) (F A)"
   3.476 +by(simp)
   3.477 +
   3.478 +declare
   3.479 +  empty_foldSetE [rule del]  foldSet.intros [rule del]
   3.480 +  -- {* Delete rules to do with @{text foldSet} relation. *}
   3.481 +
   3.482 +subsubsection{*Lemmas about @{text fold}*}
   3.483 +
   3.484 +lemma (in ACf) fold_commute:
   3.485 +  "finite A ==> (!!e. f (g x) (fold f g e A) = fold f g (f (g x) e) A)"
   3.486 +  apply (induct set: Finites, simp)
   3.487 +  apply (simp add: left_commute)
   3.488 +  done
   3.489 +
   3.490 +lemma (in ACf) fold_nest_Un_Int:
   3.491 +  "finite A ==> finite B
   3.492 +    ==> fold f g (fold f g e B) A = fold f g (fold f g e (A Int B)) (A Un B)"
   3.493 +  apply (induct set: Finites, simp)
   3.494 +  apply (simp add: fold_commute Int_insert_left insert_absorb)
   3.495 +  done
   3.496 +
   3.497 +lemma (in ACf) fold_nest_Un_disjoint:
   3.498 +  "finite A ==> finite B ==> A Int B = {}
   3.499 +    ==> fold f g e (A Un B) = fold f g (fold f g e B) A"
   3.500 +  by (simp add: fold_nest_Un_Int)
   3.501 +
   3.502 +lemma (in ACf) fold_reindex:
   3.503 +assumes fin: "finite B"
   3.504 +shows "inj_on h B \<Longrightarrow> fold f g e (h ` B) = fold f (g \<circ> h) e B"
   3.505 +using fin apply (induct)
   3.506 + apply simp
   3.507 +apply simp
   3.508 +done
   3.509 +
   3.510 +lemma (in ACe) fold_Un_Int:
   3.511 +  "finite A ==> finite B ==>
   3.512 +    fold f g e A \<cdot> fold f g e B =
   3.513 +    fold f g e (A Un B) \<cdot> fold f g e (A Int B)"
   3.514 +  apply (induct set: Finites, simp)
   3.515 +  apply (simp add: AC insert_absorb Int_insert_left)
   3.516 +  done
   3.517 +
   3.518 +corollary (in ACe) fold_Un_disjoint:
   3.519 +  "finite A ==> finite B ==> A Int B = {} ==>
   3.520 +    fold f g e (A Un B) = fold f g e A \<cdot> fold f g e B"
   3.521 +  by (simp add: fold_Un_Int)
   3.522 +
   3.523 +lemma (in ACe) fold_UN_disjoint:
   3.524 +  "\<lbrakk> finite I; ALL i:I. finite (A i);
   3.525 +     ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {} \<rbrakk>
   3.526 +   \<Longrightarrow> fold f g e (UNION I A) =
   3.527 +       fold f (%i. fold f g e (A i)) e I"
   3.528 +  apply (induct set: Finites, simp, atomize)
   3.529 +  apply (subgoal_tac "ALL i:F. x \<noteq> i")
   3.530 +   prefer 2 apply blast
   3.531 +  apply (subgoal_tac "A x Int UNION F A = {}")
   3.532 +   prefer 2 apply blast
   3.533 +  apply (simp add: fold_Un_disjoint)
   3.534 +  done
   3.535 +
   3.536 +lemma (in ACf) fold_cong:
   3.537 +  "finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold f g a A = fold f h a A"
   3.538 +  apply (subgoal_tac "ALL C. C <= A --> (ALL x:C. g x = h x) --> fold f g a C = fold f h a C")
   3.539 +   apply simp
   3.540 +  apply (erule finite_induct, simp)
   3.541 +  apply (simp add: subset_insert_iff, clarify)
   3.542 +  apply (subgoal_tac "finite C")
   3.543 +   prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
   3.544 +  apply (subgoal_tac "C = insert x (C - {x})")
   3.545 +   prefer 2 apply blast
   3.546 +  apply (erule ssubst)
   3.547 +  apply (drule spec)
   3.548 +  apply (erule (1) notE impE)
   3.549 +  apply (simp add: Ball_def del: insert_Diff_single)
   3.550 +  done
   3.551 +
   3.552 +lemma (in ACe) fold_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
   3.553 +  fold f (%x. fold f (g x) e (B x)) e A =
   3.554 +  fold f (split g) e (SIGMA x:A. B x)"
   3.555 +apply (subst Sigma_def)
   3.556 +apply (subst fold_UN_disjoint)
   3.557 +   apply assumption
   3.558 +  apply simp
   3.559 + apply blast
   3.560 +apply (erule fold_cong)
   3.561 +apply (subst fold_UN_disjoint)
   3.562 +   apply simp
   3.563 +  apply simp
   3.564 + apply blast
   3.565 +apply (simp)
   3.566 +done
   3.567 +
   3.568 +lemma (in ACe) fold_distrib: "finite A \<Longrightarrow>
   3.569 +   fold f (%x. f (g x) (h x)) e A = f (fold f g e A) (fold f h e A)"
   3.570 +apply (erule finite_induct)
   3.571 + apply simp
   3.572 +apply (simp add:AC)
   3.573 +done
   3.574 +
   3.575 +
   3.576  subsection {* Finite cardinality *}
   3.577  
   3.578  text {*
   3.579 @@ -565,286 +1043,415 @@
   3.580    apply (blast elim!: equalityE)
   3.581    done
   3.582  
   3.583 -text {*
   3.584 -  \medskip Relates to equivalence classes.  Based on a theorem of
   3.585 -  F. Kammüller's.  The @{prop "finite C"} premise is redundant.
   3.586 -*}
   3.587 +text {* Relates to equivalence classes.  Based on a theorem of
   3.588 +F. Kammüller's.  *}
   3.589  
   3.590  lemma dvd_partition:
   3.591 -  "finite C ==> finite (Union C) ==>
   3.592 +  "finite (Union C) ==>
   3.593      ALL c : C. k dvd card c ==>
   3.594      (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
   3.595    k dvd card (Union C)"
   3.596 +apply(frule finite_UnionD)
   3.597 +apply(rotate_tac -1)
   3.598    apply (induct set: Finites, simp_all, clarify)
   3.599    apply (subst card_Un_disjoint)
   3.600    apply (auto simp add: dvd_add disjoint_eq_subset_Compl)
   3.601    done
   3.602  
   3.603  
   3.604 -subsection {* A fold functional for finite sets *}
   3.605 +subsubsection {* Theorems about @{text "choose"} *}
   3.606  
   3.607  text {*
   3.608 -  For @{text n} non-negative we have @{text "fold f e {x1, ..., xn} =
   3.609 -  f x1 (... (f xn e))"} where @{text f} is at least left-commutative.
   3.610 +  \medskip Basic theorem about @{text "choose"}.  By Florian
   3.611 +  Kamm\"uller, tidied by LCP.
   3.612  *}
   3.613  
   3.614 -consts
   3.615 -  foldSet :: "('b => 'a => 'a) => 'a => ('b set \<times> 'a) set"
   3.616 -
   3.617 -inductive "foldSet f e"
   3.618 -  intros
   3.619 -    emptyI [intro]: "({}, e) : foldSet f e"
   3.620 -    insertI [intro]: "x \<notin> A ==> (A, y) : foldSet f e ==> (insert x A, f x y) : foldSet f e"
   3.621 -
   3.622 -inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f e"
   3.623 -
   3.624 -constdefs
   3.625 -  fold :: "('b => 'a => 'a) => 'a => 'b set => 'a"
   3.626 -  "fold f e A == THE x. (A, x) : foldSet f e"
   3.627 -
   3.628 -lemma Diff1_foldSet: "(A - {x}, y) : foldSet f e ==> x: A ==> (A, f x y) : foldSet f e"
   3.629 -by (erule insert_Diff [THEN subst], rule foldSet.intros, auto)
   3.630 -
   3.631 -lemma foldSet_imp_finite [simp]: "(A, x) : foldSet f e ==> finite A"
   3.632 -  by (induct set: foldSet) auto
   3.633 -
   3.634 -lemma finite_imp_foldSet: "finite A ==> EX x. (A, x) : foldSet f e"
   3.635 -  by (induct set: Finites) auto
   3.636 -
   3.637 -
   3.638 -subsubsection {* Left-commutative operations *}
   3.639 -
   3.640 -locale LC =
   3.641 -  fixes f :: "'b => 'a => 'a"    (infixl "\<cdot>" 70)
   3.642 -  assumes left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
   3.643 +lemma card_s_0_eq_empty:
   3.644 +    "finite A ==> card {B. B \<subseteq> A & card B = 0} = 1"
   3.645 +  apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
   3.646 +  apply (simp cong add: rev_conj_cong)
   3.647 +  done
   3.648  
   3.649 -lemma (in LC) foldSet_determ_aux:
   3.650 -  "ALL A x. card A < n --> (A, x) : foldSet f e -->
   3.651 -    (ALL y. (A, y) : foldSet f e --> y = x)"
   3.652 -  apply (induct n)
   3.653 -   apply (auto simp add: less_Suc_eq)
   3.654 -  apply (erule foldSet.cases, blast)
   3.655 -  apply (erule foldSet.cases, blast, clarify)
   3.656 -  txt {* force simplification of @{text "card A < card (insert ...)"}. *}
   3.657 -  apply (erule rev_mp)
   3.658 -  apply (simp add: less_Suc_eq_le)
   3.659 -  apply (rule impI)
   3.660 -  apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb")
   3.661 -   apply (subgoal_tac "Aa = Ab")
   3.662 -    prefer 2 apply (blast elim!: equalityE, blast)
   3.663 -  txt {* case @{prop "xa \<notin> xb"}. *}
   3.664 -  apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb : Aa & xa : Ab")
   3.665 -   prefer 2 apply (blast elim!: equalityE, clarify)
   3.666 -  apply (subgoal_tac "Aa = insert xb Ab - {xa}")
   3.667 -   prefer 2 apply blast
   3.668 -  apply (subgoal_tac "card Aa <= card Ab")
   3.669 -   prefer 2
   3.670 -   apply (rule Suc_le_mono [THEN subst])
   3.671 -   apply (simp add: card_Suc_Diff1)
   3.672 -  apply (rule_tac A1 = "Aa - {xb}" and f1 = f in finite_imp_foldSet [THEN exE])
   3.673 -  apply (blast intro: foldSet_imp_finite finite_Diff)
   3.674 -  apply (frule (1) Diff1_foldSet)
   3.675 -  apply (subgoal_tac "ya = f xb x")
   3.676 -   prefer 2 apply (blast del: equalityCE)
   3.677 -  apply (subgoal_tac "(Ab - {xa}, x) : foldSet f e")
   3.678 -   prefer 2 apply simp
   3.679 -  apply (subgoal_tac "yb = f xa x")
   3.680 -   prefer 2 apply (blast del: equalityCE dest: Diff1_foldSet)
   3.681 -  apply (simp (no_asm_simp) add: left_commute)
   3.682 +lemma choose_deconstruct: "finite M ==> x \<notin> M
   3.683 +  ==> {s. s <= insert x M & card(s) = Suc k}
   3.684 +       = {s. s <= M & card(s) = Suc k} Un
   3.685 +         {s. EX t. t <= M & card(t) = k & s = insert x t}"
   3.686 +  apply safe
   3.687 +   apply (auto intro: finite_subset [THEN card_insert_disjoint])
   3.688 +  apply (drule_tac x = "xa - {x}" in spec)
   3.689 +  apply (subgoal_tac "x \<notin> xa", auto)
   3.690 +  apply (erule rev_mp, subst card_Diff_singleton)
   3.691 +  apply (auto intro: finite_subset)
   3.692    done
   3.693  
   3.694 -lemma (in LC) foldSet_determ:
   3.695 -  "(A, x) : foldSet f e ==> (A, y) : foldSet f e ==> y = x"
   3.696 -by (blast intro: foldSet_determ_aux [rule_format])
   3.697 +lemma card_inj_on_le:
   3.698 +    "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B"
   3.699 +apply (subgoal_tac "finite A") 
   3.700 + apply (force intro: card_mono simp add: card_image [symmetric])
   3.701 +apply (blast intro: finite_imageD dest: finite_subset) 
   3.702 +done
   3.703  
   3.704 -lemma (in LC) fold_equality: "(A, y) : foldSet f e ==> fold f e A = y"
   3.705 -  by (unfold fold_def) (blast intro: foldSet_determ)
   3.706 +lemma card_bij_eq:
   3.707 +    "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
   3.708 +       finite A; finite B |] ==> card A = card B"
   3.709 +  by (auto intro: le_anti_sym card_inj_on_le)
   3.710  
   3.711 -lemma fold_empty [simp]: "fold f e {} = e"
   3.712 -  by (unfold fold_def) blast
   3.713 -
   3.714 -lemma (in LC) fold_insert_aux: "x \<notin> A ==>
   3.715 -    ((insert x A, v) : foldSet f e) =
   3.716 -    (EX y. (A, y) : foldSet f e & v = f x y)"
   3.717 -  apply auto
   3.718 -  apply (rule_tac A1 = A and f1 = f in finite_imp_foldSet [THEN exE])
   3.719 -   apply (fastsimp dest: foldSet_imp_finite)
   3.720 -  apply (blast intro: foldSet_determ)
   3.721 +text{*There are as many subsets of @{term A} having cardinality @{term k}
   3.722 + as there are sets obtained from the former by inserting a fixed element
   3.723 + @{term x} into each.*}
   3.724 +lemma constr_bij:
   3.725 +   "[|finite A; x \<notin> A|] ==>
   3.726 +    card {B. EX C. C <= A & card(C) = k & B = insert x C} =
   3.727 +    card {B. B <= A & card(B) = k}"
   3.728 +  apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq)
   3.729 +       apply (auto elim!: equalityE simp add: inj_on_def)
   3.730 +    apply (subst Diff_insert0, auto)
   3.731 +   txt {* finiteness of the two sets *}
   3.732 +   apply (rule_tac [2] B = "Pow (A)" in finite_subset)
   3.733 +   apply (rule_tac B = "Pow (insert x A)" in finite_subset)
   3.734 +   apply fast+
   3.735    done
   3.736  
   3.737 -lemma (in LC) fold_insert[simp]:
   3.738 -    "finite A ==> x \<notin> A ==> fold f e (insert x A) = f x (fold f e A)"
   3.739 -  apply (unfold fold_def)
   3.740 -  apply (simp add: fold_insert_aux)
   3.741 -  apply (rule the_equality)
   3.742 -  apply (auto intro: finite_imp_foldSet
   3.743 -    cong add: conj_cong simp add: fold_def [symmetric] fold_equality)
   3.744 -  done
   3.745 +text {*
   3.746 +  Main theorem: combinatorial statement about number of subsets of a set.
   3.747 +*}
   3.748  
   3.749 -corollary (in LC) fold_insert_def:
   3.750 -    "\<lbrakk> F \<equiv> fold f e; finite A; x \<notin> A \<rbrakk> \<Longrightarrow> F (insert x A) = f x (F A)"
   3.751 -by(simp)
   3.752 -
   3.753 -lemma (in LC) fold_commute:
   3.754 -  "finite A ==> (!!e. f x (fold f e A) = fold f (f x e) A)"
   3.755 -  apply (induct set: Finites, simp)
   3.756 -  apply (simp add: left_commute)
   3.757 -  done
   3.758 -
   3.759 -lemma (in LC) fold_nest_Un_Int:
   3.760 -  "finite A ==> finite B
   3.761 -    ==> fold f (fold f e B) A = fold f (fold f e (A Int B)) (A Un B)"
   3.762 -  apply (induct set: Finites, simp)
   3.763 -  apply (simp add: fold_commute Int_insert_left insert_absorb)
   3.764 +lemma n_sub_lemma:
   3.765 +  "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
   3.766 +  apply (induct k)
   3.767 +   apply (simp add: card_s_0_eq_empty, atomize)
   3.768 +  apply (rotate_tac -1, erule finite_induct)
   3.769 +   apply (simp_all (no_asm_simp) cong add: conj_cong
   3.770 +     add: card_s_0_eq_empty choose_deconstruct)
   3.771 +  apply (subst card_Un_disjoint)
   3.772 +     prefer 4 apply (force simp add: constr_bij)
   3.773 +    prefer 3 apply force
   3.774 +   prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
   3.775 +     finite_subset [of _ "Pow (insert x F)", standard])
   3.776 +  apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
   3.777    done
   3.778  
   3.779 -lemma (in LC) fold_nest_Un_disjoint:
   3.780 -  "finite A ==> finite B ==> A Int B = {}
   3.781 -    ==> fold f e (A Un B) = fold f (fold f e B) A"
   3.782 -  by (simp add: fold_nest_Un_Int)
   3.783 +theorem n_subsets:
   3.784 +    "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
   3.785 +  by (simp add: n_sub_lemma)
   3.786 +
   3.787 +
   3.788 +subsection{* A fold functional for non-empty sets *}
   3.789 +
   3.790 +text{* Does not require start value. *}
   3.791  
   3.792 -declare foldSet_imp_finite [simp del]
   3.793 -    empty_foldSetE [rule del]  foldSet.intros [rule del]
   3.794 -  -- {* Delete rules to do with @{text foldSet} relation. *}
   3.795 +consts
   3.796 +  foldSet1 :: "('a => 'a => 'a) => ('a set \<times> 'a) set"
   3.797 +
   3.798 +inductive "foldSet1 f"
   3.799 +intros
   3.800 +foldSet1_singletonI [intro]: "({a}, a) : foldSet1 f"
   3.801 +foldSet1_insertI [intro]:
   3.802 + "\<lbrakk> (A, x) : foldSet1 f; a \<notin> A; A \<noteq> {} \<rbrakk>
   3.803 +  \<Longrightarrow> (insert a A, f a x) : foldSet1 f"
   3.804  
   3.805 -lemma (in LC) o_closed: "LC(f o g)"
   3.806 -by(insert prems, simp add:LC_def)
   3.807 +constdefs
   3.808 +  fold1 :: "('a => 'a => 'a) => 'a set => 'a"
   3.809 +  "fold1 f A == THE x. (A, x) : foldSet1 f"
   3.810 +
   3.811 +lemma foldSet1_nonempty:
   3.812 + "(A, x) : foldSet1 f \<Longrightarrow> A \<noteq> {}"
   3.813 +by(erule foldSet1.cases, simp_all) 
   3.814 +
   3.815  
   3.816 -lemma (in LC) fold_reindex:
   3.817 -assumes fin: "finite B"
   3.818 -shows "inj_on g B \<Longrightarrow> fold f e (g ` B) = fold (f \<circ> g) e B"
   3.819 -using fin apply (induct)
   3.820 - apply simp
   3.821 -apply simp
   3.822 -apply(simp add:LC.fold_insert[OF o_closed])
   3.823 +inductive_cases empty_foldSet1E [elim!]: "({}, x) : foldSet1 f"
   3.824 +
   3.825 +lemma foldSet1_sing[iff]: "(({a},b) : foldSet1 f) = (a = b)"
   3.826 +apply(rule iffI)
   3.827 + prefer 2 apply fast
   3.828 +apply (erule foldSet1.cases)
   3.829 + apply blast
   3.830 +apply (erule foldSet1.cases)
   3.831 + apply blast
   3.832 +apply blast
   3.833  done
   3.834  
   3.835 -subsubsection {* Commutative monoids *}
   3.836 -
   3.837 -text {*
   3.838 -  We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"}
   3.839 -  instead of @{text "'b => 'a => 'a"}.
   3.840 -*}
   3.841 +lemma Diff1_foldSet1:
   3.842 +  "(A - {x}, y) : foldSet1 f ==> x: A ==> (A, f x y) : foldSet1 f"
   3.843 +by (erule insert_Diff [THEN subst], rule foldSet1.intros,
   3.844 +    auto dest!:foldSet1_nonempty)
   3.845  
   3.846 -locale ACf =
   3.847 -  fixes f :: "'a => 'a => 'a"    (infixl "\<cdot>" 70)
   3.848 -  assumes commute: "x \<cdot> y = y \<cdot> x"
   3.849 -    and assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
   3.850 +lemma foldSet1_imp_finite: "(A, x) : foldSet1 f ==> finite A"
   3.851 +  by (induct set: foldSet1) auto
   3.852  
   3.853 -locale ACe = ACf +
   3.854 -  fixes e :: 'a
   3.855 -  assumes ident [simp]: "x \<cdot> e = x"
   3.856 +lemma finite_nonempty_imp_foldSet1:
   3.857 +  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. (A, x) : foldSet1 f"
   3.858 +  by (induct set: Finites) auto
   3.859  
   3.860 -lemma (in ACf) left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
   3.861 -proof -
   3.862 -  have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp only: commute)
   3.863 -  also have "... = y \<cdot> (z \<cdot> x)" by (simp only: assoc)
   3.864 -  also have "z \<cdot> x = x \<cdot> z" by (simp only: commute)
   3.865 -  finally show ?thesis .
   3.866 -qed
   3.867 -
   3.868 -corollary (in ACf) LC: "LC f"
   3.869 -by(simp add:LC_def left_commute)
   3.870 -
   3.871 -lemmas (in ACf) AC = assoc commute left_commute
   3.872 -
   3.873 -lemma (in ACe) left_ident [simp]: "e \<cdot> x = x"
   3.874 -proof -
   3.875 -  have "x \<cdot> e = x" by (rule ident)
   3.876 -  thus ?thesis by (subst commute)
   3.877 +lemma (in ACf) foldSet1_determ_aux:
   3.878 +  "!!A x y. \<lbrakk> card A < n; (A, x) : foldSet1 f; (A, y) : foldSet1 f \<rbrakk> \<Longrightarrow> y = x"
   3.879 +proof (induct n)
   3.880 +  case 0 thus ?case by simp
   3.881 +next
   3.882 +  case (Suc n)
   3.883 +  have IH: "!!A x y. \<lbrakk>card A < n; (A, x) \<in> foldSet1 f; (A, y) \<in> foldSet1 f\<rbrakk>
   3.884 +           \<Longrightarrow> y = x" and card: "card A < Suc n"
   3.885 +  and Afoldx: "(A, x) \<in> foldSet1 f" and Afoldy: "(A, y) \<in> foldSet1 f" .
   3.886 +  from card have "card A < n \<or> card A = n" by arith
   3.887 +  thus ?case
   3.888 +  proof
   3.889 +    assume less: "card A < n"
   3.890 +    show ?thesis by(rule IH[OF less Afoldx Afoldy])
   3.891 +  next
   3.892 +    assume cardA: "card A = n"
   3.893 +    show ?thesis
   3.894 +    proof (rule foldSet1.cases[OF Afoldx])
   3.895 +      fix a assume "(A, x) = ({a}, a)"
   3.896 +      thus "y = x" using Afoldy by (simp add:foldSet1_sing)
   3.897 +    next
   3.898 +      fix Ax ax x'
   3.899 +      assume eq1: "(A, x) = (insert ax Ax, ax \<cdot> x')"
   3.900 +	and x': "(Ax, x') \<in> foldSet1 f" and notinx: "ax \<notin> Ax"
   3.901 +	and Axnon: "Ax \<noteq> {}"
   3.902 +      hence A1: "A = insert ax Ax" and x: "x = ax \<cdot> x'" by auto
   3.903 +      show ?thesis
   3.904 +      proof (rule foldSet1.cases[OF Afoldy])
   3.905 +	fix ay assume "(A, y) = ({ay}, ay)"
   3.906 +	thus ?thesis using eq1 x' Axnon notinx
   3.907 +	  by (fastsimp simp:foldSet1_sing)
   3.908 +      next
   3.909 +	fix Ay ay y'
   3.910 +	assume eq2: "(A, y) = (insert ay Ay, ay \<cdot> y')"
   3.911 +	  and y': "(Ay, y') \<in> foldSet1 f" and notiny: "ay \<notin> Ay"
   3.912 +	  and Aynon: "Ay \<noteq> {}"
   3.913 +	hence A2: "A = insert ay Ay" and y: "y = ay \<cdot> y'" by auto
   3.914 +	have finA: "finite A" by(rule foldSet1_imp_finite[OF Afoldx])
   3.915 +	with cardA A1 notinx have less: "card Ax < n" by simp
   3.916 +	show ?thesis
   3.917 +	proof cases
   3.918 +	  assume "ax = ay"
   3.919 +	  then moreover have "Ax = Ay" using A1 A2 notinx notiny by auto
   3.920 +	  ultimately show ?thesis using IH[OF less x'] y' eq1 eq2 by auto
   3.921 +	next
   3.922 +	  assume diff: "ax \<noteq> ay"
   3.923 +	  let ?B = "Ax - {ay}"
   3.924 +	  have Ax: "Ax = insert ay ?B" and Ay: "Ay = insert ax ?B"
   3.925 +	    using A1 A2 notinx notiny diff by(blast elim!:equalityE)+
   3.926 +	  show ?thesis
   3.927 +	  proof cases
   3.928 +	    assume "?B = {}"
   3.929 +	    with Ax Ay show ?thesis using x' y' x y by(simp add:commute)
   3.930 +	  next
   3.931 +	    assume Bnon: "?B \<noteq> {}"
   3.932 +	    moreover have "finite ?B" using finA A1 by simp
   3.933 +	    ultimately obtain b where Bfoldb: "(?B,b) \<in> foldSet1 f"
   3.934 +	      using finite_nonempty_imp_foldSet1 by(blast)
   3.935 +	    moreover have ayinAx: "ay \<in> Ax" using Ax by(auto)
   3.936 +	    ultimately have "(Ax,ay\<cdot>b) \<in> foldSet1 f" by(rule Diff1_foldSet1)
   3.937 +	    hence "ay\<cdot>b = x'" by(rule IH[OF less x'])
   3.938 +            moreover have "ax\<cdot>b = y'"
   3.939 +	    proof (rule IH[OF _ y'])
   3.940 +	      show "card Ay < n" using Ay cardA A1 notinx finA ayinAx
   3.941 +		by(auto simp:card_Diff1_less)
   3.942 +	    next
   3.943 +	      show "(Ay,ax\<cdot>b) \<in> foldSet1 f" using Ay notinx Bfoldb Bnon
   3.944 +		by fastsimp
   3.945 +	    qed
   3.946 +	    ultimately show ?thesis using x y by(auto simp:AC)
   3.947 +	  qed
   3.948 +	qed
   3.949 +      qed
   3.950 +    qed
   3.951 +  qed
   3.952  qed
   3.953  
   3.954 -lemma (in ACe) fold_o_Un_Int:
   3.955 -  "finite A ==> finite B ==>
   3.956 -    fold (f o g) e A \<cdot> fold (f o g) e B =
   3.957 -    fold (f o g) e (A Un B) \<cdot> fold (f o g) e (A Int B)"
   3.958 -  apply (induct set: Finites, simp)
   3.959 -  apply (simp add: AC insert_absorb Int_insert_left
   3.960 -    LC.fold_insert [OF LC.intro])
   3.961 -  done
   3.962 +
   3.963 +lemma (in ACf) foldSet1_determ:
   3.964 +  "(A, x) : foldSet1 f ==> (A, y) : foldSet1 f ==> y = x"
   3.965 +by (blast intro: foldSet1_determ_aux [rule_format])
   3.966 +
   3.967 +lemma (in ACf) foldSet1_equality: "(A, y) : foldSet1 f ==> fold1 f A = y"
   3.968 +  by (unfold fold1_def) (blast intro: foldSet1_determ)
   3.969 +
   3.970 +lemma fold1_singleton: "fold1 f {a} = a"
   3.971 +  by (unfold fold1_def) blast
   3.972  
   3.973 -corollary (in ACe) fold_Un_Int:
   3.974 -  "finite A ==> finite B ==>
   3.975 -    fold f e A \<cdot> fold f e B = fold f e (A Un B) \<cdot> fold f e (A Int B)"
   3.976 -  by (rule fold_o_Un_Int[where g = id,simplified])
   3.977 +lemma (in ACf) foldSet1_insert_aux: "x \<notin> A ==> A \<noteq> {} \<Longrightarrow> 
   3.978 +    ((insert x A, v) : foldSet1 f) =
   3.979 +    (EX y. (A, y) : foldSet1 f & v = f x y)"
   3.980 +apply auto
   3.981 +apply (rule_tac A1 = A and f1 = f in finite_nonempty_imp_foldSet1 [THEN exE])
   3.982 +  apply (fastsimp dest: foldSet1_imp_finite)
   3.983 + apply blast
   3.984 +apply (blast intro: foldSet1_determ)
   3.985 +done
   3.986  
   3.987 -corollary (in ACe) fold_o_Un_disjoint:
   3.988 -  "finite A ==> finite B ==> A Int B = {} ==>
   3.989 -    fold (f o g) e (A Un B) = fold (f o g) e A \<cdot> fold (f o g) e B"
   3.990 -  by (simp add: fold_o_Un_Int)
   3.991 +lemma (in ACf) fold1_insert:
   3.992 +  "finite A ==> x \<notin> A ==> A \<noteq> {} \<Longrightarrow> fold1 f (insert x A) = f x (fold1 f A)"
   3.993 +apply (unfold fold1_def)
   3.994 +apply (simp add: foldSet1_insert_aux)
   3.995 +apply (rule the_equality)
   3.996 +apply (auto intro: finite_nonempty_imp_foldSet1
   3.997 +    cong add: conj_cong simp add: fold1_def [symmetric] foldSet1_equality)
   3.998 +done
   3.999  
  3.1000 -corollary (in ACe) fold_Un_disjoint:
  3.1001 -  "finite A ==> finite B ==> A Int B = {} ==>
  3.1002 -    fold f e (A Un B) = fold f e A \<cdot> fold f e B"
  3.1003 -  by (simp add: fold_Un_Int)
  3.1004 +locale ACIf = ACf +
  3.1005 +  assumes idem: "x \<cdot> x = x"
  3.1006  
  3.1007 -lemma (in ACe) fold_o_UN_disjoint:
  3.1008 -  "\<lbrakk> finite I; ALL i:I. finite (A i);
  3.1009 -     ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {} \<rbrakk>
  3.1010 -   \<Longrightarrow> fold (f o g) e (UNION I A) =
  3.1011 -       fold (f o (%i. fold (f o g) e (A i))) e I"
  3.1012 -  apply (induct set: Finites, simp, atomize)
  3.1013 -  apply (subgoal_tac "ALL i:F. x \<noteq> i")
  3.1014 -   prefer 2 apply blast
  3.1015 -  apply (subgoal_tac "A x Int UNION F A = {}")
  3.1016 -   prefer 2 apply blast
  3.1017 -  apply (simp add: fold_o_Un_disjoint LC.fold_insert[OF LC.o_closed[OF LC]])
  3.1018 -  done
  3.1019 +lemma (in ACIf) fold1_insert2:
  3.1020 +assumes finA: "finite A" and nonA: "A \<noteq> {}"
  3.1021 +shows "fold1 f (insert a A) = f a (fold1 f A)"
  3.1022 +proof cases
  3.1023 +  assume "a \<in> A"
  3.1024 +  then obtain B where A: "A = insert a B" and disj: "a \<notin> B"
  3.1025 +    by(blast dest: mk_disjoint_insert)
  3.1026 +  show ?thesis
  3.1027 +  proof cases
  3.1028 +    assume "B = {}"
  3.1029 +    thus ?thesis using A by(simp add:idem fold1_singleton)
  3.1030 +  next
  3.1031 +    assume nonB: "B \<noteq> {}"
  3.1032 +    from finA A have finB: "finite B" by(blast intro: finite_subset)
  3.1033 +    have "fold1 f (insert a A) = fold1 f (insert a B)" using A by simp
  3.1034 +    also have "\<dots> = f a (fold1 f B)"
  3.1035 +      using finB nonB disj by(simp add: fold1_insert)
  3.1036 +    also have "\<dots> = f a (fold1 f A)"
  3.1037 +      using A finB nonB disj by(simp add:idem fold1_insert assoc[symmetric])
  3.1038 +    finally show ?thesis .
  3.1039 +  qed
  3.1040 +next
  3.1041 +  assume "a \<notin> A"
  3.1042 +  with finA nonA show ?thesis by(simp add:fold1_insert)
  3.1043 +qed
  3.1044 +
  3.1045  
  3.1046 -lemma (in ACf) fold_cong:
  3.1047 -  "finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold (f o g) a A = fold (f o h) a A"
  3.1048 -  apply (subgoal_tac "ALL C. C <= A --> (ALL x:C. g x = h x) --> fold (f o g) a C = fold (f o h) a C")
  3.1049 -   apply simp
  3.1050 -  apply (erule finite_induct, simp)
  3.1051 -  apply (simp add: subset_insert_iff, clarify)
  3.1052 -  apply (subgoal_tac "finite C")
  3.1053 -   prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
  3.1054 -  apply (subgoal_tac "C = insert x (C - {x})")
  3.1055 -   prefer 2 apply blast
  3.1056 -  apply (erule ssubst)
  3.1057 -  apply (drule spec)
  3.1058 -  apply (erule (1) notE impE)
  3.1059 -  apply (fold o_def)
  3.1060 -  apply (simp add: Ball_def LC.fold_insert[OF LC.o_closed[OF LC]]
  3.1061 -              del: insert_Diff_single)
  3.1062 -  done
  3.1063 +text{* Now the recursion rules for definitions: *}
  3.1064 +
  3.1065 +lemma fold1_singleton_def: "g \<equiv> fold1 f \<Longrightarrow> g {a} = a"
  3.1066 +by(simp add:fold1_singleton)
  3.1067 +
  3.1068 +lemma (in ACf) fold1_insert_def:
  3.1069 +  "\<lbrakk> g \<equiv> fold1 f; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)"
  3.1070 +by(simp add:fold1_insert)
  3.1071 +
  3.1072 +lemma (in ACIf) fold1_insert2_def:
  3.1073 +  "\<lbrakk> g \<equiv> fold1 f; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)"
  3.1074 +by(simp add:fold1_insert2)
  3.1075 +
  3.1076  
  3.1077 -lemma (in ACe) fold_o_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
  3.1078 -fold (f o (%x. fold (f o g x) e (B x))) e A =
  3.1079 -fold (f o (split g)) e (SIGMA x:A. B x)"
  3.1080 -apply (subst Sigma_def)
  3.1081 -apply (subst fold_o_UN_disjoint)
  3.1082 -   apply assumption
  3.1083 -  apply simp
  3.1084 - apply blast
  3.1085 -apply (erule fold_cong)
  3.1086 -apply (subst fold_o_UN_disjoint)
  3.1087 -   apply simp
  3.1088 -  apply simp
  3.1089 - apply blast
  3.1090 -apply (simp add: LC.fold_insert [OF LC.o_closed[OF LC]])
  3.1091 -apply(simp add:o_def)
  3.1092 +subsection{*Min and Max*}
  3.1093 +
  3.1094 +text{* As an application of @{text fold1} we define the minimal and
  3.1095 +maximal element of a (non-empty) set over a linear order. First we
  3.1096 +show that @{text min} and @{text max} are ACI: *}
  3.1097 +
  3.1098 +lemma ACf_min: "ACf(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  3.1099 +apply(rule ACf.intro)
  3.1100 +apply(auto simp:min_def)
  3.1101 +done
  3.1102 +
  3.1103 +lemma ACIf_min: "ACIf(min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  3.1104 +apply(rule ACIf.intro[OF ACf_min])
  3.1105 +apply(rule ACIf_axioms.intro)
  3.1106 +apply(auto simp:min_def)
  3.1107  done
  3.1108  
  3.1109 -lemma (in ACe) fold_o_distrib: "finite A \<Longrightarrow>
  3.1110 -   fold (f o (%x. f (g x) (h x))) e A =
  3.1111 -   f (fold (f o g) e A) (fold (f o h) e A)"
  3.1112 -apply (erule finite_induct)
  3.1113 - apply simp
  3.1114 -apply(simp add: LC.fold_insert[OF LC.o_closed[OF LC]] del:o_apply)
  3.1115 -apply(subgoal_tac "(%x. f(g x)) = (%u ua. f ua (g u))")
  3.1116 - prefer 2 apply(rule ext, rule ext, simp add:AC)
  3.1117 -apply(subgoal_tac "(%x. f(h x)) = (%u ua. f ua (h u))")
  3.1118 - prefer 2 apply(rule ext, rule ext, simp add:AC)
  3.1119 -apply (simp add:AC o_def)
  3.1120 +lemma ACf_max: "ACf(max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  3.1121 +apply(rule ACf.intro)
  3.1122 +apply(auto simp:max_def)
  3.1123 +done
  3.1124 +
  3.1125 +lemma ACIf_max: "ACIf(max:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  3.1126 +apply(rule ACIf.intro[OF ACf_max])
  3.1127 +apply(rule ACIf_axioms.intro)
  3.1128 +apply(auto simp:max_def)
  3.1129  done
  3.1130  
  3.1131 +text{* Now we make the definitions: *}
  3.1132 +
  3.1133 +constdefs
  3.1134 +  Min :: "('a::linorder)set => 'a"
  3.1135 +  "Min  ==  fold1 min"
  3.1136 +
  3.1137 +  Max :: "('a::linorder)set => 'a"
  3.1138 +  "Max  ==  fold1 max"
  3.1139 +
  3.1140 +text{* Now we instantiate the recursiuon equations and declare them
  3.1141 +simplification rules: *}
  3.1142 +
  3.1143 +declare
  3.1144 +  fold1_singleton_def[OF Min_def, simp]
  3.1145 +  ACIf.fold1_insert2_def[OF ACIf_min Min_def, simp]
  3.1146 +  fold1_singleton_def[OF Max_def, simp]
  3.1147 +  ACIf.fold1_insert2_def[OF ACIf_max Max_def, simp]
  3.1148 +
  3.1149 +text{* Now we prove some properties by induction: *}
  3.1150 +
  3.1151 +lemma Min_in [simp]:
  3.1152 +  assumes a: "finite S"
  3.1153 +  shows "S \<noteq> {} \<Longrightarrow> Min S \<in> S"
  3.1154 +using a
  3.1155 +proof induct
  3.1156 +  case empty thus ?case by simp
  3.1157 +next
  3.1158 +  case (insert x S)
  3.1159 +  show ?case
  3.1160 +  proof cases
  3.1161 +    assume "S = {}" thus ?thesis by simp
  3.1162 +  next
  3.1163 +    assume "S \<noteq> {}" thus ?thesis using insert by (simp add:min_def)
  3.1164 +  qed
  3.1165 +qed
  3.1166 +
  3.1167 +lemma Min_le [simp]:
  3.1168 +  assumes a: "finite S"
  3.1169 +  shows "\<lbrakk> S \<noteq> {}; x \<in> S \<rbrakk> \<Longrightarrow> Min S \<le> x"
  3.1170 +using a
  3.1171 +proof induct
  3.1172 +  case empty thus ?case by simp
  3.1173 +next
  3.1174 +  case (insert y S)
  3.1175 +  show ?case
  3.1176 +  proof cases
  3.1177 +    assume "S = {}" thus ?thesis using insert by simp
  3.1178 +  next
  3.1179 +    assume "S \<noteq> {}" thus ?thesis using insert by (auto simp add:min_def)
  3.1180 +  qed
  3.1181 +qed
  3.1182 +
  3.1183 +lemma Max_in [simp]:
  3.1184 +  assumes a: "finite S"
  3.1185 +  shows "S \<noteq> {} \<Longrightarrow> Max S \<in> S"
  3.1186 +using a
  3.1187 +proof induct
  3.1188 +  case empty thus ?case by simp
  3.1189 +next
  3.1190 +  case (insert x S)
  3.1191 +  show ?case
  3.1192 +  proof cases
  3.1193 +    assume "S = {}" thus ?thesis by simp
  3.1194 +  next
  3.1195 +    assume "S \<noteq> {}" thus ?thesis using insert by (simp add:max_def)
  3.1196 +  qed
  3.1197 +qed
  3.1198 +
  3.1199 +lemma Max_le [simp]:
  3.1200 +  assumes a: "finite S"
  3.1201 +  shows "\<lbrakk> S \<noteq> {}; x \<in> S \<rbrakk> \<Longrightarrow> x \<le> Max S"
  3.1202 +using a
  3.1203 +proof induct
  3.1204 +  case empty thus ?case by simp
  3.1205 +next
  3.1206 +  case (insert y S)
  3.1207 +  show ?case
  3.1208 +  proof cases
  3.1209 +    assume "S = {}" thus ?thesis using insert by simp
  3.1210 +  next
  3.1211 +    assume "S \<noteq> {}" thus ?thesis using insert by (auto simp add:max_def)
  3.1212 +  qed
  3.1213 +qed
  3.1214 +
  3.1215  
  3.1216  subsection {* Generalized summation over a set *}
  3.1217  
  3.1218  constdefs
  3.1219    setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
  3.1220 -  "setsum f A == if finite A then fold (op + o f) 0 A else 0"
  3.1221 +  "setsum f A == if finite A then fold (op +) f 0 A else 0"
  3.1222  
  3.1223  text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
  3.1224  written @{text"\<Sum>x\<in>A. e"}. *}
  3.1225 @@ -874,14 +1481,26 @@
  3.1226    "SUM x|P. t" => "setsum (%x. t) {x. P}"
  3.1227    "\<Sum>x|P. t" => "setsum (%x. t) {x. P}"
  3.1228  
  3.1229 +text{* Finally we abbreviate @{term"\<Sum>x\<in>A. x"} by @{text"\<Sum>A"}. *}
  3.1230 +
  3.1231 +syntax
  3.1232 +  "_Setsum" :: "'a set => 'a::comm_monoid_mult"  ("\<Sum>_" [1000] 999)
  3.1233 +
  3.1234 +parse_translation {*
  3.1235 +  let
  3.1236 +    fun Setsum_tr [A] = Syntax.const "setsum" $ Abs ("", dummyT, Bound 0) $ A
  3.1237 +  in [("_Setsum", Setsum_tr)] end;
  3.1238 +*}
  3.1239 +
  3.1240  print_translation {*
  3.1241  let
  3.1242 -  fun setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) $ Abs(y,Ty,P)] = 
  3.1243 -    (if x<>y then raise Match
  3.1244 -     else let val x' = Syntax.mark_bound x
  3.1245 -              val t' = subst_bound(x',t)
  3.1246 -              val P' = subst_bound(x',P)
  3.1247 -          in Syntax.const "_qsetsum" $ Syntax.mark_bound x $ P' $ t' end)
  3.1248 +  fun setsum_tr' [Abs(_,_,Bound 0), A] = Syntax.const "_Setsum" $ A
  3.1249 +    | setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) $ Abs(y,Ty,P)] = 
  3.1250 +       if x<>y then raise Match
  3.1251 +       else let val x' = Syntax.mark_bound x
  3.1252 +                val t' = subst_bound(x',t)
  3.1253 +                val P' = subst_bound(x',P)
  3.1254 +            in Syntax.const "_qsetsum" $ Syntax.mark_bound x $ P' $ t' end
  3.1255  in
  3.1256  [("setsum", setsum_tr')]
  3.1257  end
  3.1258 @@ -895,38 +1514,34 @@
  3.1259  lemma ACe_add: "ACe (op +) (0::'a::comm_monoid_add)"
  3.1260  by(fastsimp intro: ACe.intro ACe_axioms.intro ACf_add)
  3.1261  
  3.1262 -corollary LC_add_o: "LC(op + o f :: 'a \<Rightarrow> 'b::comm_monoid_add \<Rightarrow> 'b)"
  3.1263 -by(rule LC.o_closed[OF ACf.LC[OF ACf_add]])
  3.1264 -
  3.1265  lemma setsum_empty [simp]: "setsum f {} = 0"
  3.1266    by (simp add: setsum_def)
  3.1267  
  3.1268  lemma setsum_insert [simp]:
  3.1269      "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
  3.1270 -  by (simp add: setsum_def LC.fold_insert [OF LC_add_o])
  3.1271 +  by (simp add: setsum_def ACf.fold_insert [OF ACf_add])
  3.1272  
  3.1273  lemma setsum_reindex:
  3.1274 -     "finite B ==> inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B"
  3.1275 -by (simp add: setsum_def LC.fold_reindex[OF LC_add_o] o_assoc)
  3.1276 +     "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B"
  3.1277 +by(auto simp add: setsum_def ACf.fold_reindex[OF ACf_add] dest!:finite_imageD)
  3.1278  
  3.1279  lemma setsum_reindex_id:
  3.1280 -     "finite B ==> inj_on f B ==> setsum f B = setsum id (f ` B)"
  3.1281 -by (auto simp add: setsum_reindex id_o)
  3.1282 +     "inj_on f B ==> setsum f B = setsum id (f ` B)"
  3.1283 +by (auto simp add: setsum_reindex)
  3.1284  
  3.1285  lemma setsum_cong:
  3.1286    "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
  3.1287  by(fastsimp simp: setsum_def intro: ACf.fold_cong[OF ACf_add])
  3.1288  
  3.1289  lemma setsum_reindex_cong:
  3.1290 -     "[|finite A; inj_on f A; B = f ` A; !!a. g a = h (f a)|] 
  3.1291 +     "[|inj_on f A; B = f ` A; !!a. g a = h (f a)|] 
  3.1292        ==> setsum h B = setsum g A"
  3.1293    by (simp add: setsum_reindex cong: setsum_cong)
  3.1294  
  3.1295  lemma setsum_0: "setsum (%i. 0) A = 0"
  3.1296 -  apply (case_tac "finite A")
  3.1297 -   prefer 2 apply (simp add: setsum_def)
  3.1298 -  apply (erule finite_induct, auto)
  3.1299 -  done
  3.1300 +apply (clarsimp simp: setsum_def)
  3.1301 +apply (erule finite_induct, auto simp:ACf.fold_insert [OF ACf_add])
  3.1302 +done
  3.1303  
  3.1304  lemma setsum_0': "ALL a:F. f a = 0 ==> setsum f F = 0"
  3.1305    apply (subgoal_tac "setsum f F = setsum (%x. 0) F")
  3.1306 @@ -938,10 +1553,10 @@
  3.1307    -- {* Could allow many @{text "card"} proofs to be simplified. *}
  3.1308    by (induct set: Finites) auto
  3.1309  
  3.1310 -lemma setsum_Un_Int: "finite A ==> finite B
  3.1311 -    ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
  3.1312 +lemma setsum_Un_Int: "finite A ==> finite B ==>
  3.1313 +  setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
  3.1314    -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
  3.1315 -by(simp add: setsum_def ACe.fold_o_Un_Int[OF ACe_add,symmetric])
  3.1316 +by(simp add: setsum_def ACe.fold_Un_Int[OF ACe_add,symmetric])
  3.1317  
  3.1318  lemma setsum_Un_disjoint: "finite A ==> finite B
  3.1319    ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
  3.1320 @@ -951,7 +1566,7 @@
  3.1321      "finite I ==> (ALL i:I. finite (A i)) ==>
  3.1322          (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  3.1323        setsum f (UNION I A) = setsum (%i. setsum f (A i)) I"
  3.1324 -by(simp add: setsum_def ACe.fold_o_UN_disjoint[OF ACe_add] cong: setsum_cong)
  3.1325 +by(simp add: setsum_def ACe.fold_UN_disjoint[OF ACe_add] cong: setsum_cong)
  3.1326  
  3.1327  
  3.1328  lemma setsum_Union_disjoint:
  3.1329 @@ -965,7 +1580,7 @@
  3.1330  lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
  3.1331      (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) =
  3.1332      (\<Sum>z\<in>(SIGMA x:A. B x). f (fst z) (snd z))"
  3.1333 -by(simp add:setsum_def ACe.fold_o_Sigma[OF ACe_add] split_def cong:setsum_cong)
  3.1334 +by(simp add:setsum_def ACe.fold_Sigma[OF ACe_add] split_def cong:setsum_cong)
  3.1335  
  3.1336  lemma setsum_cartesian_product: "finite A ==> finite B ==>
  3.1337      (\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) =
  3.1338 @@ -973,7 +1588,7 @@
  3.1339    by (erule setsum_Sigma, auto)
  3.1340  
  3.1341  lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
  3.1342 -by(simp add:setsum_def ACe.fold_o_distrib[OF ACe_add])
  3.1343 +by(simp add:setsum_def ACe.fold_distrib[OF ACe_add])
  3.1344  
  3.1345  
  3.1346  subsubsection {* Properties in more restricted classes of structures *}
  3.1347 @@ -1198,7 +1813,7 @@
  3.1348  
  3.1349  constdefs
  3.1350    setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult"
  3.1351 -  "setprod f A == if finite A then fold (op * o f) 1 A else 1"
  3.1352 +  "setprod f A == if finite A then fold (op *) f 1 A else 1"
  3.1353  
  3.1354  syntax
  3.1355    "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_:_. _)" [0, 51, 10] 10)
  3.1356 @@ -1210,6 +1825,23 @@
  3.1357  translations
  3.1358    "\<Prod>i:A. b" == "setprod (%i. b) A"  -- {* Beware of argument permutation! *}
  3.1359  
  3.1360 +syntax
  3.1361 +  "_Setprod" :: "'a set => 'a::comm_monoid_mult"  ("\<Prod>_" [1000] 999)
  3.1362 +
  3.1363 +parse_translation {*
  3.1364 +  let
  3.1365 +    fun Setprod_tr [A] = Syntax.const "setprod" $ Abs ("", dummyT, Bound 0) $ A
  3.1366 +  in [("_Setprod", Setprod_tr)] end;
  3.1367 +*}
  3.1368 +print_translation {*
  3.1369 +let fun setprod_tr' [Abs(x,Tx,t), A] =
  3.1370 +    if t = Bound 0 then Syntax.const "_Setprod" $ A else raise Match
  3.1371 +in
  3.1372 +[("setprod", setprod_tr')]
  3.1373 +end
  3.1374 +*}
  3.1375 +
  3.1376 +
  3.1377  text{* Instantiation of locales: *}
  3.1378  
  3.1379  lemma ACf_mult: "ACf (op * :: 'a::comm_monoid_mult \<Rightarrow> 'a \<Rightarrow> 'a)"
  3.1380 @@ -1218,31 +1850,27 @@
  3.1381  lemma ACe_mult: "ACe (op *) (1::'a::comm_monoid_mult)"
  3.1382  by(fastsimp intro: ACe.intro ACe_axioms.intro ACf_mult)
  3.1383  
  3.1384 -corollary LC_mult_o: "LC(op * o f :: 'a \<Rightarrow> 'b::comm_monoid_mult \<Rightarrow> 'b)"
  3.1385 -by(rule LC.o_closed[OF ACf.LC[OF ACf_mult]])
  3.1386 -
  3.1387  lemma setprod_empty [simp]: "setprod f {} = 1"
  3.1388    by (auto simp add: setprod_def)
  3.1389  
  3.1390  lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
  3.1391      setprod f (insert a A) = f a * setprod f A"
  3.1392 -by (simp add: setprod_def LC.fold_insert [OF LC_mult_o])
  3.1393 +by (simp add: setprod_def ACf.fold_insert [OF ACf_mult])
  3.1394  
  3.1395  lemma setprod_reindex:
  3.1396 -     "finite B ==> inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
  3.1397 -by (simp add: setprod_def LC.fold_reindex[OF LC_mult_o] o_assoc)
  3.1398 +     "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
  3.1399 +by(auto simp: setprod_def ACf.fold_reindex[OF ACf_mult] dest!:finite_imageD)
  3.1400  
  3.1401 -lemma setprod_reindex_id: "finite B ==> inj_on f B ==>
  3.1402 -    setprod f B = setprod id (f ` B)"
  3.1403 -by (auto simp add: setprod_reindex id_o)
  3.1404 +lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
  3.1405 +by (auto simp add: setprod_reindex)
  3.1406  
  3.1407  lemma setprod_cong:
  3.1408    "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
  3.1409  by(fastsimp simp: setprod_def intro: ACf.fold_cong[OF ACf_mult])
  3.1410  
  3.1411 -lemma setprod_reindex_cong: "finite A ==> inj_on f A ==>
  3.1412 +lemma setprod_reindex_cong: "inj_on f A ==>
  3.1413      B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
  3.1414 -  by (frule setprod_reindex, assumption, simp)
  3.1415 +  by (frule setprod_reindex, simp)
  3.1416  
  3.1417  
  3.1418  lemma setprod_1: "setprod (%i. 1) A = 1"
  3.1419 @@ -1259,7 +1887,7 @@
  3.1420  
  3.1421  lemma setprod_Un_Int: "finite A ==> finite B
  3.1422      ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
  3.1423 -by(simp add: setprod_def ACe.fold_o_Un_Int[OF ACe_mult,symmetric])
  3.1424 +by(simp add: setprod_def ACe.fold_Un_Int[OF ACe_mult,symmetric])
  3.1425  
  3.1426  lemma setprod_Un_disjoint: "finite A ==> finite B
  3.1427    ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
  3.1428 @@ -1269,7 +1897,7 @@
  3.1429      "finite I ==> (ALL i:I. finite (A i)) ==>
  3.1430          (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  3.1431        setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
  3.1432 -by(simp add: setprod_def ACe.fold_o_UN_disjoint[OF ACe_mult] cong: setprod_cong)
  3.1433 +by(simp add: setprod_def ACe.fold_UN_disjoint[OF ACe_mult] cong: setprod_cong)
  3.1434  
  3.1435  lemma setprod_Union_disjoint:
  3.1436    "finite C ==> (ALL A:C. finite A) ==>
  3.1437 @@ -1282,7 +1910,7 @@
  3.1438  lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
  3.1439      (\<Prod>x:A. (\<Prod>y: B x. f x y)) =
  3.1440      (\<Prod>z:(SIGMA x:A. B x). f (fst z) (snd z))"
  3.1441 -by(simp add:setprod_def ACe.fold_o_Sigma[OF ACe_mult] split_def cong:setprod_cong)
  3.1442 +by(simp add:setprod_def ACe.fold_Sigma[OF ACe_mult] split_def cong:setprod_cong)
  3.1443  
  3.1444  lemma setprod_cartesian_product: "finite A ==> finite B ==>
  3.1445      (\<Prod>x:A. (\<Prod>y: B. f x y)) =
  3.1446 @@ -1291,7 +1919,7 @@
  3.1447  
  3.1448  lemma setprod_timesf:
  3.1449    "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
  3.1450 -by(simp add:setprod_def ACe.fold_o_distrib[OF ACe_mult])
  3.1451 +by(simp add:setprod_def ACe.fold_distrib[OF ACe_mult])
  3.1452  
  3.1453  
  3.1454  subsubsection {* Properties in more restricted classes of structures *}
  3.1455 @@ -1392,319 +2020,4 @@
  3.1456    apply (subst divide_inverse, auto)
  3.1457    done
  3.1458  
  3.1459 -
  3.1460 -subsection{* Min and Max of finite linearly ordered sets *}
  3.1461 -
  3.1462 -consts
  3.1463 -  foldSet1 :: "('a => 'a => 'a) => ('a set \<times> 'a) set"
  3.1464 -
  3.1465 -inductive "foldSet1 f"
  3.1466 -intros
  3.1467 -fold1_singletonI [intro]: "({a}, a) : foldSet1 f"
  3.1468 -fold1_insertI [intro]:
  3.1469 - "\<lbrakk> (A, x) : foldSet1 f; a \<notin> A; A \<noteq> {} \<rbrakk>
  3.1470 -  \<Longrightarrow> (insert a A, f a x) : foldSet1 f"
  3.1471 -
  3.1472 -constdefs
  3.1473 -  fold1 :: "('a => 'a => 'a) => 'a set => 'a"
  3.1474 -  "fold1 f A == THE x. (A, x) : foldSet1 f"
  3.1475 -
  3.1476 -lemma foldSet1_nonempty:
  3.1477 - "(A, x) : foldSet1 f \<Longrightarrow> A \<noteq> {}"
  3.1478 -by(erule foldSet1.cases, simp_all) 
  3.1479 -
  3.1480 -
  3.1481 -inductive_cases empty_foldSet1E [elim!]: "({}, x) : foldSet1 f"
  3.1482 -
  3.1483 -lemma foldSet1_sing[iff]: "(({a},b) : foldSet1 f) = (a = b)"
  3.1484 -apply(rule iffI)
  3.1485 - prefer 2 apply fast
  3.1486 -apply (erule foldSet1.cases)
  3.1487 - apply blast
  3.1488 -apply (erule foldSet1.cases)
  3.1489 - apply blast
  3.1490 -apply blast
  3.1491 -done
  3.1492 -
  3.1493 -lemma Diff1_foldSet1:
  3.1494 -  "(A - {x}, y) : foldSet1 f ==> x: A ==> (A, f x y) : foldSet1 f"
  3.1495 -by (erule insert_Diff [THEN subst], rule foldSet1.intros,
  3.1496 -    auto dest!:foldSet1_nonempty)
  3.1497 -
  3.1498 -lemma foldSet_imp_finite [simp]: "(A, x) : foldSet1 f ==> finite A"
  3.1499 -  by (induct set: foldSet1) auto
  3.1500 -
  3.1501 -lemma finite_nonempty_imp_foldSet1:
  3.1502 -  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. (A, x) : foldSet1 f"
  3.1503 -  by (induct set: Finites) auto
  3.1504 -
  3.1505 -lemma lem: "(A \<subseteq> {a}) = (A = {} \<or> A = {a})"
  3.1506 -by blast
  3.1507 -
  3.1508 -(* FIXME structured proof to avoid ML hack and speed things up *)
  3.1509 -ML"simp_depth_limit := 3"
  3.1510 -lemma (in ACf) foldSet1_determ_aux:
  3.1511 -  "ALL A x. card A < n --> (A, x) : foldSet1 f -->
  3.1512 -    (ALL y. (A, y) : foldSet1 f --> y = x)"
  3.1513 -apply (induct n)
  3.1514 - apply (auto simp add: less_Suc_eq)
  3.1515 -apply (erule foldSet1.cases)
  3.1516 - apply (simp add:foldSet1_sing)
  3.1517 -apply (erule foldSet1.cases)
  3.1518 - apply (fastsimp simp:foldSet1_sing lem)
  3.1519 -apply (clarify)
  3.1520 -  txt {* force simplification of @{text "card A < card (insert ...)"}. *}
  3.1521 -apply (erule rev_mp)
  3.1522 -apply (simp add: less_Suc_eq_le)
  3.1523 -apply (rule impI)
  3.1524 -apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb")
  3.1525 - apply (subgoal_tac "Aa = Ab")
  3.1526 -  prefer 2 apply (blast elim!: equalityE, blast)
  3.1527 -  txt {* case @{prop "xa \<notin> xb"}. *}
  3.1528 -apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb : Aa & xa : Ab")
  3.1529 - prefer 2 apply (blast elim!: equalityE, clarify)
  3.1530 -apply (subgoal_tac "Aa = insert xb Ab - {xa}")
  3.1531 - prefer 2 apply blast
  3.1532 -apply (subgoal_tac "card Aa <= card Ab")
  3.1533 - prefer 2
  3.1534 - apply (rule Suc_le_mono [THEN subst])
  3.1535 - apply (simp add: card_Suc_Diff1)
  3.1536 -apply(case_tac "Aa - {xb} = {}")
  3.1537 - apply(subgoal_tac "Aa = {xb}")
  3.1538 -  prefer 2 apply (fast elim!: equalityE)
  3.1539 - apply(subgoal_tac "Ab = {xa}")
  3.1540 -  prefer 2 apply (fast elim!: equalityE)
  3.1541 - apply (simp add:insert_Diff_if AC)
  3.1542 -apply (rule_tac A1 = "Aa - {xb}" and f1 = f in finite_nonempty_imp_foldSet1 [THEN exE])
  3.1543 -  apply (blast intro: foldSet_imp_finite finite_Diff)
  3.1544 - apply assumption
  3.1545 -apply (frule (1) Diff1_foldSet1)
  3.1546 -apply (subgoal_tac "ya = f xb x")
  3.1547 - prefer 2 apply (blast del: equalityCE)
  3.1548 -apply (subgoal_tac "(Ab - {xa}, x) : foldSet1 f")
  3.1549 - prefer 2 apply (simp)
  3.1550 -apply (subgoal_tac "yb = f xa x")
  3.1551 - prefer 2 apply (blast del: equalityCE dest: Diff1_foldSet1)
  3.1552 -apply (simp (no_asm_simp) add: left_commute)
  3.1553 -done
  3.1554 -ML"simp_depth_limit := 1000"
  3.1555 -
  3.1556 -lemma (in ACf) foldSet1_determ:
  3.1557 -  "(A, x) : foldSet1 f ==> (A, y) : foldSet1 f ==> y = x"
  3.1558 -by (blast intro: foldSet1_determ_aux [rule_format])
  3.1559 -
  3.1560 -lemma (in ACf) fold1_equality: "(A, y) : foldSet1 f ==> fold1 f A = y"
  3.1561 -  by (unfold fold1_def) (blast intro: foldSet1_determ)
  3.1562 -
  3.1563 -lemma fold1_singleton [simp]: "fold1 f {a} = a"
  3.1564 -  by (unfold fold1_def) blast
  3.1565 -
  3.1566 -lemma (in ACf) fold1_insert_aux: "x \<notin> A ==> A \<noteq> {} \<Longrightarrow> 
  3.1567 -    ((insert x A, v) : foldSet1 f) =
  3.1568 -    (EX y. (A, y) : foldSet1 f & v = f x y)"
  3.1569 -apply auto
  3.1570 -apply (rule_tac A1 = A and f1 = f in finite_nonempty_imp_foldSet1 [THEN exE])
  3.1571 -  apply (fastsimp dest: foldSet_imp_finite)
  3.1572 - apply blast
  3.1573 -apply (blast intro: foldSet1_determ)
  3.1574 -done
  3.1575 -
  3.1576 -lemma (in ACf) fold1_insert:
  3.1577 -  "finite A ==> x \<notin> A ==> A \<noteq> {} \<Longrightarrow> fold1 f (insert x A) = f x (fold1 f A)"
  3.1578 -apply (unfold fold1_def)
  3.1579 -apply (simp add: fold1_insert_aux)
  3.1580 -apply (rule the_equality)
  3.1581 -apply (auto intro: finite_nonempty_imp_foldSet1
  3.1582 -    cong add: conj_cong simp add: fold1_def [symmetric] fold1_equality)
  3.1583 -done
  3.1584 -
  3.1585 -locale ACIf = ACf +
  3.1586 -  assumes idem: "x \<cdot> x = x"
  3.1587 -
  3.1588 -lemma (in ACIf) fold1_insert2:
  3.1589 -assumes finA: "finite A" and nonA: "A \<noteq> {}"
  3.1590 -shows "fold1 f (insert a A) = f a (fold1 f A)"
  3.1591 -proof cases
  3.1592 -  assume "a \<in> A"
  3.1593 -  then obtain B where A: "A = insert a B" and disj: "a \<notin> B"
  3.1594 -    by(blast dest: mk_disjoint_insert)
  3.1595 -  show ?thesis
  3.1596 -  proof cases
  3.1597 -    assume "B = {}"
  3.1598 -    thus ?thesis using A by(simp add:idem)
  3.1599 -  next
  3.1600 -    assume nonB: "B \<noteq> {}"
  3.1601 -    from finA A have finB: "finite B" by(blast intro: finite_subset)
  3.1602 -    have "fold1 f (insert a A) = fold1 f (insert a B)" using A by simp
  3.1603 -    also have "\<dots> = f a (fold1 f B)"
  3.1604 -      using finB nonB disj by(simp add: fold1_insert)
  3.1605 -    also have "\<dots> = f a (fold1 f A)"
  3.1606 -      using A finB nonB disj by(simp add: idem fold1_insert assoc[symmetric])
  3.1607 -    finally show ?thesis .
  3.1608 -  qed
  3.1609 -next
  3.1610 -  assume "a \<notin> A"
  3.1611 -  with finA nonA show ?thesis by(simp add:fold1_insert)
  3.1612 -qed
  3.1613 -
  3.1614 -text{* Seemed easier to define directly than via fold. *}
  3.1615 -
  3.1616 -(* FIXME define Min/Max via fold1 *)
  3.1617 -
  3.1618 -lemma ex_Max: fixes S :: "('a::linorder)set"
  3.1619 -  assumes fin: "finite S" shows "S \<noteq> {} ==> \<exists>m\<in>S. \<forall>s \<in> S. s \<le> m"
  3.1620 -using fin
  3.1621 -proof (induct)
  3.1622 -  case empty thus ?case by simp
  3.1623 -next
  3.1624 -  case (insert x S)
  3.1625 -  show ?case
  3.1626 -  proof (cases)
  3.1627 -    assume "S = {}" thus ?thesis by simp
  3.1628 -  next
  3.1629 -    assume nonempty: "S \<noteq> {}"
  3.1630 -    then obtain m where m: "m\<in>S" "\<forall>s\<in>S. s \<le> m" using insert by blast
  3.1631 -    show ?thesis
  3.1632 -    proof (cases)
  3.1633 -      assume "x \<le> m" thus ?thesis using m by blast
  3.1634 -    next
  3.1635 -      assume "~ x \<le> m" thus ?thesis using m
  3.1636 -        by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
  3.1637 -    qed
  3.1638 -  qed
  3.1639 -qed
  3.1640 -
  3.1641 -lemma ex_Min: fixes S :: "('a::linorder)set"
  3.1642 -  assumes fin: "finite S" shows "S \<noteq> {} ==> \<exists>m\<in>S. \<forall>s \<in> S. m \<le> s"
  3.1643 -using fin
  3.1644 -proof (induct)
  3.1645 -  case empty thus ?case by simp
  3.1646 -next
  3.1647 -  case (insert x S)
  3.1648 -  show ?case
  3.1649 -  proof (cases)
  3.1650 -    assume "S = {}" thus ?thesis by simp
  3.1651 -  next
  3.1652 -    assume nonempty: "S \<noteq> {}"
  3.1653 -    then obtain m where m: "m\<in>S" "\<forall>s\<in>S. m \<le> s" using insert by blast
  3.1654 -    show ?thesis
  3.1655 -    proof (cases)
  3.1656 -      assume "m \<le> x" thus ?thesis using m by blast
  3.1657 -    next
  3.1658 -      assume "~ m \<le> x" thus ?thesis using m
  3.1659 -        by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
  3.1660 -    qed
  3.1661 -  qed
  3.1662 -qed
  3.1663 -
  3.1664 -constdefs
  3.1665 -  Min :: "('a::linorder)set => 'a"
  3.1666 -  "Min S  ==  THE m. m \<in> S \<and> (\<forall>s \<in> S. m \<le> s)"
  3.1667 -
  3.1668 -  Max :: "('a::linorder)set => 'a"
  3.1669 -  "Max S  ==  THE m. m \<in> S \<and> (\<forall>s \<in> S. s \<le> m)"
  3.1670 -
  3.1671 -lemma Min [simp]:
  3.1672 -  assumes a: "finite S"  "S \<noteq> {}"
  3.1673 -  shows "Min S \<in> S \<and> (\<forall>s \<in> S. Min S \<le> s)" (is "?P(Min S)")
  3.1674 -proof (unfold Min_def, rule theI')
  3.1675 -  show "\<exists>!m. ?P m"
  3.1676 -  proof (rule ex_ex1I)
  3.1677 -    show "\<exists>m. ?P m" using ex_Min[OF a] by blast
  3.1678 -  next
  3.1679 -    fix m1 m2 assume "?P m1" and "?P m2"
  3.1680 -    thus "m1 = m2" by (blast dest: order_antisym)
  3.1681 -  qed
  3.1682 -qed
  3.1683 -
  3.1684 -lemma Max [simp]:
  3.1685 -  assumes a: "finite S"  "S \<noteq> {}"
  3.1686 -  shows "Max S \<in> S \<and> (\<forall>s \<in> S. s \<le> Max S)" (is "?P(Max S)")
  3.1687 -proof (unfold Max_def, rule theI')
  3.1688 -  show "\<exists>!m. ?P m"
  3.1689 -  proof (rule ex_ex1I)
  3.1690 -    show "\<exists>m. ?P m" using ex_Max[OF a] by blast
  3.1691 -  next
  3.1692 -    fix m1 m2 assume "?P m1" "?P m2"
  3.1693 -    thus "m1 = m2" by (blast dest: order_antisym)
  3.1694 -  qed
  3.1695 -qed
  3.1696 -
  3.1697 -
  3.1698 -subsection {* Theorems about @{text "choose"} *}
  3.1699 -
  3.1700 -text {*
  3.1701 -  \medskip Basic theorem about @{text "choose"}.  By Florian
  3.1702 -  Kamm\"uller, tidied by LCP.
  3.1703 -*}
  3.1704 -
  3.1705 -lemma card_s_0_eq_empty:
  3.1706 -    "finite A ==> card {B. B \<subseteq> A & card B = 0} = 1"
  3.1707 -  apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
  3.1708 -  apply (simp cong add: rev_conj_cong)
  3.1709 -  done
  3.1710 -
  3.1711 -lemma choose_deconstruct: "finite M ==> x \<notin> M
  3.1712 -  ==> {s. s <= insert x M & card(s) = Suc k}
  3.1713 -       = {s. s <= M & card(s) = Suc k} Un
  3.1714 -         {s. EX t. t <= M & card(t) = k & s = insert x t}"
  3.1715 -  apply safe
  3.1716 -   apply (auto intro: finite_subset [THEN card_insert_disjoint])
  3.1717 -  apply (drule_tac x = "xa - {x}" in spec)
  3.1718 -  apply (subgoal_tac "x \<notin> xa", auto)
  3.1719 -  apply (erule rev_mp, subst card_Diff_singleton)
  3.1720 -  apply (auto intro: finite_subset)
  3.1721 -  done
  3.1722 -
  3.1723 -lemma card_inj_on_le:
  3.1724 -    "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B"
  3.1725 -apply (subgoal_tac "finite A") 
  3.1726 - apply (force intro: card_mono simp add: card_image [symmetric])
  3.1727 -apply (blast intro: finite_imageD dest: finite_subset) 
  3.1728 -done
  3.1729 -
  3.1730 -lemma card_bij_eq:
  3.1731 -    "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
  3.1732 -       finite A; finite B |] ==> card A = card B"
  3.1733 -  by (auto intro: le_anti_sym card_inj_on_le)
  3.1734 -
  3.1735 -text{*There are as many subsets of @{term A} having cardinality @{term k}
  3.1736 - as there are sets obtained from the former by inserting a fixed element
  3.1737 - @{term x} into each.*}
  3.1738 -lemma constr_bij:
  3.1739 -   "[|finite A; x \<notin> A|] ==>
  3.1740 -    card {B. EX C. C <= A & card(C) = k & B = insert x C} =
  3.1741 -    card {B. B <= A & card(B) = k}"
  3.1742 -  apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq)
  3.1743 -       apply (auto elim!: equalityE simp add: inj_on_def)
  3.1744 -    apply (subst Diff_insert0, auto)
  3.1745 -   txt {* finiteness of the two sets *}
  3.1746 -   apply (rule_tac [2] B = "Pow (A)" in finite_subset)
  3.1747 -   apply (rule_tac B = "Pow (insert x A)" in finite_subset)
  3.1748 -   apply fast+
  3.1749 -  done
  3.1750 -
  3.1751 -text {*
  3.1752 -  Main theorem: combinatorial statement about number of subsets of a set.
  3.1753 -*}
  3.1754 -
  3.1755 -lemma n_sub_lemma:
  3.1756 -  "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
  3.1757 -  apply (induct k)
  3.1758 -   apply (simp add: card_s_0_eq_empty, atomize)
  3.1759 -  apply (rotate_tac -1, erule finite_induct)
  3.1760 -   apply (simp_all (no_asm_simp) cong add: conj_cong
  3.1761 -     add: card_s_0_eq_empty choose_deconstruct)
  3.1762 -  apply (subst card_Un_disjoint)
  3.1763 -     prefer 4 apply (force simp add: constr_bij)
  3.1764 -    prefer 3 apply force
  3.1765 -   prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
  3.1766 -     finite_subset [of _ "Pow (insert x F)", standard])
  3.1767 -  apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
  3.1768 -  done
  3.1769 -
  3.1770 -theorem n_subsets:
  3.1771 -    "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
  3.1772 -  by (simp add: n_sub_lemma)
  3.1773 -
  3.1774  end
     4.1 --- a/src/HOL/List.thy	Thu Dec 09 16:45:46 2004 +0100
     4.2 +++ b/src/HOL/List.thy	Thu Dec 09 18:30:59 2004 +0100
     4.3 @@ -13,7 +13,7 @@
     4.4      Nil    ("[]")
     4.5    | Cons 'a  "'a list"    (infixr "#" 65)
     4.6  
     4.7 -section{*Basic list processing functions*}
     4.8 +subsection{*Basic list processing functions*}
     4.9  
    4.10  consts
    4.11    "@" :: "'a list => 'a list => 'a list"    (infixr 65)
    4.12 @@ -237,7 +237,7 @@
    4.13  by (rule measure_induct [of length]) rules
    4.14  
    4.15  
    4.16 -subsection {* @{text length} *}
    4.17 +subsubsection {* @{text length} *}
    4.18  
    4.19  text {*
    4.20  Needs to come before @{text "@"} because of theorem @{text
    4.21 @@ -289,7 +289,7 @@
    4.22  apply(simp)
    4.23  done
    4.24  
    4.25 -subsection {* @{text "@"} -- append *}
    4.26 +subsubsection {* @{text "@"} -- append *}
    4.27  
    4.28  lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
    4.29  by (induct xs) auto
    4.30 @@ -444,7 +444,7 @@
    4.31  *}
    4.32  
    4.33  
    4.34 -subsection {* @{text map} *}
    4.35 +subsubsection {* @{text map} *}
    4.36  
    4.37  lemma map_ext: "(!!x. x : set xs --> f x = g x) ==> map f xs = map g xs"
    4.38  by (induct xs) simp_all
    4.39 @@ -553,7 +553,7 @@
    4.40  by (induct rule:list_induct2, simp_all)
    4.41  
    4.42  
    4.43 -subsection {* @{text rev} *}
    4.44 +subsubsection {* @{text rev} *}
    4.45  
    4.46  lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs"
    4.47  by (induct xs) auto
    4.48 @@ -587,7 +587,7 @@
    4.49  lemmas rev_cases = rev_exhaust
    4.50  
    4.51  
    4.52 -subsection {* @{text set} *}
    4.53 +subsubsection {* @{text set} *}
    4.54  
    4.55  lemma finite_set [iff]: "finite (set xs)"
    4.56  by (induct xs) auto
    4.57 @@ -650,7 +650,7 @@
    4.58  by (induct xs) (auto simp add: card_insert_if)
    4.59  
    4.60  
    4.61 -subsection {* @{text mem} *}
    4.62 +subsubsection {* @{text mem} *}
    4.63  
    4.64  text{* Only use @{text mem} for generating executable code.  Otherwise
    4.65  use @{prop"x : set xs"} instead --- it is much easier to reason
    4.66 @@ -660,7 +660,7 @@
    4.67  by (induct xs) auto
    4.68  
    4.69  
    4.70 -subsection {* @{text list_all} *}
    4.71 +subsubsection {* @{text list_all} *}
    4.72  
    4.73  lemma list_all_conv: "list_all P xs = (\<forall>x \<in> set xs. P x)"
    4.74  by (induct xs) auto
    4.75 @@ -670,7 +670,7 @@
    4.76  by (induct xs) auto
    4.77  
    4.78  
    4.79 -subsection {* @{text filter} *}
    4.80 +subsubsection {* @{text filter} *}
    4.81  
    4.82  lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys"
    4.83  by (induct xs) auto
    4.84 @@ -739,7 +739,7 @@
    4.85  qed
    4.86  
    4.87  
    4.88 -subsection {* @{text concat} *}
    4.89 +subsubsection {* @{text concat} *}
    4.90  
    4.91  lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys"
    4.92  by (induct xs) auto
    4.93 @@ -763,7 +763,7 @@
    4.94  by (induct xs) auto
    4.95  
    4.96  
    4.97 -subsection {* @{text nth} *}
    4.98 +subsubsection {* @{text nth} *}
    4.99  
   4.100  lemma nth_Cons_0 [simp]: "(x # xs)!0 = x"
   4.101  by auto
   4.102 @@ -815,7 +815,7 @@
   4.103  by (auto simp add: set_conv_nth)
   4.104  
   4.105  
   4.106 -subsection {* @{text list_update} *}
   4.107 +subsubsection {* @{text list_update} *}
   4.108  
   4.109  lemma length_list_update [simp]: "!!i. length(xs[i:=x]) = length xs"
   4.110  by (induct xs) (auto split: nat.split)
   4.111 @@ -865,7 +865,7 @@
   4.112  by (blast dest!: set_update_subset_insert [THEN subsetD])
   4.113  
   4.114  
   4.115 -subsection {* @{text last} and @{text butlast} *}
   4.116 +subsubsection {* @{text last} and @{text butlast} *}
   4.117  
   4.118  lemma last_snoc [simp]: "last (xs @ [x]) = x"
   4.119  by (induct xs) auto
   4.120 @@ -908,7 +908,7 @@
   4.121  by (auto dest: in_set_butlastD simp add: butlast_append)
   4.122  
   4.123  
   4.124 -subsection {* @{text take} and @{text drop} *}
   4.125 +subsubsection {* @{text take} and @{text drop} *}
   4.126  
   4.127  lemma take_0 [simp]: "take 0 xs = []"
   4.128  by (induct xs) auto
   4.129 @@ -1084,7 +1084,7 @@
   4.130  done
   4.131  
   4.132  
   4.133 -subsection {* @{text takeWhile} and @{text dropWhile} *}
   4.134 +subsubsection {* @{text takeWhile} and @{text dropWhile} *}
   4.135  
   4.136  lemma takeWhile_dropWhile_id [simp]: "takeWhile P xs @ dropWhile P xs = xs"
   4.137  by (induct xs) auto
   4.138 @@ -1124,7 +1124,7 @@
   4.139  by(induct xs, auto)
   4.140  
   4.141  
   4.142 -subsection {* @{text zip} *}
   4.143 +subsubsection {* @{text zip} *}
   4.144  
   4.145  lemma zip_Nil [simp]: "zip [] ys = []"
   4.146  by (induct ys) auto
   4.147 @@ -1189,7 +1189,7 @@
   4.148  done
   4.149  
   4.150  
   4.151 -subsection {* @{text list_all2} *}
   4.152 +subsubsection {* @{text list_all2} *}
   4.153  
   4.154  lemma list_all2_lengthD [intro?]: 
   4.155    "list_all2 P xs ys ==> length xs = length ys"
   4.156 @@ -1332,7 +1332,7 @@
   4.157    done
   4.158  
   4.159  
   4.160 -subsection {* @{text foldl} and @{text foldr} *}
   4.161 +subsubsection {* @{text foldl} and @{text foldr} *}
   4.162  
   4.163  lemma foldl_append [simp]:
   4.164  "!!a. foldl f a (xs @ ys) = foldl f (foldl f a xs) ys"
   4.165 @@ -1363,7 +1363,7 @@
   4.166  by (induct ns) auto
   4.167  
   4.168  
   4.169 -subsection {* @{text upto} *}
   4.170 +subsubsection {* @{text upto} *}
   4.171  
   4.172  lemma upt_rec: "[i..j(] = (if i<j then i#[Suc i..j(] else [])"
   4.173  -- {* Does not terminate! *}
   4.174 @@ -1474,7 +1474,7 @@
   4.175                  nth_Cons'[of _ _ "number_of v",standard]
   4.176  
   4.177  
   4.178 -subsection {* @{text "distinct"} and @{text remdups} *}
   4.179 +subsubsection {* @{text "distinct"} and @{text remdups} *}
   4.180  
   4.181  lemma distinct_append [simp]:
   4.182  "distinct (xs @ ys) = (distinct xs \<and> distinct ys \<and> set xs \<inter> set ys = {})"
   4.183 @@ -1572,7 +1572,7 @@
   4.184  done
   4.185  
   4.186  
   4.187 -subsection {* @{text remove1} *}
   4.188 +subsubsection {* @{text remove1} *}
   4.189  
   4.190  lemma set_remove1_subset: "set(remove1 x xs) <= set xs"
   4.191  apply(induct xs)
   4.192 @@ -1597,7 +1597,7 @@
   4.193  by (induct xs) simp_all
   4.194  
   4.195  
   4.196 -subsection {* @{text replicate} *}
   4.197 +subsubsection {* @{text replicate} *}
   4.198  
   4.199  lemma length_replicate [simp]: "length (replicate n x) = n"
   4.200  by (induct n) auto
   4.201 @@ -1644,7 +1644,7 @@
   4.202  by (simp add: set_replicate_conv_if split: split_if_asm)
   4.203  
   4.204  
   4.205 -subsection{*@{text rotate1} and @{text rotate}*}
   4.206 +subsubsection{*@{text rotate1} and @{text rotate}*}
   4.207  
   4.208  lemma rotate_simps[simp]: "rotate1 [] = [] \<and> rotate1 (x#xs) = xs @ [x]"
   4.209  by(simp add:rotate1_def)
   4.210 @@ -1722,7 +1722,7 @@
   4.211  by (induct n) (simp_all add:rotate_def)
   4.212  
   4.213  
   4.214 -subsection {* @{text sublist} --- a generalization of @{text nth} to sets *}
   4.215 +subsubsection {* @{text sublist} --- a generalization of @{text nth} to sets *}
   4.216  
   4.217  lemma sublist_empty [simp]: "sublist xs {} = []"
   4.218  by (auto simp add: sublist_def)
   4.219 @@ -1800,9 +1800,9 @@
   4.220  done
   4.221  
   4.222  
   4.223 -subsection{*Sets of Lists*}
   4.224 -
   4.225 -subsection {* @{text lists}: the list-forming operator over sets *}
   4.226 +subsubsection{*Sets of Lists*}
   4.227 +
   4.228 +subsubsection {* @{text lists}: the list-forming operator over sets *}
   4.229  
   4.230  consts lists :: "'a set => 'a list set"
   4.231  inductive "lists A"
   4.232 @@ -1842,7 +1842,7 @@
   4.233  lemma lists_UNIV [simp]: "lists UNIV = UNIV"
   4.234  by auto
   4.235  
   4.236 -subsection{*Lists as Cartesian products*}
   4.237 +subsubsection{*Lists as Cartesian products*}
   4.238  
   4.239  text{*@{text"set_Cons A Xs"}: the set of lists with head drawn from
   4.240  @{term A} and tail drawn from @{term Xs}.*}
   4.241 @@ -1863,9 +1863,9 @@
   4.242     "listset(A#As) = set_Cons A (listset As)"
   4.243  
   4.244  
   4.245 -section{*Relations on lists*}
   4.246 -
   4.247 -subsection {* Lexicographic orderings on lists *}
   4.248 +subsection{*Relations on lists*}
   4.249 +
   4.250 +subsubsection {* Lexicographic orderings on lists *}
   4.251  
   4.252  consts
   4.253  lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
   4.254 @@ -1946,7 +1946,7 @@
   4.255  done
   4.256  
   4.257  
   4.258 -subsection{*Lifting a Relation on List Elements to the Lists*}
   4.259 +subsubsection{*Lifting a Relation on List Elements to the Lists*}
   4.260  
   4.261  consts  listrel :: "('a * 'a)set => ('a list * 'a list)set"
   4.262  
   4.263 @@ -2004,9 +2004,9 @@
   4.264  by (auto simp add: set_Cons_def intro: listrel.intros) 
   4.265  
   4.266  
   4.267 -section{*Miscellany*}
   4.268 -
   4.269 -subsection {* Characters and strings *}
   4.270 +subsection{*Miscellany*}
   4.271 +
   4.272 +subsubsection {* Characters and strings *}
   4.273  
   4.274  datatype nibble =
   4.275      Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
   4.276 @@ -2084,7 +2084,7 @@
   4.277    in [("Char", char_ast_tr'), ("@list", list_ast_tr')] end;
   4.278  *}
   4.279  
   4.280 -subsection {* Code generator setup *}
   4.281 +subsubsection {* Code generator setup *}
   4.282  
   4.283  ML {*
   4.284  local
     5.1 --- a/src/HOL/Matrix/MatrixGeneral.thy	Thu Dec 09 16:45:46 2004 +0100
     5.2 +++ b/src/HOL/Matrix/MatrixGeneral.thy	Thu Dec 09 18:30:59 2004 +0100
     5.3 @@ -41,7 +41,8 @@
     5.4    from hyp have d: "Max (?S) < m" by (simp add: a nrows_def)
     5.5    have "m \<notin> ?S"
     5.6      proof -
     5.7 -      have "m \<in> ?S \<Longrightarrow> m <= Max(?S)" by (simp add: Max[OF c b])
     5.8 +      have "m \<in> ?S \<Longrightarrow> m <= Max(?S)" by (simp add:Max_le[OF
     5.9 +  c b])
    5.10        moreover from d have "~(m <= Max ?S)" by (simp)
    5.11        ultimately show "m \<notin> ?S" by (auto)
    5.12      qed
     6.1 --- a/src/HOL/NumberTheory/Euler.thy	Thu Dec 09 16:45:46 2004 +0100
     6.2 +++ b/src/HOL/NumberTheory/Euler.thy	Thu Dec 09 18:30:59 2004 +0100
     6.3 @@ -150,7 +150,7 @@
     6.4  
     6.5  lemma SetS_setprod_prop: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p));
     6.6                                ~(QuadRes p a); x \<in> (SetS a p) |] ==> 
     6.7 -                          [setprod x = a] (mod p)";
     6.8 +                          [\<Prod>x = a] (mod p)";
     6.9    apply (auto simp add: SetS_def MultInvPair_def)
    6.10    apply (frule StandardRes_SRStar_prop1a)
    6.11    apply (subgoal_tac "StandardRes p x \<noteq> StandardRes p (a * MultInv p x)");
    6.12 @@ -186,49 +186,49 @@
    6.13  done
    6.14  
    6.15  lemma Union_SetS_setprod_prop1: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
    6.16 -                                 [setprod (Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)";
    6.17 -proof -;
    6.18 -  assume "p \<in> zprime" and "2 < p" and  "~([a = 0] (mod p))" and "~(QuadRes p a)";
    6.19 -  then have "[setprod (Union (SetS a p)) = 
    6.20 -      gsetprod setprod (SetS a p)] (mod p)";
    6.21 +                                 [\<Prod>(Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)"
    6.22 +proof -
    6.23 +  assume "p \<in> zprime" and "2 < p" and  "~([a = 0] (mod p))" and "~(QuadRes p a)"
    6.24 +  then have "[\<Prod>(Union (SetS a p)) = 
    6.25 +      setprod (setprod (%x. x)) (SetS a p)] (mod p)"
    6.26      by (auto simp add: SetS_finite SetS_elems_finite
    6.27 -                       MultInvPair_prop1c setprod_disj_sets)
    6.28 -  also; have "[gsetprod setprod (SetS a p) = 
    6.29 -      gsetprod (%x. a) (SetS a p)] (mod p)";
    6.30 -    apply (rule gsetprod_same_function_zcong)
    6.31 +                       MultInvPair_prop1c setprod_Union_disjoint)
    6.32 +  also have "[setprod (setprod (%x. x)) (SetS a p) = 
    6.33 +      setprod (%x. a) (SetS a p)] (mod p)"
    6.34 +    apply (rule setprod_same_function_zcong)
    6.35      by (auto simp add: prems SetS_setprod_prop SetS_finite)
    6.36 -  also (zcong_trans) have "[gsetprod (%x. a) (SetS a p) = 
    6.37 -      a^(card (SetS a p))] (mod p)";
    6.38 -    by (auto simp add: prems SetS_finite gsetprod_const)
    6.39 -  finally (zcong_trans) show ?thesis;
    6.40 +  also (zcong_trans) have "[setprod (%x. a) (SetS a p) = 
    6.41 +      a^(card (SetS a p))] (mod p)"
    6.42 +    by (auto simp add: prems SetS_finite setprod_constant)
    6.43 +  finally (zcong_trans) show ?thesis
    6.44      apply (rule zcong_trans)
    6.45 -    apply (subgoal_tac "card(SetS a p) = nat((p - 1) div 2)", auto);
    6.46 -    apply (subgoal_tac "nat(int(card(SetS a p))) = nat((p - 1) div 2)", force);
    6.47 +    apply (subgoal_tac "card(SetS a p) = nat((p - 1) div 2)", auto)
    6.48 +    apply (subgoal_tac "nat(int(card(SetS a p))) = nat((p - 1) div 2)", force)
    6.49      apply (auto simp add: prems SetS_card)
    6.50    done
    6.51 -qed;
    6.52 +qed
    6.53  
    6.54  lemma Union_SetS_setprod_prop2: "[| p \<in> zprime; 2 < p; ~([a = 0](mod p)) |] ==> 
    6.55 -                                    setprod (Union (SetS a p)) = zfact (p - 1)";
    6.56 +                                    \<Prod>(Union (SetS a p)) = zfact (p - 1)";
    6.57  proof -;
    6.58    assume "p \<in> zprime" and "2 < p" and "~([a = 0](mod p))";
    6.59 -  then have "setprod (Union (SetS a p)) = setprod (SRStar p)";
    6.60 +  then have "\<Prod>(Union (SetS a p)) = \<Prod>(SRStar p)"
    6.61      by (auto simp add: MultInvPair_prop2)
    6.62 -  also have "... = setprod ({1} \<union> (d22set (p - 1)))";
    6.63 +  also have "... = \<Prod>({1} \<union> (d22set (p - 1)))"
    6.64      by (auto simp add: prems SRStar_d22set_prop)
    6.65 -  also have "... = zfact(p - 1)";
    6.66 -  proof -;
    6.67 -     have "~(1 \<in> d22set (p - 1)) & finite( d22set (p - 1))";
    6.68 +  also have "... = zfact(p - 1)"
    6.69 +  proof -
    6.70 +     have "~(1 \<in> d22set (p - 1)) & finite( d22set (p - 1))"
    6.71        apply (insert prems, auto)
    6.72        apply (drule d22set_g_1)
    6.73        apply (auto simp add: d22set_fin)
    6.74       done
    6.75 -     then have "setprod({1} \<union> (d22set (p - 1))) = setprod (d22set (p - 1))";
    6.76 +     then have "\<Prod>({1} \<union> (d22set (p - 1))) = \<Prod>(d22set (p - 1))";
    6.77         by auto
    6.78       then show ?thesis
    6.79         by (auto simp add: d22set_prod_zfact)
    6.80    qed;
    6.81 -  finally show ?thesis .;
    6.82 +  finally show ?thesis .
    6.83  qed;
    6.84  
    6.85  lemma zfact_prop: "[| p \<in> zprime; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
     7.1 --- a/src/HOL/NumberTheory/EulerFermat.thy	Thu Dec 09 16:45:46 2004 +0100
     7.2 +++ b/src/HOL/NumberTheory/EulerFermat.thy	Thu Dec 09 18:30:59 2004 +0100
     7.3 @@ -255,8 +255,8 @@
     7.4  by (unfold inj_on_def, auto)
     7.5  
     7.6  lemma Bnor_prod_power [rule_format]:
     7.7 -  "x \<noteq> 0 ==> a < m --> setprod ((\<lambda>a. a * x) ` BnorRset (a, m)) =
     7.8 -      setprod (BnorRset(a, m)) * x^card (BnorRset (a, m))"
     7.9 +  "x \<noteq> 0 ==> a < m --> \<Prod>((\<lambda>a. a * x) ` BnorRset (a, m)) =
    7.10 +      \<Prod>(BnorRset(a, m)) * x^card (BnorRset (a, m))"
    7.11    apply (induct a m rule: BnorRset_induct)
    7.12     prefer 2
    7.13     apply (subst BnorRset.simps)
    7.14 @@ -273,7 +273,7 @@
    7.15  subsection {* Fermat *}
    7.16  
    7.17  lemma bijzcong_zcong_prod:
    7.18 -    "(A, B) \<in> bijR (zcongm m) ==> [setprod A = setprod B] (mod m)"
    7.19 +    "(A, B) \<in> bijR (zcongm m) ==> [\<Prod>A = \<Prod>B] (mod m)"
    7.20    apply (unfold zcongm_def)
    7.21    apply (erule bijR.induct)
    7.22     apply (subgoal_tac [2] "a \<notin> A \<and> b \<notin> B \<and> finite A \<and> finite B")
    7.23 @@ -281,7 +281,7 @@
    7.24    done
    7.25  
    7.26  lemma Bnor_prod_zgcd [rule_format]:
    7.27 -    "a < m --> zgcd (setprod (BnorRset (a, m)), m) = 1"
    7.28 +    "a < m --> zgcd (\<Prod>(BnorRset(a, m)), m) = 1"
    7.29    apply (induct a m rule: BnorRset_induct)
    7.30     prefer 2
    7.31     apply (subst BnorRset.simps)
    7.32 @@ -296,7 +296,7 @@
    7.33    apply (case_tac "x = 0")
    7.34     apply (case_tac [2] "m = 1")
    7.35      apply (rule_tac [3] iffD1)
    7.36 -     apply (rule_tac [3] k = "setprod (BnorRset (m - 1, m))"
    7.37 +     apply (rule_tac [3] k = "\<Prod>(BnorRset(m - 1, m))"
    7.38         in zcong_cancel2)
    7.39        prefer 5
    7.40        apply (subst Bnor_prod_power [symmetric])
     8.1 --- a/src/HOL/NumberTheory/Finite2.thy	Thu Dec 09 16:45:46 2004 +0100
     8.2 +++ b/src/HOL/NumberTheory/Finite2.thy	Thu Dec 09 18:30:59 2004 +0100
     8.3 @@ -5,7 +5,9 @@
     8.4  
     8.5  header {*Finite Sets and Finite Sums*}
     8.6  
     8.7 -theory Finite2 = Main + IntFact:;
     8.8 +theory Finite2
     8.9 +imports IntFact
    8.10 +begin
    8.11  
    8.12  text{*These are useful for combinatorial and number-theoretic counting
    8.13  arguments.*}
    8.14 @@ -15,208 +17,163 @@
    8.15  
    8.16  (******************************************************************)
    8.17  (*                                                                *)
    8.18 -(* gsetprod: A generalized set product function, for ints only.   *)
    8.19 -(* Note that "setprod", as defined in IntFact, is equivalent to   *)
    8.20 -(*   our "gsetprod id".                                           *) 
    8.21 +(* Useful properties of sums and products                         *)
    8.22  (*                                                                *)
    8.23  (******************************************************************)
    8.24  
    8.25 -consts
    8.26 -  gsetprod :: "('a => int) => 'a set => int"
    8.27 -
    8.28 -defs
    8.29 -  gsetprod_def: "gsetprod f A ==  if finite A then fold (op * o f) 1 A else 1";
    8.30 -
    8.31 -lemma gsetprod_empty [simp]: "gsetprod f {} = 1";
    8.32 -  by (auto simp add: gsetprod_def)
    8.33 -
    8.34 -lemma gsetprod_insert [simp]: "[| finite A; a \<notin> A |] ==> 
    8.35 -    gsetprod f (insert a A) = f a * gsetprod f A";
    8.36 -  by (simp add: gsetprod_def LC_def LC.fold_insert)
    8.37 -
    8.38 -(******************************************************************)
    8.39 -(*                                                                *)
    8.40 -(* Useful properties of sums and products                         *)
    8.41 -(*                                                                *)
    8.42 -(******************************************************************);
    8.43 -
    8.44  subsection {* Useful properties of sums and products *}
    8.45  
    8.46 -lemma setprod_gsetprod_id: "setprod A = gsetprod id A";
    8.47 -  by (auto simp add: setprod_def gsetprod_def)
    8.48 -
    8.49 -lemma setsum_same_function: "[| finite S; \<forall>x \<in> S. f x = g x |] ==> 
    8.50 -    setsum f S = setsum g S";
    8.51 -by (induct set: Finites, auto)
    8.52 -
    8.53 -lemma gsetprod_same_function: "[| finite S; \<forall>x \<in> S. f x = g x |] ==> 
    8.54 -  gsetprod f S = gsetprod g S";
    8.55 -by (induct set: Finites, auto)
    8.56 -
    8.57  lemma setsum_same_function_zcong: 
    8.58 -   "[| finite S; \<forall>x \<in> S. [f x = g x](mod m) |] 
    8.59 -     ==> [setsum f S = setsum g S] (mod m)";
    8.60 -   by (induct set: Finites, auto simp add: zcong_zadd)
    8.61 +assumes a: "\<forall>x \<in> S. [f x = g x](mod m)"
    8.62 +shows "[setsum f S = setsum g S] (mod m)"
    8.63 +proof cases
    8.64 +  assume "finite S"
    8.65 +  thus ?thesis using a by induct (simp_all add: zcong_zadd)
    8.66 +next
    8.67 +  assume "infinite S" thus ?thesis by(simp add:setsum_def)
    8.68 +qed
    8.69  
    8.70 -lemma gsetprod_same_function_zcong: 
    8.71 -   "[| finite S; \<forall>x \<in> S. [f x = g x](mod m) |] 
    8.72 -     ==> [gsetprod f S = gsetprod g S] (mod m)";
    8.73 -by (induct set: Finites, auto simp add: zcong_zmult)
    8.74 +lemma setprod_same_function_zcong:
    8.75 +assumes a: "\<forall>x \<in> S. [f x = g x](mod m)"
    8.76 +shows "[setprod f S = setprod g S] (mod m)"
    8.77 +proof cases
    8.78 +  assume "finite S"
    8.79 +  thus ?thesis using a by induct (simp_all add: zcong_zmult)
    8.80 +next
    8.81 +  assume "infinite S" thus ?thesis by(simp add:setprod_def)
    8.82 +qed
    8.83  
    8.84 -lemma gsetprod_Un_Int: "finite A ==> finite B
    8.85 -    ==> gsetprod g (A \<union> B) * gsetprod g (A \<inter> B) = 
    8.86 -    gsetprod g A * gsetprod g B";
    8.87 -  apply (induct set: Finites)
    8.88 -by (auto simp add: Int_insert_left insert_absorb)
    8.89 -
    8.90 -lemma gsetprod_Un_disjoint: "[| finite A; finite B; A \<inter> B = {} |] ==> 
    8.91 -    gsetprod g (A \<union> B) = gsetprod g A * gsetprod g B";
    8.92 -  apply (subst gsetprod_Un_Int [symmetric])
    8.93 -by auto
    8.94 -
    8.95 -lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)";
    8.96 +lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)"
    8.97    apply (induct set: Finites)
    8.98    apply (auto simp add: left_distrib right_distrib int_eq_of_nat)
    8.99    done
   8.100  
   8.101  lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) = 
   8.102 -    int(c) * int(card X)";
   8.103 +    int(c) * int(card X)"
   8.104    apply (induct set: Finites)
   8.105    apply (auto simp add: zadd_zmult_distrib2)
   8.106  done
   8.107  
   8.108 -lemma setsum_minus: "finite A ==> setsum (%x. ((f x)::int) - g x) A = 
   8.109 -  setsum f A - setsum g A";
   8.110 -  by (induct set: Finites, auto)
   8.111 -
   8.112  lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A = 
   8.113 -    c * setsum f A";
   8.114 +    c * setsum f A"
   8.115    apply (induct set: Finites, auto)
   8.116 -  by (auto simp only: zadd_zmult_distrib2) 
   8.117 -
   8.118 -lemma setsum_non_neg: "[| finite A; \<forall>x \<in> A. (0::int) \<le> f x |] ==>
   8.119 -    0 \<le>  setsum f A";
   8.120 -  by (induct set: Finites, auto)
   8.121 -
   8.122 -lemma gsetprod_const: "finite X ==> gsetprod (%x. (c :: int)) X = c ^ (card X)";
   8.123 -  apply (induct set: Finites)
   8.124 -by auto
   8.125 +  by (auto simp only: zadd_zmult_distrib2)
   8.126  
   8.127  (******************************************************************)
   8.128  (*                                                                *)
   8.129  (* Cardinality of some explicit finite sets                       *)
   8.130  (*                                                                *)
   8.131 -(******************************************************************);
   8.132 +(******************************************************************)
   8.133  
   8.134  subsection {* Cardinality of explicit finite sets *}
   8.135  
   8.136 -lemma finite_surjI: "[| B \<subseteq> f ` A; finite A |] ==> finite B";
   8.137 +lemma finite_surjI: "[| B \<subseteq> f ` A; finite A |] ==> finite B"
   8.138  by (simp add: finite_subset finite_imageI)
   8.139  
   8.140 -lemma bdd_nat_set_l_finite: "finite { y::nat . y < x}";
   8.141 +lemma bdd_nat_set_l_finite: "finite { y::nat . y < x}"
   8.142  apply (rule_tac N = "{y. y < x}" and n = x in bounded_nat_set_is_finite)
   8.143  by auto
   8.144  
   8.145 -lemma bdd_nat_set_le_finite: "finite { y::nat . y \<le> x  }";
   8.146 +lemma bdd_nat_set_le_finite: "finite { y::nat . y \<le> x  }"
   8.147  apply (subgoal_tac "{ y::nat . y \<le> x  } = { y::nat . y < Suc x}")
   8.148  by (auto simp add: bdd_nat_set_l_finite)
   8.149  
   8.150 -lemma  bdd_int_set_l_finite: "finite { x::int . 0 \<le> x & x < n}";
   8.151 +lemma  bdd_int_set_l_finite: "finite { x::int . 0 \<le> x & x < n}"
   8.152  apply (subgoal_tac " {(x :: int). 0 \<le> x & x < n} \<subseteq> 
   8.153 -    int ` {(x :: nat). x < nat n}");
   8.154 +    int ` {(x :: nat). x < nat n}")
   8.155  apply (erule finite_surjI)
   8.156  apply (auto simp add: bdd_nat_set_l_finite image_def)
   8.157  apply (rule_tac x = "nat x" in exI, simp) 
   8.158  done
   8.159  
   8.160 -lemma bdd_int_set_le_finite: "finite {x::int. 0 \<le> x & x \<le> n}";
   8.161 +lemma bdd_int_set_le_finite: "finite {x::int. 0 \<le> x & x \<le> n}"
   8.162  apply (subgoal_tac "{x. 0 \<le> x & x \<le> n} = {x. 0 \<le> x & x < n + 1}")
   8.163  apply (erule ssubst)
   8.164  apply (rule bdd_int_set_l_finite)
   8.165  by auto
   8.166  
   8.167 -lemma bdd_int_set_l_l_finite: "finite {x::int. 0 < x & x < n}";
   8.168 +lemma bdd_int_set_l_l_finite: "finite {x::int. 0 < x & x < n}"
   8.169  apply (subgoal_tac "{x::int. 0 < x & x < n} \<subseteq> {x::int. 0 \<le> x & x < n}")
   8.170  by (auto simp add: bdd_int_set_l_finite finite_subset)
   8.171  
   8.172 -lemma bdd_int_set_l_le_finite: "finite {x::int. 0 < x & x \<le> n}";
   8.173 +lemma bdd_int_set_l_le_finite: "finite {x::int. 0 < x & x \<le> n}"
   8.174  apply (subgoal_tac "{x::int. 0 < x & x \<le> n} \<subseteq> {x::int. 0 \<le> x & x \<le> n}")
   8.175  by (auto simp add: bdd_int_set_le_finite finite_subset)
   8.176  
   8.177 -lemma card_bdd_nat_set_l: "card {y::nat . y < x} = x";
   8.178 +lemma card_bdd_nat_set_l: "card {y::nat . y < x} = x"
   8.179  apply (induct_tac x, force)
   8.180 -proof -;
   8.181 -  fix n::nat;
   8.182 -  assume "card {y. y < n} = n"; 
   8.183 -  have "{y. y < Suc n} = insert n {y. y < n}";
   8.184 +proof -
   8.185 +  fix n::nat
   8.186 +  assume "card {y. y < n} = n" 
   8.187 +  have "{y. y < Suc n} = insert n {y. y < n}"
   8.188      by auto
   8.189 -  then have "card {y. y < Suc n} = card (insert n {y. y < n})";
   8.190 +  then have "card {y. y < Suc n} = card (insert n {y. y < n})"
   8.191      by auto
   8.192 -  also have "... = Suc (card {y. y < n})";
   8.193 +  also have "... = Suc (card {y. y < n})"
   8.194      apply (rule card_insert_disjoint)
   8.195      by (auto simp add: bdd_nat_set_l_finite)
   8.196 -  finally show "card {y. y < Suc n} = Suc n"; 
   8.197 +  finally show "card {y. y < Suc n} = Suc n" 
   8.198      by (simp add: prems)
   8.199 -qed;
   8.200 +qed
   8.201  
   8.202 -lemma card_bdd_nat_set_le: "card { y::nat. y \<le> x} = Suc x";
   8.203 +lemma card_bdd_nat_set_le: "card { y::nat. y \<le> x} = Suc x"
   8.204  apply (subgoal_tac "{ y::nat. y \<le> x} = { y::nat. y < Suc x}")
   8.205  by (auto simp add: card_bdd_nat_set_l)
   8.206  
   8.207 -lemma card_bdd_int_set_l: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y < n} = nat n";
   8.208 -proof -;
   8.209 -  fix n::int;
   8.210 -  assume "0 \<le> n";
   8.211 -  have "finite {y. y < nat n}";
   8.212 +lemma card_bdd_int_set_l: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y < n} = nat n"
   8.213 +proof -
   8.214 +  fix n::int
   8.215 +  assume "0 \<le> n"
   8.216 +  have "finite {y. y < nat n}"
   8.217      by (rule bdd_nat_set_l_finite)
   8.218 -  moreover have "inj_on (%y. int y) {y. y < nat n}";
   8.219 +  moreover have "inj_on (%y. int y) {y. y < nat n}"
   8.220      by (auto simp add: inj_on_def)
   8.221 -  ultimately have "card (int ` {y. y < nat n}) = card {y. y < nat n}";
   8.222 +  ultimately have "card (int ` {y. y < nat n}) = card {y. y < nat n}"
   8.223      by (rule card_image)
   8.224 -  also from prems have "int ` {y. y < nat n} = {y. 0 \<le> y & y < n}";
   8.225 +  also from prems have "int ` {y. y < nat n} = {y. 0 \<le> y & y < n}"
   8.226      apply (auto simp add: zless_nat_eq_int_zless image_def)
   8.227      apply (rule_tac x = "nat x" in exI)
   8.228      by (auto simp add: nat_0_le)
   8.229 -  also; have "card {y. y < nat n} = nat n" 
   8.230 +  also have "card {y. y < nat n} = nat n" 
   8.231      by (rule card_bdd_nat_set_l)
   8.232 -  finally show "card {y. 0 \<le> y & y < n} = nat n"; .;
   8.233 -qed;
   8.234 +  finally show "card {y. 0 \<le> y & y < n} = nat n" .
   8.235 +qed
   8.236  
   8.237  lemma card_bdd_int_set_le: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y \<le> n} = 
   8.238 -  nat n + 1";
   8.239 +  nat n + 1"
   8.240  apply (subgoal_tac "{y. 0 \<le> y & y \<le> n} = {y. 0 \<le> y & y < n+1}")
   8.241  apply (insert card_bdd_int_set_l [of "n+1"])
   8.242  by (auto simp add: nat_add_distrib)
   8.243  
   8.244  lemma card_bdd_int_set_l_le: "0 \<le> (n::int) ==> 
   8.245 -    card {x. 0 < x & x \<le> n} = nat n";
   8.246 -proof -;
   8.247 -  fix n::int;
   8.248 -  assume "0 \<le> n";
   8.249 -  have "finite {x. 0 \<le> x & x < n}";
   8.250 +    card {x. 0 < x & x \<le> n} = nat n"
   8.251 +proof -
   8.252 +  fix n::int
   8.253 +  assume "0 \<le> n"
   8.254 +  have "finite {x. 0 \<le> x & x < n}"
   8.255      by (rule bdd_int_set_l_finite)
   8.256 -  moreover have "inj_on (%x. x+1) {x. 0 \<le> x & x < n}";
   8.257 +  moreover have "inj_on (%x. x+1) {x. 0 \<le> x & x < n}"
   8.258      by (auto simp add: inj_on_def)
   8.259    ultimately have "card ((%x. x+1) ` {x. 0 \<le> x & x < n}) = 
   8.260 -     card {x. 0 \<le> x & x < n}";
   8.261 +     card {x. 0 \<le> x & x < n}"
   8.262      by (rule card_image)
   8.263 -  also from prems have "... = nat n";
   8.264 +  also from prems have "... = nat n"
   8.265      by (rule card_bdd_int_set_l)
   8.266 -  also; have "(%x. x + 1) ` {x. 0 \<le> x & x < n} = {x. 0 < x & x<= n}";
   8.267 +  also have "(%x. x + 1) ` {x. 0 \<le> x & x < n} = {x. 0 < x & x<= n}"
   8.268      apply (auto simp add: image_def)
   8.269      apply (rule_tac x = "x - 1" in exI)
   8.270      by arith
   8.271 -  finally; show "card {x. 0 < x & x \<le> n} = nat n";.;
   8.272 -qed;
   8.273 +  finally show "card {x. 0 < x & x \<le> n} = nat n".
   8.274 +qed
   8.275  
   8.276  lemma card_bdd_int_set_l_l: "0 < (n::int) ==> 
   8.277 -    card {x. 0 < x & x < n} = nat n - 1";
   8.278 +    card {x. 0 < x & x < n} = nat n - 1"
   8.279    apply (subgoal_tac "{x. 0 < x & x < n} = {x. 0 < x & x \<le> n - 1}")
   8.280    apply (insert card_bdd_int_set_l_le [of "n - 1"])
   8.281    by (auto simp add: nat_diff_distrib)
   8.282  
   8.283  lemma int_card_bdd_int_set_l_l: "0 < n ==> 
   8.284 -    int(card {x. 0 < x & x < n}) = n - 1";
   8.285 +    int(card {x. 0 < x & x < n}) = n - 1"
   8.286    apply (auto simp add: card_bdd_int_set_l_l)
   8.287    apply (subgoal_tac "Suc 0 \<le> nat n")
   8.288    apply (auto simp add: zdiff_int [THEN sym])
   8.289 @@ -224,7 +181,7 @@
   8.290    by (simp add: zero_less_nat_eq)
   8.291  
   8.292  lemma int_card_bdd_int_set_l_le: "0 \<le> n ==> 
   8.293 -    int(card {x. 0 < x & x \<le> n}) = n";
   8.294 +    int(card {x. 0 < x & x \<le> n}) = n"
   8.295    by (auto simp add: card_bdd_int_set_l_le)
   8.296  
   8.297  (******************************************************************)
   8.298 @@ -236,23 +193,23 @@
   8.299  subsection {* Cardinality of finite cartesian products *}
   8.300  
   8.301  lemma insert_Sigma [simp]: "~(A = {}) ==>
   8.302 -  (insert x A) <*> B = ({ x } <*> B) \<union> (A <*> B)";
   8.303 +  (insert x A) <*> B = ({ x } <*> B) \<union> (A <*> B)"
   8.304    by blast
   8.305  
   8.306  lemma cartesian_product_finite: "[| finite A; finite B |] ==> 
   8.307 -    finite (A <*> B)";
   8.308 +    finite (A <*> B)"
   8.309    apply (rule_tac F = A in finite_induct)
   8.310    by auto
   8.311  
   8.312  lemma cartesian_product_card_a [simp]: "finite A ==> 
   8.313 -    card({x} <*> A) = card(A)"; 
   8.314 -  apply (subgoal_tac "inj_on (%y .(x,y)) A");
   8.315 +    card({x} <*> A) = card(A)" 
   8.316 +  apply (subgoal_tac "inj_on (%y .(x,y)) A")
   8.317    apply (frule card_image, assumption)
   8.318 -  apply (subgoal_tac "(Pair x ` A) = {x} <*> A");
   8.319 +  apply (subgoal_tac "(Pair x ` A) = {x} <*> A")
   8.320    by (auto simp add: inj_on_def)
   8.321  
   8.322  lemma cartesian_product_card [simp]: "[| finite A; finite B |] ==> 
   8.323 -  card (A <*> B) = card(A) * card(B)";
   8.324 +  card (A <*> B) = card(A) * card(B)"
   8.325    apply (rule_tac F = A in finite_induct, auto)
   8.326    done
   8.327  
   8.328 @@ -262,101 +219,61 @@
   8.329  (*                                                                *)
   8.330  (******************************************************************)
   8.331  
   8.332 -subsection {* Reindexing sums and products *}
   8.333 -
   8.334 -lemma sum_prop [rule_format]: "finite B ==>
   8.335 -                  inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B";
   8.336 -by (rule finite_induct, auto)
   8.337 -
   8.338 -lemma sum_prop_id: "finite B ==> inj_on f B ==> 
   8.339 -    setsum f B = setsum id (f ` B)";
   8.340 -by (auto simp add: sum_prop id_o)
   8.341 -
   8.342 -lemma prod_prop [rule_format]: "finite B ==>
   8.343 -        inj_on f B --> gsetprod h (f ` B) = gsetprod (h \<circ> f) B";
   8.344 -  apply (rule finite_induct, assumption, force)
   8.345 -  apply (rule impI)
   8.346 -  apply (auto simp add: inj_on_def)
   8.347 -  apply (subgoal_tac "f x \<notin> f ` F")
   8.348 -  apply (subgoal_tac "finite (f ` F)");
   8.349 -by (auto simp add: gsetprod_insert)
   8.350 -
   8.351 -lemma prod_prop_id: "[| finite B; inj_on f B |] ==> 
   8.352 -    gsetprod id (f ` B) = (gsetprod f B)";
   8.353 -  by (simp add: prod_prop id_o)
   8.354 -
   8.355  subsection {* Lemmas for counting arguments *}
   8.356  
   8.357  lemma finite_union_finite_subsets: "[| finite A; \<forall>X \<in> A. finite X |] ==> 
   8.358 -    finite (Union A)";
   8.359 +    finite (Union A)"
   8.360  apply (induct set: Finites)
   8.361  by auto
   8.362  
   8.363  lemma finite_index_UNION_finite_sets: "finite A ==> 
   8.364 -    (\<forall>x \<in> A. finite (f x)) --> finite (UNION A f)";
   8.365 +    (\<forall>x \<in> A. finite (f x)) --> finite (UNION A f)"
   8.366  by (induct_tac rule: finite_induct, auto)
   8.367  
   8.368  lemma card_union_disjoint_sets: "finite A ==> 
   8.369      ((\<forall>X \<in> A. finite X) & (\<forall>X \<in> A. \<forall>Y \<in> A. X \<noteq> Y --> X \<inter> Y = {})) ==> 
   8.370 -    card (Union A) = setsum card A";
   8.371 +    card (Union A) = setsum card A"
   8.372    apply auto
   8.373    apply (induct set: Finites, auto)
   8.374    apply (frule_tac B = "Union F" and A = x in card_Un_Int)
   8.375  by (auto simp add: finite_union_finite_subsets)
   8.376  
   8.377 -(*
   8.378 -  We just duplicated something in the standard library: the next lemma 
   8.379 -  is setsum_UN_disjoint in Finite_Set
   8.380 -
   8.381 -lemma setsum_indexed_union_disjoint_sets [rule_format]: "finite A ==> 
   8.382 -    ((\<forall>x \<in> A. finite (g x)) & 
   8.383 -    (\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y --> (g x) \<inter> (g y) = {})) --> 
   8.384 -      setsum f (UNION A g) = setsum (%x. setsum f (g x)) A";
   8.385 -apply (induct_tac rule: finite_induct)
   8.386 -apply (assumption, simp, clarify)
   8.387 -apply (subgoal_tac "g x \<inter> (UNION F g) = {}");
   8.388 -apply (subgoal_tac "finite (UNION F g)");
   8.389 -apply (simp add: setsum_Un_disjoint)
   8.390 -by (auto simp add: finite_index_UNION_finite_sets)
   8.391 -
   8.392 -*)
   8.393 -
   8.394  lemma int_card_eq_setsum [rule_format]: "finite A ==> 
   8.395 -    int (card A) = setsum (%x. 1) A";
   8.396 +    int (card A) = setsum (%x. 1) A"
   8.397    by (erule finite_induct, auto)
   8.398  
   8.399  lemma card_indexed_union_disjoint_sets [rule_format]: "finite A ==> 
   8.400      ((\<forall>x \<in> A. finite (g x)) & 
   8.401      (\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y --> (g x) \<inter> (g y) = {})) --> 
   8.402 -      card (UNION A g) = setsum (%x. card (g x)) A";
   8.403 +      card (UNION A g) = setsum (%x. card (g x)) A"
   8.404  apply clarify
   8.405  apply (frule_tac f = "%x.(1::nat)" and A = g in 
   8.406 -    setsum_UN_disjoint);
   8.407 -apply assumption+;
   8.408 -apply (subgoal_tac "finite (UNION A g)");
   8.409 -apply (subgoal_tac "(\<Sum>x \<in> UNION A g. 1) = (\<Sum>x \<in> A. \<Sum>x \<in> g x. 1)");
   8.410 +    setsum_UN_disjoint)
   8.411 +apply assumption+
   8.412 +apply (subgoal_tac "finite (UNION A g)")
   8.413 +apply (subgoal_tac "(\<Sum>x \<in> UNION A g. 1) = (\<Sum>x \<in> A. \<Sum>x \<in> g x. 1)")
   8.414  apply (auto simp only: card_eq_setsum)
   8.415 -apply (erule setsum_same_function)
   8.416 -by auto;
   8.417 +apply (rule setsum_cong)
   8.418 +by auto
   8.419  
   8.420  lemma int_card_indexed_union_disjoint_sets [rule_format]: "finite A ==> 
   8.421      ((\<forall>x \<in> A. finite (g x)) & 
   8.422      (\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y --> (g x) \<inter> (g y) = {})) --> 
   8.423 -       int(card (UNION A g)) = setsum (%x. int( card (g x))) A";
   8.424 +       int(card (UNION A g)) = setsum (%x. int( card (g x))) A"
   8.425  apply clarify
   8.426  apply (frule_tac f = "%x.(1::int)" and A = g in 
   8.427 -    setsum_UN_disjoint);
   8.428 -apply assumption+;
   8.429 -apply (subgoal_tac "finite (UNION A g)");
   8.430 -apply (subgoal_tac "(\<Sum>x \<in> UNION A g. 1) = (\<Sum>x \<in> A. \<Sum>x \<in> g x. 1)");
   8.431 +    setsum_UN_disjoint)
   8.432 +apply assumption+
   8.433 +apply (subgoal_tac "finite (UNION A g)")
   8.434 +apply (subgoal_tac "(\<Sum>x \<in> UNION A g. 1) = (\<Sum>x \<in> A. \<Sum>x \<in> g x. 1)")
   8.435  apply (auto simp only: int_card_eq_setsum)
   8.436 -apply (erule setsum_same_function)
   8.437 +apply (rule setsum_cong)
   8.438  by (auto simp add: int_card_eq_setsum)
   8.439  
   8.440  lemma setsum_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A; 
   8.441 -    g ` B \<subseteq> A; inj_on g B |] ==> setsum g B = setsum (g \<circ> f) A";
   8.442 -apply (frule_tac h = g and f = f in sum_prop, auto)
   8.443 -apply (subgoal_tac "setsum g B = setsum g (f ` A)");
   8.444 +    g ` B \<subseteq> A; inj_on g B |] ==> setsum g B = setsum (g \<circ> f) A"
   8.445 +apply (frule_tac h = g and f = f in setsum_reindex)
   8.446 +apply (subgoal_tac "setsum g B = setsum g (f ` A)")
   8.447  apply (simp add: inj_on_def)
   8.448  apply (subgoal_tac "card A = card B")
   8.449  apply (drule_tac A = "f ` A" and B = B in card_seteq)
   8.450 @@ -365,10 +282,10 @@
   8.451  apply (frule_tac A = B and B = A and f = g in card_inj_on_le)
   8.452  by auto
   8.453  
   8.454 -lemma gsetprod_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A; 
   8.455 -    g ` B \<subseteq> A; inj_on g B |] ==> gsetprod g B = gsetprod (g \<circ> f) A";
   8.456 -  apply (frule_tac h = g and f = f in prod_prop, auto) 
   8.457 -  apply (subgoal_tac "gsetprod g B = gsetprod g (f ` A)"); 
   8.458 +lemma setprod_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A; 
   8.459 +    g ` B \<subseteq> A; inj_on g B |] ==> setprod g B = setprod (g \<circ> f) A"
   8.460 +  apply (frule_tac h = g and f = f in setprod_reindex)
   8.461 +  apply (subgoal_tac "setprod g B = setprod g (f ` A)") 
   8.462    apply (simp add: inj_on_def)
   8.463    apply (subgoal_tac "card A = card B")
   8.464    apply (drule_tac A = "f ` A" and B = B in card_seteq)
   8.465 @@ -376,40 +293,4 @@
   8.466    apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
   8.467  by (frule_tac A = B and B = A and f = g in card_inj_on_le, auto)
   8.468  
   8.469 -lemma setsum_union_disjoint_sets [rule_format]: "finite A ==> 
   8.470 -    ((\<forall>X \<in> A. finite X) & (\<forall>X \<in> A. \<forall>Y \<in> A. X \<noteq> Y --> X \<inter> Y = {})) 
   8.471 -    --> setsum f (Union A) = setsum (%x. setsum f x) A";
   8.472 -apply (induct_tac rule: finite_induct)
   8.473 -apply (assumption, simp, clarify)
   8.474 -apply (subgoal_tac "x \<inter> (Union F) = {}");
   8.475 -apply (subgoal_tac "finite (Union F)");
   8.476 -  by (auto simp add: setsum_Un_disjoint Union_def)
   8.477 -
   8.478 -lemma gsetprod_union_disjoint_sets [rule_format]: "[| 
   8.479 -    finite (A :: int set set); 
   8.480 -    (\<forall>X \<in> A. finite (X :: int set));
   8.481 -    (\<forall>X \<in> A. (\<forall>Y \<in> A. (X :: int set) \<noteq> (Y :: int set) --> 
   8.482 -      (X \<inter> Y) = {})) |] ==> 
   8.483 -  ( gsetprod (f :: int => int) (Union A) = gsetprod (%x. gsetprod f x) A)";
   8.484 -  apply (induct set: Finites)
   8.485 -  apply (auto simp add: gsetprod_empty) 
   8.486 -  apply (subgoal_tac "gsetprod f (x \<union> Union F) = 
   8.487 -    gsetprod f x * gsetprod f (Union F)");
   8.488 -  apply simp
   8.489 -  apply (rule gsetprod_Un_disjoint)
   8.490 -by (auto simp add: gsetprod_Un_disjoint Union_def)
   8.491 -
   8.492 -lemma gsetprod_disjoint_sets: "[| finite A;
   8.493 -    \<forall>X \<in> A. finite X; 
   8.494 -    \<forall>X \<in> A. \<forall>Y \<in> A. (X \<noteq> Y --> X \<inter> Y = {}) |] ==> 
   8.495 -  gsetprod id (Union A) = gsetprod (gsetprod id) A";
   8.496 -  apply (rule_tac f = id in gsetprod_union_disjoint_sets)
   8.497 -  by auto
   8.498 -
   8.499 -lemma setprod_disj_sets: "[| finite (A::int set set);
   8.500 -    \<forall>X \<in> A. finite X;
   8.501 -    \<forall>X \<in> A. \<forall>Y \<in> A. (X \<noteq> Y --> X \<inter> Y = {}) |] ==> 
   8.502 -  setprod (Union A) = gsetprod (%x. setprod x) A";
   8.503 -  by (auto simp add: setprod_gsetprod_id gsetprod_disjoint_sets)
   8.504 -
   8.505 -end;
   8.506 +end
   8.507 \ No newline at end of file
     9.1 --- a/src/HOL/NumberTheory/Gauss.thy	Thu Dec 09 16:45:46 2004 +0100
     9.2 +++ b/src/HOL/NumberTheory/Gauss.thy	Thu Dec 09 18:30:59 2004 +0100
     9.3 @@ -274,7 +274,7 @@
     9.4    apply (insert p_prime p_minus_one_l)
     9.5  by (auto simp add: A_def zless_zprime_imp_zrelprime)
     9.6  
     9.7 -lemma (in GAUSS) A_prod_relprime: "zgcd((gsetprod id A),p) = 1";
     9.8 +lemma (in GAUSS) A_prod_relprime: "zgcd((setprod id A),p) = 1";
     9.9    by (insert all_A_relprime finite_A, simp add: all_relprime_prod_relprime)
    9.10  
    9.11  subsection {* Relationships Between Gauss Sets *}
    9.12 @@ -303,17 +303,16 @@
    9.13  lemma (in GAUSS) C_card_eq_D_plus_E: "card C = card D + card E";
    9.14    by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E)
    9.15  
    9.16 -lemma (in GAUSS) C_prod_eq_D_times_E: "gsetprod id E * gsetprod id D = gsetprod id C";
    9.17 +lemma (in GAUSS) C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C";
    9.18    apply (insert D_E_disj finite_D finite_E C_eq)
    9.19 -  apply (frule gsetprod_Un_disjoint [of D E id])
    9.20 +  apply (frule setprod_Un_disjoint [of D E id])
    9.21  by auto
    9.22  
    9.23 -lemma (in GAUSS) C_B_zcong_prod: "[gsetprod id C = gsetprod id B] (mod p)";
    9.24 -thm gsetprod_same_function_zcong;  
    9.25 +lemma (in GAUSS) C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)";
    9.26    apply (auto simp add: C_def)
    9.27    apply (insert finite_B SR_B_inj) 
    9.28 -  apply (frule_tac f = "StandardRes p" in prod_prop_id, auto) 
    9.29 -  apply (rule gsetprod_same_function_zcong)
    9.30 +  apply (frule_tac f1 = "StandardRes p" in setprod_reindex_id[THEN sym], auto)
    9.31 +  apply (rule setprod_same_function_zcong)
    9.32  by (auto simp add: StandardRes_prop1 zcong_sym p_g_0)
    9.33  
    9.34  lemma (in GAUSS) F_Un_D_subset: "(F \<union> D) \<subseteq> A";
    9.35 @@ -384,127 +383,127 @@
    9.36  by (auto simp add: card_seteq)
    9.37  
    9.38  lemma (in GAUSS) prod_D_F_eq_prod_A: 
    9.39 -    "(gsetprod id D) * (gsetprod id F) = gsetprod id A";
    9.40 +    "(setprod id D) * (setprod id F) = setprod id A";
    9.41    apply (insert F_D_disj finite_D finite_F)
    9.42 -  apply (frule gsetprod_Un_disjoint [of F D id])
    9.43 +  apply (frule setprod_Un_disjoint [of F D id])
    9.44  by (auto simp add: F_Un_D_eq_A)
    9.45  
    9.46  lemma (in GAUSS) prod_F_zcong:
    9.47 -    "[gsetprod id F = ((-1) ^ (card E)) * (gsetprod id E)] (mod p)";
    9.48 -  proof -;
    9.49 -    have "gsetprod id F = gsetprod id (op - p ` E)";
    9.50 +    "[setprod id F = ((-1) ^ (card E)) * (setprod id E)] (mod p)"
    9.51 +  proof -
    9.52 +    have "setprod id F = setprod id (op - p ` E)"
    9.53        by (auto simp add: F_def)
    9.54 -    then have "gsetprod id F = gsetprod (op - p) E";
    9.55 +    then have "setprod id F = setprod (op - p) E"
    9.56        apply simp
    9.57        apply (insert finite_E inj_on_pminusx_E)
    9.58 -      by (frule_tac f = "op - p" in prod_prop_id, auto)
    9.59 +      by (frule_tac f = "op - p" in setprod_reindex_id, auto)
    9.60      then have one: 
    9.61 -      "[gsetprod id F = gsetprod (StandardRes p o (op - p)) E] (mod p)";
    9.62 +      "[setprod id F = setprod (StandardRes p o (op - p)) E] (mod p)"
    9.63        apply simp
    9.64        apply (insert p_g_0 finite_E)
    9.65        by (auto simp add: StandardRes_prod)
    9.66 -    moreover have a: "\<forall>x \<in> E. [p - x = 0 - x] (mod p)";
    9.67 +    moreover have a: "\<forall>x \<in> E. [p - x = 0 - x] (mod p)"
    9.68        apply clarify
    9.69        apply (insert zcong_id [of p])
    9.70        by (rule_tac a = p and m = p and c = x and d = x in zcong_zdiff, auto)
    9.71 -    moreover have b: "\<forall>x \<in> E. [StandardRes p (p - x) = p - x](mod p)";
    9.72 +    moreover have b: "\<forall>x \<in> E. [StandardRes p (p - x) = p - x](mod p)"
    9.73        apply clarify
    9.74        by (simp add: StandardRes_prop1 zcong_sym)
    9.75 -    moreover have "\<forall>x \<in> E. [StandardRes p (p - x) = - x](mod p)";
    9.76 +    moreover have "\<forall>x \<in> E. [StandardRes p (p - x) = - x](mod p)"
    9.77        apply clarify
    9.78        apply (insert a b)
    9.79        by (rule_tac b = "p - x" in zcong_trans, auto)
    9.80      ultimately have c:
    9.81 -      "[gsetprod (StandardRes p o (op - p)) E = gsetprod (uminus) E](mod p)";
    9.82 +      "[setprod (StandardRes p o (op - p)) E = setprod (uminus) E](mod p)"
    9.83        apply simp
    9.84        apply (insert finite_E p_g_0)
    9.85 -      by (frule gsetprod_same_function_zcong [of E "StandardRes p o (op - p)"
    9.86 -                                                     uminus p], auto);
    9.87 -    then have two: "[gsetprod id F = gsetprod (uminus) E](mod p)";
    9.88 +      by (rule setprod_same_function_zcong [of E "StandardRes p o (op - p)"
    9.89 +                                                     uminus p], auto)
    9.90 +    then have two: "[setprod id F = setprod (uminus) E](mod p)"
    9.91        apply (insert one c)
    9.92 -      by (rule zcong_trans [of "gsetprod id F" 
    9.93 -                               "gsetprod (StandardRes p o op - p) E" p
    9.94 -                               "gsetprod uminus E"], auto); 
    9.95 -    also have "gsetprod uminus E = (gsetprod id E) * (-1)^(card E)"; 
    9.96 +      by (rule zcong_trans [of "setprod id F" 
    9.97 +                               "setprod (StandardRes p o op - p) E" p
    9.98 +                               "setprod uminus E"], auto) 
    9.99 +    also have "setprod uminus E = (setprod id E) * (-1)^(card E)" 
   9.100        apply (insert finite_E)
   9.101        by (induct set: Finites, auto)
   9.102 -    then have "gsetprod uminus E = (-1) ^ (card E) * (gsetprod id E)";
   9.103 +    then have "setprod uminus E = (-1) ^ (card E) * (setprod id E)"
   9.104        by (simp add: zmult_commute)
   9.105      with two show ?thesis
   9.106        by simp
   9.107 -qed;
   9.108 +qed
   9.109  
   9.110  subsection {* Gauss' Lemma *}
   9.111  
   9.112 -lemma (in GAUSS) aux: "gsetprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = gsetprod id A * a ^ card A";
   9.113 +lemma (in GAUSS) aux: "setprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = setprod id A * a ^ card A"
   9.114    by (auto simp add: finite_E neg_one_special)
   9.115  
   9.116  theorem (in GAUSS) pre_gauss_lemma:
   9.117 -    "[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)";
   9.118 -  proof -;
   9.119 -    have "[gsetprod id A = gsetprod id F * gsetprod id D](mod p)";
   9.120 +    "[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)"
   9.121 +  proof -
   9.122 +    have "[setprod id A = setprod id F * setprod id D](mod p)"
   9.123        by (auto simp add: prod_D_F_eq_prod_A zmult_commute)
   9.124 -    then have "[gsetprod id A = ((-1)^(card E) * gsetprod id E) * 
   9.125 -        gsetprod id D] (mod p)";
   9.126 +    then have "[setprod id A = ((-1)^(card E) * setprod id E) * 
   9.127 +        setprod id D] (mod p)"
   9.128        apply (rule zcong_trans)
   9.129        by (auto simp add: prod_F_zcong zcong_scalar)
   9.130 -    then have "[gsetprod id A = ((-1)^(card E) * gsetprod id C)] (mod p)";
   9.131 +    then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
   9.132        apply (rule zcong_trans)
   9.133        apply (insert C_prod_eq_D_times_E, erule subst)
   9.134        by (subst zmult_assoc, auto)
   9.135 -    then have "[gsetprod id A = ((-1)^(card E) * gsetprod id B)] (mod p)"
   9.136 +    then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
   9.137        apply (rule zcong_trans)
   9.138        by (simp add: C_B_zcong_prod zcong_scalar2)
   9.139 -    then have "[gsetprod id A = ((-1)^(card E) *
   9.140 -        (gsetprod id ((%x. x * a) ` A)))] (mod p)";
   9.141 +    then have "[setprod id A = ((-1)^(card E) *
   9.142 +        (setprod id ((%x. x * a) ` A)))] (mod p)"
   9.143        by (simp add: B_def)
   9.144 -    then have "[gsetprod id A = ((-1)^(card E) * (gsetprod (%x. x * a) A))] 
   9.145 -        (mod p)";
   9.146 +    then have "[setprod id A = ((-1)^(card E) * (setprod (%x. x * a) A))] 
   9.147 +        (mod p)"
   9.148        apply (rule zcong_trans)
   9.149 -      by (simp add: finite_A inj_on_xa_A prod_prop_id zcong_scalar2)
   9.150 -    moreover have "gsetprod (%x. x * a) A = 
   9.151 -        gsetprod (%x. a) A * gsetprod id A";
   9.152 +      by (simp add: finite_A inj_on_xa_A setprod_reindex_id zcong_scalar2)
   9.153 +    moreover have "setprod (%x. x * a) A = 
   9.154 +        setprod (%x. a) A * setprod id A"
   9.155        by (insert finite_A, induct set: Finites, auto)
   9.156 -    ultimately have "[gsetprod id A = ((-1)^(card E) * (gsetprod (%x. a) A * 
   9.157 -        gsetprod id A))] (mod p)";
   9.158 +    ultimately have "[setprod id A = ((-1)^(card E) * (setprod (%x. a) A * 
   9.159 +        setprod id A))] (mod p)"
   9.160        by simp 
   9.161 -    then have "[gsetprod id A = ((-1)^(card E) * a^(card A) * 
   9.162 -        gsetprod id A)](mod p)";
   9.163 +    then have "[setprod id A = ((-1)^(card E) * a^(card A) * 
   9.164 +        setprod id A)](mod p)"
   9.165        apply (rule zcong_trans)
   9.166 -      by (simp add: zcong_scalar2 zcong_scalar finite_A gsetprod_const
   9.167 +      by (simp add: zcong_scalar2 zcong_scalar finite_A setprod_constant
   9.168          zmult_assoc)
   9.169 -    then have a: "[gsetprod id A * (-1)^(card E) = 
   9.170 -        ((-1)^(card E) * a^(card A) * gsetprod id A * (-1)^(card E))](mod p)";
   9.171 +    then have a: "[setprod id A * (-1)^(card E) = 
   9.172 +        ((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)"
   9.173        by (rule zcong_scalar)
   9.174 -    then have "[gsetprod id A * (-1)^(card E) = gsetprod id A * 
   9.175 -        (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)";
   9.176 +    then have "[setprod id A * (-1)^(card E) = setprod id A * 
   9.177 +        (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
   9.178        apply (rule zcong_trans)
   9.179        by (simp add: a mult_commute mult_left_commute)
   9.180 -    then have "[gsetprod id A * (-1)^(card E) = gsetprod id A * 
   9.181 -        a^(card A)](mod p)";
   9.182 +    then have "[setprod id A * (-1)^(card E) = setprod id A * 
   9.183 +        a^(card A)](mod p)"
   9.184        apply (rule zcong_trans)
   9.185        by (simp add: aux)
   9.186 -    with this zcong_cancel2 [of p "gsetprod id A" "-1 ^ card E" "a ^ card A"]
   9.187 -         p_g_0 A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)";
   9.188 +    with this zcong_cancel2 [of p "setprod id A" "-1 ^ card E" "a ^ card A"]
   9.189 +         p_g_0 A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)"
   9.190         by (simp add: order_less_imp_le)
   9.191      from this show ?thesis
   9.192        by (simp add: A_card_eq zcong_sym)
   9.193 -qed;
   9.194 +qed
   9.195  
   9.196 -theorem (in GAUSS) gauss_lemma: "(Legendre a p) = (-1) ^ (card E)";
   9.197 -proof -;
   9.198 +theorem (in GAUSS) gauss_lemma: "(Legendre a p) = (-1) ^ (card E)"
   9.199 +proof -
   9.200    from Euler_Criterion p_prime p_g_2 have
   9.201 -    "[(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)";
   9.202 +    "[(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)"
   9.203      by auto
   9.204 -  moreover note pre_gauss_lemma;
   9.205 -  ultimately have "[(Legendre a p) = (-1) ^ (card E)] (mod p)";
   9.206 +  moreover note pre_gauss_lemma
   9.207 +  ultimately have "[(Legendre a p) = (-1) ^ (card E)] (mod p)"
   9.208      by (rule zcong_trans)
   9.209 -  moreover from p_a_relprime have "(Legendre a p) = 1 | (Legendre a p) = (-1)";
   9.210 +  moreover from p_a_relprime have "(Legendre a p) = 1 | (Legendre a p) = (-1)"
   9.211      by (auto simp add: Legendre_def)
   9.212 -  moreover have "(-1::int) ^ (card E) = 1 | (-1::int) ^ (card E) = -1";
   9.213 +  moreover have "(-1::int) ^ (card E) = 1 | (-1::int) ^ (card E) = -1"
   9.214      by (rule neg_one_power)
   9.215 -  ultimately show ?thesis;
   9.216 +  ultimately show ?thesis
   9.217      by (auto simp add: p_g_2 one_not_neg_one_mod_m zcong_sym)
   9.218 -qed;
   9.219 +qed
   9.220  
   9.221 -end;
   9.222 \ No newline at end of file
   9.223 +end
   9.224 \ No newline at end of file
    10.1 --- a/src/HOL/NumberTheory/Int2.thy	Thu Dec 09 16:45:46 2004 +0100
    10.2 +++ b/src/HOL/NumberTheory/Int2.thy	Thu Dec 09 18:30:59 2004 +0100
    10.3 @@ -178,7 +178,7 @@
    10.4  by (frule_tac m = m in zcong_not_zero, auto)
    10.5  
    10.6  lemma all_relprime_prod_relprime: "[| finite A; \<forall>x \<in> A. (zgcd(x,y) = 1) |]
    10.7 -    ==> zgcd (gsetprod id A,y) = 1";
    10.8 +    ==> zgcd (setprod id A,y) = 1";
    10.9    by (induct set: Finites, auto simp add: zgcd_zgcd_zmult)
   10.10  
   10.11  (*****************************************************************)
    11.1 --- a/src/HOL/NumberTheory/IntFact.thy	Thu Dec 09 16:45:46 2004 +0100
    11.2 +++ b/src/HOL/NumberTheory/IntFact.thy	Thu Dec 09 18:30:59 2004 +0100
    11.3 @@ -18,29 +18,15 @@
    11.4  
    11.5  consts
    11.6    zfact :: "int => int"
    11.7 -  setprod :: "int set => int"
    11.8    d22set :: "int => int set"
    11.9  
   11.10  recdef zfact  "measure ((\<lambda>n. nat n) :: int => nat)"
   11.11    "zfact n = (if n \<le> 0 then 1 else n * zfact (n - 1))"
   11.12  
   11.13 -defs
   11.14 -  setprod_def: "setprod A == (if finite A then fold (op *) 1 A else 1)"
   11.15 -
   11.16  recdef d22set  "measure ((\<lambda>a. nat a) :: int => nat)"
   11.17    "d22set a = (if 1 < a then insert a (d22set (a - 1)) else {})"
   11.18  
   11.19  
   11.20 -text {* \medskip @{term setprod} --- product of finite set *}
   11.21 -
   11.22 -lemma setprod_empty [simp]: "setprod {} = 1"
   11.23 -  apply (simp add: setprod_def)
   11.24 -  done
   11.25 -
   11.26 -lemma setprod_insert [simp]:
   11.27 -    "finite A ==> a \<notin> A ==> setprod (insert a A) = a * setprod A"
   11.28 -  by (simp add: setprod_def mult_left_commute LC.fold_insert [OF LC.intro])
   11.29 -
   11.30  text {*
   11.31    \medskip @{term d22set} --- recursively defined set including all
   11.32    integers from @{text 2} up to @{text a}
   11.33 @@ -100,7 +86,7 @@
   11.34  
   11.35  declare zfact.simps [simp del]
   11.36  
   11.37 -lemma d22set_prod_zfact: "setprod (d22set a) = zfact a"
   11.38 +lemma d22set_prod_zfact: "\<Prod>(d22set a) = zfact a"
   11.39    apply (induct a rule: d22set.induct)
   11.40    apply safe
   11.41     apply (simp add: d22set.simps zfact.simps)
    12.1 --- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Thu Dec 09 16:45:46 2004 +0100
    12.2 +++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Thu Dec 09 18:30:59 2004 +0100
    12.3 @@ -5,7 +5,9 @@
    12.4  
    12.5  header {* The law of Quadratic reciprocity *}
    12.6  
    12.7 -theory Quadratic_Reciprocity = Gauss:;
    12.8 +theory Quadratic_Reciprocity
    12.9 +imports Gauss
   12.10 +begin
   12.11  
   12.12  (***************************************************************)
   12.13  (*                                                             *)
   12.14 @@ -15,137 +17,137 @@
   12.15  (***************************************************************)
   12.16  
   12.17  lemma (in GAUSS) QRLemma1: "a * setsum id A = 
   12.18 -  p * setsum (%x. ((x * a) div p)) A + setsum id D + setsum id E";
   12.19 -proof -;
   12.20 -  from finite_A have "a * setsum id A = setsum (%x. a * x) A"; 
   12.21 +  p * setsum (%x. ((x * a) div p)) A + setsum id D + setsum id E"
   12.22 +proof -
   12.23 +  from finite_A have "a * setsum id A = setsum (%x. a * x) A" 
   12.24      by (auto simp add: setsum_const_mult id_def)
   12.25 -  also have "setsum (%x. a * x) = setsum (%x. x * a)"; 
   12.26 +  also have "setsum (%x. a * x) = setsum (%x. x * a)" 
   12.27      by (auto simp add: zmult_commute)
   12.28 -  also; have "setsum (%x. x * a) A = setsum id B";
   12.29 -    by (auto simp add: B_def sum_prop_id finite_A inj_on_xa_A)
   12.30 -  also have "... = setsum (%x. p * (x div p) + StandardRes p x) B";
   12.31 -    apply (rule setsum_same_function)
   12.32 +  also have "setsum (%x. x * a) A = setsum id B"
   12.33 +    by (auto simp add: B_def setsum_reindex_id finite_A inj_on_xa_A)
   12.34 +  also have "... = setsum (%x. p * (x div p) + StandardRes p x) B"
   12.35 +    apply (rule setsum_cong)
   12.36      by (auto simp add: finite_B StandardRes_def zmod_zdiv_equality)
   12.37 -  also have "... = setsum (%x. p * (x div p)) B + setsum (StandardRes p) B";
   12.38 +  also have "... = setsum (%x. p * (x div p)) B + setsum (StandardRes p) B"
   12.39      by (rule setsum_addf)
   12.40 -  also; have "setsum (StandardRes p) B = setsum id C";
   12.41 -    by (auto simp add: C_def sum_prop_id [THEN sym] finite_B 
   12.42 +  also have "setsum (StandardRes p) B = setsum id C"
   12.43 +    by (auto simp add: C_def setsum_reindex_id [THEN sym] finite_B 
   12.44        SR_B_inj)
   12.45 -  also; from C_eq have "... = setsum id (D \<union> E)";
   12.46 +  also from C_eq have "... = setsum id (D \<union> E)"
   12.47      by auto
   12.48 -  also; from finite_D finite_E have "... = setsum id D + setsum id E";
   12.49 +  also from finite_D finite_E have "... = setsum id D + setsum id E"
   12.50      apply (rule setsum_Un_disjoint)
   12.51      by (auto simp add: D_def E_def)
   12.52    also have "setsum (%x. p * (x div p)) B = 
   12.53 -      setsum ((%x. p * (x div p)) o (%x. (x * a))) A";
   12.54 -    by (auto simp add: B_def sum_prop finite_A inj_on_xa_A)
   12.55 -  also have "... = setsum (%x. p * ((x * a) div p)) A";
   12.56 +      setsum ((%x. p * (x div p)) o (%x. (x * a))) A"
   12.57 +    by (auto simp add: B_def setsum_reindex finite_A inj_on_xa_A)
   12.58 +  also have "... = setsum (%x. p * ((x * a) div p)) A"
   12.59      by (auto simp add: o_def)
   12.60    also from finite_A have "setsum (%x. p * ((x * a) div p)) A = 
   12.61 -    p * setsum (%x. ((x * a) div p)) A";
   12.62 +    p * setsum (%x. ((x * a) div p)) A"
   12.63      by (auto simp add: setsum_const_mult)
   12.64    finally show ?thesis by arith
   12.65 -qed;
   12.66 +qed
   12.67  
   12.68  lemma (in GAUSS) QRLemma2: "setsum id A = p * int (card E) - setsum id E + 
   12.69 -  setsum id D"; 
   12.70 -proof -;
   12.71 -  from F_Un_D_eq_A have "setsum id A = setsum id (D \<union> F)";
   12.72 +  setsum id D" 
   12.73 +proof -
   12.74 +  from F_Un_D_eq_A have "setsum id A = setsum id (D \<union> F)"
   12.75      by (simp add: Un_commute)
   12.76    also from F_D_disj finite_D finite_F have 
   12.77 -      "... = setsum id D + setsum id F";
   12.78 +      "... = setsum id D + setsum id F"
   12.79      apply (simp add: Int_commute)
   12.80      by (intro setsum_Un_disjoint) 
   12.81 -  also from F_def have "F = (%x. (p - x)) ` E";
   12.82 +  also from F_def have "F = (%x. (p - x)) ` E"
   12.83      by auto
   12.84    also from finite_E inj_on_pminusx_E have "setsum id ((%x. (p - x)) ` E) =
   12.85 -      setsum (%x. (p - x)) E";
   12.86 -    by (auto simp add: sum_prop)
   12.87 -  also from finite_E have "setsum (op - p) E = setsum (%x. p) E - setsum id E";
   12.88 -    by (auto simp add: setsum_minus id_def)
   12.89 -  also from finite_E have "setsum (%x. p) E = p * int(card E)";
   12.90 +      setsum (%x. (p - x)) E"
   12.91 +    by (auto simp add: setsum_reindex)
   12.92 +  also from finite_E have "setsum (op - p) E = setsum (%x. p) E - setsum id E"
   12.93 +    by (auto simp add: setsum_subtractf id_def)
   12.94 +  also from finite_E have "setsum (%x. p) E = p * int(card E)"
   12.95      by (intro setsum_const)
   12.96 -  finally show ?thesis;
   12.97 +  finally show ?thesis
   12.98      by arith
   12.99 -qed;
  12.100 +qed
  12.101  
  12.102  lemma (in GAUSS) QRLemma3: "(a - 1) * setsum id A = 
  12.103 -    p * (setsum (%x. ((x * a) div p)) A - int(card E)) + 2 * setsum id E";
  12.104 -proof -;
  12.105 -  have "(a - 1) * setsum id A = a * setsum id A - setsum id A";
  12.106 +    p * (setsum (%x. ((x * a) div p)) A - int(card E)) + 2 * setsum id E"
  12.107 +proof -
  12.108 +  have "(a - 1) * setsum id A = a * setsum id A - setsum id A"
  12.109      by (auto simp add: zdiff_zmult_distrib)  
  12.110 -  also note QRLemma1;
  12.111 -  also; from QRLemma2 have "p * (\<Sum>x \<in> A. x * a div p) + setsum id D + 
  12.112 +  also note QRLemma1
  12.113 +  also from QRLemma2 have "p * (\<Sum>x \<in> A. x * a div p) + setsum id D + 
  12.114       setsum id E - setsum id A = 
  12.115        p * (\<Sum>x \<in> A. x * a div p) + setsum id D + 
  12.116 -      setsum id E - (p * int (card E) - setsum id E + setsum id D)";
  12.117 +      setsum id E - (p * int (card E) - setsum id E + setsum id D)"
  12.118      by auto
  12.119 -  also; have "... = p * (\<Sum>x \<in> A. x * a div p) - 
  12.120 -      p * int (card E) + 2 * setsum id E"; 
  12.121 +  also have "... = p * (\<Sum>x \<in> A. x * a div p) - 
  12.122 +      p * int (card E) + 2 * setsum id E" 
  12.123      by arith
  12.124 -  finally show ?thesis;
  12.125 +  finally show ?thesis
  12.126      by (auto simp only: zdiff_zmult_distrib2)
  12.127 -qed;
  12.128 +qed
  12.129  
  12.130  lemma (in GAUSS) QRLemma4: "a \<in> zOdd ==> 
  12.131 -    (setsum (%x. ((x * a) div p)) A \<in> zEven) = (int(card E): zEven)";
  12.132 -proof -;
  12.133 -  assume a_odd: "a \<in> zOdd";
  12.134 +    (setsum (%x. ((x * a) div p)) A \<in> zEven) = (int(card E): zEven)"
  12.135 +proof -
  12.136 +  assume a_odd: "a \<in> zOdd"
  12.137    from QRLemma3 have a: "p * (setsum (%x. ((x * a) div p)) A - int(card E)) =
  12.138 -      (a - 1) * setsum id A - 2 * setsum id E"; 
  12.139 +      (a - 1) * setsum id A - 2 * setsum id E" 
  12.140      by arith
  12.141    from a_odd have "a - 1 \<in> zEven"
  12.142      by (rule odd_minus_one_even)
  12.143 -  hence "(a - 1) * setsum id A \<in> zEven";
  12.144 +  hence "(a - 1) * setsum id A \<in> zEven"
  12.145      by (rule even_times_either)
  12.146 -  moreover have "2 * setsum id E \<in> zEven";
  12.147 +  moreover have "2 * setsum id E \<in> zEven"
  12.148      by (auto simp add: zEven_def)
  12.149    ultimately have "(a - 1) * setsum id A - 2 * setsum id E \<in> zEven"
  12.150      by (rule even_minus_even)
  12.151 -  with a have "p * (setsum (%x. ((x * a) div p)) A - int(card E)): zEven";
  12.152 +  with a have "p * (setsum (%x. ((x * a) div p)) A - int(card E)): zEven"
  12.153      by simp
  12.154 -  hence "p \<in> zEven | (setsum (%x. ((x * a) div p)) A - int(card E)): zEven";
  12.155 +  hence "p \<in> zEven | (setsum (%x. ((x * a) div p)) A - int(card E)): zEven"
  12.156      by (rule EvenOdd.even_product)
  12.157 -  with p_odd have "(setsum (%x. ((x * a) div p)) A - int(card E)): zEven";
  12.158 +  with p_odd have "(setsum (%x. ((x * a) div p)) A - int(card E)): zEven"
  12.159      by (auto simp add: odd_iff_not_even)
  12.160 -  thus ?thesis;
  12.161 +  thus ?thesis
  12.162      by (auto simp only: even_diff [THEN sym])
  12.163 -qed;
  12.164 +qed
  12.165  
  12.166  lemma (in GAUSS) QRLemma5: "a \<in> zOdd ==> 
  12.167 -   (-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))";
  12.168 -proof -;
  12.169 -  assume "a \<in> zOdd";
  12.170 +   (-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))"
  12.171 +proof -
  12.172 +  assume "a \<in> zOdd"
  12.173    from QRLemma4 have
  12.174 -    "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)";..;
  12.175 -  moreover have "0 \<le> int(card E)";
  12.176 +    "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)"..
  12.177 +  moreover have "0 \<le> int(card E)"
  12.178      by auto
  12.179 -  moreover have "0 \<le> setsum (%x. ((x * a) div p)) A";
  12.180 -    proof (intro setsum_non_neg);
  12.181 -      from finite_A show "finite A";.;
  12.182 -      next show "\<forall>x \<in> A. 0 \<le> x * a div p";
  12.183 -      proof;
  12.184 -        fix x;
  12.185 -        assume "x \<in> A";
  12.186 -        then have "0 \<le> x";
  12.187 +  moreover have "0 \<le> setsum (%x. ((x * a) div p)) A"
  12.188 +    proof (intro setsum_nonneg)
  12.189 +      from finite_A show "finite A".
  12.190 +      next show "\<forall>x \<in> A. 0 \<le> x * a div p"
  12.191 +      proof
  12.192 +        fix x
  12.193 +        assume "x \<in> A"
  12.194 +        then have "0 \<le> x"
  12.195            by (auto simp add: A_def)
  12.196 -        with a_nonzero have "0 \<le> x * a";
  12.197 +        with a_nonzero have "0 \<le> x * a"
  12.198            by (auto simp add: zero_le_mult_iff)
  12.199 -        with p_g_2 show "0 \<le> x * a div p"; 
  12.200 +        with p_g_2 show "0 \<le> x * a div p" 
  12.201            by (auto simp add: pos_imp_zdiv_nonneg_iff)
  12.202 -      qed;
  12.203 -    qed;
  12.204 +      qed
  12.205 +    qed
  12.206    ultimately have "(-1::int)^nat((int (card E))) =
  12.207 -      (-1)^nat(((\<Sum>x \<in> A. x * a div p)))";
  12.208 +      (-1)^nat(((\<Sum>x \<in> A. x * a div p)))"
  12.209      by (intro neg_one_power_parity, auto)
  12.210 -  also have "nat (int(card E)) = card E";
  12.211 +  also have "nat (int(card E)) = card E"
  12.212      by auto
  12.213 -  finally show ?thesis;.;
  12.214 -qed;
  12.215 +  finally show ?thesis .
  12.216 +qed
  12.217  
  12.218  lemma MainQRLemma: "[| a \<in> zOdd; 0 < a; ~([a = 0] (mod p));p \<in> zprime; 2 < p;
  12.219    A = {x. 0 < x & x \<le> (p - 1) div 2} |] ==> 
  12.220 -  (Legendre a p) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))";
  12.221 +  (Legendre a p) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))"
  12.222    apply (subst GAUSS.gauss_lemma)
  12.223    apply (auto simp add: GAUSS_def)
  12.224    apply (subst GAUSS.QRLemma5)
  12.225 @@ -182,34 +184,34 @@
  12.226    defines f1_def:    "f1 j  == { (j1, y). (j1, y):S & j1 = j & 
  12.227                                   (y \<le> (q * j) div p) }"
  12.228    defines f2_def:    "f2 j  == { (x, j1). (x, j1):S & j1 = j & 
  12.229 -                                 (x \<le> (p * j) div q) }";
  12.230 +                                 (x \<le> (p * j) div q) }"
  12.231  
  12.232 -lemma (in QRTEMP) p_fact: "0 < (p - 1) div 2";
  12.233 -proof -;
  12.234 +lemma (in QRTEMP) p_fact: "0 < (p - 1) div 2"
  12.235 +proof -
  12.236    from prems have "2 < p" by (simp add: QRTEMP_def)
  12.237    then have "2 \<le> p - 1" by arith
  12.238    then have "2 div 2 \<le> (p - 1) div 2" by (rule zdiv_mono1, auto)
  12.239    then show ?thesis by auto
  12.240 -qed;
  12.241 +qed
  12.242  
  12.243 -lemma (in QRTEMP) q_fact: "0 < (q - 1) div 2";
  12.244 -proof -;
  12.245 +lemma (in QRTEMP) q_fact: "0 < (q - 1) div 2"
  12.246 +proof -
  12.247    from prems have "2 < q" by (simp add: QRTEMP_def)
  12.248    then have "2 \<le> q - 1" by arith
  12.249    then have "2 div 2 \<le> (q - 1) div 2" by (rule zdiv_mono1, auto)
  12.250    then show ?thesis by auto
  12.251 -qed;
  12.252 +qed
  12.253  
  12.254  lemma (in QRTEMP) pb_neq_qa: "[|1 \<le> b; b \<le> (q - 1) div 2 |] ==> 
  12.255 -    (p * b \<noteq> q * a)";
  12.256 -proof;
  12.257 -  assume "p * b = q * a" and "1 \<le> b" and "b \<le> (q - 1) div 2";
  12.258 +    (p * b \<noteq> q * a)"
  12.259 +proof
  12.260 +  assume "p * b = q * a" and "1 \<le> b" and "b \<le> (q - 1) div 2"
  12.261    then have "q dvd (p * b)" by (auto simp add: dvd_def)
  12.262 -  with q_prime p_g_2 have "q dvd p | q dvd b";
  12.263 +  with q_prime p_g_2 have "q dvd p | q dvd b"
  12.264      by (auto simp add: zprime_zdvd_zmult)
  12.265 -  moreover have "~ (q dvd p)";
  12.266 -  proof;
  12.267 -    assume "q dvd p";
  12.268 +  moreover have "~ (q dvd p)"
  12.269 +  proof
  12.270 +    assume "q dvd p"
  12.271      with p_prime have "q = 1 | q = p"
  12.272        apply (auto simp add: zprime_def QRTEMP_def)
  12.273        apply (drule_tac x = q and R = False in allE)
  12.274 @@ -218,410 +220,404 @@
  12.275        apply (insert prems)
  12.276      by (auto simp add: QRTEMP_def)
  12.277      with q_g_2 p_neq_q show False by auto
  12.278 -  qed;
  12.279 +  qed
  12.280    ultimately have "q dvd b" by auto
  12.281 -  then have "q \<le> b";
  12.282 -  proof -;
  12.283 -    assume "q dvd b";
  12.284 +  then have "q \<le> b"
  12.285 +  proof -
  12.286 +    assume "q dvd b"
  12.287      moreover from prems have "0 < b" by auto
  12.288      ultimately show ?thesis by (insert zdvd_bounds [of q b], auto)
  12.289 -  qed;
  12.290 +  qed
  12.291    with prems have "q \<le> (q - 1) div 2" by auto
  12.292    then have "2 * q \<le> 2 * ((q - 1) div 2)" by arith
  12.293 -  then have "2 * q \<le> q - 1";
  12.294 -  proof -;
  12.295 -    assume "2 * q \<le> 2 * ((q - 1) div 2)";
  12.296 +  then have "2 * q \<le> q - 1"
  12.297 +  proof -
  12.298 +    assume "2 * q \<le> 2 * ((q - 1) div 2)"
  12.299      with prems have "q \<in> zOdd" by (auto simp add: QRTEMP_def zprime_zOdd_eq_grt_2)
  12.300      with odd_minus_one_even have "(q - 1):zEven" by auto
  12.301      with even_div_2_prop2 have "(q - 1) = 2 * ((q - 1) div 2)" by auto
  12.302      with prems show ?thesis by auto
  12.303 -  qed;
  12.304 +  qed
  12.305    then have p1: "q \<le> -1" by arith
  12.306    with q_g_2 show False by auto
  12.307 -qed;
  12.308 +qed
  12.309  
  12.310 -lemma (in QRTEMP) P_set_finite: "finite (P_set)";
  12.311 +lemma (in QRTEMP) P_set_finite: "finite (P_set)"
  12.312    by (insert p_fact, auto simp add: P_set_def bdd_int_set_l_le_finite)
  12.313  
  12.314 -lemma (in QRTEMP) Q_set_finite: "finite (Q_set)";
  12.315 +lemma (in QRTEMP) Q_set_finite: "finite (Q_set)"
  12.316    by (insert q_fact, auto simp add: Q_set_def bdd_int_set_l_le_finite)
  12.317  
  12.318 -lemma (in QRTEMP) S_finite: "finite S";
  12.319 +lemma (in QRTEMP) S_finite: "finite S"
  12.320    by (auto simp add: S_def  P_set_finite Q_set_finite cartesian_product_finite)
  12.321  
  12.322 -lemma (in QRTEMP) S1_finite: "finite S1";
  12.323 -proof -;
  12.324 +lemma (in QRTEMP) S1_finite: "finite S1"
  12.325 +proof -
  12.326    have "finite S" by (auto simp add: S_finite)
  12.327    moreover have "S1 \<subseteq> S" by (auto simp add: S1_def S_def)
  12.328    ultimately show ?thesis by (auto simp add: finite_subset)
  12.329 -qed;
  12.330 +qed
  12.331  
  12.332 -lemma (in QRTEMP) S2_finite: "finite S2";
  12.333 -proof -;
  12.334 +lemma (in QRTEMP) S2_finite: "finite S2"
  12.335 +proof -
  12.336    have "finite S" by (auto simp add: S_finite)
  12.337    moreover have "S2 \<subseteq> S" by (auto simp add: S2_def S_def)
  12.338    ultimately show ?thesis by (auto simp add: finite_subset)
  12.339 -qed;
  12.340 +qed
  12.341  
  12.342 -lemma (in QRTEMP) P_set_card: "(p - 1) div 2 = int (card (P_set))";
  12.343 +lemma (in QRTEMP) P_set_card: "(p - 1) div 2 = int (card (P_set))"
  12.344    by (insert p_fact, auto simp add: P_set_def card_bdd_int_set_l_le)
  12.345  
  12.346 -lemma (in QRTEMP) Q_set_card: "(q - 1) div 2 = int (card (Q_set))";
  12.347 +lemma (in QRTEMP) Q_set_card: "(q - 1) div 2 = int (card (Q_set))"
  12.348    by (insert q_fact, auto simp add: Q_set_def card_bdd_int_set_l_le)
  12.349  
  12.350 -lemma (in QRTEMP) S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))";
  12.351 +lemma (in QRTEMP) S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))"
  12.352    apply (insert P_set_card Q_set_card P_set_finite Q_set_finite)
  12.353    apply (auto simp add: S_def zmult_int setsum_constant_nat) 
  12.354  done
  12.355  
  12.356 -lemma (in QRTEMP) S1_Int_S2_prop: "S1 \<inter> S2 = {}";
  12.357 +lemma (in QRTEMP) S1_Int_S2_prop: "S1 \<inter> S2 = {}"
  12.358    by (auto simp add: S1_def S2_def)
  12.359  
  12.360 -lemma (in QRTEMP) S1_Union_S2_prop: "S = S1 \<union> S2";
  12.361 +lemma (in QRTEMP) S1_Union_S2_prop: "S = S1 \<union> S2"
  12.362    apply (auto simp add: S_def P_set_def Q_set_def S1_def S2_def)
  12.363 -  proof -;
  12.364 -    fix a and b;
  12.365 -    assume "~ q * a < p * b" and b1: "0 < b" and b2: "b \<le> (q - 1) div 2";
  12.366 +  proof -
  12.367 +    fix a and b
  12.368 +    assume "~ q * a < p * b" and b1: "0 < b" and b2: "b \<le> (q - 1) div 2"
  12.369      with zless_linear have "(p * b < q * a) | (p * b = q * a)" by auto
  12.370      moreover from pb_neq_qa b1 b2 have "(p * b \<noteq> q * a)" by auto
  12.371      ultimately show "p * b < q * a" by auto
  12.372 -  qed;
  12.373 +  qed
  12.374  
  12.375  lemma (in QRTEMP) card_sum_S1_S2: "((p - 1) div 2) * ((q - 1) div 2) = 
  12.376 -    int(card(S1)) + int(card(S2))";
  12.377 -proof-;
  12.378 -  have "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))";
  12.379 +    int(card(S1)) + int(card(S2))"
  12.380 +proof-
  12.381 +  have "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))"
  12.382      by (auto simp add: S_card)
  12.383 -  also have "... = int( card(S1) + card(S2))";
  12.384 +  also have "... = int( card(S1) + card(S2))"
  12.385      apply (insert S1_finite S2_finite S1_Int_S2_prop S1_Union_S2_prop)
  12.386      apply (drule card_Un_disjoint, auto)
  12.387    done
  12.388    also have "... = int(card(S1)) + int(card(S2))" by auto
  12.389 -  finally show ?thesis .;
  12.390 -qed;
  12.391 +  finally show ?thesis .
  12.392 +qed
  12.393  
  12.394  lemma (in QRTEMP) aux1a: "[| 0 < a; a \<le> (p - 1) div 2; 
  12.395                               0 < b; b \<le> (q - 1) div 2 |] ==>
  12.396 -                          (p * b < q * a) = (b \<le> q * a div p)";
  12.397 -proof -;
  12.398 -  assume "0 < a" and "a \<le> (p - 1) div 2" and "0 < b" and "b \<le> (q - 1) div 2";
  12.399 -  have "p * b < q * a ==> b \<le> q * a div p";
  12.400 -  proof -;
  12.401 -    assume "p * b < q * a";
  12.402 +                          (p * b < q * a) = (b \<le> q * a div p)"
  12.403 +proof -
  12.404 +  assume "0 < a" and "a \<le> (p - 1) div 2" and "0 < b" and "b \<le> (q - 1) div 2"
  12.405 +  have "p * b < q * a ==> b \<le> q * a div p"
  12.406 +  proof -
  12.407 +    assume "p * b < q * a"
  12.408      then have "p * b \<le> q * a" by auto
  12.409 -    then have "(p * b) div p \<le> (q * a) div p";
  12.410 +    then have "(p * b) div p \<le> (q * a) div p"
  12.411        by (rule zdiv_mono1, insert p_g_2, auto)
  12.412 -    then show "b \<le> (q * a) div p";
  12.413 +    then show "b \<le> (q * a) div p"
  12.414        apply (subgoal_tac "p \<noteq> 0")
  12.415        apply (frule zdiv_zmult_self2, force)
  12.416        by (insert p_g_2, auto)
  12.417 -  qed;
  12.418 -  moreover have "b \<le> q * a div p ==> p * b < q * a";
  12.419 -  proof -;
  12.420 -    assume "b \<le> q * a div p";
  12.421 -    then have "p * b \<le> p * ((q * a) div p)";
  12.422 +  qed
  12.423 +  moreover have "b \<le> q * a div p ==> p * b < q * a"
  12.424 +  proof -
  12.425 +    assume "b \<le> q * a div p"
  12.426 +    then have "p * b \<le> p * ((q * a) div p)"
  12.427        by (insert p_g_2, auto simp add: mult_le_cancel_left)
  12.428 -    also have "... \<le> q * a";
  12.429 +    also have "... \<le> q * a"
  12.430        by (rule zdiv_leq_prop, insert p_g_2, auto)
  12.431 -    finally have "p * b \<le> q * a" .;
  12.432 -    then have "p * b < q * a | p * b = q * a";
  12.433 +    finally have "p * b \<le> q * a" .
  12.434 +    then have "p * b < q * a | p * b = q * a"
  12.435        by (simp only: order_le_imp_less_or_eq)
  12.436 -    moreover have "p * b \<noteq> q * a";
  12.437 +    moreover have "p * b \<noteq> q * a"
  12.438        by (rule  pb_neq_qa, insert prems, auto)
  12.439      ultimately show ?thesis by auto
  12.440 -  qed;
  12.441 -  ultimately show ?thesis ..;
  12.442 -qed;
  12.443 +  qed
  12.444 +  ultimately show ?thesis ..
  12.445 +qed
  12.446  
  12.447  lemma (in QRTEMP) aux1b: "[| 0 < a; a \<le> (p - 1) div 2; 
  12.448                               0 < b; b \<le> (q - 1) div 2 |] ==>
  12.449 -                          (q * a < p * b) = (a \<le> p * b div q)";
  12.450 -proof -;
  12.451 -  assume "0 < a" and "a \<le> (p - 1) div 2" and "0 < b" and "b \<le> (q - 1) div 2";
  12.452 -  have "q * a < p * b ==> a \<le> p * b div q";
  12.453 -  proof -;
  12.454 -    assume "q * a < p * b";
  12.455 +                          (q * a < p * b) = (a \<le> p * b div q)"
  12.456 +proof -
  12.457 +  assume "0 < a" and "a \<le> (p - 1) div 2" and "0 < b" and "b \<le> (q - 1) div 2"
  12.458 +  have "q * a < p * b ==> a \<le> p * b div q"
  12.459 +  proof -
  12.460 +    assume "q * a < p * b"
  12.461      then have "q * a \<le> p * b" by auto
  12.462 -    then have "(q * a) div q \<le> (p * b) div q";
  12.463 +    then have "(q * a) div q \<le> (p * b) div q"
  12.464        by (rule zdiv_mono1, insert q_g_2, auto)
  12.465 -    then show "a \<le> (p * b) div q";
  12.466 +    then show "a \<le> (p * b) div q"
  12.467        apply (subgoal_tac "q \<noteq> 0")
  12.468        apply (frule zdiv_zmult_self2, force)
  12.469        by (insert q_g_2, auto)
  12.470 -  qed;
  12.471 -  moreover have "a \<le> p * b div q ==> q * a < p * b";
  12.472 -  proof -;
  12.473 -    assume "a \<le> p * b div q";
  12.474 -    then have "q * a \<le> q * ((p * b) div q)";
  12.475 +  qed
  12.476 +  moreover have "a \<le> p * b div q ==> q * a < p * b"
  12.477 +  proof -
  12.478 +    assume "a \<le> p * b div q"
  12.479 +    then have "q * a \<le> q * ((p * b) div q)"
  12.480        by (insert q_g_2, auto simp add: mult_le_cancel_left)
  12.481 -    also have "... \<le> p * b";
  12.482 +    also have "... \<le> p * b"
  12.483        by (rule zdiv_leq_prop, insert q_g_2, auto)
  12.484 -    finally have "q * a \<le> p * b" .;
  12.485 -    then have "q * a < p * b | q * a = p * b";
  12.486 +    finally have "q * a \<le> p * b" .
  12.487 +    then have "q * a < p * b | q * a = p * b"
  12.488        by (simp only: order_le_imp_less_or_eq)
  12.489 -    moreover have "p * b \<noteq> q * a";
  12.490 +    moreover have "p * b \<noteq> q * a"
  12.491        by (rule  pb_neq_qa, insert prems, auto)
  12.492      ultimately show ?thesis by auto
  12.493 -  qed;
  12.494 -  ultimately show ?thesis ..;
  12.495 -qed;
  12.496 +  qed
  12.497 +  ultimately show ?thesis ..
  12.498 +qed
  12.499  
  12.500  lemma aux2: "[| p \<in> zprime; q \<in> zprime; 2 < p; 2 < q |] ==> 
  12.501 -             (q * ((p - 1) div 2)) div p \<le> (q - 1) div 2";
  12.502 -proof-;
  12.503 -  assume "p \<in> zprime" and "q \<in> zprime" and "2 < p" and "2 < q";
  12.504 +             (q * ((p - 1) div 2)) div p \<le> (q - 1) div 2"
  12.505 +proof-
  12.506 +  assume "p \<in> zprime" and "q \<in> zprime" and "2 < p" and "2 < q"
  12.507    (* Set up what's even and odd *)
  12.508 -  then have "p \<in> zOdd & q \<in> zOdd";
  12.509 +  then have "p \<in> zOdd & q \<in> zOdd"
  12.510      by (auto simp add:  zprime_zOdd_eq_grt_2)
  12.511 -  then have even1: "(p - 1):zEven & (q - 1):zEven";
  12.512 +  then have even1: "(p - 1):zEven & (q - 1):zEven"
  12.513      by (auto simp add: odd_minus_one_even)
  12.514 -  then have even2: "(2 * p):zEven & ((q - 1) * p):zEven";
  12.515 +  then have even2: "(2 * p):zEven & ((q - 1) * p):zEven"
  12.516      by (auto simp add: zEven_def)
  12.517 -  then have even3: "(((q - 1) * p) + (2 * p)):zEven";
  12.518 +  then have even3: "(((q - 1) * p) + (2 * p)):zEven"
  12.519      by (auto simp: EvenOdd.even_plus_even)
  12.520    (* using these prove it *)
  12.521 -  from prems have "q * (p - 1) < ((q - 1) * p) + (2 * p)";
  12.522 +  from prems have "q * (p - 1) < ((q - 1) * p) + (2 * p)"
  12.523      by (auto simp add: int_distrib)
  12.524 -  then have "((p - 1) * q) div 2 < (((q - 1) * p) + (2 * p)) div 2";
  12.525 -    apply (rule_tac x = "((p - 1) * q)" in even_div_2_l);
  12.526 +  then have "((p - 1) * q) div 2 < (((q - 1) * p) + (2 * p)) div 2"
  12.527 +    apply (rule_tac x = "((p - 1) * q)" in even_div_2_l)
  12.528      by (auto simp add: even3, auto simp add: zmult_ac)
  12.529 -  also have "((p - 1) * q) div 2 = q * ((p - 1) div 2)";
  12.530 +  also have "((p - 1) * q) div 2 = q * ((p - 1) div 2)"
  12.531      by (auto simp add: even1 even_prod_div_2)
  12.532 -  also have "(((q - 1) * p) + (2 * p)) div 2 = (((q - 1) div 2) * p) + p";
  12.533 +  also have "(((q - 1) * p) + (2 * p)) div 2 = (((q - 1) div 2) * p) + p"
  12.534      by (auto simp add: even1 even2 even_prod_div_2 even_sum_div_2)
  12.535    finally show ?thesis 
  12.536      apply (rule_tac x = " q * ((p - 1) div 2)" and 
  12.537 -                    y = "(q - 1) div 2" in div_prop2);
  12.538 +                    y = "(q - 1) div 2" in div_prop2)
  12.539      by (insert prems, auto)
  12.540 -qed;
  12.541 +qed
  12.542  
  12.543 -lemma (in QRTEMP) aux3a: "\<forall>j \<in> P_set. int (card (f1 j)) = (q * j) div p";
  12.544 -proof;
  12.545 -  fix j;
  12.546 -  assume j_fact: "j \<in> P_set";
  12.547 -  have "int (card (f1 j)) = int (card {y. y \<in> Q_set & y \<le> (q * j) div p})";
  12.548 -  proof -;
  12.549 -    have "finite (f1 j)";
  12.550 -    proof -;
  12.551 +lemma (in QRTEMP) aux3a: "\<forall>j \<in> P_set. int (card (f1 j)) = (q * j) div p"
  12.552 +proof
  12.553 +  fix j
  12.554 +  assume j_fact: "j \<in> P_set"
  12.555 +  have "int (card (f1 j)) = int (card {y. y \<in> Q_set & y \<le> (q * j) div p})"
  12.556 +  proof -
  12.557 +    have "finite (f1 j)"
  12.558 +    proof -
  12.559        have "(f1 j) \<subseteq> S" by (auto simp add: f1_def)
  12.560        with S_finite show ?thesis by (auto simp add: finite_subset)
  12.561 -    qed;
  12.562 -    moreover have "inj_on (%(x,y). y) (f1 j)";
  12.563 +    qed
  12.564 +    moreover have "inj_on (%(x,y). y) (f1 j)"
  12.565        by (auto simp add: f1_def inj_on_def)
  12.566 -    ultimately have "card ((%(x,y). y) ` (f1 j)) = card  (f1 j)";
  12.567 +    ultimately have "card ((%(x,y). y) ` (f1 j)) = card  (f1 j)"
  12.568        by (auto simp add: f1_def card_image)
  12.569 -    moreover have "((%(x,y). y) ` (f1 j)) = {y. y \<in> Q_set & y \<le> (q * j) div p}";
  12.570 +    moreover have "((%(x,y). y) ` (f1 j)) = {y. y \<in> Q_set & y \<le> (q * j) div p}"
  12.571        by (insert prems, auto simp add: f1_def S_def Q_set_def P_set_def 
  12.572          image_def)
  12.573      ultimately show ?thesis by (auto simp add: f1_def)
  12.574 -  qed;
  12.575 -  also have "... = int (card {y. 0 < y & y \<le> (q * j) div p})";
  12.576 -  proof -;
  12.577 +  qed
  12.578 +  also have "... = int (card {y. 0 < y & y \<le> (q * j) div p})"
  12.579 +  proof -
  12.580      have "{y. y \<in> Q_set & y \<le> (q * j) div p} = 
  12.581 -        {y. 0 < y & y \<le> (q * j) div p}";
  12.582 +        {y. 0 < y & y \<le> (q * j) div p}"
  12.583        apply (auto simp add: Q_set_def)
  12.584 -      proof -;
  12.585 -        fix x;
  12.586 -        assume "0 < x" and "x \<le> q * j div p";
  12.587 -        with j_fact P_set_def  have "j \<le> (p - 1) div 2"; by auto
  12.588 -        with q_g_2; have "q * j \<le> q * ((p - 1) div 2)";
  12.589 +      proof -
  12.590 +        fix x
  12.591 +        assume "0 < x" and "x \<le> q * j div p"
  12.592 +        with j_fact P_set_def  have "j \<le> (p - 1) div 2" by auto
  12.593 +        with q_g_2 have "q * j \<le> q * ((p - 1) div 2)"
  12.594            by (auto simp add: mult_le_cancel_left)
  12.595 -        with p_g_2 have "q * j div p \<le> q * ((p - 1) div 2) div p";
  12.596 +        with p_g_2 have "q * j div p \<le> q * ((p - 1) div 2) div p"
  12.597            by (auto simp add: zdiv_mono1)
  12.598 -        also from prems have "... \<le> (q - 1) div 2";
  12.599 +        also from prems have "... \<le> (q - 1) div 2"
  12.600            apply simp apply (insert aux2) by (simp add: QRTEMP_def)
  12.601          finally show "x \<le> (q - 1) div 2" by (insert prems, auto)
  12.602 -      qed;
  12.603 +      qed
  12.604      then show ?thesis by auto
  12.605 -  qed;
  12.606 -  also have "... = (q * j) div p";
  12.607 -  proof -;
  12.608 +  qed
  12.609 +  also have "... = (q * j) div p"
  12.610 +  proof -
  12.611      from j_fact P_set_def have "0 \<le> j" by auto
  12.612      with q_g_2 have "q * 0 \<le> q * j" by (auto simp only: mult_left_mono)
  12.613      then have "0 \<le> q * j" by auto
  12.614 -    then have "0 div p \<le> (q * j) div p";
  12.615 +    then have "0 div p \<le> (q * j) div p"
  12.616        apply (rule_tac a = 0 in zdiv_mono1)
  12.617        by (insert p_g_2, auto)
  12.618      also have "0 div p = 0" by auto
  12.619      finally show ?thesis by (auto simp add: card_bdd_int_set_l_le)
  12.620 -  qed;
  12.621 -  finally show "int (card (f1 j)) = q * j div p" .;
  12.622 -qed;
  12.623 +  qed
  12.624 +  finally show "int (card (f1 j)) = q * j div p" .
  12.625 +qed
  12.626  
  12.627 -lemma (in QRTEMP) aux3b: "\<forall>j \<in> Q_set. int (card (f2 j)) = (p * j) div q";
  12.628 -proof;
  12.629 -  fix j;
  12.630 -  assume j_fact: "j \<in> Q_set";
  12.631 -  have "int (card (f2 j)) = int (card {y. y \<in> P_set & y \<le> (p * j) div q})";
  12.632 -  proof -;
  12.633 -    have "finite (f2 j)";
  12.634 -    proof -;
  12.635 +lemma (in QRTEMP) aux3b: "\<forall>j \<in> Q_set. int (card (f2 j)) = (p * j) div q"
  12.636 +proof
  12.637 +  fix j
  12.638 +  assume j_fact: "j \<in> Q_set"
  12.639 +  have "int (card (f2 j)) = int (card {y. y \<in> P_set & y \<le> (p * j) div q})"
  12.640 +  proof -
  12.641 +    have "finite (f2 j)"
  12.642 +    proof -
  12.643        have "(f2 j) \<subseteq> S" by (auto simp add: f2_def)
  12.644        with S_finite show ?thesis by (auto simp add: finite_subset)
  12.645 -    qed;
  12.646 -    moreover have "inj_on (%(x,y). x) (f2 j)";
  12.647 +    qed
  12.648 +    moreover have "inj_on (%(x,y). x) (f2 j)"
  12.649        by (auto simp add: f2_def inj_on_def)
  12.650 -    ultimately have "card ((%(x,y). x) ` (f2 j)) = card  (f2 j)";
  12.651 +    ultimately have "card ((%(x,y). x) ` (f2 j)) = card  (f2 j)"
  12.652        by (auto simp add: f2_def card_image)
  12.653 -    moreover have "((%(x,y). x) ` (f2 j)) = {y. y \<in> P_set & y \<le> (p * j) div q}";
  12.654 +    moreover have "((%(x,y). x) ` (f2 j)) = {y. y \<in> P_set & y \<le> (p * j) div q}"
  12.655        by (insert prems, auto simp add: f2_def S_def Q_set_def 
  12.656          P_set_def image_def)
  12.657      ultimately show ?thesis by (auto simp add: f2_def)
  12.658 -  qed;
  12.659 -  also have "... = int (card {y. 0 < y & y \<le> (p * j) div q})";
  12.660 -  proof -;
  12.661 +  qed
  12.662 +  also have "... = int (card {y. 0 < y & y \<le> (p * j) div q})"
  12.663 +  proof -
  12.664      have "{y. y \<in> P_set & y \<le> (p * j) div q} = 
  12.665 -        {y. 0 < y & y \<le> (p * j) div q}";
  12.666 +        {y. 0 < y & y \<le> (p * j) div q}"
  12.667        apply (auto simp add: P_set_def)
  12.668 -      proof -;
  12.669 -        fix x;
  12.670 -        assume "0 < x" and "x \<le> p * j div q";
  12.671 -        with j_fact Q_set_def  have "j \<le> (q - 1) div 2"; by auto
  12.672 -        with p_g_2; have "p * j \<le> p * ((q - 1) div 2)";
  12.673 +      proof -
  12.674 +        fix x
  12.675 +        assume "0 < x" and "x \<le> p * j div q"
  12.676 +        with j_fact Q_set_def  have "j \<le> (q - 1) div 2" by auto
  12.677 +        with p_g_2 have "p * j \<le> p * ((q - 1) div 2)"
  12.678            by (auto simp add: mult_le_cancel_left)
  12.679 -        with q_g_2 have "p * j div q \<le> p * ((q - 1) div 2) div q";
  12.680 +        with q_g_2 have "p * j div q \<le> p * ((q - 1) div 2) div q"
  12.681            by (auto simp add: zdiv_mono1)
  12.682 -        also from prems have "... \<le> (p - 1) div 2";
  12.683 +        also from prems have "... \<le> (p - 1) div 2"
  12.684            by (auto simp add: aux2 QRTEMP_def)
  12.685          finally show "x \<le> (p - 1) div 2" by (insert prems, auto)
  12.686 -      qed;
  12.687 +      qed
  12.688      then show ?thesis by auto
  12.689 -  qed;
  12.690 -  also have "... = (p * j) div q";
  12.691 -  proof -;
  12.692 +  qed
  12.693 +  also have "... = (p * j) div q"
  12.694 +  proof -
  12.695      from j_fact Q_set_def have "0 \<le> j" by auto
  12.696      with p_g_2 have "p * 0 \<le> p * j" by (auto simp only: mult_left_mono)
  12.697      then have "0 \<le> p * j" by auto
  12.698 -    then have "0 div q \<le> (p * j) div q";
  12.699 +    then have "0 div q \<le> (p * j) div q"
  12.700        apply (rule_tac a = 0 in zdiv_mono1)
  12.701        by (insert q_g_2, auto)
  12.702      also have "0 div q = 0" by auto
  12.703      finally show ?thesis by (auto simp add: card_bdd_int_set_l_le)
  12.704 -  qed;
  12.705 -  finally show "int (card (f2 j)) = p * j div q" .;
  12.706 -qed;
  12.707 +  qed
  12.708 +  finally show "int (card (f2 j)) = p * j div q" .
  12.709 +qed
  12.710  
  12.711 -lemma (in QRTEMP) S1_card: "int (card(S1)) = setsum (%j. (q * j) div p) P_set";
  12.712 -proof -;
  12.713 -  have "\<forall>x \<in> P_set. finite (f1 x)";
  12.714 -  proof;
  12.715 -    fix x;
  12.716 +lemma (in QRTEMP) S1_card: "int (card(S1)) = setsum (%j. (q * j) div p) P_set"
  12.717 +proof -
  12.718 +  have "\<forall>x \<in> P_set. finite (f1 x)"
  12.719 +  proof
  12.720 +    fix x
  12.721      have "f1 x \<subseteq> S" by (auto simp add: f1_def)
  12.722      with S_finite show "finite (f1 x)" by (auto simp add: finite_subset)
  12.723 -  qed;
  12.724 -  moreover have "(\<forall>x \<in> P_set. \<forall>y \<in> P_set. x \<noteq> y --> (f1 x) \<inter> (f1 y) = {})";
  12.725 +  qed
  12.726 +  moreover have "(\<forall>x \<in> P_set. \<forall>y \<in> P_set. x \<noteq> y --> (f1 x) \<inter> (f1 y) = {})"
  12.727      by (auto simp add: f1_def)
  12.728 -  moreover note P_set_finite;
  12.729 +  moreover note P_set_finite
  12.730    ultimately have "int(card (UNION P_set f1)) = 
  12.731 -      setsum (%x. int(card (f1 x))) P_set";
  12.732 +      setsum (%x. int(card (f1 x))) P_set"
  12.733      by (rule_tac A = P_set in int_card_indexed_union_disjoint_sets, auto)
  12.734 -  moreover have "S1 = UNION P_set f1";
  12.735 +  moreover have "S1 = UNION P_set f1"
  12.736      by (auto simp add: f1_def S_def S1_def S2_def P_set_def Q_set_def aux1a)
  12.737    ultimately have "int(card (S1)) = setsum (%j. int(card (f1 j))) P_set" 
  12.738      by auto
  12.739 -  also have "... = setsum (%j. q * j div p) P_set";
  12.740 -  proof -;
  12.741 -    note aux3a
  12.742 -    with  P_set_finite show ?thesis by (rule setsum_same_function)
  12.743 -  qed;
  12.744 -  finally show ?thesis .;
  12.745 -qed;
  12.746 +  also have "... = setsum (%j. q * j div p) P_set"
  12.747 +    using aux3a by(fastsimp intro: setsum_cong)
  12.748 +  finally show ?thesis .
  12.749 +qed
  12.750  
  12.751 -lemma (in QRTEMP) S2_card: "int (card(S2)) = setsum (%j. (p * j) div q) Q_set";
  12.752 -proof -;
  12.753 -  have "\<forall>x \<in> Q_set. finite (f2 x)";
  12.754 -  proof;
  12.755 -    fix x;
  12.756 +lemma (in QRTEMP) S2_card: "int (card(S2)) = setsum (%j. (p * j) div q) Q_set"
  12.757 +proof -
  12.758 +  have "\<forall>x \<in> Q_set. finite (f2 x)"
  12.759 +  proof
  12.760 +    fix x
  12.761      have "f2 x \<subseteq> S" by (auto simp add: f2_def)
  12.762      with S_finite show "finite (f2 x)" by (auto simp add: finite_subset)
  12.763 -  qed;
  12.764 +  qed
  12.765    moreover have "(\<forall>x \<in> Q_set. \<forall>y \<in> Q_set. x \<noteq> y --> 
  12.766 -      (f2 x) \<inter> (f2 y) = {})";
  12.767 +      (f2 x) \<inter> (f2 y) = {})"
  12.768      by (auto simp add: f2_def)
  12.769 -  moreover note Q_set_finite;
  12.770 +  moreover note Q_set_finite
  12.771    ultimately have "int(card (UNION Q_set f2)) = 
  12.772 -      setsum (%x. int(card (f2 x))) Q_set";
  12.773 +      setsum (%x. int(card (f2 x))) Q_set"
  12.774      by (rule_tac A = Q_set in int_card_indexed_union_disjoint_sets, auto)
  12.775 -  moreover have "S2 = UNION Q_set f2";
  12.776 +  moreover have "S2 = UNION Q_set f2"
  12.777      by (auto simp add: f2_def S_def S1_def S2_def P_set_def Q_set_def aux1b)
  12.778    ultimately have "int(card (S2)) = setsum (%j. int(card (f2 j))) Q_set" 
  12.779      by auto
  12.780 -  also have "... = setsum (%j. p * j div q) Q_set";
  12.781 -  proof -;
  12.782 -    note aux3b;
  12.783 -    with Q_set_finite show ?thesis by (rule setsum_same_function)
  12.784 -  qed;
  12.785 -  finally show ?thesis .;
  12.786 -qed;
  12.787 +  also have "... = setsum (%j. p * j div q) Q_set"
  12.788 +    using aux3b by(fastsimp intro: setsum_cong)
  12.789 +  finally show ?thesis .
  12.790 +qed
  12.791  
  12.792  lemma (in QRTEMP) S1_carda: "int (card(S1)) = 
  12.793 -    setsum (%j. (j * q) div p) P_set";
  12.794 +    setsum (%j. (j * q) div p) P_set"
  12.795    by (auto simp add: S1_card zmult_ac)
  12.796  
  12.797  lemma (in QRTEMP) S2_carda: "int (card(S2)) = 
  12.798 -    setsum (%j. (j * p) div q) Q_set";
  12.799 +    setsum (%j. (j * p) div q) Q_set"
  12.800    by (auto simp add: S2_card zmult_ac)
  12.801  
  12.802  lemma (in QRTEMP) pq_sum_prop: "(setsum (%j. (j * p) div q) Q_set) + 
  12.803 -    (setsum (%j. (j * q) div p) P_set) = ((p - 1) div 2) * ((q - 1) div 2)";
  12.804 -proof -;
  12.805 +    (setsum (%j. (j * q) div p) P_set) = ((p - 1) div 2) * ((q - 1) div 2)"
  12.806 +proof -
  12.807    have "(setsum (%j. (j * p) div q) Q_set) + 
  12.808 -      (setsum (%j. (j * q) div p) P_set) = int (card S2) + int (card S1)";
  12.809 +      (setsum (%j. (j * q) div p) P_set) = int (card S2) + int (card S1)"
  12.810      by (auto simp add: S1_carda S2_carda)
  12.811 -  also have "... = int (card S1) + int (card S2)";
  12.812 +  also have "... = int (card S1) + int (card S2)"
  12.813      by auto
  12.814 -  also have "... = ((p - 1) div 2) * ((q - 1) div 2)";
  12.815 +  also have "... = ((p - 1) div 2) * ((q - 1) div 2)"
  12.816      by (auto simp add: card_sum_S1_S2)
  12.817 -  finally show ?thesis .;
  12.818 -qed;
  12.819 +  finally show ?thesis .
  12.820 +qed
  12.821  
  12.822 -lemma pq_prime_neq: "[| p \<in> zprime; q \<in> zprime; p \<noteq> q |] ==> (~[p = 0] (mod q))";
  12.823 +lemma pq_prime_neq: "[| p \<in> zprime; q \<in> zprime; p \<noteq> q |] ==> (~[p = 0] (mod q))"
  12.824    apply (auto simp add: zcong_eq_zdvd_prop zprime_def)
  12.825    apply (drule_tac x = q in allE)
  12.826    apply (drule_tac x = p in allE)
  12.827  by auto
  12.828  
  12.829  lemma (in QRTEMP) QR_short: "(Legendre p q) * (Legendre q p) = 
  12.830 -    (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))";
  12.831 -proof -;
  12.832 -  from prems have "~([p = 0] (mod q))";
  12.833 +    (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))"
  12.834 +proof -
  12.835 +  from prems have "~([p = 0] (mod q))"
  12.836      by (auto simp add: pq_prime_neq QRTEMP_def)
  12.837    with prems have a1: "(Legendre p q) = (-1::int) ^ 
  12.838 -      nat(setsum (%x. ((x * p) div q)) Q_set)";
  12.839 +      nat(setsum (%x. ((x * p) div q)) Q_set)"
  12.840      apply (rule_tac p = q in  MainQRLemma)
  12.841      by (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
  12.842 -  from prems have "~([q = 0] (mod p))";
  12.843 +  from prems have "~([q = 0] (mod p))"
  12.844      apply (rule_tac p = q and q = p in pq_prime_neq)
  12.845 -    apply (simp add: QRTEMP_def)+;
  12.846 +    apply (simp add: QRTEMP_def)+
  12.847      by arith
  12.848    with prems have a2: "(Legendre q p) = 
  12.849 -      (-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)";
  12.850 +      (-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)"
  12.851      apply (rule_tac p = p in  MainQRLemma)
  12.852      by (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
  12.853    from a1 a2 have "(Legendre p q) * (Legendre q p) = 
  12.854        (-1::int) ^ nat(setsum (%x. ((x * p) div q)) Q_set) *
  12.855 -        (-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)";
  12.856 +        (-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)"
  12.857      by auto
  12.858    also have "... = (-1::int) ^ (nat(setsum (%x. ((x * p) div q)) Q_set) + 
  12.859 -                   nat(setsum (%x. ((x * q) div p)) P_set))";
  12.860 +                   nat(setsum (%x. ((x * q) div p)) P_set))"
  12.861      by (auto simp add: zpower_zadd_distrib)
  12.862    also have "nat(setsum (%x. ((x * p) div q)) Q_set) + 
  12.863        nat(setsum (%x. ((x * q) div p)) P_set) =
  12.864          nat((setsum (%x. ((x * p) div q)) Q_set) + 
  12.865 -          (setsum (%x. ((x * q) div p)) P_set))";
  12.866 +          (setsum (%x. ((x * q) div p)) P_set))"
  12.867      apply (rule_tac z1 = "setsum (%x. ((x * p) div q)) Q_set" in 
  12.868 -      nat_add_distrib [THEN sym]);
  12.869 +      nat_add_distrib [THEN sym])
  12.870      by (auto simp add: S1_carda [THEN sym] S2_carda [THEN sym])
  12.871 -  also have "... = nat(((p - 1) div 2) * ((q - 1) div 2))";
  12.872 +  also have "... = nat(((p - 1) div 2) * ((q - 1) div 2))"
  12.873      by (auto simp add: pq_sum_prop)
  12.874 -  finally show ?thesis .;
  12.875 -qed;
  12.876 +  finally show ?thesis .
  12.877 +qed
  12.878  
  12.879  theorem Quadratic_Reciprocity:
  12.880       "[| p \<in> zOdd; p \<in> zprime; q \<in> zOdd; q \<in> zprime; 
  12.881           p \<noteq> q |] 
  12.882        ==> (Legendre p q) * (Legendre q p) = 
  12.883 -          (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))";
  12.884 +          (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))"
  12.885    by (auto simp add: QRTEMP.QR_short zprime_zOdd_eq_grt_2 [THEN sym] 
  12.886                       QRTEMP_def)
  12.887  
    13.1 --- a/src/HOL/NumberTheory/Residues.thy	Thu Dec 09 16:45:46 2004 +0100
    13.2 +++ b/src/HOL/NumberTheory/Residues.thy	Thu Dec 09 18:30:59 2004 +0100
    13.3 @@ -168,7 +168,7 @@
    13.4    by (auto simp add: zcong_zmod)
    13.5  
    13.6  lemma StandardRes_prod: "[| finite X; 0 < m |] 
    13.7 -     ==> [gsetprod f X = gsetprod (StandardRes m o f) X] (mod m)";
    13.8 +     ==> [setprod f X = setprod (StandardRes m o f) X] (mod m)";
    13.9    apply (rule_tac F = X in finite_induct)
   13.10  by (auto intro!: zcong_zmult simp add: StandardRes_prop1)
   13.11  
    14.1 --- a/src/HOL/NumberTheory/WilsonBij.thy	Thu Dec 09 16:45:46 2004 +0100
    14.2 +++ b/src/HOL/NumberTheory/WilsonBij.thy	Thu Dec 09 18:30:59 2004 +0100
    14.3 @@ -229,7 +229,7 @@
    14.4  subsection {* Wilson *}
    14.5  
    14.6  lemma bijER_zcong_prod_1:
    14.7 -    "p \<in> zprime ==> A \<in> bijER (reciR p) ==> [setprod A = 1] (mod p)"
    14.8 +    "p \<in> zprime ==> A \<in> bijER (reciR p) ==> [\<Prod>A = 1] (mod p)"
    14.9    apply (unfold reciR_def)
   14.10    apply (erule bijER.induct)
   14.11      apply (subgoal_tac [2] "a = 1 \<or> a = p - 1")
   14.12 @@ -239,7 +239,7 @@
   14.13      prefer 3
   14.14      apply (subst setprod_insert)
   14.15        apply (auto simp add: fin_bijER)
   14.16 -  apply (subgoal_tac "zcong ((a * b) * setprod A) (1 * 1) p")
   14.17 +  apply (subgoal_tac "zcong ((a * b) * \<Prod>A) (1 * 1) p")
   14.18     apply (simp add: zmult_assoc)
   14.19    apply (rule zcong_zmult)
   14.20     apply auto
    15.1 --- a/src/HOL/NumberTheory/WilsonRuss.thy	Thu Dec 09 16:45:46 2004 +0100
    15.2 +++ b/src/HOL/NumberTheory/WilsonRuss.thy	Thu Dec 09 18:30:59 2004 +0100
    15.3 @@ -261,7 +261,7 @@
    15.4  
    15.5  lemma wset_zcong_prod_1 [rule_format]:
    15.6    "p \<in> zprime -->
    15.7 -    5 \<le> p --> a < p - 1 --> [setprod (wset (a, p)) = 1] (mod p)"
    15.8 +    5 \<le> p --> a < p - 1 --> [(\<Prod>x\<in>wset(a, p). x) = 1] (mod p)"
    15.9    apply (induct a p rule: wset_induct)
   15.10     prefer 2
   15.11     apply (subst wset.simps)
   15.12 @@ -269,7 +269,7 @@
   15.13    apply (subst setprod_insert)
   15.14      apply (tactic {* stac (thm "setprod_insert") 3 *})
   15.15        apply (subgoal_tac [5]
   15.16 -	"zcong (a * inv p a * setprod (wset (a - 1, p))) (1 * 1) p")
   15.17 +	"zcong (a * inv p a * (\<Prod>x\<in> wset(a - 1, p). x)) (1 * 1) p")
   15.18         prefer 5
   15.19         apply (simp add: zmult_assoc)
   15.20        apply (rule_tac [5] zcong_zmult)