author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 44066  d74182c93f04 
child 58889  5b7a9633cfa8 
permissions  rwrr 
4530  1 
(* Title: HOL/IOA/IOA.thy 
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

2 
Author: Tobias Nipkow & Konrad Slind 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

3 
Copyright 1994 TU Muenchen 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

4 
*) 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

5 

17288  6 
header {* The I/O automata of Lynch and Tuttle *} 
7 

8 
theory IOA 

9 
imports Asig 

10 
begin 

3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

11 

42174  12 
type_synonym 'a seq = "nat => 'a" 
13 
type_synonym 'a oseq = "nat => 'a option" 

14 
type_synonym ('a, 'b) execution = "'a oseq * 'b seq" 

15 
type_synonym ('a, 's) transition = "('s * 'a * 's)" 

16 
type_synonym ('a,'s) ioa = "'a signature * 's set * ('a, 's) transition set" 

3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

17 

984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

18 
consts 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

19 

984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

20 
(* IO automata *) 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

21 
state_trans::"['action signature, ('action,'state)transition set] => bool" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

22 
asig_of ::"('action,'state)ioa => 'action signature" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

23 
starts_of ::"('action,'state)ioa => 'state set" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

24 
trans_of ::"('action,'state)ioa => ('action,'state)transition set" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

25 
IOA ::"('action,'state)ioa => bool" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

26 

984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

27 
(* Executions, schedules, and traces *) 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

28 

17288  29 
is_execution_fragment ::"[('action,'state)ioa, ('action,'state)execution] => bool" 
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

30 
has_execution ::"[('action,'state)ioa, ('action,'state)execution] => bool" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

31 
executions :: "('action,'state)ioa => ('action,'state)execution set" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

32 
mk_trace :: "[('action,'state)ioa, 'action oseq] => 'action oseq" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

33 
reachable :: "[('action,'state)ioa, 'state] => bool" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

34 
invariant :: "[('action,'state)ioa, 'state=>bool] => bool" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

35 
has_trace :: "[('action,'state)ioa, 'action oseq] => bool" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

36 
traces :: "('action,'state)ioa => 'action oseq set" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

37 
NF :: "'a oseq => 'a oseq" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

38 

984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

39 
(* Composition of action signatures and automata *) 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

40 
compatible_asigs ::"('a => 'action signature) => bool" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

41 
asig_composition ::"('a => 'action signature) => 'action signature" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

42 
compatible_ioas ::"('a => ('action,'state)ioa) => bool" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

43 
ioa_composition ::"('a => ('action, 'state)ioa) =>('action,'a => 'state)ioa" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

44 

984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

45 
(* binary composition of action signatures and automata *) 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

46 
compat_asigs ::"['action signature, 'action signature] => bool" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

47 
asig_comp ::"['action signature, 'action signature] => 'action signature" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

48 
compat_ioas ::"[('action,'s)ioa, ('action,'t)ioa] => bool" 
17288  49 
par ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa" (infixr "" 10) 
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

50 

984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

51 
(* Filtering and hiding *) 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

52 
filter_oseq :: "('a => bool) => 'a oseq => 'a oseq" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

53 

984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

54 
restrict_asig :: "['a signature, 'a set] => 'a signature" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

55 
restrict :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

56 

984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

57 
(* Notions of correctness *) 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

58 
ioa_implements :: "[('action,'state1)ioa, ('action,'state2)ioa] => bool" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

59 

984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

60 
(* Instantiation of abstract IOA by concrete actions *) 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

61 
rename:: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

62 

984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

63 
defs 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

64 

17288  65 
state_trans_def: 
66 
"state_trans asig R == 

67 
(!triple. triple:R > fst(snd(triple)):actions(asig)) & 

3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

68 
(!a. (a:inputs(asig)) > (!s1. ? s2. (s1,a,s2):R))" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

69 

984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

70 

17288  71 
asig_of_def: "asig_of == fst" 
72 
starts_of_def: "starts_of == (fst o snd)" 

73 
trans_of_def: "trans_of == (snd o snd)" 

3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

74 

17288  75 
ioa_def: 
76 
"IOA(ioa) == (is_asig(asig_of(ioa)) & 

77 
(~ starts_of(ioa) = {}) & 

3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

78 
state_trans (asig_of ioa) (trans_of ioa))" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

79 

984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

80 

984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

81 
(* An execution fragment is modelled with a pair of sequences: 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

82 
* the first is the action options, the second the state sequence. 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

83 
* Finite executions have None actions from some point on. 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

84 
*******) 
17288  85 
is_execution_fragment_def: 
86 
"is_execution_fragment A ex == 

87 
let act = fst(ex); state = snd(ex) 

88 
in !n a. (act(n)=None > state(Suc(n)) = state(n)) & 

3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

89 
(act(n)=Some(a) > (state(n),a,state(Suc(n))):trans_of(A))" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

90 

984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

91 

17288  92 
executions_def: 
93 
"executions(ioa) == {e. snd e 0:starts_of(ioa) & 

3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

94 
is_execution_fragment ioa e}" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

95 

17288  96 

97 
reachable_def: 

3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

98 
"reachable ioa s == (? ex:executions(ioa). ? n. (snd ex n) = s)" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

99 

984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

100 

17288  101 
invariant_def: "invariant A P == (!s. reachable A s > P(s))" 
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

102 

984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

103 

984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

104 
(* Restrict the trace to those members of the set s *) 
17288  105 
filter_oseq_def: 
106 
"filter_oseq p s == 

107 
(%i. case s(i) 

108 
of None => None 

3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

109 
 Some(x) => if p x then Some x else None)" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

110 

984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

111 

17288  112 
mk_trace_def: 
3842  113 
"mk_trace(ioa) == filter_oseq(%a. a:externals(asig_of(ioa)))" 
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

114 

984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

115 

984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

116 
(* Does an ioa have an execution with the given trace *) 
17288  117 
has_trace_def: 
118 
"has_trace ioa b == 

3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

119 
(? ex:executions(ioa). b = mk_trace ioa (fst ex))" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

120 

17288  121 
normal_form_def: 
122 
"NF(tr) == @nf. ? f. mono(f) & (!i. nf(i)=tr(f(i))) & 

123 
(!j. j ~: range(f) > nf(j)= None) & 

3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

124 
(!i. nf(i)=None > (nf (Suc i)) = None) " 
17288  125 

3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

126 
(* All the traces of an ioa *) 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

127 

17288  128 
traces_def: 
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

129 
"traces(ioa) == {trace. ? tr. trace=NF(tr) & has_trace ioa tr}" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

130 

984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

131 
(* 
17288  132 
traces_def: 
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

133 
"traces(ioa) == {tr. has_trace ioa tr}" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

134 
*) 
17288  135 

136 
compat_asigs_def: 

137 
"compat_asigs a1 a2 == 

138 
(((outputs(a1) Int outputs(a2)) = {}) & 

139 
((internals(a1) Int actions(a2)) = {}) & 

3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

140 
((internals(a2) Int actions(a1)) = {}))" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

141 

984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

142 

17288  143 
compat_ioas_def: 
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

144 
"compat_ioas ioa1 ioa2 == compat_asigs (asig_of(ioa1)) (asig_of(ioa2))" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

145 

984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

146 

17288  147 
asig_comp_def: 
148 
"asig_comp a1 a2 == 

149 
(((inputs(a1) Un inputs(a2))  (outputs(a1) Un outputs(a2)), 

150 
(outputs(a1) Un outputs(a2)), 

3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

151 
(internals(a1) Un internals(a2))))" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

152 

984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

153 

17288  154 
par_def: 
155 
"(ioa1  ioa2) == 

156 
(asig_comp (asig_of ioa1) (asig_of ioa2), 

157 
{pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)}, 

158 
{tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) 

159 
in (a:actions(asig_of(ioa1))  a:actions(asig_of(ioa2))) & 

160 
(if a:actions(asig_of(ioa1)) then 

161 
(fst(s),a,fst(t)):trans_of(ioa1) 

162 
else fst(t) = fst(s)) 

163 
& 

164 
(if a:actions(asig_of(ioa2)) then 

165 
(snd(s),a,snd(t)):trans_of(ioa2) 

3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

166 
else snd(t) = snd(s))})" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

167 

984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

168 

17288  169 
restrict_asig_def: 
170 
"restrict_asig asig actns == 

171 
(inputs(asig) Int actns, outputs(asig) Int actns, 

3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

172 
internals(asig) Un (externals(asig)  actns))" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

173 

984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

174 

17288  175 
restrict_def: 
176 
"restrict ioa actns == 

3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

177 
(restrict_asig (asig_of ioa) actns, starts_of(ioa), trans_of(ioa))" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

178 

984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

179 

17288  180 
ioa_implements_def: 
181 
"ioa_implements ioa1 ioa2 == 

182 
((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) & 

183 
(outputs(asig_of(ioa1)) = outputs(asig_of(ioa2))) & 

3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

184 
traces(ioa1) <= traces(ioa2))" 
17288  185 

186 
rename_def: 

187 
"rename ioa ren == 

188 
(({b. ? x. Some(x)= ren(b) & x : inputs(asig_of(ioa))}, 

189 
{b. ? x. Some(x)= ren(b) & x : outputs(asig_of(ioa))}, 

190 
{b. ? x. Some(x)= ren(b) & x : internals(asig_of(ioa))}), 

191 
starts_of(ioa) , 

192 
{tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) 

193 
in 

3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

194 
? x. Some(x) = ren(a) & (s,x,t):trans_of(ioa)})" 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset

195 

19801  196 

197 
declare Let_def [simp] 

198 

199 
lemmas ioa_projections = asig_of_def starts_of_def trans_of_def 

200 
and exec_rws = executions_def is_execution_fragment_def 

201 

202 
lemma ioa_triple_proj: 

203 
"asig_of(x,y,z) = x & starts_of(x,y,z) = y & trans_of(x,y,z) = z" 

204 
apply (simp add: ioa_projections) 

205 
done 

206 

207 
lemma trans_in_actions: 

208 
"[ IOA(A); (s1,a,s2):trans_of(A) ] ==> a:actions(asig_of(A))" 

209 
apply (unfold ioa_def state_trans_def actions_def is_asig_def) 

210 
apply (erule conjE)+ 

211 
apply (erule allE, erule impE, assumption) 

212 
apply simp 

213 
done 

214 

215 

216 
lemma filter_oseq_idemp: "filter_oseq p (filter_oseq p s) = filter_oseq p s" 

217 
apply (simp add: filter_oseq_def) 

218 
apply (rule ext) 

219 
apply (case_tac "s i") 

220 
apply simp_all 

221 
done 

222 

223 
lemma mk_trace_thm: 

224 
"(mk_trace A s n = None) = 

225 
(s(n)=None  (? a. s(n)=Some(a) & a ~: externals(asig_of(A)))) 

226 
& 

227 
(mk_trace A s n = Some(a)) = 

228 
(s(n)=Some(a) & a : externals(asig_of(A)))" 

229 
apply (unfold mk_trace_def filter_oseq_def) 

230 
apply (case_tac "s n") 

231 
apply auto 

232 
done 

233 

234 
lemma reachable_0: "s:starts_of(A) ==> reachable A s" 

235 
apply (unfold reachable_def) 

236 
apply (rule_tac x = "(%i. None, %i. s)" in bexI) 

237 
apply simp 

238 
apply (simp add: exec_rws) 

239 
done 

240 

241 
lemma reachable_n: 

242 
"!!A. [ reachable A s; (s,a,t) : trans_of(A) ] ==> reachable A t" 

243 
apply (unfold reachable_def exec_rws) 

244 
apply (simp del: bex_simps) 

245 
apply (simp (no_asm_simp) only: split_tupled_all) 

246 
apply safe 

247 
apply (rename_tac ex1 ex2 n) 

248 
apply (rule_tac x = "(%i. if i<n then ex1 i else (if i=n then Some a else None) , %i. if i<Suc n then ex2 i else t)" in bexI) 

249 
apply (rule_tac x = "Suc n" in exI) 

250 
apply (simp (no_asm)) 

251 
apply simp 

24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
19801
diff
changeset

252 
apply (metis ioa_triple_proj less_antisym) 
19801  253 
done 
254 

255 

256 
lemma invariantI: 

257 
assumes p1: "!!s. s:starts_of(A) ==> P(s)" 

258 
and p2: "!!s t a. [reachable A s; P(s)] ==> (s,a,t): trans_of(A) > P(t)" 

259 
shows "invariant A P" 

260 
apply (unfold invariant_def reachable_def Let_def exec_rws) 

261 
apply safe 

262 
apply (rename_tac ex1 ex2 n) 

263 
apply (rule_tac Q = "reachable A (ex2 n) " in conjunct1) 

264 
apply simp 

265 
apply (induct_tac n) 

266 
apply (fast intro: p1 reachable_0) 

267 
apply (erule_tac x = na in allE) 

268 
apply (case_tac "ex1 na", simp_all) 

269 
apply safe 

270 
apply (erule p2 [THEN mp]) 

271 
apply (fast dest: reachable_n)+ 

272 
done 

273 

274 
lemma invariantI1: 

275 
"[ !!s. s : starts_of(A) ==> P(s); 

276 
!!s t a. reachable A s ==> P(s) > (s,a,t):trans_of(A) > P(t) 

277 
] ==> invariant A P" 

278 
apply (blast intro!: invariantI) 

279 
done 

280 

281 
lemma invariantE: 

282 
"[ invariant A P; reachable A s ] ==> P(s)" 

283 
apply (unfold invariant_def) 

284 
apply blast 

285 
done 

286 

287 
lemma actions_asig_comp: 

288 
"actions(asig_comp a b) = actions(a) Un actions(b)" 

289 
apply (auto simp add: actions_def asig_comp_def asig_projections) 

290 
done 

291 

292 
lemma starts_of_par: 

293 
"starts_of(A  B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}" 

294 
apply (simp add: par_def ioa_projections) 

295 
done 

296 

297 
(* Every state in an execution is reachable *) 

298 
lemma states_of_exec_reachable: 

299 
"ex:executions(A) ==> !n. reachable A (snd ex n)" 

300 
apply (unfold reachable_def) 

301 
apply fast 

302 
done 

303 

304 

305 
lemma trans_of_par4: 

306 
"(s,a,t) : trans_of(A  B  C  D) = 

307 
((a:actions(asig_of(A))  a:actions(asig_of(B))  a:actions(asig_of(C))  

308 
a:actions(asig_of(D))) & 

309 
(if a:actions(asig_of(A)) then (fst(s),a,fst(t)):trans_of(A) 

310 
else fst t=fst s) & 

311 
(if a:actions(asig_of(B)) then (fst(snd(s)),a,fst(snd(t))):trans_of(B) 

312 
else fst(snd(t))=fst(snd(s))) & 

313 
(if a:actions(asig_of(C)) then 

314 
(fst(snd(snd(s))),a,fst(snd(snd(t)))):trans_of(C) 

315 
else fst(snd(snd(t)))=fst(snd(snd(s)))) & 

316 
(if a:actions(asig_of(D)) then 

317 
(snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D) 

318 
else snd(snd(snd(t)))=snd(snd(snd(s)))))" 

319 
(*SLOW*) 

44066
d74182c93f04
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
huffman
parents:
42174
diff
changeset

320 
apply (simp (no_asm) add: par_def actions_asig_comp prod_eq_iff ioa_projections) 
19801  321 
done 
322 

323 
lemma cancel_restrict: "starts_of(restrict ioa acts) = starts_of(ioa) & 

324 
trans_of(restrict ioa acts) = trans_of(ioa) & 

325 
reachable (restrict ioa acts) s = reachable ioa s" 

326 
apply (simp add: is_execution_fragment_def executions_def 

327 
reachable_def restrict_def ioa_projections) 

328 
done 

329 

330 
lemma asig_of_par: "asig_of(A  B) = asig_comp (asig_of A) (asig_of B)" 

331 
apply (simp add: par_def ioa_projections) 

332 
done 

333 

334 

335 
lemma externals_of_par: "externals(asig_of(A1A2)) = 

336 
(externals(asig_of(A1)) Un externals(asig_of(A2)))" 

337 
apply (simp add: externals_def asig_of_par asig_comp_def 

26806  338 
asig_inputs_def asig_outputs_def Un_def set_diff_eq) 
19801  339 
apply blast 
340 
done 

341 

342 
lemma ext1_is_not_int2: 

343 
"[ compat_ioas A1 A2; a:externals(asig_of(A1))] ==> a~:internals(asig_of(A2))" 

344 
apply (unfold externals_def actions_def compat_ioas_def compat_asigs_def) 

345 
apply auto 

346 
done 

347 

348 
lemma ext2_is_not_int1: 

349 
"[ compat_ioas A2 A1 ; a:externals(asig_of(A1))] ==> a~:internals(asig_of(A2))" 

350 
apply (unfold externals_def actions_def compat_ioas_def compat_asigs_def) 

351 
apply auto 

352 
done 

353 

354 
lemmas ext1_ext2_is_not_act2 = ext1_is_not_int2 [THEN int_and_ext_is_act] 

355 
and ext1_ext2_is_not_act1 = ext2_is_not_int1 [THEN int_and_ext_is_act] 

17288  356 

357 
end 