tuned proofs;
authorwenzelm
Fri Sep 02 18:17:45 2011 +0200 (2011-09-02)
changeset 44655fe0365331566
parent 44654 d80fe56788a5
child 44657 17dbd9d9db38
child 44663 3bc39cfe27fe
tuned proofs;
src/HOL/Algebra/AbelCoset.thy
src/HOL/Algebra/Divisibility.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/IntRing.thy
src/HOL/Algebra/Lattice.thy
src/HOL/Algebra/RingHom.thy
src/HOL/Algebra/UnivPoly.thy
     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"