doc-src/TutorialI/CTL/CTL.thy

 primrec
 "s \<Turnstile> Atom a  =  (a \<in> L s)"
 "s \<Turnstile> Neg f   = (~(s \<Turnstile> f))"
 "s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)"
 "s \<Turnstile> AX f    = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)"
-"s \<Turnstile> EF f    = (\<exists>t. (s,t) \<in> M^* \<and> t \<Turnstile> f)"
+"s \<Turnstile> EF f    = (\<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<Turnstile> f)"
 (*>*)
 "s \<Turnstile> AF f    = (\<forall>p \<in> Paths s. \<exists>i. p i \<Turnstile> f)";
 
 text{*\noindent
 Model checking @{term AF} involves a function which

 primrec
 "mc(Atom a)  = {s. a \<in> L s}"
 "mc(Neg f)   = -mc f"
 "mc(And f g) = mc f \<inter> mc g"
 "mc(AX f)    = {s. \<forall>t. (s,t) \<in> M  \<longrightarrow> t \<in> mc f}"
-"mc(EF f)    = lfp(\<lambda>T. mc f \<union> M^-1 ``` T)"(*>*)
+"mc(EF f)    = lfp(\<lambda>T. mc f \<union> M\<inverse> ``` T)"(*>*)
 "mc(AF f)    = lfp(af(mc f))";
 
 text{*\noindent
 Because @{term af} is monotone in its second argument (and also its first, but
 that is irrelevant) @{term"af A"} has a least fixed point:

 lemma mono_af: "mono(af A)";
 apply(simp add: mono_def af_def);
 apply blast;
 done
 (*<*)
-lemma mono_ef: "mono(\<lambda>T. A \<union> M^-1 ``` T)";
+lemma mono_ef: "mono(\<lambda>T. A \<union> M\<inverse> ``` T)";
 apply(rule monoI);
 by(blast);
 
 lemma EF_lemma:
-  "lfp(\<lambda>T. A \<union> M^-1 ``` T) = {s. \<exists>t. (s,t) \<in> M^* \<and> t \<in> A}";
+  "lfp(\<lambda>T. A \<union> M\<inverse> ``` T) = {s. \<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<in> A}";
 apply(rule equalityI);
  apply(rule subsetI);
  apply(simp);
  apply(erule lfp_induct);
   apply(rule mono_ef);

 the semantics of @{term EU} is straightforward:
 @{text[display]"s \<Turnstile> EU f g = (\<exists>p. until A B s p)"}
 Note that @{term EU} is not definable in terms of the other operators!
 
 Model checking @{term EU} is again a least fixed point construction:
-@{text[display]"mc(EU f g) = lfp(\<lambda>T. mc g \<union> mc f \<inter> (M^-1 ``` T))"}
+@{text[display]"mc(EU f g) = lfp(\<lambda>T. mc g \<union> mc f \<inter> (M\<inverse> ``` T))"}
 
 \begin{exercise}
 Extend the datatype of formulae by the above until operator
 and prove the equivalence between semantics and model checking, i.e.\ that
 @{prop[display]"mc(EU f g) = {s. s \<Turnstile> EU f g}"}

 *}
 
 (*<*)
 constdefs
  eufix :: "state set \<Rightarrow> state set \<Rightarrow> state set \<Rightarrow> state set"
-"eufix A B T \<equiv> B \<union> A \<inter> (M^-1 ``` T)"
+"eufix A B T \<equiv> B \<union> A \<inter> (M\<inverse> ``` T)"
 
 lemma "lfp(eufix A B) \<subseteq> eusem A B"
 apply(rule lfp_lowerbound)
 apply(clarsimp simp add:eusem_def eufix_def);
 apply(erule disjE);