1(* Title: HOL/HOLCF/IOA/NTP/Correctness.thy 2 Author: Tobias Nipkow & Konrad Slind 3*) 4 5section \<open>The main correctness proof: Impl implements Spec\<close> 6 7theory Correctness 8imports Impl Spec 9begin 10 11definition 12 hom :: "'m impl_state => 'm list" where 13 "hom s = rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s) 14 else tl(sq(sen s)))" 15 16setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close> 17 18lemmas hom_ioas = Spec.ioa_def Spec.trans_def sender_trans_def receiver_trans_def impl_ioas 19 and impl_asigs = sender_asig_def receiver_asig_def srch_asig_def rsch_asig_def 20 21declare split_paired_All [simp del] 22 23 24text \<open> 25 A lemma about restricting the action signature of the implementation 26 to that of the specification. 27\<close> 28 29lemma externals_lemma: 30 "a\<in>externals(asig_of(Automata.restrict impl_ioa (externals spec_sig))) = 31 (case a of 32 S_msg(m) \<Rightarrow> True 33 | R_msg(m) \<Rightarrow> True 34 | S_pkt(pkt) \<Rightarrow> False 35 | R_pkt(pkt) \<Rightarrow> False 36 | S_ack(b) \<Rightarrow> False 37 | R_ack(b) \<Rightarrow> False 38 | C_m_s \<Rightarrow> False 39 | C_m_r \<Rightarrow> False 40 | C_r_s \<Rightarrow> False 41 | C_r_r(m) \<Rightarrow> False)" 42 apply (simp (no_asm) add: externals_def restrict_def restrict_asig_def Spec.sig_def asig_projections) 43 44 apply (induct_tac "a") 45 apply (simp_all (no_asm) add: actions_def asig_projections) 46 txt \<open>2\<close> 47 apply (simp (no_asm) add: impl_ioas) 48 apply (simp (no_asm) add: impl_asigs) 49 apply (simp (no_asm) add: asig_of_par asig_comp_def asig_projections) 50 apply (simp (no_asm) add: "transitions"(1) unfold_renaming) 51 txt \<open>1\<close> 52 apply (simp (no_asm) add: impl_ioas) 53 apply (simp (no_asm) add: impl_asigs) 54 apply (simp (no_asm) add: asig_of_par asig_comp_def asig_projections) 55 done 56 57lemmas sels = sbit_def sq_def ssending_def rbit_def rq_def rsending_def 58 59 60text \<open>Proof of correctness\<close> 61lemma ntp_correct: 62 "is_weak_ref_map hom (Automata.restrict impl_ioa (externals spec_sig)) spec_ioa" 63apply (unfold Spec.ioa_def is_weak_ref_map_def) 64apply (simp (no_asm) cong del: if_weak_cong split del: if_split add: Correctness.hom_def 65 cancel_restrict externals_lemma) 66apply (rule conjI) 67 apply (simp (no_asm) add: hom_ioas) 68 apply (simp (no_asm_simp) add: sels) 69apply (rule allI)+ 70apply (rule imp_conj_lemma) 71 72apply (induct_tac "a") 73apply (simp_all (no_asm_simp) add: hom_ioas) 74apply (frule inv4) 75apply force 76 77apply (frule inv4) 78apply (frule inv2) 79apply (erule disjE) 80apply (simp (no_asm_simp)) 81apply force 82 83apply (frule inv2) 84apply (erule disjE) 85 86apply (frule inv3) 87apply (case_tac "sq (sen (s))=[]") 88 89apply (simp add: hom_ioas) 90apply (blast dest!: add_leD1 [THEN leD]) 91 92apply (rename_tac m, case_tac "m = hd (sq (sen (s)))") 93 94apply force 95 96apply simp 97apply (blast dest!: add_leD1 [THEN leD]) 98 99apply simp 100done 101 102end 103