src/Doc/Tutorial/Inductive/Star.thy
 changeset 67406 23307fd33906 parent 58860 fee7cfa69c50 child 67613 ce654b0e6d69
--- a/src/Doc/Tutorial/Inductive/Star.thy	Thu Jan 11 13:48:17 2018 +0100
+++ b/src/Doc/Tutorial/Inductive/Star.thy	Fri Jan 12 14:08:53 2018 +0100
@@ -1,8 +1,8 @@
(*<*)theory Star imports Main begin(*>*)

-section{*The Reflexive Transitive Closure*}
+section\<open>The Reflexive Transitive Closure\<close>

-text{*\label{sec:rtc}
+text\<open>\label{sec:rtc}
\index{reflexive transitive closure!defining inductively|(}%
An inductive definition may accept parameters, so it can express
functions that yield sets.
@@ -12,7 +12,7 @@
introduced in \S\ref{sec:Relations}, where the operator @{text"\<^sup>*"} was
defined as a least fixed point because inductive definitions were not yet
available. But now they are:
-*}
+\<close>

inductive_set
rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set"   ("_*" [1000] 999)
@@ -21,7 +21,7 @@
rtc_refl[iff]:  "(x,x) \<in> r*"
| rtc_step:       "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"

-text{*\noindent
+text\<open>\noindent
The function @{term rtc} is annotated with concrete syntax: instead of
@{text"rtc r"} we can write @{term"r*"}. The actual definition
consists of two rules. Reflexivity is obvious and is immediately given the
@@ -36,12 +36,12 @@
for a start, it does not even mention transitivity.
The rest of this section is devoted to proving that it is equivalent to
-*}
+\<close>

lemma [intro]: "(x,y) \<in> r \<Longrightarrow> (x,y) \<in> r*"
by(blast intro: rtc_step)

-text{*\noindent
+text\<open>\noindent
Although the lemma itself is an unremarkable consequence of the basic rules,
it has the advantage that it can be declared an introduction rule without the
danger of killing the automatic tactics because @{term"r*"} occurs only in
@@ -61,12 +61,12 @@
expects a premise of the form $(x@1,\dots,x@n) \in R$.

Now we turn to the inductive proof of transitivity:
-*}
+\<close>

lemma rtc_trans: "\<lbrakk> (x,y) \<in> r*; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
apply(erule rtc.induct)

-txt{*\noindent
+txt\<open>\noindent
Unfortunately, even the base case is a problem:
@{subgoals[display,indent=0,goals_limit=1]}
We have to abandon this proof attempt.
@@ -85,12 +85,12 @@
goal, of the pair @{term"(x,y)"} only @{term x} appears also in the
conclusion, but not @{term y}. Thus our induction statement is too
general. Fortunately, it can easily be specialized:
-transfer the additional premise @{prop"(y,z):r*"} into the conclusion:*}
+transfer the additional premise @{prop"(y,z):r*"} into the conclusion:\<close>
(*<*)oops(*>*)
lemma rtc_trans[rule_format]:
"(x,y) \<in> r* \<Longrightarrow> (y,z) \<in> r* \<longrightarrow> (x,z) \<in> r*"

-txt{*\noindent
+txt\<open>\noindent
This is not an obscure trick but a generally applicable heuristic:
\begin{quote}\em
When proving a statement by rule induction on $(x@1,\dots,x@n) \in R$,
@@ -101,24 +101,24 @@
\S\ref{sec:ind-var-in-prems}. The @{text rule_format} directive turns
@{text"\<longrightarrow>"} back into @{text"\<Longrightarrow>"}: in the end we obtain the original
statement of our lemma.
-*}
+\<close>

apply(erule rtc.induct)

-txt{*\noindent
+txt\<open>\noindent
Now induction produces two subgoals which are both proved automatically:
@{subgoals[display,indent=0]}
-*}
+\<close>

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

-text{*
+text\<open>
Let us now prove that @{term"r*"} is really the reflexive transitive closure
of @{term r}, i.e.\ the least reflexive and transitive
relation containing @{term r}. The latter is easily formalized
-*}
+\<close>

inductive_set
rtc2 :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set"
@@ -128,10 +128,10 @@
| "(x,x) \<in> rtc2 r"
| "\<lbrakk> (x,y) \<in> rtc2 r; (y,z) \<in> rtc2 r \<rbrakk> \<Longrightarrow> (x,z) \<in> rtc2 r"

-text{*\noindent
+text\<open>\noindent
and the equivalence of the two definitions is easily shown by the obvious rule
inductions:
-*}
+\<close>

lemma "(x,y) \<in> rtc2 r \<Longrightarrow> (x,y) \<in> r*"
apply(erule rtc2.induct)
@@ -146,7 +146,7 @@
apply(blast intro: rtc2.intros)
done

-text{*
+text\<open>
So why did we start with the first definition? Because it is simpler. It
contains only two rules, and the single step rule is simpler than
transitivity.  As a consequence, @{thm[source]rtc.induct} is simpler than
@@ -164,7 +164,7 @@
@{term rtc} where @{thm[source]rtc_step} is replaced by its converse as shown
in exercise~\ref{ex:converse-rtc-step}.
\end{exercise}
-*}
+\<close>
(*<*)
lemma rtc_step2[rule_format]: "(x,y) : r* \<Longrightarrow> (y,z) : r --> (x,z) : r*"
apply(erule rtc.induct)