# HG changeset patch
# User ballarin
# Date 1122994341 -7200
# Node ID 552df70f52c221c3a86e74c80e3cb9b2bbf9d1b8
# Parent  307b2ec590ffd5b7455cd74409e7fb7e52d01e83
First version of interpretation in locales.  Not yet fully functional.

diff -r 307b2ec590ff -r 552df70f52c2 src/FOL/ex/LocaleTest.thy
--- a/src/FOL/ex/LocaleTest.thy	Tue Aug 02 16:50:55 2005 +0200
+++ b/src/FOL/ex/LocaleTest.thy	Tue Aug 02 16:52:21 2005 +0200
@@ -17,159 +17,166 @@
 ML {* set show_hyps *}
 ML {* set show_sorts *}
 
-section {* Renaming with Syntax *}
+
+section {* Context Elements and Locale Expressions *}
 
+text {* Naming convention for global objects: prefixes L and l *}
 
-locale (open) S = var mult +
+subsection {* Renaming with Syntax *}
+
+locale (open) LS = var mult +
   assumes "mult(x, y) = mult(y, x)"
 
-print_locale S
+print_locale LS
 
-locale S' = S mult (infixl "**" 60)
+locale LS' = LS mult (infixl "**" 60)
 
-print_locale S'
+print_locale LS'
 
-locale T = var mult (infixl "**" 60) +
+locale LT = var mult (infixl "**" 60) +
   assumes "x ** y = y ** x"
 
-locale U = T mult (infixl "**" 60) + T add (infixl "++" 55) + var h +
+locale LU = LT mult (infixl "**" 60) + LT add (infixl "++" 55) + var h +
   assumes hom: "h(x ** y) = h(x) ++ h(y)"
 
-locale V = U _ add
+locale LV = LU _ add
 
 
-section {* Constrains *}
+subsection {* Constrains *}
 
-locale Z = fixes a (structure)
-locale Z' = Z +
+locale LZ = fixes a (structure)
+locale LZ' = LZ +
   constrains a :: "'a => 'b"
   assumes "a (x :: 'a) = a (y)"
-print_locale Z'
+print_locale LZ'
 
 
 section {* Interpretation *}
 
-(* interpretation input syntax *)
+text {* Naming convention for global objects: prefixes I and i *}
 
-locale L
-locale M = fixes a and b and c
+text {* interpretation input syntax *}
 
-interpretation test [simp]: L + M a b c [x y z] .
+locale IL
+locale IM = fixes a and b and c
 
-print_interps L    (* output: test *)
-print_interps M    (* output: test *)
+interpretation test [simp]: IL + IM a b c [x y z] .
+
+print_interps IL    (* output: test *)
+print_interps IM    (* output: test *)
 
-interpretation test [simp]: L print_interps M .
+interpretation test [simp]: IL print_interps IM .
 
-interpretation L .
+interpretation IL .
 
-(* processing of locale expression *)
+text {* Processing of locale expression *}
 
-locale A = fixes a assumes asm_A: "a = a"
+locale IA = fixes a assumes asm_A: "a = a"
 
-locale (open) B = fixes b assumes asm_B [simp]: "b = b"
+locale (open) IB = fixes b assumes asm_B [simp]: "b = b"
 
-locale C = A + B + assumes asm_C: "c = c"
+locale IC = IA + IB + assumes asm_C: "c = c"
   (* TODO: independent type var in c, prohibit locale declaration *)
 
-locale D = A + B + fixes d defines def_D: "d == (a = b)"
+locale ID = IA + IB + fixes d defines def_D: "d == (a = b)"
 
-theorem (in A)
-  includes D
+theorem (in IA)
+  includes ID
   shows True ..
 
-theorem (in D) True ..
+theorem (in ID) True ..
 
 typedecl i
 arities i :: "term"
 
 
-interpretation p1: C ["X::i" "Y::i"] by (auto intro: A.intro C_axioms.intro)
+interpretation i1: IC ["X::i" "Y::i"] by (auto intro: IA.intro IC_axioms.intro)
 
-print_interps A  (* output: p1 *)
+print_interps IA  (* output: i1 *)
 
 (* possible accesses *)
-thm p1.a.asm_A thm LocaleTest.p1.a.asm_A
-thm p1.asm_A thm LocaleTest.p1.asm_A
+thm i1.a.asm_A thm LocaleTest.i1.a.asm_A
+thm i1.asm_A thm LocaleTest.i1.asm_A
 
 
 (* without prefix *)
 
-interpretation C ["W::i" "Z::i"] .  (* subsumed by p1: C *)
-interpretation C ["W::'a" "Z::i"] by (auto intro: A.intro C_axioms.intro)
-  (* subsumes p1: A and p1: C *)
+interpretation IC ["W::i" "Z::i"] .  (* subsumed by i1: IC *)
+interpretation IC ["W::'a" "Z::i"] by (auto intro: IA.intro IC_axioms.intro)
+  (* subsumes i1: IA and i1: IC *)
 
 
-print_interps A  (* output: <no prefix>, p1 *)
+print_interps IA  (* output: <no prefix>, i1 *)
 
 (* possible accesses *)
 thm asm_C thm a_b.asm_C thm LocaleTest.a_b.asm_C thm LocaleTest.a_b.asm_C
 
 
-interpretation p2: D [X "Y::i" "Y = X"] by (simp add: eq_commute)
+interpretation i2: ID [X "Y::i" "Y = X"] by (simp add: eq_commute)
 
-print_interps A  (* output: <no prefix>, p1 *)
-print_interps D  (* output: p2 *)
+print_interps IA  (* output: <no prefix>, i1 *)
+print_interps ID  (* output: i2 *)
 
 
-interpretation p3: D [X "Y::i"] .
+interpretation i3: ID [X "Y::i"] .
 
 (* duplicate: not registered *)
 
-(* thm p3.a.asm_A *)
+(* thm i3.a.asm_A *)
 
 
-print_interps A  (* output: <no prefix>, p1 *)
-print_interps B  (* output: p1 *)
-print_interps C  (* output: <no name>, p1 *)
-print_interps D  (* output: p2, p3 *)
+print_interps IA  (* output: <no prefix>, i1 *)
+print_interps IB  (* output: i1 *)
+print_interps IC  (* output: <no prefix, i1 *)
+print_interps ID  (* output: i2, i3 *)
 
 (* schematic vars in instantiation not permitted *)
 (*
-interpretation p4: A ["?x::?'a1"] apply (rule A.intro) apply rule done
-print_interps A
+interpretation i4: IA ["?x::?'a1"] apply (rule IA.intro) apply rule done
+print_interps IA
 *)
 
-interpretation p10: D + D a' b' d' [X "Y::i" _ u "v::i" _] .
+interpretation i10: ID + ID a' b' d' [X "Y::i" _ u "v::i" _] .
 
-corollary (in D) th_x: True ..
+corollary (in ID) th_x: True ..
 
 (* possible accesses: for each registration *)
 
-thm p2.th_x thm p3.th_x
+thm i2.th_x thm i3.th_x
 
-lemma (in D) th_y: "d == (a = b)" .
+lemma (in ID) th_y: "d == (a = b)" .
 
-thm p2.th_y thm p3.th_y
+thm i2.th_y thm i3.th_y
 
-lemmas (in D) th_z = th_y
+lemmas (in ID) th_z = th_y
 
-thm p2.th_z
+thm i2.th_z
 
-section {* Interpretation in proof contexts *}
 
-locale F = fixes f assumes asm_F: "f & f --> f"
+subsection {* Interpretation in Proof Contexts *}
+
+locale IF = fixes f assumes asm_F: "f & f --> f"
 
 theorem True
 proof -
   fix alpha::i and beta::'a and gamma::o
-  (* FIXME: omitting type of beta leads to error later at interpret p6 *)
-  have alpha_A: "A(alpha)" by (auto intro: A.intro)
-  interpret p5: A [alpha] .  (* subsumed *)
-  print_interps A  (* output: <no prefix>, p1 *)
-  interpret p6: C [alpha beta] by (auto intro: C_axioms.intro)
-  print_interps A   (* output: <no prefix>, p1 *)
-  print_interps C   (* output: <no prefix>, p1, p6 *)
-  interpret p11: F [gamma] by (fast intro: F.intro)
-  thm p11.asm_F      (* gamma is a Free *)
+  (* FIXME: omitting type of beta leads to error later at interpret i6 *)
+  have alpha_A: "IA(alpha)" by (auto intro: IA.intro)
+  interpret i5: IA [alpha] .  (* subsumed *)
+  print_interps IA  (* output: <no prefix>, i1 *)
+  interpret i6: IC [alpha beta] by (auto intro: IC_axioms.intro)
+  print_interps IA   (* output: <no prefix>, i1 *)
+  print_interps IC   (* output: <no prefix>, i1, i6 *)
+  interpret i11: IF [gamma] by (fast intro: IF.intro)
+  thm i11.asm_F      (* gamma is a Free *)
 qed rule
 
-theorem (in A) True
+theorem (in IA) True
 proof -
-  print_interps A
+  print_interps IA
   fix beta and gamma
-  interpret p9: D [a beta _]
-    (* no proof obligation for A !!! *)
+  interpret i9: ID [a beta _]
+    (* no proof obligation for IA !!! *)
     apply - apply (rule refl) apply assumption done
 qed rule
 
@@ -178,64 +185,91 @@
 
 ML {* reset show_sorts *}
 
-locale E = fixes e defines e_def: "e(x) == x & x"
+locale IE = fixes e defines e_def: "e(x) == x & x"
   notes e_def2 = e_def
 
-lemma (in E) True thm e_def by fast
+lemma (in IE) True thm e_def by fast
 
-interpretation p7: E ["%x. x"] by simp
+interpretation i7: IE ["%x. x"] by simp
 
-thm p7.e_def2 (* has no premise *)
+thm i7.e_def2 (* has no premise *)
 
-locale E' = fixes e defines e_def: "e == (%x. x & x)"
+locale IE' = fixes e defines e_def: "e == (%x. x & x)"
   notes e_def2 = e_def
 
-interpretation p7': E' ["(%x. x)"] by simp
+interpretation i7': IE' ["(%x. x)"] by simp
 
-thm p7'.e_def2
+thm i7'.e_def2
 
 (* Definition involving free variable in assm *)
 
-locale (open) G = fixes g assumes asm_G: "g --> x"
+locale (open) IG = fixes g assumes asm_G: "g --> x"
   notes asm_G2 = asm_G
 
-interpretation p8: G ["False"] by fast
+interpretation i8: IG ["False"] by fast
 
-thm p8.asm_G2
+thm i8.asm_G2
 
-subsection {* Locale without assumptions *}
+text {* Locale without assumptions *}
 
-locale L1 = notes rev_conjI [intro] = conjI [THEN iffD1 [OF conj_commute]]
+locale IL1 = notes rev_conjI [intro] = conjI [THEN iffD1 [OF conj_commute]]
 
 lemma "[| P; Q |] ==> P & Q"
 proof -
-  interpret my: L1 .           txt {* No chained fact required. *}
+  interpret my: IL1 .          txt {* No chained fact required. *}
   assume Q and P               txt {* order reversed *}
   then show "P & Q" ..         txt {* Applies @{thm my.rev_conjI}. *}
 qed
 
-locale L11 = notes rev_conjI = conjI [THEN iffD1 [OF conj_commute]]
+locale IL11 = notes rev_conjI = conjI [THEN iffD1 [OF conj_commute]]
 
 lemma "[| P; Q |] ==> P & Q"
 proof -
-  interpret [intro]: L11 .     txt {* Attribute supplied at instantiation. *}
+  interpret [intro]: IL11 .     txt {* Attribute supplied at instantiation. *}
   assume Q and P
   then show "P & Q" ..
 qed
 
 subsection {* Simple locale with assumptions *}
 
-consts bin :: "[i, i] => i" (infixl "#" 60)
+consts ibin :: "[i, i] => i" (infixl "#" 60)
 
 axioms i_assoc: "(x # y) # z = x # (y # z)"
   i_comm: "x # y = y # x"
 
-locale L2 =
+locale IL2 =
   fixes OP (infixl "+" 60)
   assumes assoc: "(x + y) + z = x + (y + z)"
     and comm: "x + y = y + x"
 
-lemma (in L2) lcomm: "x + (y + z) = y + (x + z)"
+lemma (in IL2) lcomm: "x + (y + z) = y + (x + z)"
+proof -
+  have "x + (y + z) = (x + y) + z" by (simp add: assoc)
+  also have "... = (y + x) + z" by (simp add: comm)
+  also have "... = y + (x + z)" by (simp add: assoc)
+  finally show ?thesis .
+qed
+
+lemmas (in IL2) AC = comm assoc lcomm
+
+lemma "(x::i) # y # z # w = y # x # w # z"
+proof -
+  interpret my: IL2 ["op #"] by (rule IL2.intro [of "op #", OF i_assoc i_comm])
+    txt {* Chained fact required to discharge assumptions of @{text IL2}
+      and instantiate parameters. *}
+  show ?thesis by (simp only: my.OP.AC)  (* or simply AC *)
+qed
+
+subsection {* Nested locale with assumptions *}
+
+locale IL3 =
+  fixes OP (infixl "+" 60)
+  assumes assoc: "(x + y) + z = x + (y + z)"
+
+locale IL4 = IL3 +
+  assumes comm: "x + y = y + x"
+
+lemma (in IL4) lcomm: "x + (y + z) = y + (x + z)"
 proof -
   have "x + (y + z) = (x + y) + z" by (simp add: assoc)
   also have "... = (y + x) + z" by (simp add: comm)
@@ -243,72 +277,282 @@
   finally show ?thesis .
 qed
 
-lemmas (in L2) AC = comm assoc lcomm
-
-lemma "(x::i) # y # z # w = y # x # w # z"
-proof -
-  interpret my: L2 ["op #"] by (rule L2.intro [of "op #", OF i_assoc i_comm])
-    txt {* Chained fact required to discharge assumptions of @{text L2}
-      and instantiate parameters. *}
-  show ?thesis by (simp only: my.OP.AC)  (* or simply AC *)
-qed
-
-subsection {* Nested locale with assumptions *}
-
-locale L3 =
-  fixes OP (infixl "+" 60)
-  assumes assoc: "(x + y) + z = x + (y + z)"
-
-locale L4 = L3 +
-  assumes comm: "x + y = y + x"
-
-lemma (in L4) lcomm: "x + (y + z) = y + (x + z)"
-proof -
-  have "x + (y + z) = (x + y) + z" by (simp add: assoc)
-  also have "... = (y + x) + z" by (simp add: comm)
-  also have "... = y + (x + z)" by (simp add: assoc)
-  finally show ?thesis .
-qed
-
-lemmas (in L4) AC = comm assoc lcomm
+lemmas (in IL4) AC = comm assoc lcomm
 
 lemma "(x::i) # y # z # w = y # x # w # z"
 proof -
-  interpret my: L4 ["op #"]
-    by (auto intro: L3.intro L4_axioms.intro i_assoc i_comm)
+  interpret my: IL4 ["op #"]
+    by (auto intro: IL3.intro IL4_axioms.intro i_assoc i_comm)
   show ?thesis by (simp only: my.OP.AC)  (* or simply AC *)
 qed
 
-subsection {* Locale with definition *}
+text {* Locale with definition *}
 
 text {* This example is admittedly not very creative :-) *}
 
-locale L5 = L4 + var A +
+locale IL5 = IL4 + var A +
   defines A_def: "A == True"
 
-lemma (in L5) lem: A
+lemma (in IL5) lem: A
   by (unfold A_def) rule
 
-lemma "L5(op #) ==> True"
+lemma "IL5(op #) ==> True"
 proof -
-  assume "L5(op #)"
-  then interpret L5 ["op #"] by (auto intro: L5.axioms)
+  assume "IL5(op #)"
+  then interpret IL5 ["op #"] by (auto intro: IL5.axioms)
   show ?thesis by (rule lem)  (* lem instantiated to True *)
 qed
 
-subsection {* Instantiation in a context with target *}
+text {* Interpretation in a context with target *}
 
-lemma (in L4)
+lemma (in IL4)
   fixes A (infixl "$" 60)
-  assumes A: "L4(A)"
+  assumes A: "IL4(A)"
   shows "(x::i) $ y $ z $ w = y $ x $ w $ z"
 proof -
-  from A interpret A: L4 ["A"] by (auto intro: L4.axioms)
+  from A interpret A: IL4 ["A"] by (auto intro: IL4.axioms)
   show ?thesis by (simp only: A.OP.AC)
 qed
 
+
 section {* Interpretation in Locales *}
 
-interpretation M < L .
+text {* Naming convention for global objects: prefixes R and r *}
+
+locale (open) Rsemi = var prod (infixl "**" 65) +
+  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
+
+locale (open) Rlgrp = Rsemi + var one + var inv +
+  assumes lone: "one ** x = x"
+    and linv: "inv(x) ** x = one"
+
+lemma (in Rlgrp) lcancel:
+  "x ** y = x ** z <-> y = z"
+proof
+  assume "x ** y = x ** z"
+  then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
+  then show "y = z" by (simp add: lone linv)
+qed simp
+
+locale (open) Rrgrp = Rsemi + var one + var inv +
+  assumes rone: "x ** one = x"
+    and rinv: "x ** inv(x) = one"
+
+lemma (in Rrgrp) rcancel:
+  "y ** x = z ** x <-> y = z"
+proof
+  assume "y ** x = z ** x"
+  then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
+    by (simp add: assoc [symmetric])
+  then show "y = z" by (simp add: rone rinv)
+qed simp
+
+interpretation Rlgrp < Rrgrp
+  proof - (* (rule Rrgrp_axioms.intro) *)
+    {
+      fix x
+      have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
+      then show "x ** one = x" by (simp add: assoc lcancel)
+    }
+    note rone = this
+    {
+      fix x
+      have "inv(x) ** x ** inv(x) = inv(x) ** one"
+	by (simp add: linv lone rone)
+      then show "x ** inv(x) = one" by (simp add: assoc lcancel)
+    }
+  qed
+
+(* effect on printed locale *)
+
+print_locale Rlgrp
+
+(* use of derived theorem *)
+
+lemma (in Rlgrp)
+  "y ** x = z ** x <-> y = z"
+  apply (rule rcancel)
+  print_interps Rrgrp thm lcancel rcancel
+  done
+
+(* circular interpretation *)
+
+interpretation Rrgrp < Rlgrp
+  proof -
+    {
+      fix x
+      have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
+      then show "one ** x = x" by (simp add: assoc [symmetric] rcancel)
+    }
+    note lone = this
+    {
+      fix x
+      have "inv(x) ** (x ** inv(x)) = one ** inv(x)"
+	by (simp add: rinv lone rone)
+      then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel)
+    }
+  qed
+
+(* effect on printed locale *)
+
+print_locale Rrgrp
+print_locale Rlgrp
+
+(* locale with many parameters ---
+   interpretations generate alternating group A5 *)
+
+locale RA5 = var A + var B + var C + var D + var E +
+  assumes eq: "A <-> B <-> C <-> D <-> E"
+
+interpretation RA5 < RA5 _ _ D E C
+print_facts
+print_interps RA5
+  using A_B_C_D_E.eq apply (blast intro: RA5.intro) done
+
+interpretation RA5 < RA5 C _ E _ A
+print_facts
+print_interps RA5
+  using A_B_C_D_E.eq apply (blast intro: RA5.intro) done
+
+interpretation RA5 < RA5 B C A _ _
+print_facts
+print_interps RA5
+  using A_B_C_D_E.eq apply (blast intro: RA5.intro) done
+
+lemma (in RA5) True
+print_facts
+print_interps RA5
+  ..
+
+interpretation RA5 < RA5 _ C D B _ .
+  (* Any even permutation of parameters is subsumed by the above. *)
+
+(* circle of three locales, forward direction *)
+
+locale (open) RA1 = var A + var B + assumes p: "A <-> B"
+locale (open) RA2 = var A + var B + assumes q: "A & B | ~ A & ~ B"
+locale (open) RA3 = var A + var B + assumes r: "(A --> B) & (B --> A)"
+
+interpretation RA1 < RA2
+  print_facts
+  using p apply fast done
+interpretation RA2 < RA3
+  print_facts
+  using q apply fast done
+interpretation RA3 < RA1
+  print_facts
+  using r apply fast done
+
+(* circle of three locales, backward direction *)
+
+locale (open) RB1 = var A + var B + assumes p: "A <-> B"
+locale (open) RB2 = var A + var B + assumes q: "A & B | ~ A & ~ B"
+locale (open) RB3 = var A + var B + assumes r: "(A --> B) & (B --> A)"
+
+interpretation RB1 < RB2
+  print_facts
+  using p apply fast done
+interpretation RB3 < RB1
+  print_facts
+  using r apply fast done
+interpretation RB2 < RB3
+  print_facts
+  using q apply fast done
+
+lemma (in RB1) True
+  print_facts
+  ..
+
+
+(* Group example revisited, with predicates *)
+
+locale Rpsemi = var prod (infixl "**" 65) +
+  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
+
+locale Rplgrp = Rpsemi + var one + var inv +
+  assumes lone: "one ** x = x"
+    and linv: "inv(x) ** x = one"
+
+lemma (in Rplgrp) lcancel:
+  "x ** y = x ** z <-> y = z"
+proof
+  assume "x ** y = x ** z"
+  then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
+  then show "y = z" by (simp add: lone linv)
+qed simp
+
+locale Rprgrp = Rpsemi + var one + var inv +
+  assumes rone: "x ** one = x"
+    and rinv: "x ** inv(x) = one"
+
+lemma (in Rprgrp) rcancel:
+  "y ** x = z ** x <-> y = z"
+proof
+  assume "y ** x = z ** x"
+  then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
+    by (simp add: assoc [symmetric])
+  then show "y = z" by (simp add: rone rinv)
+qed simp
+
+interpretation Rplgrp < Rprgrp
+  proof (rule Rprgrp_axioms.intro)
+    {
+      fix x
+      have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
+      then show "x ** one = x" by (simp add: assoc lcancel)
+    }
+    note rone = this
+    {
+      fix x
+      have "inv(x) ** x ** inv(x) = inv(x) ** one"
+	by (simp add: linv lone rone)
+      then show "x ** inv(x) = one" by (simp add: assoc lcancel)
+    }
+  qed
+
+(* effect on printed locale *)
+
+print_locale Rplgrp
+
+(* use of derived theorem *)
+
+(* doesn't work yet
+lemma (in Rplgrp)
+  "y ** x = z ** x <-> y = z"
+  apply (rule rcancel)
+  print_interps Rprgrp thm lcancel rcancel
+  done
+*)
+
+(* circular interpretation *)
+
+interpretation Rprgrp < Rplgrp
+  proof (rule Rplgrp_axioms.intro)
+    {
+      fix x
+      have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
+      then show "one ** x = x" by (simp add: assoc [symmetric] rcancel)
+    }
+    note lone = this
+    {
+      fix x
+      have "inv(x) ** (x ** inv(x)) = one ** inv(x)"
+	by (simp add: rinv lone rone)
+      then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel)
+    }
+  qed
+
+(* effect on printed locale *)
+
+print_locale Rprgrp
+print_locale Rplgrp
 
 end
+
+(* Known problems:
+- var vs. fixes in locale to be interpreted (interpretation command)
+  (possibly caused by early registrations)
+- registrations too early -> proper after qed
+- predicate generation in group example, thms have wrong hyps
+- reprocess registrations in theory (after qed)
+*)
diff -r 307b2ec590ff -r 552df70f52c2 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Tue Aug 02 16:50:55 2005 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Tue Aug 02 16:52:21 2005 +0200
@@ -659,9 +659,24 @@
 fun register_in_locale (target, expr) int thy =
   let
     val target = Locale.intern thy target;
+    val (target_expr, thy', propss, activate) =
+        Locale.prep_registration_in_locale target expr thy;
+    fun witness id (thy, thm) = let
+        (* push outer quantifiers inside implications *)
+        val {prop, sign, ...} = rep_thm thm;
+        val frees = map (cterm_of sign o Free) (strip_all_vars prop);
+            (* are hopefully distinct *)
+        val prems = Logic.strip_imp_prems (strip_all_body prop);
+        val cprems = map (cterm_of sign) prems;
+        val thm' = thm |> forall_elim_list frees
+                       |> (fn th => implies_elim_list th (map Thm.assume cprems))
+                       |> forall_intr_list frees;
+      in (Locale.add_witness_in_locale target id thm' thy, thm') end;
   in
-    locale_multi_theorem_i Drule.internalK target ("",[]) []
-      [] (*concl*) int thy
+    multi_theorem_i Drule.internalK activate ProofContext.export_plain
+      ("",[]) [Locale.Expr target_expr]
+      (map (fn (id as (n, _), props) => ((NameSpace.base n, [witness id]),
+        map (fn prop => (prop, ([], []))) props)) propss) int thy'
   end;
 
 fun register_locally (((prfx, atts), expr), insts) =
diff -r 307b2ec590ff -r 552df70f52c2 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Aug 02 16:50:55 2005 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Aug 02 16:52:21 2005 +0200
@@ -88,15 +88,16 @@
   val prep_global_registration:
     string * Attrib.src list -> expr -> string option list -> theory ->
     theory * ((string * term list) * term list) list * (theory -> theory)
-(*
   val prep_registration_in_locale:
-    string -> expr -> string option list -> theory ->
-*)
+    string -> expr -> theory ->
+    expr * theory * ((string * string list) * term list) list * (theory -> theory)
   val prep_local_registration:
     string * Attrib.src list -> expr -> string option list -> context ->
     context * ((string * term list) * term list) list * (context -> context)
   val add_global_witness:
     string * term list -> thm -> theory -> theory
+  val add_witness_in_locale:
+    string -> string * string list -> thm -> theory -> theory
   val add_local_witness:
     string * term list -> thm -> context -> context
 end;
@@ -462,6 +463,14 @@
 val put_local_registration =
      gen_put_registration LocalLocalesData.map ProofContext.theory_of;
 
+fun put_registration_in_locale name id thy =
+    let
+      val {predicate, import, elems, params, regs} = the_locale thy name;
+    in
+      put_locale name {predicate = predicate, import = import,
+        elems = elems, params = params, regs = regs @ [(id, [])]} thy
+    end;
+
 
 (* add witness theorem to registration in theory or context,
    ignored if registration not present *)
@@ -480,6 +489,15 @@
          (space, locs, f regs)));
 val add_local_witness = gen_add_witness LocalLocalesData.map;
 
+fun add_witness_in_locale name id thm thy =
+    let
+      val {predicate, import, elems, params, regs} = the_locale thy name;
+      fun add (id', thms) =
+          if id = id' then (id', thm :: thms) else (id', thms);
+    in
+      put_locale name {predicate = predicate, import = import,
+	elems = elems, params = params, regs = map add regs} thy
+    end;
 
 (* import hierarchy
    implementation could be more efficient, eg. by maintaining a database
@@ -745,6 +763,19 @@
     ("Conflicting syntax for parameter(s): " ^ commas_quote xs) (map fst ids);
 
 
+(* Distinction of assumed vs. derived identifiers.
+   The former may have axioms relating assumptions of the context to
+   assumptions of the specification fragment (for locales with
+   predicates).  The latter have witness theorems relating assumptions of the
+   specification fragment to assumptions of other (assumed) specification
+   fragments. *)
+
+datatype 'a mode = Assumed of 'a | Derived of 'a;
+
+fun map_mode f (Assumed x) = Assumed (f x)
+  | map_mode f (Derived x) = Derived (f x);
+
+
 (* flatten expressions *)
 
 local
@@ -806,12 +837,13 @@
   | unify_elemss ctxt fixed_parms elemss =
       let
         val envs = unify_parms ctxt fixed_parms (map (#2 o #1 o #1) elemss);
-        fun inst ((((name, ps), axs), elems), env) =
+        fun inst ((((name, ps), mode), elems), env) =
           (((name, map (apsnd (Option.map (inst_type env))) ps), 
-            map (inst_thm ctxt env) axs), map (inst_elem ctxt env) elems);
+              map_mode (map (inst_thm ctxt env)) mode),
+            map (inst_elem ctxt env) elems);
       in map inst (elemss ~~ envs) end;
 
-(* like unify_elemss, but does not touch axioms, additional
+(* like unify_elemss, but does not touch mode, additional
    parameter c_parms for enforcing further constraints (eg. syntax) *)
 
 fun unify_elemss' _ _ [] [] = []
@@ -819,11 +851,12 @@
   | unify_elemss' ctxt fixed_parms elemss c_parms =
       let
         val envs = unify_parms ctxt fixed_parms (map (#2 o #1 o #1) elemss @ map single c_parms);
-        fun inst ((((name, ps), axs), elems), env) =
-          (((name, map (apsnd (Option.map (inst_type env))) ps),  axs),
+        fun inst ((((name, ps), mode), elems), env) =
+          (((name, map (apsnd (Option.map (inst_type env))) ps),  mode),
            map (inst_elem ctxt env) elems);
       in map inst (elemss ~~ (Library.take (length elemss, envs))) end;
 
+
 (* flatten_expr:
    Extend list of identifiers by those new in locale expression expr.
    Compute corresponding list of lists of locale elements (one entry per
@@ -858,14 +891,53 @@
       | renaming xs [] = raise ERROR_MESSAGE ("Too many arguments in renaming: " ^
           commas (map (fn NONE => "_" | SOME x => quote (fst x)) xs));
 
-    fun rename_parms top ren ((name, ps), (parms, axs)) =
+    fun rename_parms top ren ((name, ps), (parms, mode)) =
       let val ps' = map (rename ren) ps in
-        (case duplicates ps' of [] => ((name, ps'),
-          if top then (map (rename ren) parms, map (rename_thm ren) axs)
-          else (parms, axs))
+        (case duplicates ps' of
+          [] => (case mode of
+              Assumed axs => ((name, ps'),
+                if top then (map (rename ren) parms, 
+                  Assumed (map (rename_thm ren) axs))
+                else (parms, Assumed axs))
+            | Derived ths => ((name, ps'),
+                (map (rename ren) parms, Derived (map (rename_thm ren) ths))))
         | dups => err_in_locale ctxt ("Duplicate parameters: " ^ commas_quote dups) [(name, ps')])
       end;
 
+    (* add registrations of (name, ps), recursively;
+       adjust hyps of witness theorems *)
+
+    fun add_regs (name, ps) (ths, ids) =
+        let
+          val {params, regs, ...} = the_locale thy name;
+          val ren = map (#1 o #1) (#1 params) ~~ map (fn x => (x, NONE)) ps;
+            (* dummy syntax, since required by rename *)
+          val regs' = map (fn ((name, ps), ths) =>
+              ((name, map (rename ren) ps), ths)) regs;
+          val new_regs = gen_rems eq_fst (regs', ids);
+          val new_ids = map fst new_regs;
+          val new_ths = map (fn (_, ths') =>
+              map (Drule.satisfy_hyps ths o rename_thm ren) ths') new_regs;
+          val new_ids' = map (fn (id, ths) =>
+              (id, ([], Derived ths))) (new_ids ~~ new_ths);
+        in
+          fold add_regs new_ids (ths @ List.concat new_ths, ids @ new_ids')
+        end;
+
+    (* distribute top-level axioms over assumed ids *)
+
+    fun axiomify all_ps ((name, parms), (_, Assumed _)) axioms =
+        let
+          val {elems, ...} = the_locale thy name;
+          val ts = List.concat (map
+            (fn (Assumes asms, _) => List.concat (map (map #1 o #2) asms)
+              | _ => [])
+            elems);
+          val (axs1, axs2) = splitAt (length ts, axioms);
+        in (((name, parms), (all_ps, Assumed axs1)), axs2) end
+      | axiomify all_ps (id, (_, Derived ths)) axioms =
+          ((id, (all_ps, Derived ths)), axioms);
+
     fun identify top (Locale name) =
     (* CB: ids_ax is a list of tuples of the form ((name, ps), axs),
        where name is a locale name, ps a list of parameter names and axs
@@ -876,23 +948,19 @@
             val {predicate = (_, axioms), import, params, ...} =
               the_locale thy name;
             val ps = map (#1 o #1) (#1 params);
-            val (ids', parms', _) = identify false import;
+            val (ids', parms', _, ths) = identify false import;
                 (* acyclic import dependencies *)
-            val ids'' = ids' @ [((name, ps), ([], []))];
-            val ids_ax = if top then snd
-                 (* get the right axioms, only if at top level *)
-                 (foldl_map (fn (axs, ((name, parms), _)) => let
-                   val {elems, ...} = the_locale thy name;
-                   val ts = List.concat (List.mapPartial (fn (Assumes asms, _) =>
-                     SOME (List.concat (map (map #1 o #2) asms)) | _ => NONE) elems);
-                   val (axs1, axs2) = splitAt (length ts, axs);
-                 in (axs2, ((name, parms), (ps, axs1))) end) (axioms, ids''))
-               else ids'';
+            val ids'' = ids' @ [((name, ps), ([], Assumed []))];
+            val (ths', ids''') = add_regs (name, ps) (ths, ids'');
+
+            val ids_ax = if top then fst
+                 (fold_map (axiomify ps) ids''' axioms)
+              else ids''';
             val syn = Symtab.make (map (apfst fst) (#1 params));
-          in (ids_ax, merge_lists parms' ps, syn) end
+          in (ids_ax, merge_lists parms' ps, syn, ths') end
       | identify top (Rename (e, xs)) =
           let
-            val (ids', parms', syn') = identify top e;
+            val (ids', parms', syn', ths) = identify top e;
             val ren = renaming xs parms'
               handle ERROR_MESSAGE msg => err_in_locale' ctxt msg ids';
             val ids'' = gen_distinct eq_fst (map (rename_parms top ren) ids');
@@ -900,14 +968,20 @@
             val syn'' = syn' |> Symtab.dest |> map (rename_var ren) |>
                   Symtab.make;
             (* check for conflicting syntax? *)
-          in (ids'', parms'', syn'') end
+            val ths' = map (rename_thm ren) ths;
+          in (ids'', parms'', syn'', ths') end
       | identify top (Merge es) =
-          Library.foldl (fn ((ids, parms, syn), e) => let
-                     val (ids', parms', syn') = identify top e
-                   in (merge_alists ids ids',
-                       merge_lists parms parms',
-                       merge_syntax ctxt ids' (syn, syn')) end)
-            (([], [], Symtab.empty), es);
+          fold (fn e => fn (ids, parms, syn, ths) =>
+                   let
+                     val (ids', parms', syn', ths') = identify top e
+                   in
+                     (merge_alists ids ids',
+                      merge_lists parms parms',
+                      merge_syntax ctxt ids' (syn, syn'),
+                      merge_lists ths ths')
+                   end)
+            es ([], [], Symtab.empty, []);
+
 
     (* CB: enrich identifiers by parameter types and 
        the corresponding elements (with renamed parameters),
@@ -934,7 +1008,7 @@
           in Ts |> Library.split_last |> op ---> |> SOME end;
 
     (* compute identifiers and syntax, merge with previous ones *)
-    val (ids, _, syn) = identify true expr;
+    val (ids, _, syn, _) = identify true expr;
     val idents = gen_rems eq_fst (ids, prev_idents);
     val syntax = merge_syntax ctxt ids (syn, prev_syntax);
     (* add types to params, check for unique params and unify them *)
@@ -945,17 +1019,18 @@
        adjust types in axioms *)
     val all_params' = params_of' elemss;
     val all_params = param_types all_params';
-    val elemss' = map (fn (((name, _), (ps, axs)), elems) =>
-         (((name, map (fn p => (p, assoc (all_params, p))) ps), axs), elems))
+    val elemss' = map (fn (((name, _), (ps, mode)), elems) =>
+         (((name, map (fn p => (p, assoc (all_params, p))) ps), mode), elems))
          elemss;
-    fun inst_ax th = let
+    fun inst_th th = let
          val {hyps, prop, ...} = Thm.rep_thm th;
          val ps = map (apsnd SOME) (fold Term.add_frees (prop :: hyps) []);
          val [env] = unify_parms ctxt all_params [ps];
          val th' = inst_thm ctxt env th;
        in th' end;
-    val final_elemss = map (fn ((id, axs), elems) =>
-         ((id, map inst_ax axs), elems)) elemss';
+    val final_elemss = map (fn ((id, mode), elems) =>
+         ((id, map_mode (map inst_th) mode), elems)) elemss';
+
   in ((prev_idents @ idents, syntax), final_elemss) end;
 
 end;
@@ -972,10 +1047,14 @@
      (* CB: turn remaining hyps into assumptions. *)
   |> Seq.single
 
-fun activate_elem _ ((ctxt, axs), Fixes fixes) =
-      ((ctxt |> ProofContext.add_fixes fixes, axs), [])
-  | activate_elem _ ((ctxt, axs), Constrains _) = ((ctxt, axs), [])
-  | activate_elem _ ((ctxt, axs), Assumes asms) =
+
+(* NB: derived ids contain only facts at this stage *)
+
+fun activate_elem _ ((ctxt, mode), Fixes fixes) =
+      ((ctxt |> ProofContext.add_fixes fixes, mode), [])
+  | activate_elem _ ((ctxt, mode), Constrains _) =
+      ((ctxt, mode), [])
+  | activate_elem _ ((ctxt, Assumed axs), Assumes asms) =
       let
         val asms' = map_attrib_specs (Attrib.context_attribute_i ctxt) asms;
         val ts = List.concat (map (map #1 o #2) asms');
@@ -983,8 +1062,10 @@
         val (ctxt', _) =
           ctxt |> ProofContext.fix_frees ts
           |> ProofContext.assume_i (export_axioms ps) asms';
-      in ((ctxt', qs), []) end
-  | activate_elem _ ((ctxt, axs), Defines defs) =
+      in ((ctxt', Assumed qs), []) end
+  | activate_elem _ ((ctxt, Derived ths), Assumes asms) =
+      ((ctxt, Derived ths), [])
+  | activate_elem _ ((ctxt, Assumed axs), Defines defs) =
       let
         val defs' = map_attrib_specs (Attrib.context_attribute_i ctxt) defs;
         val (ctxt', _) =
@@ -992,32 +1073,40 @@
           (defs' |> map (fn ((name, atts), (t, ps)) =>
             let val (c, t') = ProofContext.cert_def ctxt t
             in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end))
-      in ((ctxt', axs), []) end
-  | activate_elem is_ext ((ctxt, axs), Notes facts) =
+      in ((ctxt', Assumed axs), []) end
+  | activate_elem _ ((ctxt, Derived ths), Defines defs) =
+      ((ctxt, Derived ths), [])
+  | activate_elem is_ext ((ctxt, mode), Notes facts) =
       let
         val facts' = map_attrib_facts (Attrib.context_attribute_i ctxt) facts;
         val (ctxt', res) = ctxt |> ProofContext.note_thmss_i facts';
-      in ((ctxt', axs), if is_ext then res else []) end;
+      in ((ctxt', mode), if is_ext then res else []) end;
 
-fun activate_elems (((name, ps), axs), elems) ctxt =
+fun activate_elems (((name, ps), mode), elems) ctxt =
   let val ((ctxt', _), res) =
-    foldl_map (activate_elem (name = "")) ((ProofContext.qualified_names ctxt, axs), elems)
+    foldl_map (activate_elem (name = "")) ((ProofContext.qualified_names ctxt, mode), elems)
       handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)]
     val ctxt'' = if name = "" then ctxt'
           else let
               val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
               val ctxt'' = put_local_registration (name, ps') ("", []) ctxt'
-            in foldl (fn (ax, ctxt) =>
-              add_local_witness (name, ps') (Thm.assume (Thm.cprop_of ax)) ctxt) ctxt'' axs
+            in case mode of
+                   Assumed axs => fold (fn ax => fn ctxt =>
+                      add_local_witness (name, ps')
+                       (Thm.assume (Thm.cprop_of ax)) ctxt) axs ctxt''
+                 | Derived ths => fold (fn th => fn ctxt =>
+                     add_local_witness (name, ps') th ctxt) ths ctxt''
             end
   in (ProofContext.restore_naming ctxt ctxt'', res) end;
 
-fun activate_elemss prep_facts = foldl_map (fn (ctxt, (((name, ps), axs), raw_elems)) =>
-  let
-    val elems = map (prep_facts ctxt) raw_elems;
-    val (ctxt', res) = apsnd List.concat (activate_elems (((name, ps), axs), elems) ctxt);
-    val elems' = map (map_attrib_elem Args.closure) elems;
-  in (ctxt', (((name, ps), elems'), res)) end);
+fun activate_elemss prep_facts =
+    fold_map (fn (((name, ps), mode), raw_elems) => fn ctxt =>
+      let
+        val elems = map (prep_facts ctxt) raw_elems;
+        val (ctxt', res) = apsnd List.concat
+            (activate_elems (((name, ps), mode), elems) ctxt);
+        val elems' = map (map_attrib_elem Args.closure) elems;
+      in ((((name, ps), elems'), res), ctxt') end);
 
 in
 
@@ -1032,13 +1121,17 @@
    If read_facts or cert_facts is used for prep_facts, these also remove
    the internal/external markers from elemss. *)
 
-fun activate_facts prep_facts arg =
-  apsnd (apsnd List.concat o Library.split_list) (activate_elemss prep_facts arg);
+fun activate_facts prep_facts (ctxt, args) =
+    let
+      val (res, ctxt') = activate_elemss prep_facts args ctxt;
+    in
+      (ctxt', apsnd List.concat (split_list res))
+    end;
 
 fun activate_note prep_facts (ctxt, args) =
   let
     val (ctxt', ([(_, [Notes args'])], facts)) =
-      activate_facts prep_facts (ctxt, [((("", []), []), [Ext (Notes args)])]);
+      activate_facts prep_facts (ctxt, [((("", []), Assumed []), [Ext (Notes args)])]);
   in (ctxt', (args', facts)) end;
 
 end;
@@ -1046,6 +1139,7 @@
 
 (* register elements *)
 
+(* not used
 fun register_elems (((_, ps), (((name, ax_ps), axs), _)), ctxt) =
   if name = "" then ctxt
       else let val ps' = map (fn (n, SOME T) => Free (n, T)) ax_ps
@@ -1056,6 +1150,7 @@
 
 fun register_elemss id_elemss ctxt = 
   foldl register_elems ctxt id_elemss;
+*)
 
 
 (** prepare context elements **)
@@ -1085,7 +1180,8 @@
 
 (* propositions and bindings *)
 
-(* flatten ((ids, syn), expr) normalises expr (which is either a locale
+(* flatten (ctxt, prep_expr) ((ids, syn), expr)
+   normalises expr (which is either a locale
    expression or a single context element) wrt.
    to the list ids of already accumulated identifiers.
    It returns (ids', syn', elemss) where ids' is an extension of ids
@@ -1105,7 +1201,7 @@
 *)
 
 fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let
-	val ids' = ids @ [(("", map #1 fixes), ([], []))]
+	val ids' = ids @ [(("", map #1 fixes), ([], Assumed []))]
       in
 	((ids',
 	 merge_syntax ctxt ids'
@@ -1113,10 +1209,10 @@
 	   handle Symtab.DUPS xs => err_in_locale ctxt
 	     ("Conflicting syntax for parameters: " ^ commas_quote xs)
              (map #1 ids')),
-	 [((("", map (rpair NONE o #1) fixes), []), Ext (Fixes fixes))])
+	 [((("", map (rpair NONE o #1) fixes), Assumed []), Ext (Fixes fixes))])
       end
   | flatten _ ((ids, syn), Elem elem) =
-      ((ids @ [(("", []), ([], []))], syn), [((("", []), []), Ext elem)])
+      ((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)])
   | flatten (ctxt, prep_expr) ((ids, syn), Expr expr) =
       apsnd (map (apsnd Int)) (flatten_expr ctxt ((ids, syn), prep_expr expr));
 
@@ -1145,13 +1241,15 @@
   | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs)
   | declare_ext_elem _ (ctxt, Notes facts) = (ctxt, []);
 
-fun declare_elems prep_parms (ctxt, (((name, ps), _), elems)) =
-  let val (ctxt', propps) =
-    (case elems of
-      Int es => foldl_map declare_int_elem (ctxt, es)
-    | Ext e => foldl_map (declare_ext_elem prep_parms) (ctxt, [e]))
-    handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)]
-  in (ctxt', propps) end;
+fun declare_elems prep_parms (ctxt, (((name, ps), Assumed _), elems)) =
+    let val (ctxt', propps) =
+      (case elems of
+        Int es => foldl_map declare_int_elem (ctxt, es)
+      | Ext e => foldl_map (declare_ext_elem prep_parms) (ctxt, [e]))
+      handle ProofContext.CONTEXT (msg, ctxt) =>
+        err_in_locale ctxt msg [(name, map fst ps)]
+    in (ctxt', propps) end
+  | declare_elems _ (ctxt, ((_, Derived _), elems)) = (ctxt, []);
 
 in
 
@@ -1181,6 +1279,7 @@
 
 val norm_term = Envir.beta_norm oo Term.subst_atomic;
 
+
 (* CB: following code (abstract_term, abstract_thm, bind_def)
    used in eval_text for Defines elements. *)
 
@@ -1210,11 +1309,13 @@
     (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths)
   end;
 
-(* CB: for finish_elems (Int and Ext) *)
+
+(* CB: for finish_elems (Int and Ext),
+   extracts specification, only of assumed elements *)
 
 fun eval_text _ _ _ (text, Fixes _) = text
   | eval_text _ _ _ (text, Constrains _) = text
-  | eval_text _ _ is_ext ((((exts, exts'), (ints, ints')), (xs, env, defs)), Assumes asms) =
+  | eval_text _ (_, Assumed _) is_ext ((((exts, exts'), (ints, ints')), (xs, env, defs)), Assumes asms) =
       let
         val ts = List.concat (map (map #1 o #2) asms);
         val ts' = map (norm_term env) ts;
@@ -1222,10 +1323,35 @@
           if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
           else ((exts, exts'), (ints @ ts, ints' @ ts'));
       in (spec', (fold Term.add_frees ts' xs, env, defs)) end
-  | eval_text ctxt (id, _) _ ((spec, binds), Defines defs) =
+  | eval_text _ (_, Derived _) _ (text, Assumes _) = text
+  | eval_text ctxt (id, Assumed _) _ ((spec, binds), Defines defs) =
       (spec, Library.foldl (bind_def ctxt id) (binds, map (#1 o #2) defs))
+  | eval_text _ (_, Derived _) _ (text, Defines _) = text
   | eval_text _ _ _ (text, Notes _) = text;
 
+
+(* for finish_elems (Int),
+   remove redundant elements of derived identifiers,
+   turn assumptions and definitions into facts,
+   adjust hypotheses of facts using witness theorems *)
+
+fun finish_derived _ _ (Assumed _) elem = SOME elem
+  | finish_derived _ _ (Derived _) (Fixes _) = NONE
+  | finish_derived _ _ (Derived _) (Constrains _) = NONE
+  | finish_derived sign wits (Derived _) (Assumes asms) = asms
+      |> map (apsnd (map (fn (a, _) =>
+           ([Thm.assume (cterm_of sign a) |> Drule.satisfy_hyps wits], []))))
+      |> Notes |> SOME
+  | finish_derived sign wits (Derived _) (Defines defs) = defs
+      |> map (apsnd (fn (d, _) =>
+           [([Thm.assume (cterm_of sign d) |> Drule.satisfy_hyps wits], [])]))
+      |> Notes |> SOME
+  | finish_derived _ wits (Derived _) (Notes facts) =
+    SOME (map_elem {name = I, var = I, typ = I, term = I,
+            fact = map (Drule.satisfy_hyps wits),
+            attrib = I} (Notes facts));
+
+
 (* CB: for finish_elems (Ext) *)
 
 fun closeup _ false elem = elem
@@ -1259,23 +1385,27 @@
       close (Defines (map #1 defs ~~ map (fn [(t, (ps, []))] => (t, ps)) propp))
   | finish_ext_elem _ _ (Notes facts, _) = Notes facts;
 
+
 (* CB: finish_parms introduces type info from parms to identifiers *)
 (* CB: only needed for types that have been NONE so far???
    If so, which are these??? *)
 
-fun finish_parms parms (((name, ps), axs), elems) =
-  (((name, map (fn (x, _) => (x, assoc (parms, x))) ps), axs), elems);
+fun finish_parms parms (((name, ps), mode), elems) =
+  (((name, map (fn (x, _) => (x, assoc (parms, x))) ps), mode), elems);
 
-fun finish_elems ctxt parms _ (text, ((id, Int e), _)) =
+fun finish_elems ctxt parms _ ((text, wits), ((id, Int e), _)) =
       let
-        val [(id', es)] = unify_elemss ctxt parms [(id, e)];
+        val [(id' as (_, mode), es)] = unify_elemss ctxt parms [(id, e)];
+        val wits' = case mode of Assumed _ => wits | Derived ths => wits @ ths;
         val text' = Library.foldl (eval_text ctxt id' false) (text, es);
-      in (text', (id', map Int es)) end
-  | finish_elems ctxt parms do_close (text, ((id, Ext e), [propp])) =
+        val es' = List.mapPartial
+              (finish_derived (ProofContext.theory_of ctxt) wits' mode) es;
+      in ((text', wits'), (id', map Int es')) end
+  | finish_elems ctxt parms do_close ((text, wits), ((id, Ext e), [propp])) =
       let
         val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp);
         val text' = eval_text ctxt id true (text, e');
-      in (text', (id, [Ext e'])) end;
+      in ((text', wits), (id, [Ext e'])) end
 
 in
 
@@ -1292,7 +1422,9 @@
    Works by building a context (through declare_elemss), extracting the
    required information and adjusting the context elements (finish_elemss).
    Can also universally close free vars in assms and defs.  This is only
-   needed for Ext elements and controlled by parameter do_close.  
+   needed for Ext elements and controlled by parameter do_close.
+
+   Only elements of assumed identifiers are considered.
 *)
 
 fun prep_elemss prep_parms prepp do_close context fixed_params raw_elemss raw_concl =
@@ -1338,8 +1470,8 @@
     (* CB: extract information from assumes and defines elements
        (fixes, constrains and notes in raw_elemss don't have an effect on
        text and elemss), compute final form of context elements. *)
-    val (text, elemss) = finish_elemss ctxt parms do_close
-      (((([], []), ([], [])), ([], [], [])), raw_elemss ~~ proppss);
+    val ((text, _), elemss) = finish_elemss ctxt parms do_close
+      ((((([], []), ([], [])), ([], [], [])), []), raw_elemss ~~ proppss);
     (* CB: text has the following structure:
            (((exts, exts'), (ints, ints')), (xs, env, defs))
        where
@@ -1417,8 +1549,11 @@
     val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close
       context fixed_params (raw_import_elemss @ raw_elemss) raw_concl;
     (* replace extended ids (for axioms) by ids *)
-    val all_elemss' = map (fn (((_, ps), _), (((n, ps'), ax), elems)) =>
-        (((n, List.filter (fn (p, _) => p mem ps) ps'), ax), elems))
+    val all_elemss' = map (fn (((_, ps), _), (((n, ps'), mode), elems)) =>
+        (((n, map (fn p => (p, assoc (ps', p) |> valOf)) ps), mode), elems))
+(*
+        (((n, List.filter (fn (p, _) => p mem ps) ps'), mode), elems))
+*)
       (ids ~~ all_elemss);
 
     (* CB: all_elemss and parms contain the correct parameter types *)
@@ -1429,8 +1564,9 @@
     val (ctxt, (elemss, _)) =
       activate_facts prep_facts (import_ctxt, qs);
     val stmt = gen_distinct Term.aconv
-       (List.concat (map (fn ((_, axs), _) =>
-         List.concat (map (#hyps o Thm.rep_thm) axs)) qs));
+       (List.concat (map (fn ((_, Assumed axs), _) =>
+         List.concat (map (#hyps o Thm.rep_thm) axs)
+                           | ((_, Derived _), _) => []) qs));
     val cstmt = map (cterm_of thy) stmt;
   in
     ((((import_ctxt, import_elemss), (ctxt, elemss, syn)), (parms, spec, defs)), (cstmt, concl))
@@ -1829,7 +1965,7 @@
                    val ts = List.concat (List.mapPartial (fn (Assumes asms) =>
                      SOME (List.concat (map (map #1 o #2) asms)) | _ => NONE) elems);
                    val (axs1, axs2) = splitAt (length ts, axs);
-                 in (axs2, ((id, axs1), elems)) end)
+                 in (axs2, ((id, Assumed axs1), elems)) end)
         |> snd;
     val (ctxt, (_, facts)) = activate_facts (K I)
       (pred_ctxt, axiomify predicate_axioms elemss');
@@ -1873,11 +2009,12 @@
       ts @ map (fn (_, (def, _)) => def) defs
   | extract_asms_elem (ts, Notes _) = ts;
 
-fun extract_asms_elems (id, elems) =
-      (id, Library.foldl extract_asms_elem ([], elems));
+fun extract_asms_elems ((id, Assumed _), elems) =
+      SOME (id, Library.foldl extract_asms_elem ([], elems))
+  | extract_asms_elems ((_, Derived _), _) = NONE;
 
 fun extract_asms_elemss elemss =
-      map extract_asms_elems elemss;
+      List.mapPartial extract_asms_elems elemss;
 
 (* activate instantiated facts in theory or context *)
 
@@ -1901,7 +2038,7 @@
       end;
 
 fun activate_facts_elems get_reg note_thmss attrib
-        disch (thy_ctxt, (id, elems)) =
+        disch (thy_ctxt, ((id, _), elems)) =
       let
         val ((prfx, atts2), _) = valOf (get_reg thy_ctxt id)
           handle Option => error ("(internal) unknown registration of " ^
@@ -1914,7 +2051,7 @@
 fun gen_activate_facts_elemss get_reg note_thmss attrib standard
         all_elemss new_elemss thy_ctxt =
       let
-        val prems = List.concat (List.mapPartial (fn (id, _) =>
+        val prems = List.concat (List.mapPartial (fn ((id, _), _) =>
               Option.map snd (get_reg thy_ctxt id)
                 handle Option => error ("(internal) unknown registration of " ^
                   quote (fst id) ^ " while activating facts.")) all_elemss);
@@ -1942,7 +2079,7 @@
     val ctxt' = ctxt |> ProofContext.theory_of |> ProofContext.init;
     val ((ids, _), raw_elemss) = flatten (ctxt', intern_expr thy)
           (([], Symtab.empty), Expr expr);
-    val ((parms, all_elemss, _), (spec, (xs, defs, _))) =
+    val ((parms, all_elemss, _), (_, (_, defs, _))) =
           read_elemss false ctxt' [] raw_elemss [];
 
 
@@ -2000,17 +2137,18 @@
     (** compute proof obligations **)
 
     (* restore "small" ids *)
-    val ids' = map (fn ((n, ps), _) =>
-          (n, map (fn p => Free (p, valOf (assoc (parms, p)))) ps)) ids;
+    val ids' = map (fn ((n, ps), (_, mode)) =>
+          ((n, map (fn p => Free (p, valOf (assoc (parms, p)))) ps), mode)) ids;
 
     (* instantiate ids and elements *)
     val inst_elemss = map
-          (fn (id, (_, elems)) => inst_tab_elems thy (inst, tinst) (id, 
-            map (fn Int e => e) elems)) 
+          (fn ((id, mode), (_, elems)) =>
+             inst_tab_elems thy (inst, tinst) (id, map (fn Int e => e) elems)
+               |> apfst (fn id => (id, mode))) 
           (ids' ~~ all_elemss);
 
     (* remove fragments already registered with theory or context *)
-    val new_inst_elemss = List.filter (fn (id, _) =>
+    val new_inst_elemss = List.filter (fn ((id, _), _) =>
           not (test_reg thy_ctxt id)) inst_elemss;
     val new_ids = map #1 new_inst_elemss;
 
@@ -2025,7 +2163,7 @@
        interpretation might contain a reference to the incomplete
        registration. *)
 
-    val thy_ctxt' = Library.foldl (fn (thy_ctxt, (id, _)) =>
+    val thy_ctxt' = Library.foldl (fn (thy_ctxt, ((id, _), _)) =>
           put_reg id attn' thy_ctxt) (thy_ctxt, new_inst_elemss);
 
   in (thy_ctxt', propss, activate inst_elemss new_inst_elemss) end;
@@ -2048,6 +2186,34 @@
      put_local_registration
      local_activate_facts_elemss;
 
+fun prep_registration_in_locale target expr thy =
+  (* target already in internal form *)
+  let
+    val ctxt = ProofContext.init thy;
+    val ((target_ids, target_syn), target_elemss) = flatten (ctxt, I)
+        (([], Symtab.empty), Expr (Locale target));
+    val fixed = the_locale thy target |> #params |> #1 |> map #1;
+    val ((all_ids, syn), raw_elemss) = flatten (ctxt, intern_expr thy)
+        ((target_ids, target_syn), Expr expr);
+    val ids = Library.drop (length target_ids, all_ids);
+    val ((parms, elemss, _), _) =
+        read_elemss false ctxt fixed raw_elemss [];
+
+    (** compute proof obligations **)
+
+    (* restore "small" ids, with mode *)
+    val ids' = map (apsnd snd) ids;
+    (* remove Int markers *)
+    val elemss' = map (fn (_, es) =>
+        map (fn Int e => e) es) elemss
+    (* extract assumptions and defs *)
+    val propss = extract_asms_elemss (ids' ~~ elemss');
+
+    (** add registrations to locale in theory **)
+    val thy' = fold (put_registration_in_locale target) (map fst ids') thy;
+
+  in (Locale target, thy', propss, I) end;
+
 end;  (* local *)