--- a/doc-src/Exercises/2003/a1/a1.thy Fri Apr 29 18:13:28 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,88 +0,0 @@
-(*<*)
-theory a1 = Main:
-(*>*)
-subsection {* Lists *}
-
-text{*
-Define a function @{term occurs}, such that @{term"occurs x xs"}
-is the number of occurrences of the element @{term x} in the list
-@{term xs}.
-*}
-
-(*<*) consts (*>*)
- occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat"
-
-text {*
-Prove or disprove (by counter example) the theorems that follow. 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.
-
-In the case of a non-theorem try to find a suitable assumption under which the theorem holds. *};
-
-theorem "occurs a (xs @ ys) = occurs a xs + occurs a ys "
-(*<*)oops(*>*)
-
-theorem "occurs a xs = occurs a (rev xs)"
-(*<*)oops(*>*)
-
-theorem "occurs a xs <= length xs"
-(*<*)oops(*>*)
-
-theorem "occurs a (replicate n a) = n"
-(*<*)oops(*>*)
-
-text{*
-Define a function @{term areAll}, such that @{term"areAll xs x"} is true iff all elements of @{term xs} are equal to @{term x}.
-*}
-(*<*) consts (*>*)
- areAll :: "'a list \<Rightarrow> 'a \<Rightarrow> bool"
-
-theorem "areAll xs a \<longrightarrow> occurs a xs = length xs"
-(*<*)oops(*>*)
-
-theorem "occurs a xs = length xs \<longrightarrow> areAll xs a"
-(*<*)oops(*>*)
-
-text{*
-Define two functions to delete elements from a list:
-@{term"del1 x xs"} deletes the first (leftmost) occurrence of @{term x} from @{term xs}.
-@{term"delall x xs"} deletes all occurrences of @{term x} from @{term xs}.
-*}
-(*<*) consts (*>*)
- delall :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
- del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
-
-theorem "occurs a (delall a xs) = 0"
-(*<*)oops(*>*)
-theorem "Suc (occurs a (del1 a xs)) = occurs a xs"
-(*<*)oops(*>*)
-
-text{*
-Define a function @{term replace}, such that @{term"replace x y zs"} yields @{term zs} with every occurrence of @{term x} replaced by @{term y}.
-*}
-(*<*) consts (*>*)
- replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
-
-theorem "occurs a xs = occurs b (replace a b xs)"
-(*<*)oops(*>*)
-
-text{*
-With the help of @{term occurs}, define a function @{term remDups} that removes all duplicates from a list.*}
-(*<*) consts (*>*)
- remDups :: "'a list \<Rightarrow> 'a list"
-text{* Use @{term occurs} to formulate and prove a lemma that expresses the fact that @{term remDups} never inserts a new element into a list.*}
-
-text{* Use @{term occurs} to formulate and prove a lemma that expresses the fact that @{term remDups} always returns a list without duplicates (i.e.\ the correctness of @{term remDups}).
-*}
-
-text{*
-Now, with the help of @{term occurs} define a function @{term unique}, such that @{term"unique xs"} is true iff every element in @{term xs} occurs only once.
-*}
-(*<*) consts (*>*)
- unique :: "'a list \<Rightarrow> bool"
-
-text{*
-Formulate and prove the correctness of @{term remDups} with the help of @{term unique}.
-*}
-(*<*) end (*>*)