26 by (Asm_full_simp_tac 1); |
26 by (Asm_full_simp_tac 1); |
27 qed "trans_in_actions"; |
27 qed "trans_in_actions"; |
28 |
28 |
29 |
29 |
30 goal IOA.thy "filter_oseq p (filter_oseq p s) = filter_oseq p s"; |
30 goal IOA.thy "filter_oseq p (filter_oseq p s) = filter_oseq p s"; |
31 by (simp_tac (!simpset addsimps [filter_oseq_def]) 1); |
31 by (simp_tac (simpset() addsimps [filter_oseq_def]) 1); |
32 by (rtac ext 1); |
32 by (rtac ext 1); |
33 by (exhaust_tac "s(i)" 1); |
33 by (exhaust_tac "s(i)" 1); |
34 by (Asm_simp_tac 1); |
34 by (Asm_simp_tac 1); |
35 by (asm_simp_tac (!simpset addsplits [expand_if]) 1); |
35 by (asm_simp_tac (simpset() addsplits [expand_if]) 1); |
36 qed "filter_oseq_idemp"; |
36 qed "filter_oseq_idemp"; |
37 |
37 |
38 goalw IOA.thy [mk_trace_def,filter_oseq_def] |
38 goalw IOA.thy [mk_trace_def,filter_oseq_def] |
39 "(mk_trace A s n = None) = \ |
39 "(mk_trace A s n = None) = \ |
40 \ (s(n)=None | (? a. s(n)=Some(a) & a ~: externals(asig_of(A)))) \ |
40 \ (s(n)=None | (? a. s(n)=Some(a) & a ~: externals(asig_of(A)))) \ |
41 \ & \ |
41 \ & \ |
42 \ (mk_trace A s n = Some(a)) = \ |
42 \ (mk_trace A s n = Some(a)) = \ |
43 \ (s(n)=Some(a) & a : externals(asig_of(A)))"; |
43 \ (s(n)=Some(a) & a : externals(asig_of(A)))"; |
44 by (exhaust_tac "s(n)" 1); |
44 by (exhaust_tac "s(n)" 1); |
45 by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if]))); |
45 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if]))); |
46 by (Fast_tac 1); |
46 by (Fast_tac 1); |
47 qed "mk_trace_thm"; |
47 qed "mk_trace_thm"; |
48 |
48 |
49 goalw IOA.thy [reachable_def] "!!A. s:starts_of(A) ==> reachable A s"; |
49 goalw IOA.thy [reachable_def] "!!A. s:starts_of(A) ==> reachable A s"; |
50 by (res_inst_tac [("x","(%i. None,%i. s)")] bexI 1); |
50 by (res_inst_tac [("x","(%i. None,%i. s)")] bexI 1); |
51 by (Simp_tac 1); |
51 by (Simp_tac 1); |
52 by (asm_simp_tac (!simpset addsimps exec_rws) 1); |
52 by (asm_simp_tac (simpset() addsimps exec_rws) 1); |
53 qed "reachable_0"; |
53 qed "reachable_0"; |
54 |
54 |
55 goalw IOA.thy (reachable_def::exec_rws) |
55 goalw IOA.thy (reachable_def::exec_rws) |
56 "!!A. [| reachable A s; (s,a,t) : trans_of(A) |] ==> reachable A t"; |
56 "!!A. [| reachable A s; (s,a,t) : trans_of(A) |] ==> reachable A t"; |
57 by (asm_full_simp_tac (!simpset delsimps bex_simps) 1); |
57 by (asm_full_simp_tac (simpset() delsimps bex_simps) 1); |
58 by (safe_tac (!claset)); |
58 by (safe_tac (claset())); |
59 by (res_inst_tac [("x","(%i. if i<n then fst ex i \ |
59 by (res_inst_tac [("x","(%i. if i<n then fst ex i \ |
60 \ else (if i=n then Some a else None), \ |
60 \ else (if i=n then Some a else None), \ |
61 \ %i. if i<Suc n then snd ex i else t)")] bexI 1); |
61 \ %i. if i<Suc n then snd ex i else t)")] bexI 1); |
62 by (res_inst_tac [("x","Suc(n)")] exI 1); |
62 by (res_inst_tac [("x","Suc(n)")] exI 1); |
63 by (Simp_tac 1); |
63 by (Simp_tac 1); |
64 by (Asm_simp_tac 1); |
64 by (Asm_simp_tac 1); |
65 by (REPEAT(rtac allI 1)); |
65 by (REPEAT(rtac allI 1)); |
66 by (res_inst_tac [("m","na"),("n","n")] (make_elim less_linear) 1); |
66 by (res_inst_tac [("m","na"),("n","n")] (make_elim less_linear) 1); |
67 by (etac disjE 1); |
67 by (etac disjE 1); |
68 by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1); |
68 by (asm_simp_tac (simpset() addsimps [less_Suc_eq]) 1); |
69 by (etac disjE 1); |
69 by (etac disjE 1); |
70 by (Asm_simp_tac 1); |
70 by (Asm_simp_tac 1); |
71 by (forward_tac [less_not_sym] 1); |
71 by (forward_tac [less_not_sym] 1); |
72 by (asm_simp_tac (!simpset addsimps [less_not_refl2,less_Suc_eq]) 1); |
72 by (asm_simp_tac (simpset() addsimps [less_not_refl2,less_Suc_eq]) 1); |
73 qed "reachable_n"; |
73 qed "reachable_n"; |
74 |
74 |
75 val [p1,p2] = goalw IOA.thy [invariant_def] |
75 val [p1,p2] = goalw IOA.thy [invariant_def] |
76 "[| !!s. s:starts_of(A) ==> P(s); \ |
76 "[| !!s. s:starts_of(A) ==> P(s); \ |
77 \ !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] \ |
77 \ !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] \ |
78 \ ==> invariant A P"; |
78 \ ==> invariant A P"; |
79 by (rewrite_goals_tac(reachable_def::Let_def::exec_rws)); |
79 by (rewrite_goals_tac(reachable_def::Let_def::exec_rws)); |
80 by (safe_tac (!claset)); |
80 by (safe_tac (claset())); |
81 by (res_inst_tac [("Q","reachable A (snd ex n)")] conjunct1 1); |
81 by (res_inst_tac [("Q","reachable A (snd ex n)")] conjunct1 1); |
82 by (nat_ind_tac "n" 1); |
82 by (nat_ind_tac "n" 1); |
83 by (fast_tac (!claset addIs [p1,reachable_0]) 1); |
83 by (fast_tac (claset() addIs [p1,reachable_0]) 1); |
84 by (eres_inst_tac[("x","n")]allE 1); |
84 by (eres_inst_tac[("x","n")]allE 1); |
85 by (exhaust_tac "fst ex n" 1 THEN ALLGOALS Asm_full_simp_tac); |
85 by (exhaust_tac "fst ex n" 1 THEN ALLGOALS Asm_full_simp_tac); |
86 by (safe_tac (!claset)); |
86 by (safe_tac (claset())); |
87 by (etac (p2 RS mp) 1); |
87 by (etac (p2 RS mp) 1); |
88 by (ALLGOALS(fast_tac(!claset addDs [reachable_n]))); |
88 by (ALLGOALS(fast_tac(claset() addDs [reachable_n]))); |
89 qed "invariantI"; |
89 qed "invariantI"; |
90 |
90 |
91 val [p1,p2] = goal IOA.thy |
91 val [p1,p2] = goal IOA.thy |
92 "[| !!s. s : starts_of(A) ==> P(s); \ |
92 "[| !!s. s : starts_of(A) ==> P(s); \ |
93 \ !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t) \ |
93 \ !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t) \ |
94 \ |] ==> invariant A P"; |
94 \ |] ==> invariant A P"; |
95 by (fast_tac (!claset addSIs [invariantI] addSDs [p1,p2]) 1); |
95 by (fast_tac (claset() addSIs [invariantI] addSDs [p1,p2]) 1); |
96 qed "invariantI1"; |
96 qed "invariantI1"; |
97 |
97 |
98 val [p1,p2] = goalw IOA.thy [invariant_def] |
98 val [p1,p2] = goalw IOA.thy [invariant_def] |
99 "[| invariant A P; reachable A s |] ==> P(s)"; |
99 "[| invariant A P; reachable A s |] ==> P(s)"; |
100 by (rtac (p2 RS (p1 RS spec RS mp)) 1); |
100 by (rtac (p2 RS (p1 RS spec RS mp)) 1); |
101 qed "invariantE"; |
101 qed "invariantE"; |
102 |
102 |
103 goal IOA.thy |
103 goal IOA.thy |
104 "actions(asig_comp a b) = actions(a) Un actions(b)"; |
104 "actions(asig_comp a b) = actions(a) Un actions(b)"; |
105 by (simp_tac (!simpset addsimps |
105 by (simp_tac (simpset() addsimps |
106 ([actions_def,asig_comp_def]@asig_projections)) 1); |
106 ([actions_def,asig_comp_def]@asig_projections)) 1); |
107 by (Fast_tac 1); |
107 by (Fast_tac 1); |
108 qed "actions_asig_comp"; |
108 qed "actions_asig_comp"; |
109 |
109 |
110 goal IOA.thy |
110 goal IOA.thy |
111 "starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}"; |
111 "starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}"; |
112 by (simp_tac (!simpset addsimps (par_def::ioa_projections)) 1); |
112 by (simp_tac (simpset() addsimps (par_def::ioa_projections)) 1); |
113 qed "starts_of_par"; |
113 qed "starts_of_par"; |
114 |
114 |
115 (* Every state in an execution is reachable *) |
115 (* Every state in an execution is reachable *) |
116 goalw IOA.thy [reachable_def] |
116 goalw IOA.thy [reachable_def] |
117 "!!A. ex:executions(A) ==> !n. reachable A (snd ex n)"; |
117 "!!A. ex:executions(A) ==> !n. reachable A (snd ex n)"; |
131 \ (fst(snd(snd(s))),a,fst(snd(snd(t)))):trans_of(C) \ |
131 \ (fst(snd(snd(s))),a,fst(snd(snd(t)))):trans_of(C) \ |
132 \ else fst(snd(snd(t)))=fst(snd(snd(s)))) & \ |
132 \ else fst(snd(snd(t)))=fst(snd(snd(s)))) & \ |
133 \ (if a:actions(asig_of(D)) then \ |
133 \ (if a:actions(asig_of(D)) then \ |
134 \ (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D) \ |
134 \ (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D) \ |
135 \ else snd(snd(snd(t)))=snd(snd(snd(s)))))"; |
135 \ else snd(snd(snd(t)))=snd(snd(snd(s)))))"; |
136 by (simp_tac (!simpset addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq]@ |
136 by (simp_tac (simpset() addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq]@ |
137 ioa_projections) |
137 ioa_projections) |
138 addsplits [expand_if]) 1); |
138 addsplits [expand_if]) 1); |
139 qed "trans_of_par4"; |
139 qed "trans_of_par4"; |
140 |
140 |
141 goal IOA.thy "starts_of(restrict ioa acts) = starts_of(ioa) & \ |
141 goal IOA.thy "starts_of(restrict ioa acts) = starts_of(ioa) & \ |
142 \ trans_of(restrict ioa acts) = trans_of(ioa) & \ |
142 \ trans_of(restrict ioa acts) = trans_of(ioa) & \ |
143 \ reachable (restrict ioa acts) s = reachable ioa s"; |
143 \ reachable (restrict ioa acts) s = reachable ioa s"; |
144 by (simp_tac (!simpset addsimps ([is_execution_fragment_def,executions_def, |
144 by (simp_tac (simpset() addsimps ([is_execution_fragment_def,executions_def, |
145 reachable_def,restrict_def]@ioa_projections)) 1); |
145 reachable_def,restrict_def]@ioa_projections)) 1); |
146 qed "cancel_restrict"; |
146 qed "cancel_restrict"; |
147 |
147 |
148 goal IOA.thy "asig_of(A || B) = asig_comp (asig_of A) (asig_of B)"; |
148 goal IOA.thy "asig_of(A || B) = asig_comp (asig_of A) (asig_of B)"; |
149 by (simp_tac (!simpset addsimps (par_def::ioa_projections)) 1); |
149 by (simp_tac (simpset() addsimps (par_def::ioa_projections)) 1); |
150 qed "asig_of_par"; |
150 qed "asig_of_par"; |
151 |
151 |
152 |
152 |
153 goal IOA.thy "externals(asig_of(A1||A2)) = \ |
153 goal IOA.thy "externals(asig_of(A1||A2)) = \ |
154 \ (externals(asig_of(A1)) Un externals(asig_of(A2)))"; |
154 \ (externals(asig_of(A1)) Un externals(asig_of(A2)))"; |
155 by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_of_par,asig_comp_def,asig_inputs_def,asig_outputs_def,Un_def,set_diff_def]) 1); |
155 by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_of_par,asig_comp_def,asig_inputs_def,asig_outputs_def,Un_def,set_diff_def]) 1); |
156 by (rtac set_ext 1); |
156 by (rtac set_ext 1); |
157 by (Fast_tac 1); |
157 by (Fast_tac 1); |
158 qed"externals_of_par"; |
158 qed"externals_of_par"; |
159 |
159 |
160 goalw IOA.thy [externals_def,actions_def,compat_ioas_def,compat_asigs_def] |
160 goalw IOA.thy [externals_def,actions_def,compat_ioas_def,compat_asigs_def] |
161 "!! a. [| compat_ioas A1 A2; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))"; |
161 "!! a. [| compat_ioas A1 A2; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))"; |
162 by (Asm_full_simp_tac 1); |
162 by (Asm_full_simp_tac 1); |
163 by (best_tac (!claset addEs [equalityCE]) 1); |
163 by (best_tac (claset() addEs [equalityCE]) 1); |
164 qed"ext1_is_not_int2"; |
164 qed"ext1_is_not_int2"; |
165 |
165 |
166 goalw IOA.thy [externals_def,actions_def,compat_ioas_def,compat_asigs_def] |
166 goalw IOA.thy [externals_def,actions_def,compat_ioas_def,compat_asigs_def] |
167 "!! a. [| compat_ioas A2 A1 ; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))"; |
167 "!! a. [| compat_ioas A2 A1 ; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))"; |
168 by (Asm_full_simp_tac 1); |
168 by (Asm_full_simp_tac 1); |
169 by (best_tac (!claset addEs [equalityCE]) 1); |
169 by (best_tac (claset() addEs [equalityCE]) 1); |
170 qed"ext2_is_not_int1"; |
170 qed"ext2_is_not_int1"; |
171 |
171 |
172 val ext1_ext2_is_not_act2 = ext1_is_not_int2 RS int_and_ext_is_act; |
172 val ext1_ext2_is_not_act2 = ext1_is_not_int2 RS int_and_ext_is_act; |
173 val ext1_ext2_is_not_act1 = ext2_is_not_int1 RS int_and_ext_is_act; |
173 val ext1_ext2_is_not_act1 = ext2_is_not_int1 RS int_and_ext_is_act; |
174 |
174 |