1.1 --- a/NEWS Sun Apr 17 19:40:43 2005 +0200
1.2 +++ b/NEWS Mon Apr 18 09:25:23 2005 +0200
1.3 @@ -163,6 +163,7 @@
1.4 do not occur in proof obligations, neither are instantiated theorems stored
1.5 in duplicate.
1.6 Use print_interps to inspect active interpretations of a particular locale.
1.7 + For details, see the Isar Reference manual.
1.8
1.9 * Locales: proper static binding of attribute syntax -- i.e. types /
1.10 terms / facts mentioned as arguments are always those of the locale
2.1 --- a/doc-src/IsarRef/generic.tex Sun Apr 17 19:40:43 2005 +0200
2.2 +++ b/doc-src/IsarRef/generic.tex Mon Apr 18 09:25:23 2005 +0200
2.3 @@ -180,7 +180,7 @@
2.4 specifications included here, e.g.\ a local $simp$ rule.
2.5
2.6 \item [$\INCLUDES{c}$] copies the specified context in a statically scoped
2.7 - manner.
2.8 + manner. Only available in the long goal format of \S\ref{sec:goals}.
2.9
2.10 In contrast, the initial $import$ specification of a locale expression
2.11 maintains a dynamic relation to the locales being referenced (benefiting
2.12 @@ -224,6 +224,79 @@
2.13 \end{descr}
2.14
2.15
2.16 +\subsubsection{Interpretation of locales}
2.17 +
2.18 +Locale expressions (more precisely, \emph{context expressions}) may be
2.19 +instantiated, and the instantiated facts added to the current context.
2.20 +This requires a proof of the instantiated specification and is called
2.21 +\emph{locale interpretation}. Interpretation is possible in theories
2.22 +($\isarcmd{interpretation}$) and proof contexts
2.23 +($\isarcmd{interpret}$).
2.24 +
2.25 +\indexisarcmd{interpretation}\indexisarcmd{interpret}
2.26 +\indexisarcmd{print-interps}
2.27 +\begin{matharray}{rcl}
2.28 + \isarcmd{interpretation} & : & \isartrans{theory}{proof(prove)} \\
2.29 + \isarcmd{interpret} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
2.30 + \isarcmd{print_interps}^* & : & \isarkeep{theory~|~proof} \\
2.31 +\end{matharray}
2.32 +
2.33 +\indexouternonterm{interp}
2.34 +
2.35 +\railalias{printinterps}{print\_interps}
2.36 +\railterm{printinterps}
2.37 +
2.38 +\begin{rail}
2.39 + 'interpretation' interp
2.40 + ;
2.41 + 'interpret' interp
2.42 + ;
2.43 + printinterps name
2.44 + ;
2.45 + interp: thmdecl? contextexpr ('[' (inst+) ']')?
2.46 + ;
2.47 +\end{rail}
2.48 +
2.49 +\begin{descr}
2.50 +
2.51 +\item [$\isarcmd{interpretation}~expr~insts$]
2.52 + interprets $expr$ in the theory. The instantiation is positional.
2.53 + All parameters must receive an instantiation term --- with the
2.54 + exception of defined parameters. These are, if omitted, derived
2.55 + from the defining equation and other instantiations. Use ``\_'' to
2.56 + omit an instantiation term. Free variables are automatically
2.57 + generalized.
2.58 +
2.59 + The context expression may be preceded by a name and/or attributes.
2.60 + These take effect in the post-processing of facts. The name is used
2.61 + to prefix fact names, for example to avoid accidental hiding of
2.62 + other facts. Attributes are applied after attributes of the
2.63 + interpreted facts.
2.64 +
2.65 + The command is aware of interpretations already active in the
2.66 + theory. No proof obligations are generated for those, neither is
2.67 + post-processing applied to their facts. This avoids duplication of
2.68 + interpreted facts, in particular. Note that, in the case of a
2.69 + locale with import, parts of the interpretation may already be
2.70 + active. The command will only generate proof obligations and add
2.71 + facts for new parts.
2.72 +
2.73 + Adding facts to locales has the
2.74 + effect of adding interpreted facts to the theory for all active
2.75 + interpretations also.
2.76 +
2.77 +\item [$\isarcmd{interpret}~expr~insts$]
2.78 + interprets $expr$ in the proof context and is otherwise similar to
2.79 + the previous command. Free variables in instantiations are not
2.80 + generalized, however.
2.81 +
2.82 +\item [$\isarcmd{print_interps}~loc$]
2.83 + prints the interpretations of a particular locale $loc$ that are
2.84 + active in the current context, either theory or proof context.
2.85 +
2.86 +\end{descr}
2.87 +
2.88 +
2.89 \section{Derived proof schemes}
2.90
2.91 \subsection{Generalized elimination}\label{sec:obtain}
3.1 --- a/src/FOL/ex/LocaleTest.thy Sun Apr 17 19:40:43 2005 +0200
3.2 +++ b/src/FOL/ex/LocaleTest.thy Mon Apr 18 09:25:23 2005 +0200
3.3 @@ -53,14 +53,12 @@
3.4
3.5
3.6 interpretation p1: C ["X::'b" "Y::'b"] by (auto intro: A.intro C_axioms.intro)
3.7 - (* both X and Y get type 'b since 'b is the internal type of parameter b,
3.8 - not wanted, but put up with for now. *)
3.9
3.10 print_interps A
3.11
3.12 (* possible accesses *)
3.13 thm p1.a.asm_A thm LocaleTest.p1.a.asm_A
3.14 -thm LocaleTest.asm_A thm p1.asm_A
3.15 +thm p1.asm_A thm LocaleTest.p1.asm_A
3.16
3.17
3.18 (* without prefix *)
4.1 --- a/src/HOL/Algebra/CRing.thy Sun Apr 17 19:40:43 2005 +0200
4.2 +++ b/src/HOL/Algebra/CRing.thy Mon Apr 18 09:25:23 2005 +0200
4.3 @@ -574,28 +574,10 @@
4.4
4.5 locale ring_hom_cring = cring R + cring S + var h +
4.6 assumes homh [simp, intro]: "h \<in> ring_hom R S"
4.7 -(*
4.8 notes hom_closed [simp, intro] = ring_hom_closed [OF homh]
4.9 and hom_mult [simp] = ring_hom_mult [OF homh]
4.10 and hom_add [simp] = ring_hom_add [OF homh]
4.11 and hom_one [simp] = ring_hom_one [OF homh]
4.12 -*)
4.13 -
4.14 -lemma (in ring_hom_cring) hom_closed [simp, intro]:
4.15 - "x \<in> carrier R ==> h x \<in> carrier S"
4.16 - by (simp add: ring_hom_closed [OF homh])
4.17 -
4.18 -lemma (in ring_hom_cring) hom_mult [simp]:
4.19 - "[| x \<in> carrier R; y \<in> carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
4.20 - by (simp add: ring_hom_mult [OF homh])
4.21 -
4.22 -lemma (in ring_hom_cring) hom_add [simp]:
4.23 - "[| x \<in> carrier R; y \<in> carrier R |] ==> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
4.24 - by (simp add: ring_hom_add [OF homh])
4.25 -
4.26 -lemma (in ring_hom_cring) hom_one [simp]:
4.27 - "h \<one> = \<one>\<^bsub>S\<^esub>"
4.28 - by (simp add: ring_hom_one [OF homh])
4.29
4.30 lemma (in ring_hom_cring) hom_zero [simp]:
4.31 "h \<zero> = \<zero>\<^bsub>S\<^esub>"
5.1 --- a/src/HOL/Algebra/Group.thy Sun Apr 17 19:40:43 2005 +0200
5.2 +++ b/src/HOL/Algebra/Group.thy Mon Apr 18 09:25:23 2005 +0200
5.3 @@ -470,8 +470,8 @@
5.4 done
5.5
5.6 text{*This alternative proof of the previous result demonstrates interpret.
5.7 - It uses @{text Prod.inv_equality} (available after instantiation) instead of
5.8 - @{text "group.inv_equality [OF DirProd_group]"}. *}
5.9 + It uses @{text Prod.inv_equality} (available after @{text interpret})
5.10 + instead of @{text "group.inv_equality [OF DirProd_group]"}. *}
5.11 lemma
5.12 includes group G + group H
5.13 assumes g: "g \<in> carrier G"
5.14 @@ -542,19 +542,8 @@
5.15 @{term H}, with a homomorphism @{term h} between them*}
5.16 locale group_hom = group G + group H + var h +
5.17 assumes homh: "h \<in> hom G H"
5.18 -(*
5.19 notes hom_mult [simp] = hom_mult [OF homh]
5.20 and hom_closed [simp] = hom_closed [OF homh]
5.21 -CB: late binding problem?
5.22 -*)
5.23 -
5.24 -lemma (in group_hom) hom_mult [simp]:
5.25 - "[| x \<in> carrier G; y \<in> carrier G |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
5.26 - by (simp add: hom_mult [OF homh])
5.27 -
5.28 -lemma (in group_hom) hom_closed [simp]:
5.29 - "x \<in> carrier G ==> h x \<in> carrier H"
5.30 - by (simp add: hom_closed [OF homh])
5.31
5.32 lemma (in group_hom) one_closed [simp]:
5.33 "h \<one> \<in> carrier H"
6.1 --- a/src/HOL/Algebra/UnivPoly.thy Sun Apr 17 19:40:43 2005 +0200
6.2 +++ b/src/HOL/Algebra/UnivPoly.thy Mon Apr 18 09:25:23 2005 +0200
6.3 @@ -1474,7 +1474,6 @@
6.4 by (simp del: monom_mult (* eval.hom_mult eval.hom_pow, delayed inst! *)
6.5 add: monom_mult [THEN sym] monom_pow)
6.6 also
6.7 - (* from ring_hom_cring_P_S [OF S] instantiate eval: ring_hom_cring *)
6.8 from R S eval_monom1 have "... = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n"
6.9 by (simp add: eval_const)
6.10 finally show ?thesis .
6.11 @@ -1487,9 +1486,6 @@
6.12 assume S: "s \<in> carrier S" and R: "r \<in> carrier R" and P: "p \<in> carrier P"
6.13 from ring_hom_cring_P_S [OF S] interpret ring_hom_cring [P S "eval R S h s"]
6.14 by - (rule ring_hom_cring.axioms, assumption)+
6.15 -(*
6.16 - from ring_hom_cring_P_S [OF S] instantiate eval: ring_hom_cring
6.17 -*)
6.18 from S R P show ?thesis
6.19 by (simp add: monom_mult_is_smult [THEN sym] eval_const)
6.20 qed
6.21 @@ -1571,11 +1567,15 @@
6.22 by (fast intro: UP_univ_propI INTEG_cring id_ring_hom)
6.23
6.24 text {*
6.25 - An instantiation mechanism would now import all theorems and lemmas
6.26 + Interpretation allows now to import all theorems and lemmas
6.27 valid in the context of homomorphisms between @{term INTEG} and @{term
6.28 "UP INTEG"} globally.
6.29 *}
6.30
6.31 +interpretation INTEG: UP_univ_prop [INTEG INTEG id]
6.32 + using INTEG_id_eval
6.33 + by - (rule UP_univ_prop.axioms, assumption)+
6.34 +
6.35 lemma INTEG_closed [intro, simp]:
6.36 "z \<in> carrier INTEG"
6.37 by (unfold INTEG_def) simp
6.38 @@ -1589,6 +1589,6 @@
6.39 by (induct n) (simp_all add: INTEG_def nat_pow_def)
6.40
6.41 lemma "eval INTEG INTEG id 10 (monom (UP INTEG) 5 2) = 500"
6.42 - by (simp add: UP_univ_prop.eval_monom [OF INTEG_id_eval])
6.43 + by (simp add: INTEG.eval_monom)
6.44
6.45 end
7.1 --- a/src/Pure/Isar/locale.ML Sun Apr 17 19:40:43 2005 +0200
7.2 +++ b/src/Pure/Isar/locale.ML Mon Apr 18 09:25:23 2005 +0200
7.3 @@ -351,8 +351,12 @@
7.4 in
7.5 (case loc_regs of
7.6 NONE => Pretty.str ("No interpretations in " ^ msg ^ ".")
7.7 - | SOME r => Pretty.big_list ("Interpretations in " ^ msg ^ ":")
7.8 - (map prt_inst (Termlisttab.dest r)))
7.9 + | SOME r => let
7.10 + val r' = Termlisttab.dest r;
7.11 + val r'' = Library.sort_wrt (fn (_, ((prfx, _), _)) => prfx) r';
7.12 + in Pretty.big_list ("Interpretations in " ^ msg ^ ":")
7.13 + (map prt_inst r'')
7.14 + end)
7.15 |> Pretty.writeln
7.16 end;
7.17
7.18 @@ -540,7 +544,6 @@
7.19 fun tinst_tab_elem sg tinst =
7.20 map_values (tinst_tab_type tinst) (tinst_tab_term tinst) (tinst_tab_thm sg tinst);
7.21
7.22 -
7.23 (* instantiate TFrees and Frees *)
7.24
7.25 fun inst_tab_term (inst, tinst) = if Symtab.is_empty inst
7.26 @@ -589,8 +592,8 @@
7.27 (map (Thm.assume o cert o inst_tab_term (inst, tinst)) hyps))
7.28 end;
7.29
7.30 -fun inst_tab_elem sg inst =
7.31 - map_values (tinst_tab_type (#2 inst)) (inst_tab_term inst) (inst_tab_thm sg inst);
7.32 +fun inst_tab_elem sg (inst as (_, tinst)) =
7.33 + map_values (tinst_tab_type tinst) (inst_tab_term inst) (inst_tab_thm sg inst);
7.34
7.35 fun inst_tab_elems sign inst ((n, ps), elems) =
7.36 ((n, map (inst_tab_term inst) ps), map (inst_tab_elem sign inst) elems);
7.37 @@ -1923,7 +1926,8 @@
7.38 disch (prfx, atts) (thy_ctxt, Notes facts) =
7.39 let
7.40 val reg_atts = map (attrib thy_ctxt) atts;
7.41 - val facts = map_attrib_facts (attrib thy_ctxt) facts;
7.42 + (* discharge hyps in attributes *)
7.43 + val facts = map_attrib_facts (attrib thy_ctxt o Args.map_values I I I disch) facts;
7.44 val facts' = map (apfst (apsnd (fn a => a @ reg_atts))) facts;
7.45 (* discharge hyps *)
7.46 val facts'' = map (apsnd (map (apfst (map disch)))) facts';