(* \$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 (*>*)