(*<*) theory sol04 imports "~~/src/HOL/IMP/BExp" "~~/src/HOL/IMP/ASM" begin (*>*) text {* \ExerciseSheet{4}{3.~11.~2015} *} 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{Odd} The odd natural numbers can be specified by an inductive predicate: *} inductive odd :: "nat \ bool" where odd1: "odd 1" | oddSS: "odd n \ odd (n+2)" text \Prove, using Isar:\ lemma assumes "odd (n+2)" shows "odd n" (*<*) using assms proof cases case odd1 hence "False" by simp thus ?thesis .. next case (oddSS n') hence "n=n'" by simp thus ?thesis using \odd n'\ by simp qed (*>*) text {* \Exercise{Binary Trees with the Same Shape} Consider this datatype of binary trees: *} datatype tree = Leaf int | Node tree tree text {* Define an inductive binary predicate @{text "sameshape :: tree \ tree \ bool"}, where @{text "sameshape t\<^sub>1 t\<^sub>2"} means that @{text "t\<^sub>1"} and @{text "t\<^sub>2"} have exactly the same overall size and shape. (The elements in the corresponding leaves may be different.) *} inductive sameshape :: "tree \ tree \ bool" where (*<*) leaf: "sameshape (Leaf x) (Leaf y)" | node: "\sameshape l\<^sub>1 l\<^sub>2; sameshape r\<^sub>1 r\<^sub>2\ \ sameshape (Node l\<^sub>1 r\<^sub>1) (Node l\<^sub>2 r\<^sub>2)" (*>*) text {* Now prove that the @{text "sameshape"} relation is transitive. Use the @{text "inductive_cases"} command to get customized elimination rules, and try to make an automatic proof. (Try to prove the lemma with induction and auto first, to figure out which cases you need.) *} (*<*) inductive_cases sameshape_elims: "sameshape (Leaf x) t" "sameshape (Node l r) t" (*>*) theorem "\sameshape t\<^sub>1 t\<^sub>2; sameshape t\<^sub>2 t\<^sub>3\ \ sameshape t\<^sub>1 t\<^sub>3" (*<*) apply (induct t\<^sub>1 t\<^sub>2 arbitrary: t\<^sub>3 rule: sameshape.induct) apply (auto elim!: sameshape_elims intro: sameshape.intros) done (*>*) (*<*) theorem "\sameshape t\<^sub>1 t\<^sub>2; sameshape t\<^sub>2 t\<^sub>3\ \ sameshape t\<^sub>1 t\<^sub>3" proof (induction t\<^sub>1 t\<^sub>2 arbitrary: t\<^sub>3 rule: sameshape.induct) case (leaf x y) thus ?case proof cases case (leaf z) thus ?thesis by (simp add: sameshape.leaf) qed next case (node l1 l2 r1 r2) from node.prems show ?case proof (cases) case (node l3 r3) from node.IH(1)[OF \sameshape l2 l3\] have 1: "sameshape l1 l3" . from node.IH(2)[OF \sameshape r2 r3\] have 2: "sameshape r1 r3" . from sameshape.node[OF 1 2] show ?thesis using \t\<^sub>3 = Node l3 r3\ by simp qed qed theorem "\sameshape t\<^sub>1 t\<^sub>2; sameshape t\<^sub>2 t\<^sub>3\ \ sameshape t\<^sub>1 t\<^sub>3" proof (induction t\<^sub>1 t\<^sub>2 arbitrary: t\<^sub>3 rule: sameshape.induct) case (leaf x y) then obtain z where "t\<^sub>3 = Leaf z" by cases thus ?case by (simp add: sameshape.leaf) next case (node l1 l2 r1 r2) from node.prems obtain l3 r3 where [simp]: "t\<^sub>3=Node l3 r3" and "sameshape l2 l3" "sameshape r2 r3" by cases simp with node.IH have "sameshape l1 l3" "sameshape r1 r3" by blast+ thus ?case by (auto intro: sameshape.node) qed (*>*) (*<*) text "Alternative using functions" fun sameshape' where "sameshape' (Leaf x) (Leaf y) \ True" | "sameshape' (Node l1 r1) (Node l2 r2) \ sameshape' l1 l2 \ sameshape' r1 r2" | "sameshape' _ _ \ False" lemma "\sameshape' t1 t2; sameshape' t2 t3\ \ sameshape' t1 t3" apply (induct t1 arbitrary: t2 t3) apply (case_tac [!] t2) apply (case_tac [!] t3) apply auto done lemma "\sameshape' t1 t2; sameshape' t2 t3\ \ sameshape' t1 t3" apply (induct t1 t2 arbitrary: t3 rule: sameshape'.induct) apply (case_tac [!] t3) apply auto done (*>*) (*<*) end (*>*)