author  wenzelm 
Sat, 27 May 2006 21:00:31 +0200  
changeset 19739  c58ef2aa5430 
parent 17244  0b2ff9541727 
child 25131  2c8caac48ade 
permissions  rwrr 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

1 
(* Title: HOL/IOA/NTP/Correctness.thy 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

2 
ID: $Id$ 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

3 
Author: Tobias Nipkow & Konrad Slind 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

4 
*) 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

5 

17244  6 
header {* The main correctness proof: Impl implements Spec *} 
7 

8 
theory Correctness 

9 
imports Impl Spec 

10 
begin 

3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

11 

88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

12 
constdefs 
17244  13 
hom :: "'m impl_state => 'm list" 
14 
"hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s) 

3898  15 
else tl(sq(sen s)))" 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

16 

19739  17 
ML_setup {* 
18 
(* repeated from Traces.ML *) 

19 
change_claset (fn cs => cs delSWrapper "split_all_tac") 

20 
*} 

21 

22 
lemmas hom_ioas = Spec.ioa_def Spec.trans_def sender_trans_def receiver_trans_def impl_ioas 

23 
and impl_asigs = sender_asig_def receiver_asig_def srch_asig_def rsch_asig_def 

24 

25 
declare split_paired_All [simp del] 

26 

27 

28 
text {* 

29 
A lemma about restricting the action signature of the implementation 

30 
to that of the specification. 

31 
*} 

32 

33 
lemma externals_lemma: 

34 
"a:externals(asig_of(Automata.restrict impl_ioa (externals spec_sig))) = 

35 
(case a of 

36 
S_msg(m) => True 

37 
 R_msg(m) => True 

38 
 S_pkt(pkt) => False 

39 
 R_pkt(pkt) => False 

40 
 S_ack(b) => False 

41 
 R_ack(b) => False 

42 
 C_m_s => False 

43 
 C_m_r => False 

44 
 C_r_s => False 

45 
 C_r_r(m) => False)" 

46 
apply (simp (no_asm) add: externals_def restrict_def restrict_asig_def Spec.sig_def asig_projections) 

47 

48 
apply (induct_tac "a") 

49 
apply (simp_all (no_asm) add: actions_def asig_projections) 

50 
txt {* 2 *} 

51 
apply (simp (no_asm) add: impl_ioas) 

52 
apply (simp (no_asm) add: impl_asigs) 

53 
apply (simp (no_asm) add: asig_of_par asig_comp_def asig_projections) 

54 
apply (simp (no_asm) add: "transitions" unfold_renaming) 

55 
txt {* 1 *} 

56 
apply (simp (no_asm) add: impl_ioas) 

57 
apply (simp (no_asm) add: impl_asigs) 

58 
apply (simp (no_asm) add: asig_of_par asig_comp_def asig_projections) 

59 
done 

60 

61 
lemmas sels = sbit_def sq_def ssending_def rbit_def rq_def rsending_def 

62 

63 

64 
text {* Proof of correctness *} 

65 
lemma ntp_correct: 

66 
"is_weak_ref_map hom (Automata.restrict impl_ioa (externals spec_sig)) spec_ioa" 

67 
apply (unfold Spec.ioa_def is_weak_ref_map_def) 

68 
apply (simp (no_asm) cong del: if_weak_cong split del: split_if add: Correctness.hom_def 

69 
cancel_restrict externals_lemma) 

70 
apply (rule conjI) 

71 
apply (simp (no_asm) add: hom_ioas) 

72 
apply (simp (no_asm_simp) add: sels) 

73 
apply (rule allI)+ 

74 
apply (rule imp_conj_lemma) 

75 

76 
apply (induct_tac "a") 

77 
apply (simp_all (no_asm_simp) add: hom_ioas) 

78 
apply (frule inv4) 

79 
apply force 

80 

81 
apply (frule inv4) 

82 
apply (frule inv2) 

83 
apply (erule disjE) 

84 
apply (simp (no_asm_simp)) 

85 
apply force 

86 

87 
apply (frule inv2) 

88 
apply (erule disjE) 

89 

90 
apply (frule inv3) 

91 
apply (case_tac "sq (sen (s))=[]") 

92 

93 
apply (simp add: hom_ioas) 

94 
apply (blast dest!: add_leD1 [THEN leD]) 

95 

96 
apply (case_tac "m = hd (sq (sen (s)))") 

97 

98 
apply force 

99 

100 
apply simp 

101 
apply (blast dest!: add_leD1 [THEN leD]) 

102 

103 
apply simp 

104 
done 

17244  105 

3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

106 
end 