1(* Title: HOL/HOLCF/IOA/ABP/Correctness.thy 2 Author: Olaf M��ller 3*) 4 5section \<open>The main correctness proof: System_fin implements System\<close> 6 7theory Correctness 8imports IOA.IOA Env Impl Impl_finite 9begin 10 11ML_file "Check.ML" 12 13primrec reduce :: "'a list => 'a list" 14where 15 reduce_Nil: "reduce [] = []" 16| reduce_Cons: "reduce(x#xs) = 17 (case xs of 18 [] => [x] 19 | y#ys => (if (x=y) 20 then reduce xs 21 else (x#(reduce xs))))" 22 23definition 24 abs where 25 "abs = 26 (%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))), 27 (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))" 28 29definition 30 system_ioa :: "('m action, bool * 'm impl_state)ioa" where 31 "system_ioa = (env_ioa \<parallel> impl_ioa)" 32 33definition 34 system_fin_ioa :: "('m action, bool * 'm impl_state)ioa" where 35 "system_fin_ioa = (env_ioa \<parallel> impl_fin_ioa)" 36 37 38axiomatization where 39 sys_IOA: "IOA system_ioa" and 40 sys_fin_IOA: "IOA system_fin_ioa" 41 42 43 44declare split_paired_All [simp del] Collect_empty_eq [simp del] 45 46lemmas [simp] = 47 srch_asig_def rsch_asig_def rsch_ioa_def srch_ioa_def ch_ioa_def 48 ch_asig_def srch_actions_def rsch_actions_def rename_def rename_set_def asig_of_def 49 actions_def exis_elim srch_trans_def rsch_trans_def ch_trans_def 50 trans_of_def asig_projections set_lemmas 51 52lemmas abschannel_fin [simp] = 53 srch_fin_asig_def rsch_fin_asig_def 54 rsch_fin_ioa_def srch_fin_ioa_def 55 ch_fin_ioa_def ch_fin_trans_def ch_fin_asig_def 56 57lemmas impl_ioas = sender_ioa_def receiver_ioa_def 58 and impl_trans = sender_trans_def receiver_trans_def 59 and impl_asigs = sender_asig_def receiver_asig_def 60 61declare let_weak_cong [cong] 62declare ioa_triple_proj [simp] starts_of_par [simp] 63 64lemmas env_ioas = env_ioa_def env_asig_def env_trans_def 65lemmas hom_ioas = 66 env_ioas [simp] impl_ioas [simp] impl_trans [simp] impl_asigs [simp] 67 asig_projections set_lemmas 68 69 70subsection \<open>lemmas about reduce\<close> 71 72lemma l_iff_red_nil: "(reduce l = []) = (l = [])" 73 by (induct l) (auto split: list.split) 74 75lemma hd_is_reduce_hd: "s ~= [] --> hd s = hd (reduce s)" 76 by (induct s) (auto split: list.split) 77 78text \<open>to be used in the following Lemma\<close> 79lemma rev_red_not_nil [rule_format]: 80 "l ~= [] --> reverse (reduce l) ~= []" 81 by (induct l) (auto split: list.split) 82 83text \<open>shows applicability of the induction hypothesis of the following Lemma 1\<close> 84lemma last_ind_on_first: 85 "l ~= [] ==> hd (reverse (reduce (a # l))) = hd (reverse (reduce l))" 86 apply simp 87 apply (tactic \<open>auto_tac (put_simpset HOL_ss @{context} 88 addsimps (@{thms reverse.simps} @ [@{thm hd_append}, @{thm rev_red_not_nil}]) 89 |> Splitter.add_split @{thm list.split})\<close>) 90 done 91 92text \<open>Main Lemma 1 for \<open>S_pkt\<close> in showing that reduce is refinement.\<close> 93lemma reduce_hd: 94 "if x=hd(reverse(reduce(l))) & reduce(l)~=[] then 95 reduce(l@[x])=reduce(l) else 96 reduce(l@[x])=reduce(l)@[x]" 97apply (simplesubst if_split) 98apply (rule conjI) 99txt \<open>\<open>-->\<close>\<close> 100apply (induct_tac "l") 101apply (simp (no_asm)) 102apply (case_tac "list=[]") 103 apply simp 104 apply (rule impI) 105apply (simp (no_asm)) 106apply (cut_tac l = "list" in cons_not_nil) 107 apply (simp del: reduce_Cons) 108 apply (erule exE)+ 109 apply hypsubst 110apply (simp del: reduce_Cons add: last_ind_on_first l_iff_red_nil) 111txt \<open>\<open><--\<close>\<close> 112apply (simp (no_asm) add: and_de_morgan_and_absorbe l_iff_red_nil) 113apply (induct_tac "l") 114apply (simp (no_asm)) 115apply (case_tac "list=[]") 116apply (cut_tac [2] l = "list" in cons_not_nil) 117apply simp 118apply (auto simp del: reduce_Cons simp add: last_ind_on_first l_iff_red_nil split: if_split) 119apply simp 120done 121 122 123text \<open>Main Lemma 2 for R_pkt in showing that reduce is refinement.\<close> 124lemma reduce_tl: "s~=[] ==> 125 if hd(s)=hd(tl(s)) & tl(s)~=[] then 126 reduce(tl(s))=reduce(s) else 127 reduce(tl(s))=tl(reduce(s))" 128apply (cut_tac l = "s" in cons_not_nil) 129apply simp 130apply (erule exE)+ 131apply (auto split: list.split) 132done 133 134 135subsection \<open>Channel Abstraction\<close> 136 137declare if_split [split del] 138 139lemma channel_abstraction: "is_weak_ref_map reduce ch_ioa ch_fin_ioa" 140apply (simp (no_asm) add: is_weak_ref_map_def) 141txt \<open>main-part\<close> 142apply (rule allI)+ 143apply (rule imp_conj_lemma) 144apply (induct_tac "a") 145txt \<open>2 cases\<close> 146apply (simp_all (no_asm) cong del: if_weak_cong add: externals_def) 147txt \<open>fst case\<close> 148 apply (rule impI) 149 apply (rule disjI2) 150apply (rule reduce_hd) 151txt \<open>snd case\<close> 152 apply (rule impI) 153 apply (erule conjE)+ 154 apply (erule disjE) 155apply (simp add: l_iff_red_nil) 156apply (erule hd_is_reduce_hd [THEN mp]) 157apply (simp add: l_iff_red_nil) 158apply (rule conjI) 159apply (erule hd_is_reduce_hd [THEN mp]) 160apply (rule bool_if_impl_or [THEN mp]) 161apply (erule reduce_tl) 162done 163 164declare if_split [split] 165 166lemma sender_abstraction: "is_weak_ref_map reduce srch_ioa srch_fin_ioa" 167apply (tactic \<open> 168 simp_tac (put_simpset HOL_ss @{context} 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}, 171 @{thm channel_abstraction}]) 1\<close>) 172done 173 174lemma receiver_abstraction: "is_weak_ref_map reduce rsch_ioa rsch_fin_ioa" 175apply (tactic \<open> 176 simp_tac (put_simpset HOL_ss @{context} 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}, 179 @{thm channel_abstraction}]) 1\<close>) 180done 181 182 183text \<open>3 thms that do not hold generally! The lucky restriction here is 184 the absence of internal actions.\<close> 185lemma sender_unchanged: "is_weak_ref_map (%id. id) sender_ioa sender_ioa" 186apply (simp (no_asm) add: is_weak_ref_map_def) 187txt \<open>main-part\<close> 188apply (rule allI)+ 189apply (induct_tac a) 190txt \<open>7 cases\<close> 191apply (simp_all (no_asm) add: externals_def) 192done 193 194text \<open>2 copies of before\<close> 195lemma receiver_unchanged: "is_weak_ref_map (%id. id) receiver_ioa receiver_ioa" 196apply (simp (no_asm) add: is_weak_ref_map_def) 197txt \<open>main-part\<close> 198apply (rule allI)+ 199apply (induct_tac a) 200txt \<open>7 cases\<close> 201apply (simp_all (no_asm) add: externals_def) 202done 203 204lemma env_unchanged: "is_weak_ref_map (%id. id) env_ioa env_ioa" 205apply (simp (no_asm) add: is_weak_ref_map_def) 206txt \<open>main-part\<close> 207apply (rule allI)+ 208apply (induct_tac a) 209txt \<open>7 cases\<close> 210apply (simp_all (no_asm) add: externals_def) 211done 212 213 214lemma compat_single_ch: "compatible srch_ioa rsch_ioa" 215apply (simp add: compatible_def Int_def) 216apply (rule set_eqI) 217apply (induct_tac x) 218apply simp_all 219done 220 221text \<open>totally the same as before\<close> 222lemma compat_single_fin_ch: "compatible srch_fin_ioa rsch_fin_ioa" 223apply (simp add: compatible_def Int_def) 224apply (rule set_eqI) 225apply (induct_tac x) 226apply simp_all 227done 228 229lemmas del_simps = trans_of_def srch_asig_def rsch_asig_def 230 asig_of_def actions_def srch_trans_def rsch_trans_def srch_ioa_def 231 srch_fin_ioa_def rsch_fin_ioa_def rsch_ioa_def sender_trans_def 232 receiver_trans_def set_lemmas 233 234lemma compat_rec: "compatible receiver_ioa (srch_ioa \<parallel> rsch_ioa)" 235apply (simp del: del_simps 236 add: compatible_def asig_of_par asig_comp_def actions_def Int_def) 237apply simp 238apply (rule set_eqI) 239apply (induct_tac x) 240apply simp_all 241done 242 243text \<open>5 proofs totally the same as before\<close> 244lemma compat_rec_fin: "compatible receiver_ioa (srch_fin_ioa \<parallel> rsch_fin_ioa)" 245apply (simp del: del_simps 246 add: compatible_def asig_of_par asig_comp_def actions_def Int_def) 247apply simp 248apply (rule set_eqI) 249apply (induct_tac x) 250apply simp_all 251done 252 253lemma compat_sen: "compatible sender_ioa 254 (receiver_ioa \<parallel> srch_ioa \<parallel> rsch_ioa)" 255apply (simp del: del_simps 256 add: compatible_def asig_of_par asig_comp_def actions_def Int_def) 257apply simp 258apply (rule set_eqI) 259apply (induct_tac x) 260apply simp_all 261done 262 263lemma compat_sen_fin: "compatible sender_ioa 264 (receiver_ioa \<parallel> srch_fin_ioa \<parallel> rsch_fin_ioa)" 265apply (simp del: del_simps 266 add: compatible_def asig_of_par asig_comp_def actions_def Int_def) 267apply simp 268apply (rule set_eqI) 269apply (induct_tac x) 270apply simp_all 271done 272 273lemma compat_env: "compatible env_ioa 274 (sender_ioa \<parallel> receiver_ioa \<parallel> srch_ioa \<parallel> rsch_ioa)" 275apply (simp del: del_simps 276 add: compatible_def asig_of_par asig_comp_def actions_def Int_def) 277apply simp 278apply (rule set_eqI) 279apply (induct_tac x) 280apply simp_all 281done 282 283lemma compat_env_fin: "compatible env_ioa 284 (sender_ioa \<parallel> receiver_ioa \<parallel> srch_fin_ioa \<parallel> rsch_fin_ioa)" 285apply (simp del: del_simps 286 add: compatible_def asig_of_par asig_comp_def actions_def Int_def) 287apply simp 288apply (rule set_eqI) 289apply (induct_tac x) 290apply simp_all 291done 292 293 294text \<open>lemmata about externals of channels\<close> 295lemma ext_single_ch: "externals(asig_of(srch_fin_ioa)) = externals(asig_of(srch_ioa)) & 296 externals(asig_of(rsch_fin_ioa)) = externals(asig_of(rsch_ioa))" 297 by (simp add: externals_def) 298 299 300subsection \<open>Soundness of Abstraction\<close> 301 302lemmas ext_simps = externals_of_par ext_single_ch 303 and compat_simps = compat_single_ch compat_single_fin_ch compat_rec 304 compat_rec_fin compat_sen compat_sen_fin compat_env compat_env_fin 305 and abstractions = env_unchanged sender_unchanged 306 receiver_unchanged sender_abstraction receiver_abstraction 307 308 309(* FIX: this proof should be done with compositionality on trace level, not on 310 weak_ref_map level, as done here with fxg_is_weak_ref_map_of_product_IOA 311 312Goal "is_weak_ref_map abs system_ioa system_fin_ioa" 313 314by (simp_tac (impl_ss delsimps ([srch_ioa_def, rsch_ioa_def, srch_fin_ioa_def, 315 rsch_fin_ioa_def] @ env_ioas @ impl_ioas) 316 addsimps [system_def, system_fin_def, abs_def, 317 impl_ioa_def, impl_fin_ioa_def, sys_IOA, 318 sys_fin_IOA]) 1); 319 320by (REPEAT (EVERY[rtac fxg_is_weak_ref_map_of_product_IOA 1, 321 simp_tac (ss addsimps abstractions) 1, 322 rtac conjI 1])); 323 324by (ALLGOALS (simp_tac (ss addsimps ext_ss @ compat_ss))); 325 326qed "system_refinement"; 327*) 328 329end 330