First release of interpretation commands.
authorballarin
Mon Apr 11 12:34:34 2005 +0200 (2005-04-11)
changeset 156961da4ce092c0b
parent 15695 f072119afa4e
child 15697 681bcb7f0389
First release of interpretation commands.
NEWS
src/FOL/ex/LocaleTest.thy
src/HOL/Algebra/CRing.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/UnivPoly.thy
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/axclass.ML
src/Pure/library.ML
src/Pure/pure_thy.ML
src/Pure/tactic.ML
src/ZF/Constructible/L_axioms.thy
     1.1 --- a/NEWS	Mon Apr 11 12:18:27 2005 +0200
     1.2 +++ b/NEWS	Mon Apr 11 12:34:34 2005 +0200
     1.3 @@ -222,6 +222,16 @@
     1.4    - Fixed parameter management in theorem generation for goals with "includes".
     1.5      INCOMPATIBILITY: rarely, the generated theorem statement is different.
     1.6  
     1.7 +* Locales:  new commands for the interpretation of locale expressions
     1.8 +  in theories (interpretation) and proof contexts (interpret).  These take an
     1.9 +  instantiation of the locale parameters and compute proof obligations from
    1.10 +  the instantiated specification.  After the obligations have been discharged,
    1.11 +  the instantiated theorems of the locale are added to the theory or proof
    1.12 +  context.  Interpretation is smart in that already active interpretations
    1.13 +  do not occur in proof obligations, neither are instantiated theorems stored
    1.14 +  in duplicate.
    1.15 +  Use print_interps to inspect active interpretations of a particular locale.
    1.16 +
    1.17  * New syntax
    1.18  
    1.19      <theorem_name> (<index>, ..., <index>-<index>, ...)
     2.1 --- a/src/FOL/ex/LocaleTest.thy	Mon Apr 11 12:18:27 2005 +0200
     2.2 +++ b/src/FOL/ex/LocaleTest.thy	Mon Apr 11 12:34:34 2005 +0200
     2.3 @@ -10,6 +10,13 @@
     2.4  
     2.5  theory LocaleTest = FOL:
     2.6  
     2.7 +ML {* set quick_and_dirty *}    (* allow for thm command in batch mode *)
     2.8 +ML {* set Toplevel.debug *}
     2.9 +ML {* set show_hyps *}
    2.10 +ML {* set show_sorts *}
    2.11 +
    2.12 +section {* interpretation *}
    2.13 +
    2.14  (* interpretation input syntax *)
    2.15  
    2.16  locale L
    2.17 @@ -26,8 +33,6 @@
    2.18  
    2.19  (* processing of locale expression *)
    2.20  
    2.21 -ML {* reset show_hyps *}
    2.22 -
    2.23  locale A = fixes a assumes asm_A: "a = a"
    2.24  
    2.25  locale (open) B = fixes b assumes asm_B [simp]: "b = b"
    2.26 @@ -37,14 +42,15 @@
    2.27  
    2.28  locale D = A + B + fixes d defines def_D: "d == (a = b)"
    2.29  
    2.30 -ML {* set show_sorts *}
    2.31 +theorem (in A)
    2.32 +  includes D
    2.33 +  shows True ..
    2.34 +
    2.35 +theorem (in D) True ..
    2.36  
    2.37  typedecl i
    2.38  arities i :: "term"
    2.39  
    2.40 -ML {* set Toplevel.debug *}
    2.41 -
    2.42 -ML {* set show_hyps *}
    2.43  
    2.44  interpretation p1: C ["X::'b" "Y::'b"] by (auto intro: A.intro C_axioms.intro)
    2.45    (* both X and Y get type 'b since 'b is the internal type of parameter b,
    2.46 @@ -52,10 +58,10 @@
    2.47  
    2.48  print_interps A
    2.49  
    2.50 -(* possible accesses
    2.51 +(* possible accesses *)
    2.52  thm p1.a.asm_A thm LocaleTest.p1.a.asm_A
    2.53  thm LocaleTest.asm_A thm p1.asm_A
    2.54 -*)
    2.55 +
    2.56  
    2.57  (* without prefix *)
    2.58  
    2.59 @@ -63,53 +69,211 @@
    2.60  
    2.61  print_interps A
    2.62  
    2.63 -(* possible accesses
    2.64 +(* possible accesses *)
    2.65  thm a.asm_A thm asm_A thm LocaleTest.a.asm_A thm LocaleTest.asm_A
    2.66 -*)
    2.67 +
    2.68  
    2.69  interpretation p2: D [X Y "Y = X"] by (auto intro: A.intro simp: eq_commute)
    2.70  
    2.71  print_interps D
    2.72  
    2.73 -(*
    2.74  thm p2.a.asm_A
    2.75 -*)
    2.76 +
    2.77  
    2.78  interpretation p3: D [X Y] .
    2.79  
    2.80  (* duplicate: not registered *)
    2.81 -(*
    2.82 -thm p3.a.asm_A
    2.83 -*)
    2.84 +
    2.85 +(* thm p3.a.asm_A *)
    2.86 +
    2.87  
    2.88  print_interps A
    2.89  print_interps B
    2.90  print_interps C
    2.91  print_interps D
    2.92  
    2.93 -(* not permitted *)
    2.94 -(*
    2.95 -interpretation p4: A ["x::?'a1"] apply (rule A.intro) apply rule done
    2.96 -*)
    2.97 +(* not permitted
    2.98 +
    2.99 +interpretation p4: A ["?x::?'a1"] apply (rule A.intro) apply rule done
   2.100 +
   2.101  print_interps A
   2.102 +*)
   2.103  
   2.104 -(* without a prefix *)
   2.105 -(* TODO!!!
   2.106 -interpretation A [Z] apply - apply (auto intro: A.intro) done
   2.107 -*)
   2.108 +interpretation p10: D + D a' b' d' [X Y _ U V _] by (auto intro: A.intro)
   2.109 +
   2.110 +corollary (in D) th_x: True ..
   2.111 +
   2.112 +(* possible accesses: for each registration *)
   2.113 +
   2.114 +thm p2.th_x thm p3.th_x thm p10.th_x
   2.115 +
   2.116 +lemma (in D) th_y: "d == (a = b)" .
   2.117 +
   2.118 +thm p2.th_y thm p3.th_y thm p10.th_y
   2.119 +
   2.120 +lemmas (in D) th_z = th_y
   2.121 +
   2.122 +thm p2.th_z
   2.123 +
   2.124 +thm asm_A
   2.125 +
   2.126 +section {* Interpretation in proof contexts *}
   2.127  
   2.128  theorem True
   2.129  proof -
   2.130    fix alpha::i and beta::i and gamma::i
   2.131 -  assume "A(alpha)"
   2.132 +  have alpha_A: "A(alpha)" by (auto intro: A.intro)
   2.133    then interpret p5: A [alpha] .
   2.134    print_interps A
   2.135 +  thm p5.asm_A
   2.136    interpret p6: C [alpha beta] by (auto intro: C_axioms.intro)
   2.137    print_interps A   (* p6 not added! *)
   2.138    print_interps C
   2.139  qed rule
   2.140  
   2.141 -(* lemma "bla.bla": True by rule *)
   2.142 +theorem (in A) True
   2.143 +proof -
   2.144 +  print_interps A
   2.145 +  fix beta and gamma
   2.146 +  interpret p9: D [a beta _]
   2.147 +    (* no proof obligation for A !!! *)
   2.148 +    apply - apply (rule refl) apply assumption done
   2.149 +qed rule
   2.150  
   2.151  
   2.152 +(* Definition involving free variable *)
   2.153 +
   2.154 +ML {* reset show_sorts *}
   2.155 +
   2.156 +locale E = fixes e defines e_def: "e(x) == x & x"
   2.157 +  notes e_def2 = e_def
   2.158 +
   2.159 +lemma (in E) True thm e_def by fast
   2.160 +
   2.161 +interpretation p7: E ["(%x. x)"] by simp
   2.162 +
   2.163 +(* TODO: goal mustn't be beta-reduced here, is doesn't match meta-hyp *)
   2.164 +
   2.165 +thm p7.e_def2
   2.166 +
   2.167 +locale E' = fixes e defines e_def: "e == (%x. x & x)"
   2.168 +  notes e_def2 = e_def
   2.169 +
   2.170 +interpretation p7': E' ["(%x. x)"] by simp
   2.171 +
   2.172 +thm p7'.e_def2
   2.173 +
   2.174 +(* Definition involving free variable in assm *)
   2.175 +
   2.176 +locale (open) F = fixes f assumes asm_F: "f --> x"
   2.177 +  notes asm_F2 = asm_F
   2.178 +
   2.179 +interpretation p8: F ["False"] by fast
   2.180 +
   2.181 +thm p8.asm_F2
   2.182 +
   2.183 +subsection {* Locale without assumptions *}
   2.184 +
   2.185 +locale L1 = notes rev_conjI [intro] = conjI [THEN iffD1 [OF conj_commute]]
   2.186 +
   2.187 +lemma "[| P; Q |] ==> P & Q"
   2.188 +proof -
   2.189 +  interpret my: L1 .           txt {* No chained fact required. *}
   2.190 +  assume Q and P               txt {* order reversed *}
   2.191 +  then show "P & Q" ..         txt {* Applies @{thm my.rev_conjI}. *}
   2.192 +qed
   2.193 +
   2.194 +locale L11 = notes rev_conjI = conjI [THEN iffD1 [OF conj_commute]]
   2.195 +
   2.196 +lemma "[| P; Q |] ==> P & Q"
   2.197 +proof -
   2.198 +  interpret [intro]: L11 .     txt {* Attribute supplied at instantiation. *}
   2.199 +  assume Q and P
   2.200 +  then show "P & Q" ..
   2.201 +qed
   2.202 +
   2.203 +subsection {* Simple locale with assumptions *}
   2.204 +
   2.205 +consts bin :: "[i, i] => i" (infixl "#" 60)
   2.206 +
   2.207 +axioms i_assoc: "(x # y) # z = x # (y # z)"
   2.208 +  i_comm: "x # y = y # x"
   2.209 +
   2.210 +locale L2 =
   2.211 +  fixes OP (infixl "+" 60)
   2.212 +  assumes assoc: "(x + y) + z = x + (y + z)"
   2.213 +    and comm: "x + y = y + x"
   2.214 +
   2.215 +lemma (in L2) lcomm: "x + (y + z) = y + (x + z)"
   2.216 +proof -
   2.217 +  have "x + (y + z) = (x + y) + z" by (simp add: assoc)
   2.218 +  also have "... = (y + x) + z" by (simp add: comm)
   2.219 +  also have "... = y + (x + z)" by (simp add: assoc)
   2.220 +  finally show ?thesis .
   2.221 +qed
   2.222 +
   2.223 +lemmas (in L2) AC = comm assoc lcomm
   2.224 +
   2.225 +lemma "(x::i) # y # z # w = y # x # w # z"
   2.226 +proof -
   2.227 +  interpret my: L2 ["op #"] by (rule L2.intro [of "op #", OF i_assoc i_comm])
   2.228 +    txt {* Chained fact required to discharge assumptions of @{text L2}
   2.229 +      and instantiate parameters. *}
   2.230 +  show ?thesis by (simp only: my.OP.AC)  (* or simply AC *)
   2.231 +qed
   2.232 +
   2.233 +subsection {* Nested locale with assumptions *}
   2.234 +
   2.235 +locale L3 =
   2.236 +  fixes OP (infixl "+" 60)
   2.237 +  assumes assoc: "(x + y) + z = x + (y + z)"
   2.238 +
   2.239 +locale L4 = L3 +
   2.240 +  assumes comm: "x + y = y + x"
   2.241 +
   2.242 +lemma (in L4) lcomm: "x + (y + z) = y + (x + z)"
   2.243 +proof -
   2.244 +  have "x + (y + z) = (x + y) + z" by (simp add: assoc)
   2.245 +  also have "... = (y + x) + z" by (simp add: comm)
   2.246 +  also have "... = y + (x + z)" by (simp add: assoc)
   2.247 +  finally show ?thesis .
   2.248 +qed
   2.249 +
   2.250 +lemmas (in L4) AC = comm assoc lcomm
   2.251 +
   2.252 +lemma "(x::i) # y # z # w = y # x # w # z"
   2.253 +proof -
   2.254 +  interpret my: L4 ["op #"]
   2.255 +    by (auto intro: L3.intro L4_axioms.intro i_assoc i_comm)
   2.256 +  show ?thesis by (simp only: my.OP.AC)  (* or simply AC *)
   2.257 +qed
   2.258 +
   2.259 +subsection {* Locale with definition *}
   2.260 +
   2.261 +text {* This example is admittedly not very creative :-) *}
   2.262 +
   2.263 +locale L5 = L4 + var A +
   2.264 +  defines A_def: "A == True"
   2.265 +
   2.266 +lemma (in L5) lem: A
   2.267 +  by (unfold A_def) rule
   2.268 +
   2.269 +lemma "L5(op #) ==> True"
   2.270 +proof -
   2.271 +  assume "L5(op #)"
   2.272 +  then interpret L5 ["op #"] by (auto intro: L5.axioms)
   2.273 +  show ?thesis by (rule lem)  (* lem instantiated to True *)
   2.274 +qed
   2.275 +
   2.276 +subsection {* Instantiation in a context with target *}
   2.277 +
   2.278 +lemma (in L4)
   2.279 +  fixes A (infixl "$" 60)
   2.280 +  assumes A: "L4(A)"
   2.281 +  shows "(x::i) $ y $ z $ w = y $ x $ w $ z"
   2.282 +proof -
   2.283 +  from A interpret A: L4 ["A"] by (auto intro: L4.axioms)
   2.284 +  show ?thesis by (simp only: A.OP.AC)
   2.285 +qed
   2.286 +
   2.287  end
     3.1 --- a/src/HOL/Algebra/CRing.thy	Mon Apr 11 12:18:27 2005 +0200
     3.2 +++ b/src/HOL/Algebra/CRing.thy	Mon Apr 11 12:34:34 2005 +0200
     3.3 @@ -574,10 +574,28 @@
     3.4  
     3.5  locale ring_hom_cring = cring R + cring S + var h +
     3.6    assumes homh [simp, intro]: "h \<in> ring_hom R S"
     3.7 +(*
     3.8    notes hom_closed [simp, intro] = ring_hom_closed [OF homh]
     3.9      and hom_mult [simp] = ring_hom_mult [OF homh]
    3.10      and hom_add [simp] = ring_hom_add [OF homh]
    3.11      and hom_one [simp] = ring_hom_one [OF homh]
    3.12 +*)
    3.13 +
    3.14 +lemma (in ring_hom_cring) hom_closed [simp, intro]:
    3.15 +  "x \<in> carrier R ==> h x \<in> carrier S"
    3.16 +  by (simp add: ring_hom_closed [OF homh])
    3.17 +
    3.18 +lemma (in ring_hom_cring) hom_mult [simp]:
    3.19 +  "[| x \<in> carrier R; y \<in> carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
    3.20 +  by (simp add: ring_hom_mult [OF homh])
    3.21 +
    3.22 +lemma (in ring_hom_cring) hom_add [simp]:
    3.23 +  "[| x \<in> carrier R; y \<in> carrier R |] ==> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
    3.24 +  by (simp add: ring_hom_add [OF homh])
    3.25 +
    3.26 +lemma (in ring_hom_cring) hom_one [simp]:
    3.27 +  "h \<one> = \<one>\<^bsub>S\<^esub>"
    3.28 +  by (simp add: ring_hom_one [OF homh])
    3.29  
    3.30  lemma (in ring_hom_cring) hom_zero [simp]:
    3.31    "h \<zero> = \<zero>\<^bsub>S\<^esub>"
     4.1 --- a/src/HOL/Algebra/Group.thy	Mon Apr 11 12:18:27 2005 +0200
     4.2 +++ b/src/HOL/Algebra/Group.thy	Mon Apr 11 12:34:34 2005 +0200
     4.3 @@ -469,7 +469,7 @@
     4.4    apply (simp_all add: prems group_def group.l_inv)
     4.5    done
     4.6  
     4.7 -text{*This alternative proof of the previous result demonstrates instantiate.
     4.8 +text{*This alternative proof of the previous result demonstrates interpret.
     4.9     It uses @{text Prod.inv_equality} (available after instantiation) instead of
    4.10     @{text "group.inv_equality [OF DirProd_group]"}. *}
    4.11  lemma
    4.12 @@ -478,9 +478,8 @@
    4.13        and h: "h \<in> carrier H"
    4.14    shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
    4.15  proof -
    4.16 -  have "group (G \<times>\<times> H)"
    4.17 -    by (blast intro: DirProd_group group.intro prems)
    4.18 -  then instantiate Prod: group
    4.19 +  interpret Prod: group ["G \<times>\<times> H"]
    4.20 +    by (auto intro: DirProd_group group.intro group.axioms prems)
    4.21    show ?thesis by (simp add: Prod.inv_equality g h)
    4.22  qed
    4.23    
    4.24 @@ -543,8 +542,19 @@
    4.25    @{term H}, with a homomorphism @{term h} between them*}
    4.26  locale group_hom = group G + group H + var h +
    4.27    assumes homh: "h \<in> hom G H"
    4.28 +(*
    4.29    notes hom_mult [simp] = hom_mult [OF homh]
    4.30      and hom_closed [simp] = hom_closed [OF homh]
    4.31 +CB: late binding problem?
    4.32 +*)
    4.33 +
    4.34 +lemma (in group_hom) hom_mult [simp]:
    4.35 +  "[| x \<in> carrier G; y \<in> carrier G |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
    4.36 +  by (simp add: hom_mult [OF homh])
    4.37 +
    4.38 +lemma (in group_hom) hom_closed [simp]:
    4.39 +  "x \<in> carrier G ==> h x \<in> carrier H"
    4.40 +  by (simp add: hom_closed [OF homh])
    4.41  
    4.42  lemma (in group_hom) one_closed [simp]:
    4.43    "h \<one> \<in> carrier H"
     5.1 --- a/src/HOL/Algebra/UnivPoly.thy	Mon Apr 11 12:18:27 2005 +0200
     5.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Mon Apr 11 12:34:34 2005 +0200
     5.3 @@ -1466,12 +1466,15 @@
     5.4    eval R S h s (monom P r n) = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n"
     5.5  proof -
     5.6    assume S: "s \<in> carrier S" and R: "r \<in> carrier R"
     5.7 +  from ring_hom_cring_P_S [OF S] interpret ring_hom_cring [P S "eval R S h s"]
     5.8 +    by - (rule ring_hom_cring.axioms, assumption)+
     5.9 +    (* why is simplifier invoked --- in done ??? *)
    5.10    from R S have "eval R S h s (monom P r n) =
    5.11      eval R S h s (monom P r 0 \<otimes>\<^bsub>P\<^esub> (monom P \<one> 1) (^)\<^bsub>P\<^esub> n)"
    5.12      by (simp del: monom_mult (* eval.hom_mult eval.hom_pow, delayed inst! *)
    5.13        add: monom_mult [THEN sym] monom_pow)
    5.14    also
    5.15 -  from ring_hom_cring_P_S [OF S] instantiate eval: ring_hom_cring
    5.16 +  (*  from ring_hom_cring_P_S [OF S] instantiate eval: ring_hom_cring *)
    5.17    from R S eval_monom1 have "... = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n"
    5.18      by (simp add: eval_const)
    5.19    finally show ?thesis .
    5.20 @@ -1482,7 +1485,11 @@
    5.21    eval R S h s (r \<odot>\<^bsub>P\<^esub> p) = h r \<otimes>\<^bsub>S\<^esub> eval R S h s p"
    5.22  proof -
    5.23    assume S: "s \<in> carrier S" and R: "r \<in> carrier R" and P: "p \<in> carrier P"
    5.24 +  from ring_hom_cring_P_S [OF S] interpret ring_hom_cring [P S "eval R S h s"]
    5.25 +    by - (rule ring_hom_cring.axioms, assumption)+
    5.26 +(*
    5.27    from ring_hom_cring_P_S [OF S] instantiate eval: ring_hom_cring
    5.28 +*)
    5.29    from S R P show ?thesis
    5.30      by (simp add: monom_mult_is_smult [THEN sym] eval_const)
    5.31  qed
    5.32 @@ -1503,20 +1510,20 @@
    5.33      and S: "s \<in> carrier S" and P: "p \<in> carrier P"
    5.34    shows "Phi p = Psi p"
    5.35  proof -
    5.36 -  have Phi_hom: "ring_hom_cring P S Phi"
    5.37 -    by (auto intro: ring_hom_cringI UP_cring S.cring Phi)
    5.38 -  have Psi_hom: "ring_hom_cring P S Psi"
    5.39 -    by (auto intro: ring_hom_cringI UP_cring S.cring Psi)
    5.40 +  from UP_cring interpret cring [P] by - (rule cring.axioms, assumption)+
    5.41 +  interpret Phi: ring_hom_cring [P S Phi]
    5.42 +    by (auto intro: ring_hom_cring.axioms ring_hom_cringI UP_cring S.cring Phi)
    5.43 +  interpret Psi: ring_hom_cring [P S Psi]
    5.44 +    by (auto intro: ring_hom_cring.axioms ring_hom_cringI UP_cring S.cring Psi)
    5.45 +
    5.46    have "Phi p =
    5.47        Phi (\<Oplus>\<^bsub>P \<^esub>i \<in> {..deg R p}. monom P (coeff P p i) 0 \<otimes>\<^bsub>P\<^esub> monom P \<one> 1 (^)\<^bsub>P\<^esub> i)"
    5.48      by (simp add: up_repr P S monom_mult [THEN sym] monom_pow del: monom_mult)
    5.49 -  also 
    5.50 -    from Phi_hom instantiate Phi: ring_hom_cring
    5.51 -    from Psi_hom instantiate Psi: ring_hom_cring
    5.52 -    have "... =
    5.53 +  also
    5.54 +  have "... =
    5.55        Psi (\<Oplus>\<^bsub>P \<^esub>i\<in>{..deg R p}. monom P (coeff P p i) 0 \<otimes>\<^bsub>P\<^esub> monom P \<one> 1 (^)\<^bsub>P\<^esub> i)"
    5.56      by (simp add: Phi Psi P S Pi_def comp_def)
    5.57 -(* Without instantiate, the following command would have been necessary.
    5.58 +(* Without interpret, the following command would have been necessary.
    5.59      by (simp add: ring_hom_cring.hom_finsum [OF Phi_hom]
    5.60        ring_hom_cring.hom_mult [OF Phi_hom]
    5.61        ring_hom_cring.hom_pow [OF Phi_hom] Phi
     6.1 --- a/src/Pure/Isar/isar_thy.ML	Mon Apr 11 12:18:27 2005 +0200
     6.2 +++ b/src/Pure/Isar/isar_thy.ML	Mon Apr 11 12:34:34 2005 +0200
     6.3 @@ -58,11 +58,17 @@
     6.4      -> bool -> theory -> ProofHistory.T
     6.5    val theorem_i: string -> (bstring * theory attribute list) *
     6.6      (term * (term list * term list)) -> bool -> theory -> ProofHistory.T
     6.7 -  val multi_theorem: string -> (theory -> theory) -> bstring * Args.src list
     6.8 +  val multi_theorem:
     6.9 +    string -> (theory -> theory) -> 
    6.10 +    (cterm list -> Proof.context -> Proof.context -> thm -> thm) ->
    6.11 +    bstring * Args.src list
    6.12      -> Args.src Locale.element Locale.elem_expr list
    6.13      -> ((bstring * Args.src list) * (string * (string list * string list)) list) list
    6.14      -> bool -> theory -> ProofHistory.T
    6.15 -  val multi_theorem_i: string -> (theory -> theory) -> bstring * theory attribute list
    6.16 +  val multi_theorem_i:
    6.17 +    string -> (theory -> theory) ->  
    6.18 +    (cterm list -> Proof.context -> Proof.context -> thm -> thm) ->
    6.19 +    bstring * theory attribute list
    6.20      -> Locale.multi_attribute Locale.element_i Locale.elem_expr list
    6.21      -> ((bstring * theory attribute list) * (term * (term list * term list)) list) list
    6.22      -> bool -> theory -> ProofHistory.T
    6.23 @@ -378,28 +384,33 @@
    6.24  
    6.25  in
    6.26  
    6.27 -fun multi_theorem k thy_mod a elems concl int thy =
    6.28 -  global_statement (Proof.multi_theorem k thy_mod NONE (apsnd (map (Attrib.global_attribute thy)) a)
    6.29 +fun multi_theorem k thy_mod export a elems concl int thy =
    6.30 +  global_statement (Proof.multi_theorem k thy_mod export NONE (apsnd (map (Attrib.global_attribute thy)) a)
    6.31      (map (Locale.map_attrib_elem_or_expr (Attrib.multi_attribute thy)) elems)) concl int thy;
    6.32  
    6.33 -fun multi_theorem_i k thy_mod a = global_statement_i o Proof.multi_theorem_i k thy_mod NONE a;
    6.34 +fun multi_theorem_i k thy_mod export a = global_statement_i o Proof.multi_theorem_i k thy_mod export NONE a;
    6.35  
    6.36  fun locale_multi_theorem k locale (name, atts) elems concl int thy =
    6.37 -  global_statement (Proof.multi_theorem k I
    6.38 +  global_statement (Proof.multi_theorem k I ProofContext.export_standard
    6.39        (SOME (locale, (map (Attrib.multi_attribute thy) atts,
    6.40            map (map (Attrib.multi_attribute thy) o snd o fst) concl)))
    6.41        (name, []) (map (Locale.map_attrib_elem_or_expr (Attrib.multi_attribute thy)) elems))
    6.42        (map (apfst (apsnd (K []))) concl) int thy;
    6.43  
    6.44  fun locale_multi_theorem_i k locale (name, atts) elems concl =
    6.45 -  global_statement_i (Proof.multi_theorem_i k I (SOME (locale, (atts, map (snd o fst) concl)))
    6.46 +  global_statement_i (Proof.multi_theorem_i k I ProofContext.export_standard
    6.47 +      (SOME (locale, (atts, map (snd o fst) concl)))
    6.48        (name, []) elems) (map (apfst (apsnd (K []))) concl);
    6.49  
    6.50 -fun theorem k (a, t) = multi_theorem k I a [] [(("", []), [t])];
    6.51 -fun theorem_i k (a, t) = multi_theorem_i k I a [] [(("", []), [t])];
    6.52 +fun theorem k (a, t) = multi_theorem k I ProofContext.export_standard
    6.53 +       a [] [(("", []), [t])];
    6.54 +fun theorem_i k (a, t) = multi_theorem_i k I ProofContext.export_standard
    6.55 +       a [] [(("", []), [t])];
    6.56  
    6.57 -fun smart_multi_theorem k NONE a elems = multi_theorem k I a elems
    6.58 -  | smart_multi_theorem k (SOME locale) a elems = locale_multi_theorem k locale a elems;
    6.59 +fun smart_multi_theorem k NONE a elems =
    6.60 +      multi_theorem k I ProofContext.export_standard a elems
    6.61 +  | smart_multi_theorem k (SOME locale) a elems =
    6.62 +      locale_multi_theorem k locale a elems;
    6.63  
    6.64  val assume      = local_statement Proof.assume I;
    6.65  val assume_i    = local_statement_i Proof.assume_i I;
    6.66 @@ -640,8 +651,10 @@
    6.67          (Locale.add_global_witness id thm' thy, thm')
    6.68        end;
    6.69    in
    6.70 -    multi_theorem_i Drule.internalK activate ("", []) [] 
    6.71 -      (map (fn (id as (n, _), props) => ((NameSpace.base n, [witness id]), 
    6.72 +    multi_theorem_i Drule.internalK activate ProofContext.export_plain
    6.73 +      ("", []) [] 
    6.74 +      (map (fn ((n, ps), props) => 
    6.75 +          ((NameSpace.base n, [witness (n, map Logic.varify ps)]), 
    6.76          map (fn prop => (prop, ([], []))) props)) propss) b thy'
    6.77    end;
    6.78  
     7.1 --- a/src/Pure/Isar/locale.ML	Mon Apr 11 12:18:27 2005 +0200
     7.2 +++ b/src/Pure/Isar/locale.ML	Mon Apr 11 12:34:34 2005 +0200
     7.3 @@ -71,19 +71,26 @@
     7.4    val print_global_registrations: string -> theory -> unit
     7.5    val print_local_registrations: string -> context -> unit
     7.6  
     7.7 -  val add_locale: bool -> bstring -> expr -> multi_attribute element list -> theory -> theory
     7.8 -  val add_locale_i: bool -> bstring -> expr -> multi_attribute element_i list
     7.9 -    -> theory -> theory
    7.10 -  val smart_note_thmss: string -> (string * 'a) option ->
    7.11 +  (* Storing results *)
    7.12 +  val add_locale:
    7.13 +    bool -> bstring -> expr -> multi_attribute element list -> theory -> theory
    7.14 +  val add_locale_i:
    7.15 +    bool -> bstring -> expr -> multi_attribute element_i list ->
    7.16 +    theory -> theory
    7.17 +  val smart_note_thmss:
    7.18 +    string -> (string * 'a) option ->
    7.19      ((bstring * theory attribute list) * (thm list * theory attribute list) list) list ->
    7.20      theory -> theory * (bstring * thm list) list
    7.21 -  val note_thmss: string -> xstring ->
    7.22 +  val note_thmss:
    7.23 +    string -> xstring ->
    7.24      ((bstring * multi_attribute list) * (thmref * multi_attribute list) list) list ->
    7.25      theory -> theory * (bstring * thm list) list
    7.26 -  val note_thmss_i: string -> string ->
    7.27 +  val note_thmss_i:
    7.28 +    string -> string ->
    7.29      ((bstring * multi_attribute list) * (thm list * multi_attribute list) list) list ->
    7.30      theory -> theory * (bstring * thm list) list
    7.31 -  val add_thmss: string -> ((string * thm list) * multi_attribute list) list ->
    7.32 +  val add_thmss:
    7.33 +    string -> string -> ((string * thm list) * multi_attribute list) list ->
    7.34      theory * context -> (theory * context) * (string * thm list) list
    7.35  
    7.36    (* Locale interpretation *)
    7.37 @@ -232,8 +239,22 @@
    7.38  
    7.39  (* access registrations *)
    7.40  
    7.41 +(* Ids of global registrations are varified,
    7.42 +   Ids of local registrations are not.
    7.43 +   Thms of registrations are never varified. *)
    7.44 +
    7.45  (* retrieve registration from theory or context *)
    7.46  
    7.47 +fun gen_get_registrations get thy_ctxt name =
    7.48 +  case Symtab.lookup (get thy_ctxt, name) of
    7.49 +      NONE => []
    7.50 +    | SOME tab => Termlisttab.dest tab;
    7.51 +
    7.52 +val get_global_registrations =
    7.53 +     gen_get_registrations (#3 o GlobalLocalesData.get);
    7.54 +val get_local_registrations =
    7.55 +     gen_get_registrations LocalLocalesData.get;
    7.56 +
    7.57  fun gen_get_registration get thy_ctxt (name, ps) =
    7.58    case Symtab.lookup (get thy_ctxt, name) of
    7.59        NONE => NONE
    7.60 @@ -271,6 +292,7 @@
    7.61           (space, locs, f regs)));
    7.62  val put_local_registration = gen_put_registration LocalLocalesData.map;
    7.63  
    7.64 +(* TODO: needed? *)
    7.65  fun smart_put_registration id attn ctxt =
    7.66    (* ignore registration if already present in theory *)
    7.67       let
    7.68 @@ -328,8 +350,14 @@
    7.69      val regs = get_regs thy_ctxt;
    7.70      val prt_term = Pretty.quote o Sign.pretty_term sg;
    7.71      fun prt_inst (ts, ((prfx, _), thms)) =
    7.72 -      Pretty.block [Pretty.str prfx, Pretty.str ":", Pretty.brk 1,
    7.73 -        Pretty.list "(" ")" (map prt_term ts)];
    7.74 +         let
    7.75 +           val pp_ts = Pretty.enclose "(" ")"
    7.76 +             (Pretty.breaks (map prt_term ts));
    7.77 +         in
    7.78 +           if prfx = "" then Pretty.block [pp_ts]
    7.79 +           else Pretty.block
    7.80 +             [Pretty.str prfx, Pretty.str ":", Pretty.brk 1, pp_ts]
    7.81 +         end;
    7.82      val loc_regs = Symtab.lookup (regs, loc_int);
    7.83    in
    7.84      (case loc_regs of
    7.85 @@ -463,6 +491,114 @@
    7.86        Notes (map (apsnd (map (apfst (map (inst_thm ctxt env))))) facts);
    7.87  
    7.88  
    7.89 +(* term and type instantiation, variant using symbol tables *)
    7.90 +
    7.91 +(* instantiate TFrees *)
    7.92 +
    7.93 +fun tinst_tab_type tinst T = if Symtab.is_empty tinst
    7.94 +      then T
    7.95 +      else Term.map_type_tfree
    7.96 +        (fn (v as (x, _)) => getOpt (Symtab.lookup (tinst, x), (TFree v))) T;
    7.97 +
    7.98 +fun tinst_tab_term tinst t = if Symtab.is_empty tinst
    7.99 +      then t
   7.100 +      else Term.map_term_types (tinst_tab_type tinst) t;
   7.101 +
   7.102 +fun tinst_tab_thm sg tinst thm = if Symtab.is_empty tinst
   7.103 +      then thm
   7.104 +      else let
   7.105 +          val cert = Thm.cterm_of sg;
   7.106 +          val certT = Thm.ctyp_of sg;
   7.107 +          val {hyps, prop, ...} = Thm.rep_thm thm;
   7.108 +          val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
   7.109 +          val tinst' = Symtab.dest tinst |>
   7.110 +                List.filter (fn (a, _) => a mem_string tfrees);
   7.111 +        in
   7.112 +          if null tinst' then thm
   7.113 +          else thm |> Drule.implies_intr_list (map cert hyps)
   7.114 +            |> Drule.tvars_intr_list (map #1 tinst')
   7.115 +            |> (fn (th, al) => th |> Thm.instantiate
   7.116 +                ((map (fn (a, T) => (valOf (assoc (al, a)), certT T)) tinst'),
   7.117 +                  []))
   7.118 +            |> (fn th => Drule.implies_elim_list th
   7.119 +                 (map (Thm.assume o cert o tinst_tab_term tinst) hyps))
   7.120 +        end;
   7.121 +
   7.122 +fun tinst_tab_elem _ tinst (Fixes fixes) =
   7.123 +      Fixes (map (fn (x, T, mx) => (x, Option.map (tinst_tab_type tinst) T, mx)) fixes)
   7.124 +  | tinst_tab_elem _ tinst (Assumes asms) =
   7.125 +      Assumes (map (apsnd (map (fn (t, (ps, qs)) =>
   7.126 +        (tinst_tab_term tinst t,
   7.127 +          (map (tinst_tab_term tinst) ps, map (tinst_tab_term tinst) qs))))) asms)
   7.128 +  | tinst_tab_elem _ tinst (Defines defs) =
   7.129 +      Defines (map (apsnd (fn (t, ps) =>
   7.130 +        (tinst_tab_term tinst t, map (tinst_tab_term tinst) ps))) defs)
   7.131 +  | tinst_tab_elem sg tinst (Notes facts) =
   7.132 +      Notes (map (apsnd (map (apfst (map (tinst_tab_thm sg tinst))))) facts);
   7.133 +
   7.134 +(* instantiate TFrees and Frees *)
   7.135 +
   7.136 +fun inst_tab_term (inst, tinst) = if Symtab.is_empty inst
   7.137 +      then tinst_tab_term tinst
   7.138 +      else (* instantiate terms and types simultaneously *)
   7.139 +        let
   7.140 +          fun instf (Const (x, T)) = Const (x, tinst_tab_type tinst T)
   7.141 +            | instf (Free (x, T)) = (case Symtab.lookup (inst, x) of
   7.142 +                 NONE => Free (x, tinst_tab_type tinst T)
   7.143 +               | SOME t => t)
   7.144 +            | instf (Var (xi, T)) = Var (xi, tinst_tab_type tinst T)
   7.145 +            | instf (b as Bound _) = b
   7.146 +            | instf (Abs (x, T, t)) = Abs (x, tinst_tab_type tinst T, instf t)
   7.147 +            | instf (s $ t) = instf s $ instf t
   7.148 +        in instf end;
   7.149 +
   7.150 +fun inst_tab_thm sg (inst, tinst) thm = if Symtab.is_empty inst
   7.151 +      then tinst_tab_thm sg tinst thm
   7.152 +      else let
   7.153 +          val cert = Thm.cterm_of sg;
   7.154 +          val certT = Thm.ctyp_of sg;
   7.155 +          val {hyps, prop, ...} = Thm.rep_thm thm;
   7.156 +          (* type instantiations *)
   7.157 +          val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
   7.158 +          val tinst' = Symtab.dest tinst |>
   7.159 +                List.filter (fn (a, _) => a mem_string tfrees);
   7.160 +          (* term instantiations;
   7.161 +             note: lhss are type instantiated, because
   7.162 +                   type insts will be done first*)
   7.163 +          val frees = foldr Term.add_term_frees [] (prop :: hyps);
   7.164 +          val inst' = Symtab.dest inst |>
   7.165 +                List.mapPartial (fn (a, t) =>
   7.166 +                  get_first (fn (Free (x, T)) => 
   7.167 +                    if a = x then SOME (Free (x, tinst_tab_type tinst T), t)
   7.168 +                    else NONE) frees);
   7.169 +        in
   7.170 +          if null tinst' andalso null inst' then tinst_tab_thm sg tinst thm
   7.171 +          else thm |> Drule.implies_intr_list (map cert hyps)
   7.172 +            |> Drule.tvars_intr_list (map #1 tinst')
   7.173 +            |> (fn (th, al) => th |> Thm.instantiate
   7.174 +                ((map (fn (a, T) => (valOf (assoc (al, a)), certT T)) tinst'),
   7.175 +                  []))
   7.176 +            |> Drule.forall_intr_list (map (cert o #1) inst')
   7.177 +            |> Drule.forall_elim_list (map (cert o #2) inst') 
   7.178 +            |> (fn th => Drule.implies_elim_list th
   7.179 +                 (map (Thm.assume o cert o inst_tab_term (inst, tinst)) hyps))
   7.180 +        end;
   7.181 +
   7.182 +fun inst_tab_elem _ (_, tinst) (Fixes fixes) =
   7.183 +      Fixes (map (fn (x, T, mx) => (x, Option.map (tinst_tab_type tinst) T, mx)) fixes)
   7.184 +  | inst_tab_elem _ inst (Assumes asms) =
   7.185 +      Assumes (map (apsnd (map (fn (t, (ps, qs)) =>
   7.186 +        (inst_tab_term inst t,
   7.187 +          (map (inst_tab_term inst) ps, map (inst_tab_term inst) qs))))) asms)
   7.188 +  | inst_tab_elem _ inst (Defines defs) =
   7.189 +      Defines (map (apsnd (fn (t, ps) =>
   7.190 +        (inst_tab_term inst t, map (inst_tab_term inst) ps))) defs)
   7.191 +  | inst_tab_elem sg inst (Notes facts) =
   7.192 +      Notes (map (apsnd (map (apfst (map (inst_tab_thm sg inst))))) facts);
   7.193 +
   7.194 +fun inst_tab_elems sign inst ((n, ps), elems) =
   7.195 +      ((n, map (inst_tab_term inst) ps), map (inst_tab_elem sign inst) elems);
   7.196 +
   7.197  
   7.198  (** structured contexts: rename + merge + implicit type instantiation **)
   7.199  
   7.200 @@ -781,7 +917,14 @@
   7.201    let val ((ctxt', _), res) =
   7.202      foldl_map (activate_elem (name = "")) ((ProofContext.qualified true ctxt, axs), elems)
   7.203        handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)]
   7.204 -  in (ProofContext.restore_qualified ctxt ctxt', res) end;
   7.205 +    val ctxt'' = if name = "" then ctxt'
   7.206 +          else let
   7.207 +              val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
   7.208 +              val ctxt'' = put_local_registration (name, ps') ("", []) ctxt'
   7.209 +            in foldl (fn (ax, ctxt) =>
   7.210 +              add_local_witness (name, ps') (Thm.assume (Thm.cprop_of ax)) ctxt) ctxt'' axs
   7.211 +            end
   7.212 +  in (ProofContext.restore_qualified ctxt ctxt'', res) end;
   7.213  
   7.214  fun activate_elemss prep_facts = foldl_map (fn (ctxt, (((name, ps), axs), raw_elems)) =>
   7.215    let
   7.216 @@ -808,6 +951,20 @@
   7.217  end;
   7.218  
   7.219  
   7.220 +(* register elements *)
   7.221 +
   7.222 +fun register_elems (((_, ps), (((name, ax_ps), axs), _)), ctxt) =
   7.223 +  if name = "" then ctxt
   7.224 +      else let val ps' = map (fn (n, SOME T) => Free (n, T)) ax_ps
   7.225 +          val ctxt' = put_local_registration (name, ps') ("", []) ctxt
   7.226 +        in foldl (fn (ax, ctxt) =>
   7.227 +          add_local_witness (name, ps') ax ctxt) ctxt' axs
   7.228 +        end;
   7.229 +
   7.230 +fun register_elemss id_elemss ctxt = 
   7.231 +  foldl register_elems ctxt id_elemss;
   7.232 +
   7.233 +
   7.234  (** prepare context elements **)
   7.235  
   7.236  (* expressions *)
   7.237 @@ -856,8 +1013,8 @@
   7.238  *)
   7.239  
   7.240  fun flatten _ (ids, Elem (Fixes fixes)) =
   7.241 -      (ids, [((("", map (rpair NONE o #1) fixes), []), Ext (Fixes fixes))])
   7.242 -  | flatten _ (ids, Elem elem) = (ids, [((("", []), []), Ext elem)])
   7.243 +      (ids @ [(("", map #1 fixes), ([], []))], [((("", map (rpair NONE o #1) fixes), []), Ext (Fixes fixes))])
   7.244 +  | flatten _ (ids, Elem elem) = (ids @ [(("", []), ([], []))], [((("", []), []), Ext elem)])
   7.245    | flatten (ctxt, prep_expr) (ids, Expr expr) =
   7.246        apsnd (map (apsnd Int)) (flatten_expr ctxt (ids, prep_expr expr));
   7.247  
   7.248 @@ -1036,7 +1193,6 @@
   7.249      (* CB: process patterns (conclusion and external elements only) *)
   7.250      val (ctxt, all_propp) =
   7.251        prepp (ProofContext.declare_terms (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
   7.252 -    
   7.253      (* CB: add type information from conclusion and external elements
   7.254         to context *)
   7.255      val ctxt = ProofContext.declare_terms (List.concat (map (map fst) all_propp)) ctxt;
   7.256 @@ -1128,14 +1284,21 @@
   7.257  
   7.258      val (import_ids, raw_import_elemss) = flatten (context, prep_expr sign) ([], Expr import);
   7.259      (* CB: normalise "includes" among elements *)
   7.260 -    val raw_elemss = List.concat (#2 ((foldl_map (flatten (context, prep_expr sign))
   7.261 -      (import_ids, elements))));
   7.262 +    val (ids, raw_elemsss) = foldl_map (flatten (context, prep_expr sign))
   7.263 +      (import_ids, elements);
   7.264 +
   7.265 +    val raw_elemss = List.concat raw_elemsss;
   7.266      (* CB: raw_import_elemss @ raw_elemss is the normalised list of
   7.267         context elements obtained from import and elements. *)
   7.268      val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close
   7.269        context fixed_params (raw_import_elemss @ raw_elemss) raw_concl;
   7.270 +    (* replace extended ids (for axioms) by ids *)
   7.271 +    val all_elemss' = map (fn (((_, ps), _), (((n, ps'), ax), elems)) =>
   7.272 +        (((n, List.filter (fn (p, _) => p mem ps) ps'), ax), elems))
   7.273 +      (ids ~~ all_elemss);
   7.274 +
   7.275      (* CB: all_elemss and parms contain the correct parameter types *)
   7.276 -    val (ps,qs) = splitAt(length raw_import_elemss, all_elemss)
   7.277 +    val (ps,qs) = splitAt(length raw_import_elemss, all_elemss')
   7.278      val (import_ctxt, (import_elemss, _)) =
   7.279        activate_facts prep_facts (context, ps);
   7.280  
   7.281 @@ -1162,7 +1325,7 @@
   7.282            let val {predicate = (stmt, _), params = (ps, _), ...} =
   7.283              the_locale thy name
   7.284            in (stmt, param_types ps, Locale name) end);
   7.285 -    val ((((locale_ctxt, _), (elems_ctxt, _)), _), (elems_stmt, concl')) =
   7.286 +    val ((((locale_ctxt, locale_elemss), (elems_ctxt, _)), _), (elems_stmt, concl')) =
   7.287        prep_ctxt false fixed_params import elems concl ctxt;
   7.288    in (locale, (target_stmt, elems_stmt), locale_ctxt, elems_ctxt, concl') end;
   7.289  
   7.290 @@ -1404,6 +1567,8 @@
   7.291  
   7.292  in
   7.293  
   7.294 +(* store exported theorem in theory *)
   7.295 +
   7.296  fun note_thmss_qualified kind name args thy =
   7.297    thy
   7.298    |> Theory.add_path (Sign.base_name name)
   7.299 @@ -1411,30 +1576,84 @@
   7.300    |>> hide_bound_names (map (#1 o #1) args)
   7.301    |>> Theory.parent_path;
   7.302  
   7.303 -fun note_thms_qualified' kind (arg as ((name, atts), thms)) thy =
   7.304 +(* accesses of interpreted theorems *)
   7.305 +
   7.306 +(* fully qualified name in theory is T.p.r.n where
   7.307 +   T: theory name, p: interpretation prefix, r: renaming prefix, n: name *)
   7.308 +
   7.309 +fun global_accesses prfx name =
   7.310 +     if prfx = "" then
   7.311 +       case NameSpace.unpack name of
   7.312 +	   [] => [""]
   7.313 +	 | [T, n] => map NameSpace.pack [[T, n], [n]]
   7.314 +	 | [T, r, n] => map NameSpace.pack [[T, r, n], [T, n], [r, n], [n]]
   7.315 +	 | _ => error ("Locale accesses: illegal name " ^ quote name)
   7.316 +     else case NameSpace.unpack name of
   7.317 +           [] => [""]
   7.318 +         | [T, p, n] => map NameSpace.pack [[T, p, n], [p, n]]
   7.319 +         | [T, p, r, n] => map NameSpace.pack
   7.320 +             [[T, p, r, n], [T, p, n], [p, r, n], [p, n]]
   7.321 +         | _ => error ("Locale accesses: illegal name " ^ quote name);
   7.322 +
   7.323 +(* fully qualified name in context is p.r.n where
   7.324 +   p: interpretation prefix, r: renaming prefix, n: name *)
   7.325 +
   7.326 +fun local_accesses prfx name =
   7.327 +     if prfx = "" then
   7.328 +       case NameSpace.unpack name of
   7.329 +	   [] => [""]
   7.330 +	 | [n] => map NameSpace.pack [[n]]
   7.331 +	 | [r, n] => map NameSpace.pack [[r, n], [n]]
   7.332 +	 | _ => error ("Locale accesses: illegal name " ^ quote name)
   7.333 +     else case NameSpace.unpack name of
   7.334 +           [] => [""]
   7.335 +         | [p, n] => map NameSpace.pack [[p, n]]
   7.336 +         | [p, r, n] => map NameSpace.pack [[p, r, n], [p, n]]
   7.337 +         | _ => error ("Locale accesses: illegal name " ^ quote name);
   7.338 +
   7.339 +
   7.340 +(* store instantiations of args for all registered interpretations
   7.341 +   of the theory *)
   7.342 +
   7.343 +fun note_thmss_registrations kind target args thy =
   7.344    let
   7.345 -    val qname = NameSpace.unpack name
   7.346 -  in
   7.347 -    if length qname <= 1
   7.348 -    then PureThy.note_thmss_i kind [arg] thy
   7.349 -  else let val (prfx, n) = split_last qname
   7.350 -    in thy
   7.351 -      |> Theory.add_path (NameSpace.pack prfx)
   7.352 -      |> PureThy.note_thmss_i kind [((n, atts), thms)]
   7.353 -      |>> funpow (length prfx) Theory.parent_path
   7.354 -    end
   7.355 -  end;
   7.356 +    val ctxt = ProofContext.init thy;
   7.357 +    val sign = Theory.sign_of thy;
   7.358 +
   7.359 +    val (parms, parmTs_o) =
   7.360 +          the_locale thy target |> #params |> fst |> split_list;
   7.361 +    val parmvTs = map (Type.varifyT o valOf) parmTs_o;
   7.362 +    val ids = flatten (ctxt, intern_expr sign) ([], Expr (Locale target))
   7.363 +          |> fst |> map fst;
   7.364 +
   7.365 +    val regs = get_global_registrations thy target;
   7.366 +
   7.367 +    (* add args to thy for all registrations *)
   7.368  
   7.369 -(* prfx may be empty (not yet), names (in args) may be qualified *)
   7.370 +    fun activate (thy, (vts, ((prfx, atts2), _))) =
   7.371 +      let
   7.372 +        val ts = map Logic.unvarify vts;
   7.373 +        (* type instantiation *)
   7.374 +        val vtinst = Library.foldl (Type.typ_match (Sign.tsig_of sign))
   7.375 +             (Vartab.empty, (parmvTs ~~ map Term.fastype_of ts));
   7.376 +        val tinst = Vartab.dest vtinst |> map (fn ((x, 0), T) => (x, T))
   7.377 +             |> Symtab.make;            
   7.378 +        (* replace parameter names in ids by instantiations *)
   7.379 +        val vinst = Symtab.make (parms ~~ vts);
   7.380 +        fun vinst_names ps = map (fn p => Symtab.lookup (vinst, p) |> valOf) ps;
   7.381 +        val inst = Symtab.make (parms ~~ ts);
   7.382 +        val ids' = map (apsnd vinst_names) ids;
   7.383 +        val prems = List.concat (map (snd o valOf o get_global_registration thy) ids');
   7.384 +        val args' = map (fn ((n, atts), [(ths, [])]) =>
   7.385 +            ((if prfx = "" orelse n = "" then ""
   7.386 +              else NameSpace.pack [prfx, n], map fst atts @ atts2),
   7.387 +             [(map (Drule.standard o Drule.satisfy_hyps prems o inst_tab_thm sign (inst, tinst)) ths, [])]))
   7.388 +          args;
   7.389 +      in
   7.390 +        PureThy.note_thmss_accesses_i (global_accesses prfx) (Drule.kind kind) args' thy |> fst
   7.391 +      end;
   7.392 +  in Library.foldl activate (thy, regs) end;
   7.393  
   7.394 -fun note_thmss_qualified' kind prfx args thy =
   7.395 -  thy
   7.396 -  |> Theory.add_path (Sign.base_name prfx)
   7.397 -  |> (fn thy => Library.foldl (fn ((thy, res), arg) =>
   7.398 -        let val (thy', res') = note_thms_qualified' (Drule.kind kind) arg thy
   7.399 -        in (thy', res @ res') end) ((thy, []), args))
   7.400 -(*  |>> hide_bound_names (map (#1 o #1) args) *)
   7.401 -  |>> Theory.parent_path;
   7.402  
   7.403  fun smart_note_thmss kind NONE = PureThy.note_thmss_i (Drule.kind kind)
   7.404    | smart_note_thmss kind (SOME (loc, _)) = note_thmss_qualified kind loc;
   7.405 @@ -1444,6 +1663,8 @@
   7.406  
   7.407  local
   7.408  
   7.409 +(* add facts to locale in theory *)
   7.410 +
   7.411  fun put_facts loc args thy =
   7.412    let
   7.413      val {predicate, import, elems, params} = the_locale thy loc;
   7.414 @@ -1452,6 +1673,9 @@
   7.415    in thy |> put_locale loc {predicate = predicate, import = import, elems = elems @ [(note, stamp ())],
   7.416      params = params} end;
   7.417  
   7.418 +(* add theorem to locale and theory,
   7.419 +   base for theorems (in loc) and declare (in loc) *)
   7.420 +
   7.421  fun gen_note_thmss prep_locale get_thms kind raw_loc raw_args thy =
   7.422    let
   7.423      val thy_ctxt = ProofContext.init thy;
   7.424 @@ -1470,6 +1694,7 @@
   7.425    in
   7.426      thy
   7.427      |> put_facts loc args
   7.428 +    |> note_thmss_registrations kind loc args
   7.429      |> note_thmss_qualified kind loc args'
   7.430    end;
   7.431  
   7.432 @@ -1483,13 +1708,14 @@
   7.433  
   7.434  (* CB: only used in Proof.finish_global. *)
   7.435  
   7.436 -fun add_thmss loc args (thy, ctxt) =
   7.437 +fun add_thmss kind loc args (thy, ctxt) =
   7.438    let
   7.439      val args' = map (fn ((a, ths), atts) => ((a, atts), [(ths, [])])) args;
   7.440      val thy' = put_facts loc args' thy;
   7.441 +    val thy'' = note_thmss_registrations kind loc args' thy';
   7.442      val (ctxt', (_, facts')) =
   7.443        activate_facts (K I) (ctxt, [((("", []), []), [Notes args'])]);
   7.444 -  in ((thy', ctxt'), facts') end;
   7.445 +  in ((thy'', ctxt'), facts') end;
   7.446  
   7.447  end;
   7.448  
   7.449 @@ -1688,112 +1914,6 @@
   7.450  
   7.451  (** instantiate free vars **)
   7.452  
   7.453 -(* instantiate TFrees *)
   7.454 -
   7.455 -fun tinst_type tinst T = if Symtab.is_empty tinst
   7.456 -      then T
   7.457 -      else Term.map_type_tfree
   7.458 -        (fn (v as (x, _)) => getOpt (Symtab.lookup (tinst, x), (TFree v))) T;
   7.459 -
   7.460 -fun tinst_term tinst t = if Symtab.is_empty tinst
   7.461 -      then t
   7.462 -      else Term.map_term_types (tinst_type tinst) t;
   7.463 -
   7.464 -fun tinst_thm sg tinst thm = if Symtab.is_empty tinst
   7.465 -      then thm
   7.466 -      else let
   7.467 -          val cert = Thm.cterm_of sg;
   7.468 -          val certT = Thm.ctyp_of sg;
   7.469 -          val {hyps, prop, ...} = Thm.rep_thm thm;
   7.470 -          val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
   7.471 -          val tinst' = Symtab.dest tinst |>
   7.472 -                List.filter (fn (a, _) => a mem_string tfrees);
   7.473 -        in
   7.474 -          if null tinst' then thm
   7.475 -          else thm |> Drule.implies_intr_list (map cert hyps)
   7.476 -            |> Drule.tvars_intr_list (map #1 tinst')
   7.477 -            |> (fn (th, al) => th |> Thm.instantiate
   7.478 -                ((map (fn (a, T) => (valOf (assoc (al, a)), certT T)) tinst'),
   7.479 -                  []))
   7.480 -            |> (fn th => Drule.implies_elim_list th
   7.481 -                 (map (Thm.assume o cert o tinst_term tinst) hyps))
   7.482 -        end;
   7.483 -
   7.484 -fun tinst_elem _ tinst (Fixes fixes) =
   7.485 -      Fixes (map (fn (x, T, mx) => (x, Option.map (tinst_type tinst) T, mx)) fixes)
   7.486 -  | tinst_elem _ tinst (Assumes asms) =
   7.487 -      Assumes (map (apsnd (map (fn (t, (ps, qs)) =>
   7.488 -        (tinst_term tinst t,
   7.489 -          (map (tinst_term tinst) ps, map (tinst_term tinst) qs))))) asms)
   7.490 -  | tinst_elem _ tinst (Defines defs) =
   7.491 -      Defines (map (apsnd (fn (t, ps) =>
   7.492 -        (tinst_term tinst t, map (tinst_term tinst) ps))) defs)
   7.493 -  | tinst_elem sg tinst (Notes facts) =
   7.494 -      Notes (map (apsnd (map (apfst (map (tinst_thm sg tinst))))) facts);
   7.495 -
   7.496 -(* instantiate TFrees and Frees *)
   7.497 -
   7.498 -fun inst_term (inst, tinst) = if Symtab.is_empty inst
   7.499 -      then tinst_term tinst
   7.500 -      else (* instantiate terms and types simultaneously *)
   7.501 -        let
   7.502 -          fun instf (Const (x, T)) = Const (x, tinst_type tinst T)
   7.503 -            | instf (Free (x, T)) = (case Symtab.lookup (inst, x) of
   7.504 -                 NONE => Free (x, tinst_type tinst T)
   7.505 -               | SOME t => t)
   7.506 -            | instf (Var (xi, T)) = Var (xi, tinst_type tinst T)
   7.507 -            | instf (b as Bound _) = b
   7.508 -            | instf (Abs (x, T, t)) = Abs (x, tinst_type tinst T, instf t)
   7.509 -            | instf (s $ t) = instf s $ instf t
   7.510 -        in instf end;
   7.511 -
   7.512 -fun inst_thm sg (inst, tinst) thm = if Symtab.is_empty inst
   7.513 -      then tinst_thm sg tinst thm
   7.514 -      else let
   7.515 -          val cert = Thm.cterm_of sg;
   7.516 -          val certT = Thm.ctyp_of sg;
   7.517 -          val {hyps, prop, ...} = Thm.rep_thm thm;
   7.518 -          (* type instantiations *)
   7.519 -          val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
   7.520 -          val tinst' = Symtab.dest tinst |>
   7.521 -                List.filter (fn (a, _) => a mem_string tfrees);
   7.522 -          (* term instantiations;
   7.523 -             note: lhss are type instantiated, because
   7.524 -                   type insts will be done first*)
   7.525 -          val frees = foldr Term.add_term_frees [] (prop :: hyps);
   7.526 -          val inst' = Symtab.dest inst |>
   7.527 -                List.mapPartial (fn (a, t) =>
   7.528 -                  get_first (fn (Free (x, T)) => 
   7.529 -                    if a = x then SOME (Free (x, tinst_type tinst T), t)
   7.530 -                    else NONE) frees);
   7.531 -        in
   7.532 -          if null tinst' andalso null inst' then tinst_thm sg tinst thm
   7.533 -          else thm |> Drule.implies_intr_list (map cert hyps)
   7.534 -            |> Drule.tvars_intr_list (map #1 tinst')
   7.535 -            |> (fn (th, al) => th |> Thm.instantiate
   7.536 -                ((map (fn (a, T) => (valOf (assoc (al, a)), certT T)) tinst'),
   7.537 -                  []))
   7.538 -            |> Drule.forall_intr_list (map (cert o #1) inst')
   7.539 -            |> Drule.forall_elim_list (map (cert o #2) inst') 
   7.540 -            |> (fn th => Drule.implies_elim_list th
   7.541 -                 (map (Thm.assume o cert o inst_term (inst, tinst)) hyps))
   7.542 -        end;
   7.543 -
   7.544 -fun inst_elem _ (_, tinst) (Fixes fixes) =
   7.545 -      Fixes (map (fn (x, T, mx) => (x, Option.map (tinst_type tinst) T, mx)) fixes)
   7.546 -  | inst_elem _ inst (Assumes asms) =
   7.547 -      Assumes (map (apsnd (map (fn (t, (ps, qs)) =>
   7.548 -        (inst_term inst t,
   7.549 -          (map (inst_term inst) ps, map (inst_term inst) qs))))) asms)
   7.550 -  | inst_elem _ inst (Defines defs) =
   7.551 -      Defines (map (apsnd (fn (t, ps) =>
   7.552 -        (inst_term inst t, map (inst_term inst) ps))) defs)
   7.553 -  | inst_elem sg inst (Notes facts) =
   7.554 -      Notes (map (apsnd (map (apfst (map (inst_thm sg inst))))) facts);
   7.555 -
   7.556 -fun inst_elems sign inst ((n, ps), elems) =
   7.557 -      ((n, map (inst_term inst) ps), map (inst_elem sign inst) elems);
   7.558 -
   7.559  (* extract proof obligations (assms and defs) from elements *)
   7.560  
   7.561  (* check if defining equation has become t == t, these are dropped
   7.562 @@ -1829,9 +1949,9 @@
   7.563        let
   7.564          (* extract theory or context attributes *)
   7.565          val (Notes facts) = map_attrib_element_i which (Notes facts);
   7.566 -        (* add attributs from registration *)
   7.567 +        (* add attributes from registration *)
   7.568          val facts' = map (apfst (apsnd (fn a => a @ atts))) facts;
   7.569 -        (* discharge hyps and varify *)
   7.570 +        (* discharge hyps  *)
   7.571          val facts'' = map (apsnd (map (apfst (map disch)))) facts';
   7.572          (* prefix names *)
   7.573          val facts''' = map (apfst (apfst (fn name =>
   7.574 @@ -1862,55 +1982,36 @@
   7.575        in Library.foldl (activate_facts_elems get_reg note_thmss which
   7.576          (standard o Drule.satisfy_hyps prems)) (thy_ctxt, new_elemss) end;
   7.577  
   7.578 -fun loc_accesses prfx name =
   7.579 -  (* full qualified name is T.p.r.n where
   7.580 -       T: theory name, p: interpretation prefix, r: renaming prefix, n: name
   7.581 -  *)
   7.582 -     if prfx = "" then
   7.583 -       case NameSpace.unpack name of
   7.584 -	   [] => [""]
   7.585 -	 | [T, n] => map NameSpace.pack [[T, n], [n]]
   7.586 -	 | [T, r, n] => map NameSpace.pack [[T, r, n], (*[T, n],*) [r, n], [n]]
   7.587 -	 | _ => error ("Locale accesses: illegal name " ^ quote name)
   7.588 -     else case NameSpace.unpack name of
   7.589 -           [] => [""]
   7.590 -         | [T, p, n] => map NameSpace.pack [[T, p, n], [p, n]]
   7.591 -         | [T, p, r, n] => map NameSpace.pack
   7.592 -             [[T, p, r, n], [T, p, n], [p, r, n], [p, n]]
   7.593 -         | _ => error ("Locale accesses: illegal name " ^ quote name);
   7.594 -
   7.595  val global_activate_facts_elemss = gen_activate_facts_elemss
   7.596 -      get_global_registration
   7.597 -      (fn prfx => PureThy.note_thmss_qualified_i (loc_accesses prfx)
   7.598 +      (fn thy => fn (name, ps) =>
   7.599 +        get_global_registration thy (name, map Logic.varify ps))
   7.600 +      (fn prfx => PureThy.note_thmss_accesses_i (global_accesses prfx)
   7.601          (Drule.kind ""))
   7.602        fst Drule.standard;
   7.603  val local_activate_facts_elemss = gen_activate_facts_elemss
   7.604 -      get_local_registration (fn prfx => fn _ => fn ctxt => (ctxt, ctxt)) snd I;
   7.605 -(*
   7.606 -val local_activate_facts_elemss = gen_activate_facts_elemss
   7.607 -      get_local_registration (fn prfx => ProofContext.note_thmss_i) snd I;
   7.608 -*)
   7.609 +      get_local_registration
   7.610 +      (fn prfx => ProofContext.note_thmss_accesses_i (local_accesses prfx))
   7.611 +      snd I;
   7.612  
   7.613 -fun gen_prep_registration mk_ctxt read_terms test_reg put_reg activate
   7.614 +fun gen_prep_registration mk_ctxt is_local read_terms test_reg put_reg activate
   7.615      attn expr insts thy_ctxt =
   7.616    let
   7.617      val ctxt = mk_ctxt thy_ctxt;
   7.618      val sign = ProofContext.sign_of ctxt;
   7.619  
   7.620 -    val (ids, raw_elemss) =
   7.621 -          flatten (ctxt, intern_expr sign) ([], Expr expr);
   7.622 +    val ctxt' = ctxt |> ProofContext.theory_of |> ProofContext.init;
   7.623 +    val (ids, raw_elemss) = flatten (ctxt', intern_expr sign) ([], Expr expr);
   7.624      val do_close = false;  (* effect unknown *)
   7.625      val ((parms, all_elemss, _), (spec, (xs, defs, _))) =
   7.626 -          read_elemss do_close ctxt [] raw_elemss [];
   7.627 +          read_elemss do_close ctxt' [] raw_elemss [];
   7.628  
   7.629  
   7.630      (** compute instantiation **)
   7.631  
   7.632 -    (* check user input *)
   7.633 +    (* user input *)
   7.634      val insts = if length parms < length insts
   7.635           then error "More arguments than parameters in instantiation."
   7.636           else insts @ replicate (length parms - length insts) NONE;
   7.637 -
   7.638      val (ps, pTs) = split_list parms;
   7.639      val pvTs = map Type.varifyT pTs;
   7.640  
   7.641 @@ -1922,17 +2023,26 @@
   7.642      val used = foldr Term.add_typ_varnames [] pvTs;
   7.643      fun sorts (a, i) = assoc (tvars, (a, i));
   7.644      val (vs, vinst) = read_terms thy_ctxt sorts used given_insts;
   7.645 +    val vars = foldl Term.add_term_tvar_ixns [] vs \\ map fst tvars;
   7.646 +    val vars' = Library.foldl Term.add_term_varnames (vars, vs);
   7.647 +    val _ = if null vars' then ()
   7.648 +         else error ("Illegal schematic variable(s) in instantiation: " ^
   7.649 +           commas_quote (map Syntax.string_of_vname vars'));
   7.650      (* replace new types (which are TFrees) by ones with new names *)
   7.651      val new_Tnames = foldr Term.add_term_tfree_names [] vs;
   7.652      val new_Tnames' = Term.invent_names used "'a" (length new_Tnames);
   7.653 -    val renameT = Term.map_type_tfree (fn (a, s) =>
   7.654 -          TFree (valOf (assoc (new_Tnames ~~ new_Tnames', a)), s));
   7.655 -    val rename = Term.map_term_types renameT;
   7.656 +    val renameT =
   7.657 +          if is_local then I
   7.658 +          else Type.unvarifyT o Term.map_type_tfree (fn (a, s) =>
   7.659 +            TFree (valOf (assoc (new_Tnames ~~ new_Tnames', a)), s));
   7.660 +    val rename =
   7.661 +          if is_local then I
   7.662 +          else Term.map_term_types renameT;
   7.663  
   7.664      val tinst = Symtab.make (map
   7.665 -                (fn ((x, 0), T) => (x, T |> renameT |> Type.unvarifyT)
   7.666 -                  | ((_, n), _) => error "Var in prep_registration") vinst);
   7.667 -    val inst = Symtab.make (given_ps ~~ map (Logic.unvarify o rename) vs);
   7.668 +                (fn ((x, 0), T) => (x, T |> renameT)
   7.669 +                  | ((_, n), _) => error "Internal error var in prep_registration") vinst);
   7.670 +    val inst = Symtab.make (given_ps ~~ map rename vs);
   7.671  
   7.672      (* defined params without user input *)
   7.673      val not_given = List.mapPartial (fn (x, (NONE, T)) => SOME (x, T)
   7.674 @@ -1942,10 +2052,10 @@
   7.675          val (t, T) = case find_first (fn (Free (a, _), _) => a = p) defs of
   7.676                 NONE => error ("Instance missing for parameter " ^ quote p)
   7.677               | SOME (Free (_, T), t) => (t, T);
   7.678 -        val d = t |> inst_term (inst, tinst) |> Envir.beta_norm;
   7.679 +        val d = t |> inst_tab_term (inst, tinst) |> Envir.beta_norm;
   7.680        in (Symtab.update_new ((p, d), inst), tinst) end;
   7.681      val (inst, tinst) = Library.foldl add_def ((inst, tinst), not_given);
   7.682 -  
   7.683 +    (* Note: inst and tinst contain no vars. *)
   7.684  
   7.685      (** compute proof obligations **)
   7.686  
   7.687 @@ -1955,7 +2065,7 @@
   7.688  
   7.689      (* instantiate ids and elements *)
   7.690      val inst_elemss = map
   7.691 -          (fn (id, (_, elems)) => inst_elems sign (inst, tinst) (id, 
   7.692 +          (fn (id, (_, elems)) => inst_tab_elems sign (inst, tinst) (id, 
   7.693              map (fn Int e => e) elems)) 
   7.694            (ids' ~~ all_elemss);
   7.695  
   7.696 @@ -1966,8 +2076,11 @@
   7.697      val propss = extract_asms_elemss new_inst_elemss;
   7.698  
   7.699  
   7.700 -    (** add registrations to theory,
   7.701 +    (** add registrations to theory or context,
   7.702          without theorems, these are added after the proof **)
   7.703 +    (* TODO: this is potentially problematic, since a proof of the
   7.704 +       interpretation might contain a reference to the incomplete
   7.705 +       registration. *)
   7.706  
   7.707      val thy_ctxt' = Library.foldl (fn (thy_ctxt, (id, _)) =>
   7.708            put_reg id attn thy_ctxt) (thy_ctxt, new_inst_elemss);
   7.709 @@ -1977,15 +2090,16 @@
   7.710  in
   7.711  
   7.712  val prep_global_registration = gen_prep_registration
   7.713 -     ProofContext.init
   7.714 +     ProofContext.init false
   7.715       (fn thy => fn sorts => fn used =>
   7.716         Sign.read_def_terms (Theory.sign_of thy, K NONE, sorts) used true)
   7.717 -     test_global_registration
   7.718 -     put_global_registration
   7.719 +     (fn thy => fn (name, ps) =>
   7.720 +       test_global_registration thy (name, map Logic.varify ps))
   7.721 +     (fn (name, ps) => put_global_registration (name, map Logic.varify ps))
   7.722       global_activate_facts_elemss;
   7.723  
   7.724  val prep_local_registration = gen_prep_registration
   7.725 -     I
   7.726 +     I true
   7.727       (fn ctxt => ProofContext.read_termTs ctxt (K false) (K NONE))
   7.728       smart_test_registration
   7.729       put_local_registration
     8.1 --- a/src/Pure/Isar/proof.ML	Mon Apr 11 12:18:27 2005 +0200
     8.2 +++ b/src/Pure/Isar/proof.ML	Mon Apr 11 12:34:34 2005 +0200
     8.3 @@ -90,13 +90,17 @@
     8.4    val def: string -> context attribute list -> string *  (string * string list) -> state -> state
     8.5    val def_i: string -> context attribute list -> string * (term * term list) -> state -> state
     8.6    val invoke_case: string * string option list * context attribute list -> state -> state
     8.7 -  val multi_theorem: string -> (theory -> theory)
     8.8 -    -> (xstring * (Locale.multi_attribute list * Locale.multi_attribute list list)) option
     8.9 +  val multi_theorem:
    8.10 +    string -> (theory -> theory) ->
    8.11 +    (cterm list -> context -> context -> thm -> thm) ->
    8.12 +    (xstring * (Locale.multi_attribute list * Locale.multi_attribute list list)) option
    8.13      -> bstring * theory attribute list -> Locale.multi_attribute Locale.element Locale.elem_expr list
    8.14      -> ((bstring * theory attribute list) * (string * (string list * string list)) list) list
    8.15      -> theory -> state
    8.16 -  val multi_theorem_i: string -> (theory -> theory)
    8.17 -    -> (string * (Locale.multi_attribute list * Locale.multi_attribute list list)) option
    8.18 +  val multi_theorem_i:
    8.19 +    string -> (theory -> theory)  ->
    8.20 +    (cterm list -> context -> context -> thm -> thm) ->
    8.21 +    (string * (Locale.multi_attribute list * Locale.multi_attribute list list)) option
    8.22      -> bstring * theory attribute list
    8.23      -> Locale.multi_attribute Locale.element_i Locale.elem_expr list
    8.24      -> ((bstring * theory attribute list) * (term * (term list * term list)) list) list
    8.25 @@ -162,10 +166,12 @@
    8.26      theory_spec: (bstring * theory attribute list) * theory attribute list list,
    8.27      locale_spec: (string * (Locale.multi_attribute list * Locale.multi_attribute list list)) option,
    8.28      view: cterm list * cterm list, (* target view and includes view *)
    8.29 -    thy_mod: theory -> theory} |   (* used in finish_global to modify final
    8.30 +    thy_mod: theory -> theory,     (* used in finish_global to modify final
    8.31                                        theory, normally set to I; used by
    8.32                                        registration command to activate
    8.33                                        registrations *)
    8.34 +    export: cterm list -> context -> context -> thm -> thm } |
    8.35 +                                   (* exporter to be used in finish_global *)
    8.36    Show of context attribute list list |
    8.37    Have of context attribute list list |
    8.38    Interpret of {attss: context attribute list list,
    8.39 @@ -796,7 +802,7 @@
    8.40    end;
    8.41  
    8.42  (*global goals*)
    8.43 -fun global_goal prep kind thy_mod raw_locale a elems concl thy =
    8.44 +fun global_goal prep kind thy_mod export raw_locale a elems concl thy =
    8.45    let
    8.46      val init = init_state thy;
    8.47      val (opt_name, view, locale_ctxt, elems_ctxt, propp) =
    8.48 @@ -814,7 +820,8 @@
    8.49          theory_spec = (a, map (snd o fst) concl),
    8.50          locale_spec = (case raw_locale of NONE => NONE | SOME (_, x) => SOME (valOf opt_name, x)),
    8.51          view = view,
    8.52 -        thy_mod = thy_mod})
    8.53 +        thy_mod = thy_mod,
    8.54 +        export = export})
    8.55        Seq.single true (map (fst o fst) concl) propp
    8.56    end;
    8.57  
    8.58 @@ -927,27 +934,28 @@
    8.59      val (goal_ctxt, (((kind, names, tss), (_, raw_thm)), _)) = current_goal state;
    8.60      val locale_ctxt = context_of (state |> close_block);
    8.61      val theory_ctxt = context_of (state |> close_block |> close_block);
    8.62 -    val {kind = k, theory_spec = ((name, atts), attss), locale_spec, view = (target_view, elems_view), thy_mod} =
    8.63 +    val {kind = k, theory_spec = ((name, atts), attss), locale_spec, view = (target_view, elems_view), thy_mod, export} =
    8.64        (case kind of Theorem x => x | _ => err_malformed "finish_global" state);
    8.65  
    8.66      val ts = List.concat tss;
    8.67 -    val locale_results = map (ProofContext.export_standard elems_view goal_ctxt locale_ctxt)
    8.68 +    val locale_results = map (export elems_view goal_ctxt locale_ctxt)
    8.69        (prep_result state ts raw_thm);
    8.70  
    8.71      val results = map (Drule.strip_shyps_warning o
    8.72 -      ProofContext.export_standard target_view locale_ctxt theory_ctxt) locale_results;
    8.73 +      export target_view locale_ctxt theory_ctxt) locale_results;
    8.74  
    8.75      val (theory', results') =
    8.76        theory_of state
    8.77 -      |> (case locale_spec of NONE => I | SOME (loc, (loc_atts, loc_attss)) => fn thy =>
    8.78 +      |> (case locale_spec of NONE => I
    8.79 +                            | SOME (loc, (loc_atts, loc_attss)) => fn thy =>
    8.80          if length names <> length loc_attss then
    8.81            raise THEORY ("Bad number of locale attributes", [thy])
    8.82          else (thy, locale_ctxt)
    8.83 -          |> Locale.add_thmss loc ((names ~~ Library.unflat tss locale_results) ~~ loc_attss)
    8.84 +          |> Locale.add_thmss k loc ((names ~~ Library.unflat tss locale_results) ~~ loc_attss)
    8.85            |> (fn ((thy', ctxt'), res) =>
    8.86              if name = "" andalso null loc_atts then thy'
    8.87              else (thy', ctxt')
    8.88 -              |> (#1 o #1 o Locale.add_thmss loc [((name, List.concat (map #2 res)), loc_atts)])))
    8.89 +              |> (#1 o #1 o Locale.add_thmss k loc [((name, List.concat (map #2 res)), loc_atts)])))
    8.90        |> Locale.smart_note_thmss k locale_spec
    8.91          ((names ~~ attss) ~~ map (single o Thm.no_attributes) (Library.unflat tss results))
    8.92        |> (fn (thy, res) => (thy, res)
     9.1 --- a/src/Pure/Isar/proof_context.ML	Mon Apr 11 12:18:27 2005 +0200
     9.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Apr 11 12:34:34 2005 +0200
     9.3 @@ -67,6 +67,7 @@
     9.4    val find_free: term -> string -> term option
     9.5    val export: bool -> context -> context -> thm -> thm Seq.seq
     9.6    val export_standard: cterm list -> context -> context -> thm -> thm
     9.7 +  val export_plain: cterm list -> context -> context -> thm -> thm
     9.8    val drop_schematic: indexname * term option -> indexname * term option
     9.9    val add_binds: (indexname * string option) list -> context -> context
    9.10    val add_binds_i: (indexname * term option) list -> context -> context
    9.11 @@ -103,11 +104,23 @@
    9.12    val put_thmss: (string * thm list) list -> context -> context
    9.13    val reset_thms: string -> context -> context
    9.14    val note_thmss:
    9.15 -    ((bstring * context attribute list) * (thmref * context attribute list) list) list ->
    9.16 -      context -> context * (bstring * thm list) list
    9.17 +    ((bstring * context attribute list) *
    9.18 +      (thmref * context attribute list) list) list ->
    9.19 +    context -> context * (bstring * thm list) list
    9.20    val note_thmss_i:
    9.21 -    ((bstring * context attribute list) * (thm list * context attribute list) list) list ->
    9.22 -      context -> context * (bstring * thm list) list
    9.23 +    ((bstring * context attribute list) *
    9.24 +      (thm list * context attribute list) list) list ->
    9.25 +    context -> context * (bstring * thm list) list
    9.26 +  val note_thmss_accesses:
    9.27 +    (string -> string list) ->
    9.28 +    ((bstring * context attribute list) *
    9.29 +      (thmref * context attribute list) list) list ->
    9.30 +    context -> context * (bstring * thm list) list
    9.31 +  val note_thmss_accesses_i:
    9.32 +    (string -> string list) ->
    9.33 +    ((bstring * context attribute list) *
    9.34 +      (thm list * context attribute list) list) list ->
    9.35 +    context -> context * (bstring * thm list) list
    9.36    val export_assume: exporter
    9.37    val export_presume: exporter
    9.38    val cert_def: context -> term -> string * term
    9.39 @@ -812,16 +825,31 @@
    9.40        end)
    9.41    end;
    9.42  
    9.43 +(* without varification *)
    9.44 +
    9.45 +fun export_view' view is_goal inner outer =
    9.46 +  let
    9.47 +    val asms = Library.drop (length (assumptions_of outer), assumptions_of inner);
    9.48 +    val exp_asms = map (fn (cprops, exp) => exp is_goal cprops) asms;
    9.49 +  in fn thm =>thm
    9.50 +    |> Tactic.norm_hhf_plain
    9.51 +    |> Seq.EVERY (rev exp_asms)
    9.52 +    |> Seq.map (Drule.implies_intr_list view)
    9.53 +    |> Seq.map Tactic.norm_hhf_plain
    9.54 +  end;
    9.55 +
    9.56  val export = export_view [];
    9.57  
    9.58 -fun export_standard view inner outer =
    9.59 -  let val exp = export_view view false inner outer in
    9.60 +fun gen_export_std exp_view view inner outer =
    9.61 +  let val exp = exp_view view false inner outer in
    9.62      fn th =>
    9.63        (case Seq.pull (exp th) of
    9.64          SOME (th', _) => th' |> Drule.local_standard
    9.65        | NONE => raise CONTEXT ("Internal failure while exporting theorem", inner))
    9.66    end;
    9.67  
    9.68 +val export_standard = gen_export_std export_view;
    9.69 +val export_plain = gen_export_std export_view';
    9.70  
    9.71  
    9.72  (** bindings **)
    9.73 @@ -1022,20 +1050,24 @@
    9.74  
    9.75  (* put_thm(s) *)
    9.76  
    9.77 -fun put_thms ("", _) ctxt = ctxt
    9.78 -  | put_thms (name, ths) ctxt = ctxt |> map_context
    9.79 +fun gen_put_thms _ _ ("", _) ctxt = ctxt
    9.80 +  | gen_put_thms override_q acc (name, ths) ctxt = ctxt |> map_context
    9.81        (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs, delta, delta_count) =>
    9.82 -        if not q andalso NameSpace.is_qualified name then
    9.83 +        if not override_q andalso not q andalso NameSpace.is_qualified name then
    9.84            raise CONTEXT ("Attempt to declare qualified name " ^ quote name, ctxt)
    9.85 -        else (thy, syntax, data, asms, binds, (q, NameSpace.extend (space, [name]),
    9.86 +        else (thy, syntax, data, asms, binds, (q, NameSpace.extend' acc (space, [name]),
    9.87            Symtab.update ((name, SOME ths), tab),
    9.88              FactIndex.add (is_known ctxt) (index, (name, ths))), cases, defs, delta, delta_count));
    9.89  
    9.90 -fun put_thm (name, th) = put_thms (name, [th]);
    9.91 +fun gen_put_thm q acc (name, th) = gen_put_thms q acc (name, [th]);
    9.92  
    9.93 -fun put_thmss [] ctxt = ctxt
    9.94 -  | put_thmss (th :: ths) ctxt = ctxt |> put_thms th |> put_thmss ths;
    9.95 +fun gen_put_thmss q acc [] ctxt = ctxt
    9.96 +  | gen_put_thmss q acc (th :: ths) ctxt =
    9.97 +      ctxt |> gen_put_thms q acc th |> gen_put_thmss q acc ths;
    9.98  
    9.99 +val put_thm = gen_put_thm false NameSpace.accesses;
   9.100 +val put_thms = gen_put_thms false NameSpace.accesses;
   9.101 +val put_thmss = gen_put_thmss false NameSpace.accesses;
   9.102  
   9.103  (* reset_thms *)
   9.104  
   9.105 @@ -1049,21 +1081,25 @@
   9.106  
   9.107  local
   9.108  
   9.109 -fun gen_note_thss get (ctxt, ((name, more_attrs), ths_attrs)) =
   9.110 +fun gen_note_thss get acc (ctxt, ((name, more_attrs), ths_attrs)) =
   9.111    let
   9.112      fun app ((ct, ths), (th, attrs)) =
   9.113        let val (ct', th') = Thm.applys_attributes ((ct, get ctxt th), attrs @ more_attrs)
   9.114        in (ct', th' :: ths) end;
   9.115      val (ctxt', rev_thms) = Library.foldl app ((ctxt, []), ths_attrs);
   9.116      val thms = List.concat (rev rev_thms);
   9.117 -  in (ctxt' |> put_thms (name, thms), (name, thms)) end;
   9.118 +  in (ctxt' |> gen_put_thms true acc (name, thms), (name, thms)) end;
   9.119  
   9.120 -fun gen_note_thmss get args ctxt = foldl_map (gen_note_thss get) (ctxt, args);
   9.121 +fun gen_note_thmss get acc args ctxt =
   9.122 +  foldl_map (gen_note_thss get acc) (ctxt, args);
   9.123  
   9.124  in
   9.125  
   9.126 -val note_thmss = gen_note_thmss get_thms;
   9.127 -val note_thmss_i = gen_note_thmss (K I);
   9.128 +val note_thmss = gen_note_thmss get_thms NameSpace.accesses;
   9.129 +val note_thmss_i = gen_note_thmss (K I) NameSpace.accesses;
   9.130 +
   9.131 +val note_thmss_accesses = gen_note_thmss get_thms;
   9.132 +val note_thmss_accesses_i = gen_note_thmss (K I);
   9.133  
   9.134  end;
   9.135  
    10.1 --- a/src/Pure/axclass.ML	Mon Apr 11 12:18:27 2005 +0200
    10.2 +++ b/src/Pure/axclass.ML	Mon Apr 11 12:34:34 2005 +0200
    10.3 @@ -407,7 +407,7 @@
    10.4  
    10.5  fun inst_proof mk_prop add_thms inst int theory =
    10.6    theory
    10.7 -  |> IsarThy.multi_theorem_i Drule.internalK I
    10.8 +  |> IsarThy.multi_theorem_i Drule.internalK I ProofContext.export_standard
    10.9      ("", [fn (thy, th) => (add_thms [th] thy, th)]) []
   10.10      (map (fn t => (("", []), [(t, ([], []))])) (mk_prop (Theory.sign_of theory) inst)) int;
   10.11  
    11.1 --- a/src/Pure/library.ML	Mon Apr 11 12:18:27 2005 +0200
    11.2 +++ b/src/Pure/library.ML	Mon Apr 11 12:34:34 2005 +0200
    11.3 @@ -128,6 +128,7 @@
    11.4    val radixstring: int * string * int -> string
    11.5    val string_of_int: int -> string
    11.6    val string_of_indexname: string * int -> string
    11.7 +    (* CB: note alternative Syntax.string_of_vname has nicer syntax *)
    11.8    val read_radixint: int * string list -> int * string list
    11.9    val read_int: string list -> int * string list
   11.10    val oct_char: string -> string
    12.1 --- a/src/Pure/pure_thy.ML	Mon Apr 11 12:18:27 2005 +0200
    12.2 +++ b/src/Pure/pure_thy.ML	Mon Apr 11 12:34:34 2005 +0200
    12.3 @@ -53,12 +53,12 @@
    12.4      theory attribute -> ((bstring * theory attribute list) *
    12.5      (thm list * theory attribute list) list) list -> theory ->
    12.6      theory * (bstring * thm list) list
    12.7 -  val note_thmss_qualified:
    12.8 +  val note_thmss_accesses:
    12.9      (string -> string list) ->
   12.10      theory attribute -> ((bstring * theory attribute list) *
   12.11      (thmref * theory attribute list) list) list -> theory ->
   12.12      theory * (bstring * thm list) list
   12.13 -  val note_thmss_qualified_i:
   12.14 +  val note_thmss_accesses_i:
   12.15      (string -> string list) ->
   12.16      theory attribute -> ((bstring * theory attribute list) *
   12.17      (thm list * theory attribute list) list) list -> theory ->
   12.18 @@ -387,9 +387,9 @@
   12.19  (* always permit qualified names,
   12.20     clients may specify non-standard access policy *)
   12.21  
   12.22 -fun note_thmss_qualified acc =
   12.23 +fun note_thmss_accesses acc =
   12.24    gen_note_thmss (gen_enter_thms Sign.full_name' acc) get_thms;
   12.25 -fun note_thmss_qualified_i acc =
   12.26 +fun note_thmss_accesses_i acc =
   12.27    gen_note_thmss (gen_enter_thms Sign.full_name' acc) (K I);
   12.28  
   12.29  end;
    13.1 --- a/src/Pure/tactic.ML	Mon Apr 11 12:18:27 2005 +0200
    13.2 +++ b/src/Pure/tactic.ML	Mon Apr 11 12:34:34 2005 +0200
    13.3 @@ -70,6 +70,7 @@
    13.4    val net_biresolve_tac : (bool*thm) list -> int -> tactic
    13.5    val net_match_tac     : thm list -> int -> tactic
    13.6    val net_resolve_tac   : thm list -> int -> tactic
    13.7 +  val norm_hhf_plain    : thm -> thm
    13.8    val norm_hhf_rule     : thm -> thm
    13.9    val norm_hhf_tac      : int -> tactic
   13.10    val prune_params_tac  : tactic
   13.11 @@ -532,9 +533,12 @@
   13.12  fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
   13.13  fun rewtac def = rewrite_goals_tac [def];
   13.14  
   13.15 +fun norm_hhf_plain th =
   13.16 +  if Drule.is_norm_hhf (prop_of th) then th
   13.17 +  else rewrite_rule [Drule.norm_hhf_eq] th;
   13.18 +
   13.19  fun norm_hhf_rule th =
   13.20 - (if Drule.is_norm_hhf (prop_of th) then th
   13.21 -  else rewrite_rule [Drule.norm_hhf_eq] th) |> Drule.gen_all;
   13.22 +  th |> norm_hhf_plain |> Drule.gen_all;
   13.23  
   13.24  val norm_hhf_tac =
   13.25    rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
    14.1 --- a/src/ZF/Constructible/L_axioms.thy	Mon Apr 11 12:18:27 2005 +0200
    14.2 +++ b/src/ZF/Constructible/L_axioms.thy	Mon Apr 11 12:34:34 2005 +0200
    14.3 @@ -100,6 +100,10 @@
    14.4    apply (rule L_nat)
    14.5    done
    14.6  
    14.7 +interpretation M_trivial ["L"] by (rule M_trivial_L)
    14.8 +
    14.9 +(* Replaces the following code.
   14.10 +
   14.11  lemmas rall_abs = M_trivial.rall_abs [OF M_trivial_L]
   14.12    and rex_abs = M_trivial.rex_abs [OF M_trivial_L]
   14.13    and ball_iff_equiv = M_trivial.ball_iff_equiv [OF M_trivial_L]
   14.14 @@ -182,7 +186,7 @@
   14.15  declare number1_abs [simp]
   14.16  declare number2_abs [simp]
   14.17  declare number3_abs [simp]
   14.18 -
   14.19 +*)
   14.20  
   14.21  subsection{*Instantiation of the locale @{text reflection}*}
   14.22