new style dummy_pats

--- a/NEWS	Fri Jul 08 16:38:31 2016 +0200
+++ b/NEWS	Fri Jul 08 19:35:31 2016 +0200
@@ -146,6 +146,10 @@
 
 *** HOL ***
 
+* Theory Library/LaTeXsugar.thy: New style "dummy_pats" for displaying
+equations in functional programming style: variables present on the
+left-hand but not on the righ-hand side are replaced by underscores.
+
 * Theory Library/Combinator_PER.thy: combinator to build partial
 equivalence relations from a predicate and an equivalence relation.
 

--- a/src/Doc/Prog_Prove/Logic.thy	Fri Jul 08 16:38:31 2016 +0200
+++ b/src/Doc/Prog_Prove/Logic.thy	Fri Jul 08 19:35:31 2016 +0200
@@ -309,12 +309,12 @@
 \begin{isabelle}
 \isacom{try}
 \end{isabelle}
-You can also add specific simplification and introduction rules:
+There is also a lightweight variant \isacom{try0} that does not call
+sledgehammer. If desired, specific simplification and introduction rules
+can be added:
 \begin{isabelle}
-\isacom{try} @{text"simp: \<dots> intro: \<dots>"}
+\isacom{try0} @{text"simp: \<dots> intro: \<dots>"}
 \end{isabelle}
-There is also a lightweight variant \isacom{try0} that does not call
-sledgehammer.
 
 \section{Single Step Proofs}
 

--- a/src/Doc/Sugar/Sugar.thy	Fri Jul 08 16:38:31 2016 +0200
+++ b/src/Doc/Sugar/Sugar.thy	Fri Jul 08 19:35:31 2016 +0200
@@ -1,6 +1,8 @@
 (*<*)
 theory Sugar
-imports "~~/src/HOL/Library/LaTeXsugar" "~~/src/HOL/Library/OptionalSugar"
+imports
+  "~~/src/HOL/Library/LaTeXsugar"
+  "~~/src/HOL/Library/OptionalSugar"
 begin
 no_translations
   ("prop") "P \<and> Q \<Longrightarrow> R" <= ("prop") "P \<Longrightarrow> Q \<Longrightarrow> R"
@@ -20,7 +22,7 @@
 
 If you have mastered the art of Isabelle's \emph{antiquotations},
 i.e.\ things like the above \verb!@!\verb!{thm...}!, beware: in your vanity
-you may be tempted to think that all readers of the stunning ps or pdf
+you may be tempted to think that all readers of the stunning
 documents you can now produce at the drop of a hat will be struck with
 awe at the beauty unfolding in front of their eyes. Until one day you
 come across that very critical of readers known as the ``common referee''.
@@ -38,7 +40,7 @@
 \item Import theory \texttt{LaTeXsugar} in the header of your own
 theory.  You may also want bits of \texttt{OptionalSugar}, which you can
 copy selectively into your own theory or import as a whole.  Both
-theories live in \texttt{HOL/Library} and are found automatically.
+theories live in \texttt{HOL/Library}.
 
 \item Should you need additional \LaTeX\ packages (the text will tell
 you so), you include them at the beginning of your \LaTeX\ document,
@@ -128,9 +130,11 @@
 \verb!@!\verb!{thm conjI}! results in @{thm conjI}. Most of the time
 you would rather not see the question marks. There is an attribute
 \verb!no_vars! that you can attach to the theorem that turns its
-schematic into ordinary free variables: \verb!@!\verb!{thm conjI[no_vars]}!
-results in @{thm conjI[no_vars]}.
-
+schematic into ordinary free variables:
+\begin{quote}
+\verb!@!\verb!{thm conjI[no_vars]}!\\
+\showout @{thm conjI[no_vars]}
+\end{quote}
 This \verb!no_vars! business can become a bit tedious.
 If you would rather never see question marks, simply put
 \begin{quote}
@@ -138,13 +142,7 @@
 \end{quote}
 into the relevant \texttt{ROOT} file, just before the \texttt{theories} for that session.
 The rest of this document is produced with this flag set to \texttt{false}.
-
-Hint: Setting \verb!show_question_marks! to \texttt{false} only
-suppresses question marks; variables that end in digits,
-e.g. @{text"x1"}, are still printed with a trailing @{text".0"},
-e.g. @{text"x1.0"}, their internal index. This can be avoided by
-turning the last digit into a subscript: write \<^verbatim>\<open>x\<^sub>1\<close> and
-obtain the much nicer @{text"x\<^sub>1"}. *}
+*}
 
 (*<*)declare [[show_question_marks = false]](*>*)
 
@@ -163,24 +161,44 @@
 It sometimes happens that you want to change the name of a
 variable in a theorem before printing it. This can easily be achieved
 with the help of Isabelle's instantiation attribute \texttt{where}:
-@{thm conjI[where P = \<phi> and Q = \<psi>]} is the result of
 \begin{quote}
-\verb!@!\verb!{thm conjI[where P = \<phi> and Q = \<psi>]}!
+\verb!@!\verb!{thm conjI[where P = \<phi> and Q = \<psi>]}!\\
+\showout @{thm conjI[where P = \<phi> and Q = \<psi>]}
 \end{quote}
 To support the ``\_''-notation for irrelevant variables
 the constant \texttt{DUMMY} has been introduced:
-@{thm fst_conv[of _ DUMMY]} is produced by
 \begin{quote}
-\verb!@!\verb!{thm fst_conv[of _ DUMMY]}!
+\verb!@!\verb!{thm fst_conv[of _ DUMMY]}!\\
+\showout @{thm fst_conv[of _ DUMMY]}
+\end{quote}
+As expected, the second argument has been replaced by ``\_'',
+but the first argument is the ugly @{text "x1.0"}, a schematic variable
+with suppressed question mark. Schematic variables that end in digits,
+e.g. @{text"x1"}, are still printed with a trailing @{text".0"},
+e.g. @{text"x1.0"}, their internal index. This can be avoided by
+turning the last digit into a subscript: write \<^verbatim>\<open>x\<^sub>1\<close> and
+obtain the much nicer @{text"x\<^sub>1"}. Alternatively, you can display trailing digits of
+schematic and free variables as subscripts with the \texttt{sub} style:
+\begin{quote}
+\verb!@!\verb!{thm (sub) fst_conv[of _ DUMMY]}!\\
+\showout @{thm (sub) fst_conv[of _ DUMMY]}
 \end{quote}
-Variables that are bound by quantifiers or lambdas cannot be renamed
-like this. Instead, the attribute \texttt{rename\_abs} does the
-job. It expects a list of names or underscores, similar to the
-\texttt{of} attribute:
+The insertion of underscores can be automated with the \verb!dummy_pats! style:
 \begin{quote}
-\verb!@!\verb!{thm split_paired_All[rename_abs _ l r]}!
+\verb!@!\verb!{thm (dummy_pats,sub) fst_conv}!\\
+\showout @{thm (dummy_pats,sub) fst_conv}
 \end{quote}
-produces @{thm split_paired_All[rename_abs _ l r]}.
+The theorem must be an equation. Then every schematic variable that occurs
+on the left-hand but not the right-hand side is replaced by \texttt{DUMMY}.
+This is convenient for displaying functional programs.
+
+Variables that are bound by quantifiers or lambdas can be renamed
+with the help of the attribute \verb!rename_abs!.
+It expects a list of names or underscores, similar to the \texttt{of} attribute:
+\begin{quote}
+\verb!@!\verb!{thm split_paired_All[rename_abs _ l r]}!\\
+\showout @{thm split_paired_All[rename_abs _ l r]}
+\end{quote}
 
 
 \subsection{Inference rules}

--- a/src/Doc/Sugar/document/root.tex	Fri Jul 08 16:38:31 2016 +0200
+++ b/src/Doc/Sugar/document/root.tex	Fri Jul 08 19:35:31 2016 +0200
@@ -12,6 +12,8 @@
 \urlstyle{rm}
 \isabellestyle{it}
 
+\newcommand{\showout}{\mbox{}\hspace{-2em}$\leadsto$\quad}
+
 \hyphenation{Isa-belle}
 \begin{document}
 

--- a/src/HOL/Library/LaTeXsugar.thy	Fri Jul 08 16:38:31 2016 +0200
+++ b/src/HOL/Library/LaTeXsugar.thy	Fri Jul 08 19:35:31 2016 +0200
@@ -112,5 +112,21 @@
   end;
 \<close>
 
+setup\<open>
+let
+  fun dummy_pats (wrap $ (eq $ lhs $ rhs)) =
+    let
+      val rhs_vars = Term.add_vars rhs [];
+      fun dummy (v as Var (ixn as (_, T))) =
+            if member (op = ) rhs_vars ixn then v else Const (@{const_name DUMMY}, T)
+        | dummy (t $ u) = dummy t $ dummy u
+        | dummy (Abs (n, T, b)) = Abs (n, T, dummy b)
+        | dummy t = t;
+    in wrap $ (eq $ dummy lhs $ rhs) end
+in
+  Term_Style.setup @{binding dummy_pats} (Scan.succeed (K dummy_pats))
+end
+\<close>
+
 end
 (*>*)