(*
$Id: ex.thy,v 1.2 2004/11/23 15:14:34 webertj Exp $
Author: Gerwin Klein
*)
header {* Quantifying Lists *}
(*<*) theory ex imports Main begin (*>*)
text {* Define a universal and an existential quantifier on lists
using primitive recursion. 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 counterexample) 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 (non-trivial) 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 primitive-recursive function @{term "is_in x xs"} that
checks if @{term x} occurs in @{term xs}. Now express
@{text is_in} via @{term exs}:
*}
lemma "is_in a xs = Z"
(*<*)oops(*>*)
text {* Define a primitive-recursive 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 counterexample) the following theorems.
*}
lemma "length (deldups xs) <= length xs"
(*<*)oops(*>*)
lemma "nodups (deldups xs)"
(*<*)oops(*>*)
lemma "deldups (rev xs) = rev (deldups xs)"
(*<*)oops(*>*)
(*<*) end (*>*)