equal
deleted
inserted
replaced
7 |
7 |
8 section\<open>Weak Progress\<close> |
8 section\<open>Weak Progress\<close> |
9 |
9 |
10 theory SubstAx imports WFair Constrains begin |
10 theory SubstAx imports WFair Constrains begin |
11 |
11 |
12 definition Ensures :: "['a set, 'a set] => 'a program set" (infixl "Ensures" 60) where |
12 definition Ensures :: "['a set, 'a set] => 'a program set" (infixl \<open>Ensures\<close> 60) where |
13 "A Ensures B == {F. F \<in> (reachable F \<inter> A) ensures B}" |
13 "A Ensures B == {F. F \<in> (reachable F \<inter> A) ensures B}" |
14 |
14 |
15 definition LeadsTo :: "['a set, 'a set] => 'a program set" (infixl "LeadsTo" 60) where |
15 definition LeadsTo :: "['a set, 'a set] => 'a program set" (infixl \<open>LeadsTo\<close> 60) where |
16 "A LeadsTo B == {F. F \<in> (reachable F \<inter> A) leadsTo B}" |
16 "A LeadsTo B == {F. F \<in> (reachable F \<inter> A) leadsTo B}" |
17 |
17 |
18 notation LeadsTo (infixl "\<longmapsto>w" 60) |
18 notation LeadsTo (infixl \<open>\<longmapsto>w\<close> 60) |
19 |
19 |
20 |
20 |
21 text\<open>Resembles the previous definition of LeadsTo\<close> |
21 text\<open>Resembles the previous definition of LeadsTo\<close> |
22 lemma LeadsTo_eq_leadsTo: |
22 lemma LeadsTo_eq_leadsTo: |
23 "A LeadsTo B = {F. F \<in> (reachable F \<inter> A) leadsTo (reachable F \<inter> B)}" |
23 "A LeadsTo B = {F. F \<in> (reachable F \<inter> A) leadsTo (reachable F \<inter> B)}" |