doc-src/TutorialI/Sets/sets.tex

 Unions can be formed over the values of a given  set.  The syntax is
 \mbox{\isa{\isasymUnion x\isasymin A.\ B}} or \isa{UN
 x\isasymin A.\ B} in \textsc{ascii}. Indexed union satisfies this basic law:
 \begin{isabelle}
 (b\ \isasymin\
-(\isasymUnion x\isasymin A.\ B\ x))\ =\ (\isasymexists x\isasymin A.\
+(\isasymUnion \isactrlbsub x\isasymin A\isactrlesub \ B\ x) =\ (\isasymexists x\isasymin A.\
 b\ \isasymin\ B\ x)
 \rulenamedx{UN_iff}
 \end{isabelle}
 It has two natural deduction rules similar to those for the existential
 quantifier.  Sometimes \isa{UN_I} must be applied explicitly:
 \begin{isabelle}
 \isasymlbrakk a\ \isasymin\
 A;\ b\ \isasymin\
 B\ a\isasymrbrakk\ \isasymLongrightarrow\
 b\ \isasymin\
-({\isasymUnion}x\isasymin A.\
-B\ x)
+(\isasymUnion \isactrlbsub x\isasymin A\isactrlesub \ B\ x)
 \rulenamedx{UN_I}%
 \isanewline
 \isasymlbrakk b\ \isasymin\
-({\isasymUnion}x\isasymin A.\
-B\ x);\
+(\isasymUnion \isactrlbsub x\isasymin A\isactrlesub \ B\ x);\
 {\isasymAnd}x.\ {\isasymlbrakk}x\ \isasymin\
 A;\ b\ \isasymin\
 B\ x\isasymrbrakk\ \isasymLongrightarrow\
 R\isasymrbrakk\ \isasymLongrightarrow\ R%
 \rulenamedx{UN_E}

 The following built-in syntax translation (see {\S}\ref{sec:syntax-translations})
 lets us express the union over a \emph{type}:
 \begin{isabelle}
 \ \ \ \ \
 ({\isasymUnion}x.\ B\ x)\ {\isasymrightleftharpoons}\
-({\isasymUnion}x{\isasymin}UNIV.\ B\ x)
+({\isasymUnion}\isactrlbsub x{\isasymin}UNIV\isactrlesub\ B\ x)
 \end{isabelle}
 %Abbreviations work as you might expect.  The term on the left-hand side of
 %the \isasymrightleftharpoons\ symbol is automatically translated to the right-hand side when the
 %term is parsed, the reverse translation being done when the term is
 %displayed.

 than unions.  The syntax below would be \isa{INT
 x:\ A.\ B} and \isa{Inter\ C} in \textsc{ascii}.  Among others, these
 theorems are available:
 \begin{isabelle}
 (b\ \isasymin\
-({\isasymInter}x\isasymin A.\
-B\ x))\
+(\isasymInter \isactrlbsub x\isasymin A\isactrlesub \ B\ x))\
 =\
 ({\isasymforall}x\isasymin A.\
 b\ \isasymin\ B\ x)
 \rulenamedx{INT_iff}%
 \isanewline

 is perhaps the best-known concept defined as a
 greatest fixed point.  Exhibiting a bisimulation to prove the equality of
 two agents in a process algebra is an example of coinduction.
 The coinduction rule can be strengthened in various ways.
 \index{fixed points|)}
+
+%The section "Case Study: Verified Model Checking" is part of this chapter
+\input{CTL/ctl}  
+\endinput