# HG changeset patch
# User haftmann
# Date 1283439709 -7200
# Node ID 352bcd845998990531b2aa73af30b8a7a5d16676
# Parent  371976383ac07c7ea50097e43ab8e5626ee8afd8
updated

diff -r 371976383ac0 -r 352bcd845998 doc-src/Codegen/Thy/document/Foundations.tex
--- a/doc-src/Codegen/Thy/document/Foundations.tex	Thu Sep 02 16:53:23 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Foundations.tex	Thu Sep 02 17:01:49 2010 +0200
@@ -247,11 +247,11 @@
 \begin{isamarkuptext}%
 \isatypewriter%
 \noindent%
-\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
-\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
-\hspace*{0pt}dequeue (AQueue xs []) =\\
-\hspace*{0pt} ~(if null xs then (Nothing,~AQueue [] [])\\
-\hspace*{0pt} ~~~else dequeue (AQueue [] (reverse xs)));%
+\hspace*{0pt}dequeue ::~forall a.~Example.Queue a -> (Maybe a,~Example.Queue a);\\
+\hspace*{0pt}dequeue (Example.AQueue xs (y :~ys)) = (Just y,~Example.AQueue xs ys);\\
+\hspace*{0pt}dequeue (Example.AQueue xs []) =\\
+\hspace*{0pt} ~(if null xs then (Nothing,~Example.AQueue [] [])\\
+\hspace*{0pt} ~~~else Example.dequeue (Example.AQueue [] (reverse xs)));%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -350,21 +350,21 @@
 \isatypewriter%
 \noindent%
 \hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt} ~type 'a eq\\
-\hspace*{0pt} ~val eq :~'a eq -> 'a -> 'a -> bool\\
-\hspace*{0pt} ~val eqa :~'a eq -> 'a -> 'a -> bool\\
-\hspace*{0pt} ~val member :~'a eq -> 'a list -> 'a -> bool\\
+\hspace*{0pt} ~type 'a equal\\
+\hspace*{0pt} ~val equal :~'a equal -> 'a -> 'a -> bool\\
+\hspace*{0pt} ~val eq :~'a equal -> 'a -> 'a -> bool\\
+\hspace*{0pt} ~val member :~'a equal -> 'a list -> 'a -> bool\\
 \hspace*{0pt} ~val collect{\char95}duplicates :\\
-\hspace*{0pt} ~~~'a eq -> 'a list -> 'a list -> 'a list -> 'a list\\
+\hspace*{0pt} ~~~'a equal -> 'a list -> 'a list -> 'a list -> 'a list\\
 \hspace*{0pt}end = struct\\
 \hspace*{0pt}\\
-\hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\
-\hspace*{0pt}val eq = {\char35}eq :~'a eq -> 'a -> 'a -> bool;\\
+\hspace*{0pt}type 'a equal = {\char123}equal :~'a -> 'a -> bool{\char125};\\
+\hspace*{0pt}val equal = {\char35}equal :~'a equal -> 'a -> 'a -> bool;\\
 \hspace*{0pt}\\
-\hspace*{0pt}fun eqa A{\char95}~a b = eq A{\char95}~a b;\\
+\hspace*{0pt}fun eq A{\char95}~a b = equal A{\char95}~a b;\\
 \hspace*{0pt}\\
 \hspace*{0pt}fun member A{\char95}~[] y = false\\
-\hspace*{0pt} ~| member A{\char95}~(x ::~xs) y = eqa A{\char95}~x y orelse member A{\char95}~xs y;\\
+\hspace*{0pt} ~| member A{\char95}~(x ::~xs) y = eq A{\char95}~x y orelse member A{\char95}~xs y;\\
 \hspace*{0pt}\\
 \hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\
 \hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\
@@ -387,11 +387,11 @@
 \begin{isamarkuptext}%
 \noindent Obviously, polymorphic equality is implemented the Haskell
   way using a type class.  How is this achieved?  HOL introduces an
-  explicit class \isa{eq} with a corresponding operation \isa{eq{\isacharunderscore}class{\isachardot}eq} such that \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharequal}\ op\ {\isacharequal}}.  The preprocessing
-  framework does the rest by propagating the \isa{eq} constraints
+  explicit class \isa{equal} with a corresponding operation \isa{equal{\isacharunderscore}class{\isachardot}equal} such that \isa{equal{\isacharunderscore}class{\isachardot}equal\ {\isacharequal}\ op\ {\isacharequal}}.  The preprocessing
+  framework does the rest by propagating the \isa{equal} constraints
   through all dependent code equations.  For datatypes, instances of
-  \isa{eq} are implicitly derived when possible.  For other types,
-  you may instantiate \isa{eq} manually like any other type class.%
+  \isa{equal} are implicitly derived when possible.  For other types,
+  you may instantiate \isa{equal} manually like any other type class.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -444,12 +444,12 @@
 \begin{isamarkuptext}%
 \isatypewriter%
 \noindent%
-\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
-\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
+\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Example.Queue a -> (a,~Example.Queue a);\\
+\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs []) =\\
 \hspace*{0pt} ~let {\char123}\\
 \hspace*{0pt} ~~~(y :~ys) = reverse xs;\\
-\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\
-\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);%
+\hspace*{0pt} ~{\char125}~in (y,~Example.AQueue [] ys);\\
+\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs (y :~ys)) = (y,~Example.AQueue xs ys);%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -538,11 +538,11 @@
 \hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\
 \hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
 \hspace*{0pt}\\
-\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
-\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
-\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
-\hspace*{0pt} ~(if null xs then empty{\char95}queue\\
-\hspace*{0pt} ~~~else strict{\char95}dequeue (AQueue [] (reverse xs)));%
+\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Example.Queue a -> (a,~Example.Queue a);\\
+\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs (y :~ys)) = (y,~Example.AQueue xs ys);\\
+\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs []) =\\
+\hspace*{0pt} ~(if null xs then Example.empty{\char95}queue\\
+\hspace*{0pt} ~~~else Example.strict{\char95}dequeue (Example.AQueue [] (reverse xs)));%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r 371976383ac0 -r 352bcd845998 doc-src/Codegen/Thy/document/Further.tex
--- a/doc-src/Codegen/Thy/document/Further.tex	Thu Sep 02 16:53:23 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Further.tex	Thu Sep 02 17:01:49 2010 +0200
@@ -216,13 +216,13 @@
 \begin{isamarkuptext}%
 \isatypewriter%
 \noindent%
-\hspace*{0pt}funpow ::~forall a.~Nat -> (a -> a) -> a -> a;\\
-\hspace*{0pt}funpow Zero{\char95}nat f = id;\\
-\hspace*{0pt}funpow (Suc n) f = f .~funpow n f;\\
+\hspace*{0pt}funpow ::~forall a.~Example.Nat -> (a -> a) -> a -> a;\\
+\hspace*{0pt}funpow Example.Zero{\char95}nat f = id;\\
+\hspace*{0pt}funpow (Example.Suc n) f = f .~Example.funpow n f;\\
 \hspace*{0pt}\\
-\hspace*{0pt}funpows ::~forall a.~[Nat] -> (a -> a) -> a -> a;\\
+\hspace*{0pt}funpows ::~forall a.~[Example.Nat] -> (a -> a) -> a -> a;\\
 \hspace*{0pt}funpows [] = id;\\
-\hspace*{0pt}funpows (x :~xs) = funpow x .~funpows xs;%
+\hspace*{0pt}funpows (x :~xs) = Example.funpow x .~Example.funpows xs;%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -242,7 +242,7 @@
   specific application, you should consider \emph{Imperative
   Functional Programming with Isabelle/HOL}
   \cite{bulwahn-et-al:2008:imperative}; the framework described there
-  is available in session \hyperlink{theory.Imperative-HOL}{\mbox{\isa{Imperative{\isacharunderscore}HOL}}}.%
+  is available in session \isa{Imperative{\isacharunderscore}HOL}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r 371976383ac0 -r 352bcd845998 doc-src/Codegen/Thy/document/Refinement.tex
--- a/doc-src/Codegen/Thy/document/Refinement.tex	Thu Sep 02 16:53:23 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Refinement.tex	Thu Sep 02 17:01:49 2010 +0200
@@ -74,10 +74,11 @@
 \begin{isamarkuptext}%
 \isatypewriter%
 \noindent%
-\hspace*{0pt}fib ::~Nat -> Nat;\\
-\hspace*{0pt}fib Zero{\char95}nat = Zero{\char95}nat;\\
-\hspace*{0pt}fib (Suc Zero{\char95}nat) = Suc Zero{\char95}nat;\\
-\hspace*{0pt}fib (Suc (Suc n)) = plus{\char95}nat (fib n) (fib (Suc n));%
+\hspace*{0pt}fib ::~Example.Nat -> Example.Nat;\\
+\hspace*{0pt}fib Example.Zero{\char95}nat = Example.Zero{\char95}nat;\\
+\hspace*{0pt}fib (Example.Suc Example.Zero{\char95}nat) = Example.Suc Example.Zero{\char95}nat;\\
+\hspace*{0pt}fib (Example.Suc (Example.Suc n)) =\\
+\hspace*{0pt} ~Example.plus{\char95}nat (Example.fib n) (Example.fib (Example.Suc n));%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -172,15 +173,17 @@
 \begin{isamarkuptext}%
 \isatypewriter%
 \noindent%
-\hspace*{0pt}fib{\char95}step ::~Nat -> (Nat,~Nat);\\
-\hspace*{0pt}fib{\char95}step (Suc n) = let {\char123}\\
-\hspace*{0pt} ~~~~~~~~~~~~~~~~~~~~(m,~q) = fib{\char95}step n;\\
-\hspace*{0pt} ~~~~~~~~~~~~~~~~~~{\char125}~in (plus{\char95}nat m q,~m);\\
-\hspace*{0pt}fib{\char95}step Zero{\char95}nat = (Suc Zero{\char95}nat,~Zero{\char95}nat);\\
+\hspace*{0pt}fib{\char95}step ::~Example.Nat -> (Example.Nat,~Example.Nat);\\
+\hspace*{0pt}fib{\char95}step (Example.Suc n) =\\
+\hspace*{0pt} ~let {\char123}\\
+\hspace*{0pt} ~~~(m,~q) = Example.fib{\char95}step n;\\
+\hspace*{0pt} ~{\char125}~in (Example.plus{\char95}nat m q,~m);\\
+\hspace*{0pt}fib{\char95}step Example.Zero{\char95}nat =\\
+\hspace*{0pt} ~(Example.Suc Example.Zero{\char95}nat,~Example.Zero{\char95}nat);\\
 \hspace*{0pt}\\
-\hspace*{0pt}fib ::~Nat -> Nat;\\
-\hspace*{0pt}fib (Suc n) = fst (fib{\char95}step n);\\
-\hspace*{0pt}fib Zero{\char95}nat = Zero{\char95}nat;%
+\hspace*{0pt}fib ::~Example.Nat -> Example.Nat;\\
+\hspace*{0pt}fib (Example.Suc n) = fst (Example.fib{\char95}step n);\\
+\hspace*{0pt}fib Example.Zero{\char95}nat = Example.Zero{\char95}nat;%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -590,28 +593,30 @@
 \hspace*{0pt}\\
 \hspace*{0pt}newtype Dlist a = Dlist [a];\\
 \hspace*{0pt}\\
-\hspace*{0pt}empty ::~forall a.~Dlist a;\\
-\hspace*{0pt}empty = Dlist [];\\
+\hspace*{0pt}empty ::~forall a.~Example.Dlist a;\\
+\hspace*{0pt}empty = Example.Dlist [];\\
 \hspace*{0pt}\\
 \hspace*{0pt}member ::~forall a.~(Eq a) => [a] -> a -> Bool;\\
 \hspace*{0pt}member [] y = False;\\
-\hspace*{0pt}member (x :~xs) y = x == y || member xs y;\\
+\hspace*{0pt}member (x :~xs) y = x == y || Example.member xs y;\\
 \hspace*{0pt}\\
 \hspace*{0pt}inserta ::~forall a.~(Eq a) => a -> [a] -> [a];\\
-\hspace*{0pt}inserta x xs = (if member xs x then xs else x :~xs);\\
+\hspace*{0pt}inserta x xs = (if Example.member xs x then xs else x :~xs);\\
 \hspace*{0pt}\\
-\hspace*{0pt}list{\char95}of{\char95}dlist ::~forall a.~Dlist a -> [a];\\
-\hspace*{0pt}list{\char95}of{\char95}dlist (Dlist x) = x;\\
+\hspace*{0pt}list{\char95}of{\char95}dlist ::~forall a.~Example.Dlist a -> [a];\\
+\hspace*{0pt}list{\char95}of{\char95}dlist (Example.Dlist x) = x;\\
 \hspace*{0pt}\\
-\hspace*{0pt}insert ::~forall a.~(Eq a) => a -> Dlist a -> Dlist a;\\
-\hspace*{0pt}insert x dxs = Dlist (inserta x (list{\char95}of{\char95}dlist dxs));\\
+\hspace*{0pt}insert ::~forall a.~(Eq a) => a -> Example.Dlist a -> Example.Dlist a;\\
+\hspace*{0pt}insert x dxs =\\
+\hspace*{0pt} ~Example.Dlist (Example.inserta x (Example.list{\char95}of{\char95}dlist dxs));\\
 \hspace*{0pt}\\
 \hspace*{0pt}remove1 ::~forall a.~(Eq a) => a -> [a] -> [a];\\
 \hspace*{0pt}remove1 x [] = [];\\
-\hspace*{0pt}remove1 x (y :~xs) = (if x == y then xs else y :~remove1 x xs);\\
+\hspace*{0pt}remove1 x (y :~xs) = (if x == y then xs else y :~Example.remove1 x xs);\\
 \hspace*{0pt}\\
-\hspace*{0pt}remove ::~forall a.~(Eq a) => a -> Dlist a -> Dlist a;\\
-\hspace*{0pt}remove x dxs = Dlist (remove1 x (list{\char95}of{\char95}dlist dxs));\\
+\hspace*{0pt}remove ::~forall a.~(Eq a) => a -> Example.Dlist a -> Example.Dlist a;\\
+\hspace*{0pt}remove x dxs =\\
+\hspace*{0pt} ~Example.Dlist (Example.remove1 x (Example.list{\char95}of{\char95}dlist dxs));\\
 \hspace*{0pt}\\
 \hspace*{0pt}{\char125}%
 \end{isamarkuptext}%