equal
deleted
inserted
replaced
48 (* post_conditions for actions and action sets *) |
48 (* post_conditions for actions and action sets *) |
49 |
49 |
50 was_enabled ::"('a,'s)ioa => 'a => 's => bool" |
50 was_enabled ::"('a,'s)ioa => 'a => 's => bool" |
51 set_was_enabled ::"('a,'s)ioa => 'a set => 's => bool" |
51 set_was_enabled ::"('a,'s)ioa => 'a set => 's => bool" |
52 |
52 |
53 (* reachability and invariants *) |
53 (* invariants *) |
54 reachable :: "('a,'s)ioa => 's set" |
|
55 invariant :: "[('a,'s)ioa, 's=>bool] => bool" |
54 invariant :: "[('a,'s)ioa, 's=>bool] => bool" |
56 |
55 |
57 (* binary composition of action signatures and automata *) |
56 (* binary composition of action signatures and automata *) |
58 asig_comp ::"['a signature, 'a signature] => 'a signature" |
57 asig_comp ::"['a signature, 'a signature] => 'a signature" |
59 compatible ::"[('a,'s)ioa, ('a,'t)ioa] => bool" |
58 compatible ::"[('a,'s)ioa, ('a,'t)ioa] => bool" |
71 |
70 |
72 |
71 |
73 syntax |
72 syntax |
74 |
73 |
75 "_trans_of" :: "'s => 'a => ('a,'s)ioa => 's => bool" ("_ -_--_-> _" [81,81,81,81] 100) |
74 "_trans_of" :: "'s => 'a => ('a,'s)ioa => 's => bool" ("_ -_--_-> _" [81,81,81,81] 100) |
76 "reachable" :: "[('a,'s)ioa, 's] => bool" |
|
77 "act" :: "('a,'s)ioa => 'a set" |
75 "act" :: "('a,'s)ioa => 'a set" |
78 "ext" :: "('a,'s)ioa => 'a set" |
76 "ext" :: "('a,'s)ioa => 'a set" |
79 "int" :: "('a,'s)ioa => 'a set" |
77 "int" :: "('a,'s)ioa => 'a set" |
80 "inp" :: "('a,'s)ioa => 'a set" |
78 "inp" :: "('a,'s)ioa => 'a set" |
81 "out" :: "('a,'s)ioa => 'a set" |
79 "out" :: "('a,'s)ioa => 'a set" |
89 |
87 |
90 notation (xsymbols) |
88 notation (xsymbols) |
91 par (infixr "\<parallel>" 10) |
89 par (infixr "\<parallel>" 10) |
92 |
90 |
93 |
91 |
94 inductive "reachable C" |
92 inductive |
95 intros |
93 reachable :: "('a, 's) ioa => 's => bool" |
96 reachable_0: "s:(starts_of C) ==> s : reachable C" |
94 for C :: "('a, 's) ioa" |
97 reachable_n: "[|s:reachable C; (s,a,t):trans_of C|] ==> t:reachable C" |
95 where |
|
96 reachable_0: "s : starts_of C ==> reachable C s" |
|
97 | reachable_n: "[| reachable C s; (s, a, t) : trans_of C |] ==> reachable C t" |
98 |
98 |
99 |
99 |
100 translations |
100 translations |
101 "s -a--A-> t" == "(s,a,t):trans_of A" |
101 "s -a--A-> t" == "(s,a,t):trans_of A" |
102 "reachable A s" == "s:reachable A" |
|
103 "act A" == "actions (asig_of A)" |
102 "act A" == "actions (asig_of A)" |
104 "ext A" == "externals (asig_of A)" |
103 "ext A" == "externals (asig_of A)" |
105 "int A" == "internals (asig_of A)" |
104 "int A" == "internals (asig_of A)" |
106 "inp A" == "inputs (asig_of A)" |
105 "inp A" == "inputs (asig_of A)" |
107 "out A" == "outputs (asig_of A)" |
106 "out A" == "outputs (asig_of A)" |
479 !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] |
478 !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] |
480 ==> invariant A P" |
479 ==> invariant A P" |
481 apply (unfold invariant_def) |
480 apply (unfold invariant_def) |
482 apply (rule allI) |
481 apply (rule allI) |
483 apply (rule impI) |
482 apply (rule impI) |
484 apply (rule_tac xa = "s" in reachable.induct) |
483 apply (rule_tac x = "s" in reachable.induct) |
485 apply assumption |
484 apply assumption |
486 apply blast |
485 apply blast |
487 apply blast |
486 apply blast |
488 done |
487 done |
489 |
488 |