# HG changeset patch
# User haftmann
# Date 1238591769 -7200
# Node ID 1344132160bb303faae60525e2d86bd8e0505990
# Parent  46e16145d4bd742721af810bf34da2dc06e0e8c6
proper external tikz pictures

diff -r 46e16145d4bd -r 1344132160bb doc-src/Classes/Thy/document/Classes.tex
--- a/doc-src/Classes/Thy/document/Classes.tex	Wed Apr 01 12:19:15 2009 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex	Wed Apr 01 15:16:09 2009 +0200
@@ -1191,7 +1191,7 @@
 \hspace*{0pt}\\
 \hspace*{0pt}pow{\char95}nat ::~forall a.~(Monoid a) => Nat -> a -> a;\\
 \hspace*{0pt}pow{\char95}nat Zero{\char95}nat x = neutral;\\
-\hspace*{0pt}pow{\char95}nat (Suc n) xa = mult xa (pow{\char95}nat n xa);\\
+\hspace*{0pt}pow{\char95}nat (Suc n) x = mult x (pow{\char95}nat n x);\\
 \hspace*{0pt}\\
 \hspace*{0pt}pow{\char95}int ::~forall a.~(Group a) => Integer -> a -> a;\\
 \hspace*{0pt}pow{\char95}int k x =\\
@@ -1272,8 +1272,8 @@
 \hspace*{0pt} ~IntInf.int group;\\
 \hspace*{0pt}\\
 \hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\
-\hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) xa =\\
-\hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) xa (pow{\char95}nat A{\char95}~n xa);\\
+\hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) x =\\
+\hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) x (pow{\char95}nat A{\char95}~n x);\\
 \hspace*{0pt}\\
 \hspace*{0pt}fun pow{\char95}int A{\char95}~k x =\\
 \hspace*{0pt} ~(if IntInf.<= ((0 :~IntInf.int),~k)\\
diff -r 46e16145d4bd -r 1344132160bb doc-src/Codegen/Thy/Adaption.thy
--- a/doc-src/Codegen/Thy/Adaption.thy	Wed Apr 01 12:19:15 2009 +0200
+++ b/doc-src/Codegen/Thy/Adaption.thy	Wed Apr 01 15:16:09 2009 +0200
@@ -59,42 +59,7 @@
   supposed to be:
 
   \begin{figure}[here]
-    \begin{tikzpicture}[scale = 0.5]
-      \tikzstyle water=[color = blue, thick]
-      \tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white]
-      \tikzstyle process=[color = green, semithick, ->]
-      \tikzstyle adaption=[color = red, semithick, ->]
-      \tikzstyle target=[color = black]
-      \foreach \x in {0, ..., 24}
-        \draw[style=water] (\x, 0.25) sin + (0.25, 0.25) cos + (0.25, -0.25) sin
-          + (0.25, -0.25) cos + (0.25, 0.25);
-      \draw[style=ice] (1, 0) --
-        (3, 6) node[above, fill=white] {logic} -- (5, 0) -- cycle;
-      \draw[style=ice] (9, 0) --
-        (11, 6) node[above, fill=white] {intermediate language} -- (13, 0) -- cycle;
-      \draw[style=ice] (15, -6) --
-        (19, 6) node[above, fill=white] {target language} -- (23, -6) -- cycle;
-      \draw[style=process]
-        (3.5, 3) .. controls (7, 5) .. node[fill=white] {translation} (10.5, 3);
-      \draw[style=process]
-        (11.5, 3) .. controls (15, 5) .. node[fill=white] (serialisation) {serialisation} (18.5, 3);
-      \node (adaption) at (11, -2) [style=adaption] {adaption};
-      \node at (19, 3) [rotate=90] {generated};
-      \node at (19.5, -5) {language};
-      \node at (19.5, -3) {library};
-      \node (includes) at (19.5, -1) {includes};
-      \node (reserved) at (16.5, -3) [rotate=72] {reserved}; % proper 71.57
-      \draw[style=process]
-        (includes) -- (serialisation);
-      \draw[style=process]
-        (reserved) -- (serialisation);
-      \draw[style=adaption]
-        (adaption) -- (serialisation);
-      \draw[style=adaption]
-        (adaption) -- (includes);
-      \draw[style=adaption]
-        (adaption) -- (reserved);
-    \end{tikzpicture}
+    \includegraphics{Thy/pictures/adaption}
     \caption{The adaption principle}
     \label{fig:adaption}
   \end{figure}
diff -r 46e16145d4bd -r 1344132160bb doc-src/Codegen/Thy/Introduction.thy
--- a/doc-src/Codegen/Thy/Introduction.thy	Wed Apr 01 12:19:15 2009 +0200
+++ b/doc-src/Codegen/Thy/Introduction.thy	Wed Apr 01 15:16:09 2009 +0200
@@ -121,29 +121,7 @@
   how it works.
 
   \begin{figure}[h]
-    \begin{tikzpicture}[x = 4.2cm, y = 1cm]
-      \tikzstyle entity=[rounded corners, draw, thick, color = black, fill = white];
-      \tikzstyle process=[ellipse, draw, thick, color = green, fill = white];
-      \tikzstyle process_arrow=[->, semithick, color = green];
-      \node (HOL) at (0, 4) [style=entity] {@{text "Isabelle/HOL"} theory};
-      \node (eqn) at (2, 2) [style=entity] {code equations};
-      \node (iml) at (2, 0) [style=entity] {intermediate language};
-      \node (seri) at (1, 0) [style=process] {serialisation};
-      \node (SML) at (0, 3) [style=entity] {@{text SML}};
-      \node (OCaml) at (0, 2) [style=entity] {@{text OCaml}};
-      \node (further) at (0, 1) [style=entity] {@{text "\<dots>"}};
-      \node (Haskell) at (0, 0) [style=entity] {@{text Haskell}};
-      \draw [style=process_arrow] (HOL) .. controls (2, 4) ..
-        node [style=process, near start] {selection}
-        node [style=process, near end] {preprocessing}
-        (eqn);
-      \draw [style=process_arrow] (eqn) -- node (transl) [style=process] {translation} (iml);
-      \draw [style=process_arrow] (iml) -- (seri);
-      \draw [style=process_arrow] (seri) -- (SML);
-      \draw [style=process_arrow] (seri) -- (OCaml);
-      \draw [style=process_arrow, dashed] (seri) -- (further);
-      \draw [style=process_arrow] (seri) -- (Haskell);
-    \end{tikzpicture}
+    \includegraphics{Thy/pictures/architecture}
     \caption{Code generator architecture}
     \label{fig:arch}
   \end{figure}
@@ -164,35 +142,29 @@
 
   \begin{itemize}
 
-    \item Out of the vast collection of theorems proven in a
-      \qn{theory}, a reasonable subset modelling
-      code equations is \qn{selected}.
-
-    \item On those selected theorems, certain
-      transformations are carried out
-      (\qn{preprocessing}).  Their purpose is to turn theorems
-      representing non- or badly executable
-      specifications into equivalent but executable counterparts.
-      The result is a structured collection of \qn{code theorems}.
+    \item Starting point is a collection of raw code equations in a
+      theory; due to proof irrelevance it is not relevant where they
+      stem from but typically they are either descendant of specification
+      tools or explicit proofs by the user.
+      
+    \item Before these raw code equations are continued
+      with, they can be subjected to theorem transformations.  This
+      \qn{preprocessor} is an interface which allows to apply the full
+      expressiveness of ML-based theorem transformations to code
+      generation.  The result of the preprocessing step is a
+      structured collection of code equations.
 
-    \item Before the selected code equations are continued with,
-      they can be \qn{preprocessed}, i.e. subjected to theorem
-      transformations.  This \qn{preprocessor} is an interface which
-      allows to apply
-      the full expressiveness of ML-based theorem transformations
-      to code generation;  motivating examples are shown below, see
-      \secref{sec:preproc}.
-      The result of the preprocessing step is a structured collection
-      of code equations.
-
-    \item These code equations are \qn{translated} to a program
-      in an abstract intermediate language.  Think of it as a kind
+    \item These code equations are \qn{translated} to a program in an
+      abstract intermediate language.  Think of it as a kind
       of \qt{Mini-Haskell} with four \qn{statements}: @{text data}
       (for datatypes), @{text fun} (stemming from code equations),
       also @{text class} and @{text inst} (for type classes).
 
     \item Finally, the abstract program is \qn{serialised} into concrete
       source code of a target language.
+      This step only produces concrete syntax but does not change the
+      program in essence; all conceptual transformations occur in the
+      translation step.
 
   \end{itemize}
 
diff -r 46e16145d4bd -r 1344132160bb doc-src/Codegen/Thy/document/Adaption.tex
--- a/doc-src/Codegen/Thy/document/Adaption.tex	Wed Apr 01 12:19:15 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Adaption.tex	Wed Apr 01 15:16:09 2009 +0200
@@ -96,42 +96,7 @@
   supposed to be:
 
   \begin{figure}[here]
-    \begin{tikzpicture}[scale = 0.5]
-      \tikzstyle water=[color = blue, thick]
-      \tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white]
-      \tikzstyle process=[color = green, semithick, ->]
-      \tikzstyle adaption=[color = red, semithick, ->]
-      \tikzstyle target=[color = black]
-      \foreach \x in {0, ..., 24}
-        \draw[style=water] (\x, 0.25) sin + (0.25, 0.25) cos + (0.25, -0.25) sin
-          + (0.25, -0.25) cos + (0.25, 0.25);
-      \draw[style=ice] (1, 0) --
-        (3, 6) node[above, fill=white] {logic} -- (5, 0) -- cycle;
-      \draw[style=ice] (9, 0) --
-        (11, 6) node[above, fill=white] {intermediate language} -- (13, 0) -- cycle;
-      \draw[style=ice] (15, -6) --
-        (19, 6) node[above, fill=white] {target language} -- (23, -6) -- cycle;
-      \draw[style=process]
-        (3.5, 3) .. controls (7, 5) .. node[fill=white] {translation} (10.5, 3);
-      \draw[style=process]
-        (11.5, 3) .. controls (15, 5) .. node[fill=white] (serialisation) {serialisation} (18.5, 3);
-      \node (adaption) at (11, -2) [style=adaption] {adaption};
-      \node at (19, 3) [rotate=90] {generated};
-      \node at (19.5, -5) {language};
-      \node at (19.5, -3) {library};
-      \node (includes) at (19.5, -1) {includes};
-      \node (reserved) at (16.5, -3) [rotate=72] {reserved}; % proper 71.57
-      \draw[style=process]
-        (includes) -- (serialisation);
-      \draw[style=process]
-        (reserved) -- (serialisation);
-      \draw[style=adaption]
-        (adaption) -- (serialisation);
-      \draw[style=adaption]
-        (adaption) -- (includes);
-      \draw[style=adaption]
-        (adaption) -- (reserved);
-    \end{tikzpicture}
+    \includegraphics{Thy/pictures/adaption}
     \caption{The adaption principle}
     \label{fig:adaption}
   \end{figure}
diff -r 46e16145d4bd -r 1344132160bb doc-src/Codegen/Thy/document/Introduction.tex
--- a/doc-src/Codegen/Thy/document/Introduction.tex	Wed Apr 01 12:19:15 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex	Wed Apr 01 15:16:09 2009 +0200
@@ -284,29 +284,7 @@
   how it works.
 
   \begin{figure}[h]
-    \begin{tikzpicture}[x = 4.2cm, y = 1cm]
-      \tikzstyle entity=[rounded corners, draw, thick, color = black, fill = white];
-      \tikzstyle process=[ellipse, draw, thick, color = green, fill = white];
-      \tikzstyle process_arrow=[->, semithick, color = green];
-      \node (HOL) at (0, 4) [style=entity] {\isa{Isabelle{\isacharslash}HOL} theory};
-      \node (eqn) at (2, 2) [style=entity] {code equations};
-      \node (iml) at (2, 0) [style=entity] {intermediate language};
-      \node (seri) at (1, 0) [style=process] {serialisation};
-      \node (SML) at (0, 3) [style=entity] {\isa{SML}};
-      \node (OCaml) at (0, 2) [style=entity] {\isa{OCaml}};
-      \node (further) at (0, 1) [style=entity] {\isa{{\isasymdots}}};
-      \node (Haskell) at (0, 0) [style=entity] {\isa{Haskell}};
-      \draw [style=process_arrow] (HOL) .. controls (2, 4) ..
-        node [style=process, near start] {selection}
-        node [style=process, near end] {preprocessing}
-        (eqn);
-      \draw [style=process_arrow] (eqn) -- node (transl) [style=process] {translation} (iml);
-      \draw [style=process_arrow] (iml) -- (seri);
-      \draw [style=process_arrow] (seri) -- (SML);
-      \draw [style=process_arrow] (seri) -- (OCaml);
-      \draw [style=process_arrow, dashed] (seri) -- (further);
-      \draw [style=process_arrow] (seri) -- (Haskell);
-    \end{tikzpicture}
+    \includegraphics{Thy/pictures/architecture}
     \caption{Code generator architecture}
     \label{fig:arch}
   \end{figure}
@@ -327,35 +305,29 @@
 
   \begin{itemize}
 
-    \item Out of the vast collection of theorems proven in a
-      \qn{theory}, a reasonable subset modelling
-      code equations is \qn{selected}.
-
-    \item On those selected theorems, certain
-      transformations are carried out
-      (\qn{preprocessing}).  Their purpose is to turn theorems
-      representing non- or badly executable
-      specifications into equivalent but executable counterparts.
-      The result is a structured collection of \qn{code theorems}.
+    \item Starting point is a collection of raw code equations in a
+      theory; due to proof irrelevance it is not relevant where they
+      stem from but typically they are either descendant of specification
+      tools or explicit proofs by the user.
+      
+    \item Before these raw code equations are continued
+      with, they can be subjected to theorem transformations.  This
+      \qn{preprocessor} is an interface which allows to apply the full
+      expressiveness of ML-based theorem transformations to code
+      generation.  The result of the preprocessing step is a
+      structured collection of code equations.
 
-    \item Before the selected code equations are continued with,
-      they can be \qn{preprocessed}, i.e. subjected to theorem
-      transformations.  This \qn{preprocessor} is an interface which
-      allows to apply
-      the full expressiveness of ML-based theorem transformations
-      to code generation;  motivating examples are shown below, see
-      \secref{sec:preproc}.
-      The result of the preprocessing step is a structured collection
-      of code equations.
-
-    \item These code equations are \qn{translated} to a program
-      in an abstract intermediate language.  Think of it as a kind
+    \item These code equations are \qn{translated} to a program in an
+      abstract intermediate language.  Think of it as a kind
       of \qt{Mini-Haskell} with four \qn{statements}: \isa{data}
       (for datatypes), \isa{fun} (stemming from code equations),
       also \isa{class} and \isa{inst} (for type classes).
 
     \item Finally, the abstract program is \qn{serialised} into concrete
       source code of a target language.
+      This step only produces concrete syntax but does not change the
+      program in essence; all conceptual transformations occur in the
+      translation step.
 
   \end{itemize}
 
diff -r 46e16145d4bd -r 1344132160bb doc-src/Codegen/Thy/pictures/adaption.tex
--- a/doc-src/Codegen/Thy/pictures/adaption.tex	Wed Apr 01 12:19:15 2009 +0200
+++ b/doc-src/Codegen/Thy/pictures/adaption.tex	Wed Apr 01 15:16:09 2009 +0200
@@ -1,7 +1,5 @@
 
 \documentclass[12pt]{article}
-\usepackage{pgf}
-\usepackage{pgflibraryshapes}
 \usepackage{tikz}
 
 \begin{document}
@@ -10,7 +8,7 @@
 \setlength{\fboxrule}{0.01pt}
 \setlength{\fboxsep}{4pt}
 
-\fbox{
+\fcolorbox{white}{white}{
 
 \begin{tikzpicture}[scale = 0.5]
   \tikzstyle water=[color = blue, thick]
diff -r 46e16145d4bd -r 1344132160bb doc-src/Codegen/Thy/pictures/architecture.tex
--- a/doc-src/Codegen/Thy/pictures/architecture.tex	Wed Apr 01 12:19:15 2009 +0200
+++ b/doc-src/Codegen/Thy/pictures/architecture.tex	Wed Apr 01 15:16:09 2009 +0200
@@ -1,8 +1,8 @@
 
 \documentclass[12pt]{article}
-\usepackage{pgf}
-\usepackage{pgflibraryshapes}
 \usepackage{tikz}
+\usetikzlibrary{shapes}
+\usetikzlibrary{arrows}
 
 \begin{document}
 
@@ -10,30 +10,39 @@
 \setlength{\fboxrule}{0.01pt}
 \setlength{\fboxsep}{4pt}
 
-\fbox{
+\fcolorbox{white}{white}{
+
+\newcommand{\sys}[1]{\emph{#1}}
 
-\begin{tikzpicture}[x = 4.2cm, y = 1cm]
-  \tikzstyle entity=[rounded corners, draw, thick, color = black, fill = white];
-  \tikzstyle process=[ellipse, draw, thick, color = green, fill = white];
-  \tikzstyle process_arrow=[->, semithick, color = green];
-  \node (HOL) at (0, 4) [style=entity] {Isabelle/HOL theory};
-  \node (eqn) at (2, 2) [style=entity] {code equations};
-  \node (iml) at (2, 0) [style=entity] {intermediate language};
-  \node (seri) at (1, 0) [style=process] {serialisation};
-  \node (SML) at (0, 3) [style=entity] {SML};
-  \node (OCaml) at (0, 2) [style=entity] {OCaml};
-  \node (further) at (0, 1) [style=entity] {\ldots};
-  \node (Haskell) at (0, 0) [style=entity] {Haskell};
-  \draw [style=process_arrow] (HOL) .. controls (2, 4) ..
-    node [style=process, near start] {selection}
-    node [style=process, near end] {preprocessing}
-    (eqn);
-  \draw [style=process_arrow] (eqn) -- node (transl) [style=process] {translation} (iml);
-  \draw [style=process_arrow] (iml) -- (seri);
-  \draw [style=process_arrow] (seri) -- (SML);
-  \draw [style=process_arrow] (seri) -- (OCaml);
-  \draw [style=process_arrow, dashed] (seri) -- (further);
-  \draw [style=process_arrow] (seri) -- (Haskell);
+\begin{tikzpicture}[x = 4cm, y = 1cm]
+  \tikzstyle positive=[color = black, fill = white];
+  \tikzstyle negative=[color = white, fill = black];
+  \tikzstyle entity=[rounded corners, draw, thick];
+  \tikzstyle process=[ellipse, draw, thick];
+  \tikzstyle arrow=[-stealth, semithick];
+  \node (spec) at (0, 3) [entity, positive] {specification tools};
+  \node (user) at (1, 3) [entity, positive] {user proofs};
+  \node (spec_user_join) at (0.5, 3) [shape=coordinate] {};
+  \node (raw) at (0.5, 4) [entity, positive] {raw code equations};
+  \node (pre) at (1.5, 4) [process, positive] {preprocessing};
+  \node (eqn) at (2.5, 4) [entity, positive] {code equations};
+  \node (iml) at (0.5, 0) [entity, positive] {intermediate program};
+  \node (seri) at (1.5, 0) [process, positive] {serialisation};
+  \node (SML) at (2.5, 3) [entity, positive] {\sys{SML}};
+  \node (OCaml) at (2.5, 2) [entity, positive] {\sys{OCaml}};
+  \node (further) at (2.5, 1) [entity, positive] {(\ldots)};
+  \node (Haskell) at (2.5, 0) [entity, positive] {\sys{Haskell}};
+  \draw [semithick] (spec) -- (spec_user_join);
+  \draw [semithick] (user) -- (spec_user_join);
+  \draw [-diamond, semithick] (spec_user_join) -- (raw);
+  \draw [arrow] (raw) -- (pre);
+  \draw [arrow] (pre) -- (eqn);
+  \draw [arrow] (eqn) -- node (transl) [process, positive] {translation} (iml);
+  \draw [arrow] (iml) -- (seri);
+  \draw [arrow] (seri) -- (SML);
+  \draw [arrow] (seri) -- (OCaml);
+  \draw [arrow, dashed] (seri) -- (further);
+  \draw [arrow] (seri) -- (Haskell);
 \end{tikzpicture}
 
 }
diff -r 46e16145d4bd -r 1344132160bb doc-src/Codegen/codegen.tex
--- a/doc-src/Codegen/codegen.tex	Wed Apr 01 12:19:15 2009 +0200
+++ b/doc-src/Codegen/codegen.tex	Wed Apr 01 15:16:09 2009 +0200
@@ -5,9 +5,6 @@
 \usepackage{../iman,../extra,../isar,../proof}
 \usepackage{../isabelle,../isabellesym}
 \usepackage{style}
-\usepackage{pgf}
-\usepackage{pgflibraryshapes}
-\usepackage{tikz}
 \usepackage{../pdfsetup}
 
 \hyphenation{Isabelle}