1051

1 
(* Title: HOL/IOA/NTP/Correctness.ML


2 
ID: $Id$


3 
Author: Tobias Nipkow & Konrad Slind


4 
Copyright 1994 TU Muenchen


5 


6 
The main correctness proof: Impl implements Spec


7 
*)


8 


9 
open Impl;


10 
open Spec;


11 


12 
val hom_ioas = [Spec.ioa_def, Spec.trans_def,


13 
Sender.sender_trans_def,Receiver.receiver_trans_def]


14 
@ impl_ioas;


15 

1266

16 
Addsimps hom_ioas;

1051

17 


18 
val impl_asigs = [Sender.sender_asig_def,Receiver.receiver_asig_def,


19 
Abschannel.srch_asig_def,Abschannel.rsch_asig_def];


20 

1266

21 
val ss =


22 
!simpset delsimps ([trans_of_def, starts_of_def, srch_asig_def,rsch_asig_def,


23 
asig_of_def, actions_def, srch_trans_def, rsch_trans_def,


24 
impl_def, srch_ioa_thm, rsch_ioa_thm, srch_ioa_def,


25 
rsch_ioa_def, Sender.sender_trans_def,


26 
Receiver.receiver_trans_def] @ set_lemmas);


27 


28 
val ss' = !simpset delsimps [trans_of_def, srch_asig_def, rsch_asig_def,


29 
srch_trans_def, rsch_trans_def, asig_of_def,


30 
actions_def]


31 
addcongs [let_weak_cong];


32 

1051

33 


34 
(* A lemma about restricting the action signature of the implementation


35 
* to that of the specification.


36 
****************************)


37 
goal Correctness.thy


38 
"a:externals(asig_of(restrict impl_ioa (externals spec_sig))) = \


39 
\ (case a of \


40 
\ S_msg(m) => True \


41 
\  R_msg(m) => True \


42 
\  S_pkt(pkt) => False \


43 
\  R_pkt(pkt) => False \


44 
\  S_ack(b) => False \


45 
\  R_ack(b) => False \


46 
\  C_m_s => False \


47 
\  C_m_r => False \


48 
\  C_r_s => False \


49 
\  C_r_r(m) => False)";

1266

50 
by(simp_tac (ss addcongs [if_weak_cong]


51 
addsimps ([externals_def, restrict_def,


52 
restrict_asig_def, Spec.sig_def])) 1);

1051

53 


54 
by(Action.action.induct_tac "a" 1);

1266

55 
by(ALLGOALS(simp_tac (ss addsimps (actions_def :: set_lemmas))));

1051

56 
(* 2 *)

1266

57 
by (simp_tac (ss addsimps impl_ioas) 1);


58 
by (simp_tac (ss addsimps impl_asigs) 1);


59 
by (simp_tac (ss addsimps ([asig_of_par, asig_comp_def])) 1);


60 
by (simp_tac (!simpset delsimps [srch_ioa_thm, rsch_ioa_thm, Let_def]) 1);

1051

61 
(* 1 *)

1266

62 
by (simp_tac (ss addsimps impl_ioas) 1);


63 
by (simp_tac (ss addsimps impl_asigs) 1);


64 
by (simp_tac (ss addsimps ([asig_of_par, asig_comp_def])) 1);


65 
by (simp_tac (!simpset delsimps [srch_ioa_thm, rsch_ioa_thm, Let_def]) 1);

1051

66 
qed "externals_lemma";


67 


68 


69 
val sels = [Sender.sbit_def, Sender.sq_def, Sender.ssending_def,


70 
Receiver.rbit_def, Receiver.rq_def, Receiver.rsending_def];


71 


72 
(* Proof of correctness *)


73 
goalw Correctness.thy [Spec.ioa_def, Solve.is_weak_pmap_def]


74 
"is_weak_pmap hom (restrict impl_ioa (externals spec_sig)) spec_ioa";

1266

75 
by(simp_tac (ss delsimps [trans_def] addsimps

1051

76 
(Correctness.hom_def::[cancel_restrict,externals_lemma])) 1);


77 
br conjI 1;

1266

78 
by(simp_tac (ss addsimps impl_ioas) 1);

1051

79 
br ballI 1;


80 
bd CollectD 1;

1266

81 
by(asm_simp_tac (!simpset addsimps sels) 1);

1051

82 
by(REPEAT(rtac allI 1));


83 
br imp_conj_lemma 1; (* from lemmas.ML *)


84 
by(Action.action.induct_tac "a" 1);

1266

85 
by(asm_simp_tac (ss' setloop (split_tac [expand_if])) 1);

1051

86 
by(forward_tac [inv4] 1);

1266

87 
by(asm_full_simp_tac (ss addsimps [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1);


88 
by(simp_tac ss' 1);


89 
by(simp_tac ss' 1);


90 
by(simp_tac ss' 1);


91 
by(simp_tac ss' 1);


92 
by(simp_tac ss' 1);


93 
by(simp_tac ss' 1);


94 
by(simp_tac ss' 1);

1051

95 

1266

96 
by(asm_simp_tac ss' 1);

1051

97 
by(forward_tac [inv4] 1);


98 
by(forward_tac [inv2] 1);


99 
be disjE 1;

1266

100 
by(asm_simp_tac ss 1);


101 
by(asm_full_simp_tac (ss addsimps [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1);

1051

102 

1266

103 
by(asm_simp_tac ss' 1);

1051

104 
by(forward_tac [inv2] 1);


105 
be disjE 1;


106 


107 
by(forward_tac [inv3] 1);


108 
by(case_tac "sq(sen(s))=[]" 1);


109 

1266

110 
by(asm_full_simp_tac ss' 1);

1051

111 
by(fast_tac (HOL_cs addSDs [add_leD1 RS leD]) 1);


112 


113 
by(case_tac "m = hd(sq(sen(s)))" 1);


114 

1266

115 
by(asm_full_simp_tac (ss addsimps

1051

116 
[imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1);


117 

1266

118 
by(asm_full_simp_tac ss 1);

1051

119 
by(fast_tac (HOL_cs addSDs [add_leD1 RS leD]) 1);


120 

1266

121 
by(asm_full_simp_tac ss 1);

1051

122 
result();
