(*<*) theory ex04 imports "~~/src/HOL/IMP/BExp" "~~/src/HOL/IMP/ASM" begin (*>*) text {* \ExerciseSheet{4}{5.~11.~2013} *} text {* \Exercise{Reflexive Transitive Closure} A binary relation is expressed by a predicate of type @{text "R :: 's \ 's \ bool"}. Intuitively, @{text "R s t"} represents a single step from state @{text "s"} to state @{text "t"}. The reflexive, transitive closure @{text "R\<^sup>*"} of @{text "R"} is the relation that contains a step @{text "R\<^sup>* s t"}, iff @{text "R"} can step from @{text "s"} to @{text "t"} in any number of steps (including zero steps). Formalize the reflexive transitive closure as inductive predicate: *} inductive star :: "('a \ 'a \ bool) \ 'a \ 'a \ bool" (*<*) for r where refl: "star r x x" | step: "r x y \ star r y z \ star r x z" (*>*) text {* When doing so, you have the choice to append or prepend a step. In any case, the following two lemmas should hold for your definition: *} lemma star_prepend: "\r x y; star r y z\ \ star r x z" (*<*) by (rule step) (*>*) lemma star_append: "\ star r x y; r y z \ \ star r x z" (*<*) by (induct rule: star.induct) (auto intro: star.intros) (*>*) text {* Now, formalize the star predicate again, this time the other way round: *} inductive star' :: "('a \ 'a \ bool) \ 'a \ 'a \ bool" (*<*) for r where refl': "star' r x x" | step': "\star' r x y; r y z\ \ star' r x z" (*>*) (*<*) lemma star'_prepend: "\star' r y z; r x y\ \ star' r x z" apply (induction rule: star'.induct) apply (auto intro: star'.intros) done (*>*) text {* Prove the equivalence of your two formalizations *} lemma "star r x y = star' r x y" (*<*) proof assume "star r x y" thus "star' r x y" by induct (auto intro: star'.intros star'_prepend) next assume "star' r x y" thus "star r x y" by induct (auto intro: star.intros star_append) qed (*>*) text {* Hint: The induction method expects the assumption about the inductive predicate to be first. *} text {* \Exercise{Rule Inversion} Recall the evenness predicate @{text "ev"} from the lecture: *} inductive ev :: "nat \ bool" where ev0: "ev 0" | evSS: "ev n \ ev (Suc (Suc n))" text {* Prove the converse of rule @{text "evSS"} using rule inversion. Hint: There are two ways to proceed. First, you can write a structured Isar-style proof using the @{text "cases"} method: *} lemma "ev (Suc (Suc n)) \ ev n" proof - assume "ev (Suc (Suc n))" then show "ev n" by cases qed text {* Alternatively, you can write a more automated proof by using the elimination rules. These rules can then be used with ``@{text "auto elim:"}''. (If given the @{text "[elim]"} attribute, @{text "auto"} will use them by default.) *} (*<*) lemma "ev (Suc (Suc n)) \ ev n" by (auto elim: ev.cases) (*>*) text {* Next, prove that the natural number three (@{text "Suc (Suc (Suc 0))"}) is not even. Hint: You may proceed either with a structured proof, or with an automatic one. An automatic proof may require additional elimination rules from \textbf{inductive\_cases}. *} lemma "\ ev (Suc (Suc (Suc 0)))" (*<*) proof assume "ev (Suc (Suc (Suc 0)))" then show "False" proof (cases) assume "ev (Suc 0)" then show "False" proof (cases) qed qed qed lemma "\ ev (Suc (Suc (Suc 0)))" by (auto elim: ev.cases) (*>*) (*<*) end (*>*)