author  nipkow 
Thu, 07 Jul 2005 12:42:21 +0200  
changeset 16734  2c76db916c51 
parent 15408  6001135caa91 
child 17244  0b2ff9541727 
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/Impl.ML 
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 

12218  5 
The implementation  Invariants. 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

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

7 

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

8 

8741
61bc5ed22b62
removal of less_SucI, le_SucI from default simpset
paulson
parents:
7322
diff
changeset

9 
Addsimps [Let_def, le_SucI]; 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

10 

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 
open Abschannel Impl; 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

13 

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

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

15 
[Impl.impl_def, 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

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

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

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

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

20 

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

21 
val transitions = [Sender.sender_trans_def, Receiver.receiver_trans_def, 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

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

23 

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

24 

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

25 
Addsimps [ioa_triple_proj, starts_of_par, trans_of_par4, 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

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

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

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

29 

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

31 
"fst(x) = sen(x) & \ 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

32 
\ fst(snd(x)) = rec(x) & \ 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

33 
\ fst(snd(snd(x))) = srch(x) & \ 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

34 
\ snd(snd(snd(x))) = rsch(x)"; 
4423  35 
by (simp_tac (simpset() addsimps 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

36 
[sen_def,rec_def,srch_def,rsch_def]) 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

37 
Addsimps [result()]; 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

38 

5068  39 
Goal "a:actions(sender_asig) \ 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

40 
\  a:actions(receiver_asig) \ 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

41 
\  a:actions(srch_asig) \ 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

42 
\  a:actions(rsch_asig)"; 
5192  43 
by (induct_tac "a" 1); 
4423  44 
by (ALLGOALS (Simp_tac)); 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

45 
Addsimps [result()]; 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

46 

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

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

48 

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

49 

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

50 
(* Three Simp_sets in different sizes 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

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

52 

4098  53 
1) simpset() does not unfold the transition relations 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

54 
2) ss unfolds transition relations 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

55 
3) renname_ss unfolds transitions and the abstract channel *) 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

56 

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

57 

6918  58 
val ss = (simpset() addsimps transitions); 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

59 
val rename_ss = (ss addsimps unfold_renaming); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

60 

4833  61 
val tac = asm_simp_tac (ss addcongs [conj_cong] addsplits [split_if]); 
62 
val tac_ren = asm_simp_tac (rename_ss addcongs [conj_cong] addsplits [split_if]); 

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

63 

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

64 

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

65 

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

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

67 

5068  68 
Goalw impl_ioas "invariant impl_ioa inv1"; 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

69 
by (rtac invariantI 1); 
4423  70 
by (asm_full_simp_tac (simpset() 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

71 
addsimps [inv1_def, hdr_sum_def, Sender.srcvd_def, 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

72 
Sender.ssent_def, Receiver.rsent_def,Receiver.rrcvd_def]) 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

73 

4423  74 
by (simp_tac (simpset() delsimps [trans_of_par4] 
15408  75 
addsimps [imp_conjR,inv1_def]) 1); 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

76 

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

77 
(* Split proof in two *) 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

78 
by (rtac conjI 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

79 

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

80 
(* First half *) 
4681  81 
by (asm_full_simp_tac (simpset() addsimps [Impl.inv1_def] 
4833  82 
delsplits [split_if]) 1); 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

83 
by (rtac Action.action.induct 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

84 

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

85 
by (EVERY1[tac, tac, tac, tac]); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

86 
by (tac 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

87 
by (tac_ren 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

88 

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

89 
(* 5 + 1 *) 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

90 

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

91 
by (tac 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

92 
by (tac_ren 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

93 

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

94 
(* 4 + 1 *) 
4423  95 
by (EVERY1[tac, tac, tac, tac]); 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

96 

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

97 

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

98 
(* Now the other half *) 
4681  99 
by (asm_full_simp_tac (simpset() addsimps [Impl.inv1_def] 
4833  100 
delsplits [split_if]) 1); 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

101 
by (rtac Action.action.induct 1); 
4423  102 
by (EVERY1[tac, tac]); 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

103 

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

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

105 
by (tac 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

106 
by (tac_ren 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

107 
by (rtac impI 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

108 
by (REPEAT (etac conjE 1)); 
4098  109 
by (asm_simp_tac (simpset() addsimps [hdr_sum_def, Multiset.count_def, 
4377  110 
Multiset.countm_nonempty_def] 
4833  111 
addsplits [split_if]) 1); 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

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

113 
by (tac 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

114 
by (tac_ren 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

115 
by (rtac impI 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

116 
by (REPEAT (etac conjE 1)); 
4098  117 
by (asm_full_simp_tac (simpset() addsimps [Impl.hdr_sum_def, 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

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

119 
Multiset.countm_nonempty_def, 
4377  120 
Multiset.delm_nonempty_def] 
4833  121 
addsplits [split_if]) 1); 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

122 
by (rtac allI 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

123 
by (rtac conjI 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

124 
by (rtac impI 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

125 
by (hyp_subst_tac 1); 
4377  126 
by (rtac (pred_suc RS iffD1) 1); 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

127 
by (dtac less_le_trans 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

128 
by (cut_facts_tac [rewrite_rule[Packet.hdr_def] 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

129 
eq_packet_imp_eq_hdr RS countm_props] 1);; 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

130 
by (assume_tac 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

131 
by (assume_tac 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

132 

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

133 
by (rtac (countm_done_delm RS mp RS sym) 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

134 
by (rtac refl 1); 
4098  135 
by (asm_simp_tac (simpset() addsimps [Multiset.count_def]) 1); 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

136 

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

137 
by (rtac impI 1); 
4098  138 
by (asm_full_simp_tac (simpset() addsimps [neg_flip]) 1); 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

139 
by (hyp_subst_tac 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

140 
by (rtac countm_spurious_delm 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

141 
by (Simp_tac 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

142 

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

143 
by (EVERY1[tac, tac, tac, tac, tac, tac]); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

144 

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

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

146 

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

147 

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

148 

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

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

150 

5068  151 
Goal "invariant impl_ioa inv2"; 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

152 

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

153 
by (rtac invariantI1 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

154 
(* Base case *) 
4098  155 
by (asm_full_simp_tac (simpset() addsimps (inv2_def :: 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

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

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

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

159 

4833  160 
by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1); 
5192  161 
by (induct_tac "a" 1); 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

162 

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

163 
(* 10 cases. First 4 are simple, since state doesn't change *) 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

164 

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

165 
val tac2 = asm_full_simp_tac (ss addsimps [inv2_def]); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

166 

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

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

168 
by (EVERY1[tac2,tac2,tac2,tac2]); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

169 
(* 6 *) 
4423  170 
by (forward_tac [rewrite_rule [Impl.inv1_def] 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

171 
(inv1 RS invariantE) RS conjunct1] 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

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

173 
by (EVERY1[tac2,tac2]); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

174 

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

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

176 
by (forward_tac [rewrite_rule [Impl.inv1_def] 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

177 
(inv1 RS invariantE) RS conjunct1] 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

178 
by (tac2 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

179 

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

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

181 
by (forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE)] 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

182 

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

183 
by (tac2 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

184 
by (fold_tac [rewrite_rule [Packet.hdr_def]Impl.hdr_sum_def]); 
7322  185 
by (arith_tac 1); 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

186 

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

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

188 
by (tac2 1); 
4423  189 
by (forward_tac [rewrite_rule [Impl.inv1_def] 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

190 
(inv1 RS invariantE) RS conjunct1] 1); 
6081  191 
by (strip_tac 1); 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

192 
by (REPEAT (etac conjE 1)); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

193 
by (Asm_full_simp_tac 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

194 

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

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

196 
by (tac2 1); 
4423  197 
by (forward_tac [rewrite_rule [Impl.inv1_def] 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

198 
(inv1 RS invariantE) RS conjunct2] 1); 
6081  199 
by (strip_tac 1); 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

200 
by (REPEAT (etac conjE 1)); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

201 
by (fold_tac [rewrite_rule[Packet.hdr_def]Impl.hdr_sum_def]); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

202 
by (Asm_full_simp_tac 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

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

204 

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

205 

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

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

207 

5068  208 
Goal "invariant impl_ioa inv3"; 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

209 

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

210 
by (rtac invariantI 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

211 
(* Base case *) 
4098  212 
by (asm_full_simp_tac (simpset() addsimps 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

213 
(Impl.inv3_def :: (receiver_projections 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

214 
@ sender_projections @ impl_ioas))) 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

215 

4833  216 
by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1); 
5192  217 
by (induct_tac "a" 1); 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

218 

6081  219 
val tac3 = asm_full_simp_tac (ss addsimps [inv3_def]); 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

220 

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

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

222 

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

223 
by (EVERY1[tac3,tac3,tac3]); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

224 

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

225 
by (tac_ren 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

226 
by (strip_tac 1 THEN REPEAT (etac conjE 1)); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

227 
by (hyp_subst_tac 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

228 
by (etac exE 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

229 
by (Asm_full_simp_tac 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

230 

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

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

232 
by (tac3 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

233 
by (tac_ren 1); 
9636  234 
by (Force_tac 1); 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

235 

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

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

237 

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

238 
by (EVERY1[tac3,tac3,tac3,tac3]); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

239 

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

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

241 
by (asm_full_simp_tac ss 1); 
4098  242 
by (simp_tac (simpset() addsimps [inv3_def]) 1); 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

243 
by (strip_tac 1 THEN REPEAT (etac conjE 1)); 
15408  244 
by (rtac (imp_disjL RS iffD1) 1); 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

245 
by (rtac impI 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

246 
by (forward_tac [rewrite_rule [Impl.inv2_def] (inv2 RS invariantE)] 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

247 
by (Asm_full_simp_tac 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

248 
by (REPEAT (etac conjE 1)); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

249 
by (res_inst_tac [("j","count (ssent(sen s)) (~sbit(sen s))"), 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

250 
("k","count (rsent(rec s)) (sbit(sen s))")] le_trans 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

251 
by (forward_tac [rewrite_rule [inv1_def] 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

252 
(inv1 RS invariantE) RS conjunct2] 1); 
4098  253 
by (asm_full_simp_tac (simpset() addsimps 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

254 
[hdr_sum_def, Multiset.count_def]) 1); 
4377  255 
by (rtac add_le_mono 1); 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

256 
by (rtac countm_props 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

257 
by (Simp_tac 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

258 
by (rtac countm_props 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

259 
by (Simp_tac 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

260 
by (assume_tac 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

261 

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

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

263 
by (tac3 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

264 
by (strip_tac 1 THEN REPEAT (etac conjE 1)); 
15408  265 
by (rtac (imp_disjL RS iffD1) 1); 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

266 
by (rtac impI 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

267 
by (forward_tac [rewrite_rule [Impl.inv2_def] (inv2 RS invariantE)] 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

268 
by (Asm_full_simp_tac 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

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

270 

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

271 

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

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

273 

5068  274 
Goal "invariant impl_ioa inv4"; 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

275 

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

276 
by (rtac invariantI 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

277 
(* Base case *) 
4098  278 
by (asm_full_simp_tac (simpset() addsimps 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

279 
(Impl.inv4_def :: (receiver_projections 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

280 
@ sender_projections @ impl_ioas))) 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

281 

4833  282 
by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1); 
5192  283 
by (induct_tac "a" 1); 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

284 

6081  285 
val tac4 = asm_full_simp_tac (ss addsimps [inv4_def]); 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

286 

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

287 
(* 10  2 *) 
6081  288 

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

289 
by (EVERY1[tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4]); 
4731  290 

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

291 
(* 2 b *) 
6081  292 

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

293 
by (strip_tac 1 THEN REPEAT (etac conjE 1)); 
4423  294 
by (forward_tac [rewrite_rule [Impl.inv2_def] 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

295 
(inv2 RS invariantE)] 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

296 
by (Asm_full_simp_tac 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

297 

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

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

299 
by (tac4 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

300 
by (strip_tac 1 THEN REPEAT (etac conjE 1)); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

301 
by (rtac ccontr 1); 
4423  302 
by (forward_tac [rewrite_rule [Impl.inv2_def] 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

303 
(inv2 RS invariantE)] 1); 
4423  304 
by (forward_tac [rewrite_rule [Impl.inv3_def] 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

305 
(inv3 RS invariantE)] 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

306 
by (Asm_full_simp_tac 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

307 
by (eres_inst_tac [("x","m")] allE 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

308 
by (Asm_full_simp_tac 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

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

310 

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

311 

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

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

313 

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

314 
val inv1 = rewrite_rule [Impl.inv1_def] (inv1 RS invariantE); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

315 
val inv2 = rewrite_rule [Impl.inv2_def] (inv2 RS invariantE); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

316 
val inv3 = rewrite_rule [Impl.inv3_def] (inv3 RS invariantE); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

317 
val inv4 = rewrite_rule [Impl.inv4_def] (inv4 RS invariantE); 