mod because of change in finite set induction
authornipkow
Wed Nov 24 11:13:00 2004 +0100 (2004-11-24)
changeset 1532835951e6a7855
parent 15327 0230a10582d3
child 15329 bd94b0a71dd2
mod because of change in finite set induction
src/HOL/Algebra/CRing.thy
src/HOL/Algebra/FiniteProduct.thy
src/HOL/Algebra/Lattice.thy
     1.1 --- a/src/HOL/Algebra/CRing.thy	Wed Nov 24 11:12:10 2004 +0100
     1.2 +++ b/src/HOL/Algebra/CRing.thy	Wed Nov 24 11:13:00 2004 +0100
     1.3 @@ -476,7 +476,7 @@
     1.4  proof (induct set: Finites)
     1.5    case empty then show ?case by simp
     1.6  next
     1.7 -  case (insert F x) then show ?case by (simp add: Pi_def l_distr)
     1.8 +  case (insert x F) then show ?case by (simp add: Pi_def l_distr)
     1.9  qed
    1.10  
    1.11  lemma (in cring) finsum_rdistr:
    1.12 @@ -485,7 +485,7 @@
    1.13  proof (induct set: Finites)
    1.14    case empty then show ?case by simp
    1.15  next
    1.16 -  case (insert F x) then show ?case by (simp add: Pi_def r_distr)
    1.17 +  case (insert x F) then show ?case by (simp add: Pi_def r_distr)
    1.18  qed
    1.19  
    1.20  subsection {* Facts of Integral Domains *}
     2.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Wed Nov 24 11:12:10 2004 +0100
     2.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Wed Nov 24 11:13:00 2004 +0100
     2.3 @@ -50,7 +50,7 @@
     2.4  proof (induct set: Finites)
     2.5    case empty then show ?case by auto
     2.6  next
     2.7 -  case (insert F x)
     2.8 +  case (insert x F)
     2.9    then obtain y where y: "(F, y) \<in> foldSetD D f e" by auto
    2.10    with insert have "y \<in> D" by (auto dest: foldSetD_closed)
    2.11    with y and insert have "(insert x F, f x y) \<in> foldSetD D f e"
    2.12 @@ -90,7 +90,7 @@
    2.13  proof (induct set: Finites)
    2.14    case empty then show ?case by auto
    2.15  next
    2.16 -  case (insert F x)
    2.17 +  case (insert x F)
    2.18    then obtain y where y: "(F, y) \<in> foldSetD D f e" by auto
    2.19    with insert have "y \<in> D" by auto
    2.20    with y and insert have "(insert x F, f x y) \<in> foldSetD D f e"
    2.21 @@ -339,7 +339,7 @@
    2.22  proof (induct set: Finites)
    2.23    case empty show ?case by simp
    2.24  next
    2.25 -  case (insert A a)
    2.26 +  case (insert a A)
    2.27    have "(%i. \<one>) \<in> A -> carrier G" by auto
    2.28    with insert show ?case by simp
    2.29  qed
    2.30 @@ -352,7 +352,7 @@
    2.31  proof induct
    2.32    case empty show ?case by simp
    2.33  next
    2.34 -  case (insert A a)
    2.35 +  case (insert a A)
    2.36    then have a: "f a \<in> carrier G" by fast
    2.37    from insert have A: "f \<in> A -> carrier G" by fast
    2.38    from insert A a show ?case by simp
    2.39 @@ -374,7 +374,7 @@
    2.40  proof (induct set: Finites)
    2.41    case empty then show ?case by (simp add: finprod_closed)
    2.42  next
    2.43 -  case (insert A a)
    2.44 +  case (insert a A)
    2.45    then have a: "g a \<in> carrier G" by fast
    2.46    from insert have A: "g \<in> A -> carrier G" by fast
    2.47    from insert A a show ?case
    2.48 @@ -396,7 +396,7 @@
    2.49  proof (induct set: Finites)
    2.50    case empty show ?case by simp
    2.51  next
    2.52 -  case (insert A a) then
    2.53 +  case (insert a A) then
    2.54    have fA: "f \<in> A -> carrier G" by fast
    2.55    from insert have fa: "f a \<in> carrier G" by fast
    2.56    from insert have gA: "g \<in> A -> carrier G" by fast
    2.57 @@ -421,7 +421,7 @@
    2.58      proof induct
    2.59        case empty thus ?case by simp
    2.60      next
    2.61 -      case (insert B x)
    2.62 +      case (insert x B)
    2.63        then have "finprod G f A = finprod G f (insert x B)" by simp
    2.64        also from insert have "... = f x \<otimes> finprod G f B"
    2.65        proof (intro finprod_insert)
     3.1 --- a/src/HOL/Algebra/Lattice.thy	Wed Nov 24 11:12:10 2004 +0100
     3.2 +++ b/src/HOL/Algebra/Lattice.thy	Wed Nov 24 11:13:00 2004 +0100
     3.3 @@ -320,7 +320,7 @@
     3.4    case empty
     3.5    then show ?case by simp
     3.6  next
     3.7 -  case (insert A x)
     3.8 +  case (insert x A)
     3.9    show ?case
    3.10    proof (cases "A = {}")
    3.11      case True
    3.12 @@ -350,7 +350,7 @@
    3.13  proof (induct set: Finites)
    3.14    case empty then show ?case by simp
    3.15  next
    3.16 -  case (insert A x) then show ?case
    3.17 +  case insert then show ?case
    3.18      by - (rule finite_sup_insertI, simp_all)
    3.19  qed
    3.20  
    3.21 @@ -546,7 +546,7 @@
    3.22  proof (induct set: Finites)
    3.23    case empty then show ?case by simp
    3.24  next
    3.25 -  case (insert A x)
    3.26 +  case (insert x A)
    3.27    show ?case
    3.28    proof (cases "A = {}")
    3.29      case True
    3.30 @@ -577,7 +577,7 @@
    3.31  proof (induct set: Finites)
    3.32    case empty then show ?case by simp
    3.33  next
    3.34 -  case (insert A x) then show ?case
    3.35 +  case insert then show ?case
    3.36      by (rule_tac finite_inf_insertI) (simp_all)
    3.37  qed
    3.38