author wenzelm Fri Sep 02 18:17:45 2011 +0200 (2011-09-02 ago) changeset 44655 fe0365331566 parent 44654 d80fe56788a5 child 44657 17dbd9d9db38 child 44663 3bc39cfe27fe
tuned proofs;
 src/HOL/Algebra/AbelCoset.thy file | annotate | diff | revisions src/HOL/Algebra/Divisibility.thy file | annotate | diff | revisions src/HOL/Algebra/Group.thy file | annotate | diff | revisions src/HOL/Algebra/IntRing.thy file | annotate | diff | revisions src/HOL/Algebra/Lattice.thy file | annotate | diff | revisions src/HOL/Algebra/RingHom.thy file | annotate | diff | revisions src/HOL/Algebra/UnivPoly.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Algebra/AbelCoset.thy	Fri Sep 02 17:58:32 2011 +0200
1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Fri Sep 02 18:17:45 2011 +0200
1.3 @@ -233,10 +233,10 @@
1.4    shows "abelian_subgroup H G"
1.5  proof -
1.6    interpret normal "H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
1.7 -  by (rule a_normal)
1.8 +    by (rule a_normal)
1.9
1.10    show "abelian_subgroup H G"
1.11 -  proof qed (simp add: a_comm)
1.12 +    by default (simp add: a_comm)
1.13  qed
1.14
1.15  lemma abelian_subgroupI2:
```
```     2.1 --- a/src/HOL/Algebra/Divisibility.thy	Fri Sep 02 17:58:32 2011 +0200
2.2 +++ b/src/HOL/Algebra/Divisibility.thy	Fri Sep 02 18:17:45 2011 +0200
2.3 @@ -25,14 +25,14 @@
2.4        and r_cancel:
2.5            "\<And>a b c. \<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"
2.6    shows "monoid_cancel G"
2.7 -  proof qed fact+
2.8 +    by default fact+
2.9
2.10  lemma (in monoid_cancel) is_monoid_cancel:
2.11    "monoid_cancel G"
2.12    ..
2.13
2.14  sublocale group \<subseteq> monoid_cancel
2.15 -  proof qed simp+
2.16 +  by default simp_all
2.17
2.18
2.19  locale comm_monoid_cancel = monoid_cancel + comm_monoid
2.20 @@ -3655,7 +3655,7 @@
2.21  done
2.22
2.23  sublocale factorial_monoid \<subseteq> primeness_condition_monoid
2.24 -  proof qed (rule irreducible_is_prime)
2.25 +  by default (rule irreducible_is_prime)
2.26
2.27
2.28  lemma (in factorial_monoid) primeness_condition:
2.29 @@ -3664,10 +3664,10 @@
2.30
2.31  lemma (in factorial_monoid) gcd_condition [simp]:
2.32    shows "gcd_condition_monoid G"
2.33 -  proof qed (rule gcdof_exists)
2.34 +  by default (rule gcdof_exists)
2.35
2.36  sublocale factorial_monoid \<subseteq> gcd_condition_monoid
2.37 -  proof qed (rule gcdof_exists)
2.38 +  by default (rule gcdof_exists)
2.39
2.40  lemma (in factorial_monoid) division_weak_lattice [simp]:
2.41    shows "weak_lattice (division_rel G)"
```
```     3.1 --- a/src/HOL/Algebra/Group.thy	Fri Sep 02 17:58:32 2011 +0200
3.2 +++ b/src/HOL/Algebra/Group.thy	Fri Sep 02 18:17:45 2011 +0200
3.3 @@ -286,7 +286,7 @@
3.4    qed
3.5    then have carrier_subset_Units: "carrier G <= Units G"
3.6      by (unfold Units_def) fast
3.7 -  show ?thesis proof qed (auto simp: r_one m_assoc carrier_subset_Units)
3.8 +  show ?thesis by default (auto simp: r_one m_assoc carrier_subset_Units)
3.9  qed
3.10
3.11  lemma (in monoid) group_l_invI:
3.12 @@ -694,7 +694,7 @@
3.13    assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
3.14        x \<otimes> y = y \<otimes> x"
3.15    shows "comm_group G"
3.16 -  proof qed (simp_all add: m_comm)
3.17 +  by default (simp_all add: m_comm)
3.18
3.19  lemma comm_groupI:
3.20    fixes G (structure)
3.21 @@ -722,7 +722,7 @@
3.22
3.23  theorem (in group) subgroups_partial_order:
3.24    "partial_order (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)"
3.25 -  proof qed simp_all
3.26 +  by default simp_all
3.27
3.28  lemma (in group) subgroup_self:
3.29    "subgroup (carrier G) G"
```
```     4.1 --- a/src/HOL/Algebra/IntRing.thy	Fri Sep 02 17:58:32 2011 +0200
4.2 +++ b/src/HOL/Algebra/IntRing.thy	Fri Sep 02 18:17:45 2011 +0200
4.3 @@ -62,7 +62,7 @@
4.4      and "pow \<Z> x n = x^n"
4.5  proof -
4.6    -- "Specification"
4.7 -  show "monoid \<Z>" proof qed auto
4.8 +  show "monoid \<Z>" by default auto
4.9    then interpret int: monoid \<Z> .
4.10
4.11    -- "Carrier"
4.12 @@ -79,7 +79,7 @@
4.13    where "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
4.14  proof -
4.15    -- "Specification"
4.16 -  show "comm_monoid \<Z>" proof qed auto
4.17 +  show "comm_monoid \<Z>" by default auto
4.18    then interpret int: comm_monoid \<Z> .
4.19
4.20    -- "Operations"
4.21 @@ -105,7 +105,7 @@
4.22      and int_finsum_eq: "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
4.23  proof -
4.24    -- "Specification"
4.25 -  show "abelian_monoid \<Z>" proof qed auto
4.26 +  show "abelian_monoid \<Z>" by default auto
4.27    then interpret int: abelian_monoid \<Z> .
4.28
4.29    -- "Carrier"
4.30 @@ -189,7 +189,7 @@
4.31      and "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
4.32  proof -
4.33    show "partial_order (| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
4.34 -    proof qed simp_all
4.35 +    by default simp_all
4.36    show "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
4.37      by simp
4.38    show "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
4.39 @@ -226,7 +226,7 @@
4.40
4.41  interpretation int (* [unfolded UNIV] *) :
4.42    total_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
4.43 -  proof qed clarsimp
4.44 +  by default clarsimp
4.45
4.46
4.47  subsection {* Generated Ideals of @{text "\<Z>"} *}
```
```     5.1 --- a/src/HOL/Algebra/Lattice.thy	Fri Sep 02 17:58:32 2011 +0200
5.2 +++ b/src/HOL/Algebra/Lattice.thy	Fri Sep 02 18:17:45 2011 +0200
5.3 @@ -921,7 +921,7 @@
5.4  lemma (in weak_partial_order) weak_total_orderI:
5.5    assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
5.6    shows "weak_total_order L"
5.7 -  proof qed (rule total)
5.8 +  by default (rule total)
5.9
5.10  text {* Total orders are lattices. *}
5.11
5.12 @@ -985,7 +985,7 @@
5.13      and inf_exists:
5.14      "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
5.15    shows "weak_complete_lattice L"
5.16 -  proof qed (auto intro: sup_exists inf_exists)
5.17 +  by default (auto intro: sup_exists inf_exists)
5.18
5.19  definition
5.20    top :: "_ => 'a" ("\<top>\<index>")
5.21 @@ -1133,14 +1133,14 @@
5.22      "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
5.23
5.24  sublocale upper_semilattice < weak: weak_upper_semilattice
5.25 -  proof qed (rule sup_of_two_exists)
5.26 +  by default (rule sup_of_two_exists)
5.27
5.28  locale lower_semilattice = partial_order +
5.29    assumes inf_of_two_exists:
5.30      "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
5.31
5.32  sublocale lower_semilattice < weak: weak_lower_semilattice
5.33 -  proof qed (rule inf_of_two_exists)
5.34 +  by default (rule inf_of_two_exists)
5.35
5.36  locale lattice = upper_semilattice + lower_semilattice
5.37
5.38 @@ -1191,19 +1191,19 @@
5.39    assumes total_order_total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
5.40
5.41  sublocale total_order < weak: weak_total_order
5.42 -  proof qed (rule total_order_total)
5.43 +  by default (rule total_order_total)
5.44
5.45  text {* Introduction rule: the usual definition of total order *}
5.46
5.47  lemma (in partial_order) total_orderI:
5.48    assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
5.49    shows "total_order L"
5.50 -  proof qed (rule total)
5.51 +  by default (rule total)
5.52
5.53  text {* Total orders are lattices. *}
5.54
5.55  sublocale total_order < weak: lattice
5.56 -  proof qed (auto intro: sup_of_two_exists inf_of_two_exists)
5.57 +  by default (auto intro: sup_of_two_exists inf_of_two_exists)
5.58
5.59
5.60  text {* Complete lattices *}
5.61 @@ -1215,7 +1215,7 @@
5.62      "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
5.63
5.64  sublocale complete_lattice < weak: weak_complete_lattice
5.65 -  proof qed (auto intro: sup_exists inf_exists)
5.66 +  by default (auto intro: sup_exists inf_exists)
5.67
5.68  text {* Introduction rule: the usual definition of complete lattice *}
5.69
5.70 @@ -1225,7 +1225,7 @@
5.71      and inf_exists:
5.72      "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
5.73    shows "complete_lattice L"
5.74 -  proof qed (auto intro: sup_exists inf_exists)
5.75 +  by default (auto intro: sup_exists inf_exists)
5.76
5.77  theorem (in partial_order) complete_lattice_criterion1:
5.78    assumes top_exists: "EX g. greatest L g (carrier L)"
```
```     6.1 --- a/src/HOL/Algebra/RingHom.thy	Fri Sep 02 17:58:32 2011 +0200
6.2 +++ b/src/HOL/Algebra/RingHom.thy	Fri Sep 02 18:17:45 2011 +0200
6.3 @@ -17,7 +17,7 @@
6.4      and hom_one [simp] = ring_hom_one [OF homh]
6.5
6.6  sublocale ring_hom_cring \<subseteq> ring: ring_hom_ring
6.7 -  proof qed (rule homh)
6.8 +  by default (rule homh)
6.9
6.10  sublocale ring_hom_ring \<subseteq> abelian_group: abelian_group_hom R S
6.11  apply (rule abelian_group_homI)
```
```     7.1 --- a/src/HOL/Algebra/UnivPoly.thy	Fri Sep 02 17:58:32 2011 +0200
7.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Fri Sep 02 18:17:45 2011 +0200
7.3 @@ -1764,7 +1764,7 @@
7.4      and deg_r_0: "deg R r = 0"
7.5      shows "r = monom P (eval R R id a f) 0"
7.6  proof -
7.7 -  interpret UP_pre_univ_prop R R id P proof qed simp
7.8 +  interpret UP_pre_univ_prop R R id P by default simp
7.9    have eval_ring_hom: "eval R R id a \<in> ring_hom P R"
7.10      using eval_ring_hom [OF a] by simp
7.11    have "eval R R id a f = eval R R id a ?gq \<oplus>\<^bsub>R\<^esub> eval R R id a r"
```