src/HOL/ex/CTL.thy
 author wenzelm Wed Jun 22 10:09:20 2016 +0200 (2016-06-22) changeset 63343 fb5d8a50c641 parent 63055 ae0ca486bd3f child 69597 ff784d5a5bfb permissions -rw-r--r--
bundle lifting_syntax;
 bauerg@15871  1 (* Title: HOL/ex/CTL.thy  bauerg@15871  2  Author: Gertrud Bauer  bauerg@15871  3 *)  bauerg@15871  4 wenzelm@61343  5 section \CTL formulae\  bauerg@15871  6 wenzelm@46685  7 theory CTL  wenzelm@46685  8 imports Main  wenzelm@46685  9 begin  bauerg@15871  10 wenzelm@61343  11 text \  wenzelm@61934  12  We formalize basic concepts of Computational Tree Logic (CTL) @{cite  wenzelm@61934  13  "McMillan-PhDThesis" and "McMillan-LectureNotes"} within the simply-typed  wenzelm@61934  14  set theory of HOL.  bauerg@15871  15 wenzelm@61934  16  By using the common technique of shallow embedding'', a CTL formula is  wenzelm@61934  17  identified with the corresponding set of states where it holds.  wenzelm@61934  18  Consequently, CTL operations such as negation, conjunction, disjunction  wenzelm@61934  19  simply become complement, intersection, union of sets. We only require a  wenzelm@61934  20  separate operation for implication, as point-wise inclusion is usually not  wenzelm@61934  21  encountered in plain set-theory.  wenzelm@61343  22 \  bauerg@15871  23 bauerg@15871  24 lemmas [intro!] = Int_greatest Un_upper2 Un_upper1 Int_lower1 Int_lower2  bauerg@15871  25 wenzelm@42463  26 type_synonym 'a ctl = "'a set"  wenzelm@20807  27 wenzelm@63054  28 definition imp :: "'a ctl \ 'a ctl \ 'a ctl" (infixr "\" 75)  wenzelm@63054  29  where "p \ q = - p \ q"  bauerg@15871  30 wenzelm@20807  31 lemma [intro!]: "p \ p \ q \ q" unfolding imp_def by auto  wenzelm@20807  32 lemma [intro!]: "p \ (q \ p)" unfolding imp_def by rule  bauerg@15871  33 bauerg@15871  34 wenzelm@61343  35 text \  wenzelm@61934  36  \<^smallskip>  wenzelm@61934  37  The CTL path operators are more interesting; they are based on an arbitrary,  wenzelm@61934  38  but fixed model \\\, which is simply a transition relation over states  wenzelm@61934  39  @{typ 'a}.  wenzelm@61343  40 \  bauerg@15871  41 wenzelm@20807  42 axiomatization \ :: "('a \ 'a) set"  bauerg@15871  43 wenzelm@61343  44 text \  wenzelm@63055  45  The operators \\<^bold>E\<^bold>X\, \\<^bold>E\<^bold>F\, \\<^bold>E\<^bold>G\ are taken as primitives, while \\<^bold>A\<^bold>X\,  wenzelm@63055  46  \\<^bold>A\<^bold>F\, \\<^bold>A\<^bold>G\ are defined as derived ones. The formula \\<^bold>E\<^bold>X p\ holds in a  wenzelm@63055  47  state \s\, iff there is a successor state \s'\ (with respect to the model  wenzelm@63055  48  \\\), such that \p\ holds in \s'\. The formula \\<^bold>E\<^bold>F p\ holds in a state  wenzelm@63055  49  \s\, iff there is a path in \\\, starting from \s\, such that there exists a  wenzelm@63055  50  state \s'\ on the path, such that \p\ holds in \s'\. The formula \\<^bold>E\<^bold>G p\  wenzelm@63055  51  holds in a state \s\, iff there is a path, starting from \s\, such that for  wenzelm@63055  52  all states \s'\ on the path, \p\ holds in \s'\. It is easy to see that \\<^bold>E\<^bold>F  wenzelm@63055  53  p\ and \\<^bold>E\<^bold>G p\ may be expressed using least and greatest fixed points  wenzelm@63055  54  @{cite "McMillan-PhDThesis"}.  wenzelm@61343  55 \  bauerg@15871  56 wenzelm@63055  57 definition EX ("\<^bold>E\<^bold>X _" [80] 90)  wenzelm@63055  58  where [simp]: "\<^bold>E\<^bold>X p = {s. \s'. (s, s') \ \ \ s' \ p}"  wenzelm@63055  59 wenzelm@63055  60 definition EF ("\<^bold>E\<^bold>F _" [80] 90)  wenzelm@63055  61  where [simp]: "\<^bold>E\<^bold>F p = lfp (\s. p \ \<^bold>E\<^bold>X s)"  wenzelm@63055  62 wenzelm@63055  63 definition EG ("\<^bold>E\<^bold>G _" [80] 90)  wenzelm@63055  64  where [simp]: "\<^bold>E\<^bold>G p = gfp (\s. p \ \<^bold>E\<^bold>X s)"  bauerg@15871  65 wenzelm@61343  66 text \  wenzelm@63055  67  \\<^bold>A\<^bold>X\, \\<^bold>A\<^bold>F\ and \\<^bold>A\<^bold>G\ are now defined dually in terms of \\<^bold>E\<^bold>X\,  wenzelm@63055  68  \\<^bold>E\<^bold>F\ and \\<^bold>E\<^bold>G\.  wenzelm@61343  69 \  bauerg@15871  70 wenzelm@63055  71 definition AX ("\<^bold>A\<^bold>X _" [80] 90)  wenzelm@63055  72  where [simp]: "\<^bold>A\<^bold>X p = - \<^bold>E\<^bold>X - p"  wenzelm@63055  73 definition AF ("\<^bold>A\<^bold>F _" [80] 90)  wenzelm@63055  74  where [simp]: "\<^bold>A\<^bold>F p = - \<^bold>E\<^bold>G - p"  wenzelm@63055  75 definition AG ("\<^bold>A\<^bold>G _" [80] 90)  wenzelm@63055  76  where [simp]: "\<^bold>A\<^bold>G p = - \<^bold>E\<^bold>F - p"  bauerg@15871  77 bauerg@15871  78 wenzelm@61343  79 subsection \Basic fixed point properties\  bauerg@15871  80 wenzelm@61343  81 text \  wenzelm@61934  82  First of all, we use the de-Morgan property of fixed points.  wenzelm@61343  83 \  bauerg@15871  84 berghofe@21026  85 lemma lfp_gfp: "lfp f = - gfp (\s::'a set. - (f (- s)))"  bauerg@15871  86 proof  bauerg@15871  87  show "lfp f \ - gfp (\s. - f (- s))"  bauerg@15871  88  proof  wenzelm@63054  89  show "x \ - gfp (\s. - f (- s))" if l: "x \ lfp f" for x  bauerg@15871  90  proof  bauerg@15871  91  assume "x \ gfp (\s. - f (- s))"  berghofe@21026  92  then obtain u where "x \ u" and "u \ - f (- u)"  haftmann@32587  93  by (auto simp add: gfp_def)  bauerg@15871  94  then have "f (- u) \ - u" by auto  bauerg@15871  95  then have "lfp f \ - u" by (rule lfp_lowerbound)  bauerg@15871  96  from l and this have "x \ u" by auto  wenzelm@61343  97  with \x \ u\ show False by contradiction  bauerg@15871  98  qed  bauerg@15871  99  qed  bauerg@15871  100  show "- gfp (\s. - f (- s)) \ lfp f"  bauerg@15871  101  proof (rule lfp_greatest)  wenzelm@63054  102  fix u  wenzelm@63054  103  assume "f u \ u"  bauerg@15871  104  then have "- u \ - f u" by auto  bauerg@15871  105  then have "- u \ - f (- (- u))" by simp  bauerg@15871  106  then have "- u \ gfp (\s. - f (- s))" by (rule gfp_upperbound)  bauerg@15871  107  then show "- gfp (\s. - f (- s)) \ u" by auto  bauerg@15871  108  qed  bauerg@15871  109 qed  bauerg@15871  110 berghofe@21026  111 lemma lfp_gfp': "- lfp f = gfp (\s::'a set. - (f (- s)))"  bauerg@15871  112  by (simp add: lfp_gfp)  bauerg@15871  113 berghofe@21026  114 lemma gfp_lfp': "- gfp f = lfp (\s::'a set. - (f (- s)))"  bauerg@15871  115  by (simp add: lfp_gfp)  bauerg@15871  116 wenzelm@61343  117 text \  wenzelm@63055  118  In order to give dual fixed point representations of @{term "\<^bold>A\<^bold>F p"} and  wenzelm@63055  119  @{term "\<^bold>A\<^bold>G p"}:  wenzelm@61343  120 \  bauerg@15871  121 wenzelm@63055  122 lemma AF_lfp: "\<^bold>A\<^bold>F p = lfp (\s. p \ \<^bold>A\<^bold>X s)"  wenzelm@61934  123  by (simp add: lfp_gfp)  bauerg@15871  124 wenzelm@63055  125 lemma AG_gfp: "\<^bold>A\<^bold>G p = gfp (\s. p \ \<^bold>A\<^bold>X s)"  wenzelm@63055  126  by (simp add: lfp_gfp)  wenzelm@63055  127 wenzelm@63055  128 lemma EF_fp: "\<^bold>E\<^bold>F p = p \ \<^bold>E\<^bold>X \<^bold>E\<^bold>F p"  bauerg@15871  129 proof -  wenzelm@63055  130  have "mono (\s. p \ \<^bold>E\<^bold>X s)" by rule auto  bauerg@15871  131  then show ?thesis by (simp only: EF_def) (rule lfp_unfold)  bauerg@15871  132 qed  bauerg@15871  133 wenzelm@63055  134 lemma AF_fp: "\<^bold>A\<^bold>F p = p \ \<^bold>A\<^bold>X \<^bold>A\<^bold>F p"  bauerg@15871  135 proof -  wenzelm@63055  136  have "mono (\s. p \ \<^bold>A\<^bold>X s)" by rule auto  bauerg@15871  137  then show ?thesis by (simp only: AF_lfp) (rule lfp_unfold)  bauerg@15871  138 qed  bauerg@15871  139 wenzelm@63055  140 lemma EG_fp: "\<^bold>E\<^bold>G p = p \ \<^bold>E\<^bold>X \<^bold>E\<^bold>G p"  bauerg@15871  141 proof -  wenzelm@63055  142  have "mono (\s. p \ \<^bold>E\<^bold>X s)" by rule auto  bauerg@15871  143  then show ?thesis by (simp only: EG_def) (rule gfp_unfold)  bauerg@15871  144 qed  bauerg@15871  145 wenzelm@61343  146 text \  wenzelm@63055  147  From the greatest fixed point definition of @{term "\<^bold>A\<^bold>G p"}, we derive as  wenzelm@61934  148  a consequence of the Knaster-Tarski theorem on the one hand that @{term  wenzelm@63055  149  "\<^bold>A\<^bold>G p"} is a fixed point of the monotonic function  wenzelm@63055  150  @{term "\s. p \ \<^bold>A\<^bold>X s"}.  wenzelm@61343  151 \  bauerg@15871  152 wenzelm@63055  153 lemma AG_fp: "\<^bold>A\<^bold>G p = p \ \<^bold>A\<^bold>X \<^bold>A\<^bold>G p"  bauerg@15871  154 proof -  wenzelm@63055  155  have "mono (\s. p \ \<^bold>A\<^bold>X s)" by rule auto  bauerg@15871  156  then show ?thesis by (simp only: AG_gfp) (rule gfp_unfold)  bauerg@15871  157 qed  bauerg@15871  158 wenzelm@61343  159 text \  wenzelm@61934  160  This fact may be split up into two inequalities (merely using transitivity  wenzelm@61934  161  of \\\, which is an instance of the overloaded \\\ in Isabelle/HOL).  wenzelm@61343  162 \  bauerg@15871  163 wenzelm@63055  164 lemma AG_fp_1: "\<^bold>A\<^bold>G p \ p"  bauerg@15871  165 proof -  wenzelm@63055  166  note AG_fp also have "p \ \<^bold>A\<^bold>X \<^bold>A\<^bold>G p \ p" by auto  bauerg@15871  167  finally show ?thesis .  bauerg@15871  168 qed  bauerg@15871  169 wenzelm@63055  170 lemma AG_fp_2: "\<^bold>A\<^bold>G p \ \<^bold>A\<^bold>X \<^bold>A\<^bold>G p"  bauerg@15871  171 proof -  wenzelm@63055  172  note AG_fp also have "p \ \<^bold>A\<^bold>X \<^bold>A\<^bold>G p \ \<^bold>A\<^bold>X \<^bold>A\<^bold>G p" by auto  bauerg@15871  173  finally show ?thesis .  bauerg@15871  174 qed  bauerg@15871  175 wenzelm@61343  176 text \  wenzelm@61934  177  On the other hand, we have from the Knaster-Tarski fixed point theorem that  wenzelm@63055  178  any other post-fixed point of @{term "\s. p \ \<^bold>A\<^bold>X s"} is smaller than  wenzelm@63055  179  @{term "\<^bold>A\<^bold>G p"}. A post-fixed point is a set of states \q\ such that @{term  wenzelm@63055  180  "q \ p \ \<^bold>A\<^bold>X q"}. This leads to the following co-induction principle for  wenzelm@63055  181  @{term "\<^bold>A\<^bold>G p"}.  wenzelm@61343  182 \  bauerg@15871  183 wenzelm@63055  184 lemma AG_I: "q \ p \ \<^bold>A\<^bold>X q \ q \ \<^bold>A\<^bold>G p"  bauerg@15871  185  by (simp only: AG_gfp) (rule gfp_upperbound)  bauerg@15871  186 bauerg@15871  187 wenzelm@61343  188 subsection \The tree induction principle \label{sec:calc-ctl-tree-induct}\  bauerg@15871  189 wenzelm@61343  190 text \  wenzelm@61934  191  With the most basic facts available, we are now able to establish a few more  wenzelm@63055  192  interesting results, leading to the \<^emph>\tree induction\ principle for \\<^bold>A\<^bold>G\  wenzelm@61934  193  (see below). We will use some elementary monotonicity and distributivity  wenzelm@61934  194  rules.  wenzelm@61343  195 \  bauerg@15871  196 wenzelm@63055  197 lemma AX_int: "\<^bold>A\<^bold>X (p \ q) = \<^bold>A\<^bold>X p \ \<^bold>A\<^bold>X q" by auto  wenzelm@63055  198 lemma AX_mono: "p \ q \ \<^bold>A\<^bold>X p \ \<^bold>A\<^bold>X q" by auto  wenzelm@63055  199 lemma AG_mono: "p \ q \ \<^bold>A\<^bold>G p \ \<^bold>A\<^bold>G q"  wenzelm@63055  200  by (simp only: AG_gfp, rule gfp_mono) auto  bauerg@15871  201 wenzelm@61343  202 text \  wenzelm@61934  203  The formula @{term "AG p"} implies @{term "AX p"} (we use substitution of  wenzelm@61934  204  \\\ with monotonicity).  wenzelm@61343  205 \  bauerg@15871  206 wenzelm@63055  207 lemma AG_AX: "\<^bold>A\<^bold>G p \ \<^bold>A\<^bold>X p"  bauerg@15871  208 proof -  wenzelm@63055  209  have "\<^bold>A\<^bold>G p \ \<^bold>A\<^bold>X \<^bold>A\<^bold>G p" by (rule AG_fp_2)  wenzelm@63055  210  also have "\<^bold>A\<^bold>G p \ p" by (rule AG_fp_1)  wenzelm@61934  211  moreover note AX_mono  bauerg@15871  212  finally show ?thesis .  bauerg@15871  213 qed  bauerg@15871  214 wenzelm@61343  215 text \  wenzelm@63055  216  Furthermore we show idempotency of the \\<^bold>A\<^bold>G\ operator. The proof is a good  wenzelm@61934  217  example of how accumulated facts may get used to feed a single rule step.  wenzelm@61343  218 \  bauerg@15871  219 wenzelm@63055  220 lemma AG_AG: "\<^bold>A\<^bold>G \<^bold>A\<^bold>G p = \<^bold>A\<^bold>G p"  bauerg@15871  221 proof  wenzelm@63055  222  show "\<^bold>A\<^bold>G \<^bold>A\<^bold>G p \ \<^bold>A\<^bold>G p" by (rule AG_fp_1)  bauerg@15871  223 next  wenzelm@63055  224  show "\<^bold>A\<^bold>G p \ \<^bold>A\<^bold>G \<^bold>A\<^bold>G p"  bauerg@15871  225  proof (rule AG_I)  wenzelm@63055  226  have "\<^bold>A\<^bold>G p \ \<^bold>A\<^bold>G p" ..  wenzelm@63055  227  moreover have "\<^bold>A\<^bold>G p \ \<^bold>A\<^bold>X \<^bold>A\<^bold>G p" by (rule AG_fp_2)  wenzelm@63055  228  ultimately show "\<^bold>A\<^bold>G p \ \<^bold>A\<^bold>G p \ \<^bold>A\<^bold>X \<^bold>A\<^bold>G p" ..  bauerg@15871  229  qed  bauerg@15871  230 qed  bauerg@15871  231 wenzelm@61343  232 text \  wenzelm@61934  233  \<^smallskip>  wenzelm@63055  234  We now give an alternative characterization of the \\<^bold>A\<^bold>G\ operator, which  wenzelm@63055  235  describes the \\<^bold>A\<^bold>G\ operator in an operational'' way by tree induction:  wenzelm@63055  236  In a state holds @{term "AG p"} iff in that state holds \p\, and in all  wenzelm@63055  237  reachable states \s\ follows from the fact that \p\ holds in \s\, that \p\  wenzelm@63055  238  also holds in all successor states of \s\. We use the co-induction principle  wenzelm@63055  239  @{thm [source] AG_I} to establish this in a purely algebraic manner.  wenzelm@61343  240 \  bauerg@15871  241 wenzelm@63055  242 theorem AG_induct: "p \ \<^bold>A\<^bold>G (p \ \<^bold>A\<^bold>X p) = \<^bold>A\<^bold>G p"  bauerg@15871  243 proof  wenzelm@63055  244  show "p \ \<^bold>A\<^bold>G (p \ \<^bold>A\<^bold>X p) \ \<^bold>A\<^bold>G p" (is "?lhs \ _")  bauerg@15871  245  proof (rule AG_I)  wenzelm@63055  246  show "?lhs \ p \ \<^bold>A\<^bold>X ?lhs"  bauerg@15871  247  proof  bauerg@15871  248  show "?lhs \ p" ..  wenzelm@63055  249  show "?lhs \ \<^bold>A\<^bold>X ?lhs"  bauerg@15871  250  proof -  wenzelm@32960  251  {  wenzelm@63055  252  have "\<^bold>A\<^bold>G (p \ \<^bold>A\<^bold>X p) \ p \ \<^bold>A\<^bold>X p" by (rule AG_fp_1)  wenzelm@63055  253  also have "p \ p \ \<^bold>A\<^bold>X p \ \<^bold>A\<^bold>X p" ..  wenzelm@63055  254  finally have "?lhs \ \<^bold>A\<^bold>X p" by auto  wenzelm@63055  255  }  wenzelm@32960  256  moreover  wenzelm@32960  257  {  wenzelm@63055  258  have "p \ \<^bold>A\<^bold>G (p \ \<^bold>A\<^bold>X p) \ \<^bold>A\<^bold>G (p \ \<^bold>A\<^bold>X p)" ..  wenzelm@63055  259  also have "\ \ \<^bold>A\<^bold>X \" by (rule AG_fp_2)  wenzelm@63055  260  finally have "?lhs \ \<^bold>A\<^bold>X \<^bold>A\<^bold>G (p \ \<^bold>A\<^bold>X p)" .  wenzelm@63055  261  }  wenzelm@63055  262  ultimately have "?lhs \ \<^bold>A\<^bold>X p \ \<^bold>A\<^bold>X \<^bold>A\<^bold>G (p \ \<^bold>A\<^bold>X p)" ..  wenzelm@63055  263  also have "\ = \<^bold>A\<^bold>X ?lhs" by (simp only: AX_int)  wenzelm@32960  264  finally show ?thesis .  bauerg@15871  265  qed  bauerg@15871  266  qed  bauerg@15871  267  qed  bauerg@15871  268 next  wenzelm@63055  269  show "\<^bold>A\<^bold>G p \ p \ \<^bold>A\<^bold>G (p \ \<^bold>A\<^bold>X p)"  bauerg@15871  270  proof  wenzelm@63055  271  show "\<^bold>A\<^bold>G p \ p" by (rule AG_fp_1)  wenzelm@63055  272  show "\<^bold>A\<^bold>G p \ \<^bold>A\<^bold>G (p \ \<^bold>A\<^bold>X p)"  bauerg@15871  273  proof -  wenzelm@63055  274  have "\<^bold>A\<^bold>G p = \<^bold>A\<^bold>G \<^bold>A\<^bold>G p" by (simp only: AG_AG)  wenzelm@63055  275  also have "\<^bold>A\<^bold>G p \ \<^bold>A\<^bold>X p" by (rule AG_AX) moreover note AG_mono  wenzelm@63055  276  also have "\<^bold>A\<^bold>X p \ (p \ \<^bold>A\<^bold>X p)" .. moreover note AG_mono  bauerg@15871  277  finally show ?thesis .  bauerg@15871  278  qed  bauerg@15871  279  qed  bauerg@15871  280 qed  bauerg@15871  281 bauerg@15871  282 wenzelm@61343  283 subsection \An application of tree induction \label{sec:calc-ctl-commute}\  bauerg@15871  284 wenzelm@61343  285 text \  wenzelm@61934  286  Further interesting properties of CTL expressions may be demonstrated with  wenzelm@63055  287  the help of tree induction; here we show that \\<^bold>A\<^bold>X\ and \\<^bold>A\<^bold>G\ commute.  wenzelm@61343  288 \  bauerg@15871  289 wenzelm@63055  290 theorem AG_AX_commute: "\<^bold>A\<^bold>G \<^bold>A\<^bold>X p = \<^bold>A\<^bold>X \<^bold>A\<^bold>G p"  bauerg@15871  291 proof -  wenzelm@63055  292  have "\<^bold>A\<^bold>G \<^bold>A\<^bold>X p = \<^bold>A\<^bold>X p \ \<^bold>A\<^bold>X \<^bold>A\<^bold>G \<^bold>A\<^bold>X p" by (rule AG_fp)  wenzelm@63055  293  also have "\ = \<^bold>A\<^bold>X (p \ \<^bold>A\<^bold>G \<^bold>A\<^bold>X p)" by (simp only: AX_int)  wenzelm@63055  294  also have "p \ \<^bold>A\<^bold>G \<^bold>A\<^bold>X p = \<^bold>A\<^bold>G p" (is "?lhs = _")  wenzelm@63055  295  proof  wenzelm@63055  296  have "\<^bold>A\<^bold>X p \ p \ \<^bold>A\<^bold>X p" ..  wenzelm@63055  297  also have "p \ \<^bold>A\<^bold>G (p \ \<^bold>A\<^bold>X p) = \<^bold>A\<^bold>G p" by (rule AG_induct)  bauerg@15871  298  also note Int_mono AG_mono  wenzelm@63055  299  ultimately show "?lhs \ \<^bold>A\<^bold>G p" by fast  wenzelm@63055  300  next  wenzelm@63055  301  have "\<^bold>A\<^bold>G p \ p" by (rule AG_fp_1)  wenzelm@63055  302  moreover  bauerg@15871  303  {  wenzelm@63055  304  have "\<^bold>A\<^bold>G p = \<^bold>A\<^bold>G \<^bold>A\<^bold>G p" by (simp only: AG_AG)  wenzelm@63055  305  also have "\<^bold>A\<^bold>G p \ \<^bold>A\<^bold>X p" by (rule AG_AX)  bauerg@15871  306  also note AG_mono  wenzelm@63055  307  ultimately have "\<^bold>A\<^bold>G p \ \<^bold>A\<^bold>G \<^bold>A\<^bold>X p" .  wenzelm@63055  308  }  wenzelm@63055  309  ultimately show "\<^bold>A\<^bold>G p \ ?lhs" ..  wenzelm@63055  310  qed  bauerg@15871  311  finally show ?thesis .  bauerg@15871  312 qed  bauerg@15871  313 bauerg@15871  314 end