summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sat, 26 Dec 2015 16:10:00 +0100 | |

changeset 61934 | 02610a806467 |

parent 61933 | cf58b5b794b2 |

child 61935 | 6512e84cc9f5 |

tuned;

--- a/src/HOL/ex/CTL.thy Sat Dec 26 15:59:27 2015 +0100 +++ b/src/HOL/ex/CTL.thy Sat Dec 26 16:10:00 2015 +0100 @@ -9,16 +9,16 @@ begin text \<open> - We formalize basic concepts of Computational Tree Logic (CTL) - @{cite "McMillan-PhDThesis" and "McMillan-LectureNotes"} within the - simply-typed set theory of HOL. + We formalize basic concepts of Computational Tree Logic (CTL) @{cite + "McMillan-PhDThesis" and "McMillan-LectureNotes"} within the simply-typed + set theory of HOL. - By using the common technique of ``shallow embedding'', a CTL - formula is identified with the corresponding set of states where it - holds. Consequently, CTL operations such as negation, conjunction, - disjunction simply become complement, intersection, union of sets. - We only require a separate operation for implication, as point-wise - inclusion is usually not encountered in plain set-theory. + By using the common technique of ``shallow embedding'', a CTL formula is + identified with the corresponding set of states where it holds. + Consequently, CTL operations such as negation, conjunction, disjunction + simply become complement, intersection, union of sets. We only require a + separate operation for implication, as point-wise inclusion is usually not + encountered in plain set-theory. \<close> lemmas [intro!] = Int_greatest Un_upper2 Un_upper1 Int_lower1 Int_lower2 @@ -34,55 +34,52 @@ text \<open> - \smallskip The CTL path operators are more interesting; they are - based on an arbitrary, but fixed model \<open>\<M>\<close>, which is simply - a transition relation over states @{typ "'a"}. + \<^smallskip> + The CTL path operators are more interesting; they are based on an arbitrary, + but fixed model \<open>\<M>\<close>, which is simply a transition relation over states + @{typ 'a}. \<close> axiomatization \<M> :: "('a \<times> 'a) set" text \<open> - The operators \<open>\<EX>\<close>, \<open>\<EF>\<close>, \<open>\<EG>\<close> are taken - as primitives, while \<open>\<AX>\<close>, \<open>\<AF>\<close>, \<open>\<AG>\<close> are - defined as derived ones. The formula \<open>\<EX> p\<close> holds in a - state @{term s}, iff there is a successor state @{term s'} (with - respect to the model @{term \<M>}), such that @{term p} holds in - @{term s'}. The formula \<open>\<EF> p\<close> holds in a state @{term - s}, iff there is a path in \<open>\<M>\<close>, starting from @{term s}, - such that there exists a state @{term s'} on the path, such that - @{term p} holds in @{term s'}. The formula \<open>\<EG> p\<close> holds - in a state @{term s}, iff there is a path, starting from @{term s}, - such that for all states @{term s'} on the path, @{term p} holds in - @{term s'}. It is easy to see that \<open>\<EF> p\<close> and \<open>\<EG> p\<close> may be expressed using least and greatest fixed points - @{cite "McMillan-PhDThesis"}. + The operators \<open>\<EX>\<close>, \<open>\<EF>\<close>, \<open>\<EG>\<close> are taken as primitives, while + \<open>\<AX>\<close>, \<open>\<AF>\<close>, \<open>\<AG>\<close> are defined as derived ones. The formula \<open>\<EX> p\<close> + holds in a state @{term s}, iff there is a successor state @{term s'} (with + respect to the model @{term \<M>}), such that @{term p} holds in @{term s'}. + The formula \<open>\<EF> p\<close> holds in a state @{term s}, iff there is a path in + \<open>\<M>\<close>, starting from @{term s}, such that there exists a state @{term s'} on + the path, such that @{term p} holds in @{term s'}. The formula \<open>\<EG> p\<close> + holds in a state @{term s}, iff there is a path, starting from @{term s}, + such that for all states @{term s'} on the path, @{term p} holds in @{term + s'}. It is easy to see that \<open>\<EF> p\<close> and \<open>\<EG> p\<close> may be expressed using + least and greatest fixed points @{cite "McMillan-PhDThesis"}. \<close> -definition - EX ("\<EX> _" [80] 90) where "\<EX> p = {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}" -definition - EF ("\<EF> _" [80] 90) where "\<EF> p = lfp (\<lambda>s. p \<union> \<EX> s)" -definition - EG ("\<EG> _" [80] 90) where "\<EG> p = gfp (\<lambda>s. p \<inter> \<EX> s)" +definition EX ("\<EX> _" [80] 90) + where [simp]: "\<EX> p = {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}" +definition EF ("\<EF> _" [80] 90) + where [simp]: "\<EF> p = lfp (\<lambda>s. p \<union> \<EX> s)" +definition EG ("\<EG> _" [80] 90) + where [simp]: "\<EG> p = gfp (\<lambda>s. p \<inter> \<EX> s)" text \<open> - \<open>\<AX>\<close>, \<open>\<AF>\<close> and \<open>\<AG>\<close> are now defined - dually in terms of \<open>\<EX>\<close>, \<open>\<EF>\<close> and \<open>\<EG>\<close>. + \<open>\<AX>\<close>, \<open>\<AF>\<close> and \<open>\<AG>\<close> are now defined dually in terms of \<open>\<EX>\<close>, + \<open>\<EF>\<close> and \<open>\<EG>\<close>. \<close> -definition - AX ("\<AX> _" [80] 90) where "\<AX> p = - \<EX> - p" -definition - AF ("\<AF> _" [80] 90) where "\<AF> p = - \<EG> - p" -definition - AG ("\<AG> _" [80] 90) where "\<AG> p = - \<EF> - p" - -lemmas [simp] = EX_def EG_def AX_def EF_def AF_def AG_def +definition AX ("\<AX> _" [80] 90) + where [simp]: "\<AX> p = - \<EX> - p" +definition AF ("\<AF> _" [80] 90) + where [simp]: "\<AF> p = - \<EG> - p" +definition AG ("\<AG> _" [80] 90) + where [simp]: "\<AG> p = - \<EF> - p" subsection \<open>Basic fixed point properties\<close> text \<open> - First of all, we use the de-Morgan property of fixed points + First of all, we use the de-Morgan property of fixed points. \<close> lemma lfp_gfp: "lfp f = - gfp (\<lambda>s::'a set. - (f (- s)))" @@ -118,12 +115,14 @@ by (simp add: lfp_gfp) text \<open> - in order to give dual fixed point representations of @{term "AF p"} - and @{term "AG p"}: + In order to give dual fixed point representations of @{term "\<AF> p"} and + @{term "\<AG> p"}: \<close> -lemma AF_lfp: "\<AF> p = lfp (\<lambda>s. p \<union> \<AX> s)" by (simp add: lfp_gfp) -lemma AG_gfp: "\<AG> p = gfp (\<lambda>s. p \<inter> \<AX> s)" by (simp add: lfp_gfp) +lemma AF_lfp: "\<AF> p = lfp (\<lambda>s. p \<union> \<AX> s)" + by (simp add: lfp_gfp) +lemma AG_gfp: "\<AG> p = gfp (\<lambda>s. p \<inter> \<AX> s)" + by (simp add: lfp_gfp) lemma EF_fp: "\<EF> p = p \<union> \<EX> \<EF> p" proof - @@ -144,10 +143,10 @@ qed text \<open> - From the greatest fixed point definition of @{term "\<AG> p"}, we - derive as a consequence of the Knaster-Tarski theorem on the one - hand that @{term "\<AG> p"} is a fixed point of the monotonic - function @{term "\<lambda>s. p \<inter> \<AX> s"}. + From the greatest fixed point definition of @{term "\<AG> p"}, we derive as + a consequence of the Knaster-Tarski theorem on the one hand that @{term + "\<AG> p"} is a fixed point of the monotonic function + @{term "\<lambda>s. p \<inter> \<AX> s"}. \<close> lemma AG_fp: "\<AG> p = p \<inter> \<AX> \<AG> p" @@ -157,9 +156,8 @@ qed text \<open> - This fact may be split up into two inequalities (merely using - transitivity of \<open>\<subseteq>\<close>, which is an instance of the overloaded - \<open>\<le>\<close> in Isabelle/HOL). + This fact may be split up into two inequalities (merely using transitivity + of \<open>\<subseteq>\<close>, which is an instance of the overloaded \<open>\<le>\<close> in Isabelle/HOL). \<close> lemma AG_fp_1: "\<AG> p \<subseteq> p" @@ -175,11 +173,11 @@ qed text \<open> - On the other hand, we have from the Knaster-Tarski fixed point - theorem that any other post-fixed point of @{term "\<lambda>s. p \<inter> AX s"} is - smaller than @{term "AG p"}. A post-fixed point is a set of states - @{term q} such that @{term "q \<subseteq> p \<inter> AX q"}. This leads to the - following co-induction principle for @{term "AG p"}. + On the other hand, we have from the Knaster-Tarski fixed point theorem that + any other post-fixed point of @{term "\<lambda>s. p \<inter> \<AX> s"} is smaller than + @{term "\<AG> p"}. A post-fixed point is a set of states @{term q} such that + @{term "q \<subseteq> p \<inter> \<AX> q"}. This leads to the following co-induction + principle for @{term "\<AG> p"}. \<close> lemma AG_I: "q \<subseteq> p \<inter> \<AX> q \<Longrightarrow> q \<subseteq> \<AG> p" @@ -189,10 +187,10 @@ subsection \<open>The tree induction principle \label{sec:calc-ctl-tree-induct}\<close> text \<open> - With the most basic facts available, we are now able to establish a - few more interesting results, leading to the \emph{tree induction} - principle for \<open>AG\<close> (see below). We will use some elementary - monotonicity and distributivity rules. + With the most basic facts available, we are now able to establish a few more + interesting results, leading to the \<^emph>\<open>tree induction\<close> principle for \<open>\<AG>\<close> + (see below). We will use some elementary monotonicity and distributivity + rules. \<close> lemma AX_int: "\<AX> (p \<inter> q) = \<AX> p \<inter> \<AX> q" by auto @@ -201,21 +199,21 @@ by (simp only: AG_gfp, rule gfp_mono) auto text \<open> - The formula @{term "AG p"} implies @{term "AX p"} (we use - substitution of \<open>\<subseteq>\<close> with monotonicity). + The formula @{term "AG p"} implies @{term "AX p"} (we use substitution of + \<open>\<subseteq>\<close> with monotonicity). \<close> lemma AG_AX: "\<AG> p \<subseteq> \<AX> p" proof - have "\<AG> p \<subseteq> \<AX> \<AG> p" by (rule AG_fp_2) - also have "\<AG> p \<subseteq> p" by (rule AG_fp_1) moreover note AX_mono + also have "\<AG> p \<subseteq> p" by (rule AG_fp_1) + moreover note AX_mono finally show ?thesis . qed text \<open> - Furthermore we show idempotency of the \<open>\<AG>\<close> operator. - The proof is a good example of how accumulated facts may get - used to feed a single rule step. + Furthermore we show idempotency of the \<open>\<AG>\<close> operator. The proof is a good + example of how accumulated facts may get used to feed a single rule step. \<close> lemma AG_AG: "\<AG> \<AG> p = \<AG> p" @@ -231,13 +229,14 @@ qed text \<open> - \smallskip We now give an alternative characterization of the \<open>\<AG>\<close> operator, which describes the \<open>\<AG>\<close> operator in - an ``operational'' way by tree induction: In a state holds @{term - "AG p"} iff in that state holds @{term p}, and in all reachable - states @{term s} follows from the fact that @{term p} holds in - @{term s}, that @{term p} also holds in all successor states of - @{term s}. We use the co-induction principle @{thm [source] AG_I} - to establish this in a purely algebraic manner. + \<^smallskip> + We now give an alternative characterization of the \<open>\<AG>\<close> operator, which + describes the \<open>\<AG>\<close> operator in an ``operational'' way by tree induction: + In a state holds @{term "AG p"} iff in that state holds @{term p}, and in + all reachable states @{term s} follows from the fact that @{term p} holds in + @{term s}, that @{term p} also holds in all successor states of @{term s}. + We use the co-induction principle @{thm [source] AG_I} to establish this in + a purely algebraic manner. \<close> theorem AG_induct: "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p" @@ -284,9 +283,8 @@ subsection \<open>An application of tree induction \label{sec:calc-ctl-commute}\<close> text \<open> - Further interesting properties of CTL expressions may be - demonstrated with the help of tree induction; here we show that - \<open>\<AX>\<close> and \<open>\<AG>\<close> commute. + Further interesting properties of CTL expressions may be demonstrated with + the help of tree induction; here we show that \<open>\<AX>\<close> and \<open>\<AG>\<close> commute. \<close> theorem AG_AX_commute: "\<AG> \<AX> p = \<AX> \<AG> p"