author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 39159  0dec18004e75 
child 51717  9e7d1c139569 
permissions  rwrr 
4530  1 
(* Title: HOL/IOA/Solve.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 {* Weak possibilities mapping (abstraction) *} 
7 

8 
theory Solve 

9 
imports IOA 

10 
begin 

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

11 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
26342
diff
changeset

12 
definition is_weak_pmap :: "['c => 'a, ('action,'c)ioa,('action,'a)ioa] => bool" where 
17288  13 
"is_weak_pmap f C A == 
14 
(!s:starts_of(C). f(s):starts_of(A)) & 

15 
(!s t a. reachable C s & 

16 
(s,a,t):trans_of(C) 

17 
> (if a:externals(asig_of(C)) then 

18 
(f(s),a,f(t)):trans_of(A) 

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

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

20 

19801  21 
declare mk_trace_thm [simp] trans_in_actions [simp] 
22 

23 
lemma trace_inclusion: 

24 
"[ IOA(C); IOA(A); externals(asig_of(C)) = externals(asig_of(A)); 

25 
is_weak_pmap f C A ] ==> traces(C) <= traces(A)" 

26 
apply (unfold is_weak_pmap_def traces_def) 

27 

28 
apply (simp (no_asm) add: has_trace_def) 

29 
apply safe 

30 
apply (rename_tac ex1 ex2) 

31 

32 
(* choose same trace, therefore same NF *) 

33 
apply (rule_tac x = "mk_trace C ex1" in exI) 

34 
apply simp 

35 

36 
(* give execution of abstract automata *) 

37 
apply (rule_tac x = "(mk_trace A ex1,%i. f (ex2 i))" in bexI) 

38 

39 
(* Traces coincide *) 

40 
apply (simp (no_asm_simp) add: mk_trace_def filter_oseq_idemp) 

41 

42 
(* Use lemma *) 

43 
apply (frule states_of_exec_reachable) 

44 

45 
(* Now show that it's an execution *) 

46 
apply (simp add: executions_def) 

47 
apply safe 

48 

49 
(* Start states map to start states *) 

50 
apply (drule bspec) 

51 
apply assumption 

52 

53 
(* Show that it's an execution fragment *) 

54 
apply (simp add: is_execution_fragment_def) 

55 
apply safe 

56 

57 
apply (erule_tac x = "ex2 n" in allE) 

58 
apply (erule_tac x = "ex2 (Suc n)" in allE) 

59 
apply (erule_tac x = a in allE) 

60 
apply simp 

61 
done 

62 

63 
(* Lemmata *) 

64 

65 
lemma imp_conj_lemma: "(P ==> Q>R) ==> P&Q > R" 

66 
by blast 

67 

68 

69 
(* fist_order_tautology of externals_of_par *) 

70 
lemma externals_of_par_extra: 

71 
"a:externals(asig_of(A1A2)) = 

72 
(a:externals(asig_of(A1)) & a:externals(asig_of(A2))  

73 
a:externals(asig_of(A1)) & a~:externals(asig_of(A2))  

74 
a~:externals(asig_of(A1)) & a:externals(asig_of(A2)))" 

75 
apply (auto simp add: externals_def asig_of_par asig_comp_def asig_inputs_def asig_outputs_def) 

76 
done 

77 

78 
lemma comp1_reachable: "[ reachable (C1C2) s ] ==> reachable C1 (fst s)" 

79 
apply (simp add: reachable_def) 

80 
apply (erule bexE) 

81 
apply (rule_tac x = 

82 
"(filter_oseq (%a. a:actions (asig_of (C1))) (fst ex) , %i. fst (snd ex i))" in bexI) 

83 
(* fst(s) is in projected execution *) 

84 
apply force 

85 
(* projected execution is indeed an execution *) 

86 
apply (simp cong del: if_weak_cong 

87 
add: executions_def is_execution_fragment_def par_def starts_of_def 

88 
trans_of_def filter_oseq_def 

89 
split add: option.split) 

90 
done 

91 

92 

93 
(* Exact copy of proof of comp1_reachable for the second 

94 
component of a parallel composition. *) 

95 
lemma comp2_reachable: "[ reachable (C1C2) s] ==> reachable C2 (snd s)" 

96 
apply (simp add: reachable_def) 

97 
apply (erule bexE) 

98 
apply (rule_tac x = 

99 
"(filter_oseq (%a. a:actions (asig_of (C2))) (fst ex) , %i. snd (snd ex i))" in bexI) 

100 
(* fst(s) is in projected execution *) 

101 
apply force 

102 
(* projected execution is indeed an execution *) 

103 
apply (simp cong del: if_weak_cong 

104 
add: executions_def is_execution_fragment_def par_def starts_of_def 

105 
trans_of_def filter_oseq_def 

106 
split add: option.split) 

107 
done 

108 

109 
declare split_if [split del] if_weak_cong [cong del] 

110 

111 
(*Composition of possibilitymappings *) 

112 
lemma fxg_is_weak_pmap_of_product_IOA: 

113 
"[ is_weak_pmap f C1 A1; 

114 
externals(asig_of(A1))=externals(asig_of(C1)); 

115 
is_weak_pmap g C2 A2; 

116 
externals(asig_of(A2))=externals(asig_of(C2)); 

117 
compat_ioas C1 C2; compat_ioas A1 A2 ] 

118 
==> is_weak_pmap (%p.(f(fst(p)),g(snd(p)))) (C1C2) (A1A2)" 

119 
apply (unfold is_weak_pmap_def) 

120 
apply (rule conjI) 

121 
(* start_states *) 

122 
apply (simp add: par_def starts_of_def) 

123 
(* transitions *) 

124 
apply (rule allI)+ 

125 
apply (rule imp_conj_lemma) 

126 
apply (simp (no_asm) add: externals_of_par_extra) 

127 
apply (simp (no_asm) add: par_def) 

128 
apply (simp add: trans_of_def) 

129 
apply (simplesubst split_if) 

130 
apply (rule conjI) 

131 
apply (rule impI) 

132 
apply (erule disjE) 

133 
(* case 1 a:e(A1)  a:e(A2) *) 

134 
apply (simp add: comp1_reachable comp2_reachable ext_is_act) 

135 
apply (erule disjE) 

136 
(* case 2 a:e(A1)  a~:e(A2) *) 

137 
apply (simp add: comp1_reachable comp2_reachable ext_is_act ext1_ext2_is_not_act2) 

138 
(* case 3 a:~e(A1)  a:e(A2) *) 

139 
apply (simp add: comp1_reachable comp2_reachable ext_is_act ext1_ext2_is_not_act1) 

140 
(* case 4 a:~e(A1)  a~:e(A2) *) 

141 
apply (rule impI) 

142 
apply (subgoal_tac "a~:externals (asig_of (A1)) & a~:externals (asig_of (A2))") 

143 
(* delete auxiliary subgoal *) 

144 
prefer 2 

145 
apply force 

146 
apply (simp (no_asm) add: conj_disj_distribR cong add: conj_cong split add: split_if) 

147 
apply (tactic {* 

148 
REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN 

39159  149 
asm_full_simp_tac(@{simpset} addsimps [@{thm comp1_reachable}, @{thm comp2_reachable}]) 1) *}) 
19801  150 
done 
151 

152 

153 
lemma reachable_rename_ioa: "[ reachable (rename C g) s ] ==> reachable C s" 

154 
apply (simp add: reachable_def) 

155 
apply (erule bexE) 

156 
apply (rule_tac x = "((%i. case (fst ex i) of None => None  Some (x) => g x) ,snd ex)" in bexI) 

157 
apply (simp (no_asm)) 

158 
(* execution is indeed an execution of C *) 

159 
apply (simp add: executions_def is_execution_fragment_def par_def 

160 
starts_of_def trans_of_def rename_def split add: option.split) 

161 
apply force 

162 
done 

163 

164 

165 
lemma rename_through_pmap: "[ is_weak_pmap f C A ] 

166 
==> (is_weak_pmap f (rename C g) (rename A g))" 

167 
apply (simp add: is_weak_pmap_def) 

168 
apply (rule conjI) 

169 
apply (simp add: rename_def starts_of_def) 

170 
apply (rule allI)+ 

171 
apply (rule imp_conj_lemma) 

172 
apply (simp (no_asm) add: rename_def) 

173 
apply (simp add: externals_def asig_inputs_def asig_outputs_def asig_of_def trans_of_def) 

174 
apply safe 

175 
apply (simplesubst split_if) 

176 
apply (rule conjI) 

177 
apply (rule impI) 

178 
apply (erule disjE) 

179 
apply (erule exE) 

180 
apply (erule conjE) 

181 
(* x is input *) 

182 
apply (drule sym) 

183 
apply (drule sym) 

184 
apply simp 

185 
apply hypsubst+ 

186 
apply (cut_tac C = "C" and g = "g" and s = "s" in reachable_rename_ioa) 

187 
apply assumption 

188 
apply simp 

189 
(* x is output *) 

190 
apply (erule exE) 

191 
apply (erule conjE) 

192 
apply (drule sym) 

193 
apply (drule sym) 

194 
apply simp 

195 
apply hypsubst+ 

196 
apply (cut_tac C = "C" and g = "g" and s = "s" in reachable_rename_ioa) 

197 
apply assumption 

198 
apply simp 

199 
(* x is internal *) 

200 
apply (simp (no_asm) add: de_Morgan_disj de_Morgan_conj not_ex cong add: conj_cong) 

201 
apply (rule impI) 

202 
apply (erule conjE) 

203 
apply (cut_tac C = "C" and g = "g" and s = "s" in reachable_rename_ioa) 

204 
apply auto 

205 
done 

206 

207 
declare split_if [split] if_weak_cong [cong] 

17288  208 

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

209 
end 