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_ss = impl_ss;


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


14 
Sender.sender_trans_def,Receiver.receiver_trans_def]


15 
@ impl_ioas;


16 


17 
val hom_ss' = hom_ss addsimps hom_ioas;


18 


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


20 
Abschannel.srch_asig_def,Abschannel.rsch_asig_def];


21 


22 


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


24 
* to that of the specification.


25 
****************************)


26 
goal Correctness.thy


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


28 
\ (case a of \


29 
\ S_msg(m) => True \


30 
\  R_msg(m) => True \


31 
\  S_pkt(pkt) => False \


32 
\  R_pkt(pkt) => False \


33 
\  S_ack(b) => False \


34 
\  R_ack(b) => False \


35 
\  C_m_s => False \


36 
\  C_m_r => False \


37 
\  C_r_s => False \


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


39 
by(simp_tac (hom_ss addcongs [if_weak_cong]


40 
addsimps ([externals_def, restrict_def, restrict_asig_def,


41 
Spec.sig_def] @ asig_projections)) 1);


42 


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


44 
by(ALLGOALS(simp_tac (action_ss addsimps


45 
(actions_def :: asig_projections @ set_lemmas))));


46 
(* 2 *)


47 
by (simp_tac (hom_ss addsimps impl_ioas) 1);


48 
by (simp_tac (hom_ss addsimps impl_asigs) 1);


49 
by(simp_tac (hom_ss addsimps ([asig_of_par, asig_comp_def]


50 
@ asig_projections)) 1);


51 
by (simp_tac abschannel_ss 1);


52 
(* 1 *)


53 
by (simp_tac (hom_ss addsimps impl_ioas) 1);


54 
by (simp_tac (hom_ss addsimps impl_asigs) 1);


55 
by(simp_tac (hom_ss addsimps ([asig_of_par, asig_comp_def]


56 
@ asig_projections)) 1);


57 
by (simp_tac abschannel_ss 1);


58 
qed "externals_lemma";


59 


60 


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


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


63 


64 
(* Proof of correctness *)


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


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


67 
by(simp_tac (hom_ss addsimps


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


69 
br conjI 1;


70 
by(simp_tac (hom_ss addsimps impl_ioas) 1);


71 
br ballI 1;


72 
bd CollectD 1;


73 
by(asm_simp_tac (hom_ss addsimps sels) 1);


74 
by(REPEAT(rtac allI 1));


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


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


77 
by(asm_simp_tac (hom_ss' setloop (split_tac [expand_if])) 1);


78 
by(forward_tac [inv4] 1);


79 
by(asm_full_simp_tac (hom_ss addsimps


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


81 
by(simp_tac hom_ss' 1);


82 
by(simp_tac hom_ss' 1);


83 
by(simp_tac hom_ss' 1);


84 
by(simp_tac hom_ss' 1);


85 
by(simp_tac hom_ss' 1);


86 
by(simp_tac hom_ss' 1);


87 
by(simp_tac hom_ss' 1);


88 


89 
by(asm_simp_tac hom_ss' 1);


90 
by(forward_tac [inv4] 1);


91 
by(forward_tac [inv2] 1);


92 
be disjE 1;


93 
by(asm_simp_tac hom_ss 1);


94 
by(asm_full_simp_tac (hom_ss addsimps


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


96 


97 
by(asm_simp_tac hom_ss' 1);


98 
by(forward_tac [inv2] 1);


99 
be disjE 1;


100 


101 
by(forward_tac [inv3] 1);


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


103 


104 
by(asm_full_simp_tac hom_ss' 1);


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


106 


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


108 


109 
by(asm_full_simp_tac (hom_ss addsimps


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


111 


112 
by(asm_full_simp_tac hom_ss 1);


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


114 


115 
by(asm_full_simp_tac hom_ss 1);


116 
result();
