Merged.
authorballarin
Fri Dec 19 15:05:37 2008 +0100 (2008-12-19)
changeset 29248f1f1bccf2fc5
parent 29247 95d3a82857e5
parent 29246 3593802c9cf1
child 29249 4dc278c8dc59
Merged.
src/HOL/Statespace/StateSpaceEx.thy
src/Pure/Isar/expression.ML
     1.1 --- a/src/FOL/ex/NewLocaleTest.thy	Thu Dec 18 11:16:48 2008 +0100
     1.2 +++ b/src/FOL/ex/NewLocaleTest.thy	Fri Dec 19 15:05:37 2008 +0100
     1.3 @@ -164,6 +164,9 @@
     1.4    assumes semi_homh: "semi_hom(prod, sum, h)"
     1.5    notes semi_hom_mult = semi_hom_mult [OF semi_homh]
     1.6  
     1.7 +thm semi_hom_loc.semi_hom_mult
     1.8 +(* unspecified, attribute not applied in backgroud theory !!! *)
     1.9 +
    1.10  lemma (in semi_hom_loc) "h(prod(x, y)) = sum(h(x), h(y))"
    1.11    by (rule semi_hom_mult)
    1.12  
     2.1 --- a/src/HOL/Algebra/Group.thy	Thu Dec 18 11:16:48 2008 +0100
     2.2 +++ b/src/HOL/Algebra/Group.thy	Fri Dec 19 15:05:37 2008 +0100
     2.3 @@ -541,15 +541,6 @@
     2.4      {h. h \<in> carrier G -> carrier H &
     2.5        (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y)}"
     2.6  
     2.7 -lemma hom_mult:
     2.8 -  "[| h \<in> hom G H; x \<in> carrier G; y \<in> carrier G |]
     2.9 -   ==> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
    2.10 -  by (simp add: hom_def)
    2.11 -
    2.12 -lemma hom_closed:
    2.13 -  "[| h \<in> hom G H; x \<in> carrier G |] ==> h x \<in> carrier H"
    2.14 -  by (auto simp add: hom_def funcset_mem)
    2.15 -
    2.16  lemma (in group) hom_compose:
    2.17       "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
    2.18  apply (auto simp add: hom_def funcset_compose) 
    2.19 @@ -589,8 +580,20 @@
    2.20  locale group_hom = G: group G + H: group H for G (structure) and H (structure) +
    2.21    fixes h
    2.22    assumes homh: "h \<in> hom G H"
    2.23 -  notes hom_mult [simp] = hom_mult [OF homh]
    2.24 -    and hom_closed [simp] = hom_closed [OF homh]
    2.25 +
    2.26 +lemma (in group_hom) hom_mult [simp]:
    2.27 +  "[| x \<in> carrier G; y \<in> carrier G |] ==> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
    2.28 +proof -
    2.29 +  assume "x \<in> carrier G" "y \<in> carrier G"
    2.30 +  with homh [unfolded hom_def] show ?thesis by simp
    2.31 +qed
    2.32 +
    2.33 +lemma (in group_hom) hom_closed [simp]:
    2.34 +  "x \<in> carrier G ==> h x \<in> carrier H"
    2.35 +proof -
    2.36 +  assume "x \<in> carrier G"
    2.37 +  with homh [unfolded hom_def] show ?thesis by (auto simp add: funcset_mem)
    2.38 +qed
    2.39  
    2.40  lemma (in group_hom) one_closed [simp]:
    2.41    "h \<one> \<in> carrier H"
     3.1 --- a/src/HOL/Algebra/Ideal.thy	Thu Dec 18 11:16:48 2008 +0100
     3.2 +++ b/src/HOL/Algebra/Ideal.thy	Fri Dec 19 15:05:37 2008 +0100
     3.3 @@ -13,7 +13,7 @@
     3.4  
     3.5  subsubsection {* General definition *}
     3.6  
     3.7 -locale ideal = additive_subgroup I R + ring R +
     3.8 +locale ideal = additive_subgroup I R + ring R for I and R (structure) +
     3.9    assumes I_l_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
    3.10        and I_r_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
    3.11  
    3.12 @@ -127,7 +127,7 @@
    3.13        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"
    3.14    shows "primeideal I R"
    3.15  proof -
    3.16 -  interpret additive_subgroup [I R] by fact
    3.17 +  interpret additive_subgroup I R by fact
    3.18    interpret cring R by fact
    3.19    show ?thesis apply (intro_locales)
    3.20      apply (intro ideal_axioms.intro)
    3.21 @@ -207,7 +207,7 @@
    3.22    shows "ideal (I \<inter> J) R"
    3.23  proof -
    3.24    interpret ideal I R by fact
    3.25 -  interpret ideal [J R] by fact
    3.26 +  interpret ideal J R by fact
    3.27    show ?thesis
    3.28  apply (intro idealI subgroup.intro)
    3.29        apply (rule is_ring)
    3.30 @@ -532,7 +532,7 @@
    3.31    assumes aJ: "a \<in> J"
    3.32    shows "PIdl a \<subseteq> J"
    3.33  proof -
    3.34 -  interpret ideal [J R] by fact
    3.35 +  interpret ideal J R by fact
    3.36    show ?thesis unfolding cgenideal_def
    3.37      apply rule
    3.38      apply clarify
    3.39 @@ -579,7 +579,7 @@
    3.40    shows "Idl (I \<union> J) = I <+> J"
    3.41  apply rule
    3.42   apply (rule ring.genideal_minimal)
    3.43 -   apply (rule R.is_ring)
    3.44 +   apply (rule is_ring)
    3.45    apply (rule add_ideals[OF idealI idealJ])
    3.46   apply (rule)
    3.47   apply (simp add: set_add_defs) apply (elim disjE) defer 1 defer 1
    3.48 @@ -829,7 +829,7 @@
    3.49        by fast
    3.50      def J \<equiv> "{x\<in>carrier R. a \<otimes> x \<in> I}"
    3.51      
    3.52 -    from R.is_cring and acarr
    3.53 +    from is_cring and acarr
    3.54      have idealJ: "ideal J R" unfolding J_def by (rule helper_max_prime)
    3.55      
    3.56      have IsubJ: "I \<subseteq> J"
     4.1 --- a/src/HOL/Algebra/IntRing.thy	Thu Dec 18 11:16:48 2008 +0100
     4.2 +++ b/src/HOL/Algebra/IntRing.thy	Fri Dec 19 15:05:37 2008 +0100
     4.3 @@ -328,7 +328,7 @@
     4.4  next
     4.5    assume "UNIV = {uu. EX x. uu = x * p}"
     4.6    from this obtain x 
     4.7 -      where "1 = x * p" by fast
     4.8 +      where "1 = x * p" by best
     4.9    from this [symmetric]
    4.10        have "p * x = 1" by (subst zmult_commute)
    4.11    hence "\<bar>p * x\<bar> = 1" by simp
     5.1 --- a/src/HOL/Algebra/Lattice.thy	Thu Dec 18 11:16:48 2008 +0100
     5.2 +++ b/src/HOL/Algebra/Lattice.thy	Fri Dec 19 15:05:37 2008 +0100
     5.3 @@ -919,7 +919,7 @@
     5.4  
     5.5  text {* Total orders are lattices. *}
     5.6  
     5.7 -sublocale weak_total_order < weak_lattice
     5.8 +sublocale weak_total_order < weak: weak_lattice
     5.9  proof
    5.10    fix x y
    5.11    assume L: "x \<in> carrier L"  "y \<in> carrier L"
    5.12 @@ -1125,14 +1125,14 @@
    5.13    assumes sup_of_two_exists:
    5.14      "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
    5.15  
    5.16 -sublocale upper_semilattice < weak_upper_semilattice
    5.17 +sublocale upper_semilattice < weak: weak_upper_semilattice
    5.18    proof qed (rule sup_of_two_exists)
    5.19  
    5.20  locale lower_semilattice = partial_order +
    5.21    assumes inf_of_two_exists:
    5.22      "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
    5.23  
    5.24 -sublocale lower_semilattice < weak_lower_semilattice
    5.25 +sublocale lower_semilattice < weak: weak_lower_semilattice
    5.26    proof qed (rule inf_of_two_exists)
    5.27  
    5.28  locale lattice = upper_semilattice + lower_semilattice
    5.29 @@ -1183,7 +1183,7 @@
    5.30  locale total_order = partial_order +
    5.31    assumes total_order_total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
    5.32  
    5.33 -sublocale total_order < weak_total_order
    5.34 +sublocale total_order < weak: weak_total_order
    5.35    proof qed (rule total_order_total)
    5.36  
    5.37  text {* Introduction rule: the usual definition of total order *}
    5.38 @@ -1195,7 +1195,7 @@
    5.39  
    5.40  text {* Total orders are lattices. *}
    5.41  
    5.42 -sublocale total_order < lattice
    5.43 +sublocale total_order < weak: lattice
    5.44    proof qed (auto intro: sup_of_two_exists inf_of_two_exists)
    5.45  
    5.46  
    5.47 @@ -1207,7 +1207,7 @@
    5.48      and inf_exists:
    5.49      "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
    5.50  
    5.51 -sublocale complete_lattice < weak_complete_lattice
    5.52 +sublocale complete_lattice < weak: weak_complete_lattice
    5.53    proof qed (auto intro: sup_exists inf_exists)
    5.54  
    5.55  text {* Introduction rule: the usual definition of complete lattice *}
     6.1 --- a/src/HOL/Algebra/QuotRing.thy	Thu Dec 18 11:16:48 2008 +0100
     6.2 +++ b/src/HOL/Algebra/QuotRing.thy	Fri Dec 19 15:05:37 2008 +0100
     6.3 @@ -175,9 +175,9 @@
     6.4    interpret cring R by fact
     6.5    show ?thesis apply (rule ring_hom_cringI)
     6.6    apply (rule rcos_ring_hom_ring)
     6.7 - apply (rule R.is_cring)
     6.8 + apply (rule is_cring)
     6.9  apply (rule quotient_is_cring)
    6.10 -apply (rule R.is_cring)
    6.11 +apply (rule is_cring)
    6.12  done
    6.13  qed
    6.14  
     7.1 --- a/src/HOL/Algebra/RingHom.thy	Thu Dec 18 11:16:48 2008 +0100
     7.2 +++ b/src/HOL/Algebra/RingHom.thy	Fri Dec 19 15:05:37 2008 +0100
     7.3 @@ -10,16 +10,17 @@
     7.4  section {* Homomorphisms of Non-Commutative Rings *}
     7.5  
     7.6  text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *}
     7.7 -locale ring_hom_ring = R: ring R + S: ring S +
     7.8 +locale ring_hom_ring = R: ring R + S: ring S
     7.9 +    for R (structure) and S (structure) +
    7.10    fixes h
    7.11    assumes homh: "h \<in> ring_hom R S"
    7.12    notes hom_mult [simp] = ring_hom_mult [OF homh]
    7.13      and hom_one [simp] = ring_hom_one [OF homh]
    7.14  
    7.15 -sublocale ring_hom_cring \<subseteq> ring_hom_ring
    7.16 +sublocale ring_hom_cring \<subseteq> ring: ring_hom_ring
    7.17    proof qed (rule homh)
    7.18  
    7.19 -sublocale ring_hom_ring \<subseteq> abelian_group_hom R S
    7.20 +sublocale ring_hom_ring \<subseteq> abelian_group: abelian_group_hom R S
    7.21  apply (rule abelian_group_homI)
    7.22    apply (rule R.is_abelian_group)
    7.23   apply (rule S.is_abelian_group)
     8.1 --- a/src/HOL/Algebra/UnivPoly.thy	Thu Dec 18 11:16:48 2008 +0100
     8.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Fri Dec 19 15:05:37 2008 +0100
     8.3 @@ -175,17 +175,17 @@
     8.4    fixes R (structure) and P (structure)
     8.5    defines P_def: "P == UP R"
     8.6  
     8.7 -locale UP_ring = UP + ring R
     8.8 +locale UP_ring = UP + R: ring R
     8.9  
    8.10 -locale UP_cring = UP + cring R
    8.11 +locale UP_cring = UP + R: cring R
    8.12  
    8.13  sublocale UP_cring < UP_ring
    8.14 -  by (rule P_def) intro_locales
    8.15 +  by intro_locales [1] (rule P_def)
    8.16  
    8.17 -locale UP_domain = UP + "domain" R
    8.18 +locale UP_domain = UP + R: "domain" R
    8.19  
    8.20  sublocale UP_domain < UP_cring
    8.21 -  by (rule P_def) intro_locales
    8.22 +  by intro_locales [1] (rule P_def)
    8.23  
    8.24  context UP
    8.25  begin
    8.26 @@ -457,8 +457,8 @@
    8.27  
    8.28  end
    8.29  
    8.30 -sublocale UP_ring < ring P using UP_ring .
    8.31 -sublocale UP_cring < cring P using UP_cring .
    8.32 +sublocale UP_ring < P: ring P using UP_ring .
    8.33 +sublocale UP_cring < P: cring P using UP_cring .
    8.34  
    8.35  
    8.36  subsection {* Polynomials Form an Algebra *}
    8.37 @@ -1203,7 +1203,9 @@
    8.38  
    8.39  text {* The universal property of the polynomial ring *}
    8.40  
    8.41 -locale UP_pre_univ_prop = ring_hom_cring R S h + UP_cring R P
    8.42 +locale UP_pre_univ_prop = ring_hom_cring + UP_cring
    8.43 +
    8.44 +(* FIXME print_locale ring_hom_cring fails *)
    8.45  
    8.46  locale UP_univ_prop = UP_pre_univ_prop +
    8.47    fixes s and Eval
    8.48 @@ -1771,7 +1773,7 @@
    8.49    shows "eval R R id a (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0) = \<zero>"
    8.50    (is "eval R R id a ?g = _")
    8.51  proof -
    8.52 -  interpret UP_pre_univ_prop R R id P proof qed simp
    8.53 +  interpret UP_pre_univ_prop R R id proof qed simp
    8.54    have eval_ring_hom: "eval R R id a \<in> ring_hom P R" using eval_ring_hom [OF a] by simp
    8.55    interpret ring_hom_cring P R "eval R R id a" proof qed (simp add: eval_ring_hom)
    8.56    have mon1_closed: "monom P \<one>\<^bsub>R\<^esub> 1 \<in> carrier P" 
    8.57 @@ -1780,8 +1782,8 @@
    8.58      using a R.a_inv_closed by auto
    8.59    have "eval R R id a ?g = eval R R id a (monom P \<one> 1) \<ominus> eval R R id a (monom P a 0)"
    8.60      unfolding P.minus_eq [OF mon1_closed mon0_closed]
    8.61 -    unfolding R_S_h.hom_add [OF mon1_closed min_mon0_closed]
    8.62 -    unfolding R_S_h.hom_a_inv [OF mon0_closed] 
    8.63 +    unfolding hom_add [OF mon1_closed min_mon0_closed]
    8.64 +    unfolding hom_a_inv [OF mon0_closed] 
    8.65      using R.minus_eq [symmetric] mon1_closed mon0_closed by auto
    8.66    also have "\<dots> = a \<ominus> a"
    8.67      using eval_monom [OF R.one_closed a, of 1] using eval_monom [OF a a, of 0] using a by simp
    8.68 @@ -1884,7 +1886,7 @@
    8.69    "UP INTEG"} globally.
    8.70  *}
    8.71  
    8.72 -interpretation INTEG!: UP_pre_univ_prop INTEG INTEG id
    8.73 +interpretation INTEG!: UP_pre_univ_prop INTEG INTEG id "UP INTEG"
    8.74    using INTEG_id_eval by simp_all
    8.75  
    8.76  lemma INTEG_closed [intro, simp]:
     9.1 --- a/src/HOL/Statespace/StateSpaceEx.thy	Thu Dec 18 11:16:48 2008 +0100
     9.2 +++ b/src/HOL/Statespace/StateSpaceEx.thy	Fri Dec 19 15:05:37 2008 +0100
     9.3 @@ -202,8 +202,10 @@
     9.4  
     9.5  text {* Hmm, I hoped this would work now...*}
     9.6  
     9.7 +(*
     9.8  locale fooX = foo +
     9.9   assumes "s<a:=i>\<cdot>b = k"
    9.10 +*)
    9.11  
    9.12  (* ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ *)
    9.13  text {* There are known problems with syntax-declarations. They currently
    10.1 --- a/src/HOLCF/CompactBasis.thy	Thu Dec 18 11:16:48 2008 +0100
    10.2 +++ b/src/HOLCF/CompactBasis.thy	Fri Dec 19 15:05:37 2008 +0100
    10.3 @@ -244,7 +244,7 @@
    10.4    assumes "ab_semigroup_idem_mult f"
    10.5    shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
    10.6  proof -
    10.7 -  interpret ab_semigroup_idem_mult f by fact
    10.8 +  class_interpret ab_semigroup_idem_mult [f] by fact
    10.9    show ?thesis unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2)
   10.10  qed
   10.11  
    11.1 --- a/src/HOLCF/ConvexPD.thy	Thu Dec 18 11:16:48 2008 +0100
    11.2 +++ b/src/HOLCF/ConvexPD.thy	Fri Dec 19 15:05:37 2008 +0100
    11.3 @@ -296,7 +296,7 @@
    11.4  apply (simp add: PDPlus_absorb)
    11.5  done
    11.6  
    11.7 -interpretation aci_convex_plus!: ab_semigroup_idem_mult "op +\<natural>"
    11.8 +class_interpretation aci_convex_plus: ab_semigroup_idem_mult ["op +\<natural>"]
    11.9    by unfold_locales
   11.10      (rule convex_plus_assoc convex_plus_commute convex_plus_absorb)+
   11.11  
    12.1 --- a/src/HOLCF/LowerPD.thy	Thu Dec 18 11:16:48 2008 +0100
    12.2 +++ b/src/HOLCF/LowerPD.thy	Fri Dec 19 15:05:37 2008 +0100
    12.3 @@ -250,7 +250,7 @@
    12.4  apply (simp add: PDPlus_absorb)
    12.5  done
    12.6  
    12.7 -interpretation aci_lower_plus!: ab_semigroup_idem_mult "op +\<flat>"
    12.8 +class_interpretation aci_lower_plus: ab_semigroup_idem_mult ["op +\<flat>"]
    12.9    by unfold_locales
   12.10      (rule lower_plus_assoc lower_plus_commute lower_plus_absorb)+
   12.11  
    13.1 --- a/src/HOLCF/UpperPD.thy	Thu Dec 18 11:16:48 2008 +0100
    13.2 +++ b/src/HOLCF/UpperPD.thy	Fri Dec 19 15:05:37 2008 +0100
    13.3 @@ -248,7 +248,7 @@
    13.4  apply (simp add: PDPlus_absorb)
    13.5  done
    13.6  
    13.7 -interpretation aci_upper_plus!: ab_semigroup_idem_mult "op +\<sharp>"
    13.8 +class_interpretation aci_upper_plus: ab_semigroup_idem_mult ["op +\<sharp>"]
    13.9    by unfold_locales
   13.10      (rule upper_plus_assoc upper_plus_commute upper_plus_absorb)+
   13.11  
    14.1 --- a/src/Pure/Isar/expression.ML	Thu Dec 18 11:16:48 2008 +0100
    14.2 +++ b/src/Pure/Isar/expression.ML	Fri Dec 19 15:05:37 2008 +0100
    14.3 @@ -271,38 +271,7 @@
    14.4    | declare_elem _ (Defines _) ctxt = ctxt
    14.5    | declare_elem _ (Notes _) ctxt = ctxt;
    14.6  
    14.7 -(** Finish locale elements, extract specification text **)
    14.8 -
    14.9 -val norm_term = Envir.beta_norm oo Term.subst_atomic;
   14.10 -
   14.11 -fun bind_def ctxt eq (xs, env, eqs) =
   14.12 -  let
   14.13 -    val _ = LocalDefs.cert_def ctxt eq;
   14.14 -    val ((y, T), b) = LocalDefs.abs_def eq;
   14.15 -    val b' = norm_term env b;
   14.16 -    fun err msg = error (msg ^ ": " ^ quote y);
   14.17 -  in
   14.18 -    exists (fn (x, _) => x = y) xs andalso
   14.19 -      err "Attempt to define previously specified variable";
   14.20 -    exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso
   14.21 -      err "Attempt to redefine variable";
   14.22 -    (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs)
   14.23 -  end;
   14.24 -
   14.25 -fun eval_text _ _ (Fixes _) text = text
   14.26 -  | eval_text _ _ (Constrains _) text = text
   14.27 -  | eval_text _ is_ext (Assumes asms)
   14.28 -        (((exts, exts'), (ints, ints')), (xs, env, defs)) =
   14.29 -      let
   14.30 -        val ts = maps (map #1 o #2) asms;
   14.31 -        val ts' = map (norm_term env) ts;
   14.32 -        val spec' =
   14.33 -          if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
   14.34 -          else ((exts, exts'), (ints @ ts, ints' @ ts'));
   14.35 -      in (spec', (fold Term.add_frees ts' xs, env, defs)) end
   14.36 -  | eval_text ctxt _ (Defines defs) (spec, binds) =
   14.37 -      (spec, fold (bind_def ctxt o #1 o #2) defs binds)
   14.38 -  | eval_text _ _ (Notes _) text = text;
   14.39 +(** Finish locale elements **)
   14.40  
   14.41  fun closeup _ _ false elem = elem
   14.42    | closeup ctxt parms true elem =
   14.43 @@ -337,36 +306,24 @@
   14.44    | finish_primitive _ close (Defines defs) = close (Defines defs)
   14.45    | finish_primitive _ _ (Notes facts) = Notes facts;
   14.46  
   14.47 -fun finish_inst ctxt parms do_close (loc, (prfx, inst)) text =
   14.48 +fun finish_inst ctxt parms do_close (loc, (prfx, inst)) =
   14.49    let
   14.50      val thy = ProofContext.theory_of ctxt;
   14.51      val (parm_names, parm_types) = NewLocale.params_of thy loc |>
   14.52        map (fn (b, SOME T, _) => (Binding.base_name b, T)) |> split_list;
   14.53 -    val (asm, defs) = NewLocale.specification_of thy loc;
   14.54      val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
   14.55 -    val asm' = Option.map (Morphism.term morph) asm;
   14.56 -    val defs' = map (Morphism.term morph) defs;
   14.57 -    val text' = text |>
   14.58 -      (if is_some asm
   14.59 -        then eval_text ctxt false (Assumes [(Attrib.empty_binding, [(the asm', [])])])
   14.60 -        else I) |>
   14.61 -      (if not (null defs)
   14.62 -        then eval_text ctxt false (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs'))
   14.63 -        else I)
   14.64 -(* FIXME clone from new_locale.ML *)
   14.65 -  in ((loc, morph), text') end;
   14.66 +  in (loc, morph) end;
   14.67  
   14.68 -fun finish_elem ctxt parms do_close elem text =
   14.69 +fun finish_elem ctxt parms do_close elem =
   14.70    let
   14.71      val elem' = finish_primitive parms (closeup ctxt parms do_close) elem;
   14.72 -    val text' = eval_text ctxt true elem' text;
   14.73 -  in (elem', text') end
   14.74 +  in elem' end
   14.75    
   14.76 -fun finish ctxt parms do_close insts elems text =
   14.77 +fun finish ctxt parms do_close insts elems =
   14.78    let
   14.79 -    val (deps, text') = fold_map (finish_inst ctxt parms do_close) insts text;
   14.80 -    val (elems', text'') = fold_map (finish_elem ctxt parms do_close) elems text';
   14.81 -  in (deps, elems', text'') end;
   14.82 +    val deps = map (finish_inst ctxt parms do_close) insts;
   14.83 +    val elems' = map (finish_elem ctxt parms do_close) elems;
   14.84 +  in (deps, elems') end;
   14.85  
   14.86  
   14.87  (** Process full context statement: instantiations + elements + conclusion **)
   14.88 @@ -422,28 +379,9 @@
   14.89      val parms = xs ~~ Ts;  (* params from expression and elements *)
   14.90  
   14.91      val Fixes fors' = finish_primitive parms I (Fixes fors);
   14.92 -    val (deps, elems', text) = finish ctxt' parms do_close insts elems ((([], []), ([], [])), ([], [], []));
   14.93 -    (* text has the following structure:
   14.94 -           (((exts, exts'), (ints, ints')), (xs, env, defs))
   14.95 -       where
   14.96 -         exts: external assumptions (terms in assumes elements)
   14.97 -         exts': dito, normalised wrt. env
   14.98 -         ints: internal assumptions (terms in assumptions from insts)
   14.99 -         ints': dito, normalised wrt. env
  14.100 -         xs: the free variables in exts' and ints' and rhss of definitions,
  14.101 -           this includes parameters except defined parameters
  14.102 -         env: list of term pairs encoding substitutions, where the first term
  14.103 -           is a free variable; substitutions represent defines elements and
  14.104 -           the rhs is normalised wrt. the previous env
  14.105 -         defs: the equations from the defines elements
  14.106 -       elems is an updated version of raw_elems:
  14.107 -         - type info added to Fixes and modified in Constrains
  14.108 -         - axiom and definition statement replaced by corresponding one
  14.109 -           from proppss in Assumes and Defines
  14.110 -         - Facts unchanged
  14.111 -       *)
  14.112 +    val (deps, elems') = finish ctxt' parms do_close insts elems;
  14.113  
  14.114 -  in ((fors', deps, elems', concl), (parms, text)) end
  14.115 +  in ((fors', deps, elems', concl), (parms, ctxt')) end
  14.116  
  14.117  in
  14.118  
  14.119 @@ -480,14 +418,13 @@
  14.120  
  14.121  fun prep_declaration prep activate raw_import raw_elems context =
  14.122    let
  14.123 -    val ((fixed, deps, elems, _), (parms, (spec, (_, _, defs)))) =
  14.124 -      prep false true context raw_import raw_elems [];
  14.125 +    val ((fixed, deps, elems, _), (parms, ctxt')) = prep false true context raw_import raw_elems [];
  14.126      (* Declare parameters and imported facts *)
  14.127      val context' = context |>
  14.128        ProofContext.add_fixes_i fixed |> snd |>
  14.129        fold NewLocale.activate_local_facts deps;
  14.130      val (elems', _) = activate elems (ProofContext.set_stmt true context');
  14.131 -  in ((fixed, deps, elems'), (parms, spec, defs)) end;
  14.132 +  in ((fixed, deps, elems'), (parms, ctxt')) end;
  14.133  
  14.134  in
  14.135  
  14.136 @@ -522,8 +459,7 @@
  14.137  
  14.138      val export = Variable.export_morphism goal_ctxt context;
  14.139      val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
  14.140 -    val thy_ref = Theory.check_thy thy; (* FIXME!!*)
  14.141 -    val exp_term = (fn t => Drule.term_rule (Theory.deref thy_ref) (singleton exp_fact) t);
  14.142 +    val exp_term = TermSubst.zero_var_indexes o Morphism.term export;
  14.143      val exp_typ = Logic.type_map exp_term;
  14.144      val export' =
  14.145        Morphism.morphism {binding = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
  14.146 @@ -539,6 +475,81 @@
  14.147  
  14.148  (*** Locale declarations ***)
  14.149  
  14.150 +(* extract specification text *)
  14.151 +
  14.152 +val norm_term = Envir.beta_norm oo Term.subst_atomic;
  14.153 +
  14.154 +fun bind_def ctxt eq (xs, env, eqs) =
  14.155 +  let
  14.156 +    val _ = LocalDefs.cert_def ctxt eq;
  14.157 +    val ((y, T), b) = LocalDefs.abs_def eq;
  14.158 +    val b' = norm_term env b;
  14.159 +    fun err msg = error (msg ^ ": " ^ quote y);
  14.160 +  in
  14.161 +    exists (fn (x, _) => x = y) xs andalso
  14.162 +      err "Attempt to define previously specified variable";
  14.163 +    exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso
  14.164 +      err "Attempt to redefine variable";
  14.165 +    (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs)
  14.166 +  end;
  14.167 +
  14.168 +(* text has the following structure:
  14.169 +       (((exts, exts'), (ints, ints')), (xs, env, defs))
  14.170 +   where
  14.171 +     exts: external assumptions (terms in assumes elements)
  14.172 +     exts': dito, normalised wrt. env
  14.173 +     ints: internal assumptions (terms in assumptions from insts)
  14.174 +     ints': dito, normalised wrt. env
  14.175 +     xs: the free variables in exts' and ints' and rhss of definitions,
  14.176 +       this includes parameters except defined parameters
  14.177 +     env: list of term pairs encoding substitutions, where the first term
  14.178 +       is a free variable; substitutions represent defines elements and
  14.179 +       the rhs is normalised wrt. the previous env
  14.180 +     defs: the equations from the defines elements
  14.181 +   *)
  14.182 +
  14.183 +fun eval_text _ _ (Fixes _) text = text
  14.184 +  | eval_text _ _ (Constrains _) text = text
  14.185 +  | eval_text _ is_ext (Assumes asms)
  14.186 +        (((exts, exts'), (ints, ints')), (xs, env, defs)) =
  14.187 +      let
  14.188 +        val ts = maps (map #1 o #2) asms;
  14.189 +        val ts' = map (norm_term env) ts;
  14.190 +        val spec' =
  14.191 +          if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
  14.192 +          else ((exts, exts'), (ints @ ts, ints' @ ts'));
  14.193 +      in (spec', (fold Term.add_frees ts' xs, env, defs)) end
  14.194 +  | eval_text ctxt _ (Defines defs) (spec, binds) =
  14.195 +      (spec, fold (bind_def ctxt o #1 o #2) defs binds)
  14.196 +  | eval_text _ _ (Notes _) text = text;
  14.197 +
  14.198 +fun eval_inst ctxt (loc, morph) text =
  14.199 +  let
  14.200 +    val thy = ProofContext.theory_of ctxt;
  14.201 +    val (asm, defs) = NewLocale.specification_of thy loc;
  14.202 +    val asm' = Option.map (Morphism.term morph) asm;
  14.203 +    val defs' = map (Morphism.term morph) defs;
  14.204 +    val text' = text |>
  14.205 +      (if is_some asm
  14.206 +        then eval_text ctxt false (Assumes [(Attrib.empty_binding, [(the asm', [])])])
  14.207 +        else I) |>
  14.208 +      (if not (null defs)
  14.209 +        then eval_text ctxt false (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs'))
  14.210 +        else I)
  14.211 +(* FIXME clone from new_locale.ML *)
  14.212 +  in text' end;
  14.213 +
  14.214 +fun eval_elem ctxt elem text =
  14.215 +  let
  14.216 +    val text' = eval_text ctxt true elem text;
  14.217 +  in text' end;
  14.218 +
  14.219 +fun eval ctxt deps elems =
  14.220 +  let
  14.221 +    val text' = fold (eval_inst ctxt) deps ((([], []), ([], [])), ([], [], []));
  14.222 +    val ((spec, (_, _, defs))) = fold (eval_elem ctxt) elems text';
  14.223 +  in (spec, defs) end;
  14.224 +
  14.225  (* axiomsN: name of theorem set with destruct rules for locale predicates,
  14.226       also name suffix of delta predicates and assumptions. *)
  14.227  
  14.228 @@ -624,7 +635,7 @@
  14.229  
  14.230  (* CB: main predicate definition function *)
  14.231  
  14.232 -fun define_preds pname (parms, ((exts, exts'), (ints, ints')), defs) thy =
  14.233 +fun define_preds pname parms (((exts, exts'), (ints, ints')), defs) thy =
  14.234    let
  14.235      val defs' = map (cterm_of thy #> Assumption.assume #> Drule.gen_all #> Drule.abs_def) defs;
  14.236  
  14.237 @@ -677,7 +688,8 @@
  14.238  
  14.239  fun defines_to_notes thy (Defines defs) =
  14.240        Notes (Thm.definitionK, map (fn (a, (def, _)) =>
  14.241 -        (a, [([Assumption.assume (cterm_of thy def)], [])])) defs)
  14.242 +        (a, [([Assumption.assume (cterm_of thy def)],
  14.243 +          [(Attrib.internal o K) NewLocale.witness_attrib])])) defs)
  14.244    | defines_to_notes _ e = e;
  14.245  
  14.246  fun gen_add_locale prep_decl
  14.247 @@ -687,10 +699,12 @@
  14.248      val _ = NewLocale.test_locale thy name andalso
  14.249        error ("Duplicate definition of locale " ^ quote name);
  14.250  
  14.251 -    val ((fixed, deps, body_elems), text as (parms, ((_, exts'), _), defs)) =
  14.252 +    val ((fixed, deps, body_elems), (parms, ctxt')) =
  14.253        prep_decl raw_imprt raw_body (ProofContext.init thy);
  14.254 +    val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
  14.255 +
  14.256      val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
  14.257 -      define_preds predicate_name text thy;
  14.258 +      define_preds predicate_name parms text thy;
  14.259  
  14.260      val extraTs = fold Term.add_tfrees exts' [] \\ fold Term.add_tfreesT (map snd parms) [];
  14.261      val _ = if null extraTs then ()
    15.1 --- a/src/Pure/Isar/new_locale.ML	Thu Dec 18 11:16:48 2008 +0100
    15.2 +++ b/src/Pure/Isar/new_locale.ML	Fri Dec 19 15:05:37 2008 +0100
    15.3 @@ -375,8 +375,8 @@
    15.4      val ctxt = init name' thy
    15.5    in
    15.6      Pretty.big_list "locale elements:"
    15.7 -      (activate_all name' thy (cons_elem show_facts) (K Morphism.identity) (empty, []) |>
    15.8 -        snd |> rev |> 
    15.9 +      (activate_all name' thy (cons_elem show_facts) (K (Element.transfer_morphism thy))
   15.10 +        (empty, []) |> snd |> rev |> 
   15.11          map (Element.pretty_ctxt ctxt) |> map Pretty.chunks) |> Pretty.writeln
   15.12    end
   15.13  
   15.14 @@ -399,9 +399,15 @@
   15.15  
   15.16  val get_global_registrations =
   15.17    Context.Theory #> RegistrationsData.get #> map fst #> map (apsnd op $>);
   15.18 -fun add_global_registration reg =
   15.19 +
   15.20 +fun add_global reg =
   15.21    (Context.theory_map o RegistrationsData.map) (cons (reg, stamp ()));
   15.22  
   15.23 +fun add_global_registration (name, (base_morph, export)) thy =
   15.24 +  roundup thy (fn _ => fn (name', morph') => fn thy => add_global (name', (morph', export)) thy)
   15.25 +    (name, base_morph) (get_global_idents thy, thy) |>
   15.26 +    snd (* FIXME ?? uncurry put_global_idents *);
   15.27 +
   15.28  fun amend_global_registration morph (name, base_morph) thy =
   15.29    let
   15.30      val regs = (Context.Theory #> RegistrationsData.get #> map fst) thy;