More porting to new locales.
authorballarin
Tue Dec 16 21:10:53 2008 +0100 (2008-12-16)
changeset 29237e90d9d51106b
parent 29236 51526dd8da8e
child 29238 eddc08920f4a
More porting to new locales.
src/HOL/Algebra/AbelCoset.thy
src/HOL/Algebra/Congruence.thy
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/Divisibility.thy
src/HOL/Algebra/FiniteProduct.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Ideal.thy
src/HOL/Algebra/IntRing.thy
src/HOL/Algebra/Lattice.thy
src/HOL/Algebra/Module.thy
src/HOL/Algebra/QuotRing.thy
src/HOL/Algebra/Ring.thy
src/HOL/Algebra/RingHom.thy
src/HOL/Algebra/UnivPoly.thy
src/HOLCF/Algebraic.thy
src/HOLCF/Bifinite.thy
src/HOLCF/CompactBasis.thy
src/HOLCF/Completion.thy
src/HOLCF/ConvexPD.thy
src/HOLCF/Deflation.thy
src/HOLCF/LowerPD.thy
src/HOLCF/Universal.thy
src/HOLCF/UpperPD.thy
     1.1 --- a/src/HOL/Algebra/AbelCoset.thy	Tue Dec 16 15:09:37 2008 +0100
     1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Tue Dec 16 21:10:53 2008 +0100
     1.3 @@ -1,6 +1,5 @@
     1.4  (*
     1.5    Title:     HOL/Algebra/AbelCoset.thy
     1.6 -  Id:        $Id$
     1.7    Author:    Stephan Hohe, TU Muenchen
     1.8  *)
     1.9  
    1.10 @@ -52,7 +51,9 @@
    1.11    "a_kernel G H h \<equiv> kernel \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
    1.12                                \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
    1.13  
    1.14 -locale abelian_group_hom = abelian_group G + abelian_group H + var h +
    1.15 +locale abelian_group_hom = G: abelian_group G + H: abelian_group H
    1.16 +    for G (structure) and H (structure) +
    1.17 +  fixes h
    1.18    assumes a_group_hom: "group_hom (| carrier = carrier G, mult = add G, one = zero G |)
    1.19                                    (| carrier = carrier H, mult = add H, one = zero H |) h"
    1.20  
    1.21 @@ -180,7 +181,8 @@
    1.22  
    1.23  subsubsection {* Subgroups *}
    1.24  
    1.25 -locale additive_subgroup = var H + struct G +
    1.26 +locale additive_subgroup =
    1.27 +  fixes H and G (structure)
    1.28    assumes a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.29  
    1.30  lemma (in additive_subgroup) is_additive_subgroup:
    1.31 @@ -218,7 +220,7 @@
    1.32  
    1.33  text {* Every subgroup of an @{text "abelian_group"} is normal *}
    1.34  
    1.35 -locale abelian_subgroup = additive_subgroup H G + abelian_group G +
    1.36 +locale abelian_subgroup = additive_subgroup + abelian_group G +
    1.37    assumes a_normal: "normal H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.38  
    1.39  lemma (in abelian_subgroup) is_abelian_subgroup:
    1.40 @@ -230,7 +232,7 @@
    1.41        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"
    1.42    shows "abelian_subgroup H G"
    1.43  proof -
    1.44 -  interpret normal ["H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"]
    1.45 +  interpret normal "H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.46    by (rule a_normal)
    1.47  
    1.48    show "abelian_subgroup H G"
    1.49 @@ -243,9 +245,9 @@
    1.50        and a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.51    shows "abelian_subgroup H G"
    1.52  proof -
    1.53 -  interpret comm_group ["\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"]
    1.54 +  interpret comm_group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.55    by (rule a_comm_group)
    1.56 -  interpret subgroup ["H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"]
    1.57 +  interpret subgroup "H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.58    by (rule a_subgroup)
    1.59  
    1.60    show "abelian_subgroup H G"
    1.61 @@ -538,8 +540,8 @@
    1.62                                    (| carrier = carrier H, mult = add H, one = zero H |) h"
    1.63    shows "abelian_group_hom G H h"
    1.64  proof -
    1.65 -  interpret G: abelian_group [G] by fact
    1.66 -  interpret H: abelian_group [H] by fact
    1.67 +  interpret G!: abelian_group G by fact
    1.68 +  interpret H!: abelian_group H by fact
    1.69    show ?thesis apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
    1.70      apply fact
    1.71      apply fact
    1.72 @@ -690,7 +692,7 @@
    1.73    assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
    1.74    shows "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
    1.75  proof -
    1.76 -  interpret G: ring [G] by fact
    1.77 +  interpret G!: ring G by fact
    1.78    from carr
    1.79    have "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)" by (rule a_rcos_module)
    1.80    with carr
     2.1 --- a/src/HOL/Algebra/Congruence.thy	Tue Dec 16 15:09:37 2008 +0100
     2.2 +++ b/src/HOL/Algebra/Congruence.thy	Tue Dec 16 21:10:53 2008 +0100
     2.3 @@ -1,6 +1,5 @@
     2.4  (*
     2.5    Title:  Algebra/Congruence.thy
     2.6 -  Id:     $Id$
     2.7    Author: Clemens Ballarin, started 3 January 2008
     2.8    Copyright: Clemens Ballarin
     2.9  *)
     3.1 --- a/src/HOL/Algebra/Coset.thy	Tue Dec 16 15:09:37 2008 +0100
     3.2 +++ b/src/HOL/Algebra/Coset.thy	Tue Dec 16 21:10:53 2008 +0100
     3.3 @@ -1,5 +1,4 @@
     3.4  (*  Title:      HOL/Algebra/Coset.thy
     3.5 -    ID:         $Id$
     3.6      Author:     Florian Kammueller, with new proofs by L C Paulson, and
     3.7                  Stephan Hohe
     3.8  *)
     3.9 @@ -114,7 +113,7 @@
    3.10        and repr:  "H #> x = H #> y"
    3.11    shows "y \<in> H #> x"
    3.12  proof -
    3.13 -  interpret subgroup [H G] by fact
    3.14 +  interpret subgroup H G by fact
    3.15    show ?thesis  apply (subst repr)
    3.16    apply (intro rcos_self)
    3.17     apply (rule ycarr)
    3.18 @@ -129,7 +128,7 @@
    3.19      and a': "a' \<in> H #> a"
    3.20    shows "a' \<in> carrier G"
    3.21  proof -
    3.22 -  interpret group [G] by fact
    3.23 +  interpret group G by fact
    3.24    from subset and acarr
    3.25    have "H #> a \<subseteq> carrier G" by (rule r_coset_subset_G)
    3.26    from this and a'
    3.27 @@ -142,7 +141,7 @@
    3.28    assumes hH: "h \<in> H"
    3.29    shows "H #> h = H"
    3.30  proof -
    3.31 -  interpret group [G] by fact
    3.32 +  interpret group G by fact
    3.33    show ?thesis apply (unfold r_coset_def)
    3.34      apply rule
    3.35      apply rule
    3.36 @@ -173,7 +172,7 @@
    3.37        and x'cos: "x' \<in> H #> x"
    3.38    shows "(x' \<otimes> inv x) \<in> H"
    3.39  proof -
    3.40 -  interpret group [G] by fact
    3.41 +  interpret group G by fact
    3.42    from xcarr x'cos
    3.43        have x'carr: "x' \<in> carrier G"
    3.44        by (rule elemrcos_carrier[OF is_group])
    3.45 @@ -213,7 +212,7 @@
    3.46        and xixH: "(x' \<otimes> inv x) \<in> H"
    3.47    shows "x' \<in> H #> x"
    3.48  proof -
    3.49 -  interpret group [G] by fact
    3.50 +  interpret group G by fact
    3.51    from xixH
    3.52        have "\<exists>h\<in>H. x' \<otimes> (inv x) = h" by fast
    3.53    from this
    3.54 @@ -244,7 +243,7 @@
    3.55    assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
    3.56    shows "(x' \<in> H #> x) = (x' \<otimes> inv x \<in> H)"
    3.57  proof -
    3.58 -  interpret group [G] by fact
    3.59 +  interpret group G by fact
    3.60    show ?thesis proof  assume "x' \<in> H #> x"
    3.61      from this and carr
    3.62      show "x' \<otimes> inv x \<in> H"
    3.63 @@ -263,7 +262,7 @@
    3.64    assumes XH: "X \<in> rcosets H"
    3.65    shows "X \<subseteq> carrier G"
    3.66  proof -
    3.67 -  interpret group [G] by fact
    3.68 +  interpret group G by fact
    3.69    from XH have "\<exists>x\<in> carrier G. X = H #> x"
    3.70        unfolding RCOSETS_def
    3.71        by fast
    3.72 @@ -348,7 +347,7 @@
    3.73        and xixH: "(inv x \<otimes> x') \<in> H"
    3.74    shows "x' \<in> x <# H"
    3.75  proof -
    3.76 -  interpret group [G] by fact
    3.77 +  interpret group G by fact
    3.78    from xixH
    3.79        have "\<exists>h\<in>H. (inv x) \<otimes> x' = h" by fast
    3.80    from this
    3.81 @@ -600,7 +599,7 @@
    3.82     assumes "group G"
    3.83     shows "equiv (carrier G) (rcong H)"
    3.84  proof -
    3.85 -  interpret group [G] by fact
    3.86 +  interpret group G by fact
    3.87    show ?thesis
    3.88    proof (intro equiv.intro)
    3.89      show "refl (carrier G) (rcong H)"
    3.90 @@ -647,7 +646,7 @@
    3.91    assumes a: "a \<in> carrier G"
    3.92    shows "a <# H = rcong H `` {a}"
    3.93  proof -
    3.94 -  interpret group [G] by fact
    3.95 +  interpret group G by fact
    3.96    show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a ) 
    3.97  qed
    3.98  
    3.99 @@ -658,7 +657,7 @@
   3.100    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"
   3.101    shows "hb \<otimes> a \<in> (\<Union>h\<in>H. {h \<otimes> b})"
   3.102  proof -
   3.103 -  interpret subgroup [H G] by fact
   3.104 +  interpret subgroup H G by fact
   3.105    from p show ?thesis apply (rule_tac UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"])
   3.106      apply (simp add: )
   3.107      apply (simp add: m_assoc transpose_inv)
   3.108 @@ -670,7 +669,7 @@
   3.109    assumes p: "a \<in> rcosets H" "b \<in> rcosets H" "a\<noteq>b"
   3.110    shows "a \<inter> b = {}"
   3.111  proof -
   3.112 -  interpret subgroup [H G] by fact
   3.113 +  interpret subgroup H G by fact
   3.114    from p show ?thesis apply (simp add: RCOSETS_def r_coset_def)
   3.115      apply (blast intro: rcos_equation prems sym)
   3.116      done
   3.117 @@ -760,7 +759,7 @@
   3.118    assumes "subgroup H G"
   3.119    shows "\<Union>(rcosets H) = carrier G"
   3.120  proof -
   3.121 -  interpret subgroup [H G] by fact
   3.122 +  interpret subgroup H G by fact
   3.123    show ?thesis
   3.124      apply (rule equalityI)
   3.125      apply (force simp add: RCOSETS_def r_coset_def)
   3.126 @@ -847,7 +846,7 @@
   3.127    assumes "group G"
   3.128    shows "H \<in> rcosets H"
   3.129  proof -
   3.130 -  interpret group [G] by fact
   3.131 +  interpret group G by fact
   3.132    from _ subgroup_axioms have "H #> \<one> = H"
   3.133      by (rule coset_join2) auto
   3.134    then show ?thesis
     4.1 --- a/src/HOL/Algebra/Divisibility.thy	Tue Dec 16 15:09:37 2008 +0100
     4.2 +++ b/src/HOL/Algebra/Divisibility.thy	Tue Dec 16 21:10:53 2008 +0100
     4.3 @@ -1,6 +1,5 @@
     4.4  (*
     4.5    Title:     Divisibility in monoids and rings
     4.6 -  Id:        $Id$
     4.7    Author:    Clemens Ballarin, started 18 July 2008
     4.8  
     4.9  Based on work by Stephan Hohe.
    4.10 @@ -32,7 +31,7 @@
    4.11    "monoid_cancel G"
    4.12    ..
    4.13  
    4.14 -interpretation group \<subseteq> monoid_cancel
    4.15 +sublocale group \<subseteq> monoid_cancel
    4.16    proof qed simp+
    4.17  
    4.18  
    4.19 @@ -45,7 +44,7 @@
    4.20            "\<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"
    4.21    shows "comm_monoid_cancel G"
    4.22  proof -
    4.23 -  interpret comm_monoid [G] by fact
    4.24 +  interpret comm_monoid G by fact
    4.25    show "comm_monoid_cancel G"
    4.26      apply unfold_locales
    4.27      apply (subgoal_tac "a \<otimes> c = b \<otimes> c")
    4.28 @@ -59,7 +58,7 @@
    4.29    "comm_monoid_cancel G"
    4.30    by intro_locales
    4.31  
    4.32 -interpretation comm_group \<subseteq> comm_monoid_cancel
    4.33 +sublocale comm_group \<subseteq> comm_monoid_cancel
    4.34    ..
    4.35  
    4.36  
    4.37 @@ -755,7 +754,7 @@
    4.38  using pf
    4.39  unfolding properfactor_lless
    4.40  proof -
    4.41 -  interpret weak_partial_order ["division_rel G"] ..
    4.42 +  interpret weak_partial_order "division_rel G" ..
    4.43    from x'x
    4.44         have "x' .=\<^bsub>division_rel G\<^esub> x" by simp
    4.45    also assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y"
    4.46 @@ -771,7 +770,7 @@
    4.47  using pf
    4.48  unfolding properfactor_lless
    4.49  proof -
    4.50 -  interpret weak_partial_order ["division_rel G"] ..
    4.51 +  interpret weak_partial_order "division_rel G" ..
    4.52    assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y"
    4.53    also from yy'
    4.54         have "y .=\<^bsub>division_rel G\<^esub> y'" by simp
    4.55 @@ -2916,7 +2915,7 @@
    4.56  lemma (in gcd_condition_monoid) division_weak_lower_semilattice [simp]:
    4.57    shows "weak_lower_semilattice (division_rel G)"
    4.58  proof -
    4.59 -  interpret weak_partial_order ["division_rel G"] ..
    4.60 +  interpret weak_partial_order "division_rel G" ..
    4.61    show ?thesis
    4.62    apply (unfold_locales, simp_all)
    4.63    proof -
    4.64 @@ -2941,7 +2940,7 @@
    4.65    shows "a' gcdof b c"
    4.66  proof -
    4.67    note carr = a'carr carr'
    4.68 -  interpret weak_lower_semilattice ["division_rel G"] by simp
    4.69 +  interpret weak_lower_semilattice "division_rel G" by simp
    4.70    have "a' \<in> carrier G \<and> a' gcdof b c"
    4.71      apply (simp add: gcdof_greatestLower carr')
    4.72      apply (subst greatest_Lower_cong_l[of _ a])
    4.73 @@ -2958,7 +2957,7 @@
    4.74    assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
    4.75    shows "somegcd G a b \<in> carrier G"
    4.76  proof -
    4.77 -  interpret weak_lower_semilattice ["division_rel G"] by simp
    4.78 +  interpret weak_lower_semilattice "division_rel G" by simp
    4.79    show ?thesis
    4.80      apply (simp add: somegcd_meet[OF carr])
    4.81      apply (rule meet_closed[simplified], fact+)
    4.82 @@ -2969,7 +2968,7 @@
    4.83    assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
    4.84    shows "(somegcd G a b) gcdof a b"
    4.85  proof -
    4.86 -  interpret weak_lower_semilattice ["division_rel G"] by simp
    4.87 +  interpret weak_lower_semilattice "division_rel G" by simp
    4.88    from carr
    4.89    have "somegcd G a b \<in> carrier G \<and> (somegcd G a b) gcdof a b"
    4.90      apply (subst gcdof_greatestLower, simp, simp)
    4.91 @@ -2983,7 +2982,7 @@
    4.92    assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
    4.93    shows "\<exists>x\<in>carrier G. x = somegcd G a b"
    4.94  proof -
    4.95 -  interpret weak_lower_semilattice ["division_rel G"] by simp
    4.96 +  interpret weak_lower_semilattice "division_rel G" by simp
    4.97    show ?thesis
    4.98      apply (simp add: somegcd_meet[OF carr])
    4.99      apply (rule meet_closed[simplified], fact+)
   4.100 @@ -2994,7 +2993,7 @@
   4.101    assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   4.102    shows "(somegcd G a b) divides a"
   4.103  proof -
   4.104 -  interpret weak_lower_semilattice ["division_rel G"] by simp
   4.105 +  interpret weak_lower_semilattice "division_rel G" by simp
   4.106    show ?thesis
   4.107      apply (simp add: somegcd_meet[OF carr])
   4.108      apply (rule meet_left[simplified], fact+)
   4.109 @@ -3005,7 +3004,7 @@
   4.110    assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   4.111    shows "(somegcd G a b) divides b"
   4.112  proof -
   4.113 -  interpret weak_lower_semilattice ["division_rel G"] by simp
   4.114 +  interpret weak_lower_semilattice "division_rel G" by simp
   4.115    show ?thesis
   4.116      apply (simp add: somegcd_meet[OF carr])
   4.117      apply (rule meet_right[simplified], fact+)
   4.118 @@ -3017,7 +3016,7 @@
   4.119      and L: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
   4.120    shows "z divides (somegcd G x y)"
   4.121  proof -
   4.122 -  interpret weak_lower_semilattice ["division_rel G"] by simp
   4.123 +  interpret weak_lower_semilattice "division_rel G" by simp
   4.124    show ?thesis
   4.125      apply (simp add: somegcd_meet L)
   4.126      apply (rule meet_le[simplified], fact+)
   4.127 @@ -3029,7 +3028,7 @@
   4.128      and carr: "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"
   4.129    shows "somegcd G x y \<sim> somegcd G x' y"
   4.130  proof -
   4.131 -  interpret weak_lower_semilattice ["division_rel G"] by simp
   4.132 +  interpret weak_lower_semilattice "division_rel G" by simp
   4.133    show ?thesis
   4.134      apply (simp add: somegcd_meet carr)
   4.135      apply (rule meet_cong_l[simplified], fact+)
   4.136 @@ -3041,7 +3040,7 @@
   4.137      and yy': "y \<sim> y'"
   4.138    shows "somegcd G x y \<sim> somegcd G x y'"
   4.139  proof -
   4.140 -  interpret weak_lower_semilattice ["division_rel G"] by simp
   4.141 +  interpret weak_lower_semilattice "division_rel G" by simp
   4.142    show ?thesis
   4.143      apply (simp add: somegcd_meet carr)
   4.144      apply (rule meet_cong_r[simplified], fact+)
   4.145 @@ -3092,7 +3091,7 @@
   4.146    assumes "finite A"  "A \<subseteq> carrier G"  "A \<noteq> {}"
   4.147    shows "\<exists>x\<in> carrier G. x = SomeGcd G A"
   4.148  proof -
   4.149 -  interpret weak_lower_semilattice ["division_rel G"] by simp
   4.150 +  interpret weak_lower_semilattice "division_rel G" by simp
   4.151    show ?thesis
   4.152      apply (simp add: SomeGcd_def)
   4.153      apply (rule finite_inf_closed[simplified], fact+)
   4.154 @@ -3103,7 +3102,7 @@
   4.155    assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   4.156    shows "somegcd G (somegcd G a b) c \<sim> somegcd G a (somegcd G b c)"
   4.157  proof -
   4.158 -  interpret weak_lower_semilattice ["division_rel G"] by simp
   4.159 +  interpret weak_lower_semilattice "division_rel G" by simp
   4.160    show ?thesis
   4.161      apply (subst (2 3) somegcd_meet, (simp add: carr)+)
   4.162      apply (simp add: somegcd_meet carr)
   4.163 @@ -3313,7 +3312,7 @@
   4.164    qed
   4.165  qed
   4.166  
   4.167 -interpretation gcd_condition_monoid \<subseteq> primeness_condition_monoid
   4.168 +sublocale gcd_condition_monoid \<subseteq> primeness_condition_monoid
   4.169    by (rule primeness_condition)
   4.170  
   4.171  
   4.172 @@ -3832,7 +3831,7 @@
   4.173    with fca fcb show ?thesis by simp
   4.174  qed
   4.175  
   4.176 -interpretation factorial_monoid \<subseteq> divisor_chain_condition_monoid
   4.177 +sublocale factorial_monoid \<subseteq> divisor_chain_condition_monoid
   4.178  apply unfold_locales
   4.179  apply (rule wfUNIVI)
   4.180  apply (rule measure_induct[of "factorcount G"])
   4.181 @@ -3854,7 +3853,7 @@
   4.182    done
   4.183  qed
   4.184  
   4.185 -interpretation factorial_monoid \<subseteq> primeness_condition_monoid
   4.186 +sublocale factorial_monoid \<subseteq> primeness_condition_monoid
   4.187    proof qed (rule irreducible_is_prime)
   4.188  
   4.189  
   4.190 @@ -3866,13 +3865,13 @@
   4.191    shows "gcd_condition_monoid G"
   4.192    proof qed (rule gcdof_exists)
   4.193  
   4.194 -interpretation factorial_monoid \<subseteq> gcd_condition_monoid
   4.195 +sublocale factorial_monoid \<subseteq> gcd_condition_monoid
   4.196    proof qed (rule gcdof_exists)
   4.197  
   4.198  lemma (in factorial_monoid) division_weak_lattice [simp]:
   4.199    shows "weak_lattice (division_rel G)"
   4.200  proof -
   4.201 -  interpret weak_lower_semilattice ["division_rel G"] by simp
   4.202 +  interpret weak_lower_semilattice "division_rel G" by simp
   4.203  
   4.204    show "weak_lattice (division_rel G)"
   4.205    apply (unfold_locales, simp_all)
   4.206 @@ -3902,14 +3901,14 @@
   4.207  proof clarify
   4.208    assume dcc: "divisor_chain_condition_monoid G"
   4.209       and pc: "primeness_condition_monoid G"
   4.210 -  interpret divisor_chain_condition_monoid ["G"] by (rule dcc)
   4.211 -  interpret primeness_condition_monoid ["G"] by (rule pc)
   4.212 +  interpret divisor_chain_condition_monoid "G" by (rule dcc)
   4.213 +  interpret primeness_condition_monoid "G" by (rule pc)
   4.214  
   4.215    show "factorial_monoid G"
   4.216        by (fast intro: factorial_monoidI wfactors_exist wfactors_unique)
   4.217  next
   4.218    assume fm: "factorial_monoid G"
   4.219 -  interpret factorial_monoid ["G"] by (rule fm)
   4.220 +  interpret factorial_monoid "G" by (rule fm)
   4.221    show "divisor_chain_condition_monoid G \<and> primeness_condition_monoid G"
   4.222        by rule unfold_locales
   4.223  qed
   4.224 @@ -3920,13 +3919,13 @@
   4.225  proof clarify
   4.226      assume dcc: "divisor_chain_condition_monoid G"
   4.227       and gc: "gcd_condition_monoid G"
   4.228 -  interpret divisor_chain_condition_monoid ["G"] by (rule dcc)
   4.229 -  interpret gcd_condition_monoid ["G"] by (rule gc)
   4.230 +  interpret divisor_chain_condition_monoid "G" by (rule dcc)
   4.231 +  interpret gcd_condition_monoid "G" by (rule gc)
   4.232    show "factorial_monoid G"
   4.233        by (simp add: factorial_condition_one[symmetric], rule, unfold_locales)
   4.234  next
   4.235    assume fm: "factorial_monoid G"
   4.236 -  interpret factorial_monoid ["G"] by (rule fm)
   4.237 +  interpret factorial_monoid "G" by (rule fm)
   4.238    show "divisor_chain_condition_monoid G \<and> gcd_condition_monoid G"
   4.239        by rule unfold_locales
   4.240  qed
     5.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Tue Dec 16 15:09:37 2008 +0100
     5.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Tue Dec 16 21:10:53 2008 +0100
     5.3 @@ -1,5 +1,4 @@
     5.4  (*  Title:      HOL/Algebra/FiniteProduct.thy
     5.5 -    ID:         $Id$
     5.6      Author:     Clemens Ballarin, started 19 November 2002
     5.7  
     5.8  This file is largely based on HOL/Finite_Set.thy.
     5.9 @@ -519,9 +518,9 @@
    5.10  lemma finprod_singleton:
    5.11    assumes i_in_A: "i \<in> A" and fin_A: "finite A" and f_Pi: "f \<in> A \<rightarrow> carrier G"
    5.12    shows "(\<Otimes>j\<in>A. if i = j then f j else \<one>) = f i"
    5.13 -  using i_in_A G.finprod_insert [of "A - {i}" i "(\<lambda>j. if i = j then f j else \<one>)"]
    5.14 -    fin_A f_Pi G.finprod_one [of "A - {i}"]
    5.15 -    G.finprod_cong [of "A - {i}" "A - {i}" "(\<lambda>j. if i = j then f j else \<one>)" "(\<lambda>i. \<one>)"] 
    5.16 +  using i_in_A finprod_insert [of "A - {i}" i "(\<lambda>j. if i = j then f j else \<one>)"]
    5.17 +    fin_A f_Pi finprod_one [of "A - {i}"]
    5.18 +    finprod_cong [of "A - {i}" "A - {i}" "(\<lambda>j. if i = j then f j else \<one>)" "(\<lambda>i. \<one>)"] 
    5.19    unfolding Pi_def simp_implies_def by (force simp add: insert_absorb)
    5.20  
    5.21  end
     6.1 --- a/src/HOL/Algebra/Group.thy	Tue Dec 16 15:09:37 2008 +0100
     6.2 +++ b/src/HOL/Algebra/Group.thy	Tue Dec 16 21:10:53 2008 +0100
     6.3 @@ -1,6 +1,5 @@
     6.4  (*
     6.5    Title:  HOL/Algebra/Group.thy
     6.6 -  Id:     $Id$
     6.7    Author: Clemens Ballarin, started 4 February 2003
     6.8  
     6.9  Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
    6.10 @@ -425,7 +424,7 @@
    6.11    assumes "group G"
    6.12    shows "group (G\<lparr>carrier := H\<rparr>)"
    6.13  proof -
    6.14 -  interpret group [G] by fact
    6.15 +  interpret group G by fact
    6.16    show ?thesis
    6.17      apply (rule monoid.group_l_invI)
    6.18      apply (unfold_locales) [1]
    6.19 @@ -489,8 +488,8 @@
    6.20    assumes "monoid G" and "monoid H"
    6.21    shows "monoid (G \<times>\<times> H)"
    6.22  proof -
    6.23 -  interpret G: monoid [G] by fact
    6.24 -  interpret H: monoid [H] by fact
    6.25 +  interpret G!: monoid G by fact
    6.26 +  interpret H!: monoid H by fact
    6.27    from assms
    6.28    show ?thesis by (unfold monoid_def DirProd_def, auto) 
    6.29  qed
    6.30 @@ -501,8 +500,8 @@
    6.31    assumes "group G" and "group H"
    6.32    shows "group (G \<times>\<times> H)"
    6.33  proof -
    6.34 -  interpret G: group [G] by fact
    6.35 -  interpret H: group [H] by fact
    6.36 +  interpret G!: group G by fact
    6.37 +  interpret H!: group H by fact
    6.38    show ?thesis by (rule groupI)
    6.39       (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
    6.40             simp add: DirProd_def)
    6.41 @@ -526,9 +525,9 @@
    6.42        and h: "h \<in> carrier H"
    6.43    shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
    6.44  proof -
    6.45 -  interpret G: group [G] by fact
    6.46 -  interpret H: group [H] by fact
    6.47 -  interpret Prod: group ["G \<times>\<times> H"]
    6.48 +  interpret G!: group G by fact
    6.49 +  interpret H!: group H by fact
    6.50 +  interpret Prod!: group "G \<times>\<times> H"
    6.51      by (auto intro: DirProd_group group.intro group.axioms assms)
    6.52    show ?thesis by (simp add: Prod.inv_equality g h)
    6.53  qed
    6.54 @@ -587,7 +586,8 @@
    6.55  
    6.56  text{*Basis for homomorphism proofs: we assume two groups @{term G} and
    6.57    @{term H}, with a homomorphism @{term h} between them*}
    6.58 -locale group_hom = group G + group H + var h +
    6.59 +locale group_hom = G: group G + H: group H for G (structure) and H (structure) +
    6.60 +  fixes h
    6.61    assumes homh: "h \<in> hom G H"
    6.62    notes hom_mult [simp] = hom_mult [OF homh]
    6.63      and hom_closed [simp] = hom_closed [OF homh]
     7.1 --- a/src/HOL/Algebra/Ideal.thy	Tue Dec 16 15:09:37 2008 +0100
     7.2 +++ b/src/HOL/Algebra/Ideal.thy	Tue Dec 16 21:10:53 2008 +0100
     7.3 @@ -1,6 +1,5 @@
     7.4  (*
     7.5    Title:     HOL/Algebra/CIdeal.thy
     7.6 -  Id:        $Id$
     7.7    Author:    Stephan Hohe, TU Muenchen
     7.8  *)
     7.9  
    7.10 @@ -18,7 +17,7 @@
    7.11    assumes I_l_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
    7.12        and I_r_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
    7.13  
    7.14 -interpretation ideal \<subseteq> abelian_subgroup I R
    7.15 +sublocale ideal \<subseteq> abelian_subgroup I R
    7.16  apply (intro abelian_subgroupI3 abelian_group.intro)
    7.17    apply (rule ideal.axioms, rule ideal_axioms)
    7.18   apply (rule abelian_group.axioms, rule ring.axioms, rule ideal.axioms, rule ideal_axioms)
    7.19 @@ -37,7 +36,7 @@
    7.20        and I_r_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
    7.21    shows "ideal I R"
    7.22  proof -
    7.23 -  interpret ring [R] by fact
    7.24 +  interpret ring R by fact
    7.25    show ?thesis  apply (intro ideal.intro ideal_axioms.intro additive_subgroupI)
    7.26       apply (rule a_subgroup)
    7.27      apply (rule is_ring)
    7.28 @@ -68,7 +67,7 @@
    7.29    assumes generate: "\<exists>i \<in> carrier R. I = Idl {i}"
    7.30    shows "principalideal I R"
    7.31  proof -
    7.32 -  interpret ideal [I R] by fact
    7.33 +  interpret ideal I R by fact
    7.34    show ?thesis  by (intro principalideal.intro principalideal_axioms.intro) (rule is_ideal, rule generate)
    7.35  qed
    7.36  
    7.37 @@ -89,7 +88,7 @@
    7.38       and I_maximal: "\<And>J. \<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> J = I \<or> J = carrier R"
    7.39    shows "maximalideal I R"
    7.40  proof -
    7.41 -  interpret ideal [I R] by fact
    7.42 +  interpret ideal I R by fact
    7.43    show ?thesis by (intro maximalideal.intro maximalideal_axioms.intro)
    7.44      (rule is_ideal, rule I_notcarr, rule I_maximal)
    7.45  qed
    7.46 @@ -112,8 +111,8 @@
    7.47        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"
    7.48    shows "primeideal I R"
    7.49  proof -
    7.50 -  interpret ideal [I R] by fact
    7.51 -  interpret cring [R] by fact
    7.52 +  interpret ideal I R by fact
    7.53 +  interpret cring R by fact
    7.54    show ?thesis by (intro primeideal.intro primeideal_axioms.intro)
    7.55      (rule is_ideal, rule is_cring, rule I_notcarr, rule I_prime)
    7.56  qed
    7.57 @@ -129,7 +128,7 @@
    7.58    shows "primeideal I R"
    7.59  proof -
    7.60    interpret additive_subgroup [I R] by fact
    7.61 -  interpret cring [R] by fact
    7.62 +  interpret cring R by fact
    7.63    show ?thesis apply (intro_locales)
    7.64      apply (intro ideal_axioms.intro)
    7.65      apply (erule (1) I_l_closed)
    7.66 @@ -207,7 +206,7 @@
    7.67    assumes "ideal J R"
    7.68    shows "ideal (I \<inter> J) R"
    7.69  proof -
    7.70 -  interpret ideal [I R] by fact
    7.71 +  interpret ideal I R by fact
    7.72    interpret ideal [J R] by fact
    7.73    show ?thesis
    7.74  apply (intro idealI subgroup.intro)
    7.75 @@ -245,7 +244,7 @@
    7.76    from notempty have "\<exists>I0. I0 \<in> S" by blast
    7.77    from this obtain I0 where I0S: "I0 \<in> S" by auto
    7.78  
    7.79 -  interpret ideal ["I0" "R"] by (rule Sideals[OF I0S])
    7.80 +  interpret ideal I0 R by (rule Sideals[OF I0S])
    7.81  
    7.82    from xI[OF I0S] have "x \<in> I0" .
    7.83    from this and a_subset show "x \<in> carrier R" by fast
    7.84 @@ -258,13 +257,13 @@
    7.85  
    7.86    fix J
    7.87    assume JS: "J \<in> S"
    7.88 -  interpret ideal ["J" "R"] by (rule Sideals[OF JS])
    7.89 +  interpret ideal J R by (rule Sideals[OF JS])
    7.90    from xI[OF JS] and yI[OF JS]
    7.91        show "x \<oplus> y \<in> J" by (rule a_closed)
    7.92  next
    7.93    fix J
    7.94    assume JS: "J \<in> S"
    7.95 -  interpret ideal ["J" "R"] by (rule Sideals[OF JS])
    7.96 +  interpret ideal J R by (rule Sideals[OF JS])
    7.97    show "\<zero> \<in> J" by simp
    7.98  next
    7.99    fix x
   7.100 @@ -273,7 +272,7 @@
   7.101  
   7.102    fix J
   7.103    assume JS: "J \<in> S"
   7.104 -  interpret ideal ["J" "R"] by (rule Sideals[OF JS])
   7.105 +  interpret ideal J R by (rule Sideals[OF JS])
   7.106  
   7.107    from xI[OF JS]
   7.108        show "\<ominus> x \<in> J" by (rule a_inv_closed)
   7.109 @@ -285,7 +284,7 @@
   7.110  
   7.111    fix J
   7.112    assume JS: "J \<in> S"
   7.113 -  interpret ideal ["J" "R"] by (rule Sideals[OF JS])
   7.114 +  interpret ideal J R by (rule Sideals[OF JS])
   7.115  
   7.116    from xI[OF JS] and ycarr
   7.117        show "y \<otimes> x \<in> J" by (rule I_l_closed)
   7.118 @@ -297,7 +296,7 @@
   7.119  
   7.120    fix J
   7.121    assume JS: "J \<in> S"
   7.122 -  interpret ideal ["J" "R"] by (rule Sideals[OF JS])
   7.123 +  interpret ideal J R by (rule Sideals[OF JS])
   7.124  
   7.125    from xI[OF JS] and ycarr
   7.126        show "x \<otimes> y \<in> J" by (rule I_r_closed)
   7.127 @@ -443,7 +442,7 @@
   7.128  lemma (in ring) genideal_one:
   7.129    "Idl {\<one>} = carrier R"
   7.130  proof -
   7.131 -  interpret ideal ["Idl {\<one>}" "R"] by (rule genideal_ideal, fast intro: one_closed)
   7.132 +  interpret ideal "Idl {\<one>}" "R" by (rule genideal_ideal, fast intro: one_closed)
   7.133    show "Idl {\<one>} = carrier R"
   7.134    apply (rule, rule a_subset)
   7.135    apply (simp add: one_imp_carrier genideal_self')
   7.136 @@ -660,7 +659,7 @@
   7.137    assumes "cring R"
   7.138    shows "\<exists>x\<in>I. I = carrier R #> x"
   7.139  proof -
   7.140 -  interpret cring [R] by fact
   7.141 +  interpret cring R by fact
   7.142    from generate
   7.143        obtain i
   7.144          where icarr: "i \<in> carrier R"
   7.145 @@ -693,7 +692,7 @@
   7.146    assumes notprime: "\<not> primeideal I R"
   7.147    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)"
   7.148  proof (rule ccontr, clarsimp)
   7.149 -  interpret cring [R] by fact
   7.150 +  interpret cring R by fact
   7.151    assume InR: "carrier R \<noteq> I"
   7.152       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)"
   7.153    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
   7.154 @@ -713,7 +712,7 @@
   7.155    obtains "carrier R = I"
   7.156      | "\<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"
   7.157  proof -
   7.158 -  interpret R: cring [R] by fact
   7.159 +  interpret R!: cring R by fact
   7.160    assume "carrier R = I ==> thesis"
   7.161      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"
   7.162    then show thesis using primeidealCD [OF R.is_cring notprime] by blast
   7.163 @@ -726,13 +725,13 @@
   7.164  apply (rule domain.intro, rule is_cring)
   7.165  apply (rule domain_axioms.intro)
   7.166  proof (rule ccontr, simp)
   7.167 -  interpret primeideal ["{\<zero>}" "R"] by (rule pi)
   7.168 +  interpret primeideal "{\<zero>}" "R" by (rule pi)
   7.169    assume "\<one> = \<zero>"
   7.170    hence "carrier R = {\<zero>}" by (rule one_zeroD)
   7.171    from this[symmetric] and I_notcarr
   7.172        show "False" by simp
   7.173  next
   7.174 -  interpret primeideal ["{\<zero>}" "R"] by (rule pi)
   7.175 +  interpret primeideal "{\<zero>}" "R" by (rule pi)
   7.176    fix a b
   7.177    assume ab: "a \<otimes> b = \<zero>"
   7.178       and carr: "a \<in> carrier R" "b \<in> carrier R"
   7.179 @@ -771,7 +770,7 @@
   7.180    assumes acarr: "a \<in> carrier R"
   7.181    shows "ideal {x\<in>carrier R. a \<otimes> x \<in> I} R"
   7.182  proof -
   7.183 -  interpret cring [R] by fact
   7.184 +  interpret cring R by fact
   7.185    show ?thesis apply (rule idealI)
   7.186      apply (rule cring.axioms[OF is_cring])
   7.187      apply (rule subgroup.intro)
   7.188 @@ -812,7 +811,7 @@
   7.189    assumes "maximalideal I R"
   7.190    shows "primeideal I R"
   7.191  proof -
   7.192 -  interpret maximalideal [I R] by fact
   7.193 +  interpret maximalideal I R by fact
   7.194    show ?thesis apply (rule ccontr)
   7.195      apply (rule primeidealCE)
   7.196      apply (rule is_cring)
   7.197 @@ -855,7 +854,7 @@
   7.198      have "\<one> \<notin> J" unfolding J_def by fast
   7.199      hence Jncarr: "J \<noteq> carrier R" by fast
   7.200      
   7.201 -    interpret ideal ["J" "R"] by (rule idealJ)
   7.202 +    interpret ideal J R by (rule idealJ)
   7.203      
   7.204      have "J = I \<or> J = carrier R"
   7.205        apply (intro I_maximal)
   7.206 @@ -932,7 +931,7 @@
   7.207    fix I
   7.208    assume a: "I \<in> {I. ideal I R}"
   7.209    with this
   7.210 -      interpret ideal ["I" "R"] by simp
   7.211 +      interpret ideal I R by simp
   7.212  
   7.213    show "I \<in> {{\<zero>}, carrier R}"
   7.214    proof (cases "\<exists>a. a \<in> I - {\<zero>}")
   7.215 @@ -1019,7 +1018,7 @@
   7.216    fix J
   7.217    assume Jn0: "J \<noteq> {\<zero>}"
   7.218       and idealJ: "ideal J R"
   7.219 -  interpret ideal ["J" "R"] by (rule idealJ)
   7.220 +  interpret ideal J R by (rule idealJ)
   7.221    have "{\<zero>} \<subseteq> J" by (rule ccontr, simp)
   7.222    from zeromax and idealJ and this and a_subset
   7.223        have "J = {\<zero>} \<or> J = carrier R" by (rule maximalideal.I_maximal)
     8.1 --- a/src/HOL/Algebra/IntRing.thy	Tue Dec 16 15:09:37 2008 +0100
     8.2 +++ b/src/HOL/Algebra/IntRing.thy	Tue Dec 16 21:10:53 2008 +0100
     8.3 @@ -1,6 +1,5 @@
     8.4  (*
     8.5    Title:     HOL/Algebra/IntRing.thy
     8.6 -  Id:        $Id$
     8.7    Author:    Stephan Hohe, TU Muenchen
     8.8  *)
     8.9  
    8.10 @@ -97,7 +96,7 @@
    8.11    interpretation needs to be done as early as possible --- that is,
    8.12    with as few assumptions as possible. *}
    8.13  
    8.14 -interpretation int: monoid ["\<Z>"]
    8.15 +interpretation int!: monoid \<Z>
    8.16    where "carrier \<Z> = UNIV"
    8.17      and "mult \<Z> x y = x * y"
    8.18      and "one \<Z> = 1"
    8.19 @@ -105,7 +104,7 @@
    8.20  proof -
    8.21    -- "Specification"
    8.22    show "monoid \<Z>" proof qed (auto simp: int_ring_def)
    8.23 -  then interpret int: monoid ["\<Z>"] .
    8.24 +  then interpret int!: monoid \<Z> .
    8.25  
    8.26    -- "Carrier"
    8.27    show "carrier \<Z> = UNIV" by (simp add: int_ring_def)
    8.28 @@ -117,12 +116,12 @@
    8.29    show "pow \<Z> x n = x^n" by (induct n) (simp, simp add: int_ring_def)+
    8.30  qed
    8.31  
    8.32 -interpretation int: comm_monoid ["\<Z>"]
    8.33 +interpretation int!: comm_monoid \<Z>
    8.34    where "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
    8.35  proof -
    8.36    -- "Specification"
    8.37    show "comm_monoid \<Z>" proof qed (auto simp: int_ring_def)
    8.38 -  then interpret int: comm_monoid ["\<Z>"] .
    8.39 +  then interpret int!: comm_monoid \<Z> .
    8.40  
    8.41    -- "Operations"
    8.42    { fix x y have "mult \<Z> x y = x * y" by (simp add: int_ring_def) }
    8.43 @@ -140,14 +139,14 @@
    8.44    qed
    8.45  qed
    8.46  
    8.47 -interpretation int: abelian_monoid ["\<Z>"]
    8.48 +interpretation int!: abelian_monoid \<Z>
    8.49    where "zero \<Z> = 0"
    8.50      and "add \<Z> x y = x + y"
    8.51      and "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
    8.52  proof -
    8.53    -- "Specification"
    8.54    show "abelian_monoid \<Z>" proof qed (auto simp: int_ring_def)
    8.55 -  then interpret int: abelian_monoid ["\<Z>"] .
    8.56 +  then interpret int!: abelian_monoid \<Z> .
    8.57  
    8.58    -- "Operations"
    8.59    { fix x y show "add \<Z> x y = x + y" by (simp add: int_ring_def) }
    8.60 @@ -165,7 +164,7 @@
    8.61    qed
    8.62  qed
    8.63  
    8.64 -interpretation int: abelian_group ["\<Z>"]
    8.65 +interpretation int!: abelian_group \<Z>
    8.66    where "a_inv \<Z> x = - x"
    8.67      and "a_minus \<Z> x y = x - y"
    8.68  proof -
    8.69 @@ -175,7 +174,7 @@
    8.70      show "!!x. x \<in> carrier \<Z> ==> EX y : carrier \<Z>. y \<oplus>\<^bsub>\<Z>\<^esub> x = \<zero>\<^bsub>\<Z>\<^esub>"
    8.71        by (simp add: int_ring_def) arith
    8.72    qed (auto simp: int_ring_def)
    8.73 -  then interpret int: abelian_group ["\<Z>"] .
    8.74 +  then interpret int!: abelian_group \<Z> .
    8.75  
    8.76    -- "Operations"
    8.77    { fix x y have "add \<Z> x y = x + y" by (simp add: int_ring_def) }
    8.78 @@ -188,7 +187,7 @@
    8.79    show "a_minus \<Z> x y = x - y" by (simp add: int.minus_eq add a_inv)
    8.80  qed
    8.81  
    8.82 -interpretation int: "domain" ["\<Z>"]
    8.83 +interpretation int!: "domain" \<Z>
    8.84    proof qed (auto simp: int_ring_def left_distrib right_distrib)
    8.85  
    8.86  
    8.87 @@ -204,8 +203,8 @@
    8.88    "(True ==> PROP R) == PROP R"
    8.89    by simp_all
    8.90  
    8.91 -interpretation int (* FIXME [unfolded UNIV] *) :
    8.92 -  partial_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
    8.93 +interpretation int! (* FIXME [unfolded UNIV] *) :
    8.94 +  partial_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
    8.95    where "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
    8.96      and "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
    8.97      and "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
    8.98 @@ -220,8 +219,8 @@
    8.99      by (simp add: lless_def) auto
   8.100  qed
   8.101  
   8.102 -interpretation int (* FIXME [unfolded UNIV] *) :
   8.103 -  lattice ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
   8.104 +interpretation int! (* FIXME [unfolded UNIV] *) :
   8.105 +  lattice "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
   8.106    where "join (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = max x y"
   8.107      and "meet (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = min x y"
   8.108  proof -
   8.109 @@ -233,7 +232,7 @@
   8.110      apply (simp add: greatest_def Lower_def)
   8.111      apply arith
   8.112      done
   8.113 -  then interpret int: lattice ["?Z"] .
   8.114 +  then interpret int!: lattice "?Z" .
   8.115    show "join ?Z x y = max x y"
   8.116      apply (rule int.joinI)
   8.117      apply (simp_all add: least_def Upper_def)
   8.118 @@ -246,8 +245,8 @@
   8.119      done
   8.120  qed
   8.121  
   8.122 -interpretation int (* [unfolded UNIV] *) :
   8.123 -  total_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
   8.124 +interpretation int! (* [unfolded UNIV] *) :
   8.125 +  total_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
   8.126    proof qed clarsimp
   8.127  
   8.128  
   8.129 @@ -404,7 +403,7 @@
   8.130    assumes zmods: "ZMod m a = ZMod m b"
   8.131    shows "a mod m = b mod m"
   8.132  proof -
   8.133 -  interpret ideal ["Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>] by (rule int.genideal_ideal, fast)
   8.134 +  interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z> by (rule int.genideal_ideal, fast)
   8.135    from zmods
   8.136        have "b \<in> ZMod m a"
   8.137        unfolding ZMod_def
   8.138 @@ -428,7 +427,7 @@
   8.139  lemma ZMod_mod:
   8.140    shows "ZMod m a = ZMod m (a mod m)"
   8.141  proof -
   8.142 -  interpret ideal ["Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>] by (rule int.genideal_ideal, fast)
   8.143 +  interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z> by (rule int.genideal_ideal, fast)
   8.144    show ?thesis
   8.145        unfolding ZMod_def
   8.146    apply (rule a_repr_independence'[symmetric])
     9.1 --- a/src/HOL/Algebra/Lattice.thy	Tue Dec 16 15:09:37 2008 +0100
     9.2 +++ b/src/HOL/Algebra/Lattice.thy	Tue Dec 16 21:10:53 2008 +0100
     9.3 @@ -1,6 +1,5 @@
     9.4  (*
     9.5    Title:     HOL/Algebra/Lattice.thy
     9.6 -  Id:        $Id$
     9.7    Author:    Clemens Ballarin, started 7 November 2003
     9.8    Copyright: Clemens Ballarin
     9.9  
    9.10 @@ -16,7 +15,7 @@
    9.11  record 'a gorder = "'a eq_object" +
    9.12    le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
    9.13  
    9.14 -locale weak_partial_order = equivalence L +
    9.15 +locale weak_partial_order = equivalence L for L (structure) +
    9.16    assumes le_refl [intro, simp]:
    9.17        "x \<in> carrier L ==> x \<sqsubseteq> x"
    9.18      and weak_le_anti_sym [intro]:
    9.19 @@ -920,7 +919,7 @@
    9.20  
    9.21  text {* Total orders are lattices. *}
    9.22  
    9.23 -interpretation weak_total_order < weak_lattice
    9.24 +sublocale weak_total_order < weak_lattice
    9.25  proof
    9.26    fix x y
    9.27    assume L: "x \<in> carrier L"  "y \<in> carrier L"
    9.28 @@ -1126,14 +1125,14 @@
    9.29    assumes sup_of_two_exists:
    9.30      "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
    9.31  
    9.32 -interpretation upper_semilattice < weak_upper_semilattice
    9.33 +sublocale upper_semilattice < weak_upper_semilattice
    9.34    proof qed (rule sup_of_two_exists)
    9.35  
    9.36  locale lower_semilattice = partial_order +
    9.37    assumes inf_of_two_exists:
    9.38      "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
    9.39  
    9.40 -interpretation lower_semilattice < weak_lower_semilattice
    9.41 +sublocale lower_semilattice < weak_lower_semilattice
    9.42    proof qed (rule inf_of_two_exists)
    9.43  
    9.44  locale lattice = upper_semilattice + lower_semilattice
    9.45 @@ -1184,7 +1183,7 @@
    9.46  locale total_order = partial_order +
    9.47    assumes total_order_total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
    9.48  
    9.49 -interpretation total_order < weak_total_order
    9.50 +sublocale total_order < weak_total_order
    9.51    proof qed (rule total_order_total)
    9.52  
    9.53  text {* Introduction rule: the usual definition of total order *}
    9.54 @@ -1196,7 +1195,7 @@
    9.55  
    9.56  text {* Total orders are lattices. *}
    9.57  
    9.58 -interpretation total_order < lattice
    9.59 +sublocale total_order < lattice
    9.60    proof qed (auto intro: sup_of_two_exists inf_of_two_exists)
    9.61  
    9.62  
    9.63 @@ -1208,7 +1207,7 @@
    9.64      and inf_exists:
    9.65      "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
    9.66  
    9.67 -interpretation complete_lattice < weak_complete_lattice
    9.68 +sublocale complete_lattice < weak_complete_lattice
    9.69    proof qed (auto intro: sup_exists inf_exists)
    9.70  
    9.71  text {* Introduction rule: the usual definition of complete lattice *}
    10.1 --- a/src/HOL/Algebra/Module.thy	Tue Dec 16 15:09:37 2008 +0100
    10.2 +++ b/src/HOL/Algebra/Module.thy	Tue Dec 16 21:10:53 2008 +0100
    10.3 @@ -1,5 +1,4 @@
    10.4  (*  Title:      HOL/Algebra/Module.thy
    10.5 -    ID:         $Id$
    10.6      Author:     Clemens Ballarin, started 15 April 2003
    10.7      Copyright:  Clemens Ballarin
    10.8  *)
    10.9 @@ -14,7 +13,7 @@
   10.10  record ('a, 'b) module = "'b ring" +
   10.11    smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)
   10.12  
   10.13 -locale module = cring R + abelian_group M +
   10.14 +locale module = R: cring + M: abelian_group M for M (structure) +
   10.15    assumes smult_closed [simp, intro]:
   10.16        "[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> x \<in> carrier M"
   10.17      and smult_l_distr:
   10.18 @@ -29,7 +28,7 @@
   10.19      and smult_one [simp]:
   10.20        "x \<in> carrier M ==> \<one> \<odot>\<^bsub>M\<^esub> x = x"
   10.21  
   10.22 -locale algebra = module R M + cring M +
   10.23 +locale algebra = module + cring M +
   10.24    assumes smult_assoc2:
   10.25        "[| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
   10.26        (a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> y)"
    11.1 --- a/src/HOL/Algebra/QuotRing.thy	Tue Dec 16 15:09:37 2008 +0100
    11.2 +++ b/src/HOL/Algebra/QuotRing.thy	Tue Dec 16 21:10:53 2008 +0100
    11.3 @@ -1,6 +1,5 @@
    11.4  (*
    11.5    Title:     HOL/Algebra/QuotRing.thy
    11.6 -  Id:        $Id$
    11.7    Author:    Stephan Hohe
    11.8  *)
    11.9  
   11.10 @@ -158,7 +157,7 @@
   11.11    assumes "cring R"
   11.12    shows "cring (R Quot I)"
   11.13  proof -
   11.14 -  interpret cring [R] by fact
   11.15 +  interpret cring R by fact
   11.16    show ?thesis apply (intro cring.intro comm_monoid.intro comm_monoid_axioms.intro)
   11.17    apply (rule quotient_is_ring)
   11.18   apply (rule ring.axioms[OF quotient_is_ring])
   11.19 @@ -173,7 +172,7 @@
   11.20    assumes "cring R"
   11.21    shows "ring_hom_cring R (R Quot I) (op +> I)"
   11.22  proof -
   11.23 -  interpret cring [R] by fact
   11.24 +  interpret cring R by fact
   11.25    show ?thesis apply (rule ring_hom_cringI)
   11.26    apply (rule rcos_ring_hom_ring)
   11.27   apply (rule R.is_cring)
   11.28 @@ -244,7 +243,7 @@
   11.29    assumes "cring R"
   11.30    shows "field (R Quot I)"
   11.31  proof -
   11.32 -  interpret cring [R] by fact
   11.33 +  interpret cring R by fact
   11.34    show ?thesis apply (intro cring.cring_fieldI2)
   11.35    apply (rule quotient_is_cring, rule is_cring)
   11.36   defer 1
    12.1 --- a/src/HOL/Algebra/Ring.thy	Tue Dec 16 15:09:37 2008 +0100
    12.2 +++ b/src/HOL/Algebra/Ring.thy	Tue Dec 16 21:10:53 2008 +0100
    12.3 @@ -1,6 +1,5 @@
    12.4  (*
    12.5    Title:     The algebraic hierarchy of rings
    12.6 -  Id:        $Id$
    12.7    Author:    Clemens Ballarin, started 9 December 1996
    12.8    Copyright: Clemens Ballarin
    12.9  *)
   12.10 @@ -187,7 +186,7 @@
   12.11    assumes cg: "comm_group \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
   12.12    shows "abelian_group G"
   12.13  proof -
   12.14 -  interpret comm_group ["\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"]
   12.15 +  interpret comm_group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
   12.16      by (rule cg)
   12.17    show "abelian_group G" ..
   12.18  qed
   12.19 @@ -360,7 +359,7 @@
   12.20  
   12.21  subsection {* Rings: Basic Definitions *}
   12.22  
   12.23 -locale ring = abelian_group R + monoid R +
   12.24 +locale ring = abelian_group R + monoid R for R (structure) +
   12.25    assumes l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
   12.26        ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
   12.27      and r_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
   12.28 @@ -585,8 +584,8 @@
   12.29    assumes RS: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier S" "d \<in> carrier S"
   12.30    shows "a \<oplus> \<ominus> (a \<oplus> \<ominus> b) = b & c \<otimes>\<^bsub>S\<^esub> d = d \<otimes>\<^bsub>S\<^esub> c"
   12.31  proof -
   12.32 -  interpret ring [R] by fact
   12.33 -  interpret cring [S] by fact
   12.34 +  interpret ring R by fact
   12.35 +  interpret cring S by fact
   12.36  ML_val {* Algebra.print_structures @{context} *}
   12.37    from RS show ?thesis by algebra
   12.38  qed
   12.39 @@ -597,7 +596,7 @@
   12.40    assumes R: "a \<in> carrier R" "b \<in> carrier R"
   12.41    shows "a \<ominus> (a \<ominus> b) = b"
   12.42  proof -
   12.43 -  interpret ring [R] by fact
   12.44 +  interpret ring R by fact
   12.45    from R show ?thesis by algebra
   12.46  qed
   12.47  
   12.48 @@ -771,7 +770,8 @@
   12.49    shows "h \<in> ring_hom R S ==> h \<one> = \<one>\<^bsub>S\<^esub>"
   12.50    by (simp add: ring_hom_def)
   12.51  
   12.52 -locale ring_hom_cring = cring R + cring S +
   12.53 +locale ring_hom_cring = R: cring R + S: cring S
   12.54 +    for R (structure) and S (structure) +
   12.55    fixes h
   12.56    assumes homh [simp, intro]: "h \<in> ring_hom R S"
   12.57    notes hom_closed [simp, intro] = ring_hom_closed [OF homh]
    13.1 --- a/src/HOL/Algebra/RingHom.thy	Tue Dec 16 15:09:37 2008 +0100
    13.2 +++ b/src/HOL/Algebra/RingHom.thy	Tue Dec 16 21:10:53 2008 +0100
    13.3 @@ -1,6 +1,5 @@
    13.4  (*
    13.5    Title:     HOL/Algebra/RingHom.thy
    13.6 -  Id:        $Id$
    13.7    Author:    Stephan Hohe, TU Muenchen
    13.8  *)
    13.9  
   13.10 @@ -11,15 +10,16 @@
   13.11  section {* Homomorphisms of Non-Commutative Rings *}
   13.12  
   13.13  text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *}
   13.14 -locale ring_hom_ring = ring R + ring S + var h +
   13.15 +locale ring_hom_ring = R: ring R + S: ring S +
   13.16 +  fixes h
   13.17    assumes homh: "h \<in> ring_hom R S"
   13.18    notes hom_mult [simp] = ring_hom_mult [OF homh]
   13.19      and hom_one [simp] = ring_hom_one [OF homh]
   13.20  
   13.21 -interpretation ring_hom_cring \<subseteq> ring_hom_ring
   13.22 +sublocale ring_hom_cring \<subseteq> ring_hom_ring
   13.23    proof qed (rule homh)
   13.24  
   13.25 -interpretation ring_hom_ring \<subseteq> abelian_group_hom R S
   13.26 +sublocale ring_hom_ring \<subseteq> abelian_group_hom R S
   13.27  apply (rule abelian_group_homI)
   13.28    apply (rule R.is_abelian_group)
   13.29   apply (rule S.is_abelian_group)
   13.30 @@ -44,8 +44,8 @@
   13.31        and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
   13.32    shows "ring_hom_ring R S h"
   13.33  proof -
   13.34 -  interpret ring [R] by fact
   13.35 -  interpret ring [S] by fact
   13.36 +  interpret ring R by fact
   13.37 +  interpret ring S by fact
   13.38    show ?thesis apply unfold_locales
   13.39  apply (unfold ring_hom_def, safe)
   13.40     apply (simp add: hom_closed Pi_def)
   13.41 @@ -60,8 +60,8 @@
   13.42    assumes h: "h \<in> ring_hom R S"
   13.43    shows "ring_hom_ring R S h"
   13.44  proof -
   13.45 -  interpret R: ring [R] by fact
   13.46 -  interpret S: ring [S] by fact
   13.47 +  interpret R!: ring R by fact
   13.48 +  interpret S!: ring S by fact
   13.49    show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
   13.50      apply (rule R.is_ring)
   13.51      apply (rule S.is_ring)
   13.52 @@ -76,9 +76,9 @@
   13.53        and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
   13.54    shows "ring_hom_ring R S h"
   13.55  proof -
   13.56 -  interpret abelian_group_hom [R S h] by fact
   13.57 -  interpret R: ring [R] by fact
   13.58 -  interpret S: ring [S] by fact
   13.59 +  interpret abelian_group_hom R S h by fact
   13.60 +  interpret R!: ring R by fact
   13.61 +  interpret S!: ring S by fact
   13.62    show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring)
   13.63      apply (insert group_hom.homh[OF a_group_hom])
   13.64      apply (unfold hom_def ring_hom_def, simp)
   13.65 @@ -92,9 +92,9 @@
   13.66    assumes "ring_hom_ring R S h" "cring R" "cring S"
   13.67    shows "ring_hom_cring R S h"
   13.68  proof -
   13.69 -  interpret ring_hom_ring [R S h] by fact
   13.70 -  interpret R: cring [R] by fact
   13.71 -  interpret S: cring [S] by fact
   13.72 +  interpret ring_hom_ring R S h by fact
   13.73 +  interpret R!: cring R by fact
   13.74 +  interpret S!: cring S by fact
   13.75    show ?thesis by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro)
   13.76      (rule R.is_cring, rule S.is_cring, rule homh)
   13.77  qed
   13.78 @@ -124,7 +124,7 @@
   13.79        and xrcos: "x \<in> a_kernel R S h +> a"
   13.80    shows "h x = h a"
   13.81  proof -
   13.82 -  interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal)
   13.83 +  interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
   13.84  
   13.85    from xrcos
   13.86        have "\<exists>i \<in> a_kernel R S h. x = i \<oplus> a" by (simp add: a_r_coset_defs)
   13.87 @@ -152,7 +152,7 @@
   13.88        and hx: "h x = h a"
   13.89    shows "x \<in> a_kernel R S h +> a"
   13.90  proof -
   13.91 -  interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal)
   13.92 +  interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
   13.93   
   13.94    note carr = acarr xcarr
   13.95    note hcarr = acarr[THEN hom_closed] xcarr[THEN hom_closed]
   13.96 @@ -180,7 +180,7 @@
   13.97  apply rule defer 1
   13.98  apply clarsimp defer 1
   13.99  proof
  13.100 -  interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal)
  13.101 +  interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
  13.102  
  13.103    fix x
  13.104    assume xrcos: "x \<in> a_kernel R S h +> a"
  13.105 @@ -193,7 +193,7 @@
  13.106    from xcarr and this
  13.107        show "x \<in> {x \<in> carrier R. h x = h a}" by fast
  13.108  next
  13.109 -  interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal)
  13.110 +  interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
  13.111  
  13.112    fix x
  13.113    assume xcarr: "x \<in> carrier R"
    14.1 --- a/src/HOL/Algebra/UnivPoly.thy	Tue Dec 16 15:09:37 2008 +0100
    14.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Tue Dec 16 21:10:53 2008 +0100
    14.3 @@ -1,6 +1,5 @@
    14.4  (*
    14.5    Title:     HOL/Algebra/UnivPoly.thy
    14.6 -  Id:        $Id$
    14.7    Author:    Clemens Ballarin, started 9 December 1996
    14.8    Copyright: Clemens Ballarin
    14.9  
   14.10 @@ -180,12 +179,12 @@
   14.11  
   14.12  locale UP_cring = UP + cring R
   14.13  
   14.14 -interpretation UP_cring < UP_ring
   14.15 +sublocale UP_cring < UP_ring
   14.16    by (rule P_def) intro_locales
   14.17  
   14.18  locale UP_domain = UP + "domain" R
   14.19  
   14.20 -interpretation UP_domain < UP_cring
   14.21 +sublocale UP_domain < UP_cring
   14.22    by (rule P_def) intro_locales
   14.23  
   14.24  context UP
   14.25 @@ -458,8 +457,8 @@
   14.26  
   14.27  end
   14.28  
   14.29 -interpretation UP_ring < ring P using UP_ring .
   14.30 -interpretation UP_cring < cring P using UP_cring .
   14.31 +sublocale UP_ring < ring P using UP_ring .
   14.32 +sublocale UP_cring < cring P using UP_cring .
   14.33  
   14.34  
   14.35  subsection {* Polynomials Form an Algebra *}
   14.36 @@ -508,7 +507,7 @@
   14.37    "algebra R P" by (auto intro!: algebraI R.cring UP_cring UP_smult_l_distr UP_smult_r_distr
   14.38      UP_smult_assoc1 UP_smult_assoc2)
   14.39  
   14.40 -interpretation UP_cring < algebra R P using UP_algebra .
   14.41 +sublocale UP_cring < algebra R P using UP_algebra .
   14.42  
   14.43  
   14.44  subsection {* Further Lemmas Involving Monomials *}
   14.45 @@ -1085,7 +1084,7 @@
   14.46    Interpretation of theorems from @{term domain}.
   14.47  *}
   14.48  
   14.49 -interpretation UP_domain < "domain" P
   14.50 +sublocale UP_domain < "domain" P
   14.51    by intro_locales (rule domain.axioms UP_domain)+
   14.52  
   14.53  
   14.54 @@ -1350,7 +1349,7 @@
   14.55  
   14.56  text {* Interpretation of ring homomorphism lemmas. *}
   14.57  
   14.58 -interpretation UP_univ_prop < ring_hom_cring P S Eval
   14.59 +sublocale UP_univ_prop < ring_hom_cring P S Eval
   14.60    apply (unfold Eval_def)
   14.61    apply intro_locales
   14.62    apply (rule ring_hom_cring.axioms)
   14.63 @@ -1391,7 +1390,7 @@
   14.64    assumes R: "r \<in> carrier R" and S: "s \<in> carrier S"
   14.65    shows "eval R S h s (monom P r n) = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n"
   14.66  proof -
   14.67 -  interpret UP_univ_prop [R S h P s _]
   14.68 +  interpret UP_univ_prop R S h P s "eval R S h s"
   14.69      using UP_pre_univ_prop_axioms P_def R S
   14.70      by (auto intro: UP_univ_prop.intro UP_univ_prop_axioms.intro)
   14.71    from R
   14.72 @@ -1428,8 +1427,8 @@
   14.73      and P: "p \<in> carrier P" and S: "s \<in> carrier S"
   14.74    shows "Phi p = Psi p"
   14.75  proof -
   14.76 -  interpret ring_hom_cring [P S Phi] by fact
   14.77 -  interpret ring_hom_cring [P S Psi] by fact
   14.78 +  interpret ring_hom_cring P S Phi by fact
   14.79 +  interpret ring_hom_cring P S Psi by fact
   14.80    have "Phi p =
   14.81        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)"
   14.82      by (simp add: up_repr P monom_mult [THEN sym] monom_pow del: monom_mult)
   14.83 @@ -1772,9 +1771,9 @@
   14.84    shows "eval R R id a (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0) = \<zero>"
   14.85    (is "eval R R id a ?g = _")
   14.86  proof -
   14.87 -  interpret UP_pre_univ_prop [R R id P] proof qed simp
   14.88 +  interpret UP_pre_univ_prop R R id P proof qed simp
   14.89    have eval_ring_hom: "eval R R id a \<in> ring_hom P R" using eval_ring_hom [OF a] by simp
   14.90 -  interpret ring_hom_cring [P R "eval R R id a"] proof qed (simp add: eval_ring_hom)
   14.91 +  interpret ring_hom_cring P R "eval R R id a" proof qed (simp add: eval_ring_hom)
   14.92    have mon1_closed: "monom P \<one>\<^bsub>R\<^esub> 1 \<in> carrier P" 
   14.93      and mon0_closed: "monom P a 0 \<in> carrier P" 
   14.94      and min_mon0_closed: "\<ominus>\<^bsub>P\<^esub> monom P a 0 \<in> carrier P"
   14.95 @@ -1819,7 +1818,7 @@
   14.96      and deg_r_0: "deg R r = 0"
   14.97      shows "r = monom P (eval R R id a f) 0"
   14.98  proof -
   14.99 -  interpret UP_pre_univ_prop [R R id P] proof qed simp
  14.100 +  interpret UP_pre_univ_prop R R id P proof qed simp
  14.101    have eval_ring_hom: "eval R R id a \<in> ring_hom P R"
  14.102      using eval_ring_hom [OF a] by simp
  14.103    have "eval R R id a f = eval R R id a ?gq \<oplus>\<^bsub>R\<^esub> eval R R id a r"
  14.104 @@ -1885,7 +1884,7 @@
  14.105    "UP INTEG"} globally.
  14.106  *}
  14.107  
  14.108 -interpretation INTEG: UP_pre_univ_prop [INTEG INTEG id]
  14.109 +interpretation INTEG!: UP_pre_univ_prop INTEG INTEG id
  14.110    using INTEG_id_eval by simp_all
  14.111  
  14.112  lemma INTEG_closed [intro, simp]:
    15.1 --- a/src/HOLCF/Algebraic.thy	Tue Dec 16 15:09:37 2008 +0100
    15.2 +++ b/src/HOLCF/Algebraic.thy	Tue Dec 16 21:10:53 2008 +0100
    15.3 @@ -1,5 +1,4 @@
    15.4  (*  Title:      HOLCF/Algebraic.thy
    15.5 -    ID:         $Id$
    15.6      Author:     Brian Huffman
    15.7  *)
    15.8  
    15.9 @@ -161,7 +160,7 @@
   15.10    assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x"
   15.11    shows "pre_deflation (d oo f)"
   15.12  proof
   15.13 -  interpret d: finite_deflation [d] by fact
   15.14 +  interpret d: finite_deflation d by fact
   15.15    fix x
   15.16    show "\<And>x. (d oo f)\<cdot>x \<sqsubseteq> x"
   15.17      by (simp, rule trans_less [OF d.less f])
   15.18 @@ -174,9 +173,9 @@
   15.19    assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x"
   15.20    shows "eventual (\<lambda>n. iterate n\<cdot>(d oo f))\<cdot>x = x \<longleftrightarrow> d\<cdot>x = x \<and> f\<cdot>x = x"
   15.21  proof -
   15.22 -  interpret d: finite_deflation [d] by fact
   15.23 +  interpret d: finite_deflation d by fact
   15.24    let ?e = "d oo f"
   15.25 -  interpret e: pre_deflation ["d oo f"]
   15.26 +  interpret e: pre_deflation "d oo f"
   15.27      using `finite_deflation d` f
   15.28      by (rule pre_deflation_d_f)
   15.29    let ?g = "eventual (\<lambda>n. iterate n\<cdot>?e)"
   15.30 @@ -216,7 +215,7 @@
   15.31  lemma finite_deflation_Rep_fin_defl: "finite_deflation (Rep_fin_defl d)"
   15.32  using Rep_fin_defl by simp
   15.33  
   15.34 -interpretation Rep_fin_defl: finite_deflation ["Rep_fin_defl d"]
   15.35 +interpretation Rep_fin_defl!: finite_deflation "Rep_fin_defl d"
   15.36  by (rule finite_deflation_Rep_fin_defl)
   15.37  
   15.38  lemma fin_defl_lessI:
   15.39 @@ -321,7 +320,7 @@
   15.40  apply (rule Rep_fin_defl.compact)
   15.41  done
   15.42  
   15.43 -interpretation fin_defl: basis_take [sq_le fd_take]
   15.44 +interpretation fin_defl!: basis_take sq_le fd_take
   15.45  apply default
   15.46  apply (rule fd_take_less)
   15.47  apply (rule fd_take_idem)
   15.48 @@ -371,8 +370,8 @@
   15.49  unfolding alg_defl_principal_def
   15.50  by (simp add: Abs_alg_defl_inverse sq_le.ideal_principal)
   15.51  
   15.52 -interpretation alg_defl:
   15.53 -  ideal_completion [sq_le fd_take alg_defl_principal Rep_alg_defl]
   15.54 +interpretation alg_defl!:
   15.55 +  ideal_completion sq_le fd_take alg_defl_principal Rep_alg_defl
   15.56  apply default
   15.57  apply (rule ideal_Rep_alg_defl)
   15.58  apply (erule Rep_alg_defl_lub)
   15.59 @@ -462,7 +461,7 @@
   15.60  apply (rule finite_deflation_Rep_fin_defl)
   15.61  done
   15.62  
   15.63 -interpretation cast: deflation ["cast\<cdot>d"]
   15.64 +interpretation cast!: deflation "cast\<cdot>d"
   15.65  by (rule deflation_cast)
   15.66  
   15.67  lemma "cast\<cdot>(\<Squnion>i. alg_defl_principal (Abs_fin_defl (approx i)))\<cdot>x = x"
   15.68 @@ -486,7 +485,7 @@
   15.69    constrains e :: "'a::profinite \<rightarrow> 'b::profinite"
   15.70    shows "\<exists>d. cast\<cdot>d = e oo p"
   15.71  proof
   15.72 -  interpret ep_pair [e p] by fact
   15.73 +  interpret ep_pair e p by fact
   15.74    let ?a = "\<lambda>i. e oo approx i oo p"
   15.75    have a: "\<And>i. finite_deflation (?a i)"
   15.76      apply (rule finite_deflation_e_d_p)
   15.77 @@ -517,7 +516,7 @@
   15.78      "\<And>i. finite_deflation (a i)"
   15.79      "(\<Squnion>i. a i) = ID"
   15.80  proof
   15.81 -  interpret ep_pair [e p] by fact
   15.82 +  interpret ep_pair e p by fact
   15.83    let ?a = "\<lambda>i. p oo cast\<cdot>(approx i\<cdot>d) oo e"
   15.84    show "\<And>i. finite_deflation (?a i)"
   15.85      apply (rule finite_deflation_p_d_e)
    16.1 --- a/src/HOLCF/Bifinite.thy	Tue Dec 16 15:09:37 2008 +0100
    16.2 +++ b/src/HOLCF/Bifinite.thy	Tue Dec 16 21:10:53 2008 +0100
    16.3 @@ -1,5 +1,4 @@
    16.4  (*  Title:      HOLCF/Bifinite.thy
    16.5 -    ID:         $Id$
    16.6      Author:     Brian Huffman
    16.7  *)
    16.8  
    16.9 @@ -38,7 +37,7 @@
   16.10      by (rule finite_fixes_approx)
   16.11  qed
   16.12  
   16.13 -interpretation approx: finite_deflation ["approx i"]
   16.14 +interpretation approx!: finite_deflation "approx i"
   16.15  by (rule finite_deflation_approx)
   16.16  
   16.17  lemma (in deflation) deflation: "deflation d" ..
    17.1 --- a/src/HOLCF/CompactBasis.thy	Tue Dec 16 15:09:37 2008 +0100
    17.2 +++ b/src/HOLCF/CompactBasis.thy	Tue Dec 16 21:10:53 2008 +0100
    17.3 @@ -1,5 +1,4 @@
    17.4  (*  Title:      HOLCF/CompactBasis.thy
    17.5 -    ID:         $Id$
    17.6      Author:     Brian Huffman
    17.7  *)
    17.8  
    17.9 @@ -47,8 +46,8 @@
   17.10  
   17.11  lemmas approx_Rep_compact_basis = Rep_compact_take [symmetric]
   17.12  
   17.13 -interpretation compact_basis:
   17.14 -  basis_take [sq_le compact_take]
   17.15 +interpretation compact_basis!:
   17.16 +  basis_take sq_le compact_take
   17.17  proof
   17.18    fix n :: nat and a :: "'a compact_basis"
   17.19    show "compact_take n a \<sqsubseteq> a"
   17.20 @@ -93,8 +92,8 @@
   17.21    approximants :: "'a \<Rightarrow> 'a compact_basis set" where
   17.22    "approximants = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})"
   17.23  
   17.24 -interpretation compact_basis:
   17.25 -  ideal_completion [sq_le compact_take Rep_compact_basis approximants]
   17.26 +interpretation compact_basis!:
   17.27 +  ideal_completion sq_le compact_take Rep_compact_basis approximants
   17.28  proof
   17.29    fix w :: 'a
   17.30    show "preorder.ideal sq_le (approximants w)"
   17.31 @@ -245,7 +244,7 @@
   17.32    assumes "ab_semigroup_idem_mult f"
   17.33    shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
   17.34  proof -
   17.35 -  interpret ab_semigroup_idem_mult [f] by fact
   17.36 +  interpret ab_semigroup_idem_mult f by fact
   17.37    show ?thesis unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2)
   17.38  qed
   17.39  
    18.1 --- a/src/HOLCF/Completion.thy	Tue Dec 16 15:09:37 2008 +0100
    18.2 +++ b/src/HOLCF/Completion.thy	Tue Dec 16 21:10:53 2008 +0100
    18.3 @@ -1,5 +1,4 @@
    18.4  (*  Title:      HOLCF/Completion.thy
    18.5 -    ID:         $Id$
    18.6      Author:     Brian Huffman
    18.7  *)
    18.8  
    18.9 @@ -157,7 +156,7 @@
   18.10  
   18.11  end
   18.12  
   18.13 -interpretation sq_le: preorder ["sq_le :: 'a::po \<Rightarrow> 'a \<Rightarrow> bool"]
   18.14 +interpretation sq_le!: preorder "sq_le :: 'a::po \<Rightarrow> 'a \<Rightarrow> bool"
   18.15  apply unfold_locales
   18.16  apply (rule refl_less)
   18.17  apply (erule (1) trans_less)
    19.1 --- a/src/HOLCF/ConvexPD.thy	Tue Dec 16 15:09:37 2008 +0100
    19.2 +++ b/src/HOLCF/ConvexPD.thy	Tue Dec 16 21:10:53 2008 +0100
    19.3 @@ -1,5 +1,4 @@
    19.4  (*  Title:      HOLCF/ConvexPD.thy
    19.5 -    ID:         $Id$
    19.6      Author:     Brian Huffman
    19.7  *)
    19.8  
    19.9 @@ -21,7 +20,7 @@
   19.10  lemma convex_le_trans: "\<lbrakk>t \<le>\<natural> u; u \<le>\<natural> v\<rbrakk> \<Longrightarrow> t \<le>\<natural> v"
   19.11  unfolding convex_le_def by (fast intro: upper_le_trans lower_le_trans)
   19.12  
   19.13 -interpretation convex_le: preorder [convex_le]
   19.14 +interpretation convex_le!: preorder convex_le
   19.15  by (rule preorder.intro, rule convex_le_refl, rule convex_le_trans)
   19.16  
   19.17  lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<natural> t"
   19.18 @@ -179,8 +178,8 @@
   19.19  unfolding convex_principal_def
   19.20  by (simp add: Abs_convex_pd_inverse convex_le.ideal_principal)
   19.21  
   19.22 -interpretation convex_pd:
   19.23 -  ideal_completion [convex_le pd_take convex_principal Rep_convex_pd]
   19.24 +interpretation convex_pd!:
   19.25 +  ideal_completion convex_le pd_take convex_principal Rep_convex_pd
   19.26  apply unfold_locales
   19.27  apply (rule pd_take_convex_le)
   19.28  apply (rule pd_take_idem)
   19.29 @@ -297,7 +296,7 @@
   19.30  apply (simp add: PDPlus_absorb)
   19.31  done
   19.32  
   19.33 -interpretation aci_convex_plus: ab_semigroup_idem_mult ["op +\<natural>"]
   19.34 +interpretation aci_convex_plus!: ab_semigroup_idem_mult "op +\<natural>"
   19.35    by unfold_locales
   19.36      (rule convex_plus_assoc convex_plus_commute convex_plus_absorb)+
   19.37  
    20.1 --- a/src/HOLCF/Deflation.thy	Tue Dec 16 15:09:37 2008 +0100
    20.2 +++ b/src/HOLCF/Deflation.thy	Tue Dec 16 21:10:53 2008 +0100
    20.3 @@ -1,5 +1,4 @@
    20.4  (*  Title:      HOLCF/Deflation.thy
    20.5 -    ID:         $Id$
    20.6      Author:     Brian Huffman
    20.7  *)
    20.8  
    20.9 @@ -82,10 +81,10 @@
   20.10    assumes "deflation g"
   20.11    shows "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>(g\<cdot>x) = f\<cdot>x"
   20.12  proof (rule antisym_less)
   20.13 -  interpret g: deflation [g] by fact
   20.14 +  interpret g: deflation g by fact
   20.15    from g.less show "f\<cdot>(g\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
   20.16  next
   20.17 -  interpret f: deflation [f] by fact
   20.18 +  interpret f: deflation f by fact
   20.19    assume "f \<sqsubseteq> g" hence "f\<cdot>x \<sqsubseteq> g\<cdot>x" by (rule monofun_cfun_fun)
   20.20    hence "f\<cdot>(f\<cdot>x) \<sqsubseteq> f\<cdot>(g\<cdot>x)" by (rule monofun_cfun_arg)
   20.21    also have "f\<cdot>(f\<cdot>x) = f\<cdot>x" by (rule f.idem)
   20.22 @@ -220,7 +219,7 @@
   20.23    assumes "deflation d"
   20.24    shows "deflation (e oo d oo p)"
   20.25  proof
   20.26 -  interpret deflation [d] by fact
   20.27 +  interpret deflation d by fact
   20.28    fix x :: 'b
   20.29    show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
   20.30      by (simp add: idem)
   20.31 @@ -232,7 +231,7 @@
   20.32    assumes "finite_deflation d"
   20.33    shows "finite_deflation (e oo d oo p)"
   20.34  proof
   20.35 -  interpret finite_deflation [d] by fact
   20.36 +  interpret finite_deflation d by fact
   20.37    fix x :: 'b
   20.38    show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
   20.39      by (simp add: idem)
   20.40 @@ -251,7 +250,7 @@
   20.41    assumes d: "\<And>x. d\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>x)"
   20.42    shows "deflation (p oo d oo e)"
   20.43  proof -
   20.44 -  interpret d: deflation [d] by fact
   20.45 +  interpret d: deflation d by fact
   20.46    {
   20.47      fix x
   20.48      have "d\<cdot>(e\<cdot>x) \<sqsubseteq> e\<cdot>x"
   20.49 @@ -288,7 +287,7 @@
   20.50    assumes d: "\<And>x. d\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>x)"
   20.51    shows "finite_deflation (p oo d oo e)"
   20.52  proof -
   20.53 -  interpret d: finite_deflation [d] by fact
   20.54 +  interpret d: finite_deflation d by fact
   20.55    show ?thesis
   20.56    proof (intro_locales)
   20.57      have "deflation d" ..
   20.58 @@ -317,8 +316,8 @@
   20.59    assumes "ep_pair e1 p" and "ep_pair e2 p"
   20.60    shows "e1 \<sqsubseteq> e2"
   20.61  proof (rule less_cfun_ext)
   20.62 -  interpret e1: ep_pair [e1 p] by fact
   20.63 -  interpret e2: ep_pair [e2 p] by fact
   20.64 +  interpret e1: ep_pair e1 p by fact
   20.65 +  interpret e2: ep_pair e2 p by fact
   20.66    fix x
   20.67    have "e1\<cdot>(p\<cdot>(e2\<cdot>x)) \<sqsubseteq> e2\<cdot>x"
   20.68      by (rule e1.e_p_less)
   20.69 @@ -334,8 +333,8 @@
   20.70    assumes "ep_pair e p1" and "ep_pair e p2"
   20.71    shows "p1 \<sqsubseteq> p2"
   20.72  proof (rule less_cfun_ext)
   20.73 -  interpret p1: ep_pair [e p1] by fact
   20.74 -  interpret p2: ep_pair [e p2] by fact
   20.75 +  interpret p1: ep_pair e p1 by fact
   20.76 +  interpret p2: ep_pair e p2 by fact
   20.77    fix x
   20.78    have "e\<cdot>(p1\<cdot>x) \<sqsubseteq> x"
   20.79      by (rule p1.e_p_less)
   20.80 @@ -358,8 +357,8 @@
   20.81    assumes "ep_pair e1 p1" and "ep_pair e2 p2"
   20.82    shows "ep_pair (e2 oo e1) (p1 oo p2)"
   20.83  proof
   20.84 -  interpret ep1: ep_pair [e1 p1] by fact
   20.85 -  interpret ep2: ep_pair [e2 p2] by fact
   20.86 +  interpret ep1: ep_pair e1 p1 by fact
   20.87 +  interpret ep2: ep_pair e2 p2 by fact
   20.88    fix x y
   20.89    show "(p1 oo p2)\<cdot>((e2 oo e1)\<cdot>x) = x"
   20.90      by simp
    21.1 --- a/src/HOLCF/LowerPD.thy	Tue Dec 16 15:09:37 2008 +0100
    21.2 +++ b/src/HOLCF/LowerPD.thy	Tue Dec 16 21:10:53 2008 +0100
    21.3 @@ -1,5 +1,4 @@
    21.4  (*  Title:      HOLCF/LowerPD.thy
    21.5 -    ID:         $Id$
    21.6      Author:     Brian Huffman
    21.7  *)
    21.8  
    21.9 @@ -27,7 +26,7 @@
   21.10  apply (erule (1) trans_less)
   21.11  done
   21.12  
   21.13 -interpretation lower_le: preorder [lower_le]
   21.14 +interpretation lower_le!: preorder lower_le
   21.15  by (rule preorder.intro, rule lower_le_refl, rule lower_le_trans)
   21.16  
   21.17  lemma lower_le_minimal [simp]: "PDUnit compact_bot \<le>\<flat> t"
   21.18 @@ -134,8 +133,8 @@
   21.19  unfolding lower_principal_def
   21.20  by (simp add: Abs_lower_pd_inverse lower_le.ideal_principal)
   21.21  
   21.22 -interpretation lower_pd:
   21.23 -  ideal_completion [lower_le pd_take lower_principal Rep_lower_pd]
   21.24 +interpretation lower_pd!:
   21.25 +  ideal_completion lower_le pd_take lower_principal Rep_lower_pd
   21.26  apply unfold_locales
   21.27  apply (rule pd_take_lower_le)
   21.28  apply (rule pd_take_idem)
   21.29 @@ -251,7 +250,7 @@
   21.30  apply (simp add: PDPlus_absorb)
   21.31  done
   21.32  
   21.33 -interpretation aci_lower_plus: ab_semigroup_idem_mult ["op +\<flat>"]
   21.34 +interpretation aci_lower_plus!: ab_semigroup_idem_mult "op +\<flat>"
   21.35    by unfold_locales
   21.36      (rule lower_plus_assoc lower_plus_commute lower_plus_absorb)+
   21.37  
    22.1 --- a/src/HOLCF/Universal.thy	Tue Dec 16 15:09:37 2008 +0100
    22.2 +++ b/src/HOLCF/Universal.thy	Tue Dec 16 21:10:53 2008 +0100
    22.3 @@ -1,5 +1,4 @@
    22.4  (*  Title:      HOLCF/Universal.thy
    22.5 -    ID:         $Id$
    22.6      Author:     Brian Huffman
    22.7  *)
    22.8  
    22.9 @@ -227,13 +226,13 @@
   22.10  apply (simp add: ubasis_take_same)
   22.11  done
   22.12  
   22.13 -interpretation udom: preorder [ubasis_le]
   22.14 +interpretation udom!: preorder ubasis_le
   22.15  apply default
   22.16  apply (rule ubasis_le_refl)
   22.17  apply (erule (1) ubasis_le_trans)
   22.18  done
   22.19  
   22.20 -interpretation udom: basis_take [ubasis_le ubasis_take]
   22.21 +interpretation udom!: basis_take ubasis_le ubasis_take
   22.22  apply default
   22.23  apply (rule ubasis_take_less)
   22.24  apply (rule ubasis_take_idem)
   22.25 @@ -282,8 +281,8 @@
   22.26  unfolding udom_principal_def
   22.27  by (simp add: Abs_udom_inverse udom.ideal_principal)
   22.28  
   22.29 -interpretation udom:
   22.30 -  ideal_completion [ubasis_le ubasis_take udom_principal Rep_udom]
   22.31 +interpretation udom!:
   22.32 +  ideal_completion ubasis_le ubasis_take udom_principal Rep_udom
   22.33  apply unfold_locales
   22.34  apply (rule ideal_Rep_udom)
   22.35  apply (erule Rep_udom_lub)
    23.1 --- a/src/HOLCF/UpperPD.thy	Tue Dec 16 15:09:37 2008 +0100
    23.2 +++ b/src/HOLCF/UpperPD.thy	Tue Dec 16 21:10:53 2008 +0100
    23.3 @@ -1,5 +1,4 @@
    23.4  (*  Title:      HOLCF/UpperPD.thy
    23.5 -    ID:         $Id$
    23.6      Author:     Brian Huffman
    23.7  *)
    23.8  
    23.9 @@ -27,7 +26,7 @@
   23.10  apply (erule (1) trans_less)
   23.11  done
   23.12  
   23.13 -interpretation upper_le: preorder [upper_le]
   23.14 +interpretation upper_le!: preorder upper_le
   23.15  by (rule preorder.intro, rule upper_le_refl, rule upper_le_trans)
   23.16  
   23.17  lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<sharp> t"
   23.18 @@ -132,8 +131,8 @@
   23.19  unfolding upper_principal_def
   23.20  by (simp add: Abs_upper_pd_inverse upper_le.ideal_principal)
   23.21  
   23.22 -interpretation upper_pd:
   23.23 -  ideal_completion [upper_le pd_take upper_principal Rep_upper_pd]
   23.24 +interpretation upper_pd!:
   23.25 +  ideal_completion upper_le pd_take upper_principal Rep_upper_pd
   23.26  apply unfold_locales
   23.27  apply (rule pd_take_upper_le)
   23.28  apply (rule pd_take_idem)
   23.29 @@ -249,7 +248,7 @@
   23.30  apply (simp add: PDPlus_absorb)
   23.31  done
   23.32  
   23.33 -interpretation aci_upper_plus: ab_semigroup_idem_mult ["op +\<sharp>"]
   23.34 +interpretation aci_upper_plus!: ab_semigroup_idem_mult "op +\<sharp>"
   23.35    by unfold_locales
   23.36      (rule upper_plus_assoc upper_plus_commute upper_plus_absorb)+
   23.37