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 

1328

9 


10 
open Impl Spec;

1051

11 


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


13 
Sender.sender_trans_def,Receiver.receiver_trans_def]


14 
@ impl_ioas;


15 


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

1328

17 
Abschannel.srch_asig_def,Abschannel.rsch_asig_def];

1051

18 

1328

19 
(* Two simpsets:  !simpset is basic, ss' unfolds hom_ioas *)

1266

20 

1328

21 
Delsimps [split_paired_All];


22 


23 
val ss' = (!simpset addsimps hom_ioas);

1266

24 

1051

25 


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


27 
* to that of the specification.


28 
****************************)


29 
goal Correctness.thy


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


31 
\ (case a of \


32 
\ S_msg(m) => True \


33 
\  R_msg(m) => True \


34 
\  S_pkt(pkt) => False \


35 
\  R_pkt(pkt) => False \


36 
\  S_ack(b) => False \


37 
\  R_ack(b) => False \


38 
\  C_m_s => False \


39 
\  C_m_r => False \


40 
\  C_r_s => False \


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

1328

42 
by(simp_tac (!simpset addsimps ([externals_def, restrict_def,


43 
restrict_asig_def, Spec.sig_def]


44 
@asig_projections)) 1);

1051

45 


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

1328

47 
by(ALLGOALS(simp_tac (!simpset addsimps [actions_def]@asig_projections)));

1051

48 
(* 2 *)

1328

49 
by (simp_tac (!simpset addsimps impl_ioas) 1);


50 
by (simp_tac (!simpset addsimps impl_asigs) 1);


51 
by (simp_tac (!simpset addsimps


52 
[asig_of_par, asig_comp_def]@asig_projections) 1);


53 
by (simp_tac rename_ss 1);

1051

54 
(* 1 *)

1328

55 
by (simp_tac (!simpset addsimps impl_ioas) 1);


56 
by (simp_tac (!simpset addsimps impl_asigs) 1);


57 
by (simp_tac (!simpset addsimps


58 
[asig_of_par, asig_comp_def]@asig_projections) 1);

1051

59 
qed "externals_lemma";


60 


61 


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


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


64 

1328

65 


66 

1051

67 
(* Proof of correctness *)


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


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

1328

70 
by(simp_tac (!simpset addsimps


71 
[Correctness.hom_def,


72 
cancel_restrict,externals_lemma]) 1);

1051

73 
br conjI 1;

1328

74 
by(simp_tac ss' 1);

1051

75 
br ballI 1;


76 
bd CollectD 1;

1266

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

1051

78 
by(REPEAT(rtac allI 1));


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

1328

80 

1051

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

1266

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

1051

83 
by(forward_tac [inv4] 1);

1328

84 
by(asm_full_simp_tac (!simpset addsimps


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

1266

86 
by(simp_tac ss' 1);


87 
by(simp_tac ss' 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);

1051

93 

1266

94 
by(asm_simp_tac ss' 1);

1051

95 
by(forward_tac [inv4] 1);


96 
by(forward_tac [inv2] 1);


97 
be disjE 1;

1328

98 
by(Asm_simp_tac 1);


99 
by(asm_full_simp_tac (!simpset addsimps [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1);

1051

100 

1266

101 
by(asm_simp_tac ss' 1);

1051

102 
by(forward_tac [inv2] 1);


103 
be disjE 1;


104 


105 
by(forward_tac [inv3] 1);


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


107 

1266

108 
by(asm_full_simp_tac ss' 1);

1051

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


110 


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


112 

1328

113 
by(asm_full_simp_tac (!simpset addsimps

1051

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


115 

1328

116 
by(Asm_full_simp_tac 1);

1051

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


118 

1328

119 
by(Asm_full_simp_tac 1);

1051

120 
result();
