# HG changeset patch
# User streckem
# Date 1080668037 -7200
# Node ID f08ea8e964d85a71757a199986a50f4429131581
# Parent  c770a2f0ea7825e1d03bfc892f17a6fb7aa18498
new

diff -r c770a2f0ea78 -r f08ea8e964d8 doc-src/Exercises/0304/IsaMakefile
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/0304/IsaMakefile	Tue Mar 30 19:33:57 2004 +0200
@@ -0,0 +1,77 @@
+#
+# $Id$
+#
+# IsaMakefile for PSV 2003 / 2004
+#
+
+SESSIONS = a1 a2 a3 a4 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
+
+## a4
+
+a4: a4/generated/session.tex
+
+a4/generated/session.tex: a4/ROOT.ML \
+  a4/*.thy
+	@$(USEDIR) HOL a4
+
+## a5
+
+a5: a5/generated/session.tex
+
+a5/generated/session.tex: a5/ROOT.ML \
+  a5/*.thy
+	@$(USEDIR) HOL a5
+
diff -r c770a2f0ea78 -r f08ea8e964d8 doc-src/Exercises/0304/Makefile
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/0304/Makefile	Tue Mar 30 19:33:57 2004 +0200
@@ -0,0 +1,49 @@
+#
+# $Id$
+#
+# IsaMakefile for PSV WS 2003/2004
+#
+
+SESSIONS = a1 a2 a3 a4 a5
+
+## targets
+
+default: sessions
+sessions: $(SESSIONS)
+
+
+## a1
+
+a1: a1/generated/session.tex
+
+a1/generated/session.tex: a1/ROOT.ML a1/*.thy
+	isatool make
+
+## a2
+
+a2: a2/generated/session.tex
+
+a2/generated/session.tex: a2/ROOT.ML a2/*.thy
+	isatool make
+
+## a3
+
+a3: a3/generated/session.tex
+
+a3/generated/session.tex: a3/ROOT.ML a3/*.thy
+	isatool make
+
+## a4
+
+a4: a4/generated/session.tex
+
+a4/generated/session.tex: a4/ROOT.ML a4/*.thy
+	isatool make
+
+## a5
+
+a5: a5/generated/session.tex
+
+a5/generated/session.tex: a5/ROOT.ML a5/*.thy
+	isatool make
+
diff -r c770a2f0ea78 -r f08ea8e964d8 doc-src/Exercises/0304/a1/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/0304/a1/ROOT.ML	Tue Mar 30 19:33:57 2004 +0200
@@ -0,0 +1,1 @@
+  use_thy "a1";
diff -r c770a2f0ea78 -r f08ea8e964d8 doc-src/Exercises/0304/a1/a1.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/0304/a1/a1.thy	Tue Mar 30 19:33:57 2004 +0200
@@ -0,0 +1,93 @@
+
+(*<*) theory a1 = Main: (*>*)
+
+subsection {* List functions *}
+
+text{* Define a function @{text sum}, which computes the sum of
+elements of a list of natural numbers. *}
+
+(*<*) consts (*>*)
+  sum :: "nat list \<Rightarrow> nat"
+
+text{* Then, define a function @{text flatten} which flattens a list
+of lists by appending the member lists. *}
+
+(*<*) consts (*>*)
+  flatten :: "'a list list \<Rightarrow> 'a list"
+
+text{* Test your function by applying them to the following example lists: *}
+
+
+lemma "sum [2::nat, 4, 8] = x"
+(*<*) oops (*>*)
+
+lemma "flatten [[2::nat, 3], [4, 5], [7, 9]] = x"
+(*<*) oops (*>*)
+
+
+text{* Prove the following statements, or give a counterexample: *}
+
+
+lemma "length (flatten xs) = sum (map length xs)"
+(*<*) oops (*>*)
+
+lemma sum_append: "sum (xs @ ys) = sum xs + sum ys"
+(*<*) oops (*>*)
+
+lemma flatten_append: "flatten (xs @ ys) = flatten xs @ flatten ys"
+(*<*) oops (*>*)
+
+lemma "flatten (map rev (rev xs)) = rev (flatten xs)"
+(*<*) oops (*>*)
+
+lemma "flatten (rev (map rev xs)) = rev (flatten xs)"
+(*<*) oops (*>*)
+
+lemma "list_all (list_all P) xs = list_all P (flatten xs)"
+(*<*) oops (*>*)
+
+lemma "flatten (rev xs) = flatten xs"
+(*<*) oops (*>*)
+
+lemma "sum (rev xs) = sum xs"
+(*<*) oops (*>*)
+
+
+text{* Find a predicate @{text P} which satisfies *}
+
+lemma "list_all P xs \<longrightarrow> length xs \<le> sum xs"
+(*<*) oops (*>*)
+
+text{* Define, by means of primitive recursion, a function @{text
+exists} which checks whether an element satisfying a given property is
+contained in the list: *}
+
+
+(*<*) consts (*>*)
+  list_exists :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<Rightarrow> bool)"
+
+text{* Test your function on the following examples: *}
+
+
+lemma "list_exists (\<lambda> n. n < 3) [4::nat, 3, 7] = b"
+(*<*) oops (*>*)
+
+lemma "list_exists (\<lambda> n. n < 4) [4::nat, 3, 7] = b"
+(*<*) oops (*>*)
+
+text{* Prove the following statements: *}
+
+lemma list_exists_append: 
+  "list_exists P (xs @ ys) = (list_exists P xs \<or> list_exists P ys)"
+(*<*) oops (*>*)
+
+lemma "list_exists (list_exists P) xs = list_exists P (flatten xs)"
+(*<*) oops (*>*)
+
+text{* You could have defined @{text list_exists} only with the aid of
+@{text list_all}. Do this now, i.e. define a function @{text
+list_exists2} and show that it is equivalent to @{text list_exists}. *}
+
+
+(*<*) end (*>*)
+
diff -r c770a2f0ea78 -r f08ea8e964d8 doc-src/Exercises/0304/a2/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/0304/a2/ROOT.ML	Tue Mar 30 19:33:57 2004 +0200
@@ -0,0 +1,1 @@
+  use_thy "a2";
diff -r c770a2f0ea78 -r f08ea8e964d8 doc-src/Exercises/0304/a2/a2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/0304/a2/a2.thy	Tue Mar 30 19:33:57 2004 +0200
@@ -0,0 +1,129 @@
+
+(*<*) theory a2 = Main: (*>*)
+
+subsection {* Folding Lists and Trees *}
+
+subsubsection {* Some more list functions *}
+
+text{* Recall the summation function *}
+
+(*<*) consts (*>*)
+  sum :: "nat list \<Rightarrow> nat"
+primrec
+  "sum [] = 0"
+  "sum (x # xs) = x + sum xs"
+
+
+text{* In the Isabelle library, you will find in theory
+\texttt{List.thy} the functions @{text foldr} and @{text foldl}, which
+allow you to define some list functions, among them @{text sum} and
+@{text length}. Show the following: *}
+
+
+lemma sum_foldr: "sum xs = foldr (op +) xs 0"
+(*<*) oops (*>*)
+
+lemma length_foldr: "length xs = foldr (\<lambda> x res. 1 + res) xs 0"
+(*<*) oops (*>*)
+
+text {* Repeated application of @{text foldr} and @{text map} has the
+disadvantage that a list is traversed several times. A single traversal is sufficient, as
+illustrated by the following example: *}
+
+lemma "sum (map (\<lambda> x. x + 3) xs) = foldr h xs b"
+(*<*) oops (*>*)
+
+text {* Find terms @{text h} and @{text b} which solve this
+equation. Generalize this result, i.e. show for appropriate @{text h}
+and @{text b}: *}
+
+
+lemma "foldr g (map f xs) a = foldr h xs b"
+(*<*) oops (*>*)
+
+text {* Hint: Isabelle can help you find the solution if you use the
+equalities arising during a proof attempt. *}
+
+text {* The following function @{text rev_acc} reverses a list in linear time: *}
+
+
+consts
+  rev_acc :: "['a list, 'a list] \<Rightarrow> 'a list"
+primrec
+  "rev_acc [] ys = ys"
+  "rev_acc (x#xs) ys = (rev_acc xs (x#ys))"
+
+text{* Show that @{text rev_acc} can be defined by means of @{text foldl}. *}
+
+lemma rev_acc_foldl: "rev_acc xs a = foldl (\<lambda> ys x. x # ys) a xs"
+(*<*) oops (*>*)
+
+text {* On the first exercise sheet, we have shown: *}
+
+lemma sum_append [simp]: "sum (xs @ ys) = sum xs + sum ys"
+  by (induct xs) auto
+
+text {* Prove a similar distributivity property for @{text foldr},
+i.e. something like @{text "foldr f (xs @ ys) a = f (foldr f xs a)
+(foldr f ys a)"}. However, you will have to strengthen the premisses
+by taking into account algebraic properties of @{text f} and @{text
+a}. *}
+
+
+lemma foldr_append: "foldr f (xs @ ys) a = f (foldr f xs a) (foldr f ys a)"
+(*<*) oops (*>*)
+
+text {* Now, define the function @{text prod}, which computes the product of all list elements: *}
+(*<*) consts (*>*)
+  prod :: "nat list \<Rightarrow> nat"
+
+text {* direcly with the aid of  a fold and prove the following: *}
+lemma "prod (xs @ ys) = prod xs * prod ys"
+(*<*) oops (*>*)
+
+
+subsubsection {* Functions on Trees *}
+
+text {* Consider the following type of binary trees: *}
+datatype 'a tree = Tip | Node "'a tree" 'a "'a tree"
+
+text {* Define functions which convert a tree into a list by traversing it in pre- resp. postorder: *}
+(*<*) consts (*>*)
+  preorder :: "'a tree \<Rightarrow> 'a list"
+  postorder :: "'a tree \<Rightarrow> 'a list"
+
+text {* You have certainly realized that computation of postorder traversal can be efficiently realized with an accumulator, in analogy to  @{text rev_acc}: *} 
+
+consts
+  postorder_acc :: "['a tree, 'a list] \<Rightarrow> 'a list"
+
+text {* Define this function and show: *}
+lemma "postorder_acc t xs = (postorder t) @ xs"
+(*<*) oops (*>*)
+
+
+text {* @{text postorder_acc} is the instance of a function
+@{text foldl_tree}, which is similar to @{text foldl}. *}
+
+consts
+  foldl_tree :: "('b => 'a => 'b) \<Rightarrow> 'b \<Rightarrow> 'a tree \<Rightarrow> 'b"
+
+text {* Show the following: *}
+
+lemma "\<forall> a. postorder_acc t a = foldl_tree (\<lambda> xs x. Cons x xs) a t"
+(*<*) oops (*>*)
+
+text {* Define a function @{text tree_sum} that computes the sum of
+the elements of a tree of natural numbers: *}
+
+consts
+  tree_sum :: "nat tree \<Rightarrow> nat"
+
+text {* and show that this function satisfies *}
+
+lemma "tree_sum t = sum (preorder t)"
+(*<*) oops (*>*)
+
+
+(*<*) end (*>*)
+
diff -r c770a2f0ea78 -r f08ea8e964d8 doc-src/Exercises/0304/a3/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/0304/a3/ROOT.ML	Tue Mar 30 19:33:57 2004 +0200
@@ -0,0 +1,1 @@
+  use_thy "a3";
diff -r c770a2f0ea78 -r f08ea8e964d8 doc-src/Exercises/0304/a3/a3.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/0304/a3/a3.thy	Tue Mar 30 19:33:57 2004 +0200
@@ -0,0 +1,74 @@
+
+(*<*) theory a3 = Main: (*>*)
+
+subsection {* Natural deduction -- Propositional Logic \label{psv0304a3} *}
+
+text {* In this exercise, we will prove some lemmas of propositional
+logic with the aid of a calculus of natural deduction.
+
+For the proofs, you may only use
+
+\begin{itemize}
+\item the following lemmas: \\
+@{text "notI:"}~@{thm notI[of A,no_vars]},\\
+@{text "notE:"}~@{thm notE[of A B,no_vars]},\\
+@{text "conjI:"}~@{thm conjI[of A B,no_vars]},\\ 
+@{text "conjE:"}~@{thm conjE[of A B C,no_vars]},\\
+@{text "disjI1:"}~@{thm disjI1[of A B,no_vars]},\\
+@{text "disjI2:"}~@{thm disjI2[of A B,no_vars]},\\
+@{text "disjE:"}~@{thm disjE[of A B C,no_vars]},\\
+@{text "impI:"}~@{thm impI[of A B,no_vars]},\\
+@{text "impE:"}~@{thm impE[of A B C,no_vars]},\\
+@{text "mp:"}~@{thm mp[of A B,no_vars]}\\
+@{text "iffI:"}~@{thm iffI[of A B,no_vars]}, \\
+@{text "iffE:"}~@{thm iffE[of A B C,no_vars]}\\
+@{text "classical:"}~@{thm classical[of A,no_vars]}
+
+\item the proof methods @{term rule}, @{term erule} and @{term assumption}
+\end{itemize}
+*}
+
+lemma I: "A \<longrightarrow> A"
+(*<*) oops (*>*)
+
+lemma "A \<and> B \<longrightarrow> B \<and> A"
+(*<*) oops (*>*)
+
+lemma "(A \<and> B) \<longrightarrow> (A \<or> B)"
+(*<*) oops (*>*)
+
+lemma "((A \<or> B) \<or> C) \<longrightarrow> A \<or> (B \<or> C)"
+(*<*) oops (*>*)
+
+lemma K: "A \<longrightarrow> B \<longrightarrow> A"
+(*<*) oops (*>*)
+
+lemma "(A \<or> A) = (A \<and> A)"
+(*<*) oops (*>*)
+
+lemma S: "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> B) \<longrightarrow> A \<longrightarrow> C"
+(*<*) oops (*>*)
+
+lemma "(A \<longrightarrow> B) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> A \<longrightarrow> C"
+(*<*) oops (*>*)
+
+lemma "\<not> \<not> A \<longrightarrow> A"
+(*<*) oops (*>*)
+
+lemma "A \<longrightarrow> \<not> \<not> A"
+(*<*) oops (*>*)
+
+lemma "(\<not> A \<longrightarrow> B) \<longrightarrow> (\<not> B \<longrightarrow> A)"
+(*<*) oops (*>*)
+
+lemma "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
+(*<*) oops (*>*)
+
+lemma "A \<or> \<not> A"
+(*<*) oops (*>*)
+
+lemma "(\<not> (A \<and> B)) = (\<not> A \<or> \<not> B)"
+(*<*) oops (*>*)
+
+(*<*) end (*>*)
+
diff -r c770a2f0ea78 -r f08ea8e964d8 doc-src/Exercises/0304/a4/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/0304/a4/ROOT.ML	Tue Mar 30 19:33:57 2004 +0200
@@ -0,0 +1,1 @@
+  use_thy "a4";
diff -r c770a2f0ea78 -r f08ea8e964d8 doc-src/Exercises/0304/a4/a4.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/0304/a4/a4.thy	Tue Mar 30 19:33:57 2004 +0200
@@ -0,0 +1,90 @@
+
+(*<*) theory a4 = Main: (*>*)
+
+subsection {* Natural Deduction -- Predicate Logic; Sets as Lists *}
+
+
+subsubsection {* Predicate Logic Formulae *}
+
+text {*
+
+We are again talking about proofs in the calculus of Natural
+Deduction. In addition to the rules of section~\ref{psv0304a3}, you may now also use
+
+
+  @{text "exI:"}~@{thm exI[no_vars]}\\
+  @{text "exE:"}~@{thm exE[no_vars]}\\
+  @{text "allI:"}~@{thm allI[no_vars]}\\
+  @{text "allE:"}~@{thm allE[no_vars]}\\
+
+Give a proof of the following propositions or an argument why the formula is not valid:
+*}
+
+
+lemma "(\<exists>x. \<forall>y. P x y) \<longrightarrow> (\<forall>y. \<exists>x. P x y)"
+(*<*) oops (*>*)
+
+lemma "(\<forall>x. P x \<longrightarrow> Q) = ((\<exists>x. P x) \<longrightarrow> Q)"
+(*<*) oops (*>*)
+
+lemma "((\<forall> x. P x)  \<and> (\<forall> x. Q x)) = (\<forall> x. (P x \<and> Q x))"
+(*<*) oops (*>*)
+
+lemma "((\<forall> x. P x) \<or> (\<forall> x. Q x)) = (\<forall> x. (P x \<or> Q x))"
+(*<*) oops (*>*)
+
+lemma "((\<exists> x. P x) \<or> (\<exists> x. Q x)) = (\<exists> x. (P x \<or> Q x))"
+(*<*) oops (*>*)
+
+lemma "\<exists>x. (P x \<longrightarrow> (\<forall>x. P x))"
+(*<*) oops (*>*)
+
+
+subsubsection {* Sets as Lists *}
+
+text {* Finite sets can obviously be implemented by lists. In the
+following, you will be asked to implement the set operations union,
+intersection and difference and to show that these implementations are
+correct. Thus, for a function  *}
+
+(*<*) consts (*>*)
+  list_union :: "['a list, 'a list] \<Rightarrow> 'a list"
+
+text {* to be defined by you it has to be shown that *}
+
+lemma "set (list_union xs ys) = set xs \<union> set ys"
+(*<*) oops (*>*)
+
+
+text {* In addition, the functions should be space efficient in the
+sense that one obtains lists without duplicates (@{text "distinct"})
+whenever the parameters of the functions are duplicate-free. Thus, for
+example, *}
+
+
+lemma [rule_format]: 
+  "distinct xs \<longrightarrow> distinct ys \<longrightarrow> (distinct (list_union xs ys))"
+(*<*) oops (*>*)
+
+text {* \emph{Hint:} @{text "distinct"} is defined in @{text
+List.thy}. Also the function @{text mem} and the lemma @{text
+set_mem_eq} may be useful. *}
+
+
+subsubsection {* Quantification over Sets *}
+
+text {* Define a set @{text S} such that the following proposition holds: *}
+
+lemma "((\<forall> x \<in> A. P x) \<and> (\<forall> x \<in> B. P x)) \<longrightarrow> (\<forall> x \<in> S. P x)"
+(*<*) oops (*>*)
+
+
+text {* Define a predicate @{text P} such that *}
+
+lemma "\<forall> x \<in> A. P (f x) \<Longrightarrow>  \<forall> y \<in> f ` A. Q y"
+(*<*) oops (*>*)
+
+
+
+(*<*) end (*>*)
+
diff -r c770a2f0ea78 -r f08ea8e964d8 doc-src/Exercises/0304/a5/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/0304/a5/ROOT.ML	Tue Mar 30 19:33:57 2004 +0200
@@ -0,0 +1,1 @@
+  use_thy "a5";
diff -r c770a2f0ea78 -r f08ea8e964d8 doc-src/Exercises/0304/a5/a5.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/0304/a5/a5.thy	Tue Mar 30 19:33:57 2004 +0200
@@ -0,0 +1,91 @@
+
+(*<*) theory a5 = Main: (*>*)
+
+subsection {* The Euclidean Algorithm -- Inductively *}
+
+subsubsection {* Rules without Base Case *}
+
+text {* Show that the following
+*}
+
+consts evenempty :: "nat set"
+inductive evenempty
+  intros
+  Add2Ie: "n \<in> evenempty \<Longrightarrow> Suc(Suc n) \<in> evenempty"
+
+text {* defines the empty set: *}
+
+lemma evenempty_empty: "evenempty = {}"
+(*<*) oops (*>*)
+
+
+subsubsection {* The Euclidean Algorithm *}
+
+text {* Define inductively the set @{text gcd}, which characterizes
+the greatest common divisor of two natural numbers: *}
+
+(*<*)consts(*>*)
+  gcd :: "(nat \<times> nat \<times> nat) set"
+
+text {* Here, @{text "(a,b,g) \<in> gcd"} means that @{text g} is the gcd
+of @{text a} und @{text b}. The definition should closely follow the
+Euclidean algorithm.
+
+Reminder: The Euclidean algorithm repeatedly subtracts the smaller
+from the larger number, until one of the numbers is 0. Then, the other
+number is the gcd. *}
+
+text {* Now, compute the gcd of 15 and 10: *}
+lemma "(15, 10, ?g)  \<in> gcd"
+(*<*) oops (*>*)
+
+text {* How does your algorithm behave on special cases as the following?  *}
+lemma "(0, 0, ?g)  \<in> gcd"
+(*<*) oops (*>*)
+
+text {* Show that the gcd is really a divisor (for the proof, you need an appropriate lemma): *}
+
+lemma gcd_divides: "(a,b,g) \<in> gcd \<Longrightarrow> g dvd a \<and> g dvd b"
+(*<*) oops (*>*)
+
+text {* Show that the gcd is the greatest common divisor: *}
+
+lemma gcd_greatest [rule_format]: "(a,b,g) \<in> gcd \<Longrightarrow>
+  0 < a \<or> 0 < b \<longrightarrow> (\<forall> d. d dvd a \<longrightarrow> d dvd b \<longrightarrow> d \<le> g)"
+(*<*) oops (*>*)
+
+text {* Here as well, you will have to prove a suitable lemma. What is
+the precondition @{text "0 < a \<or> 0 < b"} good for?
+
+So far, we have only shown that @{text gcd} is correct, but your
+algorithm might not compute a result for all values @{text
+"a,b"}. Thus, show completeness of the algorithm: *}
+
+lemma gcd_defined: "\<forall> a b. \<exists> g. (a, b, g) \<in> gcd"
+(*<*) oops (*>*)
+
+text {* The following lemma, proved by course-of-value recursion over
+@{text n}, may be useful. Why does standard induction over natural
+numbers not work here?  *}
+
+lemma gcd_defined_aux [rule_format]: 
+  "\<forall> a b. (a + b) \<le> n \<longrightarrow> (\<exists> g. (a, b, g) \<in> gcd)"
+apply (induct rule: nat_less_induct)
+apply clarify
+
+(*<*) oops (*>*)
+
+text {* The idea is to show that @{text gcd} yields a result for all
+@{text "a, b"} whenever it is known that @{text gcd} yields a result
+for all @{text "a', b'"} whose sum is smaller than @{text "a + b"}.
+
+In order to prove this lemma, make case distinctions corresponding to
+the different clauses of the algorithm, and show how to reduce
+computation of @{text gcd} for @{text "a, b"} to computation of @{text
+gcd} for suitable smaller @{text "a', b'"}.
+
+*}
+
+
+(*<*) end (*>*)
+