equal
deleted
inserted
replaced
23 |
23 |
24 instance .. |
24 instance .. |
25 |
25 |
26 end |
26 end |
27 |
27 |
28 definition component_of :: "'a program =>'a program=> bool" (infixl "component'_of" 50) |
28 definition component_of :: "'a program =>'a program=> bool" (infixl \<open>component'_of\<close> 50) |
29 where "F component_of H == \<exists>G. F ok G & F\<squnion>G = H" |
29 where "F component_of H == \<exists>G. F ok G & F\<squnion>G = H" |
30 |
30 |
31 definition strict_component_of :: "'a program\<Rightarrow>'a program=> bool" (infixl "strict'_component'_of" 50) |
31 definition strict_component_of :: "'a program\<Rightarrow>'a program=> bool" (infixl \<open>strict'_component'_of\<close> 50) |
32 where "F strict_component_of H == F component_of H & F\<noteq>H" |
32 where "F strict_component_of H == F component_of H & F\<noteq>H" |
33 |
33 |
34 definition preserves :: "('a=>'b) => 'a program set" |
34 definition preserves :: "('a=>'b) => 'a program set" |
35 where "preserves v == \<Inter>z. stable {s. v s = z}" |
35 where "preserves v == \<Inter>z. stable {s. v s = z}" |
36 |
36 |