tuned proofs;
authorwenzelm
Mon Feb 27 21:07:00 2012 +0100 (2012-02-27)
changeset 46721f88b187ad8ca
parent 46720 9722171731af
child 46722 d0491ab69c84
tuned proofs;
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/FiniteProduct.thy
src/HOL/Algebra/Ring.thy
     1.1 --- a/src/HOL/Algebra/Coset.thy	Mon Feb 27 20:55:30 2012 +0100
     1.2 +++ b/src/HOL/Algebra/Coset.thy	Mon Feb 27 21:07:00 2012 +0100
     1.3 @@ -232,7 +232,7 @@
     1.4    also from carr
     1.5        have "\<dots> = x' \<otimes> ((inv x) \<otimes> x)" by (simp add: m_assoc)
     1.6    also from carr
     1.7 -      have "\<dots> = x' \<otimes> \<one>" by (simp add: l_inv)
     1.8 +      have "\<dots> = x' \<otimes> \<one>" by simp
     1.9    also from carr
    1.10        have "\<dots> = x'" by simp
    1.11    finally
    1.12 @@ -520,8 +520,7 @@
    1.13  apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def image_def)
    1.14  apply (rule_tac x = x in bexI)
    1.15  apply (rule bexI [of _ "\<one>"])
    1.16 -apply (auto simp add: subgroup.m_closed subgroup.one_closed
    1.17 -                      r_one subgroup.subset [THEN subsetD])
    1.18 +apply (auto simp add: subgroup.one_closed subgroup.subset [THEN subsetD])
    1.19  done
    1.20  
    1.21  
    1.22 @@ -612,7 +611,7 @@
    1.23        fix x y
    1.24        assume [simp]: "x \<in> carrier G" "y \<in> carrier G" 
    1.25           and "inv x \<otimes> y \<in> H"
    1.26 -      hence "inv (inv x \<otimes> y) \<in> H" by (simp add: m_inv_closed) 
    1.27 +      hence "inv (inv x \<otimes> y) \<in> H" by simp
    1.28        thus "inv y \<otimes> x \<in> H" by (simp add: inv_mult_group)
    1.29      qed
    1.30    next
    1.31 @@ -722,7 +721,7 @@
    1.32    assume abrcong: "(a, b) \<in> rcong H"
    1.33      and ccarr: "c \<in> carrier G"
    1.34  
    1.35 -  from ccarr have "c \<in> Units G" by (simp add: Units_eq)
    1.36 +  from ccarr have "c \<in> Units G" by simp
    1.37    hence cinvc_one: "inv c \<otimes> c = \<one>" by (rule Units_l_inv)
    1.38  
    1.39    from abrcong
     2.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Mon Feb 27 20:55:30 2012 +0100
     2.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Mon Feb 27 21:07:00 2012 +0100
     2.3 @@ -190,7 +190,7 @@
     2.4  lemma (in LCD) foldD_closed [simp]:
     2.5    "[| finite A; e \<in> D; A \<subseteq> B |] ==> foldD D f e A \<in> D"
     2.6  proof (induct set: finite)
     2.7 -  case empty then show ?case by (simp add: foldD_empty)
     2.8 +  case empty then show ?case by simp
     2.9  next
    2.10    case insert then show ?case by (simp add: foldD_insert)
    2.11  qed
    2.12 @@ -328,7 +328,7 @@
    2.13             apply fast
    2.14            apply fast
    2.15           apply assumption
    2.16 -        apply (fastforce intro: m_closed)
    2.17 +        apply fastforce
    2.18         apply simp+
    2.19     apply fast
    2.20    apply (auto simp add: finprod_def)
    2.21 @@ -372,14 +372,13 @@
    2.22       finprod G g A \<otimes> finprod G g B"
    2.23  -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
    2.24  proof (induct set: finite)
    2.25 -  case empty then show ?case by (simp add: finprod_closed)
    2.26 +  case empty then show ?case by simp
    2.27  next
    2.28    case (insert a A)
    2.29    then have a: "g a \<in> carrier G" by fast
    2.30    from insert have A: "g \<in> A -> carrier G" by fast
    2.31    from insert A a show ?case
    2.32 -    by (simp add: m_ac Int_insert_left insert_absorb finprod_closed
    2.33 -          Int_mono2) 
    2.34 +    by (simp add: m_ac Int_insert_left insert_absorb Int_mono2) 
    2.35  qed
    2.36  
    2.37  lemma finprod_Un_disjoint:
    2.38 @@ -387,7 +386,7 @@
    2.39        g \<in> A -> carrier G; g \<in> B -> carrier G |]
    2.40     ==> finprod G g (A Un B) = finprod G g A \<otimes> finprod G g B"
    2.41    apply (subst finprod_Un_Int [symmetric])
    2.42 -      apply (auto simp add: finprod_closed)
    2.43 +      apply auto
    2.44    done
    2.45  
    2.46  lemma finprod_multf:
    2.47 @@ -498,9 +497,8 @@
    2.48    assumes fin: "finite A"
    2.49      shows "f : (h ` A) \<rightarrow> carrier G \<Longrightarrow> 
    2.50          inj_on h A ==> finprod G f (h ` A) = finprod G (%x. f (h x)) A"
    2.51 -  using fin apply induct
    2.52 -  apply (auto simp add: finprod_insert Pi_def)
    2.53 -done
    2.54 +  using fin
    2.55 +  by induct (auto simp add: Pi_def)
    2.56  
    2.57  lemma finprod_const:
    2.58    assumes fin [simp]: "finite A"
    2.59 @@ -512,7 +510,7 @@
    2.60    apply auto
    2.61    apply (subst m_comm)
    2.62    apply auto
    2.63 -done
    2.64 +  done
    2.65  
    2.66  (* The following lemma was contributed by Jesus Aransay. *)
    2.67  
     3.1 --- a/src/HOL/Algebra/Ring.thy	Mon Feb 27 20:55:30 2012 +0100
     3.2 +++ b/src/HOL/Algebra/Ring.thy	Mon Feb 27 21:07:00 2012 +0100
     3.3 @@ -259,16 +259,12 @@
     3.4  
     3.5  context ring begin
     3.6  
     3.7 -lemma is_abelian_group:
     3.8 -  "abelian_group R"
     3.9 -  ..
    3.10 +lemma is_abelian_group: "abelian_group R" ..
    3.11  
    3.12 -lemma is_monoid:
    3.13 -  "monoid R"
    3.14 +lemma is_monoid: "monoid R"
    3.15    by (auto intro!: monoidI m_assoc)
    3.16  
    3.17 -lemma is_ring:
    3.18 -  "ring R"
    3.19 +lemma is_ring: "ring R"
    3.20    by (rule ring_axioms)
    3.21  
    3.22  end
    3.23 @@ -444,12 +440,13 @@
    3.24        show "\<one> = \<zero>" by simp
    3.25  qed
    3.26  
    3.27 -lemma carrier_one_zero:
    3.28 -  shows "(carrier R = {\<zero>}) = (\<one> = \<zero>)"
    3.29 -  by (rule, erule one_zeroI, erule one_zeroD)
    3.30 +lemma carrier_one_zero: "(carrier R = {\<zero>}) = (\<one> = \<zero>)"
    3.31 +  apply rule
    3.32 +   apply (erule one_zeroI)
    3.33 +  apply (erule one_zeroD)
    3.34 +  done
    3.35  
    3.36 -lemma carrier_one_not_zero:
    3.37 -  shows "(carrier R \<noteq> {\<zero>}) = (\<one> \<noteq> \<zero>)"
    3.38 +lemma carrier_one_not_zero: "(carrier R \<noteq> {\<zero>}) = (\<one> \<noteq> \<zero>)"
    3.39    by (simp add: carrier_one_zero)
    3.40  
    3.41  end
    3.42 @@ -571,7 +568,7 @@
    3.43      from bcarr
    3.44      have "b = \<one> \<otimes> b" by algebra
    3.45      also from aUnit acarr
    3.46 -    have "... = (inv a \<otimes> a) \<otimes> b" by (simp add: Units_l_inv)
    3.47 +    have "... = (inv a \<otimes> a) \<otimes> b" by simp
    3.48      also from acarr bcarr aUnit[THEN Units_inv_closed]
    3.49      have "... = (inv a) \<otimes> (a \<otimes> b)" by algebra
    3.50      also from ab and acarr bcarr aUnit