src/HOL/Algebra/FiniteProduct.thy
changeset 46721 f88b187ad8ca
parent 44890 22f665a2e91c
child 56142 8bb21318e10b
     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Mon Feb 27 20:55:30 2012 +0100
     1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Mon Feb 27 21:07:00 2012 +0100
     1.3 @@ -190,7 +190,7 @@
     1.4  lemma (in LCD) foldD_closed [simp]:
     1.5    "[| finite A; e \<in> D; A \<subseteq> B |] ==> foldD D f e A \<in> D"
     1.6  proof (induct set: finite)
     1.7 -  case empty then show ?case by (simp add: foldD_empty)
     1.8 +  case empty then show ?case by simp
     1.9  next
    1.10    case insert then show ?case by (simp add: foldD_insert)
    1.11  qed
    1.12 @@ -328,7 +328,7 @@
    1.13             apply fast
    1.14            apply fast
    1.15           apply assumption
    1.16 -        apply (fastforce intro: m_closed)
    1.17 +        apply fastforce
    1.18         apply simp+
    1.19     apply fast
    1.20    apply (auto simp add: finprod_def)
    1.21 @@ -372,14 +372,13 @@
    1.22       finprod G g A \<otimes> finprod G g B"
    1.23  -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
    1.24  proof (induct set: finite)
    1.25 -  case empty then show ?case by (simp add: finprod_closed)
    1.26 +  case empty then show ?case by simp
    1.27  next
    1.28    case (insert a A)
    1.29    then have a: "g a \<in> carrier G" by fast
    1.30    from insert have A: "g \<in> A -> carrier G" by fast
    1.31    from insert A a show ?case
    1.32 -    by (simp add: m_ac Int_insert_left insert_absorb finprod_closed
    1.33 -          Int_mono2) 
    1.34 +    by (simp add: m_ac Int_insert_left insert_absorb Int_mono2) 
    1.35  qed
    1.36  
    1.37  lemma finprod_Un_disjoint:
    1.38 @@ -387,7 +386,7 @@
    1.39        g \<in> A -> carrier G; g \<in> B -> carrier G |]
    1.40     ==> finprod G g (A Un B) = finprod G g A \<otimes> finprod G g B"
    1.41    apply (subst finprod_Un_Int [symmetric])
    1.42 -      apply (auto simp add: finprod_closed)
    1.43 +      apply auto
    1.44    done
    1.45  
    1.46  lemma finprod_multf:
    1.47 @@ -498,9 +497,8 @@
    1.48    assumes fin: "finite A"
    1.49      shows "f : (h ` A) \<rightarrow> carrier G \<Longrightarrow> 
    1.50          inj_on h A ==> finprod G f (h ` A) = finprod G (%x. f (h x)) A"
    1.51 -  using fin apply induct
    1.52 -  apply (auto simp add: finprod_insert Pi_def)
    1.53 -done
    1.54 +  using fin
    1.55 +  by induct (auto simp add: Pi_def)
    1.56  
    1.57  lemma finprod_const:
    1.58    assumes fin [simp]: "finite A"
    1.59 @@ -512,7 +510,7 @@
    1.60    apply auto
    1.61    apply (subst m_comm)
    1.62    apply auto
    1.63 -done
    1.64 +  done
    1.65  
    1.66  (* The following lemma was contributed by Jesus Aransay. *)
    1.67