section \<open>Solutions for Session 6\<close>

theory Solutions06
  imports Demo06
begin

subsection \<open>Exercise 1\<close>

text \<open>
Prove that the inductive definition @{const is_odd} is equivalent to
the standard one given by @{const odd}.
\<close>

lemma
  shows even_is_odd_Suc: "even x \<Longrightarrow> is_odd (Suc x)"
    and odd_is_odd: "odd x \<Longrightarrow> is_odd x"
  by (induction x) (auto intro: is_odd.intros)

lemma "odd x \<longleftrightarrow> is_odd x"
  by (auto simp: odd_is_odd is_odd_odd)


subsection \<open>Exercise 2\<close>

text \<open>
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.
\<close>

lemma star_imp_star_star:
  assumes "(x, y) \<in> star R"
  shows "(x, y) \<in> star (star R)"
  using assms by (auto intro: star.intros)

lemma star_star_imp_star:
  assumes "(x, y) \<in> star (star R)"
  shows "(x, y) \<in> 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 \<open>Exercise 3\<close>

text \<open>
Implement a function \<open>le\<close> that given a natural number \<open>n\<close> together with a list of
natural numbers \<open>xs\<close>, checks whether \<open>n\<close> is less than or equal to all elements of \<open>xs\<close>.

Using \<open>le\<close>, give an inductive predicate \<open>is_sorted\<close> that checks whether a list of
natural numbers is sorted.

Give an alternative definition \<open>is_sorted'\<close> as a recursive function.

Finally, prove that both definitions are equivalent.
\<close>

fun le :: "nat \<Rightarrow> nat list \<Rightarrow> bool"
  where
    "le x [] \<longleftrightarrow> True"
  | "le x (y # ys) \<longleftrightarrow> x \<le> y \<and> le x ys"

inductive is_sorted :: "nat list \<Rightarrow> bool"
  where
    Nil [simp]: "is_sorted []"
  | Cons: "le x xs \<Longrightarrow> is_sorted xs \<Longrightarrow> is_sorted (x # xs)"

fun is_sorted' :: "nat list \<Rightarrow> bool"
  where
    "is_sorted' [] \<longleftrightarrow> True"
  | "is_sorted' (x # xs) \<longleftrightarrow> le x xs \<and> 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