(*
This file contains the source text of the first exercise, along with a skeleton
theory for you to build on. The markup you see below integrates text with the
Isabelle theory elements, and in some cases, hiding Isabelle elements so that
they don't appear in the typeset document.
Feel free to delete this markup as you complete the exercises, or alternatively,
to extend the markup with commentary on your solutions.
*)
header {* Replace, Reverse and Delete *}
(*<*) theory replace_ex imports Main begin (*>*)
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 counterexample) 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 counterexample) 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(*>*)
text {*
\newpage*}
(*<*)
end
(*>*)