src/Doc/Tutorial/CTL/CTLind.thy
author wenzelm
Mon, 07 Oct 2013 21:24:44 +0200
changeset 54313 da2e6282a4f5
parent 48985 5386df44a037
child 58860 fee7cfa69c50
permissions -rw-r--r--
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17914
99ead7a7eb42 fix headers;
wenzelm
parents: 15904
diff changeset
     1
(*<*)theory CTLind imports CTL begin(*>*)
10218
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
     2
10885
90695f46440b lcp's pass over the book, chapters 1-8
paulson
parents: 10855
diff changeset
     3
subsection{*CTL Revisited*}
10218
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
     4
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
     5
text{*\label{sec:CTL-revisited}
11494
23a118849801 revisions and indexing
paulson
parents: 11277
diff changeset
     6
\index{CTL|(}%
23a118849801 revisions and indexing
paulson
parents: 11277
diff changeset
     7
The purpose of this section is twofold: to demonstrate
23a118849801 revisions and indexing
paulson
parents: 11277
diff changeset
     8
some of the induction principles and heuristics discussed above and to
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10241
diff changeset
     9
show how inductive definitions can simplify proofs.
10218
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    10
In \S\ref{sec:CTL} we gave a fairly involved proof of the correctness of a
10795
9e888d60d3e5 minor edits to Chapters 1-3
paulson
parents: 10281
diff changeset
    11
model checker for CTL\@. In particular the proof of the
10218
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    12
@{thm[source]infinity_lemma} on the way to @{thm[source]AF_lemma2} is not as
11494
23a118849801 revisions and indexing
paulson
parents: 11277
diff changeset
    13
simple as one might expect, due to the @{text SOME} operator
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10241
diff changeset
    14
involved. Below we give a simpler proof of @{thm[source]AF_lemma2}
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10241
diff changeset
    15
based on an auxiliary inductive definition.
10218
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    16
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    17
Let us call a (finite or infinite) path \emph{@{term A}-avoiding} if it does
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    18
not touch any node in the set @{term A}. Then @{thm[source]AF_lemma2} says
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    19
that if no infinite path from some state @{term s} is @{term A}-avoiding,
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    20
then @{prop"s \<in> lfp(af A)"}. We prove this by inductively defining the set
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    21
@{term"Avoid s A"} of states reachable from @{term s} by a finite @{term
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    22
A}-avoiding path:
10241
e0428c2778f1 wellfounded -> well-founded
paulson
parents: 10235
diff changeset
    23
% Second proof of opposite direction, directly by well-founded induction
10218
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    24
% on the initial segment of M that avoids A.
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    25
*}
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    26
23733
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 17914
diff changeset
    27
inductive_set
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 17914
diff changeset
    28
  Avoid :: "state \<Rightarrow> state set \<Rightarrow> state set"
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 17914
diff changeset
    29
  for s :: state and A :: "state set"
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 17914
diff changeset
    30
where
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 17914
diff changeset
    31
    "s \<in> Avoid s A"
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 17914
diff changeset
    32
  | "\<lbrakk> t \<in> Avoid s A; t \<notin> A; (t,u) \<in> M \<rbrakk> \<Longrightarrow> u \<in> Avoid s A";
10218
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    33
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    34
text{*
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    35
It is easy to see that for any infinite @{term A}-avoiding path @{term f}
12492
a4dd02e744e0 *** empty log message ***
nipkow
parents: 11494
diff changeset
    36
with @{prop"f(0::nat) \<in> Avoid s A"} there is an infinite @{term A}-avoiding path
15904
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 12815
diff changeset
    37
starting with @{term s} because (by definition of @{const Avoid}) there is a
12492
a4dd02e744e0 *** empty log message ***
nipkow
parents: 11494
diff changeset
    38
finite @{term A}-avoiding path from @{term s} to @{term"f(0::nat)"}.
a4dd02e744e0 *** empty log message ***
nipkow
parents: 11494
diff changeset
    39
The proof is by induction on @{prop"f(0::nat) \<in> Avoid s A"}. However,
10218
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    40
this requires the following
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    41
reformulation, as explained in \S\ref{sec:ind-var-in-prems} above;
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    42
the @{text rule_format} directive undoes the reformulation after the proof.
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    43
*}
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    44
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    45
lemma ex_infinite_path[rule_format]:
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    46
  "t \<in> Avoid s A  \<Longrightarrow>
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    47
   \<forall>f\<in>Paths t. (\<forall>i. f i \<notin> A) \<longrightarrow> (\<exists>p\<in>Paths s. \<forall>i. p i \<notin> A)";
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    48
apply(erule Avoid.induct);
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    49
 apply(blast);
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    50
apply(clarify);
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    51
apply(drule_tac x = "\<lambda>i. case i of 0 \<Rightarrow> t | Suc i \<Rightarrow> f i" in bspec);
12815
wenzelm
parents: 12492
diff changeset
    52
apply(simp_all add: Paths_def split: nat.split);
10218
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    53
done
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    54
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    55
text{*\noindent
11494
23a118849801 revisions and indexing
paulson
parents: 11277
diff changeset
    56
The base case (@{prop"t = s"}) is trivial and proved by @{text blast}.
10218
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    57
In the induction step, we have an infinite @{term A}-avoiding path @{term f}
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    58
starting from @{term u}, a successor of @{term t}. Now we simply instantiate
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    59
the @{text"\<forall>f\<in>Paths t"} in the induction hypothesis by the path starting with
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    60
@{term t} and continuing with @{term f}. That is what the above $\lambda$-term
10885
90695f46440b lcp's pass over the book, chapters 1-8
paulson
parents: 10855
diff changeset
    61
expresses.  Simplification shows that this is a path starting with @{term t} 
90695f46440b lcp's pass over the book, chapters 1-8
paulson
parents: 10855
diff changeset
    62
and that the instantiated induction hypothesis implies the conclusion.
10218
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    63
11196
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10971
diff changeset
    64
Now we come to the key lemma. Assuming that no infinite @{term A}-avoiding
11277
a2bff98d6e5d *** empty log message ***
nipkow
parents: 11196
diff changeset
    65
path starts from @{term s}, we want to show @{prop"s \<in> lfp(af A)"}. For the
a2bff98d6e5d *** empty log message ***
nipkow
parents: 11196
diff changeset
    66
inductive proof this must be generalized to the statement that every point @{term t}
11494
23a118849801 revisions and indexing
paulson
parents: 11277
diff changeset
    67
``between'' @{term s} and @{term A}, in other words all of @{term"Avoid s A"},
11196
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10971
diff changeset
    68
is contained in @{term"lfp(af A)"}:
10218
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    69
*}
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    70
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    71
lemma Avoid_in_lfp[rule_format(no_asm)]:
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    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
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10971
diff changeset
    73
10218
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    74
txt{*\noindent
11196
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10971
diff changeset
    75
The proof is by induction on the ``distance'' between @{term t} and @{term
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10971
diff changeset
    76
A}. Remember that @{prop"lfp(af A) = A \<union> M\<inverse> `` lfp(af A)"}.
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10971
diff changeset
    77
If @{term t} is already in @{term A}, then @{prop"t \<in> lfp(af A)"} is
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10971
diff changeset
    78
trivial. If @{term t} is not in @{term A} but all successors are in
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10971
diff changeset
    79
@{term"lfp(af A)"} (induction hypothesis), then @{prop"t \<in> lfp(af A)"} is
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10971
diff changeset
    80
again trivial.
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10971
diff changeset
    81
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10971
diff changeset
    82
The formal counterpart of this proof sketch is a well-founded induction
11494
23a118849801 revisions and indexing
paulson
parents: 11277
diff changeset
    83
on~@{term M} restricted to @{term"Avoid s A - A"}, roughly speaking:
11196
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10971
diff changeset
    84
@{term[display]"{(y,x). (x,y) \<in> M \<and> x \<in> Avoid s A \<and> x \<notin> A}"}
11277
a2bff98d6e5d *** empty log message ***
nipkow
parents: 11196
diff changeset
    85
As we shall see presently, the absence of infinite @{term A}-avoiding paths
10241
e0428c2778f1 wellfounded -> well-founded
paulson
parents: 10235
diff changeset
    86
starting from @{term s} implies well-foundedness of this relation. For the
10218
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    87
moment we assume this and proceed with the induction:
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    88
*}
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    89
11196
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10971
diff changeset
    90
apply(subgoal_tac "wf{(y,x). (x,y) \<in> M \<and> x \<in> Avoid s A \<and> x \<notin> A}");
10218
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    91
 apply(erule_tac a = t in wf_induct);
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    92
 apply(clarsimp);
11196
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10971
diff changeset
    93
(*<*)apply(rename_tac t)(*>*)
10218
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    94
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    95
txt{*\noindent
10885
90695f46440b lcp's pass over the book, chapters 1-8
paulson
parents: 10855
diff changeset
    96
@{subgoals[display,indent=0,margin=65]}
90695f46440b lcp's pass over the book, chapters 1-8
paulson
parents: 10855
diff changeset
    97
Now the induction hypothesis states that if @{prop"t \<notin> A"}
10218
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
    98
then all successors of @{term t} that are in @{term"Avoid s A"} are in
11196
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10971
diff changeset
    99
@{term"lfp (af A)"}. Unfolding @{term lfp} in the conclusion of the first
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10971
diff changeset
   100
subgoal once, we have to prove that @{term t} is in @{term A} or all successors
11494
23a118849801 revisions and indexing
paulson
parents: 11277
diff changeset
   101
of @{term t} are in @{term"lfp (af A)"}.  But if @{term t} is not in @{term A},
11196
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10971
diff changeset
   102
the second 
15904
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 12815
diff changeset
   103
@{const Avoid}-rule implies that all successors of @{term t} are in
11494
23a118849801 revisions and indexing
paulson
parents: 11277
diff changeset
   104
@{term"Avoid s A"}, because we also assume @{prop"t \<in> Avoid s A"}.
23a118849801 revisions and indexing
paulson
parents: 11277
diff changeset
   105
Hence, by the induction hypothesis, all successors of @{term t} are indeed in
10218
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
   106
@{term"lfp(af A)"}. Mechanically:
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
   107
*}
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
   108
11196
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10971
diff changeset
   109
 apply(subst lfp_unfold[OF mono_af]);
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10971
diff changeset
   110
 apply(simp (no_asm) add: af_def);
12815
wenzelm
parents: 12492
diff changeset
   111
 apply(blast intro: Avoid.intros);
10218
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
   112
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
   113
txt{*
11494
23a118849801 revisions and indexing
paulson
parents: 11277
diff changeset
   114
Having proved the main goal, we return to the proof obligation that the 
23a118849801 revisions and indexing
paulson
parents: 11277
diff changeset
   115
relation used above is indeed well-founded. This is proved by contradiction: if
10885
90695f46440b lcp's pass over the book, chapters 1-8
paulson
parents: 10855
diff changeset
   116
the relation is not well-founded then there exists an infinite @{term
10218
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
   117
A}-avoiding path all in @{term"Avoid s A"}, by theorem
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
   118
@{thm[source]wf_iff_no_infinite_down_chain}:
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
   119
@{thm[display]wf_iff_no_infinite_down_chain[no_vars]}
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
   120
From lemma @{thm[source]ex_infinite_path} the existence of an infinite
10885
90695f46440b lcp's pass over the book, chapters 1-8
paulson
parents: 10855
diff changeset
   121
@{term A}-avoiding path starting in @{term s} follows, contradiction.
10218
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
   122
*}
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
   123
10235
20cf817f3b4a renaming of contrapos rules
paulson
parents: 10218
diff changeset
   124
apply(erule contrapos_pp);
12815
wenzelm
parents: 12492
diff changeset
   125
apply(simp add: wf_iff_no_infinite_down_chain);
10218
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
   126
apply(erule exE);
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
   127
apply(rule ex_infinite_path);
12815
wenzelm
parents: 12492
diff changeset
   128
apply(auto simp add: Paths_def);
10218
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
   129
done
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
   130
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
   131
text{*
11196
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10971
diff changeset
   132
The @{text"(no_asm)"} modifier of the @{text"rule_format"} directive in the
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10971
diff changeset
   133
statement of the lemma means
11494
23a118849801 revisions and indexing
paulson
parents: 11277
diff changeset
   134
that the assumption is left unchanged; otherwise the @{text"\<forall>p"} 
23a118849801 revisions and indexing
paulson
parents: 11277
diff changeset
   135
would be turned
10218
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
   136
into a @{text"\<And>p"}, which would complicate matters below. As it is,
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
   137
@{thm[source]Avoid_in_lfp} is now
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
   138
@{thm[display]Avoid_in_lfp[no_vars]}
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
   139
The main theorem is simply the corollary where @{prop"t = s"},
11494
23a118849801 revisions and indexing
paulson
parents: 11277
diff changeset
   140
when the assumption @{prop"t \<in> Avoid s A"} is trivially true
15904
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 12815
diff changeset
   141
by the first @{const Avoid}-rule. Isabelle confirms this:%
11494
23a118849801 revisions and indexing
paulson
parents: 11277
diff changeset
   142
\index{CTL|)}*}
10218
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
   143
10855
140a1ed65665 *** empty log message ***
nipkow
parents: 10845
diff changeset
   144
theorem AF_lemma2:  "{s. \<forall>p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";
12815
wenzelm
parents: 12492
diff changeset
   145
by(auto elim: Avoid_in_lfp intro: Avoid.intros);
10218
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
   146
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
   147
54411746c549 *** empty log message ***
nipkow
parents:
diff changeset
   148
(*<*)end(*>*)