Restructured locales with predicates: import is now an interpretation.
authorballarin
Tue Jun 20 15:53:44 2006 +0200 (2006-06-20)
changeset 19931fb32b43e7f80
parent 19930 baeb0aeb4891
child 19932 63bd0eeb4e0d
Restructured locales with predicates: import is now an interpretation.
New method intro_locales.
NEWS
src/Cube/Example.thy
src/FOL/ex/LocaleTest.thy
src/HOL/Algebra/CRing.thy
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Lattice.thy
src/HOL/Algebra/Module.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/Algebra/ringsimp.ML
src/HOL/Finite_Set.thy
src/HOL/Hyperreal/Filter.thy
src/HOL/Hyperreal/HyperDef.thy
src/HOL/Orderings.thy
src/HOL/Real/HahnBanach/FunctionNorm.thy
src/HOL/Real/HahnBanach/HahnBanach.thy
src/HOL/Real/HahnBanach/NormedSpace.thy
src/HOL/ex/Locales.thy
src/Pure/Isar/element.ML
src/Pure/Isar/locale.ML
src/ZF/Constructible/DPow_absolute.thy
src/ZF/Constructible/Rank_Separation.thy
src/ZF/Constructible/Rec_Separation.thy
src/ZF/Constructible/Satisfies_absolute.thy
src/ZF/Constructible/Separation.thy
src/ZF/ex/Group.thy
     1.1 --- a/NEWS	Tue Jun 20 14:51:59 2006 +0200
     1.2 +++ b/NEWS	Tue Jun 20 15:53:44 2006 +0200
     1.3 @@ -209,6 +209,23 @@
     1.4    This enables, for example, to define a locale for endomorphisms thus:
     1.5    locale endom = homom mult mult h.
     1.6  
     1.7 +* Isar/locales: changed the way locales with predicates are defined.
     1.8 +Instead of accumulating the specification, the imported expression is
     1.9 +now an interpretation.
    1.10 +INCOMPATIBILITY: different normal form of locale expressions.
    1.11 +In particular, in interpretations of locales with predicates,
    1.12 +goals repesenting already interpreted fragments are not removed
    1.13 +automatically.  Use method intro_locales; see below.
    1.14 +
    1.15 +* Isar/locales: new method intro_locales.  Backward reasoning for locale
    1.16 +predicates.  In addition the method is aware of interpretations and
    1.17 +discharges corresponding goals.  Optional argument `!' prevents
    1.18 +unfolding of predicates to assumptions.
    1.19 +
    1.20 +* Isar/locales: the order in which locale fragments are accumulated
    1.21 +has changed.  This enables to override declarations from fragments
    1.22 +due to interpretations -- for example, unwanted simp rules.
    1.23 +
    1.24  * Provers/induct: improved internal context management to support
    1.25  local fixes and defines on-the-fly.  Thus explicit meta-level
    1.26  connectives !! and ==> are rarely required anymore in inductive goals
     2.1 --- a/src/Cube/Example.thy	Tue Jun 20 14:51:59 2006 +0200
     2.2 +++ b/src/Cube/Example.thy	Tue Jun 20 15:53:44 2006 +0200
     2.3 @@ -16,7 +16,7 @@
     2.4  
     2.5  method_setup depth_solve = {*
     2.6    Method.thms_args (fn thms => Method.METHOD (fn facts =>
     2.7 -  (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms))))))
     2.8 +  (DEPTH_SOLVE (HEADGOAL (ares_tac (PolyML.print (facts @ thms)))))))
     2.9  *} ""
    2.10  
    2.11  method_setup depth_solve1 = {*
     3.1 --- a/src/FOL/ex/LocaleTest.thy	Tue Jun 20 14:51:59 2006 +0200
     3.2 +++ b/src/FOL/ex/LocaleTest.thy	Tue Jun 20 15:53:44 2006 +0200
     3.3 @@ -104,7 +104,10 @@
     3.4  
     3.5  theorem (in IA)
     3.6    includes ID
     3.7 -  shows True ..
     3.8 +  shows True
     3.9 +  print_interps! IA
    3.10 +  print_interps! ID
    3.11 +  ..
    3.12  
    3.13  theorem (in ID) True ..
    3.14  
    3.15 @@ -112,7 +115,7 @@
    3.16  arities i :: "term"
    3.17  
    3.18  
    3.19 -interpretation i1: IC ["X::i" "Y::i"] by (auto intro: IA.intro IC_axioms.intro)
    3.20 +interpretation i1: IC ["X::i" "Y::i"] by (intro_locales) auto
    3.21  
    3.22  print_interps IA  (* output: i1 *)
    3.23  
    3.24 @@ -125,10 +128,9 @@
    3.25  (* without prefix *)
    3.26  
    3.27  interpretation IC ["W::i" "Z::i"] .  (* subsumed by i1: IC *)
    3.28 -interpretation IC ["W::'a" "Z::i"] by (auto intro: IA.intro IC_axioms.intro)
    3.29 +interpretation IC ["W::'a" "Z::i"] by intro_locales auto
    3.30    (* subsumes i1: IA and i1: IC *)
    3.31  
    3.32 -
    3.33  print_interps IA  (* output: <no prefix>, i1 *)
    3.34  
    3.35  (* possible accesses *)
    3.36 @@ -136,13 +138,14 @@
    3.37  
    3.38  ML {* check_thm "asm_C" *}
    3.39  
    3.40 -interpretation i2: ID [X "Y::i" "Y = X"] by (simp add: eq_commute)
    3.41 +interpretation i2: ID [X "Y::i" "Y = X"]
    3.42 +  by (simp add: eq_commute) intro_locales
    3.43  
    3.44  print_interps IA  (* output: <no prefix>, i1 *)
    3.45  print_interps ID  (* output: i2 *)
    3.46  
    3.47  
    3.48 -interpretation i3: ID [X "Y::i"] .
    3.49 +interpretation i3: ID [X "Y::i"] by simp intro_locales
    3.50  
    3.51  (* duplicate: thm not added *)
    3.52  
    3.53 @@ -191,10 +194,10 @@
    3.54  proof -
    3.55    fix alpha::i and beta::'a and gamma::o
    3.56    (* FIXME: omitting type of beta leads to error later at interpret i6 *)
    3.57 -  have alpha_A: "IA(alpha)" by (auto intro: IA.intro)
    3.58 +  have alpha_A: "IA(alpha)" by intro_locales simp
    3.59    interpret i5: IA [alpha] .  (* subsumed *)
    3.60    print_interps IA  (* output: <no prefix>, i1 *)
    3.61 -  interpret i6: IC [alpha beta] by (auto intro: IC_axioms.intro)
    3.62 +  interpret i6: IC [alpha beta] by intro_locales auto
    3.63    print_interps IA   (* output: <no prefix>, i1 *)
    3.64    print_interps IC   (* output: <no prefix>, i1, i6 *)
    3.65    interpret i11: IF [gamma] by (fast intro: IF.intro)
    3.66 @@ -203,11 +206,12 @@
    3.67  
    3.68  theorem (in IA) True
    3.69  proof -
    3.70 -  print_interps IA
    3.71 +  print_interps! IA
    3.72    fix beta and gamma
    3.73    interpret i9: ID [a beta _]
    3.74 -    (* no proof obligation for IA !!! *)
    3.75 -    apply - apply (rule refl) apply assumption done
    3.76 +    apply - apply assumption
    3.77 +    apply intro_locales
    3.78 +    apply (rule refl) done
    3.79  qed rule
    3.80  
    3.81  
    3.82 @@ -316,7 +320,7 @@
    3.83  lemma "(x::i) # y # z # w = y # x # w # z"
    3.84  proof -
    3.85    interpret my: IL4 ["op #"]
    3.86 -    by (auto intro: IL3.intro IL4_axioms.intro i_assoc i_comm)
    3.87 +    by (auto intro: IL4.intro IL3.intro IL4_axioms.intro i_assoc i_comm)
    3.88    show ?thesis by (simp only: my.OP.AC)  (* or simply AC *)
    3.89  qed
    3.90  
    3.91 @@ -399,7 +403,7 @@
    3.92  
    3.93  (* effect on printed locale *)
    3.94  
    3.95 -print_locale Rlgrp
    3.96 +print_locale! Rlgrp
    3.97  
    3.98  (* use of derived theorem *)
    3.99  
   3.100 @@ -453,11 +457,6 @@
   3.101  print_interps RA5
   3.102    using A_B_C_D_E.eq apply (blast intro: RA5.intro) done
   3.103  
   3.104 -lemma (in RA5) True
   3.105 -print_facts
   3.106 -print_interps RA5
   3.107 -  ..
   3.108 -
   3.109  interpretation RA5 < RA5 _ C D B _ .
   3.110    (* Any even permutation of parameters is subsumed by the above. *)
   3.111  
   3.112 @@ -529,7 +528,7 @@
   3.113  qed simp
   3.114  
   3.115  interpretation Rplgrp < Rprgrp
   3.116 -  proof (rule Rprgrp_axioms.intro)
   3.117 +  proof intro_locales
   3.118      {
   3.119        fix x
   3.120        have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
   3.121 @@ -546,7 +545,7 @@
   3.122  
   3.123  (* effect on printed locale *)
   3.124  
   3.125 -print_locale Rplgrp
   3.126 +print_locale! Rplgrp
   3.127  
   3.128  (* use of derived theorem *)
   3.129  
   3.130 @@ -559,7 +558,7 @@
   3.131  (* circular interpretation *)
   3.132  
   3.133  interpretation Rprgrp < Rplgrp
   3.134 -  proof (rule Rplgrp_axioms.intro)
   3.135 +  proof intro_locales
   3.136      {
   3.137        fix x
   3.138        have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
   3.139 @@ -576,8 +575,8 @@
   3.140  
   3.141  (* effect on printed locale *)
   3.142  
   3.143 -print_locale Rprgrp
   3.144 -print_locale Rplgrp
   3.145 +print_locale! Rprgrp
   3.146 +print_locale! Rplgrp
   3.147  
   3.148  subsection {* Interaction of Interpretation in Theories and Locales:
   3.149    in Locale, then in Theory *}
   3.150 @@ -656,27 +655,16 @@
   3.151  qed simp
   3.152  
   3.153  interpretation Rqrgrp < Rprgrp
   3.154 -proof -
   3.155 -  show "Rpsemi(op **)"
   3.156 -    apply (rule Rpsemi.intro) apply (rule assoc) done
   3.157 -next
   3.158 -  show "Rprgrp_axioms(op **, one, inv)"
   3.159 -    apply (rule Rprgrp_axioms.intro) apply (rule rone) apply (rule rinv) done
   3.160 -qed
   3.161 +  apply intro_locales
   3.162 +  apply (rule assoc)
   3.163 +  apply (rule rone)
   3.164 +  apply (rule rinv)
   3.165 +  done
   3.166  
   3.167  interpretation R2: Rqlgrp ["op #" "rone" "rinv"] 
   3.168 -proof -
   3.169 -  apply_end (rule Rqsemi.intro)
   3.170 -  fix x y z
   3.171 -  {
   3.172 -    show "(x # y) # z = x # (y # z)" by (rule i_assoc)
   3.173 -  next
   3.174 -  apply_end (rule Rqlgrp_axioms.intro)
   3.175 -    show "rone # x = x" by (rule r_one)
   3.176 -  next
   3.177 -    show "rinv(x) # x = rone" by (rule r_inv)
   3.178 -  }
   3.179 -qed
   3.180 +  apply intro_locales  (* FIXME: intro_locales is too eager and shouldn't
   3.181 +                          solve this. *)
   3.182 +  done
   3.183  
   3.184  print_interps Rqsemi
   3.185  print_interps Rqlgrp
   3.186 @@ -684,7 +672,7 @@
   3.187  
   3.188  
   3.189  interpretation Rqlgrp < Rqrgrp
   3.190 -  proof (rule Rqrgrp_axioms.intro)
   3.191 +  proof intro_locales
   3.192      {
   3.193        fix x
   3.194        have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
   3.195 @@ -718,12 +706,12 @@
   3.196    assumes x: "x = x" and y: "y = y"
   3.197  
   3.198  interpretation Rtriv2 < Rtriv x
   3.199 -  apply (rule Rtriv.intro)
   3.200 +  apply intro_locales
   3.201    apply (rule x)
   3.202    done
   3.203  
   3.204  interpretation Rtriv2 < Rtriv y
   3.205 -  apply (rule Rtriv.intro)
   3.206 +  apply intro_locales
   3.207    apply (rule y)
   3.208    done
   3.209  
   3.210 @@ -733,7 +721,7 @@
   3.211    assumes x: "x = x" and y: "y = y" and z: "z = z"
   3.212  
   3.213  interpretation Rtriv3 < Rtriv2 x y
   3.214 -  apply (rule Rtriv2.intro)
   3.215 +  apply intro_locales
   3.216    apply (rule x)
   3.217    apply (rule y)
   3.218    done
   3.219 @@ -741,7 +729,7 @@
   3.220  print_locale Rtriv3
   3.221  
   3.222  interpretation Rtriv3 < Rtriv2 x z
   3.223 -  apply (rule Rtriv2.intro)
   3.224 +  apply intro_locales
   3.225    apply (rule x_y_z.x)
   3.226    apply (rule z)
   3.227    done
   3.228 @@ -774,7 +762,8 @@
   3.229  proof (rule Rpsemi.intro)
   3.230    fix x y z
   3.231    show "(x *** y) *** z = x *** (y *** z)"
   3.232 -    by (unfold P_def) (simp add: assoc)
   3.233 +    apply (simp only: P_def) apply (simp add: assoc) (* FIXME: unfold P_def fails *)
   3.234 +    done
   3.235  qed
   3.236  
   3.237  locale Rsemi_rev = Rpsemi + var rprod (infixl "++" 65) +
     4.1 --- a/src/HOL/Algebra/CRing.thy	Tue Jun 20 14:51:59 2006 +0200
     4.2 +++ b/src/HOL/Algebra/CRing.thy	Tue Jun 20 15:53:44 2006 +0200
     4.3 @@ -80,7 +80,8 @@
     4.4  
     4.5  lemma (in abelian_group) a_group:
     4.6    "group (| carrier = carrier G, mult = add G, one = zero G |)"
     4.7 -by (simp add: group_def a_monoid comm_group.axioms a_comm_group) 
     4.8 +  by (simp add: group_def a_monoid)
     4.9 +    (simp add: comm_group.axioms group.axioms a_comm_group)
    4.10  
    4.11  lemmas monoid_record_simps = partial_object.simps monoid.simps
    4.12  
    4.13 @@ -336,16 +337,13 @@
    4.14    by (auto intro!: monoidI m_assoc)
    4.15  
    4.16  lemma cringI:
    4.17 -(*
    4.18 -  includes struct R
    4.19 -*)
    4.20    fixes R (structure)
    4.21    assumes abelian_group: "abelian_group R"
    4.22      and comm_monoid: "comm_monoid R"
    4.23      and l_distr: "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
    4.24        ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
    4.25    shows "cring R"
    4.26 -  proof (rule cring.intro)
    4.27 +  proof (intro cring.intro ring.intro)
    4.28      show "ring_axioms R"
    4.29      -- {* Right-distributivity follows from left-distributivity and
    4.30            commutativity. *}
     5.1 --- a/src/HOL/Algebra/Coset.thy	Tue Jun 20 14:51:59 2006 +0200
     5.2 +++ b/src/HOL/Algebra/Coset.thy	Tue Jun 20 15:53:44 2006 +0200
     5.3 @@ -305,7 +305,7 @@
     5.4       "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
     5.5        \<Longrightarrow> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)"
     5.6  by (simp add: setmult_rcos_assoc coset_mult_assoc
     5.7 -              subgroup_mult_id subset prems)
     5.8 +              subgroup_mult_id normal.axioms subset prems)
     5.9  
    5.10  lemma (in normal) rcos_sum:
    5.11       "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
    5.12 @@ -315,7 +315,7 @@
    5.13  lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M"
    5.14    -- {* generalizes @{text subgroup_mult_id} *}
    5.15    by (auto simp add: RCOSETS_def subset
    5.16 -        setmult_rcos_assoc subgroup_mult_id prems)
    5.17 +        setmult_rcos_assoc subgroup_mult_id normal.axioms prems)
    5.18  
    5.19  
    5.20  subsubsection{*An Equivalence Relation*}
    5.21 @@ -504,7 +504,7 @@
    5.22  
    5.23  lemma (in normal) rcosets_inv_mult_group_eq:
    5.24       "M \<in> rcosets H \<Longrightarrow> set_inv M <#> M = H"
    5.25 -by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset prems)
    5.26 +by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset normal.axioms prems)
    5.27  
    5.28  theorem (in normal) factorgroup_is_group:
    5.29    "group (G Mod H)"
    5.30 @@ -552,8 +552,8 @@
    5.31  
    5.32  text{*The kernel of a homomorphism is a normal subgroup*}
    5.33  lemma (in group_hom) normal_kernel: "(kernel G H h) \<lhd> G"
    5.34 -apply (simp add: group.normal_inv_iff subgroup_kernel group.intro prems)
    5.35 -apply (simp add: kernel_def)  
    5.36 +apply (simp add: G.normal_inv_iff subgroup_kernel)
    5.37 +apply (simp add: kernel_def)
    5.38  done
    5.39  
    5.40  lemma (in group_hom) FactGroup_nonempty:
     6.1 --- a/src/HOL/Algebra/Group.thy	Tue Jun 20 14:51:59 2006 +0200
     6.2 +++ b/src/HOL/Algebra/Group.thy	Tue Jun 20 15:53:44 2006 +0200
     6.3 @@ -189,8 +189,7 @@
     6.4    assumes Units: "carrier G <= Units G"
     6.5  
     6.6  
     6.7 -lemma (in group) is_group: "group G"
     6.8 -  by (rule group.intro [OF prems]) 
     6.9 +lemma (in group) is_group: "group G" .
    6.10  
    6.11  theorem groupI:
    6.12    fixes G (structure)
    6.13 @@ -468,7 +467,7 @@
    6.14        and h: "h \<in> carrier H"
    6.15    shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
    6.16    apply (rule group.inv_equality [OF DirProd_group])
    6.17 -  apply (simp_all add: prems group_def group.l_inv)
    6.18 +  apply (simp_all add: prems group.l_inv)
    6.19    done
    6.20  
    6.21  text{*This alternative proof of the previous result demonstrates interpret.
    6.22 @@ -643,8 +642,7 @@
    6.23    assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
    6.24        x \<otimes> y = y \<otimes> x"
    6.25    shows "comm_group G"
    6.26 -  by (fast intro: comm_group.intro comm_monoid_axioms.intro
    6.27 -                  is_group prems)
    6.28 +  by intro_locales (simp_all add: m_comm)
    6.29  
    6.30  lemma comm_groupI:
    6.31    fixes G (structure)
    6.32 @@ -679,7 +677,7 @@
    6.33  
    6.34  lemma (in group) subgroup_imp_group:
    6.35    "subgroup H G ==> group (G(| carrier := H |))"
    6.36 -  using subgroup.subgroup_is_group [OF _ group.intro] .
    6.37 +  by (rule subgroup.subgroup_is_group)
    6.38  
    6.39  lemma (in group) is_monoid [intro, simp]:
    6.40    "monoid G"
     7.1 --- a/src/HOL/Algebra/Lattice.thy	Tue Jun 20 14:51:59 2006 +0200
     7.2 +++ b/src/HOL/Algebra/Lattice.thy	Tue Jun 20 15:53:44 2006 +0200
     7.3 @@ -654,7 +654,7 @@
     7.4  lemma (in partial_order) total_orderI:
     7.5    assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
     7.6    shows "total_order L"
     7.7 -proof (rule total_order.intro)
     7.8 +proof (intro_locales!)
     7.9    show "lattice_axioms L"
    7.10    proof (rule lattice_axioms.intro)
    7.11      fix x y
    7.12 @@ -716,7 +716,7 @@
    7.13      and inf_exists:
    7.14      "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
    7.15    shows "complete_lattice L"
    7.16 -proof (rule complete_lattice.intro)
    7.17 +proof (intro_locales!)
    7.18    show "lattice_axioms L"
    7.19      by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+
    7.20  qed (assumption | rule complete_lattice_axioms.intro)+
     8.1 --- a/src/HOL/Algebra/Module.thy	Tue Jun 20 14:51:59 2006 +0200
     8.2 +++ b/src/HOL/Algebra/Module.thy	Tue Jun 20 15:53:44 2006 +0200
     8.3 @@ -73,16 +73,26 @@
     8.4        "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
     8.5        (a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> y)"
     8.6    shows "algebra R M"
     8.7 -  by (auto intro!: algebra.intro algebra_axioms.intro cring.axioms 
     8.8 -    module_axioms.intro prems)
     8.9 +apply (intro_locales!)
    8.10 +apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms prems)+
    8.11 +apply (rule module_axioms.intro)
    8.12 + apply (simp add: smult_closed)
    8.13 + apply (simp add: smult_l_distr)
    8.14 + apply (simp add: smult_r_distr)
    8.15 + apply (simp add: smult_assoc1)
    8.16 + apply (simp add: smult_one)
    8.17 +apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms prems)+
    8.18 +apply (rule algebra_axioms.intro)
    8.19 + apply (simp add: smult_assoc2)
    8.20 +done
    8.21  
    8.22  lemma (in algebra) R_cring:
    8.23    "cring R"
    8.24 -  by (rule cring.intro)
    8.25 +  by intro_locales
    8.26  
    8.27  lemma (in algebra) M_cring:
    8.28    "cring M"
    8.29 -  by (rule cring.intro)
    8.30 +  by intro_locales
    8.31  
    8.32  lemma (in algebra) module:
    8.33    "module R M"
     9.1 --- a/src/HOL/Algebra/UnivPoly.thy	Tue Jun 20 14:51:59 2006 +0200
     9.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Tue Jun 20 15:53:44 2006 +0200
     9.3 @@ -397,8 +397,8 @@
     9.4  *}
     9.5  
     9.6  interpretation UP_cring < cring P
     9.7 -  using UP_cring
     9.8 -  by - (erule cring.axioms)+
     9.9 +  by (intro_locales!)
    9.10 +    (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms UP_cring)+
    9.11  
    9.12  
    9.13  subsection {* Polynomials form an Algebra *}
    9.14 @@ -441,8 +441,8 @@
    9.15      UP_smult_assoc1 UP_smult_assoc2)
    9.16  
    9.17  interpretation UP_cring < algebra R P
    9.18 -  using UP_algebra
    9.19 -  by - (erule algebra.axioms)+
    9.20 +  by (intro_locales!)
    9.21 +    (rule module.axioms algebra.axioms UP_algebra)+
    9.22  
    9.23  
    9.24  subsection {* Further lemmas involving monomials *}
    9.25 @@ -945,8 +945,7 @@
    9.26  *}
    9.27  
    9.28  interpretation UP_domain < "domain" P
    9.29 -  using UP_domain
    9.30 -  by (rule domain.axioms)
    9.31 +  by (intro_locales!) (rule domain.axioms UP_domain)+
    9.32  
    9.33  
    9.34  subsection {* Evaluation Homomorphism and Universal Property*}
    9.35 @@ -1148,9 +1147,15 @@
    9.36  text {* Interpretation of ring homomorphism lemmas. *}
    9.37  
    9.38  interpretation UP_univ_prop < ring_hom_cring P S Eval
    9.39 -  by (unfold Eval_def)
    9.40 -    (fast intro!: ring_hom_cring.intro UP_cring cring.axioms prems
    9.41 -      intro: ring_hom_cring_axioms.intro eval_ring_hom)
    9.42 +  apply (unfold Eval_def)
    9.43 +  apply (intro_locales!)
    9.44 +  apply (rule ring_hom_cring.axioms)
    9.45 +  apply (rule ring_hom_cring.intro)
    9.46 +  apply intro_locales
    9.47 +  apply (rule eval_ring_hom)
    9.48 +  apply rule
    9.49 +  done
    9.50 +
    9.51  
    9.52  text {* Further properties of the evaluation homomorphism. *}
    9.53  
    9.54 @@ -1220,8 +1225,8 @@
    9.55    assumes R: "r \<in> carrier R" and S: "s \<in> carrier S"
    9.56    shows "eval R S h s (monom P r n) = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n"
    9.57  proof -
    9.58 -  from S interpret UP_univ_prop [R S h P s _]
    9.59 -    by (auto intro!: UP_univ_prop_axioms.intro)
    9.60 +  interpret UP_univ_prop [R S h P s _]
    9.61 +    by (auto! intro: UP_univ_prop.intro UP_univ_prop_axioms.intro)
    9.62    from R
    9.63    show ?thesis by (rule Eval_monom)
    9.64  qed
    9.65 @@ -1271,7 +1276,7 @@
    9.66  proof (rule ring_hom_cring.intro)
    9.67    show "ring_hom_cring_axioms P S Phi"
    9.68    by (rule ring_hom_cring_axioms.intro) (rule Phi)
    9.69 -qed (auto intro: P.cring cring.axioms)
    9.70 +qed intro_locales
    9.71  
    9.72  theorem (in UP_pre_univ_prop) UP_universal_property:
    9.73    assumes S: "s \<in> carrier S"
    9.74 @@ -1291,9 +1296,9 @@
    9.75    assumes "cring R"
    9.76      and "cring S"
    9.77      and "h \<in> ring_hom R S"
    9.78 -  shows "UP_pre_univ_prop R S h "
    9.79 -  by (fast intro: UP_pre_univ_prop.intro ring_hom_cring_axioms.intro
    9.80 -    cring.axioms prems)
    9.81 +  shows "UP_pre_univ_prop R S h"
    9.82 +  by (auto intro!: UP_pre_univ_prop.intro ring_hom_cring.intro
    9.83 +    ring_hom_cring_axioms.intro UP_cring.intro)
    9.84  
    9.85  constdefs
    9.86    INTEG :: "int ring"
    9.87 @@ -1315,8 +1320,10 @@
    9.88  *}
    9.89  
    9.90  interpretation INTEG: UP_pre_univ_prop [INTEG INTEG id]
    9.91 +  apply simp
    9.92    using INTEG_id_eval
    9.93 -  by - (erule UP_pre_univ_prop.axioms)+
    9.94 +  apply simp
    9.95 +  done
    9.96  
    9.97  lemma INTEG_closed [intro, simp]:
    9.98    "z \<in> carrier INTEG"
    10.1 --- a/src/HOL/Algebra/ringsimp.ML	Tue Jun 20 14:51:59 2006 +0200
    10.2 +++ b/src/HOL/Algebra/ringsimp.ML	Tue Jun 20 15:53:44 2006 +0200
    10.3 @@ -16,20 +16,38 @@
    10.4  val cring_ss = HOL_ss settermless termless_ring;
    10.5  
    10.6  fun cring_normalise ctxt = let
    10.7 -    fun ring_filter t = (case HOLogic.dest_Trueprop t of
    10.8 -        Const ("CRing.ring_axioms", _) $ Free (s, _) => [s]
    10.9 +    fun filter p t = (case HOLogic.dest_Trueprop t of
   10.10 +        Const (p', _) $ Free (s, _) => if p = p' then [s] else []
   10.11 +      | _ => [])
   10.12 +      handle TERM _ => [];
   10.13 +    fun filter21 p t = (case HOLogic.dest_Trueprop t of
   10.14 +        Const (p', _) $ Free (s, _) $ _ => if p = p' then [s] else []
   10.15        | _ => [])
   10.16        handle TERM _ => [];
   10.17 -    fun comm_filter t = (case HOLogic.dest_Trueprop t of
   10.18 -        Const ("Group.comm_monoid_axioms", _) $ Free (s, _) => [s]
   10.19 +    fun filter22 p t = (case HOLogic.dest_Trueprop t of
   10.20 +        Const (p', _) $ _ $ Free (s, _) => if p = p' then [s] else []
   10.21 +      | _ => [])
   10.22 +      handle TERM _ => [];
   10.23 +    fun filter31 p t = (case HOLogic.dest_Trueprop t of
   10.24 +        Const (p', _) $ Free (s, _) $ _ $ _ => if p = p' then [s] else []
   10.25 +      | _ => [])
   10.26 +      handle TERM _ => [];
   10.27 +    fun filter32 p t = (case HOLogic.dest_Trueprop t of
   10.28 +        Const (p', _) $ _ $ Free (s, _) $ _ => if p = p' then [s] else []
   10.29        | _ => [])
   10.30        handle TERM _ => [];
   10.31  
   10.32      val prems = ProofContext.prems_of ctxt;
   10.33 -    val rings = List.concat (map (ring_filter o #prop o rep_thm) prems);
   10.34 -    val comms = List.concat (map (comm_filter o #prop o rep_thm) prems);
   10.35 -    val non_comm_rings = rings \\ comms;
   10.36 -    val comm_rings = rings inter_string comms;
   10.37 +    val non_comm_rings = List.concat (map (filter "CRing.ring" o #prop o rep_thm) prems);
   10.38 +    val comm_rings = List.concat (map (filter "CRing.cring" o #prop o rep_thm) prems) @
   10.39 +        List.concat (map (filter "CRing.domain" o #prop o rep_thm) prems) @
   10.40 +        List.concat (map (filter21 "Module.module" o #prop o rep_thm) prems) @
   10.41 +        List.concat (map (filter21 "Module.algebra" o #prop o rep_thm) prems) @
   10.42 +        List.concat (map (filter22 "Module.algebra" o #prop o rep_thm) prems) @
   10.43 +        List.concat (map (filter "UnivPoly.UP_cring" o #prop o rep_thm) prems) @
   10.44 +        List.concat (map (filter "UnivPoly.UP_domain" o #prop o rep_thm) prems) @
   10.45 +        List.concat (map (filter31 "CRing.ring_hom_cring" o #prop o rep_thm) prems) @
   10.46 +        List.concat (map (filter32 "CRing.ring_hom_cring" o #prop o rep_thm) prems);
   10.47      val _ = tracing
   10.48        ("Non-commutative rings in proof context: " ^ commas non_comm_rings ^
   10.49         "\nCommutative rings in proof context: " ^ commas comm_rings);
    11.1 --- a/src/HOL/Finite_Set.thy	Tue Jun 20 14:51:59 2006 +0200
    11.2 +++ b/src/HOL/Finite_Set.thy	Tue Jun 20 15:53:44 2006 +0200
    11.3 @@ -502,13 +502,10 @@
    11.4  text{* Interpretation of locales: *}
    11.5  
    11.6  interpretation AC_add: ACe ["op +" "0::'a::comm_monoid_add"]
    11.7 -  by(auto intro: ACf.intro ACe_axioms.intro add_assoc add_commute)
    11.8 +  by intro_locales (auto intro: add_assoc add_commute)
    11.9  
   11.10  interpretation AC_mult: ACe ["op *" "1::'a::comm_monoid_mult"]
   11.11 -   apply (fast intro: ACf.intro mult_assoc mult_commute)
   11.12 -  apply (fastsimp intro: ACe_axioms.intro mult_assoc mult_commute)
   11.13 -  done
   11.14 -
   11.15 +  by intro_locales (auto intro: mult_assoc mult_commute)
   11.16  
   11.17  subsubsection{*From @{term foldSet} to @{term fold}*}
   11.18  
   11.19 @@ -1312,7 +1309,7 @@
   11.20  
   11.21  lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
   11.22      setprod f (insert a A) = f a * setprod f A"
   11.23 -by (simp add: setprod_def)
   11.24 +  by (simp add: setprod_def)
   11.25  
   11.26  lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1"
   11.27    by (simp add: setprod_def)
   11.28 @@ -1983,7 +1980,7 @@
   11.29  declare
   11.30    empty_foldSetE [rule del]   foldSet.intros [rule del]
   11.31    empty_fold1SetE [rule del]  insert_fold1SetE [rule del]
   11.32 -  -- {* No more proves involve these relations. *}
   11.33 +  -- {* No more proofs involve these relations. *}
   11.34  
   11.35  subsubsection{* Semi-Lattices *}
   11.36  
   11.37 @@ -2061,7 +2058,7 @@
   11.38  
   11.39  
   11.40  lemma (in ACIfSLlin) strict_above_f_conv:
   11.41 - "x \<cdot> y \<sqsubset> z = (x \<sqsubset> z \<or> y \<sqsubset> z)"
   11.42 +  "x \<cdot> y \<sqsubset> z = (x \<sqsubset> z \<or> y \<sqsubset> z)"
   11.43  apply(simp add: strict_below_def above_f_conv)
   11.44  using lin[of y z] lin[of x z] by (auto simp:below_def ACI)
   11.45  
   11.46 @@ -2206,6 +2203,7 @@
   11.47  
   11.48  lemma (in Lattice) ACIfSL_inf: "ACIfSL inf (op \<sqsubseteq>)"
   11.49  apply(rule ACIfSL.intro)
   11.50 +apply(rule ACIf.intro)
   11.51  apply(rule ACf_inf)
   11.52  apply(rule ACIf.axioms[OF ACIf_inf])
   11.53  apply(rule ACIfSL_axioms.intro)
   11.54 @@ -2216,7 +2214,9 @@
   11.55  done
   11.56  
   11.57  lemma (in Lattice) ACIfSL_sup: "ACIfSL sup (%x y. y \<sqsubseteq> x)"
   11.58 +(* FIXME: insert ACf_sup and use intro_locales *)
   11.59  apply(rule ACIfSL.intro)
   11.60 +apply(rule ACIf.intro)
   11.61  apply(rule ACf_sup)
   11.62  apply(rule ACIf.axioms[OF ACIf_sup])
   11.63  apply(rule ACIfSL_axioms.intro)
   11.64 @@ -2370,43 +2370,43 @@
   11.65  done
   11.66  
   11.67  interpretation min: ACIf ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
   11.68 -apply(rule ACIf_axioms.intro)
   11.69 +apply intro_locales
   11.70  apply(auto simp:min_def)
   11.71  done
   11.72  
   11.73  interpretation max: ACf ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
   11.74 -apply(rule ACf.intro)
   11.75 +apply intro_locales
   11.76  apply(auto simp:max_def)
   11.77  done
   11.78  
   11.79  interpretation max: ACIf ["max:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
   11.80 -apply(rule ACIf_axioms.intro)
   11.81 +apply intro_locales
   11.82  apply(auto simp:max_def)
   11.83  done
   11.84  
   11.85  interpretation min:
   11.86    ACIfSL ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>" "op <"]
   11.87  apply(simp add:order_less_le)
   11.88 -apply(rule ACIfSL_axioms.intro)
   11.89 +apply intro_locales
   11.90  apply(auto simp:min_def)
   11.91  done
   11.92  
   11.93  interpretation min:
   11.94    ACIfSLlin ["min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>" "op <"]
   11.95 -apply(rule ACIfSLlin_axioms.intro)
   11.96 +apply intro_locales
   11.97  apply(auto simp:min_def)
   11.98  done
   11.99  
  11.100  interpretation max:
  11.101    ACIfSL ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x" "%x y. y<x"]
  11.102  apply(simp add:order_less_le eq_sym_conv)
  11.103 -apply(rule ACIfSL_axioms.intro)
  11.104 +apply intro_locales
  11.105  apply(auto simp:max_def)
  11.106  done
  11.107  
  11.108  interpretation max:
  11.109    ACIfSLlin ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x" "%x y. y<x"]
  11.110 -apply(rule ACIfSLlin_axioms.intro)
  11.111 +apply intro_locales
  11.112  apply(auto simp:max_def)
  11.113  done
  11.114  
  11.115 @@ -2415,12 +2415,14 @@
  11.116  apply -
  11.117  apply(rule Min_def)
  11.118  apply(rule Max_def)
  11.119 +apply intro_locales
  11.120  done
  11.121  
  11.122  
  11.123  interpretation min_max:
  11.124    Distrib_Lattice ["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max" "Min" "Max"]
  11.125 -.
  11.126 +  by intro_locales
  11.127 +
  11.128  
  11.129  text{* Now we instantiate the recursion equations and declare them
  11.130  simplification rules: *}
    12.1 --- a/src/HOL/Hyperreal/Filter.thy	Tue Jun 20 14:51:59 2006 +0200
    12.2 +++ b/src/HOL/Hyperreal/Filter.thy	Tue Jun 20 15:53:44 2006 +0200
    12.3 @@ -68,10 +68,11 @@
    12.4  lemma (in freeultrafilter) finite: "finite A \<Longrightarrow> A \<notin> F"
    12.5  by (erule contrapos_pn, erule infinite)
    12.6  
    12.7 -lemma (in freeultrafilter) filter: "filter F" .
    12.8 +lemma (in freeultrafilter) filter: "filter F" by intro_locales
    12.9  
   12.10  lemma (in freeultrafilter) ultrafilter: "ultrafilter F"
   12.11 -by (rule ultrafilter.intro)
   12.12 +  by intro_locales
   12.13 +
   12.14  
   12.15  subsection {* Collect properties *}
   12.16  
   12.17 @@ -385,7 +386,8 @@
   12.18      with U show "infinite A" by (rule mem_superfrechet_all_infinite)
   12.19    qed
   12.20    from fil ultra free have "freeultrafilter U"
   12.21 -    by (rule freeultrafilter.intro)
   12.22 +    by (rule freeultrafilter.intro [OF ultrafilter.intro])
   12.23 +    (* FIXME: intro_locales should use chained facts *)
   12.24    thus ?thesis ..
   12.25  qed
   12.26  
    13.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Tue Jun 20 14:51:59 2006 +0200
    13.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Tue Jun 20 15:53:44 2006 +0200
    13.3 @@ -58,6 +58,9 @@
    13.4  by (rule FreeUltrafilterNat_mem [THEN freeultrafilter.finite])
    13.5  
    13.6  lemma FreeUltrafilterNat_not_finite: "x \<in> FreeUltrafilterNat ==> ~ finite x"
    13.7 +thm FreeUltrafilterNat_mem
    13.8 +thm freeultrafilter.infinite
    13.9 +thm FreeUltrafilterNat_mem [THEN freeultrafilter.infinite]
   13.10  by (rule FreeUltrafilterNat_mem [THEN freeultrafilter.infinite])
   13.11  
   13.12  lemma FreeUltrafilterNat_empty [simp]: "{} \<notin> FreeUltrafilterNat"
    14.1 --- a/src/HOL/Orderings.thy	Tue Jun 20 14:51:59 2006 +0200
    14.2 +++ b/src/HOL/Orderings.thy	Tue Jun 20 15:53:44 2006 +0200
    14.3 @@ -388,7 +388,7 @@
    14.4  
    14.5  interpretation min_max:
    14.6    lower_semilattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
    14.7 -apply(rule lower_semilattice_axioms.intro)
    14.8 +apply intro_locales
    14.9  apply(simp add:min_def linorder_not_le order_less_imp_le)
   14.10  apply(simp add:min_def linorder_not_le order_less_imp_le)
   14.11  apply(simp add:min_def linorder_not_le order_less_imp_le)
   14.12 @@ -396,8 +396,7 @@
   14.13  
   14.14  interpretation min_max:
   14.15    upper_semilattice["op \<le>" "max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
   14.16 -apply -
   14.17 -apply(rule upper_semilattice_axioms.intro)
   14.18 +apply intro_locales
   14.19  apply(simp add: max_def linorder_not_le order_less_imp_le)
   14.20  apply(simp add: max_def linorder_not_le order_less_imp_le)
   14.21  apply(simp add: max_def linorder_not_le order_less_imp_le)
   14.22 @@ -405,11 +404,11 @@
   14.23  
   14.24  interpretation min_max:
   14.25    lattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
   14.26 -.
   14.27 +  by intro_locales
   14.28  
   14.29  interpretation min_max:
   14.30    distrib_lattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
   14.31 -apply(rule distrib_lattice_axioms.intro)
   14.32 +apply intro_locales
   14.33  apply(rule_tac x=x and y=y in linorder_le_cases)
   14.34  apply(rule_tac x=x and y=z in linorder_le_cases)
   14.35  apply(rule_tac x=y and y=z in linorder_le_cases)
    15.1 --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Tue Jun 20 14:51:59 2006 +0200
    15.2 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Tue Jun 20 15:53:44 2006 +0200
    15.3 @@ -164,7 +164,7 @@
    15.4    shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"
    15.5  proof -
    15.6    have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
    15.7 -    by (unfold B_def fn_norm_def) (rule fn_norm_works [OF continuous.intro])
    15.8 +    by (unfold B_def fn_norm_def) (rule fn_norm_works)
    15.9    from this and b show ?thesis ..
   15.10  qed
   15.11  
   15.12 @@ -174,7 +174,7 @@
   15.13    shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"
   15.14  proof -
   15.15    have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
   15.16 -    by (unfold B_def fn_norm_def) (rule fn_norm_works [OF continuous.intro])
   15.17 +    by (unfold B_def fn_norm_def) (rule fn_norm_works)
   15.18    from this and b show ?thesis ..
   15.19  qed
   15.20  
   15.21 @@ -188,7 +188,7 @@
   15.22      So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge>
   15.23      0"}, provided the supremum exists and @{text B} is not empty. *}
   15.24    have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
   15.25 -    by (unfold B_def fn_norm_def) (rule fn_norm_works [OF continuous.intro])
   15.26 +    by (unfold B_def fn_norm_def) (rule fn_norm_works)
   15.27    moreover have "0 \<in> B V f" ..
   15.28    ultimately show ?thesis ..
   15.29  qed
   15.30 @@ -207,11 +207,10 @@
   15.31  proof cases
   15.32    assume "x = 0"
   15.33    then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp
   15.34 -  also have "f 0 = 0" ..
   15.35 +  also have "f 0 = 0" by rule intro_locales
   15.36    also have "\<bar>\<dots>\<bar> = 0" by simp
   15.37    also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
   15.38 -      by (unfold B_def fn_norm_def)
   15.39 -        (rule fn_norm_ge_zero [OF continuous.intro])
   15.40 +      by (unfold B_def fn_norm_def) (rule fn_norm_ge_zero)
   15.41      have "0 \<le> norm x" ..
   15.42    with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff)
   15.43    finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" .
   15.44 @@ -225,7 +224,7 @@
   15.45      from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
   15.46        by (auto simp add: B_def real_divide_def)
   15.47      then show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
   15.48 -      by (unfold B_def fn_norm_def) (rule fn_norm_ub [OF continuous.intro])
   15.49 +      by (unfold B_def fn_norm_def) (rule fn_norm_ub)
   15.50    qed
   15.51    finally show ?thesis .
   15.52  qed
    16.1 --- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Tue Jun 20 14:51:59 2006 +0200
    16.2 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Tue Jun 20 15:53:44 2006 +0200
    16.3 @@ -334,17 +334,16 @@
    16.4       \<and> (\<forall>x \<in> F. g x = f x)
    16.5       \<and> \<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
    16.6  proof -
    16.7 -  have E: "vectorspace E" .
    16.8 -  have E_norm: "normed_vectorspace E norm" ..
    16.9 +  have E: "vectorspace E" by intro_locales
   16.10 +  have E_norm: "normed_vectorspace E norm" by rule intro_locales
   16.11    have FE: "F \<unlhd> E" .
   16.12 -  have F: "vectorspace F" ..
   16.13 +  have F: "vectorspace F" by rule intro_locales
   16.14    have linearform: "linearform F f" .
   16.15    have F_norm: "normed_vectorspace F norm"
   16.16 -    by (rule subspace_normed_vs [OF E_norm])
   16.17 +    by (rule subspace_normed_vs)
   16.18    have ge_zero: "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
   16.19      by (rule normed_vectorspace.fn_norm_ge_zero
   16.20 -      [OF F_norm continuous.intro, folded B_def fn_norm_def])
   16.21 -
   16.22 +      [OF F_norm (* continuous.intro*), folded B_def fn_norm_def])
   16.23    txt {* We define a function @{text p} on @{text E} as follows:
   16.24      @{text "p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"} *}
   16.25    def p \<equiv> "\<lambda>x. \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
   16.26 @@ -393,7 +392,7 @@
   16.27      fix x assume "x \<in> F"
   16.28      show "\<bar>f x\<bar> \<le> p x"
   16.29        by (unfold p_def) (rule normed_vectorspace.fn_norm_le_cong
   16.30 -        [OF F_norm continuous.intro, folded B_def fn_norm_def])
   16.31 +        [OF F_norm, folded B_def fn_norm_def])
   16.32    qed
   16.33  
   16.34    txt {* Using the fact that @{text p} is a seminorm and @{text f} is bounded
   16.35 @@ -466,7 +465,7 @@
   16.36  	using g_cont
   16.37  	by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def])
   16.38      next
   16.39 -      show "continuous F norm f" by (rule continuous.intro)
   16.40 +      show "continuous F norm f" .
   16.41      qed
   16.42    qed
   16.43    with linearformE a g_cont show ?thesis by blast
    17.1 --- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Tue Jun 20 14:51:59 2006 +0200
    17.2 +++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Tue Jun 20 15:53:44 2006 +0200
    17.3 @@ -97,11 +97,11 @@
    17.4    includes subspace F E + normed_vectorspace E
    17.5    shows "normed_vectorspace F norm"
    17.6  proof
    17.7 -  show "vectorspace F" by (rule vectorspace)
    17.8 -  have "seminorm E norm" . with subset show "seminorm F norm"
    17.9 -    by (simp add: seminorm_def)
   17.10 -  have "norm_axioms E norm" . with subset show "norm_axioms F norm"
   17.11 -    by (simp add: norm_axioms_def)
   17.12 +  show "vectorspace F" by (rule vectorspace) intro_locales
   17.13 +next
   17.14 +  have "NormedSpace.norm E norm" by intro_locales
   17.15 +  with subset show "NormedSpace.norm F norm"
   17.16 +    by (simp add: norm_def seminorm_def norm_axioms_def)
   17.17  qed
   17.18  
   17.19  end
    18.1 --- a/src/HOL/ex/Locales.thy	Tue Jun 20 14:51:59 2006 +0200
    18.2 +++ b/src/HOL/ex/Locales.thy	Tue Jun 20 15:53:44 2006 +0200
    18.3 @@ -481,7 +481,7 @@
    18.4  	semigroup_product_def semigroup.defs)
    18.5      moreover
    18.6      have "semigroup ?G'" and "semigroup ?H'"
    18.7 -      using prems by (simp_all add: semigroup_def semigroup.defs)
    18.8 +      using prems by (simp_all add: semigroup_def semigroup.defs G.assoc H.assoc)
    18.9      then have "semigroup (semigroup_product ?G' ?H')" ..
   18.10      ultimately show ?thesis by (simp add: I_def semigroup_def)
   18.11    qed
    19.1 --- a/src/Pure/Isar/element.ML	Tue Jun 20 14:51:59 2006 +0200
    19.2 +++ b/src/Pure/Isar/element.ML	Tue Jun 20 15:53:44 2006 +0200
    19.3 @@ -42,6 +42,7 @@
    19.4    val conclude_witness: witness -> thm
    19.5    val mark_witness: term -> term
    19.6    val make_witness: term -> thm -> witness
    19.7 +  val dest_witness: witness -> term * thm
    19.8    val refine_witness: Proof.state -> Proof.state Seq.seq
    19.9    val rename: (string * (string * mixfix option)) list -> string -> string
   19.10    val rename_var: (string * (string * mixfix option)) list -> string * mixfix -> string * mixfix
   19.11 @@ -283,6 +284,8 @@
   19.12  
   19.13  fun make_witness t th = Witness (t, th);
   19.14  
   19.15 +fun dest_witness (Witness w) = w;
   19.16 +
   19.17  val refine_witness =
   19.18    Proof.refine (Method.Basic (K (Method.RAW_METHOD
   19.19      (K (ALLGOALS
    20.1 --- a/src/Pure/Isar/locale.ML	Tue Jun 20 14:51:59 2006 +0200
    20.2 +++ b/src/Pure/Isar/locale.ML	Tue Jun 20 15:53:44 2006 +0200
    20.3 @@ -121,6 +121,18 @@
    20.4  structure Locale: LOCALE =
    20.5  struct
    20.6  
    20.7 +fun legacy_unvarifyT thm =
    20.8 +  let
    20.9 +    val cT = Thm.ctyp_of (Thm.theory_of_thm thm);
   20.10 +    val tfrees = map (fn ((x, _), S) => SOME (cT (TFree (x, S)))) (Drule.tvars_of thm);
   20.11 +  in Drule.instantiate' tfrees [] thm end;
   20.12 +
   20.13 +fun legacy_unvarify raw_thm =
   20.14 +  let
   20.15 +    val thm = legacy_unvarifyT raw_thm;
   20.16 +    val ct = Thm.cterm_of (Thm.theory_of_thm thm);
   20.17 +    val frees = map (fn ((x, _), T) => SOME (ct (Free (x, T)))) (Drule.vars_of thm);
   20.18 +  in Drule.instantiate' [] frees thm end;
   20.19  
   20.20  (** locale elements and expressions **)
   20.21  
   20.22 @@ -140,25 +152,19 @@
   20.23    | map_elem _ (Expr e) = Expr e;
   20.24  
   20.25  type locale =
   20.26 - {predicate: cterm list * Element.witness list,
   20.27 -    (* CB: For locales with "(open)" this entry is ([], []).
   20.28 -       For new-style locales, which declare predicates, if the locale declares
   20.29 -       no predicates, this is also ([], []).
   20.30 -       If the locale declares predicates, the record field is
   20.31 -       ([statement], axioms), where statement is the locale predicate applied
   20.32 -       to the (assumed) locale parameters.  Axioms contains the projections
   20.33 -       from the locale predicate to the normalised assumptions of the locale
   20.34 -       (cf. [1], normalisation of locale expressions.)
   20.35 -    *)
   20.36 + {axiom: Element.witness list,
   20.37 +    (* For locales that define predicates this is [A [A]], where a is the locale
   20.38 +       specification.  Otherwise []. *)
   20.39    import: expr,                                                     (*dynamic import*)
   20.40    elems: (Element.context_i * stamp) list,
   20.41      (* Static content, neither Fixes nor Constrains elements *)
   20.42    params: ((string * typ) * mixfix) list,                           (*all params*)
   20.43 -  lparams: string list,                                             (*local parmas*)
   20.44 +  lparams: string list,                                             (*local params*)
   20.45    term_syntax: ((Proof.context -> Proof.context) * stamp) list, (* FIXME depend on morphism *)
   20.46 -  regs: ((string * string list) * Element.witness list) list}
   20.47 +  regs: ((string * string list) * Element.witness list) list,
   20.48      (* Registrations: indentifiers and witnesses of locales interpreted in the locale. *)
   20.49 -
   20.50 +  intros: thm list * thm list}
   20.51 +    (* Introduction rules: of delta predicate and locale predicate. *)
   20.52  
   20.53  (* CB: an internal (Int) locale element was either imported or included,
   20.54     an external (Ext) element appears directly in the locale text. *)
   20.55 @@ -268,15 +274,16 @@
   20.56    val copy = I;
   20.57    val extend = I;
   20.58  
   20.59 -  fun join_locs _ ({predicate, import, elems, params, lparams, term_syntax, regs}: locale,
   20.60 +  fun join_locs _ ({axiom, import, elems, params, lparams, term_syntax, regs, intros}: locale,
   20.61        {elems = elems', term_syntax = term_syntax', regs = regs', ...}: locale) =
   20.62 -     {predicate = predicate,
   20.63 +     {axiom = axiom,
   20.64        import = import,
   20.65        elems = gen_merge_lists (eq_snd (op =)) elems elems',
   20.66        params = params,
   20.67        lparams = lparams,
   20.68        term_syntax = Library.merge (eq_snd (op =)) (term_syntax, term_syntax'),
   20.69 -      regs = merge_alists regs regs'};
   20.70 +      regs = merge_alists regs regs',
   20.71 +      intros = intros};
   20.72    fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) =
   20.73      (NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2),
   20.74       Symtab.join (K Registrations.join) (regs1, regs2));
   20.75 @@ -328,12 +335,14 @@
   20.76  
   20.77  fun change_locale name f thy =
   20.78    let
   20.79 -    val {predicate, import, elems, params, lparams, term_syntax, regs} = the_locale thy name;
   20.80 -    val (predicate', import', elems', params', lparams', term_syntax', regs') =
   20.81 -      f (predicate, import, elems, params, lparams, term_syntax, regs);
   20.82 +    val {axiom, import, elems, params, lparams, term_syntax, regs, intros} =
   20.83 +        the_locale thy name;
   20.84 +    val (axiom', import', elems', params', lparams', term_syntax', regs', intros') =
   20.85 +      f (axiom, import, elems, params, lparams, term_syntax, regs, intros);
   20.86    in
   20.87 -    put_locale name {predicate = predicate', import = import', elems = elems',
   20.88 -      params = params', lparams = lparams', term_syntax = term_syntax', regs = regs'} thy
   20.89 +    put_locale name {axiom = axiom', import = import', elems = elems',
   20.90 +      params = params', lparams = lparams', term_syntax = term_syntax', regs = regs',
   20.91 +      intros = intros'} thy
   20.92    end;
   20.93  
   20.94  
   20.95 @@ -398,8 +407,8 @@
   20.96       gen_put_registration LocalLocalesData.map ProofContext.theory_of;
   20.97  
   20.98  fun put_registration_in_locale name id =
   20.99 -  change_locale name (fn (predicate, import, elems, params, lparams, term_syntax, regs) =>
  20.100 -    (predicate, import, elems, params, lparams, term_syntax, regs @ [(id, [])]));
  20.101 +  change_locale name (fn (axiom, import, elems, params, lparams, term_syntax, regs, intros) =>
  20.102 +    (axiom, import, elems, params, lparams, term_syntax, regs @ [(id, [])], intros));
  20.103  
  20.104  
  20.105  (* add witness theorem to registration in theory or context,
  20.106 @@ -414,11 +423,11 @@
  20.107  val add_local_witness = LocalLocalesData.map oo add_witness;
  20.108  
  20.109  fun add_witness_in_locale name id thm =
  20.110 -  change_locale name (fn (predicate, import, elems, params, lparams, term_syntax, regs) =>
  20.111 +  change_locale name (fn (axiom, import, elems, params, lparams, term_syntax, regs, intros) =>
  20.112      let
  20.113        fun add (id', thms) =
  20.114          if id = id' then (id', thm :: thms) else (id', thms);
  20.115 -    in (predicate, import, elems, params, lparams, term_syntax, map add regs) end);
  20.116 +    in (axiom, import, elems, params, lparams, term_syntax, map add regs, intros) end);
  20.117  
  20.118  
  20.119  (* printing of registrations *)
  20.120 @@ -790,17 +799,17 @@
  20.121         identify at top level (top = true);
  20.122         parms is accumulated list of parameters *)
  20.123            let
  20.124 -            val {predicate = (_, axioms), import, params, ...} =
  20.125 +            val {axiom, import, params, ...} =
  20.126                the_locale thy name;
  20.127              val ps = map (#1 o #1) params;
  20.128              val (ids', parms', _) = identify false import;
  20.129                  (* acyclic import dependencies *)
  20.130 +
  20.131              val ids'' = ids' @ [((name, ps), ([], Assumed []))];
  20.132              val (_, ids''') = add_regs (name, map #1 params) ([], ids'');
  20.133 -
  20.134 -            val ids_ax = if top then fst
  20.135 -                 (fold_map (axiomify ps) ids''' axioms)
  20.136 -              else ids''';
  20.137 +            val (_, ids4) = chop (length ids' + 1) ids''';
  20.138 +            val ids5 = ids' @ ids4 @ [((name, ps), ([], Assumed []))];
  20.139 +            val ids_ax = if top then fst (fold_map (axiomify ps) ids5 axiom) else ids5;
  20.140              val syn = Symtab.make (map (apfst fst) params);
  20.141              in (ids_ax, merge_lists parms' ps, syn) end
  20.142        | identify top (Rename (e, xs)) =
  20.143 @@ -837,8 +846,8 @@
  20.144          fun lookup_syn x = (case Symtab.lookup syn x of SOME Structure => NONE | opt => opt);
  20.145          val ren = map #1 ps' ~~ map (fn x => (x, lookup_syn x)) xs;
  20.146          val (params', elems') =
  20.147 -          if null ren then ((ps'(*, qs*)), map #1 elems)
  20.148 -          else ((map (apfst (Element.rename ren)) ps'(*, map (Element.rename ren) qs*)),
  20.149 +          if null ren then (ps', map #1 elems)
  20.150 +          else (map (apfst (Element.rename ren)) ps',
  20.151              map (Element.rename_ctxt ren o #1) elems);
  20.152          val elems'' = elems' |> map (Element.map_ctxt
  20.153            {var = I, typ = I, term = I, fact = I, attrib = I,
  20.154 @@ -854,7 +863,7 @@
  20.155      val idents = gen_rems (eq_fst (op =)) (ids, prev_idents);
  20.156      val syntax = merge_syntax ctxt ids (syn, prev_syntax);
  20.157      (* add types to params and unify them *)
  20.158 -    val raw_elemss = (*unique_parms ctxt*) (map (eval syntax) idents);
  20.159 +    val raw_elemss = map (eval syntax) idents;
  20.160      val elemss = unify_elemss' ctxt [] raw_elemss (map (apsnd mixfix_type) (Symtab.dest syntax));
  20.161      (* replace params in ids by params from axioms,
  20.162         adjust types in mode *)
  20.163 @@ -890,22 +899,22 @@
  20.164  
  20.165  (* NB: derived ids contain only facts at this stage *)
  20.166  
  20.167 -fun activate_elem _ ((ctxt, mode), Fixes fixes) =
  20.168 +fun activate_elem _ _ ((ctxt, mode), Fixes fixes) =
  20.169        ((ctxt |> ProofContext.add_fixes_i fixes |> snd, mode), [])
  20.170 -  | activate_elem _ ((ctxt, mode), Constrains _) =
  20.171 +  | activate_elem _ _ ((ctxt, mode), Constrains _) =
  20.172        ((ctxt, mode), [])
  20.173 -  | activate_elem _ ((ctxt, Assumed axs), Assumes asms) =
  20.174 +  | activate_elem ax_in_ctxt _ ((ctxt, Assumed axs), Assumes asms) =
  20.175        let
  20.176          val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
  20.177          val ts = maps (map #1 o #2) asms';
  20.178          val (ps, qs) = chop (length ts) axs;
  20.179          val (_, ctxt') =
  20.180            ctxt |> fold ProofContext.fix_frees ts
  20.181 -          |> ProofContext.add_assms_i (axioms_export ps) asms';
  20.182 +          |> ProofContext.add_assms_i (axioms_export (if ax_in_ctxt then ps else [])) asms';
  20.183        in ((ctxt', Assumed qs), []) end
  20.184 -  | activate_elem _ ((ctxt, Derived ths), Assumes asms) =
  20.185 +  | activate_elem _ _ ((ctxt, Derived ths), Assumes asms) =
  20.186        ((ctxt, Derived ths), [])
  20.187 -  | activate_elem _ ((ctxt, Assumed axs), Defines defs) =
  20.188 +  | activate_elem _ _ ((ctxt, Assumed axs), Defines defs) =
  20.189        let
  20.190          val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
  20.191          val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
  20.192 @@ -915,19 +924,19 @@
  20.193            ctxt |> fold (ProofContext.fix_frees o #1) asms
  20.194            |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
  20.195        in ((ctxt', Assumed axs), []) end
  20.196 -  | activate_elem _ ((ctxt, Derived ths), Defines defs) =
  20.197 +  | activate_elem _ _ ((ctxt, Derived ths), Defines defs) =
  20.198        ((ctxt, Derived ths), [])
  20.199 -  | activate_elem is_ext ((ctxt, mode), Notes facts) =
  20.200 +  | activate_elem _ is_ext ((ctxt, mode), Notes facts) =
  20.201        let
  20.202          val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
  20.203          val (res, ctxt') = ctxt |> ProofContext.note_thmss_i facts';
  20.204        in ((ctxt', mode), if is_ext then res else []) end;
  20.205  
  20.206 -fun activate_elems (((name, ps), mode), elems) ctxt =
  20.207 +fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt =
  20.208    let
  20.209      val thy = ProofContext.theory_of ctxt;
  20.210      val ((ctxt', _), res) =
  20.211 -        foldl_map (activate_elem (name = "")) ((ProofContext.qualified_names ctxt, mode), elems)
  20.212 +        foldl_map (activate_elem ax_in_ctxt (name = "")) ((ProofContext.qualified_names ctxt, mode), elems)
  20.213        handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)]
  20.214      val ctxt'' = if name = "" then ctxt'
  20.215            else let
  20.216 @@ -941,15 +950,15 @@
  20.217              end
  20.218    in (ProofContext.restore_naming ctxt ctxt'', res) end;
  20.219  
  20.220 -fun activate_elemss prep_facts =
  20.221 +fun activate_elemss ax_in_ctxt prep_facts =
  20.222      fold_map (fn (((name, ps), mode), raw_elems) => fn ctxt =>
  20.223        let
  20.224          val elems = map (prep_facts ctxt) raw_elems;
  20.225          val (ctxt', res) = apsnd flat
  20.226 -            (activate_elems (((name, ps), mode), elems) ctxt);
  20.227 +            (activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt);
  20.228          val elems' = elems |> map (Element.map_ctxt
  20.229            {name = I, var = I, typ = I, term = I, fact = I, attrib = Args.closure});
  20.230 -      in ((((name, ps), elems'), res), ctxt') end);
  20.231 +      in (((((name, ps), mode), elems'), res), ctxt') end);
  20.232  
  20.233  in
  20.234  
  20.235 @@ -964,8 +973,8 @@
  20.236     If read_facts or cert_facts is used for prep_facts, these also remove
  20.237     the internal/external markers from elemss. *)
  20.238  
  20.239 -fun activate_facts prep_facts (ctxt, args) =
  20.240 -  let val ((elemss, factss), ctxt') = activate_elemss prep_facts args ctxt |>> split_list
  20.241 +fun activate_facts ax_in_ctxt prep_facts (ctxt, args) =
  20.242 +  let val ((elemss, factss), ctxt') = activate_elemss ax_in_ctxt prep_facts args ctxt |>> split_list
  20.243    in (ctxt', (elemss, flat factss)) end;
  20.244  
  20.245  end;
  20.246 @@ -1010,7 +1019,7 @@
  20.247           merge_syntax ctxt ids'
  20.248             (syn, Symtab.make (map (fn fx => (#1 fx, #3 fx)) fixes))
  20.249             handle Symtab.DUPS xs => err_in_locale ctxt
  20.250 -             ("Conflicting syntax (3) for parameters: " ^ commas_quote xs)
  20.251 +             ("Conflicting syntax for parameters: " ^ commas_quote xs)
  20.252               (map #1 ids')),
  20.253           [((("", map (rpair NONE o #1) fixes), Assumed []), Ext (Fixes fixes))])
  20.254        end
  20.255 @@ -1301,7 +1310,7 @@
  20.256  end;
  20.257  
  20.258  
  20.259 -(* specification of a locale *)
  20.260 +(* Get the specification of a locale *)
  20.261  
  20.262  (*The global specification is made from the parameters and global
  20.263    assumptions, the local specification from the parameters and the
  20.264 @@ -1394,32 +1403,30 @@
  20.265  
  20.266      val (ps, qs) = chop (length raw_import_params_elemss + length raw_import_elemss) all_elemss';
  20.267      val (import_ctxt, (import_elemss, _)) =
  20.268 -      activate_facts prep_facts (context, ps);
  20.269 +      activate_facts false prep_facts (context, ps);
  20.270  
  20.271      val (ctxt, (elemss, _)) =
  20.272 -      activate_facts prep_facts (import_ctxt, qs);
  20.273 -    val stmt = distinct Term.aconv
  20.274 -       (maps (fn ((_, Assumed axs), _) => maps Element.witness_hyps axs
  20.275 -                           | ((_, Derived _), _) => []) qs);
  20.276 -    val cstmt = map (cterm_of thy) stmt;
  20.277 +      activate_facts false prep_facts (import_ctxt, qs);
  20.278    in
  20.279      ((((import_ctxt, import_elemss), (ctxt, elemss, syn)),
  20.280 -      (parms, spec, defs)), (cstmt, concl))
  20.281 +      (parms, spec, defs)), ([], concl))
  20.282 +(* FIXME: change signature, remove [] *)
  20.283    end;
  20.284  
  20.285  fun prep_statement prep_locale prep_ctxt raw_locale elems concl ctxt =
  20.286    let
  20.287      val thy = ProofContext.theory_of ctxt;
  20.288      val locale = Option.map (prep_locale thy) raw_locale;
  20.289 -    val (locale_stmt, fixed_params, import) =
  20.290 +    val (fixed_params, import) =
  20.291        (case locale of
  20.292 -        NONE => ([], [], empty)
  20.293 +        NONE => ([], empty)
  20.294        | SOME name =>
  20.295 -          let val {predicate = (stmt, _), params = ps, ...} = the_locale thy name
  20.296 -          in (stmt, map fst ps, Locale name) end);
  20.297 -    val ((((locale_ctxt, _), (elems_ctxt, _, _)), _), (elems_stmt, concl')) =
  20.298 +          let val {params = ps, ...} = the_locale thy name
  20.299 +          in (map fst ps, Locale name) end);
  20.300 +    val ((((locale_ctxt, _), (elems_ctxt, _, _)), _), ([], concl')) =
  20.301        prep_ctxt false fixed_params import elems concl ctxt;
  20.302 -  in (locale, (locale_stmt, locale_ctxt), (elems_stmt, elems_ctxt), concl') end;
  20.303 +  in (locale, ([], locale_ctxt), ([], elems_ctxt), concl') end;
  20.304 +  (* FIXME: change signatures, remove empty statement lists *)
  20.305  
  20.306  fun prep_expr prep import body ctxt =
  20.307    let
  20.308 @@ -1530,8 +1537,8 @@
  20.309  
  20.310  fun add_term_syntax loc syn =
  20.311    snd #> syn #> ProofContext.map_theory (change_locale loc
  20.312 -    (fn (predicate, import, elems, params, lparams, term_syntax, regs) =>
  20.313 -      (predicate, import, elems, params, lparams, (syn, stamp ()) :: term_syntax, regs)));
  20.314 +    (fn (axiom, import, elems, params, lparams, term_syntax, regs, intros) =>
  20.315 +      (axiom, import, elems, params, lparams, (syn, stamp ()) :: term_syntax, regs, intros)));
  20.316  
  20.317  fun init_term_syntax loc ctxt =
  20.318    fold_rev (fn (f, _) => fn ctxt' => f ctxt')
  20.319 @@ -1557,11 +1564,11 @@
  20.320  fun gen_thmss prep_facts global_results kind loc args (view, ctxt) thy =
  20.321    let
  20.322      val (ctxt', ([(_, [Notes args'])], facts)) =
  20.323 -      activate_facts prep_facts (ctxt, [((("", []), Assumed []), [Ext (Notes args)])]);
  20.324 +      activate_facts true prep_facts (ctxt, [((("", []), Assumed []), [Ext (Notes args)])]);
  20.325      val (facts', thy') =
  20.326        thy
  20.327 -      |> change_locale loc (fn (predicate, import, elems, params, lparams, term_syntax, regs) =>
  20.328 -        (predicate, import, elems @ [(Notes args', stamp ())], params, lparams, term_syntax, regs))
  20.329 +      |> change_locale loc (fn (axiom, import, elems, params, lparams, term_syntax, regs, intros) =>
  20.330 +        (axiom, import, elems @ [(Notes args', stamp ())], params, lparams, term_syntax, regs, intros))
  20.331        |> note_thmss_registrations kind loc args'
  20.332        |> global_results (map (#1 o #1) args' ~~ map #2 facts) (view, ctxt);
  20.333    in ((facts, facts'), (ProofContext.transfer thy' ctxt', thy')) end;
  20.334 @@ -1670,18 +1677,19 @@
  20.335    in ((statement, intro, axioms), defs_thy) end;
  20.336  
  20.337  fun assumes_to_notes (Assumes asms) axms =
  20.338 -       axms
  20.339 -       |> fold_map (fn (a, spec) => fn axs =>
  20.340 -            let val (ps, qs) = chop (length spec) axs
  20.341 -            in ((a, [(ps, [])]), qs) end) asms
  20.342 -       |-> (pair o Notes)
  20.343 +    fold_map (fn (a, spec) => fn axs =>
  20.344 +       let val (ps, qs) = chop (length spec) axs
  20.345 +       in ((a, [(ps, [])]), qs) end) asms axms
  20.346 +    |> apfst Notes
  20.347    | assumes_to_notes e axms = (e, axms);
  20.348  
  20.349 -(* CB: changes only "new" elems, these have identifier ("", _). *)
  20.350 +(* CB: the following two change only "new" elems, these have identifier ("", _). *)
  20.351 +
  20.352 +(* turn Assumes into Notes elements *)
  20.353  
  20.354 -fun change_elemss axioms elemss =
  20.355 +fun change_assumes_elemss axioms elemss =
  20.356    let
  20.357 -    fun change (id as ("", _), es)=
  20.358 +    fun change (id as ("", _), es) =
  20.359            fold_map assumes_to_notes
  20.360              (map (Element.map_ctxt_values I I (Element.satisfy_thm axioms)) es)
  20.361            #-> (fn es' => pair (id, es'))
  20.362 @@ -1690,44 +1698,53 @@
  20.363      fst (fold_map change elemss (map Element.conclude_witness axioms))
  20.364    end;
  20.365  
  20.366 +(* adjust hyps of Notes elements *)
  20.367 +
  20.368 +fun change_elemss_hyps axioms elemss =
  20.369 +  let
  20.370 +    fun change (id as ("", _), es) =
  20.371 +        (id, map (fn e as (Notes _) => Element.map_ctxt_values I I (Element.satisfy_thm axioms) e
  20.372 +                   | e => e) es)
  20.373 +      | change e = e;
  20.374 +  in map change elemss end;
  20.375 +
  20.376  in
  20.377  
  20.378  (* CB: main predicate definition function *)
  20.379  
  20.380  fun define_preds bname (parms, ((exts, exts'), (ints, ints')), defs) elemss thy =
  20.381    let
  20.382 -    val ((elemss', more_ts), thy') =
  20.383 -      if null exts then ((elemss, []), thy)
  20.384 +    val ((elemss', more_ts), a_elem, a_intro, thy') =
  20.385 +      if null exts then ((elemss, []), [], [], thy)
  20.386        else
  20.387          let
  20.388            val aname = if null ints then bname else bname ^ "_" ^ axiomsN;
  20.389            val ((statement, intro, axioms), def_thy) =
  20.390              thy |> def_pred aname parms defs exts exts';
  20.391 -          val elemss' =
  20.392 -            change_elemss axioms elemss
  20.393 -            @ [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
  20.394 -        in
  20.395 -          def_thy
  20.396 -          |> PureThy.note_thmss_qualified "" aname [((introN, []), [([intro], [])])]
  20.397 -          |> snd
  20.398 -          |> pair (elemss', [statement])
  20.399 -        end;
  20.400 -    val (predicate, thy'') =
  20.401 -      if null ints then (([], []), thy')
  20.402 +          val elemss' = change_assumes_elemss axioms elemss;
  20.403 +          val def_thy' = def_thy
  20.404 +            |> PureThy.note_thmss_qualified "" aname [((introN, []), [([intro], [])])]
  20.405 +            |> snd
  20.406 +          val a_elem = [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
  20.407 +        in ((elemss', [statement]), a_elem, [intro], def_thy') end;
  20.408 +    val (predicate, stmt', elemss'', b_intro, thy'') =
  20.409 +      if null ints then (([], []), more_ts, elemss' @ a_elem, [], thy')
  20.410        else
  20.411          let
  20.412            val ((statement, intro, axioms), def_thy) =
  20.413              thy' |> def_pred bname parms defs (ints @ more_ts) (ints' @ more_ts);
  20.414            val cstatement = Thm.cterm_of def_thy statement;
  20.415 -        in
  20.416 +          val elemss'' = change_elemss_hyps axioms elemss';
  20.417 +          val def_thy' =
  20.418            def_thy
  20.419            |> PureThy.note_thmss_qualified "" bname
  20.420                 [((introN, []), [([intro], [])]),
  20.421                  ((axiomsN, []), [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
  20.422 -          |> snd
  20.423 -          |> pair ([cstatement], axioms)
  20.424 -        end;
  20.425 -  in ((elemss', predicate), thy'') end;
  20.426 +          |> snd;
  20.427 +          val b_elem = [(("", []),
  20.428 +               [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
  20.429 +        in (([cstatement], axioms), [statement], elemss'' @ b_elem, [intro], def_thy') end;
  20.430 +  in (((elemss'', predicate, stmt'), (a_intro, b_intro)), thy'') end;
  20.431  
  20.432  end;
  20.433  
  20.434 @@ -1736,6 +1753,24 @@
  20.435  
  20.436  local
  20.437  
  20.438 +(* turn Defines into Notes elements, accumulate definition terms *)
  20.439 +
  20.440 +fun defines_to_notes true thy (Defines defs) ts =
  20.441 +    fold_map (fn (a, (def, _)) => fn ts =>
  20.442 +      ((a, [([assume (cterm_of thy def)], [])]), ts @ [def])) defs ts
  20.443 +    |> apfst (SOME o Notes)
  20.444 +  | defines_to_notes false _ (Defines defs) ts =
  20.445 +    fold (fn (_, (def, _)) => fn ts => ts @ [def]) defs ts |> pair NONE
  20.446 +  | defines_to_notes _ _ e ts = (SOME e, ts);
  20.447 +
  20.448 +fun change_defines_elemss thy elemss ts =
  20.449 +  let
  20.450 +    fun change (id as (n, _), es) ts =
  20.451 +        let
  20.452 +          val (es', ts') = fold_map (defines_to_notes (n="") thy) es ts
  20.453 +        in ((id, map_filter I es'), ts') end
  20.454 +  in fold_map change elemss ts end;
  20.455 +
  20.456  fun gen_add_locale prep_ctxt prep_expr
  20.457      do_predicate bname raw_import raw_body thy =
  20.458    let
  20.459 @@ -1745,9 +1780,10 @@
  20.460  
  20.461      val thy_ctxt = ProofContext.init thy;
  20.462      val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)),
  20.463 -      text as (parms, ((_, exts'), _), _)) =
  20.464 +      text as (parms, ((_, exts'), _), defs)) =
  20.465        prep_ctxt raw_import raw_body thy_ctxt;
  20.466 -    val elemss = import_elemss @ body_elemss;
  20.467 +    val elemss = import_elemss @ body_elemss |>
  20.468 +        map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE);
  20.469      val import = prep_expr thy raw_import;
  20.470  
  20.471      val extraTs = foldr Term.add_term_tfrees [] exts' \\
  20.472 @@ -1755,9 +1791,25 @@
  20.473      val _ = if null extraTs then ()
  20.474        else warning ("Additional type variable(s) in locale specification " ^ quote bname);
  20.475  
  20.476 -    val ((elemss', predicate as (predicate_statement, predicate_axioms)), pred_thy) =
  20.477 -      if do_predicate then thy |> define_preds bname text elemss
  20.478 -      else ((elemss, ([], [])), thy);
  20.479 +    val ((((elemss', predicate as (predicate_statement, predicate_axioms), stmt'), intros),
  20.480 +          pred_thy), (import, regs)) =
  20.481 +      if do_predicate then
  20.482 +        let
  20.483 +          val (elemss', defs) = change_defines_elemss thy elemss [];
  20.484 +          val elemss'' = elemss' @
  20.485 +              [(("", []), [Defines (map (fn t => (("", []), (t, []))) defs)])];
  20.486 +          val (((elemss''', predicate as (_, axioms), stmt'), intros), thy') =
  20.487 +            define_preds bname text elemss'' thy;
  20.488 +          fun mk_regs elemss wits =
  20.489 +            fold_map (fn (id, elems) => fn wts => let
  20.490 +                val ts = List.concat (List.mapPartial (fn (Assumes asms) =>
  20.491 +                  SOME (List.concat (map (map #1 o #2) asms)) | _ => NONE) elems);
  20.492 +                val (wts1, wts2) = chop (length ts) wts
  20.493 +              in ((apsnd (map fst) id, wts1), wts2) end) elemss wits |> fst;
  20.494 +          val regs = mk_regs elemss''' axioms |>
  20.495 +                map_filter (fn (("", _), _) => NONE | e => SOME e);
  20.496 +        in ((((elemss''', predicate, stmt'), intros), thy'), (empty, regs)) end
  20.497 +      else ((((elemss, ([], []), []), ([], [])), thy), (import, []));
  20.498  
  20.499      fun axiomify axioms elemss =
  20.500        (axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let
  20.501 @@ -1767,23 +1819,25 @@
  20.502                   in (axs2, ((id, Assumed axs1), elems)) end)
  20.503          |> snd;
  20.504      val pred_ctxt = ProofContext.init pred_thy;
  20.505 -    val (ctxt, (_, facts)) = activate_facts (K I)
  20.506 +    val (ctxt, (_, facts)) = activate_facts true (K I)
  20.507        (pred_ctxt, axiomify predicate_axioms elemss');
  20.508      val export = ProofContext.export_view predicate_statement ctxt thy_ctxt;
  20.509      val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
  20.510      val elems' = maps #2 (filter (equal "" o #1 o #1) elemss');
  20.511      val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems';
  20.512 +    val axs' = map (Element.assume_witness pred_thy) stmt';
  20.513      val thy' = pred_thy
  20.514        |> PureThy.note_thmss_qualified "" bname facts' |> snd
  20.515        |> declare_locale name
  20.516        |> put_locale name
  20.517 -       {predicate = predicate,
  20.518 +       {axiom = axs',
  20.519          import = import,
  20.520          elems = map (fn e => (e, stamp ())) elems'',
  20.521          params = params_of elemss' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),
  20.522 -        lparams = map #1 (params_of body_elemss),
  20.523 +        lparams = map #1 (params_of' body_elemss),
  20.524          term_syntax = [],
  20.525 -        regs = []};
  20.526 +        regs = regs,
  20.527 +        intros = intros};
  20.528    in ((name, ProofContext.transfer thy' body_ctxt), thy') end;
  20.529  
  20.530  in
  20.531 @@ -1891,6 +1945,51 @@
  20.532  end;
  20.533  
  20.534  
  20.535 +(** Normalisation of locale statements ---
  20.536 +    discharges goals implied by interpretations **)
  20.537 +
  20.538 +local
  20.539 +
  20.540 +fun locale_assm_intros thy =
  20.541 +  Symtab.fold (fn (_, {intros = (a, _), ...}) => fn intros => (a @ intros))
  20.542 +    (#2 (GlobalLocalesData.get thy)) [];
  20.543 +fun locale_base_intros thy =
  20.544 +  Symtab.fold (fn (_, {intros = (_, b), ...}) => fn intros => (b @ intros))
  20.545 +    (#2 (GlobalLocalesData.get thy)) [];
  20.546 +
  20.547 +fun all_witnesses ctxt =
  20.548 +  let
  20.549 +    val thy = ProofContext.theory_of ctxt;
  20.550 +    fun get registrations = Symtab.fold (fn (_, regs) => fn thms =>
  20.551 +        (Registrations.dest regs |> map (fn (_, (_, wits)) =>
  20.552 +          map Element.conclude_witness wits) |> flat) @ thms)
  20.553 +      registrations [];
  20.554 +    val globals = get (#3 (GlobalLocalesData.get thy));
  20.555 +    val locals = get (LocalLocalesData.get ctxt);
  20.556 +  in globals @ locals end;
  20.557 +(* FIXME: proper varification *)
  20.558 +
  20.559 +in
  20.560 +
  20.561 +fun intro_locales_tac (ctxt, eager) facts st =
  20.562 +  let
  20.563 +    val wits = all_witnesses ctxt |> map Thm.varifyT;
  20.564 +    val thy = ProofContext.theory_of ctxt;
  20.565 +    val intros = locale_base_intros thy @ (if eager then locale_assm_intros thy else []);
  20.566 +  in
  20.567 +    (ALLGOALS (Method.insert_tac facts THEN'
  20.568 +        REPEAT_ALL_NEW (resolve_tac (wits @ intros)))
  20.569 +      THEN Tactic.distinct_subgoals_tac) st
  20.570 +  end;
  20.571 +
  20.572 +val _ = Context.add_setup (Method.add_methods
  20.573 +  [("intro_locales",
  20.574 +    fn src => fn ctxt => Method.METHOD (intro_locales_tac
  20.575 +      (Method.syntax (Scan.lift (Scan.optional (Args.bang >> K false) true)) src ctxt)),
  20.576 +    "back-chain introduction rules of locales and discharge goals with interpretations")]);
  20.577 +
  20.578 +end;
  20.579 +
  20.580  
  20.581  (** Interpretation commands **)
  20.582  
  20.583 @@ -1941,7 +2040,7 @@
  20.584          (* add witnesses of Derived elements *)
  20.585          |> fold (fn (id, thms) => fold (add_wit id o Element.satisfy_witness prems) thms)
  20.586             (map_filter (fn ((_, Assumed _), _) => NONE
  20.587 -              | ((id, Derived thms), _) => SOME (id, thms)) all_elemss)
  20.588 +              | ((id, Derived thms), _) => SOME (id, thms)) new_elemss)
  20.589  
  20.590        val disch' = std o Element.satisfy_thm prems;  (* FIXME *)
  20.591      in
  20.592 @@ -1957,7 +2056,7 @@
  20.593        Attrib.attribute_i Drule.standard
  20.594        (fn (name, ps) => put_global_registration (name, map Logic.varify ps))
  20.595        (fn (n, ps) => add_global_witness (n, map Logic.varify ps) o
  20.596 -        Element.map_witness (fn (t, th) => (Logic.legacy_unvarify t, Drule.unvarify th))
  20.597 +        Element.map_witness (fn (t, th) => (Logic.legacy_unvarify t, legacy_unvarify th))
  20.598          (* FIXME *)) x;
  20.599  
  20.600  fun local_activate_facts_elemss x = gen_activate_facts_elemss
  20.601 @@ -2041,9 +2140,10 @@
  20.602      (* restore "small" ids *)
  20.603      val ids' = map (fn ((n, ps), (_, mode)) =>
  20.604            ((n, map (fn p => Free (p, (the o AList.lookup (op =) parms) p)) ps), mode))
  20.605 -        (params_ids @ ids);
  20.606 +        ids;
  20.607 +    val (_, all_elemss') = chop (length raw_params_elemss) all_elemss
  20.608      (* instantiate ids and elements *)
  20.609 -    val inst_elemss = (ids' ~~ all_elemss) |> map (fn (((n, ps), _), ((_, mode), elems)) =>
  20.610 +    val inst_elemss = (ids' ~~ all_elemss') |> map (fn (((n, ps), _), ((_, mode), elems)) =>
  20.611        ((n, map (Element.inst_term insts) ps),
  20.612          map (fn Int e => Element.inst_ctxt thy insts e) elems)
  20.613        |> apfst (fn id => (id, map_mode (map (Element.inst_witness thy insts)) mode)));
    21.1 --- a/src/ZF/Constructible/DPow_absolute.thy	Tue Jun 20 14:51:59 2006 +0200
    21.2 +++ b/src/ZF/Constructible/DPow_absolute.thy	Tue Jun 20 15:53:44 2006 +0200
    21.3 @@ -294,7 +294,7 @@
    21.4  
    21.5  theorem M_DPow_L: "PROP M_DPow(L)"
    21.6    apply (rule M_DPow.intro)
    21.7 -       apply (rule M_satisfies.axioms [OF M_satisfies_L])+
    21.8 +   apply (rule M_satisfies_L)
    21.9    apply (rule M_DPow_axioms_L)
   21.10    done
   21.11  
   21.12 @@ -596,10 +596,10 @@
   21.13    done
   21.14  
   21.15  theorem M_Lset_L: "PROP M_Lset(L)"
   21.16 -apply (rule M_Lset.intro) 
   21.17 -     apply (rule M_DPow.axioms [OF M_DPow_L])+
   21.18 -apply (rule M_Lset_axioms_L) 
   21.19 -done
   21.20 +  apply (rule M_Lset.intro) 
   21.21 +   apply (rule M_DPow_L)
   21.22 +  apply (rule M_Lset_axioms_L) 
   21.23 +  done
   21.24  
   21.25  text{*Finally: the point of the whole theory!*}
   21.26  lemmas Lset_closed = M_Lset.Lset_closed [OF M_Lset_L]
    22.1 --- a/src/ZF/Constructible/Rank_Separation.thy	Tue Jun 20 14:51:59 2006 +0200
    22.2 +++ b/src/ZF/Constructible/Rank_Separation.thy	Tue Jun 20 15:53:44 2006 +0200
    22.3 @@ -122,10 +122,10 @@
    22.4    done
    22.5  
    22.6  theorem M_ordertype_L: "PROP M_ordertype(L)"
    22.7 -apply (rule M_ordertype.intro)
    22.8 -     apply (rule M_basic.axioms [OF M_basic_L])+
    22.9 -apply (rule M_ordertype_axioms_L) 
   22.10 -done
   22.11 +  apply (rule M_ordertype.intro)
   22.12 +   apply (rule M_basic_L)
   22.13 +  apply (rule M_ordertype_axioms_L) 
   22.14 +  done
   22.15  
   22.16  
   22.17  subsection{*The Locale @{text "M_wfrank"}*}
   22.18 @@ -224,7 +224,7 @@
   22.19  
   22.20  theorem M_wfrank_L: "PROP M_wfrank(L)"
   22.21    apply (rule M_wfrank.intro)
   22.22 -     apply (rule M_trancl.axioms [OF M_trancl_L])+
   22.23 +   apply (rule M_trancl_L)
   22.24    apply (rule M_wfrank_axioms_L) 
   22.25    done
   22.26  
    23.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Tue Jun 20 14:51:59 2006 +0200
    23.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Tue Jun 20 15:53:44 2006 +0200
    23.3 @@ -181,10 +181,9 @@
    23.4    done
    23.5  
    23.6  theorem M_trancl_L: "PROP M_trancl(L)"
    23.7 -by (rule M_trancl.intro
    23.8 -         [OF M_trivial_L M_basic_axioms_L M_trancl_axioms_L])
    23.9 +by (rule M_trancl.intro [OF M_basic_L M_trancl_axioms_L])
   23.10  
   23.11 -interpretation M_trancl [L] by (rule M_trancl_axioms_L)
   23.12 +interpretation M_trancl [L] by (rule M_trancl_L)
   23.13  
   23.14  
   23.15  subsection{*@{term L} is Closed Under the Operator @{term list}*}
   23.16 @@ -366,11 +365,11 @@
   23.17  
   23.18  theorem M_datatypes_L: "PROP M_datatypes(L)"
   23.19    apply (rule M_datatypes.intro)
   23.20 -      apply (rule M_trancl.axioms [OF M_trancl_L])+
   23.21 - apply (rule M_datatypes_axioms_L) 
   23.22 - done
   23.23 +   apply (rule M_trancl_L)
   23.24 +  apply (rule M_datatypes_axioms_L) 
   23.25 +  done
   23.26  
   23.27 -interpretation M_datatypes [L] by (rule M_datatypes_axioms_L)
   23.28 +interpretation M_datatypes [L] by (rule M_datatypes_L)
   23.29  
   23.30  
   23.31  subsection{*@{term L} is Closed Under the Operator @{term eclose}*}
   23.32 @@ -429,11 +428,11 @@
   23.33  
   23.34  theorem M_eclose_L: "PROP M_eclose(L)"
   23.35    apply (rule M_eclose.intro)
   23.36 -       apply (rule M_datatypes.axioms [OF M_datatypes_L])+
   23.37 +   apply (rule M_datatypes_L)
   23.38    apply (rule M_eclose_axioms_L)
   23.39    done
   23.40  
   23.41 -interpretation M_eclose [L] by (rule M_eclose_axioms_L)
   23.42 +interpretation M_eclose [L] by (rule M_eclose_L)
   23.43  
   23.44  
   23.45  end
    24.1 --- a/src/ZF/Constructible/Satisfies_absolute.thy	Tue Jun 20 14:51:59 2006 +0200
    24.2 +++ b/src/ZF/Constructible/Satisfies_absolute.thy	Tue Jun 20 15:53:44 2006 +0200
    24.3 @@ -473,9 +473,10 @@
    24.4  			 satisfies_b(A), satisfies_is_b(M,A), 
    24.5  			 satisfies_c(A), satisfies_is_c(M,A), 
    24.6  			 satisfies_d(A), satisfies_is_d(M,A))"
    24.7 -apply (rule Formula_Rec.intro, assumption+)
    24.8 -apply (erule Formula_Rec_axioms_M) 
    24.9 -done
   24.10 +  apply (rule Formula_Rec.intro)
   24.11 +   apply (rule M_satisfies.axioms) apply assumption
   24.12 +  apply (erule Formula_Rec_axioms_M) 
   24.13 +  done
   24.14  
   24.15  lemmas (in M_satisfies) 
   24.16      satisfies_closed' = Formula_Rec.formula_rec_closed [OF Formula_Rec_M]
   24.17 @@ -1010,10 +1011,10 @@
   24.18    done
   24.19  
   24.20  theorem M_satisfies_L: "PROP M_satisfies(L)"
   24.21 -apply (rule M_satisfies.intro) 
   24.22 -     apply (rule M_eclose.axioms [OF M_eclose_L])+
   24.23 -apply (rule M_satisfies_axioms_L) 
   24.24 -done
   24.25 +  apply (rule M_satisfies.intro)
   24.26 +   apply (rule M_eclose_L)
   24.27 +  apply (rule M_satisfies_axioms_L)
   24.28 +  done
   24.29  
   24.30  text{*Finally: the point of the whole theory!*}
   24.31  lemmas satisfies_closed = M_satisfies.satisfies_closed [OF M_satisfies_L]
    25.1 --- a/src/ZF/Constructible/Separation.thy	Tue Jun 20 14:51:59 2006 +0200
    25.2 +++ b/src/ZF/Constructible/Separation.thy	Tue Jun 20 15:53:44 2006 +0200
    25.3 @@ -305,7 +305,7 @@
    25.4  theorem M_basic_L: "PROP M_basic(L)"
    25.5  by (rule M_basic.intro [OF M_trivial_L M_basic_axioms_L])
    25.6  
    25.7 -interpretation M_basic [L] by (rule M_basic_axioms_L)
    25.8 +interpretation M_basic [L] by (rule M_basic_L)
    25.9  
   25.10  
   25.11  end
    26.1 --- a/src/ZF/ex/Group.thy	Tue Jun 20 14:51:59 2006 +0200
    26.2 +++ b/src/ZF/ex/Group.thy	Tue Jun 20 15:53:44 2006 +0200
    26.3 @@ -89,8 +89,7 @@
    26.4    assumes inv_ex:
    26.5       "\<And>x. x \<in> carrier(G) \<Longrightarrow> \<exists>y \<in> carrier(G). y \<cdot> x = \<one> & x \<cdot> y = \<one>"
    26.6  
    26.7 -lemma (in group) is_group [simp]: "group(G)"
    26.8 -  by (rule group.intro [OF prems]) 
    26.9 +lemma (in group) is_group [simp]: "group(G)" .
   26.10  
   26.11  theorem groupI:
   26.12    includes struct G
   26.13 @@ -328,7 +327,7 @@
   26.14        and h: "h \<in> carrier(H)"
   26.15    shows "inv \<^bsub>G \<Otimes> H\<^esub> <g, h> = <inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h>"
   26.16    apply (rule group.inv_equality [OF DirProdGroup_group])
   26.17 -  apply (simp_all add: prems group_def group.l_inv)
   26.18 +  apply (simp_all add: prems group.l_inv)
   26.19    done
   26.20  
   26.21  subsection {* Isomorphisms *}
   26.22 @@ -636,8 +635,7 @@
   26.23  
   26.24  lemma (in group) normalI: 
   26.25    "subgroup(H,G) \<Longrightarrow> (\<forall>x \<in> carrier(G). H #> x = x <# H) \<Longrightarrow> H \<lhd> G";
   26.26 -apply (simp add: normal_def normal_axioms_def, auto) 
   26.27 -  by (blast intro: prems)
   26.28 +  by (simp add: normal_def normal_axioms_def)
   26.29  
   26.30  lemma (in normal) inv_op_closed1:
   26.31       "\<lbrakk>x \<in> carrier(G); h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<cdot> h \<cdot> x \<in> H"
   26.32 @@ -822,8 +820,8 @@
   26.33  lemma (in normal) rcos_mult_step3:
   26.34       "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk>
   26.35        \<Longrightarrow> (H <#> (H #> x)) #> y = H #> (x \<cdot> y)"
   26.36 -by (simp add: setmult_rcos_assoc coset_mult_assoc
   26.37 -              subgroup_mult_id subset prems)
   26.38 +  by (simp add: setmult_rcos_assoc coset_mult_assoc
   26.39 +              subgroup_mult_id subset prems normal.axioms)
   26.40  
   26.41  lemma (in normal) rcos_sum:
   26.42       "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk>
   26.43 @@ -833,7 +831,7 @@
   26.44  lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M"
   26.45    -- {* generalizes @{text subgroup_mult_id} *}
   26.46    by (auto simp add: RCOSETS_def subset
   26.47 -        setmult_rcos_assoc subgroup_mult_id prems)
   26.48 +        setmult_rcos_assoc subgroup_mult_id prems normal.axioms)
   26.49  
   26.50  
   26.51  subsubsection{*Two distinct right cosets are disjoint*}
   26.52 @@ -1008,7 +1006,7 @@
   26.53  
   26.54  lemma (in normal) rcosets_inv_mult_group_eq:
   26.55       "M \<in> rcosets H \<Longrightarrow> set_inv M <#> M = H"
   26.56 -by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset prems)
   26.57 +by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset prems normal.axioms)
   26.58  
   26.59  theorem (in normal) factorgroup_is_group:
   26.60    "group (G Mod H)"