(*<*)
theory Exercise
imports Main
begin
(*>*)


section {* Permutations of Lists *}

text {*

\newcommand{\Perm}{\mathop{\textbf{Perm}}}

In this exercise we consider lists (over an arbitrary element type).
The cons operation is denoted by $x \cdot xs$, $|xs|$ is the length of
$xs$ and $xs_i$ the $i$th element.

Permutations of lists are defined inductively by the following four rules.

\[
\begin{array}{c@ {\quad}l@ {\qquad}c@ {\quad}l}
  ([], []) \in \Perm & \text{(Nil)} &
  (x \cdot y \cdot l, y \cdot x \cdot l) \in \Perm & \text{(Swap)} \\[2ex]
  \inferrule{(xs, ys) \in \Perm}{(z\cdot xs, z\cdot ys) \in \Perm}
  & \text{(Cons)} &
  \inferrule{(xs, ys) \in \Perm \\ (ys, zs) \in \Perm}{%
    (xs, zs) \in \Perm} & \text{(Trans)}
\end{array}
\]
The defined set $\Perm$ contains pairs of lists.  In each pair the
lists only in the order of elements.

$\rhd$ State the induction rule and prove the following statements (on
paper).
\begin{enumerate}
\item[a)]
  For $(xs, ys) \in \Perm$ holds: $xs$ and $ys$ have equal length.

\item[b)]
  For $(xs, ys) \in \Perm$ holds: there is a permutation $\pi$ of
  numbers $1 \ldots |xs|$, such that $xs_i = ys_{\pi(i)}$ for all $i =
  1 \ldots |xs|$.
\end{enumerate}

*}


section {* Rule Induction *}

text {*
  Formalise part of the lecture on inductive sets in Isabelle.

  We define a predicate @{term "closed f A"},
  where @{term [show_types] "f :: 'a set \<Rightarrow> 'a set"} and @{term
  [show_types] "A :: 'a set"}.
*}

definition closed :: "('a set \<Rightarrow> 'a set) \<Rightarrow> 'a set \<Rightarrow> bool"
  where "closed f A \<equiv> f A \<subseteq> A"

text {*
  $\rhd$ Show @{term "closed f A \<and> closed f B \<Longrightarrow> closed f
  (A \<inter> B)"} if @{term "f"} is monotone (the predicate @{term "mono"}
  is predefined).  *}

text {*
  $\rhd$ Define a function @{term lfpt} mapping @{term f} to the
  intersection of all @{term f}-closed sets.  *}

text {*
  $\rhd$ Show that @{term "lfpt f"} is a fixed point of @{term "f"} if
  @{term "f"} is monotone.
*}

text {*
  $\rhd$ Show that @{term "lfpt f"} is the least fixpoint of @{term "f"}.
*}

text {*
  We now declare a constant @{term [show_types] "R :: ('a set \<times> 'a)
  set"}.  This is the set of rules, which will not be further
  specified here.
*}

consts R :: "('a set \<times> 'a) set"

text {*
  Then we define @{term [show_types] "Rhat :: 'a set => 'a set"} in terms of
  @{term "R"}.
*}

definition Rhat :: "'a set \<Rightarrow> 'a set"
  where "Rhat B \<equiv> {x. \<exists>H. (H,x) \<in> R \<and> H \<subseteq> B}"

text {*
  $\rhd$ Show soundness of rule induction using @{term "R"} and @{term "lfpt
  Rhat"}.
*}


section {* Two Grammars *}

text{*
  The most natural definition of valid sequences of parentheses is
  this: \[ S \quad\to\quad \epsilon \quad\mid\quad '('~S~')'
  \quad\mid\quad S~S \] where $\epsilon$ is the empty word.

  A second, somewhat unusual grammar is the following one: \[ T
  \quad\to\quad \epsilon \quad\mid\quad T~'('~T~')' \]
*}

text {*
  $\rhd$ Model both grammars as inductive sets $S$ and $T$ and prove, on
  paper and using rule inducion, $S = T$.
*}

(*<*)
end
(*>*)