author | kleing |
Mon, 21 Jun 2004 10:25:57 +0200 | |
changeset 14981 | e73f8140af78 |
parent 14401 | 477380c74c1d |
child 17244 | 0b2ff9541727 |
permissions | -rw-r--r-- |
12218 | 1 |
(* Title: HOLCF/IOA/ABP/Correctness.ML |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
2 |
ID: $Id$ |
12218 | 3 |
Author: Olaf Müller |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
4 |
*) |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
5 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
6 |
|
3842 | 7 |
goal Abschannel.thy "(? x. x=P & Q(x)) = Q(P)"; |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
8 |
by (Fast_tac 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
9 |
qed"exis_elim"; |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
10 |
|
7958 | 11 |
Delsimps [split_paired_All,Collect_empty_eq]; |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
12 |
Addsimps |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
13 |
([srch_asig_def, rsch_asig_def, rsch_ioa_def, srch_ioa_def, ch_ioa_def, |
3522 | 14 |
ch_asig_def, srch_actions_def, rsch_actions_def, rename_def, rename_set_def, asig_of_def, |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
15 |
actions_def, exis_elim, srch_trans_def, rsch_trans_def, ch_trans_def, |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
16 |
trans_of_def] @ asig_projections @ set_lemmas); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
17 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
18 |
val abschannel_fin = [srch_fin_asig_def, rsch_fin_asig_def, |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
19 |
rsch_fin_ioa_def, srch_fin_ioa_def, |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
20 |
ch_fin_ioa_def,ch_fin_trans_def,ch_fin_asig_def]; |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
21 |
Addsimps abschannel_fin; |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
22 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
23 |
val impl_ioas = [Sender.sender_ioa_def,Receiver.receiver_ioa_def]; |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
24 |
val impl_trans = [Sender.sender_trans_def,Receiver.receiver_trans_def]; |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
25 |
val impl_asigs = [Sender.sender_asig_def,Receiver.receiver_asig_def]; |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
26 |
Addcongs [let_weak_cong]; |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
27 |
Addsimps [Let_def, ioa_triple_proj, starts_of_par]; |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
28 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
29 |
val env_ioas = [Env.env_ioa_def,Env.env_asig_def,Env.env_trans_def]; |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
30 |
val hom_ioas = env_ioas @ impl_ioas @ impl_trans @ impl_asigs @ |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
31 |
asig_projections @ set_lemmas; |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
32 |
Addsimps hom_ioas; |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
33 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
34 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
35 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
36 |
(* auxiliary function *) |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
37 |
fun rotate n i = EVERY(replicate n (etac revcut_rl i)); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
38 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
39 |
(* lemmas about reduce *) |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
40 |
|
5068 | 41 |
Goal "(reduce(l)=[]) = (l=[])"; |
6916 | 42 |
by (induct_tac "l" 1); |
14401 | 43 |
by (auto_tac (claset(), simpset() addsplits [thm"list.split"])); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
44 |
val l_iff_red_nil = result(); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
45 |
|
5068 | 46 |
Goal "s~=[] --> hd(s)=hd(reduce(s))"; |
5192 | 47 |
by (induct_tac "s" 1); |
14401 | 48 |
by (auto_tac (claset(), simpset() addsplits [thm"list.split"])); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
49 |
qed"hd_is_reduce_hd"; |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
50 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
51 |
(* to be used in the following Lemma *) |
5068 | 52 |
Goal "l~=[] --> reverse(reduce(l))~=[]"; |
5192 | 53 |
by (induct_tac "l" 1); |
14401 | 54 |
by (auto_tac (claset(), simpset() addsplits [thm"list.split"])); |
6916 | 55 |
qed_spec_mp "rev_red_not_nil"; |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
56 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
57 |
(* shows applicability of the induction hypothesis of the following Lemma 1 *) |
6916 | 58 |
Goal "l~=[] ==> hd(reverse(reduce(a#l))) = hd(reverse(reduce(l)))"; |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
59 |
by (Simp_tac 1); |
14401 | 60 |
by (auto_tac (claset(), HOL_ss addsplits [thm"list.split"] |
6916 | 61 |
addsimps [reverse_Cons,hd_append, |
14401 | 62 |
rev_red_not_nil])); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
63 |
qed"last_ind_on_first"; |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
64 |
|
4098 | 65 |
val impl_ss = simpset() delsimps [reduce_Cons]; |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
66 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
67 |
(* Main Lemma 1 for S_pkt in showing that reduce is refinement *) |
5068 | 68 |
Goal |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
69 |
"if x=hd(reverse(reduce(l))) & reduce(l)~=[] then \ |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
70 |
\ reduce(l@[x])=reduce(l) else \ |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
71 |
\ reduce(l@[x])=reduce(l)@[x]"; |
4833 | 72 |
by (stac split_if 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
73 |
by (rtac conjI 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
74 |
(* --> *) |
5192 | 75 |
by (induct_tac "l" 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
76 |
by (Simp_tac 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
77 |
by (case_tac "list=[]" 1); |
4098 | 78 |
by (asm_full_simp_tac (simpset() addsimps [reverse_Nil,reverse_Cons]) 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
79 |
by (rtac impI 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
80 |
by (Simp_tac 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
81 |
by (cut_inst_tac [("l","list")] cons_not_nil 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
82 |
by (asm_full_simp_tac impl_ss 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
83 |
by (REPEAT (etac exE 1)); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
84 |
by (hyp_subst_tac 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
85 |
by (asm_full_simp_tac (impl_ss addsimps [last_ind_on_first,l_iff_red_nil]) 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
86 |
(* <-- *) |
4098 | 87 |
by (simp_tac (simpset() addsimps [and_de_morgan_and_absorbe,l_iff_red_nil]) 1); |
5192 | 88 |
by (induct_tac "l" 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
89 |
by (Simp_tac 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
90 |
by (case_tac "list=[]" 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
91 |
by (cut_inst_tac [("l","list")] cons_not_nil 2); |
4833 | 92 |
by (Asm_full_simp_tac 1); |
4098 | 93 |
by (auto_tac (claset(), |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
94 |
impl_ss addsimps [last_ind_on_first,l_iff_red_nil] |
4833 | 95 |
setloop split_tac [split_if])); |
96 |
by (Asm_full_simp_tac 1); |
|
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
97 |
qed"reduce_hd"; |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
98 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
99 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
100 |
(* Main Lemma 2 for R_pkt in showing that reduce is refinement *) |
6916 | 101 |
Goal "s~=[] ==> \ |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
102 |
\ if hd(s)=hd(tl(s)) & tl(s)~=[] then \ |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
103 |
\ reduce(tl(s))=reduce(s) else \ |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
104 |
\ reduce(tl(s))=tl(reduce(s))"; |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
105 |
by (cut_inst_tac [("l","s")] cons_not_nil 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
106 |
by (Asm_full_simp_tac 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
107 |
by (REPEAT (etac exE 1)); |
14401 | 108 |
by (auto_tac (claset(), simpset() addsplits [thm"list.split"])); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
109 |
val reduce_tl =result(); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
110 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
111 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
112 |
(******************************************************************* |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
113 |
C h a n n e l A b s t r a c t i o n |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
114 |
*******************************************************************) |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
115 |
|
6916 | 116 |
Delsplits [split_if]; |
117 |
||
118 |
Goal "is_weak_ref_map reduce ch_ioa ch_fin_ioa"; |
|
4098 | 119 |
by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
120 |
(* ---------------- main-part ------------------- *) |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
121 |
by (REPEAT (rtac allI 1)); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
122 |
by (rtac imp_conj_lemma 1); |
5192 | 123 |
by (induct_tac "a" 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
124 |
(* ----------------- 2 cases ---------------------*) |
6916 | 125 |
by (ALLGOALS (simp_tac (simpset() delcongs [if_weak_cong] |
126 |
addsimps [externals_def]))); |
|
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
127 |
(* fst case --------------------------------------*) |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
128 |
by (rtac impI 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
129 |
by (rtac disjI2 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
130 |
by (rtac reduce_hd 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
131 |
(* snd case --------------------------------------*) |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
132 |
by (rtac impI 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
133 |
by (REPEAT (etac conjE 1)); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
134 |
by (etac disjE 1); |
4098 | 135 |
by (asm_full_simp_tac (simpset() addsimps [l_iff_red_nil]) 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
136 |
by (etac (hd_is_reduce_hd RS mp) 1); |
4098 | 137 |
by (asm_full_simp_tac (simpset() addsimps [l_iff_red_nil]) 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
138 |
by (rtac conjI 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
139 |
by (etac (hd_is_reduce_hd RS mp) 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
140 |
by (rtac (bool_if_impl_or RS mp) 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
141 |
by (etac reduce_tl 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
142 |
qed"channel_abstraction"; |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
143 |
|
6916 | 144 |
Addsplits [split_if]; |
145 |
||
146 |
Goal "is_weak_ref_map reduce srch_ioa srch_fin_ioa"; |
|
14401 | 147 |
by (simp_tac (HOL_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def, |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
148 |
srch_ioa_def,rsch_ioa_def,rename_through_pmap,channel_abstraction]) 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
149 |
qed"sender_abstraction"; |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
150 |
|
6916 | 151 |
Goal "is_weak_ref_map reduce rsch_ioa rsch_fin_ioa"; |
14401 | 152 |
by (simp_tac (HOL_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def, |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
153 |
srch_ioa_def,rsch_ioa_def,rename_through_pmap,channel_abstraction]) 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
154 |
qed"receiver_abstraction"; |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
155 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
156 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
157 |
(* 3 thms that do not hold generally! The lucky restriction here is |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
158 |
the absence of internal actions. *) |
6916 | 159 |
Goal "is_weak_ref_map (%id. id) sender_ioa sender_ioa"; |
4098 | 160 |
by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
161 |
(* main-part *) |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
162 |
by (REPEAT (rtac allI 1)); |
5192 | 163 |
by (induct_tac "a" 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
164 |
(* 7 cases *) |
6916 | 165 |
by (ALLGOALS (simp_tac (simpset() addsimps [externals_def]))); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
166 |
qed"sender_unchanged"; |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
167 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
168 |
(* 2 copies of before *) |
6916 | 169 |
Goal "is_weak_ref_map (%id. id) receiver_ioa receiver_ioa"; |
4098 | 170 |
by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
171 |
(* main-part *) |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
172 |
by (REPEAT (rtac allI 1)); |
5192 | 173 |
by (induct_tac "a" 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
174 |
(* 7 cases *) |
6916 | 175 |
by (ALLGOALS(simp_tac (simpset() addsimps [externals_def]))); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
176 |
qed"receiver_unchanged"; |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
177 |
|
6916 | 178 |
Goal "is_weak_ref_map (%id. id) env_ioa env_ioa"; |
4098 | 179 |
by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
180 |
(* main-part *) |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
181 |
by (REPEAT (rtac allI 1)); |
5192 | 182 |
by (induct_tac "a" 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
183 |
(* 7 cases *) |
6916 | 184 |
by (ALLGOALS(simp_tac (simpset() addsimps [externals_def]))); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
185 |
qed"env_unchanged"; |
6916 | 186 |
|
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
187 |
|
5068 | 188 |
Goal "compatible srch_ioa rsch_ioa"; |
13898 | 189 |
by (simp_tac (simpset() addsimps [compatible_def,Int_def]) 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
190 |
by (rtac set_ext 1); |
5192 | 191 |
by (induct_tac "x" 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
192 |
by (ALLGOALS(Simp_tac)); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
193 |
val compat_single_ch = result(); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
194 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
195 |
(* totally the same as before *) |
5068 | 196 |
Goal "compatible srch_fin_ioa rsch_fin_ioa"; |
13898 | 197 |
by (simp_tac (simpset() addsimps [compatible_def,Int_def]) 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
198 |
by (rtac set_ext 1); |
5192 | 199 |
by (induct_tac "x" 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
200 |
by (ALLGOALS(Simp_tac)); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
201 |
val compat_single_fin_ch = result(); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
202 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
203 |
val ss = |
4098 | 204 |
simpset() delsimps ([trans_of_def, srch_asig_def,rsch_asig_def, |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
205 |
asig_of_def, actions_def, srch_trans_def, rsch_trans_def, |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
206 |
srch_ioa_def, srch_fin_ioa_def, rsch_fin_ioa_def, |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
207 |
rsch_ioa_def, Sender.sender_trans_def, |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
208 |
Receiver.receiver_trans_def] @ set_lemmas); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
209 |
|
5068 | 210 |
Goal "compatible receiver_ioa (srch_ioa || rsch_ioa)"; |
13898 | 211 |
by (simp_tac (ss addsimps [compatible_def,asig_of_par,asig_comp_def, |
7958 | 212 |
actions_def,Int_def]) 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
213 |
by (Simp_tac 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
214 |
by (rtac set_ext 1); |
5192 | 215 |
by (induct_tac "x" 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
216 |
by (ALLGOALS Simp_tac); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
217 |
val compat_rec = result(); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
218 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
219 |
(* 5 proofs totally the same as before *) |
5068 | 220 |
Goal "compatible receiver_ioa (srch_fin_ioa || rsch_fin_ioa)"; |
13898 | 221 |
by (simp_tac (ss addsimps [compatible_def,asig_of_par,asig_comp_def, |
7958 | 222 |
actions_def,Int_def]) 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
223 |
by (Simp_tac 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
224 |
by (rtac set_ext 1); |
5192 | 225 |
by (induct_tac "x" 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
226 |
by (ALLGOALS Simp_tac); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
227 |
val compat_rec_fin =result(); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
228 |
|
5068 | 229 |
Goal "compatible sender_ioa \ |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
230 |
\ (receiver_ioa || srch_ioa || rsch_ioa)"; |
13898 | 231 |
by (simp_tac (ss addsimps [compatible_def,asig_of_par,asig_comp_def, |
7958 | 232 |
actions_def,Int_def]) 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
233 |
by (Simp_tac 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
234 |
by (rtac set_ext 1); |
5192 | 235 |
by (induct_tac "x" 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
236 |
by (ALLGOALS(Simp_tac)); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
237 |
val compat_sen=result(); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
238 |
|
5068 | 239 |
Goal "compatible sender_ioa\ |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
240 |
\ (receiver_ioa || srch_fin_ioa || rsch_fin_ioa)"; |
13898 | 241 |
by (simp_tac (ss addsimps [compatible_def,asig_of_par,asig_comp_def, |
7958 | 242 |
actions_def,Int_def]) 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
243 |
by (Simp_tac 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
244 |
by (rtac set_ext 1); |
5192 | 245 |
by (induct_tac "x" 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
246 |
by (ALLGOALS(Simp_tac)); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
247 |
val compat_sen_fin =result(); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
248 |
|
5068 | 249 |
Goal "compatible env_ioa\ |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
250 |
\ (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"; |
13898 | 251 |
by (simp_tac (ss addsimps [compatible_def,asig_of_par,asig_comp_def, |
7958 | 252 |
actions_def,Int_def]) 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
253 |
by (Simp_tac 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
254 |
by (rtac set_ext 1); |
5192 | 255 |
by (induct_tac "x" 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
256 |
by (ALLGOALS(Simp_tac)); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
257 |
val compat_env=result(); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
258 |
|
5068 | 259 |
Goal "compatible env_ioa\ |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
260 |
\ (sender_ioa || receiver_ioa || srch_fin_ioa || rsch_fin_ioa)"; |
13898 | 261 |
by (simp_tac (ss addsimps [compatible_def,asig_of_par,asig_comp_def, |
7958 | 262 |
actions_def,Int_def]) 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
263 |
by (Simp_tac 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
264 |
by (rtac set_ext 1); |
5192 | 265 |
by (induct_tac "x" 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
266 |
by (ALLGOALS Simp_tac); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
267 |
val compat_env_fin=result(); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
268 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
269 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
270 |
(* lemmata about externals of channels *) |
6916 | 271 |
Goal "externals(asig_of(srch_fin_ioa)) = externals(asig_of(srch_ioa)) & \ |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
272 |
\ externals(asig_of(rsch_fin_ioa)) = externals(asig_of(rsch_ioa))"; |
4098 | 273 |
by (simp_tac (simpset() addsimps [externals_def]) 1); |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
274 |
val ext_single_ch = result(); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
275 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
276 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
277 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
278 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
279 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
280 |
val ext_ss = [externals_of_par,ext_single_ch]; |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
281 |
val compat_ss = [compat_single_ch,compat_single_fin_ch,compat_rec, |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
282 |
compat_rec_fin,compat_sen,compat_sen_fin,compat_env,compat_env_fin]; |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
283 |
val abstractions = [env_unchanged,sender_unchanged, |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
284 |
receiver_unchanged,sender_abstraction,receiver_abstraction]; |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
285 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
286 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
287 |
(************************************************************************ |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
288 |
S o u n d n e s s o f A b s t r a c t i o n |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
289 |
*************************************************************************) |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
290 |
|
4098 | 291 |
val ss = simpset() delsimps ([asig_of_def, srch_ioa_def, rsch_ioa_def, |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
292 |
srch_fin_ioa_def, rsch_fin_ioa_def] @ |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
293 |
impl_ioas @ env_ioas); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
294 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
295 |
(* FIX: this proof should be done with compositionality on trace level, not on |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
296 |
weak_ref_map level, as done here with fxg_is_weak_ref_map_of_product_IOA |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
297 |
|
6916 | 298 |
Goal "is_weak_ref_map abs system_ioa system_fin_ioa"; |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
299 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
300 |
by (simp_tac (impl_ss delsimps ([srch_ioa_def, rsch_ioa_def, srch_fin_ioa_def, |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
301 |
rsch_fin_ioa_def] @ env_ioas @ impl_ioas) |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
302 |
addsimps [system_def, system_fin_def, abs_def, |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
303 |
impl_ioa_def, impl_fin_ioa_def, sys_IOA, |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
304 |
sys_fin_IOA]) 1); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
305 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
306 |
by (REPEAT (EVERY[rtac fxg_is_weak_ref_map_of_product_IOA 1, |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
307 |
simp_tac (ss addsimps abstractions) 1, |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
308 |
rtac conjI 1])); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
309 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
310 |
by (ALLGOALS (simp_tac (ss addsimps ext_ss @ compat_ss))); |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
311 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
312 |
qed "system_refinement"; |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
313 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
314 |
|
3983
93ca73409df3
Deleted very odd Delsimps[Collect_False_empty] which made proofs fail!
nipkow
parents:
3842
diff
changeset
|
315 |
*) |