equal
deleted
inserted
replaced
141 done |
141 done |
142 |
142 |
143 |
143 |
144 |
144 |
145 text{* p15: universal property: all Components well behave *} |
145 text{* p15: universal property: all Components well behave *} |
146 lemma system_well_behaves [rule_format]: |
146 lemma system_well_behaves: "system \<in> Highest i co Highest i Un Lowest i" |
147 "\<forall>i. system \<in> Highest i co Highest i Un Lowest i" |
147 by (simp add: system_def Component_def mk_total_program_def totalize_JN, safety, auto) |
148 apply clarify |
|
149 apply (simp add: system_def Component_def mk_total_program_def totalize_JN, |
|
150 safety, auto) |
|
151 done |
|
152 |
148 |
153 |
149 |
154 lemma Acyclic_eq: "Acyclic = (\<Inter>i. {s. i\<notin>above i s})" |
150 lemma Acyclic_eq: "Acyclic = (\<Inter>i. {s. i\<notin>above i s})" |
155 by (auto simp add: Acyclic_def acyclic_def trancl_converse) |
151 by (auto simp add: Acyclic_def acyclic_def trancl_converse) |
156 |
152 |
157 |
153 |
158 lemmas system_co = |
154 lemmas system_co = |
159 constrains_Un [OF above_not_increase [rule_format] system_well_behaves] |
155 constrains_Un [OF above_not_increase [rule_format] system_well_behaves] |
160 |
156 |