section \Solutions for Session 6\ theory Solutions06 imports Demo06 begin subsection \Exercise 1\ text \ Prove that the inductive definition @{const is_odd} is equivalent to the standard one given by @{const odd}. \ lemma shows even_is_odd_Suc: "even x \ is_odd (Suc x)" and odd_is_odd: "odd x \ is_odd x" by (induction x) (auto intro: is_odd.intros) lemma "odd x \ is_odd x" by (auto simp: odd_is_odd is_odd_odd) subsection \Exercise 2\ text \ Prove that taking the reflexive transitive closure of a relation is idempotent, that is, applying the operation twice has the same effect as applying it just once. \ lemma star_imp_star_star: assumes "(x, y) \ star R" shows "(x, y) \ star (star R)" using assms by (auto intro: star.intros) lemma star_star_imp_star: assumes "(x, y) \ star (star R)" shows "(x, y) \ star R" using assms by (induction) (auto intro: star_trans) lemma star_star_idemp: "star (star R) = star R" (* apply (auto simp: star_star_imp_star star_imp_star_star) (*loop!*)*) by (auto simp: star_star_imp_star intro: star_imp_star_star) subsection \Exercise 3\ text \ Implement a function \le\ that given a natural number \n\ together with a list of natural numbers \xs\, checks whether \n\ is less than or equal to all elements of \xs\. Using \le\, give an inductive predicate \is_sorted\ that checks whether a list of natural numbers is sorted. Give an alternative definition \is_sorted'\ as a recursive function. Finally, prove that both definitions are equivalent. \ fun le :: "nat \ nat list \ bool" where "le x [] \ True" | "le x (y # ys) \ x \ y \ le x ys" inductive is_sorted :: "nat list \ bool" where Nil [simp]: "is_sorted []" | Cons: "le x xs \ is_sorted xs \ is_sorted (x # xs)" fun is_sorted' :: "nat list \ bool" where "is_sorted' [] \ True" | "is_sorted' (x # xs) \ le x xs \ is_sorted' xs" lemma is_sorted_imp_sorted': assumes "is_sorted xs" shows "is_sorted' xs" using assms by (induction) (auto) lemma is_sorted'_imp_is_sorted: assumes "is_sorted' xs" shows "is_sorted xs" using assms by (induction xs) (auto intro: is_sorted.intros) lemma is_sorted'_is_sorted_conv: "is_sorted' xs = is_sorted xs" by (auto simp: is_sorted_imp_sorted' is_sorted'_imp_is_sorted) end