(*<*)
theory Solution
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 differ in the order of elements.

$\rhd$ State the induction rule and prove the following statements (on
paper).

The induction rule consists of two bases cases and two induction
steps.  For $(xs, ys) \in \Perm \Rightarrow P(xs,ys)$ for some
property $P$ one needs to show:


\begin{itemize}
\item Base cases:
\begin{description}
\item[Nil: \ \  \ ] $P([], [])$
\item[Swap: ] $\forall x,y,l. \ P(x\cdot y\cdot l,y\cdot x\cdot l)$
\end{description}
\item{Induction steps}
\begin{description}
\item[Cons: ] $\forall xs,ys,z. \ P(xs,ys) \Rightarrow P(z\cdot xs,z\cdot ys)$
\item[Trans:] $\forall xs,ys,zs. \ P(xs,ys) \wedge P(ys,zs) \Rightarrow P(xs,zs)$
\end{description}
\end{itemize}

\begin{enumerate}
\item[a)]
  For $(xs, ys) \in \Perm$ holds: $xs$ and $ys$ have equal length.

To be shown: $(xs,ys) \in \Perm \Rightarrow |xs| = |ys|$. \\
Applying the induction rule yields four statements to be shown:
\begin{description}
\item[Nil: \ \ \ ] $|[]| = |[]| \ \surd$
\item[Swap: ] $|x\cdot y\cdot l| = |y\cdot x\cdot l| \ \surd$
\item[Cons: ] Induction hypothesis: $|xs| = |ys|$\\
	From this the following is immediate: $|z\cdot xs| = |xs| + 1 \stackrel{\rm IH}{=} |ys| + 1 = |z\cdot ys|$.
\item[Trans:] Induction hypothesis: $|xs| = |ys|, |ys| = |zs|$\\
	By transitivity of equality: $|xs| = |zs|$
\end{description}

\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|$.

By rule induction we again obtain four statements, which are to be shown:
\begin{description}
\item[Nil: \ \ \ ]
  There is a permutation $\pi$ with $[]_i = []_{\pi(i)}$.  This is
  trivial since the list is empty.

\item[Swap: ]
  There is a permuation $\pi$ with $(x \cdot y \cdot l)_i = (y \cdot
  x \cdot l)_{\pi(i)}$.  This holds for $\pi = (1 2)$.

\item[Cons: ]
  The induction hypothesis says that there exists a permutation $\pi$
  with $xs_i = ys_{\pi(i)}$ for all $i$ (from 1 to $|xs|$).

  From this we obtain a permuation $\tau$ by setting $\tau(1) := 1$
  and $\tau(i) := \pi(i-1)+1$ für $i > 1$.  We have $(z\cdot xs)_i =
  (z\cdot ys)_{\tau(i)}$.

\item[Trans:]
  Induction hypothesis: there is a permutation $\pi$ with $xs_i =
  ys_{\pi(i)}$ for all $i$ and a permutation $\tau$ with $ys_i =
  zs_{\tau(i)}$ for all $i$.

  Then $\tau \circ \pi$ is also a permutation, and $xs_i =
  zs_{\tau(\pi(i))}$.

\end{description}

\end{enumerate}

*}


section {* Rule Induction *}

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

  $\rhd$ 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).  *}

lemma closed_int:
  "\<lbrakk> mono f; closed f A; closed f B \<rbrakk> \<Longrightarrow> closed f (A \<inter> B)"
  by (unfold closed_def mono_def) blast

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

definition lfpt :: "('a set \<Rightarrow> 'a set) \<Rightarrow> 'a set"
  where "lfpt f \<equiv> \<Inter> {B. closed f B}"

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

lemma lfpt_lower: "closed f B \<Longrightarrow> lfpt f \<subseteq> B"
  by (unfold lfpt_def) auto

lemma lfpt_greatest:
  assumes A_smaller: "\<And>B. closed f B \<Longrightarrow> A \<subseteq> B"
  shows "A \<subseteq> lfpt f"
  by (unfold lfpt_def) (blast dest: A_smaller)

lemma 1:
  "mono f \<Longrightarrow> f (lfpt f) \<subseteq> lfpt f"
  apply (rule lfpt_greatest)
  apply (rule subset_trans)
   apply (erule monoD)
   apply (erule lfpt_lower)
  apply (unfold closed_def)
  apply assumption
  done

lemma 2:
  "mono f \<Longrightarrow> lfpt f \<subseteq> f (lfpt f)"
  apply (rule lfpt_lower)
  apply (unfold closed_def)
  apply (rule monoD, assumption)
  apply (rule 1, assumption)
  done

lemma lfpt_fixpoint:
  "mono f \<Longrightarrow> f (lfpt f) = lfpt f"
  by (blast intro!: 1 2)

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

lemma lfpt_least:
  assumes A: "A = f A"
  shows "lfpt f \<subseteq> A"
proof -
  from A have "closed f A" by (unfold closed_def) blast
  then show "lfpt f \<subseteq> A" by (rule lfpt_lower)
qed

text {*
  $\rhd$ 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 {*
  $\rhd$ 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"}.
*}

lemma monoRhat: "mono Rhat"
  by (unfold mono_def Rhat_def) blast

text {*
  Soundness of \emph{rule induction} means that if some predicate
  @{term "P"} can be verified by rule induction, then @{term "P"}
  holds for all elements of the set (constructed as least fixed
  point).
*}

lemma soundness:
  assumes hyp: "\<forall>(H,x) \<in> R. ((\<forall>h \<in> H. P h) \<longrightarrow> P x)"
  shows "\<forall>x \<in> lfpt Rhat. P x"
proof -
  from hyp have "closed Rhat {x. P x}"
    by (unfold closed_def Rhat_def) blast
  then have "lfpt Rhat \<subseteq> {x. P x}" by (rule lfpt_lower)
  then show ?thesis by blast
qed


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$.
*}

text {*
  The inductive definitions are
\[
\begin{array}{c@ {\quad}l@ {\qquad}c@ {\quad}l@ {\qquad}c@ {\quad}l}
  \varepsilon \in S & \text{(S1)} &
  \inferrule{w \in S}{(w) \in S} & \text{(S2)} &
  \inferrule{v \in S \\ w \in S}{vw \in S} & \text{(S3)}
\end{array}
\]
and
\[
\begin{array}{c@ {\quad}l@ {\qquad}c@ {\quad}l}
  \varepsilon \in T & \text{(T1)} &
  \inferrule{v \in T \\ w \in T}{v(w) \in T} & \text{(T23)}
\end{array}
\]
In order to show $S = T$ we show that $S$ is contained in $T$ and $T$
in $S$.  The latter is simpler, hence it is shown first.

In order to show $T \subseteq S$ we show that for any $x$, $x \in T \Longrightarrow x \in S$ by rule induction for the set $T$.
\begin{description}
\item[T1:] $\varepsilon \in S \quad \surd$
\item[T23:] Induction hypothesis: $v \in S, w \in S$.

  We need to show that $v(w) \in S$, which follows from the induction
  hypothesis by the following inference:
  \[
    \inferrule*[Right=(S3)]{v \in S \\ \inferrule*[Right=(S2)]{w \in S}{(w) \in S}}{v(w) \in S}
  \]
\end{description}

For the direction $S \subseteq T$ we use the lemma (shown below).
\[
  \inferrule*[Right=(T3)]{v \in T \\ w \in T}{vw \in T}
\]
Similar to the before, we show that for any $x$, $x \in S \Longrightarrow x \in T$, this time by rule induction for the set $S$.
\begin{description}
\item[S1:] $\varepsilon \in T \quad \surd$
\item[S2:] Induction hypothesis: $w \in T$.

  Show that $(w) \in T$.  This follows from the induction hypothesis by (T23) where $v = \varepsilon$.
\item[S3:] Induction hypothesis: $v \in T, w \in T$.

  Show that $vw \in T$.  Immediate with (T3).
\end{description}

\textbf{Proof of Lemma~(T3).}

Following the scheme of the lecture, the induction rule for $T$ is the theorem
\[
  \inferrule*{x \in T \\ P \, \varepsilon \\
    \inferrule*{P \, v \\ P \, w}{P \, v(w)}}{P \, x}
\]
By setting $P \, x \: \equiv \: x \in T \land Q \, x$ for an arbitrary predicate $Q$ we obtain this stronger version of the induction rule:
\[
  \inferrule*{x \in T \\ Q \, \varepsilon \\
    \inferrule*{v \in T \\ Q \, v \\ w \in T \\Q \, w}{Q \, v(w)}}{Q \, x}
\]
This is the rule that Isabelle derives.  This rule is used in the proof of (T3).  We will use the additional induction hypotheses in the proof of (T3).  We show $vw \in T$ by rule induction on the second premise $w \in T$:
\begin{description}
\item[T1] $w = \varepsilon$

  Show $v\varepsilon \in T$.  This follows from the first premise $v \in T$.
\item[T23] $w = v'(w')$

  Show $vv'(w') \in T$.  By induction hypothesis $vv' \in T, vw' \in T$.  By induction hypothesis of the stronger induction rule also $v' \in T, w' \in T$.  The goal is shown by (T23) from $vv' \in T$ and $w' \in T$.
\end{description}
*}

(*<*)
end
(*>*)