17914

1 
(*<*)theory CTLind imports CTL begin(*>*)

10218

2 

10885

3 
subsection{*CTL Revisited*}

10218

4 


5 
text{*\label{sec:CTLrevisited}

11494

6 
\index{CTL(}%


7 
The purpose of this section is twofold: to demonstrate


8 
some of the induction principles and heuristics discussed above and to

10281

9 
show how inductive definitions can simplify proofs.

10218

10 
In \S\ref{sec:CTL} we gave a fairly involved proof of the correctness of a

10795

11 
model checker for CTL\@. In particular the proof of the

10218

12 
@{thm[source]infinity_lemma} on the way to @{thm[source]AF_lemma2} is not as

11494

13 
simple as one might expect, due to the @{text SOME} operator

10281

14 
involved. Below we give a simpler proof of @{thm[source]AF_lemma2}


15 
based on an auxiliary inductive definition.

10218

16 


17 
Let us call a (finite or infinite) path \emph{@{term A}avoiding} if it does


18 
not touch any node in the set @{term A}. Then @{thm[source]AF_lemma2} says


19 
that if no infinite path from some state @{term s} is @{term A}avoiding,


20 
then @{prop"s \<in> lfp(af A)"}. We prove this by inductively defining the set


21 
@{term"Avoid s A"} of states reachable from @{term s} by a finite @{term


22 
A}avoiding path:

10241

23 
% Second proof of opposite direction, directly by wellfounded induction

10218

24 
% on the initial segment of M that avoids A.


25 
*}


26 

23733

27 
inductive_set


28 
Avoid :: "state \<Rightarrow> state set \<Rightarrow> state set"


29 
for s :: state and A :: "state set"


30 
where


31 
"s \<in> Avoid s A"


32 
 "\<lbrakk> t \<in> Avoid s A; t \<notin> A; (t,u) \<in> M \<rbrakk> \<Longrightarrow> u \<in> Avoid s A";

10218

33 


34 
text{*


35 
It is easy to see that for any infinite @{term A}avoiding path @{term f}

12492

36 
with @{prop"f(0::nat) \<in> Avoid s A"} there is an infinite @{term A}avoiding path

15904

37 
starting with @{term s} because (by definition of @{const Avoid}) there is a

12492

38 
finite @{term A}avoiding path from @{term s} to @{term"f(0::nat)"}.


39 
The proof is by induction on @{prop"f(0::nat) \<in> Avoid s A"}. However,

10218

40 
this requires the following


41 
reformulation, as explained in \S\ref{sec:indvarinprems} above;


42 
the @{text rule_format} directive undoes the reformulation after the proof.


43 
*}


44 


45 
lemma ex_infinite_path[rule_format]:


46 
"t \<in> Avoid s A \<Longrightarrow>


47 
\<forall>f\<in>Paths t. (\<forall>i. f i \<notin> A) \<longrightarrow> (\<exists>p\<in>Paths s. \<forall>i. p i \<notin> A)";


48 
apply(erule Avoid.induct);


49 
apply(blast);


50 
apply(clarify);


51 
apply(drule_tac x = "\<lambda>i. case i of 0 \<Rightarrow> t  Suc i \<Rightarrow> f i" in bspec);

12815

52 
apply(simp_all add: Paths_def split: nat.split);

10218

53 
done


54 


55 
text{*\noindent

11494

56 
The base case (@{prop"t = s"}) is trivial and proved by @{text blast}.

10218

57 
In the induction step, we have an infinite @{term A}avoiding path @{term f}


58 
starting from @{term u}, a successor of @{term t}. Now we simply instantiate


59 
the @{text"\<forall>f\<in>Paths t"} in the induction hypothesis by the path starting with


60 
@{term t} and continuing with @{term f}. That is what the above $\lambda$term

10885

61 
expresses. Simplification shows that this is a path starting with @{term t}


62 
and that the instantiated induction hypothesis implies the conclusion.

10218

63 

11196

64 
Now we come to the key lemma. Assuming that no infinite @{term A}avoiding

11277

65 
path starts from @{term s}, we want to show @{prop"s \<in> lfp(af A)"}. For the


66 
inductive proof this must be generalized to the statement that every point @{term t}

11494

67 
``between'' @{term s} and @{term A}, in other words all of @{term"Avoid s A"},

11196

68 
is contained in @{term"lfp(af A)"}:

10218

69 
*}


70 


71 
lemma Avoid_in_lfp[rule_format(no_asm)]:


72 
"\<forall>p\<in>Paths s. \<exists>i. p i \<in> A \<Longrightarrow> t \<in> Avoid s A \<longrightarrow> t \<in> lfp(af A)";

11196

73 

10218

74 
txt{*\noindent

11196

75 
The proof is by induction on the ``distance'' between @{term t} and @{term


76 
A}. Remember that @{prop"lfp(af A) = A \<union> M\<inverse> `` lfp(af A)"}.


77 
If @{term t} is already in @{term A}, then @{prop"t \<in> lfp(af A)"} is


78 
trivial. If @{term t} is not in @{term A} but all successors are in


79 
@{term"lfp(af A)"} (induction hypothesis), then @{prop"t \<in> lfp(af A)"} is


80 
again trivial.


81 


82 
The formal counterpart of this proof sketch is a wellfounded induction

11494

83 
on~@{term M} restricted to @{term"Avoid s A  A"}, roughly speaking:

11196

84 
@{term[display]"{(y,x). (x,y) \<in> M \<and> x \<in> Avoid s A \<and> x \<notin> A}"}

11277

85 
As we shall see presently, the absence of infinite @{term A}avoiding paths

10241

86 
starting from @{term s} implies wellfoundedness of this relation. For the

10218

87 
moment we assume this and proceed with the induction:


88 
*}


89 

11196

90 
apply(subgoal_tac "wf{(y,x). (x,y) \<in> M \<and> x \<in> Avoid s A \<and> x \<notin> A}");

10218

91 
apply(erule_tac a = t in wf_induct);


92 
apply(clarsimp);

11196

93 
(*<*)apply(rename_tac t)(*>*)

10218

94 


95 
txt{*\noindent

10885

96 
@{subgoals[display,indent=0,margin=65]}


97 
Now the induction hypothesis states that if @{prop"t \<notin> A"}

10218

98 
then all successors of @{term t} that are in @{term"Avoid s A"} are in

11196

99 
@{term"lfp (af A)"}. Unfolding @{term lfp} in the conclusion of the first


100 
subgoal once, we have to prove that @{term t} is in @{term A} or all successors

11494

101 
of @{term t} are in @{term"lfp (af A)"}. But if @{term t} is not in @{term A},

11196

102 
the second

15904

103 
@{const Avoid}rule implies that all successors of @{term t} are in

11494

104 
@{term"Avoid s A"}, because we also assume @{prop"t \<in> Avoid s A"}.


105 
Hence, by the induction hypothesis, all successors of @{term t} are indeed in

10218

106 
@{term"lfp(af A)"}. Mechanically:


107 
*}


108 

11196

109 
apply(subst lfp_unfold[OF mono_af]);


110 
apply(simp (no_asm) add: af_def);

12815

111 
apply(blast intro: Avoid.intros);

10218

112 


113 
txt{*

11494

114 
Having proved the main goal, we return to the proof obligation that the


115 
relation used above is indeed wellfounded. This is proved by contradiction: if

10885

116 
the relation is not wellfounded then there exists an infinite @{term

10218

117 
A}avoiding path all in @{term"Avoid s A"}, by theorem


118 
@{thm[source]wf_iff_no_infinite_down_chain}:


119 
@{thm[display]wf_iff_no_infinite_down_chain[no_vars]}


120 
From lemma @{thm[source]ex_infinite_path} the existence of an infinite

10885

121 
@{term A}avoiding path starting in @{term s} follows, contradiction.

10218

122 
*}


123 

10235

124 
apply(erule contrapos_pp);

12815

125 
apply(simp add: wf_iff_no_infinite_down_chain);

10218

126 
apply(erule exE);


127 
apply(rule ex_infinite_path);

12815

128 
apply(auto simp add: Paths_def);

10218

129 
done


130 


131 
text{*

11196

132 
The @{text"(no_asm)"} modifier of the @{text"rule_format"} directive in the


133 
statement of the lemma means

11494

134 
that the assumption is left unchanged; otherwise the @{text"\<forall>p"}


135 
would be turned

10218

136 
into a @{text"\<And>p"}, which would complicate matters below. As it is,


137 
@{thm[source]Avoid_in_lfp} is now


138 
@{thm[display]Avoid_in_lfp[no_vars]}


139 
The main theorem is simply the corollary where @{prop"t = s"},

11494

140 
when the assumption @{prop"t \<in> Avoid s A"} is trivially true

15904

141 
by the first @{const Avoid}rule. Isabelle confirms this:%

11494

142 
\index{CTL)}*}

10218

143 

10855

144 
theorem AF_lemma2: "{s. \<forall>p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";

12815

145 
by(auto elim: Avoid_in_lfp intro: Avoid.intros);

10218

146 


147 


148 
(*<*)end(*>*)
