# HG changeset patch # User kleing # Date 1039104727 -3600 # Node ID f5d0a66c8124789f52d30b997a3549e2a5b4d29e # Parent d48d1716bb6d0d7b2853c6aa443585e8b5aacfd5 exercise collection diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/2000/IsaMakefile --- /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 + diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/2000/a1/Arithmetic.thy --- /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 diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/2000/a1/Hanoi.thy --- /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 +(*>*) diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/2000/a1/ROOT.ML --- /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 diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/2000/a1/Snoc.thy --- /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 +(*>*) diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/2001/IsaMakefile --- /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 + diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/2001/a1/Aufgabe1.thy --- /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 \ 'a \ 'a list \ '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 \ 'a list \ 'a list" + delall :: "'a \ 'a list \ '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 diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/2001/a1/ROOT.ML --- /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"; diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/2001/a2/Aufgabe2.thy --- /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 \ 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 @{text"\"}. +\end{itemize} +*} + +(*<*) +end; +(*>*) diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/2001/a2/ROOT.ML --- /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"; + diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/2001/a3/ROOT.ML --- /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"; diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/2001/a3/Trie1.thy --- /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 \ 'v option" +primrec "value (Trie ov al) = ov"; + +consts alist :: "('a, 'v) trie \ ('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 \ 'key \ '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 \ 'a list \ 'v option"; +primrec "lookup t [] = value t" + "lookup t (a#as) = (case assoc (alist t) a of + None \ None + | Some at \ 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 \ 'a list \ 'v \ ('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 \ Trie None [] + | Some at \ 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 "\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 \ 'a list \ 'v option \ ('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; +(*>*) diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/2001/a3/Trie2.thy --- /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 \ 'b \ ('a * 'b) list \ ('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; +(*>*) diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/2001/a3/Trie3.thy --- /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 \ '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 \ ('a,'v) trie option"; + +text{* Modify the definitions of @{term lookup} and @{term modify} +accordingly and show the same correctness theorem as above. *} + +(*<*) +end; +(*>*) diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/2001/a5/Aufgabe5.thy --- /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 \ n\m \ inv2 n ins" +(*<*)oops(*>*) + +text {* +Now show that @{term add} and @{term rem} preserve the invariant: +*} + +theorem inv_add: "\ i\j; inv ins \ \ inv (add (i,j) ins)" +(*<*)oops(*>*) + +theorem inv_rem: "\ i\j; inv ins \ \ 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"\"} and @{text"-"} on sets: *} + +theorem set_of_add: + "\ i\j; inv ins \ \ set_of (add (i,j) ins) = set_of [(i,j)] \ set_of ins" +(*<*)oops(*>*) + +theorem set_of_rem: + "\ i \ j; inv ins \ \ 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 +(*>*) diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/2001/a5/ROOT.ML --- /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"; + diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/2002/IsaMakefile --- /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 diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/2002/a1/ROOT.ML --- /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"; diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/2002/a1/a1.thy --- /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 \ bool) \ 'a list \ bool" + exs :: "('a \ bool) \ 'a list \ 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 (\x. P x \ Q x) xs = (alls P xs \ alls Q xs)" +(*<*)oops(*>*) + +lemma "alls P (rev xs) = alls P xs" +(*<*)oops(*>*) + +lemma "exs (\x. P x \ Q x) xs = (exs P xs \ 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 (\x. P x \ 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 diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/2002/a2/ROOT.ML --- /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"; diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/2002/a2/a2.thy --- /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 \ nat list \ nat list" + sort :: "nat list \ nat list" + le :: "nat \ nat list \ bool" + sorted :: "nat list \ 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 \ y \ le y xs \ 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 \ sorted b \ ge x a \ le x b)"} +\end{itemize} +*} + +(*<*) +end +(*>*) \ No newline at end of file diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/2002/a3/ROOT.ML --- /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"; diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/2002/a3/a3.thy --- /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 \ 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 diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/2002/a5/ROOT.ML --- /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"; diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/2002/a5/a5.thy --- /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 \ nat list \ nat list" + msort :: "nat list \ 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 +(*>*) diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/2002/a5/l2.thy --- /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 \ nat list \ nat list" + sort :: "nat list \ nat list" + le :: "nat \ nat list \ bool" + sorted :: "nat list \ 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 "\ le 3 [7,10,2]" by auto + +lemma "sorted [1,2,3,4]" by auto + +lemma "\ 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 \ y \ le y xs \ 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 \ bool" + tge :: "nat \ bintree \ bool" + tle :: "nat \ bintree \ bool" + ins :: "nat \ bintree \ bintree" + tree_of :: "nat list \ bintree" + +primrec + "tsorted Empty = True" + "tsorted (Node n t1 t2) = (tsorted t1 \ tsorted t2 \ tge n t1 \ tle n t2)" + +primrec + "tge x Empty = True" + "tge x (Node n t1 t2) = (n \ x \ tge x t1 \ tge x t2)" + +primrec + "tle x Empty = True" + "tle x (Node n t1 t2) = (x \ n \ tle x t1 \ tle x t2)" + +primrec + "ins x Empty = Node x Empty Empty" + "ins x (Node n t1 t2) = (if x \ 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 "\ tge 5 (Node 3 Empty (Node 7 Empty Empty))" by auto + +lemma "\ tle 5 (Node 3 (Node 2 Empty Empty) Empty)" by auto + +lemma "\ 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 \ a \ tge a t)" + apply (induct_tac t) + apply auto + done + +lemma [simp]: + "tle a (ins x t) = (a \ x \ 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 \ nat list \ bool" + list_of :: "bintree \ nat list" + +primrec + "ge a [] = True" + "ge a (x#xs) = (x \ a \ 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 \ le x b)" + apply (induct_tac a) + apply auto + done + +lemma [simp]: + "ge x (a@b) = (ge x a \ ge x b)" + apply (induct_tac a) + apply auto + done + +lemma [simp]: + "sorted (a@x#b) = (sorted a \ sorted b \ ge x a \ 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 diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/2002/a6/ROOT.ML --- /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"; diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/2002/a6/a6.thy --- /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 diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/Hanoi.pdf Binary file doc-src/Exercises/Hanoi.pdf has changed diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/Makefile --- /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 diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/exercises.bib --- /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}} +} diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/exercises.tex --- /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} diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/isabelle.sty --- /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}% +} diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/isabellesym.sty --- /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{~~}} diff -r d48d1716bb6d -r f5d0a66c8124 doc-src/Exercises/style.tex --- /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: