82 |
82 |
83 text {* shows applicability of the induction hypothesis of the following Lemma 1 *} |
83 text {* shows applicability of the induction hypothesis of the following Lemma 1 *} |
84 lemma last_ind_on_first: |
84 lemma last_ind_on_first: |
85 "l ~= [] ==> hd (reverse (reduce (a # l))) = hd (reverse (reduce l))" |
85 "l ~= [] ==> hd (reverse (reduce (a # l))) = hd (reverse (reduce l))" |
86 apply simp |
86 apply simp |
87 apply (tactic {* auto_tac (map_simpset (fn _ => |
87 apply (tactic {* auto_tac (put_simpset HOL_ss @{context} |
88 HOL_ss |
|
89 addsimps (@{thms reverse.simps} @ [@{thm hd_append}, @{thm rev_red_not_nil}]) |
88 addsimps (@{thms reverse.simps} @ [@{thm hd_append}, @{thm rev_red_not_nil}]) |
90 |> Splitter.add_split @{thm list.split}) @{context}) *}) |
89 |> Splitter.add_split @{thm list.split}) *}) |
91 done |
90 done |
92 |
91 |
93 text {* Main Lemma 1 for @{text "S_pkt"} in showing that reduce is refinement. *} |
92 text {* Main Lemma 1 for @{text "S_pkt"} in showing that reduce is refinement. *} |
94 lemma reduce_hd: |
93 lemma reduce_hd: |
95 "if x=hd(reverse(reduce(l))) & reduce(l)~=[] then |
94 "if x=hd(reverse(reduce(l))) & reduce(l)~=[] then |
164 |
163 |
165 declare split_if [split] |
164 declare split_if [split] |
166 |
165 |
167 lemma sender_abstraction: "is_weak_ref_map reduce srch_ioa srch_fin_ioa" |
166 lemma sender_abstraction: "is_weak_ref_map reduce srch_ioa srch_fin_ioa" |
168 apply (tactic {* |
167 apply (tactic {* |
169 simp_tac (HOL_ss addsimps [@{thm srch_fin_ioa_def}, @{thm rsch_fin_ioa_def}, |
168 simp_tac (put_simpset HOL_ss @{context} |
170 @{thm srch_ioa_def}, @{thm rsch_ioa_def}, @{thm rename_through_pmap}, |
169 addsimps [@{thm srch_fin_ioa_def}, @{thm rsch_fin_ioa_def}, |
171 @{thm channel_abstraction}]) 1 *}) |
170 @{thm srch_ioa_def}, @{thm rsch_ioa_def}, @{thm rename_through_pmap}, |
|
171 @{thm channel_abstraction}]) 1 *}) |
172 done |
172 done |
173 |
173 |
174 lemma receiver_abstraction: "is_weak_ref_map reduce rsch_ioa rsch_fin_ioa" |
174 lemma receiver_abstraction: "is_weak_ref_map reduce rsch_ioa rsch_fin_ioa" |
175 apply (tactic {* |
175 apply (tactic {* |
176 simp_tac (HOL_ss addsimps [@{thm srch_fin_ioa_def}, @{thm rsch_fin_ioa_def}, |
176 simp_tac (put_simpset HOL_ss @{context} |
177 @{thm srch_ioa_def}, @{thm rsch_ioa_def}, @{thm rename_through_pmap}, |
177 addsimps [@{thm srch_fin_ioa_def}, @{thm rsch_fin_ioa_def}, |
178 @{thm channel_abstraction}]) 1 *}) |
178 @{thm srch_ioa_def}, @{thm rsch_ioa_def}, @{thm rename_through_pmap}, |
|
179 @{thm channel_abstraction}]) 1 *}) |
179 done |
180 done |
180 |
181 |
181 |
182 |
182 text {* 3 thms that do not hold generally! The lucky restriction here is |
183 text {* 3 thms that do not hold generally! The lucky restriction here is |
183 the absence of internal actions. *} |
184 the absence of internal actions. *} |