Interpretation supports statically scoped attributes; documentation.
authorballarin
Mon Apr 18 09:25:23 2005 +0200 (2005-04-18)
changeset 15763b901a127ac73
parent 15762 13d1ec61bc89
child 15764 250df939a1de
Interpretation supports statically scoped attributes; documentation.
NEWS
doc-src/IsarRef/generic.tex
src/FOL/ex/LocaleTest.thy
src/HOL/Algebra/CRing.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/UnivPoly.thy
src/Pure/Isar/locale.ML
     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';