equal
deleted
inserted
replaced
62 \ \ {\isachardoublequote}lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymsubseteq}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}\ p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}% |
62 \ \ {\isachardoublequote}lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymsubseteq}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}\ p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}% |
63 \begin{isamarkuptxt}% |
63 \begin{isamarkuptxt}% |
64 \noindent |
64 \noindent |
65 In contrast to the analogous property for \isa{EF}, and just |
65 In contrast to the analogous property for \isa{EF}, and just |
66 for a change, we do not use fixed point induction but a weaker theorem, |
66 for a change, we do not use fixed point induction but a weaker theorem, |
67 \isa{lfp{\isacharunderscore}lowerbound}: |
67 also known in the literature (after David Park) as \emph{Park-induction}: |
68 \begin{isabelle}% |
68 \begin{center} |
69 \ \ \ \ \ f\ S\ {\isasymsubseteq}\ S\ {\isasymLongrightarrow}\ lfp\ f\ {\isasymsubseteq}\ S% |
69 \isa{f\ S\ {\isasymsubseteq}\ S\ {\isasymLongrightarrow}\ lfp\ f\ {\isasymsubseteq}\ S} \hfill (\isa{lfp{\isacharunderscore}lowerbound}) |
70 \end{isabelle} |
70 \end{center} |
71 The instance of the premise \isa{f\ S\ {\isasymsubseteq}\ S} is proved pointwise, |
71 The instance of the premise \isa{f\ S\ {\isasymsubseteq}\ S} is proved pointwise, |
72 a decision that clarification takes for us:% |
72 a decision that clarification takes for us:% |
73 \end{isamarkuptxt}% |
73 \end{isamarkuptxt}% |
74 \isacommand{apply}{\isacharparenleft}rule\ lfp{\isacharunderscore}lowerbound{\isacharparenright}\isanewline |
74 \isacommand{apply}{\isacharparenleft}rule\ lfp{\isacharunderscore}lowerbound{\isacharparenright}\isanewline |
75 \isacommand{apply}{\isacharparenleft}clarsimp\ simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}% |
75 \isacommand{apply}{\isacharparenleft}clarsimp\ simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}% |