--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/NTP/Abschannel.ML Wed Apr 30 11:25:31 1997 +0200
@@ -0,0 +1,53 @@
+(* Title: HOL/IOA/NTP/Abschannel.ML
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1994 TU Muenchen
+
+Derived rules
+*)
+
+open Abschannel;
+
+val unfold_renaming =
+ [srch_asig_def, rsch_asig_def, rsch_ioa_def, srch_ioa_def, ch_ioa_def,
+ ch_asig_def, srch_actions_def, rsch_actions_def, rename_def, asig_of_def,
+ actions_def, srch_trans_def, rsch_trans_def, ch_trans_def,starts_of_def,
+ trans_of_def] @ asig_projections;
+
+goal Abschannel.thy
+ "S_msg(m) ~: actions(srch_asig) & \
+ \ R_msg(m) ~: actions(srch_asig) & \
+ \ S_pkt(pkt) : actions(srch_asig) & \
+ \ R_pkt(pkt) : actions(srch_asig) & \
+ \ S_ack(b) ~: actions(srch_asig) & \
+ \ R_ack(b) ~: actions(srch_asig) & \
+ \ C_m_s ~: actions(srch_asig) & \
+ \ C_m_r ~: actions(srch_asig) & \
+ \ C_r_s ~: actions(srch_asig) & C_r_r(m) ~: actions(srch_asig)";
+
+by(simp_tac (!simpset addsimps unfold_renaming) 1);
+qed"in_srch_asig";
+
+goal Abschannel.thy
+ "S_msg(m) ~: actions(rsch_asig) & \
+ \ R_msg(m) ~: actions(rsch_asig) & \
+ \ S_pkt(pkt) ~: actions(rsch_asig) & \
+ \ R_pkt(pkt) ~: actions(rsch_asig) & \
+ \ S_ack(b) : actions(rsch_asig) & \
+ \ R_ack(b) : actions(rsch_asig) & \
+ \ C_m_s ~: actions(rsch_asig) & \
+ \ C_m_r ~: actions(rsch_asig) & \
+ \ C_r_s ~: actions(rsch_asig) & \
+ \ C_r_r(m) ~: actions(rsch_asig)";
+
+by(simp_tac (!simpset addsimps unfold_renaming) 1);
+qed"in_rsch_asig";
+
+goal Abschannel.thy "srch_ioa = (srch_asig, {{|}}, srch_trans)";
+by(simp_tac (!simpset addsimps unfold_renaming) 1);
+qed"srch_ioa_thm";
+
+goal Abschannel.thy "rsch_ioa = (rsch_asig, {{|}}, rsch_trans)";
+by(simp_tac (!simpset addsimps unfold_renaming) 1);
+qed"rsch_ioa_thm";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/NTP/Abschannel.thy Wed Apr 30 11:25:31 1997 +0200
@@ -0,0 +1,103 @@
+(* Title: HOL/IOA/NTP/Abschannel.thy
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1994 TU Muenchen
+
+The (faulty) transmission channel (both directions)
+*)
+
+Abschannel = IOA + Action +
+
+datatype ('a)abs_action = S('a) | R('a)
+
+consts
+
+ch_asig :: 'a abs_action signature
+
+ch_trans :: ('a abs_action, 'a multiset)transition set
+
+ch_ioa :: ('a abs_action, 'a multiset)ioa
+
+rsch_actions :: 'm action => bool abs_action option
+srch_actions :: "'m action =>(bool * 'm) abs_action option"
+
+srch_asig,
+rsch_asig :: 'm action signature
+
+srch_trans :: ('m action, 'm packet multiset)transition set
+rsch_trans :: ('m action, bool multiset)transition set
+
+srch_ioa :: ('m action, 'm packet multiset)ioa
+rsch_ioa :: ('m action, bool multiset)ioa
+
+
+defs
+
+srch_asig_def "srch_asig == asig_of(srch_ioa)"
+rsch_asig_def "rsch_asig == asig_of(rsch_ioa)"
+
+srch_trans_def "srch_trans == trans_of(srch_ioa)"
+rsch_trans_def "rsch_trans == trans_of(rsch_ioa)"
+
+srch_ioa_def "srch_ioa == rename ch_ioa srch_actions"
+rsch_ioa_def "rsch_ioa == rename ch_ioa rsch_actions"
+
+
+ch_asig_def "ch_asig == (UN b. {S(b)}, UN b. {R(b)}, {})"
+
+ch_trans_def "ch_trans ==
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in
+ case fst(snd(tr))
+ of S(b) => t = addm s b |
+ R(b) => count s b ~= 0 & t = delm s b}"
+
+ch_ioa_def "ch_ioa == (ch_asig, {{|}}, ch_trans)"
+
+
+rsch_actions_def "rsch_actions (akt) ==
+ case akt of
+ S_msg(m) => None |
+ R_msg(m) => None |
+ S_pkt(packet) => None |
+ R_pkt(packet) => None |
+ S_ack(b) => Some(S(b)) |
+ R_ack(b) => Some(R(b)) |
+ C_m_s => None |
+ C_m_r => None |
+ C_r_s => None |
+ C_r_r(m) => None"
+
+srch_actions_def "srch_actions (akt) ==
+ case akt of
+ S_msg(m) => None |
+ R_msg(m) => None |
+ S_pkt(p) => Some(S(p)) |
+ R_pkt(p) => Some(R(p)) |
+ S_ack(b) => None |
+ R_ack(b) => None |
+ C_m_s => None |
+ C_m_r => None |
+ C_r_s => None |
+ C_r_r(m) => None"
+
+end
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/NTP/Action.ML Wed Apr 30 11:25:31 1997 +0200
@@ -0,0 +1,13 @@
+(* Title: HOL/IOA/NTP/Action.ML
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+Derived rules for actions
+*)
+
+goal Action.thy "!!x. x = y ==> action_case a b c d e f g h i j x = \
+\ action_case a b c d e f g h i j y";
+by (Asm_simp_tac 1);
+
+Addcongs [result()];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/NTP/Action.thy Wed Apr 30 11:25:31 1997 +0200
@@ -0,0 +1,14 @@
+(* Title: HOL/IOA/NTP/Action.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+The set of all actions of the system
+*)
+
+Action = Packet +
+datatype 'm action = S_msg ('m) | R_msg ('m)
+ | S_pkt ('m packet) | R_pkt ('m packet)
+ | S_ack (bool) | R_ack (bool)
+ | C_m_s | C_m_r | C_r_s | C_r_r ('m)
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/NTP/Correctness.ML Wed Apr 30 11:25:31 1997 +0200
@@ -0,0 +1,114 @@
+(* Title: HOL/IOA/NTP/Correctness.ML
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+The main correctness proof: Impl implements Spec
+*)
+
+
+
+val hom_ioas = [Spec.ioa_def, Spec.trans_def,
+ Sender.sender_trans_def,Receiver.receiver_trans_def]
+ @ impl_ioas;
+
+val impl_asigs = [Sender.sender_asig_def,Receiver.receiver_asig_def,
+ Abschannel.srch_asig_def,Abschannel.rsch_asig_def];
+
+(* Two simpsets: - !simpset is basic, ss' unfolds hom_ioas *)
+
+Delsimps [split_paired_All];
+
+val ss' = (!simpset addsimps hom_ioas);
+
+
+(* A lemma about restricting the action signature of the implementation
+ * to that of the specification.
+ ****************************)
+goal Correctness.thy
+ "a:externals(asig_of(restrict impl_ioa (externals spec_sig))) = \
+\ (case a of \
+\ S_msg(m) => True \
+\ | R_msg(m) => True \
+\ | S_pkt(pkt) => False \
+\ | R_pkt(pkt) => False \
+\ | S_ack(b) => False \
+\ | R_ack(b) => False \
+\ | C_m_s => False \
+\ | C_m_r => False \
+\ | C_r_s => False \
+\ | C_r_r(m) => False)";
+ by (simp_tac (!simpset addsimps ([externals_def, restrict_def,
+ restrict_asig_def, Spec.sig_def]
+ @asig_projections)) 1);
+
+ by (Action.action.induct_tac "a" 1);
+ by (ALLGOALS(simp_tac (!simpset addsimps [actions_def]@asig_projections)));
+ (* 2 *)
+ by (simp_tac (!simpset addsimps impl_ioas) 1);
+ by (simp_tac (!simpset addsimps impl_asigs) 1);
+ by (simp_tac (!simpset addsimps
+ [asig_of_par, asig_comp_def]@asig_projections) 1);
+ by (simp_tac rename_ss 1);
+ (* 1 *)
+ by (simp_tac (!simpset addsimps impl_ioas) 1);
+ by (simp_tac (!simpset addsimps impl_asigs) 1);
+ by (simp_tac (!simpset addsimps
+ [asig_of_par, asig_comp_def]@asig_projections) 1);
+qed "externals_lemma";
+
+
+val sels = [Sender.sbit_def, Sender.sq_def, Sender.ssending_def,
+ Receiver.rbit_def, Receiver.rq_def, Receiver.rsending_def];
+
+
+
+(* Proof of correctness *)
+goalw Correctness.thy [Spec.ioa_def, is_weak_ref_map_def]
+ "is_weak_ref_map hom (restrict impl_ioa (externals spec_sig)) spec_ioa";
+by (simp_tac (!simpset addsimps
+ [Correctness.hom_def, cancel_restrict, externals_lemma]) 1);
+by (rtac conjI 1);
+by (simp_tac ss' 1);
+by (asm_simp_tac (!simpset addsimps sels) 1);
+by (REPEAT(rtac allI 1));
+by (rtac imp_conj_lemma 1); (* from lemmas.ML *)
+
+by (Action.action.induct_tac "a" 1);
+by (asm_simp_tac (ss' setloop (split_tac [expand_if])) 1);
+by (forward_tac [inv4] 1);
+by (fast_tac (!claset unsafe_addss (!simpset addsimps [neq_Nil_conv])) 1);
+by (simp_tac ss' 1);
+by (simp_tac ss' 1);
+by (simp_tac ss' 1);
+by (simp_tac ss' 1);
+by (simp_tac ss' 1);
+by (simp_tac ss' 1);
+by (simp_tac ss' 1);
+
+by (asm_simp_tac ss' 1);
+by (forward_tac [inv4] 1);
+by (forward_tac [inv2] 1);
+by (etac disjE 1);
+by (Asm_simp_tac 1);
+by (fast_tac (!claset unsafe_addss (!simpset addsimps [neq_Nil_conv])) 1);
+
+by (asm_simp_tac ss' 1);
+by (forward_tac [inv2] 1);
+by (etac disjE 1);
+
+by (forward_tac [inv3] 1);
+by (case_tac "sq(sen(s))=[]" 1);
+
+by (asm_full_simp_tac ss' 1);
+by (fast_tac (!claset addSDs [add_leD1 RS leD]) 1);
+
+by (case_tac "m = hd(sq(sen(s)))" 1);
+
+by (fast_tac (!claset unsafe_addss (!simpset addsimps [neq_Nil_conv])) 1);
+
+by (Asm_full_simp_tac 1);
+by (fast_tac (!claset addSDs [add_leD1 RS leD]) 1);
+
+by (Asm_full_simp_tac 1);
+qed"ntp_correct";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/NTP/Correctness.thy Wed Apr 30 11:25:31 1997 +0200
@@ -0,0 +1,17 @@
+(* Title: HOL/IOA/NTP/Correctness.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+The main correctness proof: Impl implements Spec
+*)
+
+Correctness = IOA + Impl + Spec +
+
+constdefs
+
+ hom :: 'm impl_state => 'm list
+ "hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s)
+ else ttl(sq(sen s)))"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/NTP/Impl.ML Wed Apr 30 11:25:31 1997 +0200
@@ -0,0 +1,345 @@
+(* Title: HOL/IOA/NTP/Impl.ML
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+The implementation --- Invariants
+*)
+
+
+Addsimps [Let_def];
+
+
+open Abschannel Impl;
+
+val impl_ioas =
+ [Impl.impl_def,
+ Sender.sender_ioa_def,
+ Receiver.receiver_ioa_def,
+ srch_ioa_thm RS eq_reflection,
+ rsch_ioa_thm RS eq_reflection];
+
+val transitions = [Sender.sender_trans_def, Receiver.receiver_trans_def,
+ srch_trans_def, rsch_trans_def];
+
+
+Addsimps [ioa_triple_proj, starts_of_par, trans_of_par4,
+ in_sender_asig, in_receiver_asig, in_srch_asig,
+ in_rsch_asig];
+Addcongs [let_weak_cong];
+
+goal Impl.thy
+ "fst(x) = sen(x) & \
+\ fst(snd(x)) = rec(x) & \
+\ fst(snd(snd(x))) = srch(x) & \
+\ snd(snd(snd(x))) = rsch(x)";
+by(simp_tac (!simpset addsimps
+ [sen_def,rec_def,srch_def,rsch_def]) 1);
+Addsimps [result()];
+
+goal Impl.thy "a:actions(sender_asig) \
+\ | a:actions(receiver_asig) \
+\ | a:actions(srch_asig) \
+\ | a:actions(rsch_asig)";
+ by(Action.action.induct_tac "a" 1);
+ by(ALLGOALS (Simp_tac));
+Addsimps [result()];
+
+Delsimps [split_paired_All];
+
+
+(* Three Simp_sets in different sizes
+----------------------------------------------
+
+1) !simpset does not unfold the transition relations
+2) ss unfolds transition relations
+3) renname_ss unfolds transitions and the abstract channel *)
+
+
+val ss = (!simpset addcongs [if_weak_cong]
+ addsimps transitions);
+val rename_ss = (ss addsimps unfold_renaming);
+
+
+
+val tac = asm_simp_tac ((ss addcongs [conj_cong])
+ setloop (split_tac [expand_if]));
+val tac_ren = asm_simp_tac ((rename_ss addcongs [conj_cong])
+ setloop (split_tac [expand_if]));
+
+
+
+(* INVARIANT 1 *)
+
+goalw Impl.thy impl_ioas "invariant impl_ioa inv1";
+by (rtac invariantI 1);
+by(asm_full_simp_tac (!simpset
+ addsimps [inv1_def, hdr_sum_def, Sender.srcvd_def,
+ Sender.ssent_def, Receiver.rsent_def,Receiver.rrcvd_def]) 1);
+
+by(simp_tac (!simpset delsimps [trans_of_par4]
+ addsimps [fork_lemma,inv1_def]) 1);
+
+(* Split proof in two *)
+by (rtac conjI 1);
+
+(* First half *)
+by(asm_full_simp_tac (!simpset addsimps [Impl.inv1_def]) 1);
+by (rtac Action.action.induct 1);
+
+by (EVERY1[tac, tac, tac, tac]);
+by (tac 1);
+by (tac_ren 1);
+
+(* 5 + 1 *)
+
+by (tac 1);
+by (tac_ren 1);
+
+(* 4 + 1 *)
+by(EVERY1[tac, tac, tac, tac]);
+
+
+(* Now the other half *)
+by(asm_full_simp_tac (!simpset addsimps [Impl.inv1_def]) 1);
+by (rtac Action.action.induct 1);
+by(EVERY1[tac, tac]);
+
+(* detour 1 *)
+by (tac 1);
+by (tac_ren 1);
+by (rtac impI 1);
+by (REPEAT (etac conjE 1));
+by (asm_simp_tac (!simpset addsimps [hdr_sum_def, Multiset.count_def,
+ Multiset.countm_nonempty_def]
+ setloop (split_tac [expand_if])) 1);
+(* detour 2 *)
+by (tac 1);
+by (tac_ren 1);
+by (rtac impI 1);
+by (REPEAT (etac conjE 1));
+by (asm_full_simp_tac (!simpset addsimps [Impl.hdr_sum_def,
+ Multiset.count_def,
+ Multiset.countm_nonempty_def,
+ Multiset.delm_nonempty_def,
+ left_plus_cancel,
+ left_plus_cancel_inside_succ,
+ unzero_less]
+ setloop (split_tac [expand_if])) 1);
+by (rtac allI 1);
+by (rtac conjI 1);
+by (rtac impI 1);
+by (hyp_subst_tac 1);
+by (rtac (pred_suc RS mp RS sym RS iffD2) 1);
+by (dtac less_le_trans 1);
+by (cut_facts_tac [rewrite_rule[Packet.hdr_def]
+ eq_packet_imp_eq_hdr RS countm_props] 1);;
+by (assume_tac 1);
+by (assume_tac 1);
+
+by (rtac (countm_done_delm RS mp RS sym) 1);
+by (rtac refl 1);
+by (asm_simp_tac (!simpset addsimps [Multiset.count_def]) 1);
+
+by (rtac impI 1);
+by (asm_full_simp_tac (!simpset addsimps [neg_flip]) 1);
+by (hyp_subst_tac 1);
+by (rtac countm_spurious_delm 1);
+by (Simp_tac 1);
+
+by (EVERY1[tac, tac, tac, tac, tac, tac]);
+
+qed "inv1";
+
+
+
+(* INVARIANT 2 *)
+
+ goal Impl.thy "invariant impl_ioa inv2";
+
+ by (rtac invariantI1 1);
+ (* Base case *)
+ by (asm_full_simp_tac (!simpset addsimps (inv2_def ::
+ (receiver_projections
+ @ sender_projections @ impl_ioas)))
+ 1);
+
+ by (asm_simp_tac (!simpset addsimps impl_ioas) 1);
+ by (Action.action.induct_tac "a" 1);
+
+ (* 10 cases. First 4 are simple, since state doesn't change *)
+
+val tac2 = asm_full_simp_tac (ss addsimps [inv2_def]);
+
+ (* 10 - 7 *)
+ by (EVERY1[tac2,tac2,tac2,tac2]);
+ (* 6 *)
+ by(forward_tac [rewrite_rule [Impl.inv1_def]
+ (inv1 RS invariantE) RS conjunct1] 1);
+ (* 6 - 5 *)
+ by (EVERY1[tac2,tac2]);
+
+ (* 4 *)
+ by (forward_tac [rewrite_rule [Impl.inv1_def]
+ (inv1 RS invariantE) RS conjunct1] 1);
+ by (tac2 1);
+ by (fast_tac (!claset addDs [add_leD1,leD]) 1);
+
+ (* 3 *)
+ by (forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE)] 1);
+
+ by (tac2 1);
+ by (fold_tac [rewrite_rule [Packet.hdr_def]Impl.hdr_sum_def]);
+ by (fast_tac (!claset addDs [add_leD1,leD]) 1);
+
+ (* 2 *)
+ by (tac2 1);
+ by(forward_tac [rewrite_rule [Impl.inv1_def]
+ (inv1 RS invariantE) RS conjunct1] 1);
+ by (rtac impI 1);
+ by (rtac impI 1);
+ by (REPEAT (etac conjE 1));
+ by (dres_inst_tac [("k","count (rsch s) (~sbit(sen s))")]
+ (standard(leq_add_leq RS mp)) 1);
+ by (Asm_full_simp_tac 1);
+
+ (* 1 *)
+ by (tac2 1);
+ by(forward_tac [rewrite_rule [Impl.inv1_def]
+ (inv1 RS invariantE) RS conjunct2] 1);
+ by (rtac impI 1);
+ by (rtac impI 1);
+ by (REPEAT (etac conjE 1));
+ by (fold_tac [rewrite_rule[Packet.hdr_def]Impl.hdr_sum_def]);
+ by (dres_inst_tac [("k","hdr_sum (srch s) (sbit(sen s))")]
+ (standard(leq_add_leq RS mp)) 1);
+ by (Asm_full_simp_tac 1);
+qed "inv2";
+
+
+(* INVARIANT 3 *)
+
+goal Impl.thy "invariant impl_ioa inv3";
+
+ by (rtac invariantI 1);
+ (* Base case *)
+ by (asm_full_simp_tac (!simpset addsimps
+ (Impl.inv3_def :: (receiver_projections
+ @ sender_projections @ impl_ioas))) 1);
+
+ by (asm_simp_tac (!simpset addsimps impl_ioas) 1);
+ by (Action.action.induct_tac "a" 1);
+
+val tac3 = asm_full_simp_tac (ss addsimps [inv3_def]
+ setloop (split_tac [expand_if]));
+
+ (* 10 - 8 *)
+
+ by (EVERY1[tac3,tac3,tac3]);
+
+ by (tac_ren 1);
+ by (strip_tac 1 THEN REPEAT (etac conjE 1));
+ by (hyp_subst_tac 1);
+ by (etac exE 1);
+ by (Asm_full_simp_tac 1);
+
+ (* 7 *)
+ by (tac3 1);
+ by (tac_ren 1);
+ by (Fast_tac 1);
+
+ (* 6 - 3 *)
+
+ by (EVERY1[tac3,tac3,tac3,tac3]);
+
+ (* 2 *)
+ by (asm_full_simp_tac ss 1);
+ by (simp_tac (!simpset addsimps [inv3_def]) 1);
+ by (strip_tac 1 THEN REPEAT (etac conjE 1));
+ by (rtac (imp_or_lem RS iffD2) 1);
+ by (rtac impI 1);
+ by (forward_tac [rewrite_rule [Impl.inv2_def] (inv2 RS invariantE)] 1);
+ by (Asm_full_simp_tac 1);
+ by (REPEAT (etac conjE 1));
+ by (res_inst_tac [("j","count (ssent(sen s)) (~sbit(sen s))"),
+ ("k","count (rsent(rec s)) (sbit(sen s))")] le_trans 1);
+ by (forward_tac [rewrite_rule [inv1_def]
+ (inv1 RS invariantE) RS conjunct2] 1);
+ by (asm_full_simp_tac (!simpset addsimps
+ [hdr_sum_def, Multiset.count_def]) 1);
+ by (rtac (less_eq_add_cong RS mp RS mp) 1);
+ by (rtac countm_props 1);
+ by (Simp_tac 1);
+ by (rtac countm_props 1);
+ by (Simp_tac 1);
+ by (assume_tac 1);
+
+ (* 1 *)
+ by (tac3 1);
+ by (strip_tac 1 THEN REPEAT (etac conjE 1));
+ by (rtac (imp_or_lem RS iffD2) 1);
+ by (rtac impI 1);
+ by (forward_tac [rewrite_rule [Impl.inv2_def] (inv2 RS invariantE)] 1);
+ by (Asm_full_simp_tac 1);
+ by (REPEAT (etac conjE 1));
+ by (dtac mp 1);
+ by (assume_tac 1);
+ by (etac allE 1);
+ by (dtac (imp_or_lem RS iffD1) 1);
+ by (dtac mp 1);
+ by (assume_tac 1);
+ by (assume_tac 1);
+qed "inv3";
+
+
+(* INVARIANT 4 *)
+
+goal Impl.thy "invariant impl_ioa inv4";
+
+ by (rtac invariantI 1);
+ (* Base case *)
+ by (asm_full_simp_tac (!simpset addsimps
+ (Impl.inv4_def :: (receiver_projections
+ @ sender_projections @ impl_ioas))) 1);
+
+ by (asm_simp_tac (!simpset addsimps impl_ioas) 1);
+ by (Action.action.induct_tac "a" 1);
+
+val tac4 = asm_full_simp_tac (ss addsimps [inv4_def]
+ setloop (split_tac [expand_if]));
+
+ (* 10 - 2 *)
+
+ by (EVERY1[tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4]);
+
+ (* 2 b *)
+
+ by (strip_tac 1 THEN REPEAT (etac conjE 1));
+ by(forward_tac [rewrite_rule [Impl.inv2_def]
+ (inv2 RS invariantE)] 1);
+ by (tac4 1);
+ by (Asm_full_simp_tac 1);
+
+ (* 1 *)
+ by (tac4 1);
+ by (strip_tac 1 THEN REPEAT (etac conjE 1));
+ by (rtac ccontr 1);
+ by(forward_tac [rewrite_rule [Impl.inv2_def]
+ (inv2 RS invariantE)] 1);
+ by(forward_tac [rewrite_rule [Impl.inv3_def]
+ (inv3 RS invariantE)] 1);
+ by (Asm_full_simp_tac 1);
+ by (eres_inst_tac [("x","m")] allE 1);
+ by (dtac less_le_trans 1);
+ by (dtac (left_add_leq RS mp) 1);
+ by (Asm_full_simp_tac 1);
+ by (Asm_full_simp_tac 1);
+qed "inv4";
+
+
+(* rebind them *)
+
+val inv1 = rewrite_rule [Impl.inv1_def] (inv1 RS invariantE);
+val inv2 = rewrite_rule [Impl.inv2_def] (inv2 RS invariantE);
+val inv3 = rewrite_rule [Impl.inv3_def] (inv3 RS invariantE);
+val inv4 = rewrite_rule [Impl.inv4_def] (inv4 RS invariantE);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/NTP/Impl.thy Wed Apr 30 11:25:31 1997 +0200
@@ -0,0 +1,71 @@
+(* Title: HOL/IOA/NTP/Impl.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+The implementation
+*)
+
+Impl = Sender + Receiver + Abschannel +
+
+types
+
+'m impl_state
+= "'m sender_state * 'm receiver_state * 'm packet multiset * bool multiset"
+(* sender_state * receiver_state * srch_state * rsch_state *)
+
+
+consts
+ impl_ioa :: ('m action, 'm impl_state)ioa
+ sen :: 'm impl_state => 'm sender_state
+ rec :: 'm impl_state => 'm receiver_state
+ srch :: 'm impl_state => 'm packet multiset
+ rsch :: 'm impl_state => bool multiset
+ inv1, inv2,
+ inv3, inv4 :: 'm impl_state => bool
+ hdr_sum :: 'm packet multiset => bool => nat
+
+defs
+
+ impl_def
+ "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
+
+ sen_def "sen == fst"
+ rec_def "rec == fst o snd"
+ srch_def "srch == fst o snd o snd"
+ rsch_def "rsch == snd o snd o snd"
+
+hdr_sum_def
+ "hdr_sum M b == countm M (%pkt.hdr(pkt) = b)"
+
+(* Lemma 5.1 *)
+inv1_def
+ "inv1(s) ==
+ (!b. count (rsent(rec s)) b = count (srcvd(sen s)) b + count (rsch s) b)
+ & (!b. count (ssent(sen s)) b
+ = hdr_sum (rrcvd(rec s)) b + hdr_sum (srch s) b)"
+
+(* Lemma 5.2 *)
+ inv2_def "inv2(s) ==
+ (rbit(rec(s)) = sbit(sen(s)) &
+ ssending(sen(s)) &
+ count (rsent(rec s)) (~sbit(sen s)) <= count (ssent(sen s)) (~sbit(sen s)) &
+ count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s)))
+ |
+ (rbit(rec(s)) = (~sbit(sen(s))) &
+ rsending(rec(s)) &
+ count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s)) &
+ count (rsent(rec s)) (sbit(sen s)) <= count (ssent(sen s)) (sbit(sen s)))"
+
+(* Lemma 5.3 *)
+ inv3_def "inv3(s) ==
+ rbit(rec(s)) = sbit(sen(s))
+ --> (!m. sq(sen(s))=[] | m ~= hd(sq(sen(s)))
+ --> count (rrcvd(rec s)) (sbit(sen(s)),m)
+ + count (srch s) (sbit(sen(s)),m)
+ <= count (rsent(rec s)) (~sbit(sen s)))"
+
+(* Lemma 5.4 *)
+ inv4_def "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) --> sq(sen(s)) ~= []"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/NTP/Lemmas.ML Wed Apr 30 11:25:31 1997 +0200
@@ -0,0 +1,210 @@
+(* Title: HOL/IOA/NTP/Lemmas.ML
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+(Mostly) Arithmetic lemmas
+Should realy go in Arith.ML.
+Also: Get rid of all the --> in favour of ==> !!!
+*)
+
+(* Logic *)
+val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
+ by(fast_tac (!claset addDs prems) 1);
+qed "imp_conj_lemma";
+
+goal HOL.thy "(P --> (? x. Q(x))) = (? x. P --> Q(x))";
+ by(Fast_tac 1);
+qed "imp_ex_equiv";
+
+goal HOL.thy "(A --> B & C) = ((A --> B) & (A --> C))";
+ by (Fast_tac 1);
+qed "fork_lemma";
+
+goal HOL.thy "((A --> B) & (C --> B)) = ((A | C) --> B)";
+ by (Fast_tac 1);
+qed "imp_or_lem";
+
+goal HOL.thy "(X = (~ Y)) = ((~X) = Y)";
+ by (Fast_tac 1);
+qed "neg_flip";
+
+goal HOL.thy "P --> Q(M) --> Q(if P then M else N)";
+ by (rtac impI 1);
+ by (rtac impI 1);
+ by (rtac (expand_if RS iffD2) 1);
+ by (Fast_tac 1);
+qed "imp_true_decompose";
+
+goal HOL.thy "(~P) --> Q(N) --> Q(if P then M else N)";
+ by (rtac impI 1);
+ by (rtac impI 1);
+ by (rtac (expand_if RS iffD2) 1);
+ by (Fast_tac 1);
+qed "imp_false_decompose";
+
+
+(* Sets *)
+val set_lemmas =
+ map (fn s => prove_goal Set.thy s (fn _ => [Fast_tac 1]))
+ ["f(x) : (UN x. {f(x)})",
+ "f x y : (UN x y. {f x y})",
+ "!!a. (!x. a ~= f(x)) ==> a ~: (UN x. {f(x)})",
+ "!!a. (!x y. a ~= f x y) ==> a ~: (UN x y. {f x y})"];
+
+
+(* Arithmetic *)
+goal Arith.thy "n ~= 0 --> Suc(m+pred(n)) = m+n";
+ by (nat_ind_tac "n" 1);
+ by (REPEAT(Simp_tac 1));
+val Suc_pred_lemma = store_thm("Suc_pred_lemma", result() RS mp);
+
+goal Arith.thy "((m::nat) + n = m + p) = (n = p)";
+ by (nat_ind_tac "m" 1);
+ by (Simp_tac 1);
+ by (Asm_simp_tac 1);
+qed "left_plus_cancel";
+
+goal Arith.thy "((x::nat) + y = Suc(x + z)) = (y = Suc(z))";
+ by (nat_ind_tac "x" 1);
+ by (Simp_tac 1);
+ by (Asm_simp_tac 1);
+qed "left_plus_cancel_inside_succ";
+
+goal Arith.thy "(x ~= 0) = (? y. x = Suc(y))";
+ by (nat_ind_tac "x" 1);
+ by (Simp_tac 1);
+ by (Asm_simp_tac 1);
+qed "nonzero_is_succ";
+
+goal Arith.thy "(m::nat) < n --> m + p < n + p";
+ by (nat_ind_tac "p" 1);
+ by (Simp_tac 1);
+ by (Asm_simp_tac 1);
+qed "less_add_same_less";
+
+goal Arith.thy "(x::nat)<= y --> x<=y+k";
+ by (nat_ind_tac "k" 1);
+ by (Simp_tac 1);
+ by (Asm_full_simp_tac 1);
+qed "leq_add_leq";
+
+goal Arith.thy "(x::nat) + y <= z --> x <= z";
+ by (nat_ind_tac "y" 1);
+ by (Simp_tac 1);
+ by (Asm_simp_tac 1);
+ by (rtac impI 1);
+ by (dtac Suc_leD 1);
+ by (Fast_tac 1);
+qed "left_add_leq";
+
+goal Arith.thy "(A::nat) < B --> C < D --> A + C < B + D";
+ by (rtac impI 1);
+ by (rtac impI 1);
+ by (rtac less_trans 1);
+ by (rtac (less_add_same_less RS mp) 1);
+ by (assume_tac 1);
+ by (rtac (add_commute RS ssubst)1);;
+ by (res_inst_tac [("m1","B")] (add_commute RS ssubst) 1);
+ by (rtac (less_add_same_less RS mp) 1);
+ by (assume_tac 1);
+qed "less_add_cong";
+
+goal Arith.thy "(A::nat) <= B --> C <= D --> A + C <= B + D";
+ by (rtac impI 1);
+ by (rtac impI 1);
+ by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
+ by (safe_tac (!claset));
+ by (rtac (less_add_cong RS mp RS mp) 1);
+ by (assume_tac 1);
+ by (assume_tac 1);
+ by (rtac (less_add_same_less RS mp) 1);
+ by (assume_tac 1);
+ by (rtac (add_commute RS ssubst)1);;
+ by (res_inst_tac [("m1","B")] (add_commute RS ssubst) 1);
+ by (rtac (less_add_same_less RS mp) 1);
+ by (assume_tac 1);
+qed "less_eq_add_cong";
+
+goal Arith.thy "(w <= y) --> ((x::nat) + y <= z) --> (x + w <= z)";
+ by (rtac impI 1);
+ by (dtac (less_eq_add_cong RS mp) 1);
+ by (cut_facts_tac [le_refl] 1);
+ by (dres_inst_tac [("P","x<=x")] mp 1);by (assume_tac 1);
+ by (asm_full_simp_tac (!simpset addsimps [add_commute]) 1);
+ by (rtac impI 1);
+ by (etac le_trans 1);
+ by (assume_tac 1);
+qed "leq_add_left_cong";
+
+goal Arith.thy "(? x. y = Suc(x)) = (~(y = 0))";
+ by (nat_ind_tac "y" 1);
+ by (Simp_tac 1);
+ by (rtac iffI 1);
+ by (Asm_full_simp_tac 1);
+ by (Fast_tac 1);
+qed "suc_not_zero";
+
+goal Arith.thy "Suc(x) <= y --> (? z. y = Suc(z))";
+ by (rtac impI 1);
+ by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
+ by (safe_tac (!claset));
+ by (Fast_tac 2);
+ by (asm_simp_tac (!simpset addsimps [suc_not_zero]) 1);
+qed "suc_leq_suc";
+
+goal Arith.thy "~0<n --> n = 0";
+ by (nat_ind_tac "n" 1);
+ by (Auto_tac ());
+qed "zero_eq";
+
+goal Arith.thy "x < Suc(y) --> x<=y";
+ by (nat_ind_tac "n" 1);
+ by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
+ by (safe_tac (!claset));
+ by (etac less_imp_le 1);
+qed "less_suc_imp_leq";
+
+goal Arith.thy "0<x --> Suc(pred(x)) = x";
+ by (nat_ind_tac "x" 1);
+ by (Simp_tac 1);
+ by (Asm_simp_tac 1);
+qed "suc_pred_id";
+
+goal Arith.thy "0<x --> (pred(x) = y) = (x = Suc(y))";
+ by (nat_ind_tac "x" 1);
+ by (Simp_tac 1);
+ by (Asm_simp_tac 1);
+qed "pred_suc";
+
+goal Arith.thy "(x ~= 0) = (0<x)";
+ by (nat_ind_tac "x" 1);
+ by (Simp_tac 1);
+ by (Asm_simp_tac 1);
+qed "unzero_less";
+
+(* Odd proof. Why do induction? *)
+goal Arith.thy "((x::nat) = y + z) --> (y <= x)";
+ by (nat_ind_tac "y" 1);
+ by (Simp_tac 1);
+ by (simp_tac (!simpset addsimps [le_refl RS (leq_add_leq RS mp)]) 1);
+qed "plus_leq_lem";
+
+(* Lists *)
+
+val list_ss = simpset_of "List";
+
+goal List.thy "(xs @ (y#ys)) ~= []";
+ by (list.induct_tac "xs" 1);
+ by (simp_tac list_ss 1);
+ by (asm_simp_tac list_ss 1);
+qed "append_cons";
+
+goal List.thy "(x ~= hd(xs@ys)) = (x ~= (if xs = [] then hd ys else hd xs))";
+ by (list.induct_tac "xs" 1);
+ by (simp_tac list_ss 1);
+ by (asm_full_simp_tac list_ss 1);
+qed "not_hd_append";
+
+
+Addsimps ([append_cons,not_hd_append,Suc_pred_lemma] @ set_lemmas);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/NTP/Lemmas.thy Wed Apr 30 11:25:31 1997 +0200
@@ -0,0 +1,9 @@
+(* Title: HOL/IOA/NTP/Lemmas.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+Arithmetic lemmas
+*)
+
+Lemmas = Arith
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/NTP/Multiset.ML Wed Apr 30 11:25:31 1997 +0200
@@ -0,0 +1,87 @@
+(* Title: HOL/IOA/NTP/Multiset.ML
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+Axiomatic multisets.
+Should be done as a subtype and moved to a global place.
+*)
+
+goalw Multiset.thy [Multiset.count_def, Multiset.countm_empty_def]
+ "count {|} x = 0";
+ by (rtac refl 1);
+qed "count_empty";
+
+goal Multiset.thy
+ "count (addm M x) y = (if y=x then Suc(count M y) else count M y)";
+ by (asm_simp_tac (!simpset addsimps
+ [Multiset.count_def,Multiset.countm_nonempty_def]
+ setloop (split_tac [expand_if])) 1);
+qed "count_addm_simp";
+
+goal Multiset.thy "count M y <= count (addm M x) y";
+ by (simp_tac (!simpset addsimps [count_addm_simp]
+ setloop (split_tac [expand_if])) 1);
+qed "count_leq_addm";
+
+goalw Multiset.thy [Multiset.count_def]
+ "count (delm M x) y = (if y=x then pred(count M y) else count M y)";
+ by (res_inst_tac [("M","M")] Multiset.induction 1);
+ by (asm_simp_tac (!simpset
+ addsimps [Multiset.delm_empty_def,Multiset.countm_empty_def]
+ setloop (split_tac [expand_if])) 1);
+ by (asm_full_simp_tac (!simpset
+ addsimps [Multiset.delm_nonempty_def,
+ Multiset.countm_nonempty_def]
+ setloop (split_tac [expand_if])) 1);
+ by (safe_tac (!claset));
+ by (Asm_full_simp_tac 1);
+qed "count_delm_simp";
+
+goal Multiset.thy "!!M. (!x. P(x) --> Q(x)) ==> (countm M P <= countm M Q)";
+ by (res_inst_tac [("M","M")] Multiset.induction 1);
+ by (simp_tac (!simpset addsimps [Multiset.countm_empty_def]) 1);
+ by (simp_tac (!simpset addsimps[Multiset.countm_nonempty_def]) 1);
+ by (etac (less_eq_add_cong RS mp RS mp) 1);
+ by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]
+ setloop (split_tac [expand_if])) 1);
+qed "countm_props";
+
+goal Multiset.thy "!!P. ~P(obj) ==> countm M P = countm (delm M obj) P";
+ by (res_inst_tac [("M","M")] Multiset.induction 1);
+ by (simp_tac (!simpset addsimps [Multiset.delm_empty_def,
+ Multiset.countm_empty_def]) 1);
+ by (asm_simp_tac (!simpset addsimps[Multiset.countm_nonempty_def,
+ Multiset.delm_nonempty_def]
+ setloop (split_tac [expand_if])) 1);
+qed "countm_spurious_delm";
+
+
+goal Multiset.thy "!!P. P(x) ==> 0<count M x --> 0<countm M P";
+ by (res_inst_tac [("M","M")] Multiset.induction 1);
+ by (simp_tac (!simpset addsimps
+ [Multiset.delm_empty_def,Multiset.count_def,
+ Multiset.countm_empty_def]) 1);
+ by (asm_simp_tac (!simpset addsimps
+ [Multiset.count_def,Multiset.delm_nonempty_def,
+ Multiset.countm_nonempty_def]
+ setloop (split_tac [expand_if])) 1);
+val pos_count_imp_pos_countm = store_thm("pos_count_imp_pos_countm", standard(result() RS mp));
+
+goal Multiset.thy
+ "!!P. P(x) ==> 0<count M x --> countm (delm M x) P = pred (countm M P)";
+ by (res_inst_tac [("M","M")] Multiset.induction 1);
+ by (simp_tac (!simpset addsimps
+ [Multiset.delm_empty_def,
+ Multiset.countm_empty_def]) 1);
+ by (asm_simp_tac (!simpset addsimps
+ [eq_sym_conv,count_addm_simp,Multiset.delm_nonempty_def,
+ Multiset.countm_nonempty_def,pos_count_imp_pos_countm,
+ suc_pred_id]
+ setloop (split_tac [expand_if])) 1);
+qed "countm_done_delm";
+
+
+Addsimps [count_addm_simp, count_delm_simp,
+ Multiset.countm_empty_def, Multiset.delm_empty_def,
+ count_empty];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/NTP/Multiset.thy Wed Apr 30 11:25:31 1997 +0200
@@ -0,0 +1,48 @@
+(* Title: HOL/IOA/NTP/Multiset.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+Axiomatic multisets.
+Should be done as a subtype and moved to a global place.
+*)
+
+Multiset = Arith + Lemmas +
+
+types
+
+ 'a multiset
+
+arities
+
+ multiset :: (term) term
+
+consts
+
+ "{|}" :: 'a multiset ("{|}")
+ addm :: ['a multiset, 'a] => 'a multiset
+ delm :: ['a multiset, 'a] => 'a multiset
+ countm :: ['a multiset, 'a => bool] => nat
+ count :: ['a multiset, 'a] => nat
+
+rules
+
+delm_empty_def
+ "delm {|} x = {|}"
+
+delm_nonempty_def
+ "delm (addm M x) y == (if x=y then M else addm (delm M y) x)"
+
+countm_empty_def
+ "countm {|} P == 0"
+
+countm_nonempty_def
+ "countm (addm M x) P == countm M P + (if P x then Suc 0 else 0)"
+
+count_def
+ "count M x == countm M (%y.y = x)"
+
+induction
+ "[| P({|}); !!M x. P(M) ==> P(addm M x) |] ==> P(M)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/NTP/Packet.ML Wed Apr 30 11:25:31 1997 +0200
@@ -0,0 +1,15 @@
+(* Title: HOL/IOA/NTP/Packet.ML
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+Packets
+*)
+
+
+(* Instantiation of a tautology? *)
+goal Packet.thy "!x. x = packet --> hdr(x) = hdr(packet)";
+ by (simp_tac (!simpset addsimps [Packet.hdr_def]) 1);
+qed "eq_packet_imp_eq_hdr";
+
+Addsimps [Packet.hdr_def,Packet.msg_def];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/NTP/Packet.thy Wed Apr 30 11:25:31 1997 +0200
@@ -0,0 +1,23 @@
+(* Title: HOL/IOA/NTP/Packet.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+Packets
+*)
+
+Packet = Arith + Multiset +
+
+types
+
+ 'msg packet = "bool * 'msg"
+
+constdefs
+
+ hdr :: 'msg packet => bool
+ "hdr == fst"
+
+ msg :: 'msg packet => 'msg
+ "msg == snd"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/NTP/ROOT.ML Wed Apr 30 11:25:31 1997 +0200
@@ -0,0 +1,18 @@
+(* Title: HOL/IOA/examples/NTP/ROOT.ML
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+This is the ROOT file for a network transmission protocol (NTP subdirectory),
+performed in the I/O automata formalization by Olaf Mueller.
+
+For details see the README.html file.
+
+Should be executed in the subdirectory HOLCF/IOA/examples/NTP.
+*)
+
+goals_limit := 1;
+
+loadpath:=["."];
+
+use_thy "Correctness";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/NTP/Read_me Wed Apr 30 11:25:31 1997 +0200
@@ -0,0 +1,182 @@
+Isabelle Verification of a protocol using IOA.
+
+------------------------------------------------------------------------------
+The theory structure looks like this picture:
+
+ Correctness
+
+ Impl
+
+Sender Receiver Channels Spec
+
+ Action IOA Multisets
+
+ Packet List
+
+ Arith
+
+------------------------------------------------------------------------------
+
+The System.
+
+The system being proved correct is a parallel composition of 4 processes:
+
+ Sender || Schannel || Receiver || Rchannel
+
+Accordingly, the system state is a 4-tuple:
+
+ (Sender_state, Schannel_state, Receiver_state, Rchannel_state)
+
+------------------------------------------------------------------------------
+Packets.
+
+The objects going over the medium from Sender to Receiver are modelled
+with the type
+
+ 'm packet = bool * 'm
+
+This expresses that messages (modelled by polymorphic type "'m") are
+sent with a single header bit. Packet fields are accessed by
+
+ hdr<b,m> = b
+ mesg<b,m> = m
+------------------------------------------------------------------------------
+
+The Sender.
+
+The state of the process "Sender" is a 5-tuple:
+
+ 1. messages : 'm list (* sq *)
+ 2. sent : bool multiset (* ssent *)
+ 3. received : bool multiset (* srcvd *)
+ 4. header : bool (* sbit *)
+ 5. mode : bool (* ssending *)
+
+
+The Receiver.
+
+The state of the process "Receiver" is a 5-tuple:
+
+ 1. messages : 'm list (* rq *)
+ 2. replies : bool multiset (* rsent *)
+ 3. received : 'm packet multiset (* rrcvd *)
+ 4. header : bool (* rbit *)
+ 5. mode : bool (* rsending *)
+
+
+The Channels.
+
+The Sender and Receiver each have a proprietary channel, named
+"Schannel" and "Rchannel" respectively. The messages sent by the Sender
+and Receiver are never lost, but the channels may mix them
+up. Accordingly, multisets are used in modelling the state of the
+channels. The state of "Schannel" is modelled with the following type:
+
+ 'm packet multiset
+
+The state of "Rchannel" is modelled with the following type:
+
+ bool multiset
+
+This expresses that replies from the Receiver are just one bit.
+
+Both Channels are instances of an abstract channel, that is modelled with
+the type
+
+ 'a multiset.
+
+------------------------------------------------------------------------------
+
+The events.
+
+An `execution' of the system is modelled by a sequence of
+
+ <system_state, action, system_state>
+
+transitions. The actions, or events, of the system are described by the
+following ML-style datatype declaration:
+
+ 'm action = S_msg ('m) (* Rqt for Sender to send mesg *)
+ | R_msg ('m) (* Mesg taken from Receiver's queue *)
+ | S_pkt_sr ('m packet) (* Packet arrives in Schannel *)
+ | R_pkt_sr ('m packet) (* Packet leaves Schannel *)
+ | S_pkt_rs (bool) (* Packet arrives in Rchannel *)
+ | R_pkt_rs (bool) (* Packet leaves Rchannel *)
+ | C_m_s (* Change mode in Sender *)
+ | C_m_r (* Change mode in Receiver *)
+ | C_r_s (* Change round in Sender *)
+ | C_r_r ('m) (* Change round in Receiver *)
+
+------------------------------------------------------------------------------
+
+The Specification.
+
+The abstract description of system behaviour is given by defining an
+IO/automaton named "Spec". The state of Spec is a message queue,
+modelled as an "'m list". The only actions performed in the abstract
+system are: "S_msg(m)" (putting message "m" at the end of the queue);
+and "R_msg(m)" (taking message "m" from the head of the queue).
+
+
+------------------------------------------------------------------------------
+
+The Verification.
+
+The verification proceeds by showing that a certain mapping ("hom") from
+the concrete system state to the abstract system state is a `weak
+possibilities map` from "Impl" to "Spec".
+
+
+ hom : (S_state * Sch_state * R_state * Rch_state) -> queue
+
+The verification depends on several system invariants that relate the
+states of the 4 processes. These invariants must hold in all reachable
+states of the system. These invariants are difficult to make sense of;
+however, we attempt to give loose English paraphrases of them.
+
+Invariant 1.
+
+This expresses that no packets from the Receiver to the Sender are
+dropped by Rchannel. The analogous statement for Schannel is also true.
+
+ !b. R.replies b = S.received b + Rch b
+ /\
+ !pkt. S.sent(hdr(pkt)) = R.received(hdr(b)) + Sch(pkt)
+
+
+Invariant 2.
+
+This expresses a complicated relationship about how many messages are
+sent and header bits.
+
+ R.header = S.header
+ /\ S.mode = SENDING
+ /\ R.replies (flip S.header) <= S.sent (flip S.header)
+ /\ S.sent (flip S.header) <= R.replies header
+ OR
+ R.header = flip S.header
+ /\ R.mode = SENDING
+ /\ S.sent (flip S.header) <= R.replies S.header
+ /\ R.replies S.header <= S.sent S.header
+
+
+Invariant 3.
+
+The number of incoming messages in the Receiver plus the number of those
+messages in transit (in Schannel) is not greater than the number of
+replies, provided the message isn't current and the header bits agree.
+
+ let mesg = <S.header, m>
+ in
+ R.header = S.header
+ ==>
+ !m. (S.messages = [] \/ m ~= hd S.messages)
+ ==> R.received mesg + Sch mesg <= R.replies (flip S.header)
+
+
+Invariant 4.
+
+If the headers are opposite, then the Sender queue has a message in it.
+
+ R.header = flip S.header ==> S.messages ~= []
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/NTP/Receiver.ML Wed Apr 30 11:25:31 1997 +0200
@@ -0,0 +1,29 @@
+(* Title: HOL/IOA/NTP/Receiver.ML
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+*)
+
+goal Receiver.thy
+ "S_msg(m) ~: actions(receiver_asig) & \
+\ R_msg(m) : actions(receiver_asig) & \
+\ S_pkt(pkt) ~: actions(receiver_asig) & \
+\ R_pkt(pkt) : actions(receiver_asig) & \
+\ S_ack(b) : actions(receiver_asig) & \
+\ R_ack(b) ~: actions(receiver_asig) & \
+\ C_m_s ~: actions(receiver_asig) & \
+\ C_m_r : actions(receiver_asig) & \
+\ C_r_s ~: actions(receiver_asig) & \
+\ C_r_r(m) : actions(receiver_asig)";
+ by(simp_tac (!simpset addsimps (Receiver.receiver_asig_def :: actions_def ::
+ asig_projections)) 1);
+qed "in_receiver_asig";
+
+val receiver_projections =
+ [Receiver.rq_def,
+ Receiver.rsent_def,
+ Receiver.rrcvd_def,
+ Receiver.rbit_def,
+ Receiver.rsending_def];
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/NTP/Receiver.thy Wed Apr 30 11:25:31 1997 +0200
@@ -0,0 +1,89 @@
+(* Title: HOL/IOA/NTP/Receiver.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+The implementation: receiver
+*)
+
+Receiver = List + IOA + Action +
+
+types
+
+'m receiver_state
+= "'m list * bool multiset * 'm packet multiset * bool * bool"
+(* messages #replies #received header mode *)
+
+consts
+
+ receiver_asig :: 'm action signature
+ receiver_trans:: ('m action, 'm receiver_state)transition set
+ receiver_ioa :: ('m action, 'm receiver_state)ioa
+ rq :: 'm receiver_state => 'm list
+ rsent :: 'm receiver_state => bool multiset
+ rrcvd :: 'm receiver_state => 'm packet multiset
+ rbit :: 'm receiver_state => bool
+ rsending :: 'm receiver_state => bool
+
+defs
+
+rq_def "rq == fst"
+rsent_def "rsent == fst o snd"
+rrcvd_def "rrcvd == fst o snd o snd"
+rbit_def "rbit == fst o snd o snd o snd"
+rsending_def "rsending == snd o snd o snd o snd"
+
+receiver_asig_def "receiver_asig ==
+ (UN pkt. {R_pkt(pkt)},
+ (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),
+ insert C_m_r (UN m. {C_r_r(m)}))"
+
+receiver_trans_def "receiver_trans ==
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in
+ case fst(snd(tr))
+ of
+ S_msg(m) => False |
+ R_msg(m) => rq(s) = (m # rq(t)) &
+ rsent(t)=rsent(s) &
+ rrcvd(t)=rrcvd(s) &
+ rbit(t)=rbit(s) &
+ rsending(t)=rsending(s) |
+ S_pkt(pkt) => False |
+ R_pkt(pkt) => rq(t) = rq(s) &
+ rsent(t) = rsent(s) &
+ rrcvd(t) = addm (rrcvd s) pkt &
+ rbit(t) = rbit(s) &
+ rsending(t) = rsending(s) |
+ S_ack(b) => b = rbit(s) &
+ rq(t) = rq(s) &
+ rsent(t) = addm (rsent s) (rbit s) &
+ rrcvd(t) = rrcvd(s) &
+ rbit(t)=rbit(s) &
+ rsending(s) &
+ rsending(t) |
+ R_ack(b) => False |
+ C_m_s => False |
+ C_m_r => count (rsent s) (~rbit s) < countm (rrcvd s) (%y.hdr(y)=rbit(s)) &
+ rq(t) = rq(s) &
+ rsent(t)=rsent(s) &
+ rrcvd(t)=rrcvd(s) &
+ rbit(t)=rbit(s) &
+ rsending(s) &
+ ~rsending(t) |
+ C_r_s => False |
+ C_r_r(m) => count (rsent s) (rbit s) <= countm (rrcvd s) (%y.hdr(y)=rbit(s)) &
+ count (rsent s) (~rbit s) < count (rrcvd s) (rbit(s),m) &
+ rq(t) = rq(s)@[m] &
+ rsent(t)=rsent(s) &
+ rrcvd(t)=rrcvd(s) &
+ rbit(t) = (~rbit(s)) &
+ ~rsending(s) &
+ rsending(t)}"
+
+
+receiver_ioa_def "receiver_ioa ==
+ (receiver_asig, {([],{|},{|},False,False)}, receiver_trans)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/NTP/Sender.ML Wed Apr 30 11:25:31 1997 +0200
@@ -0,0 +1,25 @@
+(* Title: HOL/IOA/NTP/Sender.ML
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+*)
+
+goal Sender.thy
+ "S_msg(m) : actions(sender_asig) & \
+\ R_msg(m) ~: actions(sender_asig) & \
+\ S_pkt(pkt) : actions(sender_asig) & \
+\ R_pkt(pkt) ~: actions(sender_asig) & \
+\ S_ack(b) ~: actions(sender_asig) & \
+\ R_ack(b) : actions(sender_asig) & \
+\ C_m_s : actions(sender_asig) & \
+\ C_m_r ~: actions(sender_asig) & \
+\ C_r_s : actions(sender_asig) & \
+\ C_r_r(m) ~: actions(sender_asig)";
+by(simp_tac (!simpset addsimps
+ (Sender.sender_asig_def :: actions_def ::
+ asig_projections)) 1);
+qed "in_sender_asig";
+
+val sender_projections =
+ [Sender.sq_def,Sender.ssent_def,Sender.srcvd_def,
+ Sender.sbit_def,Sender.ssending_def];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/NTP/Sender.thy Wed Apr 30 11:25:31 1997 +0200
@@ -0,0 +1,85 @@
+(* Title: HOL/IOA/NTP/Sender.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+The implementation: sender
+*)
+
+Sender = IOA + Action + List +
+
+types
+
+'m sender_state = "'m list * bool multiset * bool multiset * bool * bool"
+(* messages #sent #received header mode *)
+
+consts
+
+sender_asig :: 'm action signature
+sender_trans :: ('m action, 'm sender_state)transition set
+sender_ioa :: ('m action, 'm sender_state)ioa
+sq :: 'm sender_state => 'm list
+ssent,srcvd :: 'm sender_state => bool multiset
+sbit :: 'm sender_state => bool
+ssending :: 'm sender_state => bool
+
+defs
+
+sq_def "sq == fst"
+ssent_def "ssent == fst o snd"
+srcvd_def "srcvd == fst o snd o snd"
+sbit_def "sbit == fst o snd o snd o snd"
+ssending_def "ssending == snd o snd o snd o snd"
+
+sender_asig_def
+ "sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),
+ UN pkt. {S_pkt(pkt)},
+ {C_m_s,C_r_s})"
+
+sender_trans_def "sender_trans ==
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in case fst(snd(tr))
+ of
+ S_msg(m) => sq(t)=sq(s)@[m] &
+ ssent(t)=ssent(s) &
+ srcvd(t)=srcvd(s) &
+ sbit(t)=sbit(s) &
+ ssending(t)=ssending(s) |
+ R_msg(m) => False |
+ S_pkt(pkt) => hdr(pkt) = sbit(s) &
+ (? Q. sq(s) = (msg(pkt)#Q)) &
+ sq(t) = sq(s) &
+ ssent(t) = addm (ssent s) (sbit s) &
+ srcvd(t) = srcvd(s) &
+ sbit(t) = sbit(s) &
+ ssending(s) &
+ ssending(t) |
+ R_pkt(pkt) => False |
+ S_ack(b) => False |
+ R_ack(b) => sq(t)=sq(s) &
+ ssent(t)=ssent(s) &
+ srcvd(t) = addm (srcvd s) b &
+ sbit(t)=sbit(s) &
+ ssending(t)=ssending(s) |
+ C_m_s => count (ssent s) (~sbit s) < count (srcvd s) (~sbit s) &
+ sq(t)=sq(s) &
+ ssent(t)=ssent(s) &
+ srcvd(t)=srcvd(s) &
+ sbit(t)=sbit(s) &
+ ssending(s) &
+ ~ssending(t) |
+ C_m_r => False |
+ C_r_s => count (ssent s) (sbit s) <= count (srcvd s) (~sbit s) &
+ sq(t)=tl(sq(s)) &
+ ssent(t)=ssent(s) &
+ srcvd(t)=srcvd(s) &
+ sbit(t) = (~sbit(s)) &
+ ~ssending(s) &
+ ssending(t) |
+ C_r_r(m) => False}"
+
+sender_ioa_def "sender_ioa ==
+ (sender_asig, {([],{|},{|},False,True)}, sender_trans)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/NTP/Spec.thy Wed Apr 30 11:25:31 1997 +0200
@@ -0,0 +1,42 @@
+(* Title: HOL/IOA/NTP/Spec.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+The specification of reliable transmission
+*)
+
+Spec = List + IOA + Action +
+
+consts
+
+spec_sig :: 'm action signature
+spec_trans :: ('m action, 'm list)transition set
+spec_ioa :: ('m action, 'm list)ioa
+
+defs
+
+sig_def "spec_sig == (UN m.{S_msg(m)},
+ UN m.{R_msg(m)},
+ {})"
+
+trans_def "spec_trans ==
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in
+ case fst(snd(tr))
+ of
+ S_msg(m) => t = s@[m] |
+ R_msg(m) => s = (m#t) |
+ S_pkt(pkt) => False |
+ R_pkt(pkt) => False |
+ S_ack(b) => False |
+ R_ack(b) => False |
+ C_m_s => False |
+ C_m_r => False |
+ C_r_s => False |
+ C_r_r(m) => False}"
+
+ioa_def "spec_ioa == (spec_sig, {[]}, spec_trans)"
+
+end