More porting to new locales.
--- a/src/HOL/Algebra/AbelCoset.thy Tue Dec 16 15:09:37 2008 +0100
+++ b/src/HOL/Algebra/AbelCoset.thy Tue Dec 16 21:10:53 2008 +0100
@@ -1,6 +1,5 @@
(*
Title: HOL/Algebra/AbelCoset.thy
- Id: $Id$
Author: Stephan Hohe, TU Muenchen
*)
@@ -52,7 +51,9 @@
"a_kernel G H h \<equiv> kernel \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
\<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
-locale abelian_group_hom = abelian_group G + abelian_group H + var h +
+locale abelian_group_hom = G: abelian_group G + H: abelian_group H
+ for G (structure) and H (structure) +
+ fixes h
assumes a_group_hom: "group_hom (| carrier = carrier G, mult = add G, one = zero G |)
(| carrier = carrier H, mult = add H, one = zero H |) h"
@@ -180,7 +181,8 @@
subsubsection {* Subgroups *}
-locale additive_subgroup = var H + struct G +
+locale additive_subgroup =
+ fixes H and G (structure)
assumes a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
lemma (in additive_subgroup) is_additive_subgroup:
@@ -218,7 +220,7 @@
text {* Every subgroup of an @{text "abelian_group"} is normal *}
-locale abelian_subgroup = additive_subgroup H G + abelian_group G +
+locale abelian_subgroup = additive_subgroup + abelian_group G +
assumes a_normal: "normal H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
lemma (in abelian_subgroup) is_abelian_subgroup:
@@ -230,7 +232,7 @@
and a_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus>\<^bsub>G\<^esub> y = y \<oplus>\<^bsub>G\<^esub> x"
shows "abelian_subgroup H G"
proof -
- interpret normal ["H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"]
+ interpret normal "H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
by (rule a_normal)
show "abelian_subgroup H G"
@@ -243,9 +245,9 @@
and a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
shows "abelian_subgroup H G"
proof -
- interpret comm_group ["\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"]
+ interpret comm_group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
by (rule a_comm_group)
- interpret subgroup ["H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"]
+ interpret subgroup "H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
by (rule a_subgroup)
show "abelian_subgroup H G"
@@ -538,8 +540,8 @@
(| carrier = carrier H, mult = add H, one = zero H |) h"
shows "abelian_group_hom G H h"
proof -
- interpret G: abelian_group [G] by fact
- interpret H: abelian_group [H] by fact
+ interpret G!: abelian_group G by fact
+ interpret H!: abelian_group H by fact
show ?thesis apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
apply fact
apply fact
@@ -690,7 +692,7 @@
assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
shows "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
proof -
- interpret G: ring [G] by fact
+ interpret G!: ring G by fact
from carr
have "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)" by (rule a_rcos_module)
with carr
--- a/src/HOL/Algebra/Congruence.thy Tue Dec 16 15:09:37 2008 +0100
+++ b/src/HOL/Algebra/Congruence.thy Tue Dec 16 21:10:53 2008 +0100
@@ -1,6 +1,5 @@
(*
Title: Algebra/Congruence.thy
- Id: $Id$
Author: Clemens Ballarin, started 3 January 2008
Copyright: Clemens Ballarin
*)
--- a/src/HOL/Algebra/Coset.thy Tue Dec 16 15:09:37 2008 +0100
+++ b/src/HOL/Algebra/Coset.thy Tue Dec 16 21:10:53 2008 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Algebra/Coset.thy
- ID: $Id$
Author: Florian Kammueller, with new proofs by L C Paulson, and
Stephan Hohe
*)
@@ -114,7 +113,7 @@
and repr: "H #> x = H #> y"
shows "y \<in> H #> x"
proof -
- interpret subgroup [H G] by fact
+ interpret subgroup H G by fact
show ?thesis apply (subst repr)
apply (intro rcos_self)
apply (rule ycarr)
@@ -129,7 +128,7 @@
and a': "a' \<in> H #> a"
shows "a' \<in> carrier G"
proof -
- interpret group [G] by fact
+ interpret group G by fact
from subset and acarr
have "H #> a \<subseteq> carrier G" by (rule r_coset_subset_G)
from this and a'
@@ -142,7 +141,7 @@
assumes hH: "h \<in> H"
shows "H #> h = H"
proof -
- interpret group [G] by fact
+ interpret group G by fact
show ?thesis apply (unfold r_coset_def)
apply rule
apply rule
@@ -173,7 +172,7 @@
and x'cos: "x' \<in> H #> x"
shows "(x' \<otimes> inv x) \<in> H"
proof -
- interpret group [G] by fact
+ interpret group G by fact
from xcarr x'cos
have x'carr: "x' \<in> carrier G"
by (rule elemrcos_carrier[OF is_group])
@@ -213,7 +212,7 @@
and xixH: "(x' \<otimes> inv x) \<in> H"
shows "x' \<in> H #> x"
proof -
- interpret group [G] by fact
+ interpret group G by fact
from xixH
have "\<exists>h\<in>H. x' \<otimes> (inv x) = h" by fast
from this
@@ -244,7 +243,7 @@
assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
shows "(x' \<in> H #> x) = (x' \<otimes> inv x \<in> H)"
proof -
- interpret group [G] by fact
+ interpret group G by fact
show ?thesis proof assume "x' \<in> H #> x"
from this and carr
show "x' \<otimes> inv x \<in> H"
@@ -263,7 +262,7 @@
assumes XH: "X \<in> rcosets H"
shows "X \<subseteq> carrier G"
proof -
- interpret group [G] by fact
+ interpret group G by fact
from XH have "\<exists>x\<in> carrier G. X = H #> x"
unfolding RCOSETS_def
by fast
@@ -348,7 +347,7 @@
and xixH: "(inv x \<otimes> x') \<in> H"
shows "x' \<in> x <# H"
proof -
- interpret group [G] by fact
+ interpret group G by fact
from xixH
have "\<exists>h\<in>H. (inv x) \<otimes> x' = h" by fast
from this
@@ -600,7 +599,7 @@
assumes "group G"
shows "equiv (carrier G) (rcong H)"
proof -
- interpret group [G] by fact
+ interpret group G by fact
show ?thesis
proof (intro equiv.intro)
show "refl (carrier G) (rcong H)"
@@ -647,7 +646,7 @@
assumes a: "a \<in> carrier G"
shows "a <# H = rcong H `` {a}"
proof -
- interpret group [G] by fact
+ interpret group G by fact
show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a )
qed
@@ -658,7 +657,7 @@
assumes p: "ha \<otimes> a = h \<otimes> b" "a \<in> carrier G" "b \<in> carrier G" "h \<in> H" "ha \<in> H" "hb \<in> H"
shows "hb \<otimes> a \<in> (\<Union>h\<in>H. {h \<otimes> b})"
proof -
- interpret subgroup [H G] by fact
+ interpret subgroup H G by fact
from p show ?thesis apply (rule_tac UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"])
apply (simp add: )
apply (simp add: m_assoc transpose_inv)
@@ -670,7 +669,7 @@
assumes p: "a \<in> rcosets H" "b \<in> rcosets H" "a\<noteq>b"
shows "a \<inter> b = {}"
proof -
- interpret subgroup [H G] by fact
+ interpret subgroup H G by fact
from p show ?thesis apply (simp add: RCOSETS_def r_coset_def)
apply (blast intro: rcos_equation prems sym)
done
@@ -760,7 +759,7 @@
assumes "subgroup H G"
shows "\<Union>(rcosets H) = carrier G"
proof -
- interpret subgroup [H G] by fact
+ interpret subgroup H G by fact
show ?thesis
apply (rule equalityI)
apply (force simp add: RCOSETS_def r_coset_def)
@@ -847,7 +846,7 @@
assumes "group G"
shows "H \<in> rcosets H"
proof -
- interpret group [G] by fact
+ interpret group G by fact
from _ subgroup_axioms have "H #> \<one> = H"
by (rule coset_join2) auto
then show ?thesis
--- a/src/HOL/Algebra/Divisibility.thy Tue Dec 16 15:09:37 2008 +0100
+++ b/src/HOL/Algebra/Divisibility.thy Tue Dec 16 21:10:53 2008 +0100
@@ -1,6 +1,5 @@
(*
Title: Divisibility in monoids and rings
- Id: $Id$
Author: Clemens Ballarin, started 18 July 2008
Based on work by Stephan Hohe.
@@ -32,7 +31,7 @@
"monoid_cancel G"
..
-interpretation group \<subseteq> monoid_cancel
+sublocale group \<subseteq> monoid_cancel
proof qed simp+
@@ -45,7 +44,7 @@
"\<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 "comm_monoid_cancel G"
proof -
- interpret comm_monoid [G] by fact
+ interpret comm_monoid G by fact
show "comm_monoid_cancel G"
apply unfold_locales
apply (subgoal_tac "a \<otimes> c = b \<otimes> c")
@@ -59,7 +58,7 @@
"comm_monoid_cancel G"
by intro_locales
-interpretation comm_group \<subseteq> comm_monoid_cancel
+sublocale comm_group \<subseteq> comm_monoid_cancel
..
@@ -755,7 +754,7 @@
using pf
unfolding properfactor_lless
proof -
- interpret weak_partial_order ["division_rel G"] ..
+ interpret weak_partial_order "division_rel G" ..
from x'x
have "x' .=\<^bsub>division_rel G\<^esub> x" by simp
also assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y"
@@ -771,7 +770,7 @@
using pf
unfolding properfactor_lless
proof -
- interpret weak_partial_order ["division_rel G"] ..
+ interpret weak_partial_order "division_rel G" ..
assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y"
also from yy'
have "y .=\<^bsub>division_rel G\<^esub> y'" by simp
@@ -2916,7 +2915,7 @@
lemma (in gcd_condition_monoid) division_weak_lower_semilattice [simp]:
shows "weak_lower_semilattice (division_rel G)"
proof -
- interpret weak_partial_order ["division_rel G"] ..
+ interpret weak_partial_order "division_rel G" ..
show ?thesis
apply (unfold_locales, simp_all)
proof -
@@ -2941,7 +2940,7 @@
shows "a' gcdof b c"
proof -
note carr = a'carr carr'
- interpret weak_lower_semilattice ["division_rel G"] by simp
+ interpret weak_lower_semilattice "division_rel G" by simp
have "a' \<in> carrier G \<and> a' gcdof b c"
apply (simp add: gcdof_greatestLower carr')
apply (subst greatest_Lower_cong_l[of _ a])
@@ -2958,7 +2957,7 @@
assumes carr: "a \<in> carrier G" "b \<in> carrier G"
shows "somegcd G a b \<in> carrier G"
proof -
- interpret weak_lower_semilattice ["division_rel G"] by simp
+ interpret weak_lower_semilattice "division_rel G" by simp
show ?thesis
apply (simp add: somegcd_meet[OF carr])
apply (rule meet_closed[simplified], fact+)
@@ -2969,7 +2968,7 @@
assumes carr: "a \<in> carrier G" "b \<in> carrier G"
shows "(somegcd G a b) gcdof a b"
proof -
- interpret weak_lower_semilattice ["division_rel G"] by simp
+ interpret weak_lower_semilattice "division_rel G" by simp
from carr
have "somegcd G a b \<in> carrier G \<and> (somegcd G a b) gcdof a b"
apply (subst gcdof_greatestLower, simp, simp)
@@ -2983,7 +2982,7 @@
assumes carr: "a \<in> carrier G" "b \<in> carrier G"
shows "\<exists>x\<in>carrier G. x = somegcd G a b"
proof -
- interpret weak_lower_semilattice ["division_rel G"] by simp
+ interpret weak_lower_semilattice "division_rel G" by simp
show ?thesis
apply (simp add: somegcd_meet[OF carr])
apply (rule meet_closed[simplified], fact+)
@@ -2994,7 +2993,7 @@
assumes carr: "a \<in> carrier G" "b \<in> carrier G"
shows "(somegcd G a b) divides a"
proof -
- interpret weak_lower_semilattice ["division_rel G"] by simp
+ interpret weak_lower_semilattice "division_rel G" by simp
show ?thesis
apply (simp add: somegcd_meet[OF carr])
apply (rule meet_left[simplified], fact+)
@@ -3005,7 +3004,7 @@
assumes carr: "a \<in> carrier G" "b \<in> carrier G"
shows "(somegcd G a b) divides b"
proof -
- interpret weak_lower_semilattice ["division_rel G"] by simp
+ interpret weak_lower_semilattice "division_rel G" by simp
show ?thesis
apply (simp add: somegcd_meet[OF carr])
apply (rule meet_right[simplified], fact+)
@@ -3017,7 +3016,7 @@
and L: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
shows "z divides (somegcd G x y)"
proof -
- interpret weak_lower_semilattice ["division_rel G"] by simp
+ interpret weak_lower_semilattice "division_rel G" by simp
show ?thesis
apply (simp add: somegcd_meet L)
apply (rule meet_le[simplified], fact+)
@@ -3029,7 +3028,7 @@
and carr: "x \<in> carrier G" "x' \<in> carrier G" "y \<in> carrier G"
shows "somegcd G x y \<sim> somegcd G x' y"
proof -
- interpret weak_lower_semilattice ["division_rel G"] by simp
+ interpret weak_lower_semilattice "division_rel G" by simp
show ?thesis
apply (simp add: somegcd_meet carr)
apply (rule meet_cong_l[simplified], fact+)
@@ -3041,7 +3040,7 @@
and yy': "y \<sim> y'"
shows "somegcd G x y \<sim> somegcd G x y'"
proof -
- interpret weak_lower_semilattice ["division_rel G"] by simp
+ interpret weak_lower_semilattice "division_rel G" by simp
show ?thesis
apply (simp add: somegcd_meet carr)
apply (rule meet_cong_r[simplified], fact+)
@@ -3092,7 +3091,7 @@
assumes "finite A" "A \<subseteq> carrier G" "A \<noteq> {}"
shows "\<exists>x\<in> carrier G. x = SomeGcd G A"
proof -
- interpret weak_lower_semilattice ["division_rel G"] by simp
+ interpret weak_lower_semilattice "division_rel G" by simp
show ?thesis
apply (simp add: SomeGcd_def)
apply (rule finite_inf_closed[simplified], fact+)
@@ -3103,7 +3102,7 @@
assumes carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G"
shows "somegcd G (somegcd G a b) c \<sim> somegcd G a (somegcd G b c)"
proof -
- interpret weak_lower_semilattice ["division_rel G"] by simp
+ interpret weak_lower_semilattice "division_rel G" by simp
show ?thesis
apply (subst (2 3) somegcd_meet, (simp add: carr)+)
apply (simp add: somegcd_meet carr)
@@ -3313,7 +3312,7 @@
qed
qed
-interpretation gcd_condition_monoid \<subseteq> primeness_condition_monoid
+sublocale gcd_condition_monoid \<subseteq> primeness_condition_monoid
by (rule primeness_condition)
@@ -3832,7 +3831,7 @@
with fca fcb show ?thesis by simp
qed
-interpretation factorial_monoid \<subseteq> divisor_chain_condition_monoid
+sublocale factorial_monoid \<subseteq> divisor_chain_condition_monoid
apply unfold_locales
apply (rule wfUNIVI)
apply (rule measure_induct[of "factorcount G"])
@@ -3854,7 +3853,7 @@
done
qed
-interpretation factorial_monoid \<subseteq> primeness_condition_monoid
+sublocale factorial_monoid \<subseteq> primeness_condition_monoid
proof qed (rule irreducible_is_prime)
@@ -3866,13 +3865,13 @@
shows "gcd_condition_monoid G"
proof qed (rule gcdof_exists)
-interpretation factorial_monoid \<subseteq> gcd_condition_monoid
+sublocale factorial_monoid \<subseteq> gcd_condition_monoid
proof qed (rule gcdof_exists)
lemma (in factorial_monoid) division_weak_lattice [simp]:
shows "weak_lattice (division_rel G)"
proof -
- interpret weak_lower_semilattice ["division_rel G"] by simp
+ interpret weak_lower_semilattice "division_rel G" by simp
show "weak_lattice (division_rel G)"
apply (unfold_locales, simp_all)
@@ -3902,14 +3901,14 @@
proof clarify
assume dcc: "divisor_chain_condition_monoid G"
and pc: "primeness_condition_monoid G"
- interpret divisor_chain_condition_monoid ["G"] by (rule dcc)
- interpret primeness_condition_monoid ["G"] by (rule pc)
+ interpret divisor_chain_condition_monoid "G" by (rule dcc)
+ interpret primeness_condition_monoid "G" by (rule pc)
show "factorial_monoid G"
by (fast intro: factorial_monoidI wfactors_exist wfactors_unique)
next
assume fm: "factorial_monoid G"
- interpret factorial_monoid ["G"] by (rule fm)
+ interpret factorial_monoid "G" by (rule fm)
show "divisor_chain_condition_monoid G \<and> primeness_condition_monoid G"
by rule unfold_locales
qed
@@ -3920,13 +3919,13 @@
proof clarify
assume dcc: "divisor_chain_condition_monoid G"
and gc: "gcd_condition_monoid G"
- interpret divisor_chain_condition_monoid ["G"] by (rule dcc)
- interpret gcd_condition_monoid ["G"] by (rule gc)
+ interpret divisor_chain_condition_monoid "G" by (rule dcc)
+ interpret gcd_condition_monoid "G" by (rule gc)
show "factorial_monoid G"
by (simp add: factorial_condition_one[symmetric], rule, unfold_locales)
next
assume fm: "factorial_monoid G"
- interpret factorial_monoid ["G"] by (rule fm)
+ interpret factorial_monoid "G" by (rule fm)
show "divisor_chain_condition_monoid G \<and> gcd_condition_monoid G"
by rule unfold_locales
qed
--- a/src/HOL/Algebra/FiniteProduct.thy Tue Dec 16 15:09:37 2008 +0100
+++ b/src/HOL/Algebra/FiniteProduct.thy Tue Dec 16 21:10:53 2008 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Algebra/FiniteProduct.thy
- ID: $Id$
Author: Clemens Ballarin, started 19 November 2002
This file is largely based on HOL/Finite_Set.thy.
@@ -519,9 +518,9 @@
lemma finprod_singleton:
assumes i_in_A: "i \<in> A" and fin_A: "finite A" and f_Pi: "f \<in> A \<rightarrow> carrier G"
shows "(\<Otimes>j\<in>A. if i = j then f j else \<one>) = f i"
- using i_in_A G.finprod_insert [of "A - {i}" i "(\<lambda>j. if i = j then f j else \<one>)"]
- fin_A f_Pi G.finprod_one [of "A - {i}"]
- G.finprod_cong [of "A - {i}" "A - {i}" "(\<lambda>j. if i = j then f j else \<one>)" "(\<lambda>i. \<one>)"]
+ using i_in_A finprod_insert [of "A - {i}" i "(\<lambda>j. if i = j then f j else \<one>)"]
+ fin_A f_Pi finprod_one [of "A - {i}"]
+ finprod_cong [of "A - {i}" "A - {i}" "(\<lambda>j. if i = j then f j else \<one>)" "(\<lambda>i. \<one>)"]
unfolding Pi_def simp_implies_def by (force simp add: insert_absorb)
end
--- a/src/HOL/Algebra/Group.thy Tue Dec 16 15:09:37 2008 +0100
+++ b/src/HOL/Algebra/Group.thy Tue Dec 16 21:10:53 2008 +0100
@@ -1,6 +1,5 @@
(*
Title: HOL/Algebra/Group.thy
- Id: $Id$
Author: Clemens Ballarin, started 4 February 2003
Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
@@ -425,7 +424,7 @@
assumes "group G"
shows "group (G\<lparr>carrier := H\<rparr>)"
proof -
- interpret group [G] by fact
+ interpret group G by fact
show ?thesis
apply (rule monoid.group_l_invI)
apply (unfold_locales) [1]
@@ -489,8 +488,8 @@
assumes "monoid G" and "monoid H"
shows "monoid (G \<times>\<times> H)"
proof -
- interpret G: monoid [G] by fact
- interpret H: monoid [H] by fact
+ interpret G!: monoid G by fact
+ interpret H!: monoid H by fact
from assms
show ?thesis by (unfold monoid_def DirProd_def, auto)
qed
@@ -501,8 +500,8 @@
assumes "group G" and "group H"
shows "group (G \<times>\<times> H)"
proof -
- interpret G: group [G] by fact
- interpret H: group [H] by fact
+ interpret G!: group G by fact
+ interpret H!: group H by fact
show ?thesis by (rule groupI)
(auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
simp add: DirProd_def)
@@ -526,9 +525,9 @@
and h: "h \<in> carrier H"
shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
proof -
- interpret G: group [G] by fact
- interpret H: group [H] by fact
- interpret Prod: group ["G \<times>\<times> H"]
+ interpret G!: group G by fact
+ interpret H!: group H by fact
+ interpret Prod!: group "G \<times>\<times> H"
by (auto intro: DirProd_group group.intro group.axioms assms)
show ?thesis by (simp add: Prod.inv_equality g h)
qed
@@ -587,7 +586,8 @@
text{*Basis for homomorphism proofs: we assume two groups @{term G} and
@{term H}, with a homomorphism @{term h} between them*}
-locale group_hom = group G + group H + var h +
+locale group_hom = G: group G + H: group H for G (structure) and H (structure) +
+ fixes h
assumes homh: "h \<in> hom G H"
notes hom_mult [simp] = hom_mult [OF homh]
and hom_closed [simp] = hom_closed [OF homh]
--- a/src/HOL/Algebra/Ideal.thy Tue Dec 16 15:09:37 2008 +0100
+++ b/src/HOL/Algebra/Ideal.thy Tue Dec 16 21:10:53 2008 +0100
@@ -1,6 +1,5 @@
(*
Title: HOL/Algebra/CIdeal.thy
- Id: $Id$
Author: Stephan Hohe, TU Muenchen
*)
@@ -18,7 +17,7 @@
assumes I_l_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
and I_r_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
-interpretation ideal \<subseteq> abelian_subgroup I R
+sublocale ideal \<subseteq> abelian_subgroup I R
apply (intro abelian_subgroupI3 abelian_group.intro)
apply (rule ideal.axioms, rule ideal_axioms)
apply (rule abelian_group.axioms, rule ring.axioms, rule ideal.axioms, rule ideal_axioms)
@@ -37,7 +36,7 @@
and I_r_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
shows "ideal I R"
proof -
- interpret ring [R] by fact
+ interpret ring R by fact
show ?thesis apply (intro ideal.intro ideal_axioms.intro additive_subgroupI)
apply (rule a_subgroup)
apply (rule is_ring)
@@ -68,7 +67,7 @@
assumes generate: "\<exists>i \<in> carrier R. I = Idl {i}"
shows "principalideal I R"
proof -
- interpret ideal [I R] by fact
+ interpret ideal I R by fact
show ?thesis by (intro principalideal.intro principalideal_axioms.intro) (rule is_ideal, rule generate)
qed
@@ -89,7 +88,7 @@
and I_maximal: "\<And>J. \<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> J = I \<or> J = carrier R"
shows "maximalideal I R"
proof -
- interpret ideal [I R] by fact
+ interpret ideal I R by fact
show ?thesis by (intro maximalideal.intro maximalideal_axioms.intro)
(rule is_ideal, rule I_notcarr, rule I_maximal)
qed
@@ -112,8 +111,8 @@
and I_prime: "\<And>a b. \<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I"
shows "primeideal I R"
proof -
- interpret ideal [I R] by fact
- interpret cring [R] by fact
+ interpret ideal I R by fact
+ interpret cring R by fact
show ?thesis by (intro primeideal.intro primeideal_axioms.intro)
(rule is_ideal, rule is_cring, rule I_notcarr, rule I_prime)
qed
@@ -129,7 +128,7 @@
shows "primeideal I R"
proof -
interpret additive_subgroup [I R] by fact
- interpret cring [R] by fact
+ interpret cring R by fact
show ?thesis apply (intro_locales)
apply (intro ideal_axioms.intro)
apply (erule (1) I_l_closed)
@@ -207,7 +206,7 @@
assumes "ideal J R"
shows "ideal (I \<inter> J) R"
proof -
- interpret ideal [I R] by fact
+ interpret ideal I R by fact
interpret ideal [J R] by fact
show ?thesis
apply (intro idealI subgroup.intro)
@@ -245,7 +244,7 @@
from notempty have "\<exists>I0. I0 \<in> S" by blast
from this obtain I0 where I0S: "I0 \<in> S" by auto
- interpret ideal ["I0" "R"] by (rule Sideals[OF I0S])
+ interpret ideal I0 R by (rule Sideals[OF I0S])
from xI[OF I0S] have "x \<in> I0" .
from this and a_subset show "x \<in> carrier R" by fast
@@ -258,13 +257,13 @@
fix J
assume JS: "J \<in> S"
- interpret ideal ["J" "R"] by (rule Sideals[OF JS])
+ interpret ideal J R by (rule Sideals[OF JS])
from xI[OF JS] and yI[OF JS]
show "x \<oplus> y \<in> J" by (rule a_closed)
next
fix J
assume JS: "J \<in> S"
- interpret ideal ["J" "R"] by (rule Sideals[OF JS])
+ interpret ideal J R by (rule Sideals[OF JS])
show "\<zero> \<in> J" by simp
next
fix x
@@ -273,7 +272,7 @@
fix J
assume JS: "J \<in> S"
- interpret ideal ["J" "R"] by (rule Sideals[OF JS])
+ interpret ideal J R by (rule Sideals[OF JS])
from xI[OF JS]
show "\<ominus> x \<in> J" by (rule a_inv_closed)
@@ -285,7 +284,7 @@
fix J
assume JS: "J \<in> S"
- interpret ideal ["J" "R"] by (rule Sideals[OF JS])
+ interpret ideal J R by (rule Sideals[OF JS])
from xI[OF JS] and ycarr
show "y \<otimes> x \<in> J" by (rule I_l_closed)
@@ -297,7 +296,7 @@
fix J
assume JS: "J \<in> S"
- interpret ideal ["J" "R"] by (rule Sideals[OF JS])
+ interpret ideal J R by (rule Sideals[OF JS])
from xI[OF JS] and ycarr
show "x \<otimes> y \<in> J" by (rule I_r_closed)
@@ -443,7 +442,7 @@
lemma (in ring) genideal_one:
"Idl {\<one>} = carrier R"
proof -
- interpret ideal ["Idl {\<one>}" "R"] by (rule genideal_ideal, fast intro: one_closed)
+ interpret ideal "Idl {\<one>}" "R" by (rule genideal_ideal, fast intro: one_closed)
show "Idl {\<one>} = carrier R"
apply (rule, rule a_subset)
apply (simp add: one_imp_carrier genideal_self')
@@ -660,7 +659,7 @@
assumes "cring R"
shows "\<exists>x\<in>I. I = carrier R #> x"
proof -
- interpret cring [R] by fact
+ interpret cring R by fact
from generate
obtain i
where icarr: "i \<in> carrier R"
@@ -693,7 +692,7 @@
assumes notprime: "\<not> primeideal I R"
shows "carrier R = I \<or> (\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I)"
proof (rule ccontr, clarsimp)
- interpret cring [R] by fact
+ interpret cring R by fact
assume InR: "carrier R \<noteq> I"
and "\<forall>a. a \<in> carrier R \<longrightarrow> (\<forall>b. a \<otimes> b \<in> I \<longrightarrow> b \<in> carrier R \<longrightarrow> a \<in> I \<or> b \<in> I)"
hence I_prime: "\<And> a b. \<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I" by simp
@@ -713,7 +712,7 @@
obtains "carrier R = I"
| "\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I"
proof -
- interpret R: cring [R] by fact
+ interpret R!: cring R by fact
assume "carrier R = I ==> thesis"
and "\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I \<Longrightarrow> thesis"
then show thesis using primeidealCD [OF R.is_cring notprime] by blast
@@ -726,13 +725,13 @@
apply (rule domain.intro, rule is_cring)
apply (rule domain_axioms.intro)
proof (rule ccontr, simp)
- interpret primeideal ["{\<zero>}" "R"] by (rule pi)
+ interpret primeideal "{\<zero>}" "R" by (rule pi)
assume "\<one> = \<zero>"
hence "carrier R = {\<zero>}" by (rule one_zeroD)
from this[symmetric] and I_notcarr
show "False" by simp
next
- interpret primeideal ["{\<zero>}" "R"] by (rule pi)
+ interpret primeideal "{\<zero>}" "R" by (rule pi)
fix a b
assume ab: "a \<otimes> b = \<zero>"
and carr: "a \<in> carrier R" "b \<in> carrier R"
@@ -771,7 +770,7 @@
assumes acarr: "a \<in> carrier R"
shows "ideal {x\<in>carrier R. a \<otimes> x \<in> I} R"
proof -
- interpret cring [R] by fact
+ interpret cring R by fact
show ?thesis apply (rule idealI)
apply (rule cring.axioms[OF is_cring])
apply (rule subgroup.intro)
@@ -812,7 +811,7 @@
assumes "maximalideal I R"
shows "primeideal I R"
proof -
- interpret maximalideal [I R] by fact
+ interpret maximalideal I R by fact
show ?thesis apply (rule ccontr)
apply (rule primeidealCE)
apply (rule is_cring)
@@ -855,7 +854,7 @@
have "\<one> \<notin> J" unfolding J_def by fast
hence Jncarr: "J \<noteq> carrier R" by fast
- interpret ideal ["J" "R"] by (rule idealJ)
+ interpret ideal J R by (rule idealJ)
have "J = I \<or> J = carrier R"
apply (intro I_maximal)
@@ -932,7 +931,7 @@
fix I
assume a: "I \<in> {I. ideal I R}"
with this
- interpret ideal ["I" "R"] by simp
+ interpret ideal I R by simp
show "I \<in> {{\<zero>}, carrier R}"
proof (cases "\<exists>a. a \<in> I - {\<zero>}")
@@ -1019,7 +1018,7 @@
fix J
assume Jn0: "J \<noteq> {\<zero>}"
and idealJ: "ideal J R"
- interpret ideal ["J" "R"] by (rule idealJ)
+ interpret ideal J R by (rule idealJ)
have "{\<zero>} \<subseteq> J" by (rule ccontr, simp)
from zeromax and idealJ and this and a_subset
have "J = {\<zero>} \<or> J = carrier R" by (rule maximalideal.I_maximal)
--- a/src/HOL/Algebra/IntRing.thy Tue Dec 16 15:09:37 2008 +0100
+++ b/src/HOL/Algebra/IntRing.thy Tue Dec 16 21:10:53 2008 +0100
@@ -1,6 +1,5 @@
(*
Title: HOL/Algebra/IntRing.thy
- Id: $Id$
Author: Stephan Hohe, TU Muenchen
*)
@@ -97,7 +96,7 @@
interpretation needs to be done as early as possible --- that is,
with as few assumptions as possible. *}
-interpretation int: monoid ["\<Z>"]
+interpretation int!: monoid \<Z>
where "carrier \<Z> = UNIV"
and "mult \<Z> x y = x * y"
and "one \<Z> = 1"
@@ -105,7 +104,7 @@
proof -
-- "Specification"
show "monoid \<Z>" proof qed (auto simp: int_ring_def)
- then interpret int: monoid ["\<Z>"] .
+ then interpret int!: monoid \<Z> .
-- "Carrier"
show "carrier \<Z> = UNIV" by (simp add: int_ring_def)
@@ -117,12 +116,12 @@
show "pow \<Z> x n = x^n" by (induct n) (simp, simp add: int_ring_def)+
qed
-interpretation int: comm_monoid ["\<Z>"]
+interpretation int!: comm_monoid \<Z>
where "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
proof -
-- "Specification"
show "comm_monoid \<Z>" proof qed (auto simp: int_ring_def)
- then interpret int: comm_monoid ["\<Z>"] .
+ then interpret int!: comm_monoid \<Z> .
-- "Operations"
{ fix x y have "mult \<Z> x y = x * y" by (simp add: int_ring_def) }
@@ -140,14 +139,14 @@
qed
qed
-interpretation int: abelian_monoid ["\<Z>"]
+interpretation int!: abelian_monoid \<Z>
where "zero \<Z> = 0"
and "add \<Z> x y = x + y"
and "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
proof -
-- "Specification"
show "abelian_monoid \<Z>" proof qed (auto simp: int_ring_def)
- then interpret int: abelian_monoid ["\<Z>"] .
+ then interpret int!: abelian_monoid \<Z> .
-- "Operations"
{ fix x y show "add \<Z> x y = x + y" by (simp add: int_ring_def) }
@@ -165,7 +164,7 @@
qed
qed
-interpretation int: abelian_group ["\<Z>"]
+interpretation int!: abelian_group \<Z>
where "a_inv \<Z> x = - x"
and "a_minus \<Z> x y = x - y"
proof -
@@ -175,7 +174,7 @@
show "!!x. x \<in> carrier \<Z> ==> EX y : carrier \<Z>. y \<oplus>\<^bsub>\<Z>\<^esub> x = \<zero>\<^bsub>\<Z>\<^esub>"
by (simp add: int_ring_def) arith
qed (auto simp: int_ring_def)
- then interpret int: abelian_group ["\<Z>"] .
+ then interpret int!: abelian_group \<Z> .
-- "Operations"
{ fix x y have "add \<Z> x y = x + y" by (simp add: int_ring_def) }
@@ -188,7 +187,7 @@
show "a_minus \<Z> x y = x - y" by (simp add: int.minus_eq add a_inv)
qed
-interpretation int: "domain" ["\<Z>"]
+interpretation int!: "domain" \<Z>
proof qed (auto simp: int_ring_def left_distrib right_distrib)
@@ -204,8 +203,8 @@
"(True ==> PROP R) == PROP R"
by simp_all
-interpretation int (* FIXME [unfolded UNIV] *) :
- partial_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
+interpretation int! (* FIXME [unfolded UNIV] *) :
+ partial_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
where "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
and "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
and "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
@@ -220,8 +219,8 @@
by (simp add: lless_def) auto
qed
-interpretation int (* FIXME [unfolded UNIV] *) :
- lattice ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
+interpretation int! (* FIXME [unfolded UNIV] *) :
+ lattice "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
where "join (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = max x y"
and "meet (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = min x y"
proof -
@@ -233,7 +232,7 @@
apply (simp add: greatest_def Lower_def)
apply arith
done
- then interpret int: lattice ["?Z"] .
+ then interpret int!: lattice "?Z" .
show "join ?Z x y = max x y"
apply (rule int.joinI)
apply (simp_all add: least_def Upper_def)
@@ -246,8 +245,8 @@
done
qed
-interpretation int (* [unfolded UNIV] *) :
- total_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
+interpretation int! (* [unfolded UNIV] *) :
+ total_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
proof qed clarsimp
@@ -404,7 +403,7 @@
assumes zmods: "ZMod m a = ZMod m b"
shows "a mod m = b mod m"
proof -
- interpret ideal ["Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>] by (rule int.genideal_ideal, fast)
+ interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z> by (rule int.genideal_ideal, fast)
from zmods
have "b \<in> ZMod m a"
unfolding ZMod_def
@@ -428,7 +427,7 @@
lemma ZMod_mod:
shows "ZMod m a = ZMod m (a mod m)"
proof -
- interpret ideal ["Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>] by (rule int.genideal_ideal, fast)
+ interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z> by (rule int.genideal_ideal, fast)
show ?thesis
unfolding ZMod_def
apply (rule a_repr_independence'[symmetric])
--- a/src/HOL/Algebra/Lattice.thy Tue Dec 16 15:09:37 2008 +0100
+++ b/src/HOL/Algebra/Lattice.thy Tue Dec 16 21:10:53 2008 +0100
@@ -1,6 +1,5 @@
(*
Title: HOL/Algebra/Lattice.thy
- Id: $Id$
Author: Clemens Ballarin, started 7 November 2003
Copyright: Clemens Ballarin
@@ -16,7 +15,7 @@
record 'a gorder = "'a eq_object" +
le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
-locale weak_partial_order = equivalence L +
+locale weak_partial_order = equivalence L for L (structure) +
assumes le_refl [intro, simp]:
"x \<in> carrier L ==> x \<sqsubseteq> x"
and weak_le_anti_sym [intro]:
@@ -920,7 +919,7 @@
text {* Total orders are lattices. *}
-interpretation weak_total_order < weak_lattice
+sublocale weak_total_order < weak_lattice
proof
fix x y
assume L: "x \<in> carrier L" "y \<in> carrier L"
@@ -1126,14 +1125,14 @@
assumes sup_of_two_exists:
"[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
-interpretation upper_semilattice < weak_upper_semilattice
+sublocale upper_semilattice < weak_upper_semilattice
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
+sublocale lower_semilattice < weak_lower_semilattice
proof qed (rule inf_of_two_exists)
locale lattice = upper_semilattice + lower_semilattice
@@ -1184,7 +1183,7 @@
locale total_order = partial_order +
assumes total_order_total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
-interpretation total_order < weak_total_order
+sublocale total_order < weak_total_order
proof qed (rule total_order_total)
text {* Introduction rule: the usual definition of total order *}
@@ -1196,7 +1195,7 @@
text {* Total orders are lattices. *}
-interpretation total_order < lattice
+sublocale total_order < lattice
proof qed (auto intro: sup_of_two_exists inf_of_two_exists)
@@ -1208,7 +1207,7 @@
and inf_exists:
"[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
-interpretation complete_lattice < weak_complete_lattice
+sublocale complete_lattice < weak_complete_lattice
proof qed (auto intro: sup_exists inf_exists)
text {* Introduction rule: the usual definition of complete lattice *}
--- a/src/HOL/Algebra/Module.thy Tue Dec 16 15:09:37 2008 +0100
+++ b/src/HOL/Algebra/Module.thy Tue Dec 16 21:10:53 2008 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Algebra/Module.thy
- ID: $Id$
Author: Clemens Ballarin, started 15 April 2003
Copyright: Clemens Ballarin
*)
@@ -14,7 +13,7 @@
record ('a, 'b) module = "'b ring" +
smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)
-locale module = cring R + abelian_group M +
+locale module = R: cring + M: abelian_group M for M (structure) +
assumes smult_closed [simp, intro]:
"[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> x \<in> carrier M"
and smult_l_distr:
@@ -29,7 +28,7 @@
and smult_one [simp]:
"x \<in> carrier M ==> \<one> \<odot>\<^bsub>M\<^esub> x = x"
-locale algebra = module R M + cring M +
+locale algebra = module + cring M +
assumes smult_assoc2:
"[| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
(a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> y)"
--- a/src/HOL/Algebra/QuotRing.thy Tue Dec 16 15:09:37 2008 +0100
+++ b/src/HOL/Algebra/QuotRing.thy Tue Dec 16 21:10:53 2008 +0100
@@ -1,6 +1,5 @@
(*
Title: HOL/Algebra/QuotRing.thy
- Id: $Id$
Author: Stephan Hohe
*)
@@ -158,7 +157,7 @@
assumes "cring R"
shows "cring (R Quot I)"
proof -
- interpret cring [R] by fact
+ interpret cring R by fact
show ?thesis apply (intro cring.intro comm_monoid.intro comm_monoid_axioms.intro)
apply (rule quotient_is_ring)
apply (rule ring.axioms[OF quotient_is_ring])
@@ -173,7 +172,7 @@
assumes "cring R"
shows "ring_hom_cring R (R Quot I) (op +> I)"
proof -
- interpret cring [R] by fact
+ interpret cring R by fact
show ?thesis apply (rule ring_hom_cringI)
apply (rule rcos_ring_hom_ring)
apply (rule R.is_cring)
@@ -244,7 +243,7 @@
assumes "cring R"
shows "field (R Quot I)"
proof -
- interpret cring [R] by fact
+ interpret cring R by fact
show ?thesis apply (intro cring.cring_fieldI2)
apply (rule quotient_is_cring, rule is_cring)
defer 1
--- a/src/HOL/Algebra/Ring.thy Tue Dec 16 15:09:37 2008 +0100
+++ b/src/HOL/Algebra/Ring.thy Tue Dec 16 21:10:53 2008 +0100
@@ -1,6 +1,5 @@
(*
Title: The algebraic hierarchy of rings
- Id: $Id$
Author: Clemens Ballarin, started 9 December 1996
Copyright: Clemens Ballarin
*)
@@ -187,7 +186,7 @@
assumes cg: "comm_group \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
shows "abelian_group G"
proof -
- interpret comm_group ["\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"]
+ interpret comm_group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
by (rule cg)
show "abelian_group G" ..
qed
@@ -360,7 +359,7 @@
subsection {* Rings: Basic Definitions *}
-locale ring = abelian_group R + monoid R +
+locale ring = abelian_group R + monoid R for R (structure) +
assumes l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
and r_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
@@ -585,8 +584,8 @@
assumes RS: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier S" "d \<in> carrier S"
shows "a \<oplus> \<ominus> (a \<oplus> \<ominus> b) = b & c \<otimes>\<^bsub>S\<^esub> d = d \<otimes>\<^bsub>S\<^esub> c"
proof -
- interpret ring [R] by fact
- interpret cring [S] by fact
+ interpret ring R by fact
+ interpret cring S by fact
ML_val {* Algebra.print_structures @{context} *}
from RS show ?thesis by algebra
qed
@@ -597,7 +596,7 @@
assumes R: "a \<in> carrier R" "b \<in> carrier R"
shows "a \<ominus> (a \<ominus> b) = b"
proof -
- interpret ring [R] by fact
+ interpret ring R by fact
from R show ?thesis by algebra
qed
@@ -771,7 +770,8 @@
shows "h \<in> ring_hom R S ==> h \<one> = \<one>\<^bsub>S\<^esub>"
by (simp add: ring_hom_def)
-locale ring_hom_cring = cring R + cring S +
+locale ring_hom_cring = R: cring R + S: cring S
+ for R (structure) and S (structure) +
fixes h
assumes homh [simp, intro]: "h \<in> ring_hom R S"
notes hom_closed [simp, intro] = ring_hom_closed [OF homh]
--- a/src/HOL/Algebra/RingHom.thy Tue Dec 16 15:09:37 2008 +0100
+++ b/src/HOL/Algebra/RingHom.thy Tue Dec 16 21:10:53 2008 +0100
@@ -1,6 +1,5 @@
(*
Title: HOL/Algebra/RingHom.thy
- Id: $Id$
Author: Stephan Hohe, TU Muenchen
*)
@@ -11,15 +10,16 @@
section {* Homomorphisms of Non-Commutative Rings *}
text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *}
-locale ring_hom_ring = ring R + ring S + var h +
+locale ring_hom_ring = R: ring R + S: ring S +
+ fixes h
assumes homh: "h \<in> ring_hom R S"
notes hom_mult [simp] = ring_hom_mult [OF homh]
and hom_one [simp] = ring_hom_one [OF homh]
-interpretation ring_hom_cring \<subseteq> ring_hom_ring
+sublocale ring_hom_cring \<subseteq> ring_hom_ring
proof qed (rule homh)
-interpretation ring_hom_ring \<subseteq> abelian_group_hom R S
+sublocale ring_hom_ring \<subseteq> abelian_group_hom R S
apply (rule abelian_group_homI)
apply (rule R.is_abelian_group)
apply (rule S.is_abelian_group)
@@ -44,8 +44,8 @@
and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
shows "ring_hom_ring R S h"
proof -
- interpret ring [R] by fact
- interpret ring [S] by fact
+ interpret ring R by fact
+ interpret ring S by fact
show ?thesis apply unfold_locales
apply (unfold ring_hom_def, safe)
apply (simp add: hom_closed Pi_def)
@@ -60,8 +60,8 @@
assumes h: "h \<in> ring_hom R S"
shows "ring_hom_ring R S h"
proof -
- interpret R: ring [R] by fact
- interpret S: ring [S] by fact
+ interpret R!: ring R by fact
+ interpret S!: ring S by fact
show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
apply (rule R.is_ring)
apply (rule S.is_ring)
@@ -76,9 +76,9 @@
and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
shows "ring_hom_ring R S h"
proof -
- interpret abelian_group_hom [R S h] by fact
- interpret R: ring [R] by fact
- interpret S: ring [S] by fact
+ interpret abelian_group_hom R S h by fact
+ interpret R!: ring R by fact
+ interpret S!: ring S by fact
show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring)
apply (insert group_hom.homh[OF a_group_hom])
apply (unfold hom_def ring_hom_def, simp)
@@ -92,9 +92,9 @@
assumes "ring_hom_ring R S h" "cring R" "cring S"
shows "ring_hom_cring R S h"
proof -
- interpret ring_hom_ring [R S h] by fact
- interpret R: cring [R] by fact
- interpret S: cring [S] by fact
+ interpret ring_hom_ring R S h by fact
+ interpret R!: cring R by fact
+ interpret S!: cring S by fact
show ?thesis by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro)
(rule R.is_cring, rule S.is_cring, rule homh)
qed
@@ -124,7 +124,7 @@
and xrcos: "x \<in> a_kernel R S h +> a"
shows "h x = h a"
proof -
- interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal)
+ interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
from xrcos
have "\<exists>i \<in> a_kernel R S h. x = i \<oplus> a" by (simp add: a_r_coset_defs)
@@ -152,7 +152,7 @@
and hx: "h x = h a"
shows "x \<in> a_kernel R S h +> a"
proof -
- interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal)
+ interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
note carr = acarr xcarr
note hcarr = acarr[THEN hom_closed] xcarr[THEN hom_closed]
@@ -180,7 +180,7 @@
apply rule defer 1
apply clarsimp defer 1
proof
- interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal)
+ interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
fix x
assume xrcos: "x \<in> a_kernel R S h +> a"
@@ -193,7 +193,7 @@
from xcarr and this
show "x \<in> {x \<in> carrier R. h x = h a}" by fast
next
- interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal)
+ interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
fix x
assume xcarr: "x \<in> carrier R"
--- a/src/HOL/Algebra/UnivPoly.thy Tue Dec 16 15:09:37 2008 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy Tue Dec 16 21:10:53 2008 +0100
@@ -1,6 +1,5 @@
(*
Title: HOL/Algebra/UnivPoly.thy
- Id: $Id$
Author: Clemens Ballarin, started 9 December 1996
Copyright: Clemens Ballarin
@@ -180,12 +179,12 @@
locale UP_cring = UP + cring R
-interpretation UP_cring < UP_ring
+sublocale UP_cring < UP_ring
by (rule P_def) intro_locales
locale UP_domain = UP + "domain" R
-interpretation UP_domain < UP_cring
+sublocale UP_domain < UP_cring
by (rule P_def) intro_locales
context UP
@@ -458,8 +457,8 @@
end
-interpretation UP_ring < ring P using UP_ring .
-interpretation UP_cring < cring P using UP_cring .
+sublocale UP_ring < ring P using UP_ring .
+sublocale UP_cring < cring P using UP_cring .
subsection {* Polynomials Form an Algebra *}
@@ -508,7 +507,7 @@
"algebra R P" by (auto intro!: algebraI R.cring UP_cring UP_smult_l_distr UP_smult_r_distr
UP_smult_assoc1 UP_smult_assoc2)
-interpretation UP_cring < algebra R P using UP_algebra .
+sublocale UP_cring < algebra R P using UP_algebra .
subsection {* Further Lemmas Involving Monomials *}
@@ -1085,7 +1084,7 @@
Interpretation of theorems from @{term domain}.
*}
-interpretation UP_domain < "domain" P
+sublocale UP_domain < "domain" P
by intro_locales (rule domain.axioms UP_domain)+
@@ -1350,7 +1349,7 @@
text {* Interpretation of ring homomorphism lemmas. *}
-interpretation UP_univ_prop < ring_hom_cring P S Eval
+sublocale UP_univ_prop < ring_hom_cring P S Eval
apply (unfold Eval_def)
apply intro_locales
apply (rule ring_hom_cring.axioms)
@@ -1391,7 +1390,7 @@
assumes R: "r \<in> carrier R" and S: "s \<in> carrier S"
shows "eval R S h s (monom P r n) = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n"
proof -
- interpret UP_univ_prop [R S h P s _]
+ interpret UP_univ_prop R S h P s "eval R S h s"
using UP_pre_univ_prop_axioms P_def R S
by (auto intro: UP_univ_prop.intro UP_univ_prop_axioms.intro)
from R
@@ -1428,8 +1427,8 @@
and P: "p \<in> carrier P" and S: "s \<in> carrier S"
shows "Phi p = Psi p"
proof -
- interpret ring_hom_cring [P S Phi] by fact
- interpret ring_hom_cring [P S Psi] by fact
+ interpret ring_hom_cring P S Phi by fact
+ interpret ring_hom_cring P S Psi by fact
have "Phi p =
Phi (\<Oplus>\<^bsub>P \<^esub>i \<in> {..deg R p}. monom P (coeff P p i) 0 \<otimes>\<^bsub>P\<^esub> monom P \<one> 1 (^)\<^bsub>P\<^esub> i)"
by (simp add: up_repr P monom_mult [THEN sym] monom_pow del: monom_mult)
@@ -1772,9 +1771,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] proof qed 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"] proof qed (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"
@@ -1819,7 +1818,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] proof qed 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"
@@ -1885,7 +1884,7 @@
"UP INTEG"} globally.
*}
-interpretation INTEG: UP_pre_univ_prop [INTEG INTEG id]
+interpretation INTEG!: UP_pre_univ_prop INTEG INTEG id
using INTEG_id_eval by simp_all
lemma INTEG_closed [intro, simp]:
--- a/src/HOLCF/Algebraic.thy Tue Dec 16 15:09:37 2008 +0100
+++ b/src/HOLCF/Algebraic.thy Tue Dec 16 21:10:53 2008 +0100
@@ -1,5 +1,4 @@
(* Title: HOLCF/Algebraic.thy
- ID: $Id$
Author: Brian Huffman
*)
@@ -161,7 +160,7 @@
assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x"
shows "pre_deflation (d oo f)"
proof
- interpret d: finite_deflation [d] by fact
+ interpret d: finite_deflation d by fact
fix x
show "\<And>x. (d oo f)\<cdot>x \<sqsubseteq> x"
by (simp, rule trans_less [OF d.less f])
@@ -174,9 +173,9 @@
assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x"
shows "eventual (\<lambda>n. iterate n\<cdot>(d oo f))\<cdot>x = x \<longleftrightarrow> d\<cdot>x = x \<and> f\<cdot>x = x"
proof -
- interpret d: finite_deflation [d] by fact
+ interpret d: finite_deflation d by fact
let ?e = "d oo f"
- interpret e: pre_deflation ["d oo f"]
+ interpret e: pre_deflation "d oo f"
using `finite_deflation d` f
by (rule pre_deflation_d_f)
let ?g = "eventual (\<lambda>n. iterate n\<cdot>?e)"
@@ -216,7 +215,7 @@
lemma finite_deflation_Rep_fin_defl: "finite_deflation (Rep_fin_defl d)"
using Rep_fin_defl by simp
-interpretation Rep_fin_defl: finite_deflation ["Rep_fin_defl d"]
+interpretation Rep_fin_defl!: finite_deflation "Rep_fin_defl d"
by (rule finite_deflation_Rep_fin_defl)
lemma fin_defl_lessI:
@@ -321,7 +320,7 @@
apply (rule Rep_fin_defl.compact)
done
-interpretation fin_defl: basis_take [sq_le fd_take]
+interpretation fin_defl!: basis_take sq_le fd_take
apply default
apply (rule fd_take_less)
apply (rule fd_take_idem)
@@ -371,8 +370,8 @@
unfolding alg_defl_principal_def
by (simp add: Abs_alg_defl_inverse sq_le.ideal_principal)
-interpretation alg_defl:
- ideal_completion [sq_le fd_take alg_defl_principal Rep_alg_defl]
+interpretation alg_defl!:
+ ideal_completion sq_le fd_take alg_defl_principal Rep_alg_defl
apply default
apply (rule ideal_Rep_alg_defl)
apply (erule Rep_alg_defl_lub)
@@ -462,7 +461,7 @@
apply (rule finite_deflation_Rep_fin_defl)
done
-interpretation cast: deflation ["cast\<cdot>d"]
+interpretation cast!: deflation "cast\<cdot>d"
by (rule deflation_cast)
lemma "cast\<cdot>(\<Squnion>i. alg_defl_principal (Abs_fin_defl (approx i)))\<cdot>x = x"
@@ -486,7 +485,7 @@
constrains e :: "'a::profinite \<rightarrow> 'b::profinite"
shows "\<exists>d. cast\<cdot>d = e oo p"
proof
- interpret ep_pair [e p] by fact
+ interpret ep_pair e p by fact
let ?a = "\<lambda>i. e oo approx i oo p"
have a: "\<And>i. finite_deflation (?a i)"
apply (rule finite_deflation_e_d_p)
@@ -517,7 +516,7 @@
"\<And>i. finite_deflation (a i)"
"(\<Squnion>i. a i) = ID"
proof
- interpret ep_pair [e p] by fact
+ interpret ep_pair e p by fact
let ?a = "\<lambda>i. p oo cast\<cdot>(approx i\<cdot>d) oo e"
show "\<And>i. finite_deflation (?a i)"
apply (rule finite_deflation_p_d_e)
--- a/src/HOLCF/Bifinite.thy Tue Dec 16 15:09:37 2008 +0100
+++ b/src/HOLCF/Bifinite.thy Tue Dec 16 21:10:53 2008 +0100
@@ -1,5 +1,4 @@
(* Title: HOLCF/Bifinite.thy
- ID: $Id$
Author: Brian Huffman
*)
@@ -38,7 +37,7 @@
by (rule finite_fixes_approx)
qed
-interpretation approx: finite_deflation ["approx i"]
+interpretation approx!: finite_deflation "approx i"
by (rule finite_deflation_approx)
lemma (in deflation) deflation: "deflation d" ..
--- a/src/HOLCF/CompactBasis.thy Tue Dec 16 15:09:37 2008 +0100
+++ b/src/HOLCF/CompactBasis.thy Tue Dec 16 21:10:53 2008 +0100
@@ -1,5 +1,4 @@
(* Title: HOLCF/CompactBasis.thy
- ID: $Id$
Author: Brian Huffman
*)
@@ -47,8 +46,8 @@
lemmas approx_Rep_compact_basis = Rep_compact_take [symmetric]
-interpretation compact_basis:
- basis_take [sq_le compact_take]
+interpretation compact_basis!:
+ basis_take sq_le compact_take
proof
fix n :: nat and a :: "'a compact_basis"
show "compact_take n a \<sqsubseteq> a"
@@ -93,8 +92,8 @@
approximants :: "'a \<Rightarrow> 'a compact_basis set" where
"approximants = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})"
-interpretation compact_basis:
- ideal_completion [sq_le compact_take Rep_compact_basis approximants]
+interpretation compact_basis!:
+ ideal_completion sq_le compact_take Rep_compact_basis approximants
proof
fix w :: 'a
show "preorder.ideal sq_le (approximants w)"
@@ -245,7 +244,7 @@
assumes "ab_semigroup_idem_mult f"
shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
proof -
- interpret ab_semigroup_idem_mult [f] by fact
+ interpret ab_semigroup_idem_mult f by fact
show ?thesis unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2)
qed
--- a/src/HOLCF/Completion.thy Tue Dec 16 15:09:37 2008 +0100
+++ b/src/HOLCF/Completion.thy Tue Dec 16 21:10:53 2008 +0100
@@ -1,5 +1,4 @@
(* Title: HOLCF/Completion.thy
- ID: $Id$
Author: Brian Huffman
*)
@@ -157,7 +156,7 @@
end
-interpretation sq_le: preorder ["sq_le :: 'a::po \<Rightarrow> 'a \<Rightarrow> bool"]
+interpretation sq_le!: preorder "sq_le :: 'a::po \<Rightarrow> 'a \<Rightarrow> bool"
apply unfold_locales
apply (rule refl_less)
apply (erule (1) trans_less)
--- a/src/HOLCF/ConvexPD.thy Tue Dec 16 15:09:37 2008 +0100
+++ b/src/HOLCF/ConvexPD.thy Tue Dec 16 21:10:53 2008 +0100
@@ -1,5 +1,4 @@
(* Title: HOLCF/ConvexPD.thy
- ID: $Id$
Author: Brian Huffman
*)
@@ -21,7 +20,7 @@
lemma convex_le_trans: "\<lbrakk>t \<le>\<natural> u; u \<le>\<natural> v\<rbrakk> \<Longrightarrow> t \<le>\<natural> v"
unfolding convex_le_def by (fast intro: upper_le_trans lower_le_trans)
-interpretation convex_le: preorder [convex_le]
+interpretation convex_le!: preorder convex_le
by (rule preorder.intro, rule convex_le_refl, rule convex_le_trans)
lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<natural> t"
@@ -179,8 +178,8 @@
unfolding convex_principal_def
by (simp add: Abs_convex_pd_inverse convex_le.ideal_principal)
-interpretation convex_pd:
- ideal_completion [convex_le pd_take convex_principal Rep_convex_pd]
+interpretation convex_pd!:
+ ideal_completion convex_le pd_take convex_principal Rep_convex_pd
apply unfold_locales
apply (rule pd_take_convex_le)
apply (rule pd_take_idem)
@@ -297,7 +296,7 @@
apply (simp add: PDPlus_absorb)
done
-interpretation aci_convex_plus: ab_semigroup_idem_mult ["op +\<natural>"]
+interpretation aci_convex_plus!: ab_semigroup_idem_mult "op +\<natural>"
by unfold_locales
(rule convex_plus_assoc convex_plus_commute convex_plus_absorb)+
--- a/src/HOLCF/Deflation.thy Tue Dec 16 15:09:37 2008 +0100
+++ b/src/HOLCF/Deflation.thy Tue Dec 16 21:10:53 2008 +0100
@@ -1,5 +1,4 @@
(* Title: HOLCF/Deflation.thy
- ID: $Id$
Author: Brian Huffman
*)
@@ -82,10 +81,10 @@
assumes "deflation g"
shows "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>(g\<cdot>x) = f\<cdot>x"
proof (rule antisym_less)
- interpret g: deflation [g] by fact
+ interpret g: deflation g by fact
from g.less show "f\<cdot>(g\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
next
- interpret f: deflation [f] by fact
+ interpret f: deflation f by fact
assume "f \<sqsubseteq> g" hence "f\<cdot>x \<sqsubseteq> g\<cdot>x" by (rule monofun_cfun_fun)
hence "f\<cdot>(f\<cdot>x) \<sqsubseteq> f\<cdot>(g\<cdot>x)" by (rule monofun_cfun_arg)
also have "f\<cdot>(f\<cdot>x) = f\<cdot>x" by (rule f.idem)
@@ -220,7 +219,7 @@
assumes "deflation d"
shows "deflation (e oo d oo p)"
proof
- interpret deflation [d] by fact
+ interpret deflation d by fact
fix x :: 'b
show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
by (simp add: idem)
@@ -232,7 +231,7 @@
assumes "finite_deflation d"
shows "finite_deflation (e oo d oo p)"
proof
- interpret finite_deflation [d] by fact
+ interpret finite_deflation d by fact
fix x :: 'b
show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
by (simp add: idem)
@@ -251,7 +250,7 @@
assumes d: "\<And>x. d\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>x)"
shows "deflation (p oo d oo e)"
proof -
- interpret d: deflation [d] by fact
+ interpret d: deflation d by fact
{
fix x
have "d\<cdot>(e\<cdot>x) \<sqsubseteq> e\<cdot>x"
@@ -288,7 +287,7 @@
assumes d: "\<And>x. d\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>x)"
shows "finite_deflation (p oo d oo e)"
proof -
- interpret d: finite_deflation [d] by fact
+ interpret d: finite_deflation d by fact
show ?thesis
proof (intro_locales)
have "deflation d" ..
@@ -317,8 +316,8 @@
assumes "ep_pair e1 p" and "ep_pair e2 p"
shows "e1 \<sqsubseteq> e2"
proof (rule less_cfun_ext)
- interpret e1: ep_pair [e1 p] by fact
- interpret e2: ep_pair [e2 p] by fact
+ interpret e1: ep_pair e1 p by fact
+ interpret e2: ep_pair e2 p by fact
fix x
have "e1\<cdot>(p\<cdot>(e2\<cdot>x)) \<sqsubseteq> e2\<cdot>x"
by (rule e1.e_p_less)
@@ -334,8 +333,8 @@
assumes "ep_pair e p1" and "ep_pair e p2"
shows "p1 \<sqsubseteq> p2"
proof (rule less_cfun_ext)
- interpret p1: ep_pair [e p1] by fact
- interpret p2: ep_pair [e p2] by fact
+ interpret p1: ep_pair e p1 by fact
+ interpret p2: ep_pair e p2 by fact
fix x
have "e\<cdot>(p1\<cdot>x) \<sqsubseteq> x"
by (rule p1.e_p_less)
@@ -358,8 +357,8 @@
assumes "ep_pair e1 p1" and "ep_pair e2 p2"
shows "ep_pair (e2 oo e1) (p1 oo p2)"
proof
- interpret ep1: ep_pair [e1 p1] by fact
- interpret ep2: ep_pair [e2 p2] by fact
+ interpret ep1: ep_pair e1 p1 by fact
+ interpret ep2: ep_pair e2 p2 by fact
fix x y
show "(p1 oo p2)\<cdot>((e2 oo e1)\<cdot>x) = x"
by simp
--- a/src/HOLCF/LowerPD.thy Tue Dec 16 15:09:37 2008 +0100
+++ b/src/HOLCF/LowerPD.thy Tue Dec 16 21:10:53 2008 +0100
@@ -1,5 +1,4 @@
(* Title: HOLCF/LowerPD.thy
- ID: $Id$
Author: Brian Huffman
*)
@@ -27,7 +26,7 @@
apply (erule (1) trans_less)
done
-interpretation lower_le: preorder [lower_le]
+interpretation lower_le!: preorder lower_le
by (rule preorder.intro, rule lower_le_refl, rule lower_le_trans)
lemma lower_le_minimal [simp]: "PDUnit compact_bot \<le>\<flat> t"
@@ -134,8 +133,8 @@
unfolding lower_principal_def
by (simp add: Abs_lower_pd_inverse lower_le.ideal_principal)
-interpretation lower_pd:
- ideal_completion [lower_le pd_take lower_principal Rep_lower_pd]
+interpretation lower_pd!:
+ ideal_completion lower_le pd_take lower_principal Rep_lower_pd
apply unfold_locales
apply (rule pd_take_lower_le)
apply (rule pd_take_idem)
@@ -251,7 +250,7 @@
apply (simp add: PDPlus_absorb)
done
-interpretation aci_lower_plus: ab_semigroup_idem_mult ["op +\<flat>"]
+interpretation aci_lower_plus!: ab_semigroup_idem_mult "op +\<flat>"
by unfold_locales
(rule lower_plus_assoc lower_plus_commute lower_plus_absorb)+
--- a/src/HOLCF/Universal.thy Tue Dec 16 15:09:37 2008 +0100
+++ b/src/HOLCF/Universal.thy Tue Dec 16 21:10:53 2008 +0100
@@ -1,5 +1,4 @@
(* Title: HOLCF/Universal.thy
- ID: $Id$
Author: Brian Huffman
*)
@@ -227,13 +226,13 @@
apply (simp add: ubasis_take_same)
done
-interpretation udom: preorder [ubasis_le]
+interpretation udom!: preorder ubasis_le
apply default
apply (rule ubasis_le_refl)
apply (erule (1) ubasis_le_trans)
done
-interpretation udom: basis_take [ubasis_le ubasis_take]
+interpretation udom!: basis_take ubasis_le ubasis_take
apply default
apply (rule ubasis_take_less)
apply (rule ubasis_take_idem)
@@ -282,8 +281,8 @@
unfolding udom_principal_def
by (simp add: Abs_udom_inverse udom.ideal_principal)
-interpretation udom:
- ideal_completion [ubasis_le ubasis_take udom_principal Rep_udom]
+interpretation udom!:
+ ideal_completion ubasis_le ubasis_take udom_principal Rep_udom
apply unfold_locales
apply (rule ideal_Rep_udom)
apply (erule Rep_udom_lub)
--- a/src/HOLCF/UpperPD.thy Tue Dec 16 15:09:37 2008 +0100
+++ b/src/HOLCF/UpperPD.thy Tue Dec 16 21:10:53 2008 +0100
@@ -1,5 +1,4 @@
(* Title: HOLCF/UpperPD.thy
- ID: $Id$
Author: Brian Huffman
*)
@@ -27,7 +26,7 @@
apply (erule (1) trans_less)
done
-interpretation upper_le: preorder [upper_le]
+interpretation upper_le!: preorder upper_le
by (rule preorder.intro, rule upper_le_refl, rule upper_le_trans)
lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<sharp> t"
@@ -132,8 +131,8 @@
unfolding upper_principal_def
by (simp add: Abs_upper_pd_inverse upper_le.ideal_principal)
-interpretation upper_pd:
- ideal_completion [upper_le pd_take upper_principal Rep_upper_pd]
+interpretation upper_pd!:
+ ideal_completion upper_le pd_take upper_principal Rep_upper_pd
apply unfold_locales
apply (rule pd_take_upper_le)
apply (rule pd_take_idem)
@@ -249,7 +248,7 @@
apply (simp add: PDPlus_absorb)
done
-interpretation aci_upper_plus: ab_semigroup_idem_mult ["op +\<sharp>"]
+interpretation aci_upper_plus!: ab_semigroup_idem_mult "op +\<sharp>"
by unfold_locales
(rule upper_plus_assoc upper_plus_commute upper_plus_absorb)+