summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Wed, 24 Nov 2004 11:13:00 +0100 | |

changeset 15328 | 35951e6a7855 |

parent 15327 | 0230a10582d3 |

child 15329 | bd94b0a71dd2 |

mod because of change in finite set induction

--- a/src/HOL/Algebra/CRing.thy Wed Nov 24 11:12:10 2004 +0100 +++ b/src/HOL/Algebra/CRing.thy Wed Nov 24 11:13:00 2004 +0100 @@ -476,7 +476,7 @@ proof (induct set: Finites) case empty then show ?case by simp next - case (insert F x) then show ?case by (simp add: Pi_def l_distr) + case (insert x F) then show ?case by (simp add: Pi_def l_distr) qed lemma (in cring) finsum_rdistr: @@ -485,7 +485,7 @@ proof (induct set: Finites) case empty then show ?case by simp next - case (insert F x) then show ?case by (simp add: Pi_def r_distr) + case (insert x F) then show ?case by (simp add: Pi_def r_distr) qed subsection {* Facts of Integral Domains *}

--- a/src/HOL/Algebra/FiniteProduct.thy Wed Nov 24 11:12:10 2004 +0100 +++ b/src/HOL/Algebra/FiniteProduct.thy Wed Nov 24 11:13:00 2004 +0100 @@ -50,7 +50,7 @@ proof (induct set: Finites) case empty then show ?case by auto next - case (insert F x) + case (insert x F) then obtain y where y: "(F, y) \<in> foldSetD D f e" by auto with insert have "y \<in> D" by (auto dest: foldSetD_closed) with y and insert have "(insert x F, f x y) \<in> foldSetD D f e" @@ -90,7 +90,7 @@ proof (induct set: Finites) case empty then show ?case by auto next - case (insert F x) + case (insert x F) then obtain y where y: "(F, y) \<in> foldSetD D f e" by auto with insert have "y \<in> D" by auto with y and insert have "(insert x F, f x y) \<in> foldSetD D f e" @@ -339,7 +339,7 @@ proof (induct set: Finites) case empty show ?case by simp next - case (insert A a) + case (insert a A) have "(%i. \<one>) \<in> A -> carrier G" by auto with insert show ?case by simp qed @@ -352,7 +352,7 @@ proof induct case empty show ?case by simp next - case (insert A a) + case (insert a A) then have a: "f a \<in> carrier G" by fast from insert have A: "f \<in> A -> carrier G" by fast from insert A a show ?case by simp @@ -374,7 +374,7 @@ proof (induct set: Finites) case empty then show ?case by (simp add: finprod_closed) next - case (insert A a) + case (insert a A) then have a: "g a \<in> carrier G" by fast from insert have A: "g \<in> A -> carrier G" by fast from insert A a show ?case @@ -396,7 +396,7 @@ proof (induct set: Finites) case empty show ?case by simp next - case (insert A a) then + case (insert a A) then have fA: "f \<in> A -> carrier G" by fast from insert have fa: "f a \<in> carrier G" by fast from insert have gA: "g \<in> A -> carrier G" by fast @@ -421,7 +421,7 @@ proof induct case empty thus ?case by simp next - case (insert B x) + case (insert x B) then have "finprod G f A = finprod G f (insert x B)" by simp also from insert have "... = f x \<otimes> finprod G f B" proof (intro finprod_insert)

--- a/src/HOL/Algebra/Lattice.thy Wed Nov 24 11:12:10 2004 +0100 +++ b/src/HOL/Algebra/Lattice.thy Wed Nov 24 11:13:00 2004 +0100 @@ -320,7 +320,7 @@ case empty then show ?case by simp next - case (insert A x) + case (insert x A) show ?case proof (cases "A = {}") case True @@ -350,7 +350,7 @@ proof (induct set: Finites) case empty then show ?case by simp next - case (insert A x) then show ?case + case insert then show ?case by - (rule finite_sup_insertI, simp_all) qed @@ -546,7 +546,7 @@ proof (induct set: Finites) case empty then show ?case by simp next - case (insert A x) + case (insert x A) show ?case proof (cases "A = {}") case True @@ -577,7 +577,7 @@ proof (induct set: Finites) case empty then show ?case by simp next - case (insert A x) then show ?case + case insert then show ?case by (rule_tac finite_inf_insertI) (simp_all) qed