# HG changeset patch
# User haftmann
# Date 1255007773 -7200
# Node ID d403b99287ffb1970728b89ad42361ca958d44ff
# Parent  77df126522101d17416786054c9a91dc7c84018a
new generalized concept for term styles

diff -r 77df12652210 -r d403b99287ff NEWS
--- 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
diff -r 77df12652210 -r d403b99287ff doc-src/IsarRef/Thy/Document_Preparation.thy
--- 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}
diff -r 77df12652210 -r d403b99287ff doc-src/LaTeXsugar/Sugar/Sugar.thy
--- 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}.
 *}
 
 (*<*)
diff -r 77df12652210 -r d403b99287ff doc-src/TutorialI/Inductive/Advanced.thy
--- 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,
diff -r 77df12652210 -r d403b99287ff doc-src/TutorialI/Inductive/Star.thy
--- 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$
diff -r 77df12652210 -r d403b99287ff doc-src/TutorialI/Protocol/NS_Public.thy
--- 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};
diff -r 77df12652210 -r d403b99287ff src/HOL/Library/OptionalSugar.thy
--- 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
diff -r 77df12652210 -r d403b99287ff src/Pure/Thy/term_style.ML
--- 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;