equal
deleted
inserted
replaced
76 where |
76 where |
77 reachable_0: "s : starts_of C ==> reachable C s" |
77 reachable_0: "s : starts_of C ==> reachable C s" |
78 | reachable_n: "[| reachable C s; (s, a, t) : trans_of C |] ==> reachable C t" |
78 | reachable_n: "[| reachable C s; (s, a, t) : trans_of C |] ==> reachable C t" |
79 |
79 |
80 abbreviation |
80 abbreviation |
81 trans_of_syn ("_ -_--_-> _" [81,81,81,81] 100) where |
81 trans_of_syn ("_ \<midarrow>_\<midarrow>_\<rightarrow> _" [81,81,81,81] 100) where |
82 "s -a--A-> t == (s,a,t):trans_of A" |
82 "s \<midarrow>a\<midarrow>A\<rightarrow> t == (s,a,t):trans_of A" |
83 |
|
84 notation (xsymbols) |
|
85 trans_of_syn ("_ \<midarrow>_\<midarrow>_\<longrightarrow> _" [81,81,81,81] 100) |
|
86 |
83 |
87 abbreviation "act A == actions (asig_of A)" |
84 abbreviation "act A == actions (asig_of A)" |
88 abbreviation "ext A == externals (asig_of A)" |
85 abbreviation "ext A == externals (asig_of A)" |
89 abbreviation int where "int A == internals (asig_of A)" |
86 abbreviation int where "int A == internals (asig_of A)" |
90 abbreviation "inp A == inputs (asig_of A)" |
87 abbreviation "inp A == inputs (asig_of A)" |
216 (! S : sfair_of A. S<= local A)" |
213 (! S : sfair_of A. S<= local A)" |
217 |
214 |
218 input_resistant_def: |
215 input_resistant_def: |
219 "input_resistant A == ! W : sfair_of A. ! s a t. |
216 "input_resistant A == ! W : sfair_of A. ! s a t. |
220 reachable A s & reachable A t & a:inp A & |
217 reachable A s & reachable A t & a:inp A & |
221 Enabled A W s & s -a--A-> t |
218 Enabled A W s & s \<midarrow>a\<midarrow>A\<rightarrow> t |
222 --> Enabled A W t" |
219 --> Enabled A W t" |
223 |
220 |
224 enabled_def: |
221 enabled_def: |
225 "enabled A a s == ? t. s-a--A-> t" |
222 "enabled A a s == ? t. s \<midarrow>a\<midarrow>A\<rightarrow> t" |
226 |
223 |
227 Enabled_def: |
224 Enabled_def: |
228 "Enabled A W s == ? w:W. enabled A w s" |
225 "Enabled A W s == ? w:W. enabled A w s" |
229 |
226 |
230 en_persistent_def: |
227 en_persistent_def: |
231 "en_persistent A W == ! s a t. Enabled A W s & |
228 "en_persistent A W == ! s a t. Enabled A W s & |
232 a ~:W & |
229 a ~:W & |
233 s -a--A-> t |
230 s \<midarrow>a\<midarrow>A\<rightarrow> t |
234 --> Enabled A W t" |
231 --> Enabled A W t" |
235 was_enabled_def: |
232 was_enabled_def: |
236 "was_enabled A a t == ? s. s-a--A-> t" |
233 "was_enabled A a t == ? s. s \<midarrow>a\<midarrow>A\<rightarrow> t" |
237 |
234 |
238 set_was_enabled_def: |
235 set_was_enabled_def: |
239 "set_was_enabled A W t == ? w:W. was_enabled A w t" |
236 "set_was_enabled A W t == ? w:W. was_enabled A w t" |
240 |
237 |
241 |
238 |
522 done |
519 done |
523 |
520 |
524 |
521 |
525 subsection "rename" |
522 subsection "rename" |
526 |
523 |
527 lemma trans_rename: "s -a--(rename C f)-> t ==> (? x. Some(x) = f(a) & s -x--C-> t)" |
524 lemma trans_rename: "s \<midarrow>a\<midarrow>(rename C f)\<rightarrow> t ==> (? x. Some(x) = f(a) & s \<midarrow>x\<midarrow>C\<rightarrow> t)" |
528 apply (simp add: Let_def rename_def trans_of_def) |
525 apply (simp add: Let_def rename_def trans_of_def) |
529 done |
526 done |
530 |
527 |
531 |
528 |
532 lemma reachable_rename: "[| reachable (rename C g) s |] ==> reachable C s" |
529 lemma reachable_rename: "[| reachable (rename C g) s |] ==> reachable C s" |