--- a/src/HOL/Algebra/AbelCoset.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Algebra/AbelCoset.thy Mon Nov 17 17:00:55 2008 +0100
@@ -234,7 +234,7 @@
by (rule a_normal)
show "abelian_subgroup H G"
- by (unfold_locales, simp add: a_comm)
+ proof qed (simp add: a_comm)
qed
lemma abelian_subgroupI2:
@@ -549,7 +549,7 @@
lemma (in abelian_group_hom) is_abelian_group_hom:
"abelian_group_hom G H h"
-by (unfold_locales)
+ ..
lemma (in abelian_group_hom) hom_add [simp]:
"[| x : carrier G; y : carrier G |]
--- a/src/HOL/Algebra/Divisibility.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Algebra/Divisibility.thy Mon Nov 17 17:00:55 2008 +0100
@@ -26,14 +26,14 @@
and r_cancel:
"\<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"
shows "monoid_cancel G"
-by unfold_locales fact+
+ proof qed fact+
lemma (in monoid_cancel) is_monoid_cancel:
"monoid_cancel G"
-by intro_locales
+ ..
interpretation group \<subseteq> monoid_cancel
-by unfold_locales simp+
+ proof qed simp+
locale comm_monoid_cancel = monoid_cancel + comm_monoid
@@ -57,10 +57,10 @@
lemma (in comm_monoid_cancel) is_comm_monoid_cancel:
"comm_monoid_cancel G"
-by intro_locales
+ by intro_locales
interpretation comm_group \<subseteq> comm_monoid_cancel
-by unfold_locales
+ ..
subsection {* Products of Units in Monoids *}
@@ -1839,7 +1839,7 @@
"\<And>a fs fs'. \<lbrakk>a \<in> carrier G; set fs \<subseteq> carrier G; set fs' \<subseteq> carrier G;
wfactors G fs a; wfactors G fs' a\<rbrakk> \<Longrightarrow> essentially_equal G fs fs'"
shows "factorial_monoid G"
-proof (unfold_locales)
+proof
fix a
assume acarr: "a \<in> carrier G" and anunit: "a \<notin> Units G"
@@ -3855,19 +3855,19 @@
qed
interpretation factorial_monoid \<subseteq> primeness_condition_monoid
- by (unfold_locales, rule irreducible_is_prime)
+ proof qed (rule irreducible_is_prime)
lemma (in factorial_monoid) primeness_condition:
shows "primeness_condition_monoid G"
-by unfold_locales
+ ..
lemma (in factorial_monoid) gcd_condition [simp]:
shows "gcd_condition_monoid G"
-by (unfold_locales, rule gcdof_exists)
+ proof qed (rule gcdof_exists)
interpretation factorial_monoid \<subseteq> gcd_condition_monoid
- by (unfold_locales, rule gcdof_exists)
+ proof qed (rule gcdof_exists)
lemma (in factorial_monoid) division_weak_lattice [simp]:
shows "weak_lattice (division_rel G)"
--- a/src/HOL/Algebra/Group.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Algebra/Group.thy Mon Nov 17 17:00:55 2008 +0100
@@ -6,7 +6,9 @@
Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
*)
-theory Group imports FuncSet Lattice begin
+theory Group
+imports Lattice FuncSet
+begin
section {* Monoids and Groups *}
@@ -280,7 +282,7 @@
qed
then have carrier_subset_Units: "carrier G <= Units G"
by (unfold Units_def) fast
- show ?thesis by unfold_locales (auto simp: r_one m_assoc carrier_subset_Units)
+ show ?thesis proof qed (auto simp: r_one m_assoc carrier_subset_Units)
qed
lemma (in monoid) group_l_invI:
@@ -685,7 +687,7 @@
assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
x \<otimes> y = y \<otimes> x"
shows "comm_group G"
- by unfold_locales (simp_all add: m_comm)
+ proof qed (simp_all add: m_comm)
lemma comm_groupI:
fixes G (structure)
@@ -713,7 +715,7 @@
theorem (in group) subgroups_partial_order:
"partial_order (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)"
- by unfold_locales simp_all
+ proof qed simp_all
lemma (in group) subgroup_self:
"subgroup (carrier G) G"
--- a/src/HOL/Algebra/IntRing.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Algebra/IntRing.thy Mon Nov 17 17:00:55 2008 +0100
@@ -5,7 +5,7 @@
*)
theory IntRing
-imports QuotRing Int Primes
+imports QuotRing Lattice Int Primes
begin
@@ -104,7 +104,7 @@
and "pow \<Z> x n = x^n"
proof -
-- "Specification"
- show "monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
+ show "monoid \<Z>" proof qed (auto simp: int_ring_def)
then interpret int: monoid ["\<Z>"] .
-- "Carrier"
@@ -121,7 +121,7 @@
where "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
proof -
-- "Specification"
- show "comm_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
+ show "comm_monoid \<Z>" proof qed (auto simp: int_ring_def)
then interpret int: comm_monoid ["\<Z>"] .
-- "Operations"
@@ -146,7 +146,7 @@
and "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
proof -
-- "Specification"
- show "abelian_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
+ show "abelian_monoid \<Z>" proof qed (auto simp: int_ring_def)
then interpret int: abelian_monoid ["\<Z>"] .
-- "Operations"
@@ -189,7 +189,7 @@
qed
interpretation int: "domain" ["\<Z>"]
- by (unfold_locales) (auto simp: int_ring_def left_distrib right_distrib)
+ proof qed (auto simp: int_ring_def left_distrib right_distrib)
text {* Removal of occurrences of @{term UNIV} in interpretation result
@@ -211,7 +211,7 @@
and "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
proof -
show "partial_order (| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
- by unfold_locales simp_all
+ proof qed simp_all
show "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
by simp
show "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
@@ -248,7 +248,7 @@
interpretation int (* [unfolded UNIV] *) :
total_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
- by unfold_locales clarsimp
+ proof qed clarsimp
subsection {* Generated Ideals of @{text "\<Z>"} *}
--- a/src/HOL/Algebra/Lattice.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Algebra/Lattice.thy Mon Nov 17 17:00:55 2008 +0100
@@ -916,12 +916,12 @@
lemma (in weak_partial_order) weak_total_orderI:
assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
shows "weak_total_order L"
- by unfold_locales (rule total)
+ proof qed (rule total)
text {* Total orders are lattices. *}
interpretation weak_total_order < weak_lattice
-proof unfold_locales
+proof
fix x y
assume L: "x \<in> carrier L" "y \<in> carrier L"
show "EX s. least L s (Upper L {x, y})"
@@ -980,7 +980,7 @@
and inf_exists:
"!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
shows "weak_complete_lattice L"
- by unfold_locales (auto intro: sup_exists inf_exists)
+ proof qed (auto intro: sup_exists inf_exists)
constdefs (structure L)
top :: "_ => 'a" ("\<top>\<index>")
@@ -1106,12 +1106,6 @@
shows "P"
using assms unfolding lless_eq by auto
-lemma lless_trans [trans]:
- assumes "a \<sqsubset> b" "b \<sqsubset> c"
- and carr[simp]: "a \<in> carrier L" "b \<in> carrier L" "c \<in> carrier L"
- shows "a \<sqsubset> c"
- using assms unfolding lless_eq by (blast dest: le_trans intro: sym)
-
end
@@ -1133,14 +1127,14 @@
"[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
interpretation upper_semilattice < weak_upper_semilattice
- by unfold_locales (rule sup_of_two_exists)
+ proof qed (rule sup_of_two_exists)
locale lower_semilattice = partial_order +
assumes inf_of_two_exists:
"[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
interpretation lower_semilattice < weak_lower_semilattice
- by unfold_locales (rule inf_of_two_exists)
+ proof qed (rule inf_of_two_exists)
locale lattice = upper_semilattice + lower_semilattice
@@ -1188,22 +1182,22 @@
text {* Total Orders *}
locale total_order = partial_order +
- assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
+ assumes total_order_total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
interpretation total_order < weak_total_order
- by unfold_locales (rule total)
+ proof qed (rule total_order_total)
text {* Introduction rule: the usual definition of total order *}
lemma (in partial_order) total_orderI:
assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
shows "total_order L"
- by unfold_locales (rule total)
+ proof qed (rule total)
text {* Total orders are lattices. *}
interpretation total_order < lattice
- by unfold_locales (auto intro: sup_of_two_exists inf_of_two_exists)
+ proof qed (auto intro: sup_of_two_exists inf_of_two_exists)
text {* Complete lattices *}
@@ -1215,7 +1209,7 @@
"[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
interpretation complete_lattice < weak_complete_lattice
- by unfold_locales (auto intro: sup_exists inf_exists)
+ proof qed (auto intro: sup_exists inf_exists)
text {* Introduction rule: the usual definition of complete lattice *}
@@ -1225,7 +1219,7 @@
and inf_exists:
"!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
shows "complete_lattice L"
- by unfold_locales (auto intro: sup_exists inf_exists)
+ proof qed (auto intro: sup_exists inf_exists)
theorem (in partial_order) complete_lattice_criterion1:
assumes top_exists: "EX g. greatest L g (carrier L)"
@@ -1282,7 +1276,7 @@
(is "complete_lattice ?L")
proof (rule partial_order.complete_latticeI)
show "partial_order ?L"
- by unfold_locales auto
+ proof qed auto
next
fix B
assume B: "B \<subseteq> carrier ?L"
--- a/src/HOL/Algebra/Module.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Algebra/Module.thy Mon Nov 17 17:00:55 2008 +0100
@@ -91,11 +91,11 @@
lemma (in algebra) R_cring:
"cring R"
- by unfold_locales
+ ..
lemma (in algebra) M_cring:
"cring M"
- by unfold_locales
+ ..
lemma (in algebra) module:
"module R M"
--- a/src/HOL/Algebra/Ring.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Algebra/Ring.thy Mon Nov 17 17:00:55 2008 +0100
@@ -5,7 +5,8 @@
Copyright: Clemens Ballarin
*)
-theory Ring imports FiniteProduct
+theory Ring
+imports FiniteProduct
uses ("ringsimp.ML") begin
@@ -188,7 +189,7 @@
proof -
interpret comm_group ["\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"]
by (rule cg)
- show "abelian_group G" by (unfold_locales)
+ show "abelian_group G" ..
qed
@@ -392,7 +393,7 @@
lemma (in ring) is_abelian_group:
"abelian_group R"
- by unfold_locales
+ ..
lemma (in ring) is_monoid:
"monoid R"
@@ -670,7 +671,7 @@
lemma (in cring) cring_fieldI:
assumes field_Units: "Units R = carrier R - {\<zero>}"
shows "field R"
-proof unfold_locales
+proof
from field_Units
have a: "\<zero> \<notin> Units R" by fast
have "\<one> \<in> Units R" by fast
--- a/src/HOL/Algebra/RingHom.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Algebra/RingHom.thy Mon Nov 17 17:00:55 2008 +0100
@@ -17,7 +17,7 @@
and hom_one [simp] = ring_hom_one [OF homh]
interpretation ring_hom_cring \<subseteq> ring_hom_ring
- by (unfold_locales, rule homh)
+ proof qed (rule homh)
interpretation ring_hom_ring \<subseteq> abelian_group_hom R S
apply (rule abelian_group_homI)
--- a/src/HOL/Algebra/UnivPoly.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy Mon Nov 17 17:00:55 2008 +0100
@@ -7,7 +7,9 @@
Contributions, in particular on long division, by Jesus Aransay.
*)
-theory UnivPoly imports Module RingHom begin
+theory UnivPoly
+imports Module RingHom
+begin
section {* Univariate Polynomials *}
@@ -500,8 +502,7 @@
*}
lemma (in cring) cring:
- "cring R"
- by unfold_locales
+ "cring R" ..
lemma (in UP_cring) UP_algebra:
"algebra R P" by (auto intro!: algebraI R.cring UP_cring UP_smult_l_distr UP_smult_r_distr
@@ -1771,9 +1772,9 @@
shows "eval R R id a (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0) = \<zero>"
(is "eval R R id a ?g = _")
proof -
- interpret UP_pre_univ_prop [R R id P] by unfold_locales simp
+ interpret UP_pre_univ_prop [R R id P] proof qed simp
have eval_ring_hom: "eval R R id a \<in> ring_hom P R" using eval_ring_hom [OF a] by simp
- interpret ring_hom_cring [P R "eval R R id a"] by unfold_locales (simp add: eval_ring_hom)
+ interpret ring_hom_cring [P R "eval R R id a"] proof qed (simp add: eval_ring_hom)
have mon1_closed: "monom P \<one>\<^bsub>R\<^esub> 1 \<in> carrier P"
and mon0_closed: "monom P a 0 \<in> carrier P"
and min_mon0_closed: "\<ominus>\<^bsub>P\<^esub> monom P a 0 \<in> carrier P"
@@ -1818,7 +1819,7 @@
and deg_r_0: "deg R r = 0"
shows "r = monom P (eval R R id a f) 0"
proof -
- interpret UP_pre_univ_prop [R R id P] by unfold_locales simp
+ interpret UP_pre_univ_prop [R R id P] proof qed simp
have eval_ring_hom: "eval R R id a \<in> ring_hom P R"
using eval_ring_hom [OF a] by simp
have "eval R R id a f = eval R R id a ?gq \<oplus>\<^bsub>R\<^esub> eval R R id a r"
@@ -1884,7 +1885,8 @@
"UP INTEG"} globally.
*}
-interpretation INTEG: UP_pre_univ_prop [INTEG INTEG id] using INTEG_id_eval by simp_all
+interpretation INTEG: UP_pre_univ_prop [INTEG INTEG id]
+ using INTEG_id_eval by simp_all
lemma INTEG_closed [intro, simp]:
"z \<in> carrier INTEG"
--- a/src/HOL/Divides.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Divides.thy Mon Nov 17 17:00:55 2008 +0100
@@ -639,8 +639,8 @@
text {* @{term "op dvd"} is a partial order *}
-interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> n \<noteq> m"]
- by unfold_locales (auto intro: dvd_refl dvd_trans dvd_anti_sym)
+interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"]
+ proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym)
lemma dvd_diff: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
unfolding dvd_def
--- a/src/HOL/Finite_Set.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Finite_Set.thy Mon Nov 17 17:00:55 2008 +0100
@@ -21,7 +21,7 @@
assumes "\<not> finite (UNIV :: 'a set)" and "finite A"
shows "\<exists>a::'a. a \<notin> A"
proof -
- from prems have "A \<noteq> UNIV" by blast
+ from assms have "A \<noteq> UNIV" by blast
thus ?thesis by blast
qed
@@ -833,7 +833,7 @@
subsection {* Generalized summation over a set *}
interpretation comm_monoid_add: comm_monoid_mult ["0::'a::comm_monoid_add" "op +"]
- by unfold_locales (auto intro: add_assoc add_commute)
+ proof qed (auto intro: add_assoc add_commute)
constdefs
setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
@@ -1727,7 +1727,7 @@
case empty then show ?case by simp
next
interpret ab_semigroup_mult ["op Un"]
- by unfold_locales auto
+ proof qed auto
case insert
then show ?case by simp
qed
@@ -2125,11 +2125,7 @@
lemma ab_semigroup_idem_mult_inf:
"ab_semigroup_idem_mult inf"
- apply unfold_locales
- apply (rule inf_assoc)
- apply (rule inf_commute)
- apply (rule inf_idem)
- done
+ proof qed (rule inf_assoc inf_commute inf_idem)+
lemma below_fold1_iff:
assumes "finite A" "A \<noteq> {}"
@@ -2357,19 +2353,19 @@
lemma ab_semigroup_idem_mult_min:
"ab_semigroup_idem_mult min"
- by unfold_locales (auto simp add: min_def)
+ proof qed (auto simp add: min_def)
lemma ab_semigroup_idem_mult_max:
"ab_semigroup_idem_mult max"
- by unfold_locales (auto simp add: max_def)
+ proof qed (auto simp add: max_def)
lemma min_lattice:
"lower_semilattice (op \<le>) (op <) min"
- by unfold_locales (auto simp add: min_def)
+ proof qed (auto simp add: min_def)
lemma max_lattice:
"lower_semilattice (op \<ge>) (op >) max"
- by unfold_locales (auto simp add: max_def)
+ proof qed (auto simp add: max_def)
lemma dual_max:
"ord.max (op \<ge>) = min"
--- a/src/HOL/Groebner_Basis.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Groebner_Basis.thy Mon Nov 17 17:00:55 2008 +0100
@@ -168,7 +168,7 @@
interpretation class_semiring: gb_semiring
["op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"]
- by unfold_locales (auto simp add: ring_simps power_Suc)
+ proof qed (auto simp add: ring_simps power_Suc)
lemmas nat_arith =
add_nat_number_of diff_nat_number_of mult_nat_number_of eq_nat_number_of less_nat_number_of
@@ -244,7 +244,7 @@
interpretation class_ring: gb_ring ["op +" "op *" "op ^"
"0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"]
- by unfold_locales simp_all
+ proof qed simp_all
declaration {* normalizer_funs @{thm class_ring.gb_ring_axioms'} *}
--- a/src/HOL/Hyperreal/FrechetDeriv.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Hyperreal/FrechetDeriv.thy Mon Nov 17 17:00:55 2008 +0100
@@ -31,7 +31,7 @@
lemma bounded_linear_zero:
"bounded_linear (\<lambda>x::'a::real_normed_vector. 0::'b::real_normed_vector)"
-proof (unfold_locales)
+proof
show "(0::'b) = 0 + 0" by simp
fix r show "(0::'b) = scaleR r 0" by simp
have "\<forall>x::'a. norm (0::'b) \<le> norm x * 0" by simp
@@ -43,7 +43,7 @@
lemma bounded_linear_ident:
"bounded_linear (\<lambda>x::'a::real_normed_vector. x)"
-proof (unfold_locales)
+proof
fix x y :: 'a show "x + y = x + y" by simp
fix r and x :: 'a show "scaleR r x = scaleR r x" by simp
have "\<forall>x::'a. norm x \<le> norm x * 1" by simp
--- a/src/HOL/Hyperreal/SEQ.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Hyperreal/SEQ.thy Mon Nov 17 17:00:55 2008 +0100
@@ -935,7 +935,7 @@
lemma real_CauchyI:
assumes "Cauchy X"
shows "real_Cauchy X"
-by unfold_locales (fact assms)
+ proof qed (fact assms)
lemma (in real_Cauchy) mem_S: "\<forall>n\<ge>N. x < X n \<Longrightarrow> x \<in> S"
by (unfold S_def, auto)
--- a/src/HOL/Lattices.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Lattices.thy Mon Nov 17 17:00:55 2008 +0100
@@ -291,7 +291,7 @@
lemma (in linorder) distrib_lattice_min_max:
"distrib_lattice (op \<le>) (op <) min max"
-proof unfold_locales
+proof
have aux: "\<And>x y \<Colon> 'a. x < y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
by (auto simp add: less_le antisym)
fix x y z
--- a/src/HOL/Library/Countable.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Library/Countable.thy Mon Nov 17 17:00:55 2008 +0100
@@ -49,7 +49,7 @@
by (rule countable_classI [of "id"]) simp
subclass (in finite) countable
-proof unfold_locales
+proof
have "finite (UNIV\<Colon>'a set)" by (rule finite_UNIV)
with finite_conv_nat_seg_image [of UNIV]
obtain n and f :: "nat \<Rightarrow> 'a"
--- a/src/HOL/Library/Multiset.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Library/Multiset.thy Mon Nov 17 17:00:55 2008 +0100
@@ -1085,11 +1085,11 @@
mset_le_trans simp: mset_less_def)
interpretation mset_order_cancel_semigroup:
- pordered_cancel_ab_semigroup_add ["op +" "op \<le>#" "op <#"]
+ pordered_cancel_ab_semigroup_add ["op +" "op \<le>#" "op <#"]
proof qed (erule mset_le_mono_add [OF mset_le_refl])
interpretation mset_order_semigroup_cancel:
- pordered_ab_semigroup_add_imp_le ["op +" "op \<le>#" "op <#"]
+ pordered_ab_semigroup_add_imp_le ["op +" "op \<le>#" "op <#"]
proof qed simp
@@ -1437,7 +1437,7 @@
"image_mset f = fold_mset (op + o single o f) {#}"
interpretation image_left_comm: left_commutative ["op + o single o f"]
-by (unfold_locales) (simp add:union_ac)
+ proof qed (simp add:union_ac)
lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
by (simp add: image_mset_def)
--- a/src/HOL/Library/Univ_Poly.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Library/Univ_Poly.thy Mon Nov 17 17:00:55 2008 +0100
@@ -173,15 +173,15 @@
class recpower_semiring_0 = semiring_0 + recpower
class recpower_ring = ring + recpower
class recpower_ring_1 = ring_1 + recpower
-subclass (in recpower_ring_1) recpower_ring by unfold_locales
+subclass (in recpower_ring_1) recpower_ring ..
class recpower_comm_semiring_1 = recpower + comm_semiring_1
class recpower_comm_ring_1 = recpower + comm_ring_1
-subclass (in recpower_comm_ring_1) recpower_comm_semiring_1 by unfold_locales
+subclass (in recpower_comm_ring_1) recpower_comm_semiring_1 ..
class recpower_idom = recpower + idom
-subclass (in recpower_idom) recpower_comm_ring_1 by unfold_locales
+subclass (in recpower_idom) recpower_comm_ring_1 ..
class idom_char_0 = idom + ring_char_0
class recpower_idom_char_0 = recpower + idom_char_0
-subclass (in recpower_idom_char_0) recpower_idom by unfold_locales
+subclass (in recpower_idom_char_0) recpower_idom ..
lemma (in recpower_comm_ring_1) poly_exp: "poly (p %^ n) x = (poly p x) ^ n"
apply (induct "n")
@@ -429,7 +429,7 @@
lemma (in comm_ring_1) poly_add_minus_mult_eq: "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))"
by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult right_distrib minus_mult_left[symmetric] minus_mult_right[symmetric])
-subclass (in idom_char_0) comm_ring_1 by unfold_locales
+subclass (in idom_char_0) comm_ring_1 ..
lemma (in idom_char_0) poly_mult_left_cancel: "(poly (p *** q) = poly (p *** r)) = (poly p = poly [] | poly q = poly r)"
proof-
have "poly (p *** q) = poly (p *** r) \<longleftrightarrow> poly (p *** q +++ -- (p *** r)) = poly []" by (simp only: poly_add_minus_zero_iff)
--- a/src/HOL/List.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/List.thy Mon Nov 17 17:00:55 2008 +0100
@@ -549,9 +549,9 @@
by (induct xs) auto
interpretation semigroup_append: semigroup_add ["op @"]
-by unfold_locales simp
+ proof qed simp
interpretation monoid_append: monoid_add ["[]" "op @"]
-by unfold_locales (simp+)
+ proof qed simp+
lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])"
by (induct xs) auto
@@ -3834,7 +3834,7 @@
"map_filter f P xs = map f (filter P xs)"
by (induct xs) auto
-lemma lenght_remdups_length_unique [code inline]:
+lemma length_remdups_length_unique [code inline]:
"length (remdups xs) = length_unique xs"
by (induct xs) simp_all
--- a/src/HOL/NSA/Filter.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/NSA/Filter.thy Mon Nov 17 17:00:55 2008 +0100
@@ -77,10 +77,9 @@
apply (simp add: singleton)
done
-lemma (in freeultrafilter) filter: "filter F" by unfold_locales
+lemma (in freeultrafilter) filter: "filter F" ..
-lemma (in freeultrafilter) ultrafilter: "ultrafilter F"
- by unfold_locales
+lemma (in freeultrafilter) ultrafilter: "ultrafilter F" ..
subsection {* Collect properties *}
--- a/src/HOL/Nat.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Nat.thy Mon Nov 17 17:00:55 2008 +0100
@@ -1233,7 +1233,7 @@
text{*Every @{text ordered_semidom} has characteristic zero.*}
subclass semiring_char_0
- by unfold_locales (simp add: eq_iff order_eq_iff)
+ proof qed (simp add: eq_iff order_eq_iff)
text{*Special cases where either operand is zero*}
--- a/src/HOL/OrderedGroup.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/OrderedGroup.thy Mon Nov 17 17:00:55 2008 +0100
@@ -83,7 +83,7 @@
begin
subclass monoid_add
- by unfold_locales (insert add_0, simp_all add: add_commute)
+ proof qed (insert add_0, simp_all add: add_commute)
end
@@ -99,7 +99,7 @@
begin
subclass monoid_mult
- by unfold_locales (insert mult_1, simp_all add: mult_commute)
+ proof qed (insert mult_1, simp_all add: mult_commute)
end
@@ -123,7 +123,7 @@
begin
subclass cancel_semigroup_add
-proof unfold_locales
+proof
fix a b c :: 'a
assume "a + b = a + c"
then show "b = c" by (rule add_imp_eq)
@@ -248,10 +248,10 @@
begin
subclass group_add
- by unfold_locales (simp_all add: ab_left_minus ab_diff_minus)
+ proof qed (simp_all add: ab_left_minus ab_diff_minus)
subclass cancel_ab_semigroup_add
-proof unfold_locales
+proof
fix a b c :: 'a
assume "a + b = a + c"
then have "- a + a + b = - a + a + c"
@@ -490,7 +490,7 @@
subclass pordered_cancel_ab_semigroup_add ..
subclass pordered_ab_semigroup_add_imp_le
-proof unfold_locales
+proof
fix a b c :: 'a
assume "c + a \<le> c + b"
hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)
@@ -646,7 +646,7 @@
subclass ordered_ab_semigroup_add ..
subclass pordered_ab_semigroup_add_imp_le
-proof unfold_locales
+proof
fix a b c :: 'a
assume le: "c + a <= c + b"
show "a <= b"
@@ -1243,7 +1243,7 @@
have abs_leI: "\<And>a b. a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
by (simp add: abs_lattice le_supI)
show ?thesis
- proof unfold_locales
+ proof
fix a
show "0 \<le> \<bar>a\<bar>" by simp
next
--- a/src/HOL/Orderings.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Orderings.thy Mon Nov 17 17:00:55 2008 +0100
@@ -71,7 +71,7 @@
lemma dual_preorder:
"preorder (op \<ge>) (op >)"
-by unfold_locales (auto simp add: less_le_not_le intro: order_trans)
+proof qed (auto simp add: less_le_not_le intro: order_trans)
end
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Mon Nov 17 17:00:55 2008 +0100
@@ -369,8 +369,8 @@
interpret subspace [F E] by fact
interpret linearform [F f] by fact
interpret continuous [F norm f] by fact
- have E: "vectorspace E" by unfold_locales
- have F: "vectorspace F" by rule unfold_locales
+ have E: "vectorspace E" by intro_locales
+ have F: "vectorspace F" by rule intro_locales
have F_norm: "normed_vectorspace F norm"
using FE E_norm by (rule subspace_normed_vs)
have ge_zero: "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy Mon Nov 17 17:00:55 2008 +0100
@@ -109,7 +109,7 @@
proof
show "vectorspace F" by (rule vectorspace) unfold_locales
next
- have "NormedSpace.norm E norm" by unfold_locales
+ have "NormedSpace.norm E norm" ..
with subset show "NormedSpace.norm F norm"
by (simp add: norm_def seminorm_def norm_axioms_def)
qed
--- a/src/HOL/Real/RealVector.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Real/RealVector.thy Mon Nov 17 17:00:55 2008 +0100
@@ -62,7 +62,7 @@
and scale_left_diff_distrib: "scale (a - b) x = scale a x - scale b x"
proof -
interpret s: additive ["\<lambda>a. scale a x"]
- by unfold_locales (rule scale_left_distrib)
+ proof qed (rule scale_left_distrib)
show "scale 0 x = 0" by (rule s.zero)
show "scale (- a) x = - (scale a x)" by (rule s.minus)
show "scale (a - b) x = scale a x - scale b x" by (rule s.diff)
@@ -73,7 +73,7 @@
and scale_right_diff_distrib: "scale a (x - y) = scale a x - scale a y"
proof -
interpret s: additive ["\<lambda>x. scale a x"]
- by unfold_locales (rule scale_right_distrib)
+ proof qed (rule scale_right_distrib)
show "scale a 0 = 0" by (rule s.zero)
show "scale a (- x) = - (scale a x)" by (rule s.minus)
show "scale a (x - y) = scale a x - scale a y" by (rule s.diff)
@@ -197,10 +197,10 @@
done
interpretation scaleR_left: additive ["(\<lambda>a. scaleR a x::'a::real_vector)"]
-by unfold_locales (rule scaleR_left_distrib)
+proof qed (rule scaleR_left_distrib)
interpretation scaleR_right: additive ["(\<lambda>x. scaleR a x::'a::real_vector)"]
-by unfold_locales (rule scaleR_right_distrib)
+proof qed (rule scaleR_right_distrib)
lemma nonzero_inverse_scaleR_distrib:
fixes x :: "'a::real_div_algebra" shows
--- a/src/HOL/Ring_and_Field.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Ring_and_Field.thy Mon Nov 17 17:00:55 2008 +0100
@@ -45,7 +45,7 @@
begin
subclass semiring_0
-proof unfold_locales
+proof
fix a :: 'a
have "0 * a + 0 * a = 0 * a + 0"
by (simp add: left_distrib [symmetric])
@@ -66,7 +66,7 @@
begin
subclass semiring
-proof unfold_locales
+proof
fix a b c :: 'a
show "(a + b) * c = a * c + b * c" by (simp add: distrib)
have "a * (b + c) = (b + c) * a" by (simp add: mult_ac)
@@ -362,7 +362,7 @@
begin
subclass ring_1_no_zero_divisors
-proof unfold_locales
+proof
fix a b :: 'a
assume a: "a \<noteq> 0" and b: "b \<noteq> 0"
show "a * b \<noteq> 0"
@@ -476,7 +476,7 @@
begin
subclass division_ring
-proof unfold_locales
+proof
fix a :: 'a
assume "a \<noteq> 0"
thus "inverse a * a = 1" by (rule field_inverse)
@@ -595,7 +595,7 @@
subclass semiring_0_cancel ..
subclass ordered_semiring
-proof unfold_locales
+proof
fix a b c :: 'a
assume A: "a \<le> b" "0 \<le> c"
from A show "c * a \<le> c * b"
@@ -713,7 +713,7 @@
begin
subclass pordered_semiring
-proof unfold_locales
+proof
fix a b c :: 'a
assume "a \<le> b" "0 \<le> c"
thus "c * a \<le> c * b" by (rule mult_mono1)
@@ -736,7 +736,7 @@
begin
subclass ordered_semiring_strict
-proof unfold_locales
+proof
fix a b c :: 'a
assume "a < b" "0 < c"
thus "c * a < c * b" by (rule mult_strict_left_mono_comm)
@@ -744,7 +744,7 @@
qed
subclass pordered_cancel_comm_semiring
-proof unfold_locales
+proof
fix a b c :: 'a
assume "a \<le> b" "0 \<le> c"
thus "c * a \<le> c * b"
@@ -815,7 +815,7 @@
subclass pordered_ring ..
subclass pordered_ab_group_add_abs
-proof unfold_locales
+proof
fix a b
show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
by (auto simp add: abs_if not_less neg_less_eq_nonneg less_eq_neg_nonpos)
@@ -852,7 +852,7 @@
by (drule mult_strict_right_mono_neg, auto)
subclass ring_no_zero_divisors
-proof unfold_locales
+proof
fix a b
assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff)
assume "b \<noteq> 0" then have B: "b < 0 \<or> 0 < b" by (simp add: neq_iff)
@@ -1019,7 +1019,7 @@
subclass idom ..
subclass ordered_semidom
-proof unfold_locales
+proof
have "0 \<le> 1 * 1" by (rule zero_le_square)
thus "0 < 1" by (simp add: le_less)
qed
--- a/src/HOL/Word/WordArith.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Word/WordArith.thy Mon Nov 17 17:00:55 2008 +0100
@@ -19,9 +19,8 @@
simp: word_uint.Rep_inject [symmetric])
lemma signed_linorder: "linorder word_sle word_sless"
- apply unfold_locales
- apply (unfold word_sle_def word_sless_def)
- by auto
+proof
+qed (unfold word_sle_def word_sless_def, auto)
interpretation signed: linorder ["word_sle" "word_sless"]
by (rule signed_linorder)
--- a/src/HOL/ex/LocaleTest2.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/ex/LocaleTest2.thy Mon Nov 17 17:00:55 2008 +0100
@@ -435,7 +435,7 @@
interpretation dlo < dlat
(* TODO: definition syntax is unavailable *)
-proof unfold_locales
+proof
fix x y
from total have "is_inf x y (if x \<sqsubseteq> y then x else y)" by (auto simp: is_inf_def)
then show "EX inf. is_inf x y inf" by blast
@@ -446,7 +446,7 @@
qed
interpretation dlo < ddlat
-proof unfold_locales
+proof
fix x y z
show "x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z" (is "?l = ?r")
txt {* Jacobson I, p.\ 462 *}
@@ -475,7 +475,7 @@
txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
proof -
show "dpo (op <= :: [int, int] => bool)"
- by unfold_locales auto
+ proof qed auto
then interpret int: dpo ["op <= :: [int, int] => bool"] .
txt {* Gives interpreted version of @{text less_def} (without condition). *}
show "(dpo.less (op <=) (x::int) y) = (x < y)"
@@ -514,7 +514,7 @@
qed
interpretation int: dlo ["op <= :: [int, int] => bool"]
- by unfold_locales arith
+ proof qed arith
text {* Interpreted theorems from the locales, involving defined terms. *}
@@ -531,7 +531,7 @@
txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
proof -
show "dpo (op <= :: [nat, nat] => bool)"
- by unfold_locales auto
+ proof qed auto
then interpret nat: dpo ["op <= :: [nat, nat] => bool"] .
txt {* Gives interpreted version of @{text less_def} (without condition). *}
show "dpo.less (op <=) (x::nat) y = (x < y)"
@@ -565,7 +565,7 @@
qed
interpretation nat: dlo ["op <= :: [nat, nat] => bool"]
- by unfold_locales arith
+ proof qed arith
text {* Interpreted theorems from the locales, involving defined terms. *}
@@ -582,7 +582,7 @@
txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
proof -
show "dpo (op dvd :: [nat, nat] => bool)"
- by unfold_locales (auto simp: dvd_def)
+ proof qed (auto simp: dvd_def)
then interpret nat_dvd: dpo ["op dvd :: [nat, nat] => bool"] .
txt {* Gives interpreted version of @{text less_def} (without condition). *}
show "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
@@ -842,7 +842,7 @@
where "Dmonoid.unit (op o) id f = bij (f::'a => 'a)"
(* and "Dmonoid.inv (op o) id" = "inv :: ('a => 'a) => ('a => 'a)" *)
proof -
- show "Dmonoid op o (id :: 'a => 'a)" by unfold_locales (simp_all add: o_assoc)
+ show "Dmonoid op o (id :: 'a => 'a)" proof qed (simp_all add: o_assoc)
note Dmonoid = this
(*
from this interpret Dmonoid ["op o" "id :: 'a => 'a"] .
@@ -891,7 +891,7 @@
interpretation Dfun: Dgrp ["op o" "id :: unit => unit"]
where "Dmonoid.inv (op o) id f = inv (f :: unit => unit)"
proof -
- have "Dmonoid op o (id :: 'a => 'a)" by unfold_locales (simp_all add: o_assoc)
+ have "Dmonoid op o (id :: 'a => 'a)" ..
note Dmonoid = this
show "Dgrp (op o) (id :: unit => unit)"
--- a/src/HOL/ex/Numeral.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/ex/Numeral.thy Mon Nov 17 17:00:55 2008 +0100
@@ -699,7 +699,7 @@
begin
subclass semiring_1_minus
- by unfold_locales (simp_all add: ring_simps)
+ proof qed (simp_all add: ring_simps)
lemma Dig_zero_minus_of_num [numeral]:
"0 - of_num n = - of_num n"
--- a/src/HOL/ex/Tarski.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/ex/Tarski.thy Mon Nov 17 17:00:55 2008 +0100
@@ -923,6 +923,6 @@
apply (rule fixf_po, clarify)
apply (simp add: P_def A_def r_def)
apply (rule Tarski.tarski_full_lemma [OF Tarski.intro [OF _ Tarski_axioms.intro]])
-proof - show "CLF cl f" by unfold_locales qed
+proof - show "CLF cl f" .. qed
end