--- a/NEWS Wed Oct 07 16:57:56 2009 +0200
+++ b/NEWS Thu Oct 08 15:16:13 2009 +0200
@@ -24,6 +24,12 @@
in proofs are not shown.
+*** document preparation ***
+
+* New generalized style concept for printing terms:
+write @{foo (style) ...} instead of @{foo_style style ...}.
+
+
*** HOL ***
* Most rules produced by inductive and datatype package
--- a/doc-src/IsarRef/Thy/Document_Preparation.thy Wed Oct 07 16:57:56 2009 +0200
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Thu Oct 08 15:16:13 2009 +0200
@@ -145,8 +145,6 @@
@{antiquotation_def abbrev} & : & @{text antiquotation} \\
@{antiquotation_def typeof} & : & @{text antiquotation} \\
@{antiquotation_def typ} & : & @{text antiquotation} \\
- @{antiquotation_def thm_style} & : & @{text antiquotation} \\
- @{antiquotation_def term_style} & : & @{text antiquotation} \\
@{antiquotation_def "text"} & : & @{text antiquotation} \\
@{antiquotation_def goals} & : & @{text antiquotation} \\
@{antiquotation_def subgoals} & : & @{text antiquotation} \\
@@ -182,16 +180,14 @@
antiquotation:
'theory' options name |
- 'thm' options thmrefs |
+ 'thm' options styles thmrefs |
'lemma' options prop 'by' method |
- 'prop' options prop |
- 'term' options term |
+ 'prop' options styles prop |
+ 'term' options styles term |
'const' options term |
'abbrev' options term |
'typeof' options term |
'typ' options type |
- 'thm\_style' options name thmref |
- 'term\_style' options name term |
'text' options name |
'goals' options |
'subgoals' options |
@@ -205,6 +201,10 @@
;
option: name | name '=' name
;
+ styles: '(' (style * ',') ')'
+ ;
+ style: (name *)
+ ;
\end{rail}
Note that the syntax of antiquotations may \emph{not} include source
@@ -241,12 +241,6 @@
\item @{text "@{typ \<tau>}"} prints a well-formed type @{text "\<tau>"}.
- \item @{text "@{thm_style s a}"} prints theorem @{text a},
- previously applying a style @{text s} to it (see below).
-
- \item @{text "@{term_style s t}"} prints a well-typed term @{text t}
- after applying a style @{text s} to it (see below).
-
\item @{text "@{text s}"} prints uninterpreted source text @{text
s}. This is particularly useful to print portions of text according
to the Isabelle document style, without demanding well-formedness,
@@ -285,9 +279,11 @@
subsubsection {* Styled antiquotations *}
-text {* Some antiquotations like @{text thm_style} and @{text
- term_style} admit an extra \emph{style} specification to modify the
- printed result. The following standard styles are available:
+text {* The antiquotations @{text thm}, @{text prop} and @{text
+ term} admit an extra \emph{style} specification to modify the
+ printed result. A style is specified by a name with a possibly
+ empty number of arguments; multiple styles can be sequenced with
+ commas. The following standard styles are available:
\begin{description}
@@ -301,8 +297,8 @@
\item @{text "concl"} extracts the conclusion @{text C} from a rule
in Horn-clause normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}.
- \item @{text "prem1"}, \dots, @{text "prem9"} extract premise number
- @{text "1, \<dots>, 9"}, respectively, from from a rule in Horn-clause
+ \item @{text "prem"} @{text n} extract premise number
+ @{text "n"} from from a rule in Horn-clause
normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}
\end{description}
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Wed Oct 07 16:57:56 2009 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Thu Oct 08 15:16:13 2009 +0200
@@ -296,20 +296,20 @@
own way, you can extract the premises and the conclusion explicitly
and combine them as you like:
\begin{itemize}
-\item \verb!@!\verb!{thm_style prem1! $thm$\verb!}!
-prints premise 1 of $thm$ (and similarly up to \texttt{prem9}).
-\item \verb!@!\verb!{thm_style concl! $thm$\verb!}!
+\item \verb!@!\verb!{thm (prem 1)! $thm$\verb!}!
+prints premise 1 of $thm$.
+\item \verb!@!\verb!{thm (concl)! $thm$\verb!}!
prints the conclusion of $thm$.
\end{itemize}
-For example, ``from @{thm_style prem2 conjI} and
-@{thm_style prem1 conjI} we conclude @{thm_style concl conjI}''
+For example, ``from @{thm (prem 2) conjI} and
+@{thm (prem 1) conjI} we conclude @{thm (concl) conjI}''
is produced by
\begin{quote}
-\verb!from !\verb!@!\verb!{thm_style prem2 conjI}! \verb!and !\verb!@!\verb!{thm_style prem1 conjI}!\\
-\verb!we conclude !\verb!@!\verb!{thm_style concl conjI}!
+\verb!from !\verb!@!\verb!{thm (prem 2) conjI}! \verb!and !\verb!@!\verb!{thm (prem 1) conjI}!\\
+\verb!we conclude !\verb!@!\verb!{thm (concl) conjI}!
\end{quote}
Thus you can rearrange or hide premises and typeset the theorem as you like.
-The \verb!thm_style! antiquotation is a general mechanism explained
+Styles like !(prem 1)! are a general mechanism explained
in \S\ref{sec:styles}.
*}
@@ -394,26 +394,27 @@
``styles'':
\begin{quote}
- \verb!@!\verb!{thm_style stylename thm}!\\
- \verb!@!\verb!{term_style stylename term}!
+ \verb!@!\verb!{thm (style) thm}!\\
+ \verb!@!\verb!{prop (style) thm}!\\
+ \verb!@!\verb!{term (style) term}!
\end{quote}
A ``style'' is a transformation of propositions. There are predefined
- styles, namely \verb!lhs! and \verb!rhs!, \verb!prem1! up to \verb!prem9!, and \verb!concl!.
+ styles, namely \verb!lhs! and \verb!rhs!, \verb!prem! with one argument, and \verb!concl!.
For example,
the output
\begin{center}
\begin{tabular}{l@ {~~@{text "="}~~}l}
- @{thm_style lhs foldl_Nil} & @{thm_style rhs foldl_Nil}\\
- @{thm_style lhs foldl_Cons} & @{thm_style rhs foldl_Cons}
+ @{thm (lhs) foldl_Nil} & @{thm (rhs) foldl_Nil}\\
+ @{thm (lhs) foldl_Cons} & @{thm (rhs) foldl_Cons}
\end{tabular}
\end{center}
is produced by the following code:
\begin{quote}
\verb!\begin{center}!\\
\verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
- \verb!@!\verb!{thm_style lhs foldl_Nil} & @!\verb!{thm_style rhs foldl_Nil}!\\
- \verb!@!\verb!{thm_style lhs foldl_Cons} & @!\verb!{thm_style rhs foldl_Cons}!\\
+ \verb!@!\verb!{thm (lhs) foldl_Nil} & @!\verb!{thm (rhs) foldl_Nil}!\\
+ \verb!@!\verb!{thm (lhs) foldl_Cons} & @!\verb!{thm (rhs) foldl_Cons}!\\
\verb!\end{tabular}!\\
\verb!\end{center}!
\end{quote}
@@ -431,12 +432,12 @@
\end{center}
To print just the conclusion,
\begin{center}
- @{thm_style [show_types] concl hd_Cons_tl}
+ @{thm [show_types] (concl) hd_Cons_tl}
\end{center}
type
\begin{quote}
\verb!\begin{center}!\\
- \verb!@!\verb!{thm_style [show_types] concl hd_Cons_tl}!\\
+ \verb!@!\verb!{thm [show_types] (concl) hd_Cons_tl}!\\
\verb!\end{center}!
\end{quote}
Beware that any options must be placed \emph{before}
@@ -445,49 +446,7 @@
Further use cases can be found in \S\ref{sec:yourself}.
If you are not afraid of ML, you may also define your own styles.
- A style is implemented by an ML function of type
- \verb!Proof.context -> term -> term!.
- Have a look at the following example:
-
-*}
-(*<*)
-setup {*
-let
- fun my_concl ctxt = Logic.strip_imp_concl
- in TermStyle.add_style "my_concl" my_concl
-end;
-*}
-(*>*)
-text {*
-
- \begin{quote}
- \verb!setup {!\verb!*!\\
- \verb!let!\\
- \verb! fun my_concl ctxt = Logic.strip_imp_concl!\\
- \verb! in TermStyle.add_style "my_concl" my_concl!\\
- \verb!end;!\\
- \verb!*!\verb!}!\\
- \end{quote}
-
- \noindent
- This example shows how the \verb!concl! style is implemented
- and may be used as as a ``copy-and-paste'' pattern to write your own styles.
-
- The code should go into your theory file, separate from the \LaTeX\ text.
- The \verb!let! expression avoids polluting the
- ML global namespace. Each style receives the current proof context
- as first argument; this is helpful in situations where the
- style has some object-logic specific behaviour for example.
-
- The mapping from identifier name to the style function
- is done by the @{ML TermStyle.add_style} expression which expects the desired
- style name and the style function as arguments.
-
- After this \verb!setup!,
- there will be a new style available named \verb!my_concl!, thus allowing
- antiquoations like \verb!@!\verb!{thm_style my_concl hd_Cons_tl}!
- yielding @{thm_style my_concl hd_Cons_tl}.
-
+ Have a look at module @{ML_struct Term_Style}.
*}
(*<*)
--- a/doc-src/TutorialI/Inductive/Advanced.thy Wed Oct 07 16:57:56 2009 +0200
+++ b/doc-src/TutorialI/Inductive/Advanced.thy Thu Oct 08 15:16:13 2009 +0200
@@ -185,7 +185,7 @@
Even with its use of the function \isa{lists}, the premise of our
introduction rule is positive:
-@{thm_style [display,indent=0] prem1 step [no_vars]}
+@{thm [display,indent=0] (prem 1) step [no_vars]}
To apply the rule we construct a list @{term args} of previously
constructed well-formed terms. We obtain a
new term, @{term "Apply f args"}. Because @{term lists} is monotone,
--- a/doc-src/TutorialI/Inductive/Star.thy Wed Oct 07 16:57:56 2009 +0200
+++ b/doc-src/TutorialI/Inductive/Star.thy Thu Oct 08 15:16:13 2009 +0200
@@ -54,7 +54,7 @@
To prove transitivity, we need rule induction, i.e.\ theorem
@{thm[source]rtc.induct}:
@{thm[display]rtc.induct}
-It says that @{text"?P"} holds for an arbitrary pair @{thm_style prem1 rtc.induct}
+It says that @{text"?P"} holds for an arbitrary pair @{thm (prem 1) rtc.induct}
if @{text"?P"} is preserved by all rules of the inductive definition,
i.e.\ if @{text"?P"} holds for the conclusion provided it holds for the
premises. In general, rule induction for an $n$-ary inductive relation $R$
--- a/doc-src/TutorialI/Protocol/NS_Public.thy Wed Oct 07 16:57:56 2009 +0200
+++ b/doc-src/TutorialI/Protocol/NS_Public.thy Thu Oct 08 15:16:13 2009 +0200
@@ -375,7 +375,7 @@
From similar assumptions, we can prove that @{text A} started the protocol
run by sending an instance of message~1 involving the nonce~@{text NA}\@.
For this theorem, the conclusion is
-@{thm_style [display] concl B_trusts_protocol [no_vars]}
+@{thm [display] (concl) B_trusts_protocol [no_vars]}
Analogous theorems can be proved for~@{text A}, stating that nonce~@{text NA}
remains secret and that message~2 really originates with~@{text B}. Even the
flawed protocol establishes these properties for~@{text A};
--- a/src/HOL/Library/OptionalSugar.thy Wed Oct 07 16:57:56 2009 +0200
+++ b/src/HOL/Library/OptionalSugar.thy Thu Oct 08 15:16:13 2009 +0200
@@ -29,7 +29,7 @@
"appendL (appendL xs ys) zs" <= "appendL xs (appendL ys zs)"
-(* deprecated, use thm_style instead, will be removed *)
+(* deprecated, use thm with style instead, will be removed *)
(* aligning equations *)
notation (tab output)
"op =" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
--- a/src/Pure/Thy/term_style.ML Wed Oct 07 16:57:56 2009 +0200
+++ b/src/Pure/Thy/term_style.ML Thu Oct 08 15:16:13 2009 +0200
@@ -62,7 +62,7 @@
(* predefined styles *)
-fun style_binargs proj = Scan.succeed (fn ctxt => fn t =>
+fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>
let
val concl = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt)
(Logic.strip_imp_concl t)
@@ -71,16 +71,31 @@
| _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)
end);
+val style_prem = Args.name >> (fn raw_i => fn ctxt => fn t =>
+ let
+ val i = (the o Int.fromString) raw_i;
+ val prems = Logic.strip_imp_prems t;
+ in
+ if i <= length prems then nth prems (i - 1)
+ else error ("Not enough premises for prem " ^ string_of_int i ^
+ " in propositon: " ^ Syntax.string_of_term ctxt t)
+ end);
+
fun style_parm_premise i = Scan.succeed (fn ctxt => fn t =>
- let val prems = Logic.strip_imp_prems t in
+ let
+ val i_str = string_of_int i;
+ val prems = Logic.strip_imp_prems t;
+ in
if i <= length prems then nth prems (i - 1)
else error ("Not enough premises for prem" ^ string_of_int i ^
" in propositon: " ^ Syntax.string_of_term ctxt t)
end);
val _ = Context.>> (Context.map_theory
- (setup "lhs" (style_binargs fst) #>
- setup "rhs" (style_binargs snd) #>
+ (setup "lhs" (style_lhs_rhs fst) #>
+ setup "rhs" (style_lhs_rhs snd) #>
+ setup "prem" style_prem #>
+ setup "concl" (Scan.succeed (K Logic.strip_imp_concl)) #>
setup "prem1" (style_parm_premise 1) #>
setup "prem2" (style_parm_premise 2) #>
setup "prem3" (style_parm_premise 3) #>
@@ -99,7 +114,6 @@
setup "prem16" (style_parm_premise 16) #>
setup "prem17" (style_parm_premise 17) #>
setup "prem18" (style_parm_premise 18) #>
- setup "prem19" (style_parm_premise 19) #>
- setup "concl" (Scan.succeed (K Logic.strip_imp_concl))));
+ setup "prem19" (style_parm_premise 19)));
end;