82 |
82 |
83 text \<open>shows applicability of the induction hypothesis of the following Lemma 1\<close> |
83 text \<open>shows applicability of the induction hypothesis of the following Lemma 1\<close> |
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 \<open>auto_tac (put_simpset HOL_ss @{context} |
87 apply (tactic \<open>auto_tac (put_simpset HOL_ss \<^context> |
88 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}]) |
89 |> Splitter.add_split @{thm list.split})\<close>) |
89 |> Splitter.add_split @{thm list.split})\<close>) |
90 done |
90 done |
91 |
91 |
92 text \<open>Main Lemma 1 for \<open>S_pkt\<close> in showing that reduce is refinement.\<close> |
92 text \<open>Main Lemma 1 for \<open>S_pkt\<close> in showing that reduce is refinement.\<close> |
163 |
163 |
164 declare if_split [split] |
164 declare if_split [split] |
165 |
165 |
166 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" |
167 apply (tactic \<open> |
167 apply (tactic \<open> |
168 simp_tac (put_simpset HOL_ss @{context} |
168 simp_tac (put_simpset HOL_ss \<^context> |
169 addsimps [@{thm srch_fin_ioa_def}, @{thm rsch_fin_ioa_def}, |
169 addsimps [@{thm srch_fin_ioa_def}, @{thm rsch_fin_ioa_def}, |
170 @{thm srch_ioa_def}, @{thm rsch_ioa_def}, @{thm rename_through_pmap}, |
170 @{thm srch_ioa_def}, @{thm rsch_ioa_def}, @{thm rename_through_pmap}, |
171 @{thm channel_abstraction}]) 1\<close>) |
171 @{thm channel_abstraction}]) 1\<close>) |
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 \<open> |
175 apply (tactic \<open> |
176 simp_tac (put_simpset HOL_ss @{context} |
176 simp_tac (put_simpset HOL_ss \<^context> |
177 addsimps [@{thm srch_fin_ioa_def}, @{thm rsch_fin_ioa_def}, |
177 addsimps [@{thm srch_fin_ioa_def}, @{thm rsch_fin_ioa_def}, |
178 @{thm srch_ioa_def}, @{thm rsch_ioa_def}, @{thm rename_through_pmap}, |
178 @{thm srch_ioa_def}, @{thm rsch_ioa_def}, @{thm rename_through_pmap}, |
179 @{thm channel_abstraction}]) 1\<close>) |
179 @{thm channel_abstraction}]) 1\<close>) |
180 done |
180 done |
181 |
181 |