--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2000/IsaMakefile Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,34 @@
+#
+# $Id$
+#
+# IsaMakefile for PSV2000
+#
+
+SESSIONS = a1
+
+## targets
+
+default: clean sessions
+sessions: $(SESSIONS)
+
+
+## global settings
+
+OUT = $(ISABELLE_OUTPUT)
+LOG = $(OUT)/log
+INFO = $(ISABELLE_BROWSER_INFO)
+USEDIR = $(ISATOOL) usedir -v true -i false -d false -D generated
+RSYNC = rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync
+
+
+clean:
+ rm -f $(LOG)/HOL-a?.gz $(LOG)/HOL-l?.gz
+
+## a1
+
+a1: a1/generated/session.tex
+
+a1/generated/session.tex: a1/ROOT.ML \
+ a1/*.thy
+ @$(USEDIR) HOL a1
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2000/a1/Arithmetic.thy Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,77 @@
+(*<*)
+theory Arithmetic = Main:;
+(*>*)
+
+subsection {* Arithmetic *}
+
+subsubsection {* Power *};
+
+text {* Define a primitive recursive function $pow~x~n$ that
+computes $x^n$ on natural numbers. *};
+
+consts
+ pow :: "nat => nat => nat";
+
+text {*
+Prove the well known equation $x^{m \cdot n} = (x^m)^n$:
+*};
+
+theorem pow_mult: "pow x (m * n) = pow (pow x m) n";
+(*<*)oops(*>*)
+
+text {* Hint: prove a suitable lemma first. If you need to appeal to
+associativity and commutativity of multiplication: the corresponding
+simplification rules are named @{text mult_ac}. *}
+
+subsubsection {* Summation *}
+
+text {*
+Define a (primitive recursive) function $sum~ns$ that sums a list
+of natural numbers: $sum [n_1, \dots, n_k] = n_1 + \cdots + n_k$.
+*}
+
+consts
+ sum :: "nat list => nat";
+
+text {*
+Show that $sum$ is compatible with $rev$. You may need a lemma.
+*}
+
+theorem sum_rev: "sum (rev ns) = sum ns"
+(*<*)oops(*>*)
+
+text {*
+Define a function $Sum~f~k$ that sums $f$ from $0$
+up to $k-1$: $Sum~f~k = f~0 + \cdots + f(k - 1)$.
+*};
+
+consts
+ Sum :: "(nat => nat) => nat => nat";
+
+text {*
+Show the following equations for the pointwise summation of functions.
+Determine first what the expression @{text whatever} should be.
+*};
+
+theorem "Sum (%i. f i + g i) k = Sum f k + Sum g k";
+(*<*)oops(*>*)
+
+theorem "Sum f (k + l) = Sum f k + Sum whatever l";
+(*<*)oops(*>*)
+
+text {*
+What is the relationship between @{term sum} and @{text Sum}?
+Prove the following equation, suitably instantiated.
+*};
+
+theorem "Sum f k = sum whatever";
+(*<*)oops(*>*)
+
+text {*
+Hint: familiarize yourself with the predefined functions @{term map} and
+@{term"[i..j(]"} on lists in theory List.
+*}
+
+(*<*)
+end
+(*>*)
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2000/a1/Hanoi.thy Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,46 @@
+(*<*)
+theory Hanoi = Main:
+(*>*)
+subsection {* The towers of Hanoi \label{psv2000hanoi} *}
+
+text {*
+
+We are given 3 pegs $A$, $B$ and $C$, and $n$ disks with a hole, such
+that no two disks have the same diameter. Initially all $n$ disks
+rest on peg $A$, ordered according to their size, with the largest one
+at the bottom. The aim is to transfer all $n$ disks from $A$ to $C$ by
+a sequence of single-disk moves such that we never place a larger disk
+on top of a smaller one. Peg $B$ may be used for intermediate storage.
+
+\begin{center}
+\includegraphics[width=0.8\textwidth]{Hanoi}
+\end{center}
+
+\medskip The pegs and moves can be modelled as follows:
+*};
+
+datatype peg = A | B | C
+types move = "peg * peg"
+
+text {*
+Define a primitive recursive function
+*};
+
+consts
+ moves :: "nat => peg => peg => peg => move list";
+
+text {* such that @{term moves}$~n~a~b~c$ returns a list of (legal)
+moves that transfer $n$ disks from peg $a$ via $b$ to $c$.
+Show that this requires $2^n - 1$ moves:
+*}
+
+theorem "length (moves n a b c) = 2^n - 1"
+(*<*)oops(*>*)
+
+text {* Hint: You need to strengthen the theorem for the
+induction to go through. Beware: subtraction on natural numbers
+behaves oddly: $n - m = 0$ if $n \le m$. *}
+
+(*<*)
+end
+(*>*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2000/a1/ROOT.ML Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,4 @@
+set quick_and_dirty;
+use_thy "Snoc";
+use_thy "Arithmetic";
+use_thy "Hanoi";
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2000/a1/Snoc.thy Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,27 @@
+(*<*)
+theory Snoc = Main:
+(*>*)
+subsection {* Lists *}
+
+text {*
+Define a primitive recursive function @{text snoc} that appends an element
+at the \emph{right} end of a list. Do not use @{text"@"} itself.
+*}
+
+consts
+ snoc :: "'a list => 'a => 'a list"
+
+text {*
+Prove the following theorem:
+*}
+
+theorem rev_cons: "rev (x # xs) = snoc (rev xs) x"
+(*<*)oops(*>*)
+
+text {*
+Hint: you need to prove a suitable lemma first.
+*}
+
+(*<*)
+end
+(*>*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2001/IsaMakefile Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,69 @@
+#
+# $Id$
+#
+# IsaMakefile for PSV2001
+#
+
+SESSIONS = a1 a2 a3 a5
+
+## targets
+
+default: clean sessions
+sessions: $(SESSIONS)
+# all: sessions
+
+
+## global settings
+
+
+SRC = $(ISABELLE_HOME)/src
+OUT = $(ISABELLE_OUTPUT)
+LOG = $(OUT)/log
+INFO = $(ISABELLE_BROWSER_INFO)
+USEDIR = $(ISATOOL) usedir -v true -i false -d false -D generated
+RSYNC = rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync
+WWW = www4.in.tum.de:/home/html/wbroy/html-data/lehre/praktika/psv
+
+
+# reomve old log files
+clean:
+ rm -f $(LOG)/HOL-a?.gz $(LOG)/HOL-l?.gz
+
+## provide style.tex
+
+style:
+ @for D in $(SESSIONS); do test -d $$D/document && { test -r $$D/document/style.tex || ln -s ../../style.tex $$D/document/style.tex; } done;
+
+
+## a1
+
+a1: a1/generated/session.tex
+
+a1/generated/session.tex: a1/ROOT.ML \
+ a1/*.thy
+ @$(USEDIR) HOL a1
+
+## a2
+
+a2: a2/generated/session.tex
+
+a2/generated/session.tex: a2/ROOT.ML \
+ a2/*.thy
+ @$(USEDIR) HOL a2
+
+## a3
+
+a3: a3/generated/session.tex
+
+a3/generated/session.tex: a3/ROOT.ML \
+ a3/*.thy
+ @$(USEDIR) HOL a3
+
+## a5
+
+a5: a5/generated/session.tex
+
+a5/generated/session.tex: a5/ROOT.ML \
+ a5/*.thy
+ @$(USEDIR) HOL a5
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2001/a1/Aufgabe1.thy Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,78 @@
+(*<*)
+theory Aufgabe1 = Main:
+(*>*)
+
+subsection {* Lists *}
+
+text{*
+Define a function @{term replace}, such that @{term"replace x y zs"}
+yields @{term zs} with every occurrence of @{term x} replaced by @{term y}.
+*}
+
+consts replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
+
+text {*
+Prove or disprove (by counter example) the following theorems.
+You may have to prove some lemmas first.
+*};
+
+theorem "rev(replace x y zs) = replace x y (rev zs)"
+(*<*)oops(*>*)
+
+theorem "replace x y (replace u v zs) = replace u v (replace x y zs)"
+(*<*)oops(*>*)
+
+theorem "replace y z (replace x y zs) = replace x z zs"
+(*<*)oops(*>*)
+
+text{* Define two functions for removing elements from a list:
+@{term"del1 x xs"} deletes the first occurrence (from the left) of
+@{term x} in @{term xs}, @{term"delall x xs"} all of them. *}
+
+consts del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
+ delall :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
+
+
+text {*
+Prove or disprove (by counter example) the following theorems.
+*};
+
+theorem "del1 x (delall x xs) = delall x xs"
+(*<*)oops(*>*)
+
+theorem "delall x (delall x xs) = delall x xs"
+(*<*)oops(*>*)
+
+theorem "delall x (del1 x xs) = delall x xs"
+(*<*)oops(*>*)
+
+theorem "del1 x (del1 y zs) = del1 y (del1 x zs)"
+(*<*)oops(*>*)
+
+theorem "delall x (del1 y zs) = del1 y (delall x zs)"
+(*<*)oops(*>*)
+
+theorem "delall x (delall y zs) = delall y (delall x zs)"
+(*<*)oops(*>*)
+
+theorem "del1 y (replace x y xs) = del1 x xs"
+(*<*)oops(*>*)
+
+theorem "delall y (replace x y xs) = delall x xs"
+(*<*)oops(*>*)
+
+theorem "replace x y (delall x zs) = delall x zs"
+(*<*)oops(*>*)
+
+theorem "replace x y (delall z zs) = delall z (replace x y zs)"
+(*<*)oops(*>*)
+
+theorem "rev(del1 x xs) = del1 x (rev xs)"
+(*<*)oops(*>*)
+
+theorem "rev(delall x xs) = delall x (rev xs)"
+(*<*)oops(*>*)
+
+(*<*)
+end
+(*>*)
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2001/a1/ROOT.ML Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,3 @@
+
+set quick_and_dirty;
+use_thy "Aufgabe1";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2001/a2/Aufgabe2.thy Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,72 @@
+(*<*)
+theory Aufgabe2 = Main:
+(*>*)
+
+subsection {* Trees *}
+
+text{* In the sequel we work with skeletons of binary trees where
+neither the leaves (``tip'') nor the nodes contain any information: *}
+
+datatype tree = Tp | Nd tree tree
+
+text{* Define a function @{term tips} that counts the tips of a
+tree, and a function @{term height} that computes the height of a
+tree.
+
+Complete binary trees of a given height are generated as follows:
+*}
+
+consts cbt :: "nat \<Rightarrow> tree"
+primrec
+"cbt 0 = Tp"
+"cbt(Suc n) = Nd (cbt n) (cbt n)"
+
+text{*
+We will now focus on these complete binary trees.
+
+Instead of generating complete binary trees, we can also \emph{test}
+if a binary tree is complete. Define a function @{term "iscbt f"}
+(where @{term f} is a function on trees) that checks for completeness:
+@{term Tp} is complete and @{term"Nd l r"} ist complete iff @{term l} and
+@{term r} are complete and @{prop"f l = f r"}.
+
+We now have 3 functions on trees, namely @{term tips}, @{term height}
+und @{term size}. The latter is defined automatically --- look it up
+in the tutorial. Thus we also have 3 kinds of completeness: complete
+wrt.\ @{term tips}, complete wrt.\ @{term height} and complete wrt.\
+@{term size}. Show that
+\begin{itemize}
+\item the 3 notions are the same (e.g.\ @{prop"iscbt tips t = iscbt size t"}),
+ and
+\item the 3 notions describe exactly the trees generated by @{term cbt}:
+the result of @{term cbt} is complete (in the sense of @{term iscbt},
+wrt.\ any function on trees), and if a tree is complete in the sense of
+@{term iscbt}, it is the result of @{term cbt} (applied to a suitable number
+--- which one?)
+\end{itemize}
+Find a function @{term f} such that @{prop"iscbt f"} is different from
+@{term"iscbt size"}.
+
+Hints:
+\begin{itemize}
+\item Work out and prove suitable relationships between @{term tips},
+ @{term height} und @{term size}.
+
+\item If you need lemmas dealing only with the basic arithmetic operations
+(@{text"+"}, @{text"*"}, @{text"^"} etc), you can ``prove'' them
+with the command @{text sorry}, if neither @{text arith} nor you can
+find a proof. Not @{text"apply sorry"}, just @{text sorry}.
+
+\item
+You do not need to show that every notion is equal to every other
+notion. It suffices to show that $A = C$ und $B = C$ --- $A = B$ is a
+trivial consequence. However, the difficulty of the proof will depend
+on which of the equivalences you prove.
+
+\item There is @{text"\<and>"} and @{text"\<longrightarrow>"}.
+\end{itemize}
+*}
+
+(*<*)
+end;
+(*>*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2001/a2/ROOT.ML Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,4 @@
+
+set quick_and_dirty;
+use_thy "Aufgabe2";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2001/a3/ROOT.ML Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,6 @@
+
+(* use "../settings.ML";*)
+set quick_and_dirty;
+use_thy "Trie1";
+use_thy "Trie2";
+use_thy "Trie3";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2001/a3/Trie1.thy Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,72 @@
+(*<*)
+theory Trie1 = Main:
+(*>*)
+
+subsection {* Tries *}
+
+text {* Section~3.4.4 of \cite{isabelle-tutorial} is a case study
+about so-called \emph{tries}, a data structure for fast indexing with
+strings. Read that section.
+
+The data type of tries over the alphabet type @{typ 'a} und the value
+type @{typ 'v} is defined as follows: *}
+
+datatype ('a, 'v) trie = Trie "'v option" "('a * ('a,'v) trie) list";
+
+text {* A trie consists of an optional value and an association list
+that maps letters of the alphabet to subtrees. Type @{typ "'a option"} is
+defined in section~2.5.3 of \cite{isabelle-tutorial}.
+
+There are also two selector functions @{term value} and @{term alist}: *}
+
+consts value :: "('a, 'v) trie \<Rightarrow> 'v option"
+primrec "value (Trie ov al) = ov";
+
+consts alist :: "('a, 'v) trie \<Rightarrow> ('a * ('a,'v) trie) list";
+primrec "alist (Trie ov al) = al";
+
+text {* Furthermore there is a function @{term lookup} on tries
+defined with the help of the generic search function @{term assoc} on
+association lists: *}
+
+consts assoc :: "('key * 'val)list \<Rightarrow> 'key \<Rightarrow> 'val option";
+primrec "assoc [] x = None"
+ "assoc (p#ps) x =
+ (let (a, b) = p in if a = x then Some b else assoc ps x)";
+
+consts lookup :: "('a, 'v) trie \<Rightarrow> 'a list \<Rightarrow> 'v option";
+primrec "lookup t [] = value t"
+ "lookup t (a#as) = (case assoc (alist t) a of
+ None \<Rightarrow> None
+ | Some at \<Rightarrow> lookup at as)";
+
+text {* Finally, @{term update} updates the value associated with some
+string with a new value, overwriting the old one: *}
+
+consts update :: "('a, 'v) trie \<Rightarrow> 'a list \<Rightarrow> 'v \<Rightarrow> ('a, 'v) trie";
+primrec
+ "update t [] v = Trie (Some v) (alist t)"
+ "update t (a#as) v =
+ (let tt = (case assoc (alist t) a of
+ None \<Rightarrow> Trie None []
+ | Some at \<Rightarrow> at)
+ in Trie (value t) ((a, update tt as v) # alist t))";
+
+text {* The following theorem tells us that @{term update} behaves as
+expected: *}
+
+theorem "\<forall>t v bs. lookup (update t as v) bs =
+ (if as = bs then Some v else lookup t bs)"
+(*<*)oops(*>*)
+
+text {* As a warming up exercise, define a function *}
+
+consts modify :: "('a, 'v) trie \<Rightarrow> 'a list \<Rightarrow> 'v option \<Rightarrow> ('a, 'v) trie"
+
+text{* for inserting as well as deleting elements from a trie. Show
+that @{term modify} satisfies a suitably modified version of the
+correctness theorem for @{term update}. *}
+
+(*<*)
+end;
+(*>*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2001/a3/Trie2.thy Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,26 @@
+(*<*)
+theory Trie2 = Main:
+(*>*)
+
+text {* Die above definition of @{term update} has the disadvantage
+that it often creates junk: each association list it passes through is
+extended at the left end with a new (letter,value) pair without
+removing any old association of that letter which may already be
+present. Logically, such cleaning up is unnecessary because @{term
+assoc} always searches the list from the left. However, it constitutes
+a space leak: the old associations cannot be garbage collected because
+physically they are still reachable. This problem can be solved by
+means of a function *}
+
+consts overwrite :: "'a \<Rightarrow> 'b \<Rightarrow> ('a * 'b) list \<Rightarrow> ('a * 'b) list"
+
+text {* that does not just add new pairs at the front but replaces old
+associations by new pairs if possible.
+
+Define @{term overwrite}, modify @{term modify} to employ @{term
+overwrite}, and show the same relationship between @{term modify} and
+@{term lookup} as before. *}
+
+(*<*)
+end;
+(*>*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2001/a3/Trie3.thy Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,19 @@
+(*<*)
+theory Trie3 = Main:
+(*>*)
+
+text {* Instead of association lists we can also use partial functions
+that map letters to subtrees. Partiality can be modelled with the help
+of type @{typ "'a option"}: if @{term f} is a function of type
+\mbox{@{typ "'a \<Rightarrow> 'b option"}}, set @{term "f a = Some b"}
+if @{term a} should be mapped to some @{term b} and set @{term "f a =
+None"} otherwise. *}
+
+datatype ('a, 'v) trie = Trie "'v option" "'a \<Rightarrow> ('a,'v) trie option";
+
+text{* Modify the definitions of @{term lookup} and @{term modify}
+accordingly and show the same correctness theorem as above. *}
+
+(*<*)
+end;
+(*>*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2001/a5/Aufgabe5.thy Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,127 @@
+(*<*)
+theory Aufgabe5 = Main:
+(*>*)
+
+subsection {* Interval lists *}
+
+
+text {* Sets of natural numbers can be implemented as lists of
+intervals, where an interval is simply a pair of numbers. For example
+the set @{term "{2, 3, 5, 7, 8, 9::nat}"} can be represented by the
+list @{term "[(2, 3), (5, 5), (7::nat,9::nat)]"}. A typical application
+is the list of free blocks of dynamically allocated memory. *}
+
+subsubsection {* Definitions *}
+
+text {* We introduce the type *}
+
+types intervals = "(nat*nat) list"
+
+text {* This type contains all possible lists of pairs of natural
+numbers, even those that we may not recognize as meaningful
+representations of sets. Thus you should introduce an \emph{invariant} *}
+
+consts inv :: "intervals => bool"
+
+text {* that characterizes exactly those interval lists representing
+sets. (The reason why we call this an invariant will become clear
+below.) For efficiency reasons intervals should be sorted in
+ascending order, the lower bound of each interval should be less or
+equal the upper bound, and the intervals should be chosen as large as
+possible, i.e.\ no two adjecent intervals should overlap or even touch
+each other. It turns out to be convenient to define @{term inv} in
+terms of a more general function *}
+
+consts inv2 :: "nat => intervals => bool"
+
+text {* such that the additional argument is a lower bound for the
+intervals in the list.
+
+To relate intervals back to sets define an \emph{abstraktion funktion} *}
+
+consts set_of :: "intervals => nat set"
+
+text {* that yields the set corresponding to an interval list (that
+satisfies the invariant).
+
+Finally, define two primitive recursive functions
+*}
+
+consts add :: "(nat*nat) => intervals => intervals"
+ rem :: "(nat*nat) => intervals => intervals"
+
+text {* for inserting and deleting an interval from an interval
+list. The result should again satisfies the invariant. Hence the name:
+@{text inv} is invariant under the application of the operations
+@{term add} and @{term rem} --- if @{text inv} holds for the input, it
+must also hold for the output.
+*}
+
+subsubsection {* Proving the invariant *}
+
+declare Let_def [simp]
+declare split_split [split]
+
+text {* Start off by proving the monotonicity of @{term inv2}: *}
+
+lemma inv2_monotone: "inv2 m ins \<Longrightarrow> n\<le>m \<Longrightarrow> inv2 n ins"
+(*<*)oops(*>*)
+
+text {*
+Now show that @{term add} and @{term rem} preserve the invariant:
+*}
+
+theorem inv_add: "\<lbrakk> i\<le>j; inv ins \<rbrakk> \<Longrightarrow> inv (add (i,j) ins)"
+(*<*)oops(*>*)
+
+theorem inv_rem: "\<lbrakk> i\<le>j; inv ins \<rbrakk> \<Longrightarrow> inv (rem (i,j) ins)"
+(*<*)oops(*>*)
+
+text {* Hint: you should first prove a more general statement
+(involving @{term inv2}). This will probably involve some advanced
+forms of induction discussed in section~9.3.1 of
+\cite{isabelle-tutorial}. *}
+
+
+subsubsection {* Proving correctness of the implementation *}
+
+text {* Show the correctness of @{term add} and @{term rem} wrt.\
+their counterparts @{text"\<union>"} and @{text"-"} on sets: *}
+
+theorem set_of_add:
+ "\<lbrakk> i\<le>j; inv ins \<rbrakk> \<Longrightarrow> set_of (add (i,j) ins) = set_of [(i,j)] \<union> set_of ins"
+(*<*)oops(*>*)
+
+theorem set_of_rem:
+ "\<lbrakk> i \<le> j; inv ins \<rbrakk> \<Longrightarrow> set_of (rem (i,j) ins) = set_of ins - set_of [(i,j)]"
+(*<*)oops(*>*)
+
+text {* Hints: in addition to the hints above, you may also find it
+useful to prove some relationship between @{term inv2} and @{term
+set_of} as a lemma. *}
+
+subsubsection{* General hints *}
+
+text {*
+\begin{itemize}
+
+\item You should be familiar both with simplification and predicate
+calculus reasoning. Automatic tactics like @{text blast} and @{text
+force} can simplify the proof.
+
+\item
+Equality of two sets can often be proved via the rule @{text set_ext}:
+@{thm[display] set_ext[of A B,no_vars]}
+
+\item
+Potentially useful theorems for the simplification of sets include \\
+@{text "Un_Diff:"}~@{thm Un_Diff [no_vars]} \\
+@{text "Diff_triv:"}~@{thm Diff_triv [no_vars]}.
+
+\item
+Theorems can be instantiated and simplified via @{text of} and
+@{text "[simplified]"} (see \cite{isabelle-tutorial}).
+\end{itemize}
+*}(*<*)
+end
+(*>*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2001/a5/ROOT.ML Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,2 @@
+use_thy "Aufgabe5";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2002/IsaMakefile Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,76 @@
+#
+# $Id$
+#
+# IsaMakefile for PSV2002
+#
+
+SESSIONS = a1 a2 a3 a5 a6
+
+## targets
+
+default: clean sessions
+sessions: $(SESSIONS)
+# all: sessions
+
+
+## global settings
+
+
+SRC = $(ISABELLE_HOME)/src
+OUT = $(ISABELLE_OUTPUT)
+LOG = $(OUT)/log
+INFO = $(ISABELLE_BROWSER_INFO)
+USEDIR = $(ISATOOL) usedir -v true -i false -d false -D generated
+RSYNC = rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync
+WWW = www4.in.tum.de:/home/html/wbroy/html-data/lehre/praktika/psv
+
+
+# reomve old log files
+clean:
+ rm -f $(LOG)/HOL-a?.gz $(LOG)/HOL-l?.gz
+
+## provide style.tex
+
+style:
+ @for D in $(SESSIONS); do test -d $$D/document && { test -r $$D/document/style.tex || ln -s ../../style.tex $$D/document/style.tex; } done;
+
+
+## a1
+
+a1: a1/generated/session.tex
+
+a1/generated/session.tex: a1/ROOT.ML \
+ a1/*.thy
+ @$(USEDIR) HOL a1
+
+## a2
+
+a2: a2/generated/session.tex
+
+a2/generated/session.tex: a2/ROOT.ML \
+ a2/*.thy
+ @$(USEDIR) HOL a2
+
+## a3
+
+a3: a3/generated/session.tex
+
+a3/generated/session.tex: a3/ROOT.ML \
+ a3/*.thy
+ @$(USEDIR) HOL a3
+
+## a5
+
+a5: a5/generated/session.tex
+
+a5/generated/session.tex: a5/ROOT.ML \
+ a5/*.thy
+ @$(USEDIR) HOL a5
+
+## a6
+
+a6: a6/generated/session.tex
+
+a6/generated/session.tex: a6/ROOT.ML \
+ a6/*.thy
+ @$(USEDIR) HOL a6
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2002/a1/ROOT.ML Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,1 @@
+ use_thy "a1";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2002/a1/a1.thy Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,74 @@
+(*<*)
+theory a1 = Main:
+(*>*)
+subsection {* Lists *}
+
+text {* Define a universal and an existential quantifier on lists.
+Expression @{term "alls P xs"} should be true iff @{term "P x"} holds
+for every element @{term x} of @{term xs}, and @{term "exs P xs"}
+should be true iff @{term "P x"} holds for some element @{term x} of
+@{term xs}.
+*}
+consts
+ alls :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
+ exs :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
+
+text {*
+Prove or disprove (by counter example) the following theorems.
+You may have to prove some lemmas first.
+
+Use the @{text "[simp]"}-attribute only if the equation is truly a
+simplification and is necessary for some later proof.
+*}
+
+lemma "alls (\<lambda>x. P x \<and> Q x) xs = (alls P xs \<and> alls Q xs)"
+(*<*)oops(*>*)
+
+lemma "alls P (rev xs) = alls P xs"
+(*<*)oops(*>*)
+
+lemma "exs (\<lambda>x. P x \<and> Q x) xs = (exs P xs \<and> exs Q xs)"
+(*<*)oops(*>*)
+
+lemma "exs P (map f xs) = exs (P o f) xs"
+(*<*)oops(*>*)
+
+lemma "exs P (rev xs) = exs P xs"
+(*<*)oops(*>*)
+
+text {* Find a term @{text Z} such that the following equation holds: *}
+lemma "exs (\<lambda>x. P x \<or> Q x) xs = Z"
+(*<*)oops(*>*)
+
+text {* Express the existential via the universal quantifier ---
+@{text exs} should not occur on the right-hand side: *}
+lemma "exs P xs = Z"
+(*<*)oops(*>*)
+
+text {*
+Define a function @{term "is_in x xs"} that checks if @{term x} occurs in
+@{term xs} vorkommt. Now express @{text is_in} via @{term exs}:
+*}
+lemma "is_in a xs = Z"
+(*<*)oops(*>*)
+
+text {* Define a function @{term "nodups xs"} that is true iff
+@{term xs} does not contain duplicates, and a function @{term "deldups
+xs"} that removes all duplicates. Note that @{term "deldups[x,y,x]"}
+(where @{term x} and @{term y} are distinct) can be either
+@{term "[x,y]"} or @{term "[y,x]"}.
+
+Prove or disprove (by counter example) the following theorems.
+*}
+lemma "length (deldups xs) <= length xs"
+(*<*)oops(*>*)
+
+lemma "nodups (deldups xs)"
+(*<*)oops(*>*)
+
+lemma "deldups (rev xs) = rev (deldups xs)"
+(*<*)oops(*>*)
+
+(*<*)
+end
+(*>*)
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2002/a2/ROOT.ML Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,1 @@
+use_thy "a2";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2002/a2/a2.thy Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,113 @@
+(*<*)
+theory a2 = Main:
+(*>*)
+subsection {* Sorting \label{psv2002a2} *}
+
+text{* For simplicity we sort natural numbers. *}
+
+subsubsection{* Sorting with lists*}
+
+text {*
+The task is to define insertion sort and prove its correctness.
+The following functions are required:
+*}
+
+consts
+ insort :: "nat \<Rightarrow> nat list \<Rightarrow> nat list"
+ sort :: "nat list \<Rightarrow> nat list"
+ le :: "nat \<Rightarrow> nat list \<Rightarrow> bool"
+ sorted :: "nat list \<Rightarrow> bool"
+
+text {* In your definition, @{term "insort x xs"} should insert a
+number @{term x} into an already sorted list @{text xs}, and @{term
+"sort ys"} should build on @{text insort} to produce the sorted
+version of @{text ys}.
+
+To show that the resulting list is indeed sorted we need a predicate
+@{term sorted} that checks if each element in the list is less or equal
+to the following ones; @{term "le n xs"} should be true iff
+@{term n} is less or equal to all elements of @{text xs}.
+
+Start out by showing a monotonicity property of @{term le}.
+For technical reasons the lemma should be phrased as follows:
+*}
+lemma [simp]: "x \<le> y \<Longrightarrow> le y xs \<longrightarrow> le x xs"
+(*<*)oops(*>*)
+
+text {* Now show the following correctness theorem: *}
+theorem "sorted (sort xs)"
+(*<*)oops(*>*)
+
+text {* This theorem alone is too weak. It does not guarantee that the
+sorted list contains the same elements as the input. In the worst
+case, @{term sort} might always return @{term"[]"} --- surely an
+undesirable implementation of sorting.
+
+Define a function @{term "count xs x"} that counts how often @{term x}
+occurs in @{term xs}. Show that
+*}
+
+theorem "count (sort xs) x = count xs x"
+(*<*)oops(*>*)
+
+subsubsection {* Sorting with trees *}
+
+text {* Our second sorting algorithm uses trees. Thus you should first
+define a data type @{text bintree} of binary trees that are either
+empty or consist of a node carrying a natural number and two subtrees.
+
+Define a function @{text tsorted} that checks if a binary tree is
+sorted. It is convenien to employ two auxiliary functions @{text
+tge}/@{text tle} that test whether a number is
+greater-or-equal/less-or-equal to all elements of a tree.
+
+Finally define a function @{text tree_of} that turns a list into a
+sorted tree. It is helpful to base @{text tree_of} on a function
+@{term "ins n b"} that inserts a number @{term n} into a sorted tree
+@{term b}.
+
+Show
+*}
+theorem [simp]: "tsorted (tree_of xs)"
+(*<*)oops(*>*)
+
+text {* Again we have to show that no elements are lost (or added).
+As for lists, define a function @{term "tcount x b"} that counts the
+number of occurrences of the number @{term x} in the tree @{term b}.
+Show
+*}
+
+theorem "tcount (tree_of xs) x = count xs x"
+(*<*)oops(*>*)
+
+text {* Now we are ready to sort lists. We know how to produce an
+ordered tree from a list. Thus we merely need a function @{text
+list_of} that turns an (ordered) tree into an (ordered) list.
+Define this function and prove
+*}
+
+theorem "sorted (list_of (tree_of xs))"
+(*<*)oops(*>*)
+
+theorem "count (list_of (tree_of xs)) n = count xs n"
+(*<*)oops(*>*)
+
+text {*
+Hints:
+\begin{itemize}
+\item
+Try to formulate all your lemmas as equations rather than implications
+because that often simplifies their proof.
+Make sure that the right-hand side is (in some sense)
+simpler than the left-hand side.
+\item
+Eventually you need to relate @{text sorted} and @{text tsorted}.
+This is facilitated by a function @{text ge} on lists (analogously to
+@{text tge} on trees) and the following lemma (that you will need to prove):
+@{term[display] "sorted (a@x#b) = (sorted a \<and> sorted b \<and> ge x a \<and> le x b)"}
+\end{itemize}
+*}
+
+(*<*)
+end
+(*>*)
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2002/a3/ROOT.ML Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,1 @@
+ use_thy "a3";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2002/a3/a3.thy Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,43 @@
+(*<*)
+theory a3 = Main:
+(*>*)
+
+subsection{* Compilation *}
+
+text {* This exercise deals with the compiler example in section~3.3
+of \cite{isabelle-tutorial}. The simple side effect free expressions
+are extended with side effects.
+\begin{enumerate}
+
+\item Read sections 3.3 and 8.2 of \cite{isabelle-tutorial}. Study
+the section about @{text fun_upd} in theory @{text Fun} of HOL:
+@{text"fun_upd f x y"}, written @{text"f(x:=y)"}, is @{text f}
+updated at @{text x} with new value @{text y}.
+
+\item Extend data type @{text "('a, 'v) expr"} with a new alternative
+@{text "Assign x e"} that shall represent an assignment @{text "x =
+e"} of the value of the expression @{text e} to the variable @{text x}.
+The value of an assignment shall be the value of @{text e}.
+
+\item Modify the evaluation function @{text value} such that it can
+deal with assignments. Note that since the evaluation of an expression
+may now change the environment, it no longer suffices to return only
+the value from the evaluation of an expression.
+
+Define a function @{text "se_free :: expr \<Rightarrow> bool"} that
+identifies side effect free expressions. Show that @{text "se_free e"}
+implies that evaluation of @{text e} does not change the environment.
+
+\item Extend data type @{text "('a, 'v) instr"} with a new instruction
+@{text "Store x"} that stores the topmost element on the stack in
+address/variable @{text x}, without removing it from the stack.
+Update the machine semantics @{text exec} accordingly. You will face
+the same problem as in the extension of @{text value}.
+
+\item Modify the compiler @{text comp} and its correctness proof to
+accommodate the above changes.
+\end{enumerate}
+*}
+(*<*)
+end
+(*>*)
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2002/a5/ROOT.ML Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,1 @@
+use_thy "a5";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2002/a5/a5.thy Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,45 @@
+(*<*)
+theory a5 = Main:
+(*>*)
+
+subsection {* Merge sort *}
+
+text {* Implement \emph{merge sort}: a list is sorted by splitting it
+into two lists, sorting them separately, and merging the results.
+
+With the help of @{text recdef} define two functions
+*}
+
+consts merge :: "nat list \<times> nat list \<Rightarrow> nat list"
+ msort :: "nat list \<Rightarrow> nat list"
+
+text {* and show *}
+
+theorem "sorted (msort xs)"
+(*<*)oops(*>*)
+
+theorem "count (msort xs) x = count xs x"
+(*<*)oops(*>*)
+
+text {* where @{term sorted} and @{term count} are defined as in
+section~\ref{psv2002a2}.
+
+Hints:
+\begin{itemize}
+\item For @{text recdef} see section~3.5 of \cite{isabelle-tutorial}.
+
+\item To split a list into two halves of almost equal length you can
+use the functions \mbox{@{text "n div 2"}}, @{term take} und @{term drop},
+where @{term "take n xs"} returns the first @{text n} elements of
+@{text xs} and @{text "drop n xs"} the remainder.
+
+\item Here are some potentially useful lemmas:\\
+ @{text "linorder_not_le:"} @{thm linorder_not_le [no_vars]}\\
+ @{text "order_less_le:"} @{thm order_less_le [no_vars]}\\
+ @{text "min_def:"} @{thm min_def [no_vars]}
+\end{itemize}
+*}
+
+(*<*)
+end
+(*>*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2002/a5/l2.thy Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,307 @@
+theory l2 = Main:
+
+text {*
+ \section*{Sortieren auf Listen}
+
+ Der erste Teil des Blattes beschäftigt sich mit einem
+ einfachen Sortieralgorithmus auf Listen von natürlichen Zahlen.
+ Ihre Aufgabe ist es, den Sortieralgorithmus in Isabelle zu
+ programmieren und zu zeigen, dass Ihre Implementierung korrekt ist.
+
+ Der Algorithmus lässt sich in folgende Funktionen zerlegen:
+*}
+consts
+ insort :: "nat \<Rightarrow> nat list \<Rightarrow> nat list"
+ sort :: "nat list \<Rightarrow> nat list"
+ le :: "nat \<Rightarrow> nat list \<Rightarrow> bool"
+ sorted :: "nat list \<Rightarrow> bool"
+text {*
+ Hierbei soll @{term "insort x xs"} eine Zahl @{term x} in eine
+ sortierte Liste @{text xs} einfügen, und die Funktion @{term "sort ys"}
+ (aufbauend auf @{text insort}) die sortierte Version von @{text ys}
+ liefern.
+
+ Um zu zeigen, dass die resultierende Liste tatsächlich sortiert
+ ist, benötigen sie das Prädikat @{term "sorted xs"}, das überprüft
+ ob jedes Element der Liste kleiner ist als alle folgenden Elemente
+ der Liste. Die Funktion @{term "le n xs"} soll genau dann wahr sein,
+ wenn @{term n} kleiner oder gleich allen Elementen von @{text xs}
+ ist.
+*}
+primrec
+ "le a [] = True"
+ "le a (x#xs) = (a <= x & le a xs)"
+
+primrec
+ "sorted [] = True"
+ "sorted (x#xs) = (le x xs & sorted xs)"
+
+primrec
+ "insort a [] = [a]"
+ "insort a (x#xs) = (if a <= x then a#x#xs else x # insort a xs)"
+
+primrec
+ "sort [] = []"
+ "sort (x#xs) = insort x (sort xs)"
+
+lemma "le 3 [7,10,3]" by auto
+
+lemma "\<not> le 3 [7,10,2]" by auto
+
+lemma "sorted [1,2,3,4]" by auto
+
+lemma "\<not> sorted [3,1,4,2]" by auto
+
+lemma "sort [3,1,4,2] = [1,2,3,4]" by auto
+
+text {*
+ Zeigen Sie zu Beginn folgendes Monotonie-Lemma über @{term le}. Die
+ Formulierung des Lemmas ist aus technischen Gründen (über die sie
+ später mehr erfahren werden) etwas ungewohnt:
+*}
+lemma [simp]: "x \<le> y \<Longrightarrow> le y xs \<longrightarrow> le x xs"
+ apply (induct_tac xs)
+ apply auto
+ done
+
+lemma [simp]:
+ "le x (insort a xs) = (x <= a & le x xs)"
+ apply (induct_tac xs)
+ apply auto
+ done
+
+lemma [simp]:
+ "sorted (insort a xs) = sorted xs"
+ apply (induct_tac xs)
+ apply auto
+ done
+
+theorem "sorted (sort xs)"
+ apply (induct_tac xs)
+ apply auto
+ done
+
+text {*
+ Das Theorem sagt zwar aus, dass Ihr Algorithmus eine sortierte
+ Liste zurückgibt, es gibt Ihnen aber nicht die Sicherheit, dass die sortierte
+ Liste auch die gleichen Elemente wie das Original enthält. Formulieren Sie deswegen
+ eine Funktion @{term "count xs x"}, die zählt, wie oft die Zahl
+ @{term x} in @{term xs} vorkommt.
+*}
+consts
+ count :: "nat list => nat => nat"
+primrec
+ "count [] y = 0"
+ "count (x#xs) y = (if x=y then Suc(count xs y) else count xs y)"
+
+lemma "count [2,3,1,3] 3 = 2" by auto
+
+lemma "count [2,3,1,3] 7 = 0" by auto
+
+lemma "count [2,3,1,3] 2 = 1" by auto
+
+lemma [simp]:
+ "count (insort x xs) y =
+ (if x=y then Suc (count xs y) else count xs y)"
+ apply (induct_tac xs)
+ apply auto
+ done
+
+theorem "count (sort xs) x = count xs x"
+ apply (induct_tac xs)
+ apply auto
+ done
+
+text {*
+ \section*{Sortieren mit Bäumen}
+
+ Der zweite Teil des Blattes beschäftigt sich mit einem
+ Sortieralgorithmus, der Bäume verwendet.
+ Definieren Sie dazu zuerst den Datentyp @{text bintree} der
+ Binärbäume. Für diese Aufgabe sind Binärbäume entweder leer, oder
+ bestehen aus einem
+ Knoten mit einer natürlichen Zahl und zwei Unterbäumen.
+
+ Schreiben Sie dann eine Funktion @{text tsorted}, die feststellt, ob
+ ein Binärbaum geordnet ist. Sie werden dazu zwei Hilfsfunktionen
+ @{text tge} und @{text tle} benötigen, die überprüfen ob eine Zahl
+ grössergleich/kleinergleich als alle Elemente eines Baumes sind.
+
+ Formulieren Sie schliesslich eine Funktion @{text tree_of}, die zu einer
+ (unsortierten) Liste den geordneten Binärbaum zurückgibt. Stützen Sie
+ sich dabei auf eine Funktion @{term "ins n b"}, die eine Zahl @{term
+ n} in einen geordneten Binärbaum @{term b} einfügt.
+*}
+
+datatype bintree = Empty | Node nat bintree bintree
+
+consts
+ tsorted :: "bintree \<Rightarrow> bool"
+ tge :: "nat \<Rightarrow> bintree \<Rightarrow> bool"
+ tle :: "nat \<Rightarrow> bintree \<Rightarrow> bool"
+ ins :: "nat \<Rightarrow> bintree \<Rightarrow> bintree"
+ tree_of :: "nat list \<Rightarrow> bintree"
+
+primrec
+ "tsorted Empty = True"
+ "tsorted (Node n t1 t2) = (tsorted t1 \<and> tsorted t2 \<and> tge n t1 \<and> tle n t2)"
+
+primrec
+ "tge x Empty = True"
+ "tge x (Node n t1 t2) = (n \<le> x \<and> tge x t1 \<and> tge x t2)"
+
+primrec
+ "tle x Empty = True"
+ "tle x (Node n t1 t2) = (x \<le> n \<and> tle x t1 \<and> tle x t2)"
+
+primrec
+ "ins x Empty = Node x Empty Empty"
+ "ins x (Node n t1 t2) = (if x \<le> n then Node n (ins x t1) t2 else Node n t1 (ins x t2))"
+
+primrec
+ "tree_of [] = Empty"
+ "tree_of (x#xs) = ins x (tree_of xs)"
+
+
+lemma "tge 5 (Node 3 (Node 2 Empty Empty) Empty)" by auto
+
+lemma "\<not> tge 5 (Node 3 Empty (Node 7 Empty Empty))" by auto
+
+lemma "\<not> tle 5 (Node 3 (Node 2 Empty Empty) Empty)" by auto
+
+lemma "\<not> tle 5 (Node 3 Empty (Node 7 Empty Empty))" by auto
+
+lemma "tle 3 (Node 3 Empty (Node 7 Empty Empty))" by auto
+
+lemma "tsorted (Node 3 Empty (Node 7 Empty Empty))" by auto
+
+lemma "tree_of [3,2] = Node 2 Empty (Node 3 Empty Empty)" by auto
+
+lemma [simp]:
+ "tge a (ins x t) = (x \<le> a \<and> tge a t)"
+ apply (induct_tac t)
+ apply auto
+ done
+
+lemma [simp]:
+ "tle a (ins x t) = (a \<le> x \<and> tle a t)"
+ apply (induct_tac t)
+ apply auto
+ done
+
+lemma [simp]:
+ "tsorted (ins x t) = tsorted t"
+ apply (induct_tac t)
+ apply auto
+ done
+
+theorem [simp]: "tsorted (tree_of xs)"
+ apply (induct_tac xs)
+ apply auto
+ done
+
+text {*
+ Auch bei diesem Algorithmus müssen wir noch zeigen, dass keine
+ Elemente beim Sortieren verloren gehen (oder erfunden werden). Formulieren
+ Sie analog zu den Listen eine Funktion @{term "tcount x b"}, die zählt, wie
+ oft die Zahl @{term x} im Baum @{term b} vorkommt.
+*}
+consts
+ tcount :: "bintree => nat => nat"
+primrec
+ "tcount Empty y = 0"
+ "tcount (Node x t1 t2) y =
+ (if x=y
+ then Suc (tcount t1 y + tcount t2 y)
+ else tcount t1 y + tcount t2 y)"
+
+lemma [simp]:
+ "tcount (ins x t) y =
+ (if x=y then Suc (tcount t y) else tcount t y)"
+ apply(induct_tac t)
+ apply auto
+ done
+
+theorem "tcount (tree_of xs) x = count xs x"
+ apply (induct_tac xs)
+ apply auto
+ done
+
+text {*
+ Die eigentliche Aufgabe war es, Listen zu sortieren. Bis jetzt haben
+ wir lediglich einen Algorithmus, der Listen in geordnete Bäume
+ transformiert. Definieren Sie deswegen eine Funktion @{text
+ list_of}, die zu einen (geordneten) Baum eine (geordnete) Liste liefert.
+*}
+
+consts
+ ge :: "nat \<Rightarrow> nat list \<Rightarrow> bool"
+ list_of :: "bintree \<Rightarrow> nat list"
+
+primrec
+ "ge a [] = True"
+ "ge a (x#xs) = (x \<le> a \<and> ge a xs)"
+
+primrec
+ "list_of Empty = []"
+ "list_of (Node n t1 t2) = list_of t1 @ [n] @ list_of t2"
+
+
+lemma [simp]:
+ "le x (a@b) = (le x a \<and> le x b)"
+ apply (induct_tac a)
+ apply auto
+ done
+
+lemma [simp]:
+ "ge x (a@b) = (ge x a \<and> ge x b)"
+ apply (induct_tac a)
+ apply auto
+ done
+
+lemma [simp]:
+ "sorted (a@x#b) = (sorted a \<and> sorted b \<and> ge x a \<and> le x b)"
+ apply (induct_tac a)
+ apply auto
+ done
+
+lemma [simp]:
+ "ge n (list_of t) = tge n t"
+ apply (induct_tac t)
+ apply auto
+ done
+
+lemma [simp]:
+ "le n (list_of t) = tle n t"
+ apply (induct_tac t)
+ apply auto
+ done
+
+lemma [simp]:
+ "sorted (list_of t) = tsorted t"
+ apply (induct_tac t)
+ apply auto
+ done
+
+theorem "sorted (list_of (tree_of xs))"
+ apply auto
+ done
+
+lemma count_append [simp]:
+ "count (a@b) n = count a n + count b n"
+ apply (induct a)
+ apply auto
+ done
+
+lemma [simp]:
+ "count (list_of b) n = tcount b n"
+ apply (induct b)
+ apply auto
+ done
+
+theorem "count (list_of (tree_of xs)) n = count xs n"
+ apply (induct xs)
+ apply auto
+ done
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2002/a6/ROOT.ML Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,1 @@
+ use_thy "a6";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2002/a6/a6.thy Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,24 @@
+(*<*)
+theory a6 = Main:
+(*>*)
+subsection {* The towers of Hanoi *}
+
+text{*
+In section \ref{psv2000hanoi} we introduced the towers of Hanoi and
+defined a function @{term moves} to generate the moves to solve the
+puzzle. Now it is time to show that @{term moves} is correct. This
+means that
+\begin{itemize}
+\item when executing the list of moves, the result is indeed the
+intended one, i.e.\ all disks are moved from one peg to another, and
+\item all of the moves are legal, i.e.\ never place a larger disk
+on top of a smaller one.
+\end{itemize}
+Hint: this is a nontrivial undertaking. The complexity of your proofs
+will depend crucially on your choice of model and you may have to
+revise your model as you proceed with the proof.
+*}
+
+(*<*)
+end
+(*>*)
\ No newline at end of file
Binary file doc-src/Exercises/Hanoi.pdf has changed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/Makefile Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,24 @@
+all: gen tex
+
+gen: g2000 g2001 g2002
+
+tex:
+ pdflatex exercises
+ bibtex exercises
+ pdflatex exercises
+ pdflatex exercises
+
+g2000:
+ cd 2000; isatool make
+
+g2001:
+ cd 2001; isatool make
+
+g2002:
+ cd 2002; isatool make
+
+clean:
+ rm -f *.log *.aux *.bbl *.blg *.toc *.out *~
+
+realclean: clean
+ rm -rf exercises.pdf */*/generated
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/exercises.bib Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,85 @@
+@string{LNCS="Lect.\ Notes in Comp.\ Sci."}
+@string{FAC="Formal Aspects of Computing"}
+
+@Book{Tanenbaum,
+ author = {Andrew S. Tanenbaum},
+ title = {Modern Operating Systems},
+ publisher = {Prentice-Hall},
+ year = 1992
+}
+
+@Misc{Unix-heritage,
+ key = {Unix},
+ title = {The {Unix} Heritage Society},
+ note = {\\ \url{http://www.tuhs.org/}}
+}
+
+@Book{Broy-PartI,
+ author = {M. Broy},
+ title = {Informatik --- Eine grundlegende Einf{\"u}hrung
+ (Teil I)},
+ publisher = {Springer},
+ year = 1992
+}
+
+@Book{Huth-Ryan:2000,
+ author = {M. R. A Huth and M. D. Ryan},
+ title = {Logic in Computer Science --- Modelling and
+ reasoning about systems},
+ publisher = {Cambridge University Press},
+ year = 2000,
+ note = {\\ \url{http://www.cs.bham.ac.uk/research/lics/}}
+}
+
+@Misc{Wenzel:2000:Hoare,
+ author = {Markus Wenzel},
+ title = {A formulation of {H}oare {L}ogic in {I}sabelle/{I}sar},
+ month = {June},
+ year = 2000,
+ note = {\\ \url{http://www4.in.tum.de/~wenzelm/papers/Hoare-Isar.pdf}}
+}
+
+@Misc{Naraschewski-Wenzel:1998:HOOL,
+author={Wolfgang Naraschewski and Markus Wenzel},
+title=
+{Object-Oriented Verification based on Record Subtyping in Higher-Order Logic},
+booktitle={Theorem Proving in Higher Order Logics:
+11th International Conference, TPHOLs'98},
+publisher={Springer},volume=1479,series=LNCS,year=1998
+}
+
+@Misc{Nipkow:1998:Winskel,
+author={Tobias Nipkow},
+title={Winskel is (almost) Right: Towards a Mechanized Semantics Textbook},
+journal=FAC,volume=10,pages={171--186},year=1998}
+}
+
+@Book{Winskel:1993,
+ author = {G. Winskel},
+ title = {The Formal Semantics of Programming Languages},
+ publisher = {MIT Press},
+ year = 1993
+}
+
+
+@manual{isabelle-isar-ref,
+ author = {Markus Wenzel},
+ title = {The {Isabelle/Isar} Reference Manual},
+ institution = {TU M{\"u}nchen},
+ year = 2000,
+ note = {\\ \url{http://isabelle.in.tum.de/doc/}}}
+
+@manual{isabelle-tutorial,
+ author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
+ title = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = 2283,
+ year = 2002,
+ note = {\\ \url{http://www4.in.tum.de/~nipkow/LNCS2283/}}}
+
+@Misc{McMillan-LectureNotes,
+ author = {Ken McMillan},
+ title = {Lecture notes for {NATO} summer school on verification of digital and hybrid systems},
+ note = {\\ \url{http://www-cad.eecs.berkeley.edu/~kenmcmil/tutorial/toc.html}}
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/exercises.tex Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,112 @@
+\input{style}
+\usepackage{graphicx}
+\usepackage[colorlinks,hyperindex]{hyperref}
+
+\newcommand{\aufgabe}[3]{
+\input{#1/#2/generated/#3}
+%\newpage
+}
+
+\title{Isabelle/HOL Exercises}
+\date{\today}
+\author{Gertrud Bauer, Gerwin Klein, Tobias Nipkow,\\ Michael Wahler, Markus Wenzel}
+
+\begin{document}
+
+\maketitle
+
+This document presents a collection of exercises for getting
+acquainted with the proof assistant
+Isabelle/HOL~\cite{isabelle-tutorial}. The exercises come out of an
+annual Isabelle/HOL course taught at the Technical University of
+Munich. They are arranged in chronological order, and in each year in
+ascending order of difficulty.
+
+\tableofcontents
+
+
+%--------------------------------------------
+\newpage
+\section{2000}
+\aufgabe{2000}{a1}{Snoc}
+\aufgabe{2000}{a1}{Arithmetic}
+\aufgabe{2000}{a1}{Hanoi}
+%\aufgabe{2000}{a2}{BDT}
+%\aufgabe{2000}{a2}{OBDT}
+%\aufgabe{2000}{a3}{NaturalDeduction}
+%\aufgabe{2000}{a3}{HoareLogic}
+%\aufgabe{2000}{a4}{CTLexample}
+%\aufgabe{2000}{a5}{Unix}
+
+%\section{L{\"o}sungen}
+%\aufgabe{2000}{l1}{Snoc}
+%\aufgabe{2000}{l1}{Arithmetic}
+%\aufgabe{2000}{l1}{Hanoi}
+%\aufgabe{2000}{l2}{BDT}
+%\aufgabe{2000}{l2}{OBDT}
+%\aufgabe{2000}{l3}{NaturalDeduction}
+%\aufgabe{2000}{l3}{HoareLogic}
+%\aufgabe{2000}{l4}{CTLexample}
+%\aufgabe{2000}{l5}{Unix}
+
+%--------------------------------------------
+\newpage
+\section{2001}
+\aufgabe{2001}{a1}{Aufgabe1}
+\aufgabe{2001}{a2}{Aufgabe2}
+\aufgabe{2001}{a3}{Trie1}
+\aufgabe{2001}{a3}{Trie2}
+\aufgabe{2001}{a3}{Trie3}
+%\aufgabe{2001}{a4}{Aufgabe4}
+\aufgabe{2001}{a5}{Aufgabe5}
+%\aufgabe{2001}{a5}{PL}
+%\aufgabe{2001}{a6}{Aufgabe6}
+
+%\section{L{\"o}sungen}
+%\aufgabe{2001}{l1}{Aufgabe1}
+%\aufgabe{2001}{l2}{Loesung2}
+%\aufgabe{2001}{l3}{Trie1}
+%\aufgabe{2001}{l3}{Trie2}
+%\aufgabe{2001}{l3}{Trie3}
+%\aufgabe{2001}{l4}{Loesung4}
+%\aufgabe{2001}{l5}{Loesung5}
+%\aufgabe{2001}{l5}{PL}
+%\aufgabe{2001}{l6}{Loesung6}
+
+
+%--------------------------------------------
+\newpage
+\section{2002}
+\aufgabe{2002}{a1}{a1}
+\aufgabe{2002}{a2}{a2}
+\aufgabe{2002}{a3}{a3}
+%\aufgabe{2002}{a4}{a4}
+\aufgabe{2002}{a5}{a5}
+\aufgabe{2002}{a6}{a6}
+%\aufgabe{2002}{a7}{a7}
+
+%\newpage
+%\section{L{\"o}sungen}
+%\aufgabe{2002}{l1}{l1}
+%\aufgabe{2002}{l2}{l2}
+%\aufgabe{2002}{l3}{l3}
+%\aufgabe{2002}{l4}{l4}
+%\aufgabe{2002}{l5}{l5}
+%\aufgabe{2002}{l6}{l6}
+%\aufgabe{2002}{l7}{ABP}
+
+%\newpage
+%\part{Anhang}
+%\section{Zu 2000}
+%\aufgabe{2000}{a4}{GfpLfp}
+%\aufgabe{2000}{a4}{CTL}
+%\aufgabe{2000}{a5}{Env}
+%\section{Zu 2001}
+%\aufgabe{2001}{a6}{Hoare}
+
+\newpage
+
+\bibliographystyle{abbrv}
+\bibliography{exercises}
+
+\end{document}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/isabelle.sty Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,157 @@
+%%
+%% Author: Markus Wenzel, TU Muenchen
+%% License: GPL (GNU GENERAL PUBLIC LICENSE)
+%%
+%% macros for Isabelle generated LaTeX output
+%%
+
+%%% Simple document preparation (based on theory token language and symbols)
+
+% isabelle environments
+
+\newcommand{\isabellecontext}{UNKNOWN}
+
+\newcommand{\isastyle}{\small\tt\slshape}
+\newcommand{\isastyleminor}{\small\tt\slshape}
+\newcommand{\isastylescript}{\footnotesize\tt\slshape}
+\newcommand{\isastyletext}{\normalsize\rm}
+\newcommand{\isastyletxt}{\rm}
+\newcommand{\isastylecmt}{\rm}
+
+%symbol markup -- \emph achieves decent spacing via italic corrections
+\newcommand{\isamath}[1]{\emph{$#1$}}
+\newcommand{\isatext}[1]{\emph{#1}}
+\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
+\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
+\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
+\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
+
+\newdimen\isa@parindent\newdimen\isa@parskip
+
+\newenvironment{isabellebody}{%
+\isamarkuptrue\par%
+\isa@parindent\parindent\parindent0pt%
+\isa@parskip\parskip\parskip0pt%
+\isastyle}{\par}
+
+\newenvironment{isabelle}
+{\begin{trivlist}\begin{isabellebody}\item\relax}
+{\end{isabellebody}\end{trivlist}}
+
+\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
+
+\newcommand{\isaindent}[1]{\hphantom{#1}}
+\newcommand{\isanewline}{\mbox{}\\\mbox{}}
+\newcommand{\isadigit}[1]{#1}
+
+\chardef\isacharbang=`\!
+\chardef\isachardoublequote=`\"
+\chardef\isacharhash=`\#
+\chardef\isachardollar=`\$
+\chardef\isacharpercent=`\%
+\chardef\isacharampersand=`\&
+\chardef\isacharprime=`\'
+\chardef\isacharparenleft=`\(
+\chardef\isacharparenright=`\)
+\chardef\isacharasterisk=`\*
+\chardef\isacharplus=`\+
+\chardef\isacharcomma=`\,
+\chardef\isacharminus=`\-
+\chardef\isachardot=`\.
+\chardef\isacharslash=`\/
+\chardef\isacharcolon=`\:
+\chardef\isacharsemicolon=`\;
+\chardef\isacharless=`\<
+\chardef\isacharequal=`\=
+\chardef\isachargreater=`\>
+\chardef\isacharquery=`\?
+\chardef\isacharat=`\@
+\chardef\isacharbrackleft=`\[
+\chardef\isacharbackslash=`\\
+\chardef\isacharbrackright=`\]
+\chardef\isacharcircum=`\^
+\chardef\isacharunderscore=`\_
+\chardef\isacharbackquote=`\`
+\chardef\isacharbraceleft=`\{
+\chardef\isacharbar=`\|
+\chardef\isacharbraceright=`\}
+\chardef\isachartilde=`\~
+
+
+% keyword and section markup
+
+\newcommand{\isakeywordcharunderscore}{\_}
+\newcommand{\isakeyword}[1]
+{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isakeywordcharunderscore}%
+\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
+\newcommand{\isacommand}[1]{\isakeyword{#1}}
+
+\newcommand{\isamarkupheader}[1]{\section{#1}}
+\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
+\newcommand{\isamarkupsection}[1]{\section{#1}}
+\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
+\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
+\newcommand{\isamarkupsect}[1]{\section{#1}}
+\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
+\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
+
+\newif\ifisamarkup
+\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
+\newcommand{\isaendpar}{\par\medskip}
+\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
+\newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}}
+\newenvironment{isamarkuptxt}{\isastyletxt\begin{isapar}}{\end{isapar}}
+\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
+
+
+% alternative styles
+
+\newcommand{\isabellestyle}{}
+\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
+
+\newcommand{\isabellestylett}{%
+\renewcommand{\isastyle}{\small\tt}%
+\renewcommand{\isastyleminor}{\small\tt}%
+\renewcommand{\isastylescript}{\footnotesize\tt}%
+}
+\newcommand{\isabellestyleit}{%
+\renewcommand{\isastyle}{\small\it}%
+\renewcommand{\isastyleminor}{\it}%
+\renewcommand{\isastylescript}{\footnotesize\it}%
+\renewcommand{\isakeywordcharunderscore}{\mbox{-}}%
+\renewcommand{\isacharbang}{\isamath{!}}%
+\renewcommand{\isachardoublequote}{}%
+\renewcommand{\isacharhash}{\isamath{\#}}%
+\renewcommand{\isachardollar}{\isamath{\$}}%
+\renewcommand{\isacharpercent}{\isamath{\%}}%
+\renewcommand{\isacharampersand}{\isamath{\&}}%
+\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
+\renewcommand{\isacharparenleft}{\isamath{(}}%
+\renewcommand{\isacharparenright}{\isamath{)}}%
+\renewcommand{\isacharasterisk}{\isamath{*}}%
+\renewcommand{\isacharplus}{\isamath{+}}%
+\renewcommand{\isacharcomma}{\isamath{\mathord,}}%
+\renewcommand{\isacharminus}{\isamath{-}}%
+\renewcommand{\isachardot}{\isamath{\mathord.}}%
+\renewcommand{\isacharslash}{\isamath{/}}%
+\renewcommand{\isacharcolon}{\isamath{\mathord:}}%
+\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
+\renewcommand{\isacharless}{\isamath{<}}%
+\renewcommand{\isacharequal}{\isamath{=}}%
+\renewcommand{\isachargreater}{\isamath{>}}%
+\renewcommand{\isacharat}{\isamath{@}}%
+\renewcommand{\isacharbrackleft}{\isamath{[}}%
+\renewcommand{\isacharbrackright}{\isamath{]}}%
+\renewcommand{\isacharunderscore}{\mbox{-}}%
+\renewcommand{\isacharbraceleft}{\isamath{\{}}%
+\renewcommand{\isacharbar}{\isamath{\mid}}%
+\renewcommand{\isacharbraceright}{\isamath{\}}}%
+\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
+}
+
+\newcommand{\isabellestylesl}{%
+\isabellestyleit%
+\renewcommand{\isastyle}{\small\sl}%
+\renewcommand{\isastyleminor}{\sl}%
+\renewcommand{\isastylescript}{\footnotesize\sl}%
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/isabellesym.sty Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,354 @@
+%%
+%% Author: Markus Wenzel, TU Muenchen
+%% License: GPL (GNU GENERAL PUBLIC LICENSE)
+%%
+%% definitions of standard Isabelle symbols
+%%
+
+% symbol definitions
+
+\newcommand{\isasymzero}{\isatext{\textzerooldstyle}} %requires textcomp
+\newcommand{\isasymone}{\isatext{\textoneoldstyle}} %requires textcomp
+\newcommand{\isasymtwo}{\isatext{\texttwooldstyle}} %requires textcomp
+\newcommand{\isasymthree}{\isatext{\textthreeoldstyle}} %requires textcomp
+\newcommand{\isasymfour}{\isatext{\textfouroldstyle}} %requires textcomp
+\newcommand{\isasymfive}{\isatext{\textfiveoldstyle}} %requires textcomp
+\newcommand{\isasymsix}{\isatext{\textsixoldstyle}} %requires textcomp
+\newcommand{\isasymseven}{\isatext{\textsevenoldstyle}} %requires textcomp
+\newcommand{\isasymeight}{\isatext{\texteightoldstyle}} %requires textcomp
+\newcommand{\isasymnine}{\isatext{\textnineoldstyle}} %requires textcomp
+\newcommand{\isasymA}{\isamath{\mathcal{A}}}
+\newcommand{\isasymB}{\isamath{\mathcal{B}}}
+\newcommand{\isasymC}{\isamath{\mathcal{C}}}
+\newcommand{\isasymD}{\isamath{\mathcal{D}}}
+\newcommand{\isasymE}{\isamath{\mathcal{E}}}
+\newcommand{\isasymF}{\isamath{\mathcal{F}}}
+\newcommand{\isasymG}{\isamath{\mathcal{G}}}
+\newcommand{\isasymH}{\isamath{\mathcal{H}}}
+\newcommand{\isasymI}{\isamath{\mathcal{I}}}
+\newcommand{\isasymJ}{\isamath{\mathcal{J}}}
+\newcommand{\isasymK}{\isamath{\mathcal{K}}}
+\newcommand{\isasymL}{\isamath{\mathcal{L}}}
+\newcommand{\isasymM}{\isamath{\mathcal{M}}}
+\newcommand{\isasymN}{\isamath{\mathcal{N}}}
+\newcommand{\isasymO}{\isamath{\mathcal{O}}}
+\newcommand{\isasymP}{\isamath{\mathcal{P}}}
+\newcommand{\isasymQ}{\isamath{\mathcal{Q}}}
+\newcommand{\isasymR}{\isamath{\mathcal{R}}}
+\newcommand{\isasymS}{\isamath{\mathcal{S}}}
+\newcommand{\isasymT}{\isamath{\mathcal{T}}}
+\newcommand{\isasymU}{\isamath{\mathcal{U}}}
+\newcommand{\isasymV}{\isamath{\mathcal{V}}}
+\newcommand{\isasymW}{\isamath{\mathcal{W}}}
+\newcommand{\isasymX}{\isamath{\mathcal{X}}}
+\newcommand{\isasymY}{\isamath{\mathcal{Y}}}
+\newcommand{\isasymZ}{\isamath{\mathcal{Z}}}
+\newcommand{\isasyma}{\isamath{\mathrm{a}}}
+\newcommand{\isasymb}{\isamath{\mathrm{b}}}
+\newcommand{\isasymc}{\isamath{\mathrm{c}}}
+\newcommand{\isasymd}{\isamath{\mathrm{d}}}
+\newcommand{\isasyme}{\isamath{\mathrm{e}}}
+\newcommand{\isasymf}{\isamath{\mathrm{f}}}
+\newcommand{\isasymg}{\isamath{\mathrm{g}}}
+\newcommand{\isasymh}{\isamath{\mathrm{h}}}
+\newcommand{\isasymi}{\isamath{\mathrm{i}}}
+\newcommand{\isasymj}{\isamath{\mathrm{j}}}
+\newcommand{\isasymk}{\isamath{\mathrm{k}}}
+\newcommand{\isasyml}{\isamath{\mathrm{l}}}
+\newcommand{\isasymm}{\isamath{\mathrm{m}}}
+\newcommand{\isasymn}{\isamath{\mathrm{n}}}
+\newcommand{\isasymo}{\isamath{\mathrm{o}}}
+\newcommand{\isasymp}{\isamath{\mathrm{p}}}
+\newcommand{\isasymq}{\isamath{\mathrm{q}}}
+\newcommand{\isasymr}{\isamath{\mathrm{r}}}
+\newcommand{\isasyms}{\isamath{\mathrm{s}}}
+\newcommand{\isasymt}{\isamath{\mathrm{t}}}
+\newcommand{\isasymu}{\isamath{\mathrm{u}}}
+\newcommand{\isasymv}{\isamath{\mathrm{v}}}
+\newcommand{\isasymw}{\isamath{\mathrm{w}}}
+\newcommand{\isasymx}{\isamath{\mathrm{x}}}
+\newcommand{\isasymy}{\isamath{\mathrm{y}}}
+\newcommand{\isasymz}{\isamath{\mathrm{z}}}
+\newcommand{\isasymAA}{\isamath{\mathfrak{A}}} %requires eufrak
+\newcommand{\isasymBB}{\isamath{\mathfrak{B}}} %requires eufrak
+\newcommand{\isasymCC}{\isamath{\mathfrak{C}}} %requires eufrak
+\newcommand{\isasymDD}{\isamath{\mathfrak{D}}} %requires eufrak
+\newcommand{\isasymEE}{\isamath{\mathfrak{E}}} %requires eufrak
+\newcommand{\isasymFF}{\isamath{\mathfrak{F}}} %requires eufrak
+\newcommand{\isasymGG}{\isamath{\mathfrak{G}}} %requires eufrak
+\newcommand{\isasymHH}{\isamath{\mathfrak{H}}} %requires eufrak
+\newcommand{\isasymII}{\isamath{\mathfrak{I}}} %requires eufrak
+\newcommand{\isasymJJ}{\isamath{\mathfrak{J}}} %requires eufrak
+\newcommand{\isasymKK}{\isamath{\mathfrak{K}}} %requires eufrak
+\newcommand{\isasymLL}{\isamath{\mathfrak{L}}} %requires eufrak
+\newcommand{\isasymMM}{\isamath{\mathfrak{M}}} %requires eufrak
+\newcommand{\isasymNN}{\isamath{\mathfrak{N}}} %requires eufrak
+\newcommand{\isasymOO}{\isamath{\mathfrak{O}}} %requires eufrak
+\newcommand{\isasymPP}{\isamath{\mathfrak{P}}} %requires eufrak
+\newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}} %requires eufrak
+\newcommand{\isasymRR}{\isamath{\mathfrak{R}}} %requires eufrak
+\newcommand{\isasymSS}{\isamath{\mathfrak{S}}} %requires eufrak
+\newcommand{\isasymTT}{\isamath{\mathfrak{T}}} %requires eufrak
+\newcommand{\isasymUU}{\isamath{\mathfrak{U}}} %requires eufrak
+\newcommand{\isasymVV}{\isamath{\mathfrak{V}}} %requires eufrak
+\newcommand{\isasymWW}{\isamath{\mathfrak{W}}} %requires eufrak
+\newcommand{\isasymXX}{\isamath{\mathfrak{X}}} %requires eufrak
+\newcommand{\isasymYY}{\isamath{\mathfrak{Y}}} %requires eufrak
+\newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}} %requires eufrak
+\newcommand{\isasymaa}{\isamath{\mathfrak{a}}} %requires eufrak
+\newcommand{\isasymbb}{\isamath{\mathfrak{b}}} %requires eufrak
+\newcommand{\isasymcc}{\isamath{\mathfrak{c}}} %requires eufrak
+\newcommand{\isasymdd}{\isamath{\mathfrak{d}}} %requires eufrak
+\newcommand{\isasymee}{\isamath{\mathfrak{e}}} %requires eufrak
+\newcommand{\isasymff}{\isamath{\mathfrak{f}}} %requires eufrak
+\newcommand{\isasymgg}{\isamath{\mathfrak{g}}} %requires eufrak
+\newcommand{\isasymhh}{\isamath{\mathfrak{h}}} %requires eufrak
+\newcommand{\isasymii}{\isamath{\mathfrak{i}}} %requires eufrak
+\newcommand{\isasymjj}{\isamath{\mathfrak{j}}} %requires eufrak
+\newcommand{\isasymkk}{\isamath{\mathfrak{k}}} %requires eufrak
+\newcommand{\isasymll}{\isamath{\mathfrak{l}}} %requires eufrak
+\newcommand{\isasymmm}{\isamath{\mathfrak{m}}} %requires eufrak
+\newcommand{\isasymnn}{\isamath{\mathfrak{n}}} %requires eufrak
+\newcommand{\isasymoo}{\isamath{\mathfrak{o}}} %requires eufrak
+\newcommand{\isasympp}{\isamath{\mathfrak{p}}} %requires eufrak
+\newcommand{\isasymqq}{\isamath{\mathfrak{q}}} %requires eufrak
+\newcommand{\isasymrr}{\isamath{\mathfrak{r}}} %requires eufrak
+\newcommand{\isasymss}{\isamath{\mathfrak{s}}} %requires eufrak
+\newcommand{\isasymtt}{\isamath{\mathfrak{t}}} %requires eufrak
+\newcommand{\isasymuu}{\isamath{\mathfrak{u}}} %requires eufrak
+\newcommand{\isasymvv}{\isamath{\mathfrak{v}}} %requires eufrak
+\newcommand{\isasymww}{\isamath{\mathfrak{w}}} %requires eufrak
+\newcommand{\isasymxx}{\isamath{\mathfrak{x}}} %requires eufrak
+\newcommand{\isasymyy}{\isamath{\mathfrak{y}}} %requires eufrak
+\newcommand{\isasymzz}{\isamath{\mathfrak{z}}} %requires eufrak
+\newcommand{\isasymalpha}{\isamath{\alpha}}
+\newcommand{\isasymbeta}{\isamath{\beta}}
+\newcommand{\isasymgamma}{\isamath{\gamma}}
+\newcommand{\isasymdelta}{\isamath{\delta}}
+\newcommand{\isasymepsilon}{\isamath{\varepsilon}}
+\newcommand{\isasymzeta}{\isamath{\zeta}}
+\newcommand{\isasymeta}{\isamath{\eta}}
+\newcommand{\isasymtheta}{\isamath{\vartheta}}
+\newcommand{\isasymiota}{\isamath{\iota}}
+\newcommand{\isasymkappa}{\isamath{\kappa}}
+\newcommand{\isasymlambda}{\isamath{\lambda}}
+\newcommand{\isasymmu}{\isamath{\mu}}
+\newcommand{\isasymnu}{\isamath{\nu}}
+\newcommand{\isasymxi}{\isamath{\xi}}
+\newcommand{\isasympi}{\isamath{\pi}}
+\newcommand{\isasymrho}{\isamath{\varrho}}
+\newcommand{\isasymsigma}{\isamath{\sigma}}
+\newcommand{\isasymtau}{\isamath{\tau}}
+\newcommand{\isasymupsilon}{\isamath{\upsilon}}
+\newcommand{\isasymphi}{\isamath{\varphi}}
+\newcommand{\isasymchi}{\isamath{\chi}}
+\newcommand{\isasympsi}{\isamath{\psi}}
+\newcommand{\isasymomega}{\isamath{\omega}}
+\newcommand{\isasymGamma}{\isamath{\Gamma}}
+\newcommand{\isasymDelta}{\isamath{\Delta}}
+\newcommand{\isasymTheta}{\isamath{\Theta}}
+\newcommand{\isasymLambda}{\isamath{\Lambda}}
+\newcommand{\isasymXi}{\isamath{\Xi}}
+\newcommand{\isasymPi}{\isamath{\Pi}}
+\newcommand{\isasymSigma}{\isamath{\Sigma}}
+\newcommand{\isasymUpsilon}{\isamath{\Upsilon}}
+\newcommand{\isasymPhi}{\isamath{\Phi}}
+\newcommand{\isasymPsi}{\isamath{\Psi}}
+\newcommand{\isasymOmega}{\isamath{\Omega}}
+\newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}}
+\newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}}
+\newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
+\newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}}
+\newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}}
+\newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}}
+\newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
+\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}
+\newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
+\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}
+\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
+\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
+\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
+\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
+\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}
+\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}
+\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}
+\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}
+\newcommand{\isasymmapsto}{\isamath{\mapsto}}
+\newcommand{\isasymlongmapsto}{\isamath{\longmapsto}}
+\newcommand{\isasymmidarrow}{\isamath{\relbar}}
+\newcommand{\isasymMidarrow}{\isamath{\Relbar}}
+\newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}}
+\newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}}
+\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
+\newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}}
+\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
+\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
+\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
+\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires latexsym
+\newcommand{\isasymup}{\isamath{\uparrow}}
+\newcommand{\isasymUp}{\isamath{\Uparrow}}
+\newcommand{\isasymdown}{\isamath{\downarrow}}
+\newcommand{\isasymDown}{\isamath{\Downarrow}}
+\newcommand{\isasymupdown}{\isamath{\updownarrow}}
+\newcommand{\isasymUpdown}{\isamath{\Updownarrow}}
+\newcommand{\isasymlangle}{\isamath{\langle}}
+\newcommand{\isasymrangle}{\isamath{\rangle}}
+\newcommand{\isasymlceil}{\isamath{\lceil}}
+\newcommand{\isasymrceil}{\isamath{\rceil}}
+\newcommand{\isasymlfloor}{\isamath{\lfloor}}
+\newcommand{\isasymrfloor}{\isamath{\rfloor}}
+\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}}
+\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}}
+\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}}
+\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}}
+\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}}
+\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
+\newcommand{\isasymguillemotleft}{\isatext{\flqq}} %requires babel
+\newcommand{\isasymguillemotright}{\isatext{\frqq}} %requires babel
+\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
+\newcommand{\isasymnot}{\isamath{\neg}}
+\newcommand{\isasymbottom}{\isamath{\bot}}
+\newcommand{\isasymtop}{\isamath{\top}}
+\newcommand{\isasymand}{\isamath{\wedge}}
+\newcommand{\isasymAnd}{\isamath{\bigwedge}}
+\newcommand{\isasymor}{\isamath{\vee}}
+\newcommand{\isasymOr}{\isamath{\bigvee}}
+\newcommand{\isasymforall}{\isamath{\forall\,}}
+\newcommand{\isasymexists}{\isamath{\exists\,}}
+\newcommand{\isasymbox}{\isamath{\Box}} %requires latexsym
+\newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires latexsym
+\newcommand{\isasymturnstile}{\isamath{\vdash}}
+\newcommand{\isasymTurnstile}{\isamath{\models}}
+\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
+\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}
+\newcommand{\isasymstileturn}{\isamath{\dashv}}
+\newcommand{\isasymsurd}{\isamath{\surd}}
+\newcommand{\isasymle}{\isamath{\le}}
+\newcommand{\isasymge}{\isamath{\ge}}
+\newcommand{\isasymlless}{\isamath{\ll}}
+\newcommand{\isasymggreater}{\isamath{\gg}}
+\newcommand{\isasymlesssim}{\isamath{\lesssim}} %requires amssymb
+\newcommand{\isasymgreatersim}{\isamath{\gtrsim}} %requires amssymb
+\newcommand{\isasymlessapprox}{\isamath{\lessapprox}} %requires amssymb
+\newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}} %requires amssymb
+\newcommand{\isasymin}{\isamath{\in}}
+\newcommand{\isasymnotin}{\isamath{\notin}}
+\newcommand{\isasymsubset}{\isamath{\subset}}
+\newcommand{\isasymsupset}{\isamath{\supset}}
+\newcommand{\isasymsubseteq}{\isamath{\subseteq}}
+\newcommand{\isasymsupseteq}{\isamath{\supseteq}}
+\newcommand{\isasymsqsubset}{\isamath{\sqsubset}}
+\newcommand{\isasymsqsupset}{\isamath{\sqsupset}} %requires latexsym
+\newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}
+\newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}
+\newcommand{\isasyminter}{\isamath{\cap}}
+\newcommand{\isasymInter}{\isamath{\bigcap\,}}
+\newcommand{\isasymunion}{\isamath{\cup}}
+\newcommand{\isasymUnion}{\isamath{\bigcup\,}}
+\newcommand{\isasymsqunion}{\isamath{\sqcup}}
+\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
+\newcommand{\isasymsqinter}{\isamath{\sqcap}}
+\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires stmaryrd
+\newcommand{\isasymuplus}{\isamath{\uplus}}
+\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
+\newcommand{\isasymnoteq}{\isamath{\not=}}
+\newcommand{\isasymsim}{\isamath{\sim}}
+\newcommand{\isasymdoteq}{\isamath{\doteq}}
+\newcommand{\isasymsimeq}{\isamath{\simeq}}
+\newcommand{\isasymapprox}{\isamath{\approx}}
+\newcommand{\isasymasymp}{\isamath{\asymp}}
+\newcommand{\isasymcong}{\isamath{\cong}}
+\newcommand{\isasymsmile}{\isamath{\smile}}
+\newcommand{\isasymequiv}{\isamath{\equiv}}
+\newcommand{\isasymfrown}{\isamath{\frown}}
+\newcommand{\isasympropto}{\isamath{\propto}}
+\newcommand{\isasymbowtie}{\isamath{\bowtie}}
+\newcommand{\isasymprec}{\isamath{\prec}}
+\newcommand{\isasymsucc}{\isamath{\succ}}
+\newcommand{\isasympreceq}{\isamath{\preceq}}
+\newcommand{\isasymsucceq}{\isamath{\succeq}}
+\newcommand{\isasymparallel}{\isamath{\parallel}}
+\newcommand{\isasymbar}{\isamath{\mid}}
+\newcommand{\isasymplusminus}{\isamath{\pm}}
+\newcommand{\isasymminusplus}{\isamath{\mp}}
+\newcommand{\isasymtimes}{\isamath{\times}}
+\newcommand{\isasymdiv}{\isamath{\div}}
+\newcommand{\isasymcdot}{\isamath{\cdot}}
+\newcommand{\isasymstar}{\isamath{\star}}
+\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}}
+\newcommand{\isasymcirc}{\isamath{\circ}}
+\newcommand{\isasymdagger}{\isamath{\dagger}}
+\newcommand{\isasymddagger}{\isamath{\ddagger}}
+\newcommand{\isasymlhd}{\isamath{\lhd}}
+\newcommand{\isasymrhd}{\isamath{\rhd}}
+\newcommand{\isasymunlhd}{\isamath{\unlhd}}
+\newcommand{\isasymunrhd}{\isamath{\unrhd}}
+\newcommand{\isasymtriangleleft}{\isamath{\triangleleft}}
+\newcommand{\isasymtriangleright}{\isamath{\triangleright}}
+\newcommand{\isasymtriangle}{\isamath{\triangle}}
+\newcommand{\isasymtriangleq}{\isamath{\triangleq}} %requires amssymb
+\newcommand{\isasymoplus}{\isamath{\oplus}}
+\newcommand{\isasymOplus}{\isamath{\bigoplus\,}}
+\newcommand{\isasymotimes}{\isamath{\otimes}}
+\newcommand{\isasymOtimes}{\isamath{\bigotimes\,}}
+\newcommand{\isasymodot}{\isamath{\odot}}
+\newcommand{\isasymOdot}{\isamath{\bigodot\,}}
+\newcommand{\isasymominus}{\isamath{\ominus}}
+\newcommand{\isasymoslash}{\isamath{\oslash}}
+\newcommand{\isasymdots}{\isamath{\dots}}
+\newcommand{\isasymcdots}{\isamath{\cdots}}
+\newcommand{\isasymSum}{\isamath{\sum\,}}
+\newcommand{\isasymProd}{\isamath{\prod\,}}
+\newcommand{\isasymCoprod}{\isamath{\coprod\,}}
+\newcommand{\isasyminfinity}{\isamath{\infty}}
+\newcommand{\isasymintegral}{\isamath{\int\,}}
+\newcommand{\isasymointegral}{\isamath{\oint\,}}
+\newcommand{\isasymclubsuit}{\isamath{\clubsuit}}
+\newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}}
+\newcommand{\isasymheartsuit}{\isamath{\heartsuit}}
+\newcommand{\isasymspadesuit}{\isamath{\spadesuit}}
+\newcommand{\isasymaleph}{\isamath{\aleph}}
+\newcommand{\isasymemptyset}{\isamath{\emptyset}}
+\newcommand{\isasymnabla}{\isamath{\nabla}}
+\newcommand{\isasympartial}{\isamath{\partial}}
+\newcommand{\isasymRe}{\isamath{\Re}}
+\newcommand{\isasymIm}{\isamath{\Im}}
+\newcommand{\isasymflat}{\isamath{\flat}}
+\newcommand{\isasymnatural}{\isamath{\natural}}
+\newcommand{\isasymsharp}{\isamath{\sharp}}
+\newcommand{\isasymangle}{\isamath{\angle}}
+\newcommand{\isasymcopyright}{\isatext{\rm\copyright}}
+\newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
+\newcommand{\isasymhyphen}{\isatext{\rm-}}
+\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
+\newcommand{\isasymonesuperior}{\isamath{\mathonesuperior}} %requires latin1
+\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}} %requires latin1
+\newcommand{\isasymtwosuperior}{\isamath{\mathtwosuperior}} %requires latin1
+\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}} %requires latin1
+\newcommand{\isasymthreesuperior}{\isamath{\maththreesuperior}} %requires latin1
+\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}} %requires latin1
+\newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
+\newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
+\newcommand{\isasymsection}{\isatext{\rm\S}}
+\newcommand{\isasymparagraph}{\isatext{\rm\P}}
+\newcommand{\isasymexclamdown}{\isatext{\rm\textexclamdown}}
+\newcommand{\isasymquestiondown}{\isatext{\rm\textquestiondown}}
+\newcommand{\isasymeuro}{\isatext{\EUR}} %requires marvosym
+\newcommand{\isasympounds}{\isamath{\pounds}}
+\newcommand{\isasymyen}{\isatext{\yen}} %requires amssymb
+\newcommand{\isasymcent}{\isatext{\cent}} %requires wasysym
+\newcommand{\isasymcurrency}{\isatext{\currency}} %requires wasysym
+\newcommand{\isasymdegree}{\isatext{\rm\textdegree}} %requires latin1
+\newcommand{\isasymamalg}{\isamath{\amalg}}
+\newcommand{\isasymmho}{\isamath{\mho}} %requires latexsym
+\newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssym
+\newcommand{\isasymJoin}{\isamath{\Join}} %requires latexsym
+\newcommand{\isasymwp}{\isamath{\wp}}
+\newcommand{\isasymwrong}{\isamath{\wr}}
+\newcommand{\isasymstruct}{\isamath{\diamond}}
+\newcommand{\isasymacute}{\isatext{\'\relax}}
+\newcommand{\isasymindex}{\isatext{\i}}
+\newcommand{\isasymdieresis}{\isatext{\"\relax}}
+\newcommand{\isasymcedilla}{\isatext{\c\relax}}
+\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
+\newcommand{\isasymspacespace}{\isamath{~~}}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/style.tex Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,97 @@
+%
+% $Id$
+%
+
+%% document setup
+
+\documentclass[12pt,a4paper]{article}
+\usepackage{ifthen,latexsym}
+%\usepackage[latin1]{inputenc}
+%\usepackage[german]{babel}\AtBeginDocument{\mdqon}
+\usepackage{isabelle,isabellesym}
+\sloppy \parindent 0pt \parskip 1ex
+
+\makeatletter
+\@ifundefined{pdfoutput}{\newcommand{\href}[2]{#2}}{}
+\makeatother
+
+%borrowed from a4wide/12pt :-(
+\oddsidemargin 0 in
+\evensidemargin 0 in
+\marginparwidth 0.75 in
+\textwidth 6.375 true in
+\addtolength{\topmargin}{-2cm}
+\addtolength{\textheight}{2cm}
+
+\thispagestyle{empty}
+
+\newlength{\TUMBr}\settowidth{\TUMBr}{{\bf Technische Universität München}}
+\newcommand{\header}[2]{{\bf
+ \parbox{0.5\textwidth}{
+ \parbox{\TUMBr}{\begin{center}
+ Technische Universität München \\
+ Institut für Informatik \\
+ Prof.~Tobias Nipkow, Ph.\,D.\\
+ Gerwin Klein\end{center}}}
+ \parbox{0.5\textwidth}{
+ \begin{flushright}
+ SS 2002 \\ #1 \\ #2 \\
+ \end{flushright}}
+ \bigskip
+ \begin{center}
+ \Large
+ Praktikum Spezifikation und Verifikation
+ \end{center}
+ \bigskip}}
+
+\newcommand{\note}[1]{\textbf{$\rhd$~#1}}
+
+
+\newcommand{\Chref}[1]{Chapter~\ref{#1}}
+\newcommand{\chref}[1]{chapter~\ref{#1}}
+\newcommand{\Secref}[1]{Section~\ref{#1}}
+\newcommand{\secref}[1]{§\ref{#1}}
+
+
+%% misc macros
+
+\newcommand{\text}[1]{\mbox{#1}}
+
+\newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
+\newcommand{\var}[1]{{?\!\idt{#1}}}
+\newcommand{\name}[1]{\textsl{#1}}
+
+\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
+\newcommand{\dsh}{\dshsym}
+
+\newcommand{\pow}[2]{#1\mathbin{\!\symbol{94}\!}#2}
+
+%\newcommand{\ap}{\mathpalette{\mathbin{\mkern-1mu}}{\mathbin{\mkern-2mu}}{\mathbin{}}{\mathbin{}}}
+\newcommand{\ap}{\mathpalette{\mathbin{}}{\mathbin{}}{\mathbin{}}{\mathbin{}}}
+\newcommand{\dt}{{\mathpunct.\;}}
+\newcommand{\lam}[1]{\mathop{\lambda} #1\dt}
+
+\newcommand{\impl}{\to}
+
+
+%% tune Isabelle output
+
+\newcommand{\isasorry}{$\;\langle\idt{proof}\rangle$}
+\newcommand{\isaoops}{$\vdots$}
+
+\renewcommand{\isacommand}[1]
+{\ifthenelse{\equal{sorry}{#1}}{\isasorry}
+ {\ifthenelse{\equal{oops}{#1}}{\isaoops}{\isakeyword{#1}}}}
+
+\renewcommand{\isabellestyle}{\footnotesize\tt\slshape}
+\renewcommand{\isa}[1]{\emph{\small\tt\slshape #1}}
+%\renewcommand\isabellemarkupsubsubsection{\subsubsection*}
+\renewcommand\isamarkupsubsubsection{\subsubsection*}
+
+\renewcommand{\isamarkupheader}[1]{\subsection*{#1}}
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: