21 *} |
21 *} |
22 |
22 |
23 lemmas [intro!] = Int_greatest Un_upper2 Un_upper1 Int_lower1 Int_lower2 |
23 lemmas [intro!] = Int_greatest Un_upper2 Un_upper1 Int_lower1 Int_lower2 |
24 |
24 |
25 types 'a ctl = "'a set" |
25 types 'a ctl = "'a set" |
26 constdefs |
26 |
|
27 definition |
27 imp :: "'a ctl \<Rightarrow> 'a ctl \<Rightarrow> 'a ctl" (infixr "\<rightarrow>" 75) |
28 imp :: "'a ctl \<Rightarrow> 'a ctl \<Rightarrow> 'a ctl" (infixr "\<rightarrow>" 75) |
28 "p \<rightarrow> q \<equiv> - p \<union> q" |
29 "p \<rightarrow> q = - p \<union> q" |
29 |
30 |
30 lemma [intro!]: "p \<inter> p \<rightarrow> q \<subseteq> q" by (unfold imp_def) auto |
31 lemma [intro!]: "p \<inter> p \<rightarrow> q \<subseteq> q" unfolding imp_def by auto |
31 lemma [intro!]: "p \<subseteq> (q \<rightarrow> p)" by (unfold imp_def) rule |
32 lemma [intro!]: "p \<subseteq> (q \<rightarrow> p)" unfolding imp_def by rule |
32 |
33 |
33 |
34 |
34 text {* |
35 text {* |
35 \smallskip The CTL path operators are more interesting; they are |
36 \smallskip The CTL path operators are more interesting; they are |
36 based on an arbitrary, but fixed model @{text \<M>}, which is simply |
37 based on an arbitrary, but fixed model @{text \<M>}, which is simply |
37 a transition relation over states @{typ "'a"}. |
38 a transition relation over states @{typ "'a"}. |
38 *} |
39 *} |
39 |
40 |
40 consts model :: "('a \<times> 'a) set" ("\<M>") |
41 axiomatization \<M> :: "('a \<times> 'a) set" |
41 |
42 |
42 text {* |
43 text {* |
43 The operators @{text \<EX>}, @{text \<EF>}, @{text \<EG>} are taken |
44 The operators @{text \<EX>}, @{text \<EF>}, @{text \<EG>} are taken |
44 as primitives, while @{text \<AX>}, @{text \<AF>}, @{text \<AG>} are |
45 as primitives, while @{text \<AX>}, @{text \<AF>}, @{text \<AG>} are |
45 defined as derived ones. The formula @{text "\<EX> p"} holds in a |
46 defined as derived ones. The formula @{text "\<EX> p"} holds in a |
54 @{term s'}. It is easy to see that @{text "\<EF> p"} and @{text |
55 @{term s'}. It is easy to see that @{text "\<EF> p"} and @{text |
55 "\<EG> p"} may be expressed using least and greatest fixed points |
56 "\<EG> p"} may be expressed using least and greatest fixed points |
56 \cite{McMillan-PhDThesis}. |
57 \cite{McMillan-PhDThesis}. |
57 *} |
58 *} |
58 |
59 |
59 constdefs |
60 definition |
60 EX :: "'a ctl \<Rightarrow> 'a ctl" ("\<EX> _" [80] 90) "\<EX> p \<equiv> {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}" |
61 EX :: "'a ctl \<Rightarrow> 'a ctl" ("\<EX> _" [80] 90) "\<EX> p = {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}" |
61 EF :: "'a ctl \<Rightarrow> 'a ctl" ("\<EF> _" [80] 90) "\<EF> p \<equiv> lfp (\<lambda>s. p \<union> \<EX> s)" |
62 EF :: "'a ctl \<Rightarrow> 'a ctl" ("\<EF> _" [80] 90) "\<EF> p = lfp (\<lambda>s. p \<union> \<EX> s)" |
62 EG :: "'a ctl \<Rightarrow> 'a ctl" ("\<EG> _" [80] 90) "\<EG> p \<equiv> gfp (\<lambda>s. p \<inter> \<EX> s)" |
63 EG :: "'a ctl \<Rightarrow> 'a ctl" ("\<EG> _" [80] 90) "\<EG> p = gfp (\<lambda>s. p \<inter> \<EX> s)" |
63 |
64 |
64 text {* |
65 text {* |
65 @{text "\<AX>"}, @{text "\<AF>"} and @{text "\<AG>"} are now defined |
66 @{text "\<AX>"}, @{text "\<AF>"} and @{text "\<AG>"} are now defined |
66 dually in terms of @{text "\<EX>"}, @{text "\<EF>"} and @{text |
67 dually in terms of @{text "\<EX>"}, @{text "\<EF>"} and @{text |
67 "\<EG>"}. |
68 "\<EG>"}. |
68 *} |
69 *} |
69 |
70 |
70 constdefs |
71 definition |
71 AX :: "'a ctl \<Rightarrow> 'a ctl" ("\<AX> _" [80] 90) "\<AX> p \<equiv> - \<EX> - p" |
72 AX :: "'a ctl \<Rightarrow> 'a ctl" ("\<AX> _" [80] 90) "\<AX> p = - \<EX> - p" |
72 AF :: "'a ctl \<Rightarrow> 'a ctl" ("\<AF> _" [80] 90) "\<AF> p \<equiv> - \<EG> - p" |
73 AF :: "'a ctl \<Rightarrow> 'a ctl" ("\<AF> _" [80] 90) "\<AF> p = - \<EG> - p" |
73 AG :: "'a ctl \<Rightarrow> 'a ctl" ("\<AG> _" [80] 90) "\<AG> p \<equiv> - \<EF> - p" |
74 AG :: "'a ctl \<Rightarrow> 'a ctl" ("\<AG> _" [80] 90) "\<AG> p = - \<EF> - p" |
74 |
75 |
75 lemmas [simp] = EX_def EG_def AX_def EF_def AF_def AG_def |
76 lemmas [simp] = EX_def EG_def AX_def EF_def AF_def AG_def |
76 |
77 |
77 |
78 |
78 section {* Basic fixed point properties *} |
79 section {* Basic fixed point properties *} |
160 lemma AG_fp_1: "\<AG> p \<subseteq> p" |
161 lemma AG_fp_1: "\<AG> p \<subseteq> p" |
161 proof - |
162 proof - |
162 note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> p" by auto |
163 note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> p" by auto |
163 finally show ?thesis . |
164 finally show ?thesis . |
164 qed |
165 qed |
165 |
|
166 text {**} |
|
167 |
166 |
168 lemma AG_fp_2: "\<AG> p \<subseteq> \<AX> \<AG> p" |
167 lemma AG_fp_2: "\<AG> p \<subseteq> \<AX> \<AG> p" |
169 proof - |
168 proof - |
170 note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> \<AX> \<AG> p" by auto |
169 note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> \<AX> \<AG> p" by auto |
171 finally show ?thesis . |
170 finally show ?thesis . |