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 |
26 |
27 definition |
27 definition |
28 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) where |
29 "p \<rightarrow> q = - p \<union> q" |
29 "p \<rightarrow> q = - p \<union> q" |
30 |
30 |
31 lemma [intro!]: "p \<inter> p \<rightarrow> q \<subseteq> q" unfolding imp_def by auto |
31 lemma [intro!]: "p \<inter> p \<rightarrow> q \<subseteq> q" unfolding imp_def by auto |
32 lemma [intro!]: "p \<subseteq> (q \<rightarrow> p)" unfolding imp_def by rule |
32 lemma [intro!]: "p \<subseteq> (q \<rightarrow> p)" unfolding imp_def by rule |
33 |
33 |
56 "\<EG> p"} may be expressed using least and greatest fixed points |
56 "\<EG> p"} may be expressed using least and greatest fixed points |
57 \cite{McMillan-PhDThesis}. |
57 \cite{McMillan-PhDThesis}. |
58 *} |
58 *} |
59 |
59 |
60 definition |
60 definition |
61 EX :: "'a ctl \<Rightarrow> 'a ctl" ("\<EX> _" [80] 90) "\<EX> p = {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}" |
61 EX ("\<EX> _" [80] 90) where "\<EX> p = {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}" |
62 EF :: "'a ctl \<Rightarrow> 'a ctl" ("\<EF> _" [80] 90) "\<EF> p = lfp (\<lambda>s. p \<union> \<EX> s)" |
62 definition |
63 EG :: "'a ctl \<Rightarrow> 'a ctl" ("\<EG> _" [80] 90) "\<EG> p = gfp (\<lambda>s. p \<inter> \<EX> s)" |
63 EF ("\<EF> _" [80] 90) where "\<EF> p = lfp (\<lambda>s. p \<union> \<EX> s)" |
|
64 definition |
|
65 EG ("\<EG> _" [80] 90) where "\<EG> p = gfp (\<lambda>s. p \<inter> \<EX> s)" |
64 |
66 |
65 text {* |
67 text {* |
66 @{text "\<AX>"}, @{text "\<AF>"} and @{text "\<AG>"} are now defined |
68 @{text "\<AX>"}, @{text "\<AF>"} and @{text "\<AG>"} are now defined |
67 dually in terms of @{text "\<EX>"}, @{text "\<EF>"} and @{text |
69 dually in terms of @{text "\<EX>"}, @{text "\<EF>"} and @{text |
68 "\<EG>"}. |
70 "\<EG>"}. |
69 *} |
71 *} |
70 |
72 |
71 definition |
73 definition |
72 AX :: "'a ctl \<Rightarrow> 'a ctl" ("\<AX> _" [80] 90) "\<AX> p = - \<EX> - p" |
74 AX ("\<AX> _" [80] 90) where "\<AX> p = - \<EX> - p" |
73 AF :: "'a ctl \<Rightarrow> 'a ctl" ("\<AF> _" [80] 90) "\<AF> p = - \<EG> - p" |
75 definition |
74 AG :: "'a ctl \<Rightarrow> 'a ctl" ("\<AG> _" [80] 90) "\<AG> p = - \<EF> - p" |
76 AF ("\<AF> _" [80] 90) where "\<AF> p = - \<EG> - p" |
|
77 definition |
|
78 AG ("\<AG> _" [80] 90) where "\<AG> p = - \<EF> - p" |
75 |
79 |
76 lemmas [simp] = EX_def EG_def AX_def EF_def AF_def AG_def |
80 lemmas [simp] = EX_def EG_def AX_def EF_def AF_def AG_def |
77 |
81 |
78 |
82 |
79 section {* Basic fixed point properties *} |
83 section {* Basic fixed point properties *} |