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