Quelle  Star.thy

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

section‹The Reflexive Transitive Closure›

text‹\label{sec:rtc}
 index{reflexive transitive closure!defining inductively|(}%
  inductive definition may accept parameters, so it can express
  that yield sets.
  too can be defined inductively, since they are just sets of pairs.
  perfect example is the function that maps a relation to its
  transitive closure. This concept was already
  in \S\ref{sec:Relations}, where the operator ‹^*› was
  as a least fixed point because inductive definitions were not yet
 . But now they are:
 ›

inductive_set
  rtc :: "('a × 'a)set ==> ('a × 'a)set"   ("_*" [1000] 999)
  for r :: "('a × 'a)set"
where
  rtc_refl[iff]:  "(x,x) ∈ r*"
| rtc_step:       "[ (x,y) ∈ r; (y,z) ∈ r* ] ==> (x,z) ∈ r*"

text‹\noindent
  function term‹rtc› is annotated with concrete syntax: instead of
 ‹rtc r› we can write term‹r*›. The actual definition
  of two rules. Reflexivity is obvious and is immediately given the
 ‹iff› attribute to increase automation. The
  rule, @{thm[source]rtc_step}, says that we can always add one more
 term‹r›-step to the left. Although we could make @{thm[source]rtc_step} an
  rule, this is dangerous: the recursion in the second premise
  down and may even kill the automatic tactics.

  above definition of the concept of reflexive transitive closure may
  sufficiently intuitive but it is certainly not the only possible one:
  a start, it does not even mention transitivity.
  rest of this section is devoted to proving that it is equivalent to
  standard definition. We start with a simple lemma:
 ›

lemma [intro]: "(x,y) ∈ r ==> (x,y) ∈ r*"
by(blast intro: rtc_step)

text‹\noindent
  the lemma itself is an unremarkable consequence of the basic rules,
  has the advantage that it can be declared an introduction rule without the
  of killing the automatic tactics because term‹r*› occurs only in
  conclusion and not in the premise. Thus some proofs that would otherwise
  @{thm[source]rtc_step} can now be found automatically. The proof also
  that ‹blast› is able to handle @{thm[source]rtc_step}. But
  of the other automatic tactics are more sensitive, and even ‹blast› can be lead astray in the presence of large numbers of rules.

  prove transitivity, we need rule induction, i.e.\ theorem
 {thm[source]rtc.induct}:
 {thm[display]rtc.induct}
  says that ‹?P› holds for an arbitrary pair @{thm (prem 1) rtc.induct}
  ‹?P› is preserved by all rules of the inductive definition,
 .e.\ if ‹?P› holds for the conclusion provided it holds for the
 . In general, rule induction for an $n$-ary inductive relation $R$
  a premise of the form $(x@1,\dots,x@n) \in R$.

  we turn to the inductive proof of transitivity:
 ›

lemma rtc_trans: "[ (x,y) ∈ r*; (y,z) ∈ r* ] ==> (x,z) ∈ r*"
apply(erule rtc.induct)

txt‹\noindent
 , even the base case is a problem:
 {subgoals[display,indent=0,goals_limit=1]}
  have to abandon this proof attempt.
  understand what is going on, let us look again at @{thm[source]rtc.induct}.
  the above application of ‹erule›, the first premise of
 {thm[source]rtc.induct} is unified with the first suitable assumption, which
  term‹(x,y) ∈ r*› rather than term‹(y,z) ∈ r*›. Although that
  what we want, it is merely due to the order in which the assumptions occur
  the subgoal, which it is not good practice to rely on. As a result,
 ‹?xb› becomes term‹x›, ‹?xa› becomes
 term‹y› and ‹?P› becomes term‹λu v. (u,z) ∈ r*›, thus
  the above subgoal. So what went wrong?

  looking at the instantiation of ‹?P› we see that it does not
  on its second parameter at all. The reason is that in our original
 , of the pair term‹(x,y)› only term‹x› appears also in the
 , but not term‹y›. Thus our induction statement is too
 . Fortunately, it can easily be specialized:
  the additional premise prop‹(y,z)∈r*› into the conclusion:›
(*<*)oops(*>*)
lemma rtc_trans[rule_format]:
  "(x,y) ∈ r* ==> (y,z) ∈ r* ⟶ (x,z) ∈ r*"

txt‹\noindent
  is not an obscure trick but a generally applicable heuristic:
 begin{quote}\em
  proving a statement by rule induction on $(x@1,\dots,x@n) \in R$,
  all other premises containing any of the $x@i$ into the conclusion
  $\longrightarrow$.
 end{quote}
  similar heuristic for other kinds of inductions is formulated in
 S\ref{sec:ind-var-in-prems}. The ‹rule_format› directive turns
 ‹⟶› back into ‹==>›: in the end we obtain the original
  of our lemma.
 ›

apply(erule rtc.induct)

txt‹\noindent
  induction produces two subgoals which are both proved automatically:
 {subgoals[display,indent=0]}
 ›

 apply(blast)
apply(blast intro: rtc_step)
done

text‹
  us now prove that term‹r*› is really the reflexive transitive closure
  term‹r›, i.e.\ the least reflexive and transitive
  containing term‹r›. The latter is easily formalized
 ›

inductive_set
  rtc2 :: "('a × 'a)set ==> ('a × 'a)set"
  for r :: "('a × 'a)set"
where
  "(x,y) ∈ r ==> (x,y) ∈ rtc2 r"
| "(x,x) ∈ rtc2 r"
| "[ (x,y) ∈ rtc2 r; (y,z) ∈ rtc2 r ] ==> (x,z) ∈ rtc2 r"

text‹\noindent
  the equivalence of the two definitions is easily shown by the obvious rule
 :
 ›

lemma "(x,y) ∈ rtc2 r ==> (x,y) ∈ r*"
apply(erule rtc2.induct)
  apply(blast)
 apply(blast)
apply(blast intro: rtc_trans)
done

lemma "(x,y) ∈ r* ==> (x,y) ∈ rtc2 r"
apply(erule rtc.induct)
 apply(blast intro: rtc2.intros)
apply(blast intro: rtc2.intros)
done

text‹
  why did we start with the first definition? Because it is simpler. It
  only two rules, and the single step rule is simpler than
 . As a consequence, @{thm[source]rtc.induct} is simpler than
 {thm[source]rtc2.induct}. Since inductive proofs are hard enough
 , we should always pick the simplest induction schema available.
  term‹rtc› is the definition of choice.
 index{reflexive transitive closure!defining inductively|)}

 begin{exercise}\label{ex:converse-rtc-step}
  that the converse of @{thm[source]rtc_step} also holds:
 {prop[display]"[| (x,y) ∈ r*; (y,z) ∈ r |] ==> (x,z) ∈ r*"}
 end{exercise}
 begin{exercise}
  the development of this section, but starting with a definition of
 term‹rtc› where @{thm[source]rtc_step} is replaced by its converse as shown
  exercise~\ref{ex:converse-rtc-step}.
 end{exercise}
 ›
(*<*)
lemma rtc_step2[rule_format]: "(x,y) ∈ r* ==> (y,z) ∈ r ⟶ (x,z) ∈ r*"
apply(erule rtc.induct)
 apply blast
apply(blast intro: rtc_step)
done

end
(*>*)