equal
deleted
inserted
replaced
108 "lfp(af A) \<subseteq> {s. \<forall> p \<in> Paths s. \<exists> i. p i \<in> A}"; |
108 "lfp(af A) \<subseteq> {s. \<forall> p \<in> Paths s. \<exists> i. p i \<in> A}"; |
109 |
109 |
110 txt{*\noindent |
110 txt{*\noindent |
111 In contrast to the analogous property for @{term EF}, and just |
111 In contrast to the analogous property for @{term EF}, and just |
112 for a change, we do not use fixed point induction but a weaker theorem, |
112 for a change, we do not use fixed point induction but a weaker theorem, |
113 @{thm[source]lfp_lowerbound}: |
113 also known in the literature (after David Park) as \emph{Park-induction}: |
114 @{thm[display]lfp_lowerbound[of _ "S",no_vars]} |
114 \begin{center} |
|
115 @{thm lfp_lowerbound[of _ "S",no_vars]} \hfill (@{thm[source]lfp_lowerbound}) |
|
116 \end{center} |
115 The instance of the premise @{prop"f S \<subseteq> S"} is proved pointwise, |
117 The instance of the premise @{prop"f S \<subseteq> S"} is proved pointwise, |
116 a decision that clarification takes for us: |
118 a decision that clarification takes for us: |
117 *}; |
119 *}; |
118 apply(rule lfp_lowerbound); |
120 apply(rule lfp_lowerbound); |
119 apply(clarsimp simp add: af_def Paths_def); |
121 apply(clarsimp simp add: af_def Paths_def); |