new style dummy_pats
authornipkow
Fri Jul 08 19:35:31 2016 +0200 (2016-07-08)
changeset 63414beb987127d0f
parent 63413 9fe2d9dc095e
child 63415 8f91c2f447a0
new style dummy_pats
NEWS
src/Doc/Prog_Prove/Logic.thy
src/Doc/Sugar/Sugar.thy
src/Doc/Sugar/document/root.tex
src/HOL/Library/LaTeXsugar.thy
     1.1 --- a/NEWS	Fri Jul 08 16:38:31 2016 +0200
     1.2 +++ b/NEWS	Fri Jul 08 19:35:31 2016 +0200
     1.3 @@ -146,6 +146,10 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Theory Library/LaTeXsugar.thy: New style "dummy_pats" for displaying
     1.8 +equations in functional programming style: variables present on the
     1.9 +left-hand but not on the righ-hand side are replaced by underscores.
    1.10 +
    1.11  * Theory Library/Combinator_PER.thy: combinator to build partial
    1.12  equivalence relations from a predicate and an equivalence relation.
    1.13  
     2.1 --- a/src/Doc/Prog_Prove/Logic.thy	Fri Jul 08 16:38:31 2016 +0200
     2.2 +++ b/src/Doc/Prog_Prove/Logic.thy	Fri Jul 08 19:35:31 2016 +0200
     2.3 @@ -309,12 +309,12 @@
     2.4  \begin{isabelle}
     2.5  \isacom{try}
     2.6  \end{isabelle}
     2.7 -You can also add specific simplification and introduction rules:
     2.8 +There is also a lightweight variant \isacom{try0} that does not call
     2.9 +sledgehammer. If desired, specific simplification and introduction rules
    2.10 +can be added:
    2.11  \begin{isabelle}
    2.12 -\isacom{try} @{text"simp: \<dots> intro: \<dots>"}
    2.13 +\isacom{try0} @{text"simp: \<dots> intro: \<dots>"}
    2.14  \end{isabelle}
    2.15 -There is also a lightweight variant \isacom{try0} that does not call
    2.16 -sledgehammer.
    2.17  
    2.18  \section{Single Step Proofs}
    2.19  
     3.1 --- a/src/Doc/Sugar/Sugar.thy	Fri Jul 08 16:38:31 2016 +0200
     3.2 +++ b/src/Doc/Sugar/Sugar.thy	Fri Jul 08 19:35:31 2016 +0200
     3.3 @@ -1,6 +1,8 @@
     3.4  (*<*)
     3.5  theory Sugar
     3.6 -imports "~~/src/HOL/Library/LaTeXsugar" "~~/src/HOL/Library/OptionalSugar"
     3.7 +imports
     3.8 +  "~~/src/HOL/Library/LaTeXsugar"
     3.9 +  "~~/src/HOL/Library/OptionalSugar"
    3.10  begin
    3.11  no_translations
    3.12    ("prop") "P \<and> Q \<Longrightarrow> R" <= ("prop") "P \<Longrightarrow> Q \<Longrightarrow> R"
    3.13 @@ -20,7 +22,7 @@
    3.14  
    3.15  If you have mastered the art of Isabelle's \emph{antiquotations},
    3.16  i.e.\ things like the above \verb!@!\verb!{thm...}!, beware: in your vanity
    3.17 -you may be tempted to think that all readers of the stunning ps or pdf
    3.18 +you may be tempted to think that all readers of the stunning
    3.19  documents you can now produce at the drop of a hat will be struck with
    3.20  awe at the beauty unfolding in front of their eyes. Until one day you
    3.21  come across that very critical of readers known as the ``common referee''.
    3.22 @@ -38,7 +40,7 @@
    3.23  \item Import theory \texttt{LaTeXsugar} in the header of your own
    3.24  theory.  You may also want bits of \texttt{OptionalSugar}, which you can
    3.25  copy selectively into your own theory or import as a whole.  Both
    3.26 -theories live in \texttt{HOL/Library} and are found automatically.
    3.27 +theories live in \texttt{HOL/Library}.
    3.28  
    3.29  \item Should you need additional \LaTeX\ packages (the text will tell
    3.30  you so), you include them at the beginning of your \LaTeX\ document,
    3.31 @@ -128,9 +130,11 @@
    3.32  \verb!@!\verb!{thm conjI}! results in @{thm conjI}. Most of the time
    3.33  you would rather not see the question marks. There is an attribute
    3.34  \verb!no_vars! that you can attach to the theorem that turns its
    3.35 -schematic into ordinary free variables: \verb!@!\verb!{thm conjI[no_vars]}!
    3.36 -results in @{thm conjI[no_vars]}.
    3.37 -
    3.38 +schematic into ordinary free variables:
    3.39 +\begin{quote}
    3.40 +\verb!@!\verb!{thm conjI[no_vars]}!\\
    3.41 +\showout @{thm conjI[no_vars]}
    3.42 +\end{quote}
    3.43  This \verb!no_vars! business can become a bit tedious.
    3.44  If you would rather never see question marks, simply put
    3.45  \begin{quote}
    3.46 @@ -138,13 +142,7 @@
    3.47  \end{quote}
    3.48  into the relevant \texttt{ROOT} file, just before the \texttt{theories} for that session.
    3.49  The rest of this document is produced with this flag set to \texttt{false}.
    3.50 -
    3.51 -Hint: Setting \verb!show_question_marks! to \texttt{false} only
    3.52 -suppresses question marks; variables that end in digits,
    3.53 -e.g. @{text"x1"}, are still printed with a trailing @{text".0"},
    3.54 -e.g. @{text"x1.0"}, their internal index. This can be avoided by
    3.55 -turning the last digit into a subscript: write \<^verbatim>\<open>x\<^sub>1\<close> and
    3.56 -obtain the much nicer @{text"x\<^sub>1"}. *}
    3.57 +*}
    3.58  
    3.59  (*<*)declare [[show_question_marks = false]](*>*)
    3.60  
    3.61 @@ -163,24 +161,44 @@
    3.62  It sometimes happens that you want to change the name of a
    3.63  variable in a theorem before printing it. This can easily be achieved
    3.64  with the help of Isabelle's instantiation attribute \texttt{where}:
    3.65 -@{thm conjI[where P = \<phi> and Q = \<psi>]} is the result of
    3.66  \begin{quote}
    3.67 -\verb!@!\verb!{thm conjI[where P = \<phi> and Q = \<psi>]}!
    3.68 +\verb!@!\verb!{thm conjI[where P = \<phi> and Q = \<psi>]}!\\
    3.69 +\showout @{thm conjI[where P = \<phi> and Q = \<psi>]}
    3.70  \end{quote}
    3.71  To support the ``\_''-notation for irrelevant variables
    3.72  the constant \texttt{DUMMY} has been introduced:
    3.73 -@{thm fst_conv[of _ DUMMY]} is produced by
    3.74  \begin{quote}
    3.75 -\verb!@!\verb!{thm fst_conv[of _ DUMMY]}!
    3.76 +\verb!@!\verb!{thm fst_conv[of _ DUMMY]}!\\
    3.77 +\showout @{thm fst_conv[of _ DUMMY]}
    3.78 +\end{quote}
    3.79 +As expected, the second argument has been replaced by ``\_'',
    3.80 +but the first argument is the ugly @{text "x1.0"}, a schematic variable
    3.81 +with suppressed question mark. Schematic variables that end in digits,
    3.82 +e.g. @{text"x1"}, are still printed with a trailing @{text".0"},
    3.83 +e.g. @{text"x1.0"}, their internal index. This can be avoided by
    3.84 +turning the last digit into a subscript: write \<^verbatim>\<open>x\<^sub>1\<close> and
    3.85 +obtain the much nicer @{text"x\<^sub>1"}. Alternatively, you can display trailing digits of
    3.86 +schematic and free variables as subscripts with the \texttt{sub} style:
    3.87 +\begin{quote}
    3.88 +\verb!@!\verb!{thm (sub) fst_conv[of _ DUMMY]}!\\
    3.89 +\showout @{thm (sub) fst_conv[of _ DUMMY]}
    3.90  \end{quote}
    3.91 -Variables that are bound by quantifiers or lambdas cannot be renamed
    3.92 -like this. Instead, the attribute \texttt{rename\_abs} does the
    3.93 -job. It expects a list of names or underscores, similar to the
    3.94 -\texttt{of} attribute:
    3.95 +The insertion of underscores can be automated with the \verb!dummy_pats! style:
    3.96  \begin{quote}
    3.97 -\verb!@!\verb!{thm split_paired_All[rename_abs _ l r]}!
    3.98 +\verb!@!\verb!{thm (dummy_pats,sub) fst_conv}!\\
    3.99 +\showout @{thm (dummy_pats,sub) fst_conv}
   3.100  \end{quote}
   3.101 -produces @{thm split_paired_All[rename_abs _ l r]}.
   3.102 +The theorem must be an equation. Then every schematic variable that occurs
   3.103 +on the left-hand but not the right-hand side is replaced by \texttt{DUMMY}.
   3.104 +This is convenient for displaying functional programs.
   3.105 +
   3.106 +Variables that are bound by quantifiers or lambdas can be renamed
   3.107 +with the help of the attribute \verb!rename_abs!.
   3.108 +It expects a list of names or underscores, similar to the \texttt{of} attribute:
   3.109 +\begin{quote}
   3.110 +\verb!@!\verb!{thm split_paired_All[rename_abs _ l r]}!\\
   3.111 +\showout @{thm split_paired_All[rename_abs _ l r]}
   3.112 +\end{quote}
   3.113  
   3.114  
   3.115  \subsection{Inference rules}
     4.1 --- a/src/Doc/Sugar/document/root.tex	Fri Jul 08 16:38:31 2016 +0200
     4.2 +++ b/src/Doc/Sugar/document/root.tex	Fri Jul 08 19:35:31 2016 +0200
     4.3 @@ -12,6 +12,8 @@
     4.4  \urlstyle{rm}
     4.5  \isabellestyle{it}
     4.6  
     4.7 +\newcommand{\showout}{\mbox{}\hspace{-2em}$\leadsto$\quad}
     4.8 +
     4.9  \hyphenation{Isa-belle}
    4.10  \begin{document}
    4.11  
     5.1 --- a/src/HOL/Library/LaTeXsugar.thy	Fri Jul 08 16:38:31 2016 +0200
     5.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Fri Jul 08 19:35:31 2016 +0200
     5.3 @@ -112,5 +112,21 @@
     5.4    end;
     5.5  \<close>
     5.6  
     5.7 +setup\<open>
     5.8 +let
     5.9 +  fun dummy_pats (wrap $ (eq $ lhs $ rhs)) =
    5.10 +    let
    5.11 +      val rhs_vars = Term.add_vars rhs [];
    5.12 +      fun dummy (v as Var (ixn as (_, T))) =
    5.13 +            if member (op = ) rhs_vars ixn then v else Const (@{const_name DUMMY}, T)
    5.14 +        | dummy (t $ u) = dummy t $ dummy u
    5.15 +        | dummy (Abs (n, T, b)) = Abs (n, T, dummy b)
    5.16 +        | dummy t = t;
    5.17 +    in wrap $ (eq $ dummy lhs $ rhs) end
    5.18 +in
    5.19 +  Term_Style.setup @{binding dummy_pats} (Scan.succeed (K dummy_pats))
    5.20 +end
    5.21 +\<close>
    5.22 +
    5.23  end
    5.24  (*>*)