src/Doc/Tutorial/CTL/CTL.thy
changeset 58860 fee7cfa69c50
parent 58620 7435b6a3f72e
child 67406 23307fd33906
     1.1 --- a/src/Doc/Tutorial/CTL/CTL.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/Doc/Tutorial/CTL/CTL.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4  (*<*)theory CTL imports Base begin(*>*)
     1.5  
     1.6 -subsection{*Computation Tree Logic --- CTL*};
     1.7 +subsection{*Computation Tree Logic --- CTL*}
     1.8  
     1.9  text{*\label{sec:CTL}
    1.10  \index{CTL|(}%
    1.11 @@ -8,21 +8,21 @@
    1.12  Let us be adventurous and introduce a more expressive temporal operator.
    1.13  We extend the datatype
    1.14  @{text formula} by a new constructor
    1.15 -*};
    1.16 +*}
    1.17  (*<*)
    1.18  datatype formula = Atom "atom"
    1.19                    | Neg formula
    1.20                    | And formula formula
    1.21                    | AX formula
    1.22                    | EF formula(*>*)
    1.23 -                  | AF formula;
    1.24 +                  | AF formula
    1.25  
    1.26  text{*\noindent
    1.27  which stands for ``\emph{A}lways in the \emph{F}uture'':
    1.28  on all infinite paths, at some point the formula holds.
    1.29  Formalizing the notion of an infinite path is easy
    1.30  in HOL: it is simply a function from @{typ nat} to @{typ state}.
    1.31 -*};
    1.32 +*}
    1.33  
    1.34  definition Paths :: "state \<Rightarrow> (nat \<Rightarrow> state)set" where
    1.35  "Paths s \<equiv> {p. s = p 0 \<and> (\<forall>i. (p i, p(i+1)) \<in> M)}"
    1.36 @@ -33,7 +33,7 @@
    1.37  extended by new constructors or equations. This is just a trick of the
    1.38  presentation (see \S\ref{sec:doc-prep-suppress}). In reality one has to define
    1.39  a new datatype and a new function.}
    1.40 -*};
    1.41 +*}
    1.42  (*<*)
    1.43  primrec valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80) where
    1.44  "s \<Turnstile> Atom a  =  (a \<in> L s)" |
    1.45 @@ -47,7 +47,7 @@
    1.46  text{*\noindent
    1.47  Model checking @{const AF} involves a function which
    1.48  is just complicated enough to warrant a separate definition:
    1.49 -*};
    1.50 +*}
    1.51  
    1.52  definition af :: "state set \<Rightarrow> state set \<Rightarrow> state set" where
    1.53  "af A T \<equiv> A \<union> {s. \<forall>t. (s, t) \<in> M \<longrightarrow> t \<in> T}"
    1.54 @@ -55,7 +55,7 @@
    1.55  text{*\noindent
    1.56  Now we define @{term "mc(AF f)"} as the least set @{term T} that includes
    1.57  @{term"mc f"} and all states all of whose direct successors are in @{term T}:
    1.58 -*};
    1.59 +*}
    1.60  (*<*)
    1.61  primrec mc :: "formula \<Rightarrow> state set" where
    1.62  "mc(Atom a)  = {s. a \<in> L s}" |
    1.63 @@ -63,45 +63,45 @@
    1.64  "mc(And f g) = mc f \<inter> mc g" |
    1.65  "mc(AX f)    = {s. \<forall>t. (s,t) \<in> M  \<longrightarrow> t \<in> mc f}" |
    1.66  "mc(EF f)    = lfp(\<lambda>T. mc f \<union> M\<inverse> `` T)"|(*>*)
    1.67 -"mc(AF f)    = lfp(af(mc f))";
    1.68 +"mc(AF f)    = lfp(af(mc f))"
    1.69  
    1.70  text{*\noindent
    1.71  Because @{const af} is monotone in its second argument (and also its first, but
    1.72  that is irrelevant), @{term"af A"} has a least fixed point:
    1.73 -*};
    1.74 +*}
    1.75  
    1.76 -lemma mono_af: "mono(af A)";
    1.77 -apply(simp add: mono_def af_def);
    1.78 -apply blast;
    1.79 +lemma mono_af: "mono(af A)"
    1.80 +apply(simp add: mono_def af_def)
    1.81 +apply blast
    1.82  done
    1.83  (*<*)
    1.84 -lemma mono_ef: "mono(\<lambda>T. A \<union> M\<inverse> `` T)";
    1.85 -apply(rule monoI);
    1.86 -by(blast);
    1.87 +lemma mono_ef: "mono(\<lambda>T. A \<union> M\<inverse> `` T)"
    1.88 +apply(rule monoI)
    1.89 +by(blast)
    1.90  
    1.91  lemma EF_lemma:
    1.92 -  "lfp(\<lambda>T. A \<union> M\<inverse> `` T) = {s. \<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<in> A}";
    1.93 -apply(rule equalityI);
    1.94 - apply(rule subsetI);
    1.95 - apply(simp);
    1.96 - apply(erule lfp_induct_set);
    1.97 -  apply(rule mono_ef);
    1.98 - apply(simp);
    1.99 - apply(blast intro: rtrancl_trans);
   1.100 -apply(rule subsetI);
   1.101 -apply(simp, clarify);
   1.102 -apply(erule converse_rtrancl_induct);
   1.103 - apply(subst lfp_unfold[OF mono_ef]);
   1.104 - apply(blast);
   1.105 -apply(subst lfp_unfold[OF mono_ef]);
   1.106 -by(blast);
   1.107 +  "lfp(\<lambda>T. A \<union> M\<inverse> `` T) = {s. \<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<in> A}"
   1.108 +apply(rule equalityI)
   1.109 + apply(rule subsetI)
   1.110 + apply(simp)
   1.111 + apply(erule lfp_induct_set)
   1.112 +  apply(rule mono_ef)
   1.113 + apply(simp)
   1.114 + apply(blast intro: rtrancl_trans)
   1.115 +apply(rule subsetI)
   1.116 +apply(simp, clarify)
   1.117 +apply(erule converse_rtrancl_induct)
   1.118 + apply(subst lfp_unfold[OF mono_ef])
   1.119 + apply(blast)
   1.120 +apply(subst lfp_unfold[OF mono_ef])
   1.121 +by(blast)
   1.122  (*>*)
   1.123  text{*
   1.124  All we need to prove now is  @{prop"mc(AF f) = {s. s \<Turnstile> AF f}"}, which states
   1.125  that @{term mc} and @{text"\<Turnstile>"} agree for @{const AF}\@.
   1.126  This time we prove the two inclusions separately, starting
   1.127  with the easy one:
   1.128 -*};
   1.129 +*}
   1.130  
   1.131  theorem AF_lemma1: "lfp(af A) \<subseteq> {s. \<forall>p \<in> Paths s. \<exists>i. p i \<in> A}"
   1.132  
   1.133 @@ -114,9 +114,9 @@
   1.134  \end{center}
   1.135  The instance of the premise @{prop"f S \<subseteq> S"} is proved pointwise,
   1.136  a decision that \isa{auto} takes for us:
   1.137 -*};
   1.138 -apply(rule lfp_lowerbound);
   1.139 -apply(auto simp add: af_def Paths_def);
   1.140 +*}
   1.141 +apply(rule lfp_lowerbound)
   1.142 +apply(auto simp add: af_def Paths_def)
   1.143  
   1.144  txt{*
   1.145  @{subgoals[display,indent=0,margin=70,goals_limit=1]}
   1.146 @@ -124,11 +124,11 @@
   1.147  The rest is automatic, which is surprising because it involves
   1.148  finding the instantiation @{term"\<lambda>i::nat. p(i+1)"}
   1.149  for @{text"\<forall>p"}.
   1.150 -*};
   1.151 +*}
   1.152  
   1.153 -apply(erule_tac x = "p 1" in allE);
   1.154 -apply(auto);
   1.155 -done;
   1.156 +apply(erule_tac x = "p 1" in allE)
   1.157 +apply(auto)
   1.158 +done
   1.159  
   1.160  
   1.161  text{*
   1.162 @@ -143,14 +143,14 @@
   1.163  
   1.164  The one-step argument in the sketch above
   1.165  is proved by a variant of contraposition:
   1.166 -*};
   1.167 +*}
   1.168  
   1.169  lemma not_in_lfp_afD:
   1.170 - "s \<notin> lfp(af A) \<Longrightarrow> s \<notin> A \<and> (\<exists> t. (s,t) \<in> M \<and> t \<notin> lfp(af A))";
   1.171 -apply(erule contrapos_np);
   1.172 -apply(subst lfp_unfold[OF mono_af]);
   1.173 -apply(simp add: af_def);
   1.174 -done;
   1.175 + "s \<notin> lfp(af A) \<Longrightarrow> s \<notin> A \<and> (\<exists> t. (s,t) \<in> M \<and> t \<notin> lfp(af A))"
   1.176 +apply(erule contrapos_np)
   1.177 +apply(subst lfp_unfold[OF mono_af])
   1.178 +apply(simp add: af_def)
   1.179 +done
   1.180  
   1.181  text{*\noindent
   1.182  We assume the negation of the conclusion and prove @{term"s : lfp(af A)"}.
   1.183 @@ -159,7 +159,7 @@
   1.184  
   1.185  Now we iterate this process. The following construction of the desired
   1.186  path is parameterized by a predicate @{term Q} that should hold along the path:
   1.187 -*};
   1.188 +*}
   1.189  
   1.190  primrec path :: "state \<Rightarrow> (state \<Rightarrow> bool) \<Rightarrow> (nat \<Rightarrow> state)" where
   1.191  "path s Q 0 = s" |
   1.192 @@ -175,41 +175,41 @@
   1.193  
   1.194  Let us show that if each state @{term s} that satisfies @{term Q}
   1.195  has a successor that again satisfies @{term Q}, then there exists an infinite @{term Q}-path:
   1.196 -*};
   1.197 +*}
   1.198  
   1.199  lemma infinity_lemma:
   1.200    "\<lbrakk> Q s; \<forall>s. Q s \<longrightarrow> (\<exists> t. (s,t) \<in> M \<and> Q t) \<rbrakk> \<Longrightarrow>
   1.201 -   \<exists>p\<in>Paths s. \<forall>i. Q(p i)";
   1.202 +   \<exists>p\<in>Paths s. \<forall>i. Q(p i)"
   1.203  
   1.204  txt{*\noindent
   1.205  First we rephrase the conclusion slightly because we need to prove simultaneously
   1.206  both the path property and the fact that @{term Q} holds:
   1.207 -*};
   1.208 +*}
   1.209  
   1.210  apply(subgoal_tac
   1.211 -  "\<exists>p. s = p 0 \<and> (\<forall>i::nat. (p i, p(i+1)) \<in> M \<and> Q(p i))");
   1.212 +  "\<exists>p. s = p 0 \<and> (\<forall>i::nat. (p i, p(i+1)) \<in> M \<and> Q(p i))")
   1.213  
   1.214  txt{*\noindent
   1.215  From this proposition the original goal follows easily:
   1.216 -*};
   1.217 +*}
   1.218  
   1.219 - apply(simp add: Paths_def, blast);
   1.220 + apply(simp add: Paths_def, blast)
   1.221  
   1.222  txt{*\noindent
   1.223  The new subgoal is proved by providing the witness @{term "path s Q"} for @{term p}:
   1.224 -*};
   1.225 +*}
   1.226  
   1.227 -apply(rule_tac x = "path s Q" in exI);
   1.228 -apply(clarsimp);
   1.229 +apply(rule_tac x = "path s Q" in exI)
   1.230 +apply(clarsimp)
   1.231  
   1.232  txt{*\noindent
   1.233  After simplification and clarification, the subgoal has the following form:
   1.234  @{subgoals[display,indent=0,margin=70,goals_limit=1]}
   1.235  It invites a proof by induction on @{term i}:
   1.236 -*};
   1.237 +*}
   1.238  
   1.239 -apply(induct_tac i);
   1.240 - apply(simp);
   1.241 +apply(induct_tac i)
   1.242 + apply(simp)
   1.243  
   1.244  txt{*\noindent
   1.245  After simplification, the base case boils down to
   1.246 @@ -223,9 +223,9 @@
   1.247  two subgoals: @{prop"EX a. (s, a) : M & Q a"}, which follows from the assumptions, and
   1.248  @{prop"(s, x) : M & Q x ==> (s,x) : M"}, which is trivial. Thus it is not surprising that
   1.249  @{text fast} can prove the base case quickly:
   1.250 -*};
   1.251 +*}
   1.252  
   1.253 - apply(fast intro: someI2_ex);
   1.254 + apply(fast intro: someI2_ex)
   1.255  
   1.256  txt{*\noindent
   1.257  What is worth noting here is that we have used \methdx{fast} rather than
   1.258 @@ -242,15 +242,15 @@
   1.259  occurrences of @{text SOME}. As a result, @{text fast} is no longer able to
   1.260  solve the subgoal and we apply @{thm[source]someI2_ex} by hand.  We merely
   1.261  show the proof commands but do not describe the details:
   1.262 -*};
   1.263 +*}
   1.264  
   1.265 -apply(simp);
   1.266 -apply(rule someI2_ex);
   1.267 - apply(blast);
   1.268 -apply(rule someI2_ex);
   1.269 - apply(blast);
   1.270 -apply(blast);
   1.271 -done;
   1.272 +apply(simp)
   1.273 +apply(rule someI2_ex)
   1.274 + apply(blast)
   1.275 +apply(rule someI2_ex)
   1.276 + apply(blast)
   1.277 +apply(blast)
   1.278 +done
   1.279  
   1.280  text{*
   1.281  Function @{const path} has fulfilled its purpose now and can be forgotten.
   1.282 @@ -261,58 +261,58 @@
   1.283  @{term[display]"rec_nat s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)"}
   1.284  is extensionally equal to @{term"path s Q"},
   1.285  where @{term rec_nat} is the predefined primitive recursor on @{typ nat}.
   1.286 -*};
   1.287 +*}
   1.288  (*<*)
   1.289  lemma
   1.290  "\<lbrakk> Q s; \<forall> s. Q s \<longrightarrow> (\<exists> t. (s,t)\<in>M \<and> Q t) \<rbrakk> \<Longrightarrow>
   1.291 - \<exists> p\<in>Paths s. \<forall> i. Q(p i)";
   1.292 + \<exists> p\<in>Paths s. \<forall> i. Q(p i)"
   1.293  apply(subgoal_tac
   1.294 - "\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(Suc i))\<in>M \<and> Q(p i))");
   1.295 - apply(simp add: Paths_def);
   1.296 - apply(blast);
   1.297 -apply(rule_tac x = "rec_nat s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)" in exI);
   1.298 -apply(simp);
   1.299 -apply(intro strip);
   1.300 -apply(induct_tac i);
   1.301 - apply(simp);
   1.302 - apply(fast intro: someI2_ex);
   1.303 -apply(simp);
   1.304 -apply(rule someI2_ex);
   1.305 - apply(blast);
   1.306 -apply(rule someI2_ex);
   1.307 - apply(blast);
   1.308 -by(blast);
   1.309 + "\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(Suc i))\<in>M \<and> Q(p i))")
   1.310 + apply(simp add: Paths_def)
   1.311 + apply(blast)
   1.312 +apply(rule_tac x = "rec_nat s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)" in exI)
   1.313 +apply(simp)
   1.314 +apply(intro strip)
   1.315 +apply(induct_tac i)
   1.316 + apply(simp)
   1.317 + apply(fast intro: someI2_ex)
   1.318 +apply(simp)
   1.319 +apply(rule someI2_ex)
   1.320 + apply(blast)
   1.321 +apply(rule someI2_ex)
   1.322 + apply(blast)
   1.323 +by(blast)
   1.324  (*>*)
   1.325  
   1.326  text{*
   1.327  At last we can prove the opposite direction of @{thm[source]AF_lemma1}:
   1.328 -*};
   1.329 +*}
   1.330  
   1.331 -theorem AF_lemma2: "{s. \<forall>p \<in> Paths s. \<exists>i. p i \<in> A} \<subseteq> lfp(af A)";
   1.332 +theorem AF_lemma2: "{s. \<forall>p \<in> Paths s. \<exists>i. p i \<in> A} \<subseteq> lfp(af A)"
   1.333  
   1.334  txt{*\noindent
   1.335  The proof is again pointwise and then by contraposition:
   1.336 -*};
   1.337 +*}
   1.338  
   1.339 -apply(rule subsetI);
   1.340 -apply(erule contrapos_pp);
   1.341 -apply simp;
   1.342 +apply(rule subsetI)
   1.343 +apply(erule contrapos_pp)
   1.344 +apply simp
   1.345  
   1.346  txt{*
   1.347  @{subgoals[display,indent=0,goals_limit=1]}
   1.348  Applying the @{thm[source]infinity_lemma} as a destruction rule leaves two subgoals, the second
   1.349  premise of @{thm[source]infinity_lemma} and the original subgoal:
   1.350 -*};
   1.351 +*}
   1.352  
   1.353 -apply(drule infinity_lemma);
   1.354 +apply(drule infinity_lemma)
   1.355  
   1.356  txt{*
   1.357  @{subgoals[display,indent=0,margin=65]}
   1.358  Both are solved automatically:
   1.359 -*};
   1.360 +*}
   1.361  
   1.362 - apply(auto dest: not_in_lfp_afD);
   1.363 -done;
   1.364 + apply(auto dest: not_in_lfp_afD)
   1.365 +done
   1.366  
   1.367  text{*
   1.368  If you find these proofs too complicated, we recommend that you read
   1.369 @@ -324,9 +324,9 @@
   1.370  @{thm[source]AF_lemma1} and @{thm[source]AF_lemma2} on the spot:
   1.371  *}
   1.372  
   1.373 -theorem "mc f = {s. s \<Turnstile> f}";
   1.374 -apply(induct_tac f);
   1.375 -apply(auto simp add: EF_lemma equalityI[OF AF_lemma1 AF_lemma2]);
   1.376 +theorem "mc f = {s. s \<Turnstile> f}"
   1.377 +apply(induct_tac f)
   1.378 +apply(auto simp add: EF_lemma equalityI[OF AF_lemma1 AF_lemma2])
   1.379  done
   1.380  
   1.381  text{*
   1.382 @@ -377,22 +377,22 @@
   1.383  apply simp
   1.384  done
   1.385  
   1.386 -lemma mono_eufix: "mono(eufix A B)";
   1.387 -apply(simp add: mono_def eufix_def);
   1.388 -apply blast;
   1.389 +lemma mono_eufix: "mono(eufix A B)"
   1.390 +apply(simp add: mono_def eufix_def)
   1.391 +apply blast
   1.392  done
   1.393  
   1.394 -lemma "eusem A B \<subseteq> lfp(eufix A B)";
   1.395 -apply(clarsimp simp add: eusem_def);
   1.396 -apply(erule rev_mp);
   1.397 -apply(rule_tac x = x in spec);
   1.398 -apply(induct_tac p);
   1.399 +lemma "eusem A B \<subseteq> lfp(eufix A B)"
   1.400 +apply(clarsimp simp add: eusem_def)
   1.401 +apply(erule rev_mp)
   1.402 +apply(rule_tac x = x in spec)
   1.403 +apply(induct_tac p)
   1.404   apply(subst lfp_unfold[OF mono_eufix])
   1.405 - apply(simp add: eufix_def);
   1.406 -apply(clarsimp);
   1.407 + apply(simp add: eufix_def)
   1.408 +apply(clarsimp)
   1.409  apply(subst lfp_unfold[OF mono_eufix])
   1.410 -apply(simp add: eufix_def);
   1.411 -apply blast;
   1.412 +apply(simp add: eufix_def)
   1.413 +apply blast
   1.414  done
   1.415  
   1.416  (*