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