# HG changeset patch # User mueller # Date 862392331 -7200 # Node ID 88366253a09af020c1e8b5b11e7a2f3b65c3760d # Parent a31419014be588494662008f27cd8b1fde7949c1 Old NTP files now running under the IOA meta theory based on HOLCF; diff -r a31419014be5 -r 88366253a09a src/HOLCF/IOA/NTP/Abschannel.ML --- /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"; + diff -r a31419014be5 -r 88366253a09a src/HOLCF/IOA/NTP/Abschannel.thy --- /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 + + + + + + + + + + + + + + + + + + diff -r a31419014be5 -r 88366253a09a src/HOLCF/IOA/NTP/Action.ML --- /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()]; diff -r a31419014be5 -r 88366253a09a src/HOLCF/IOA/NTP/Action.thy --- /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 diff -r a31419014be5 -r 88366253a09a src/HOLCF/IOA/NTP/Correctness.ML --- /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"; diff -r a31419014be5 -r 88366253a09a src/HOLCF/IOA/NTP/Correctness.thy --- /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 diff -r a31419014be5 -r 88366253a09a src/HOLCF/IOA/NTP/Impl.ML --- /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); diff -r a31419014be5 -r 88366253a09a src/HOLCF/IOA/NTP/Impl.thy --- /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 diff -r a31419014be5 -r 88366253a09a src/HOLCF/IOA/NTP/Lemmas.ML --- /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 = 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 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 (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 (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); diff -r a31419014be5 -r 88366253a09a src/HOLCF/IOA/NTP/Lemmas.thy --- /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 diff -r a31419014be5 -r 88366253a09a src/HOLCF/IOA/NTP/Multiset.ML --- /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 0 0 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]; diff -r a31419014be5 -r 88366253a09a src/HOLCF/IOA/NTP/Multiset.thy --- /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 diff -r a31419014be5 -r 88366253a09a src/HOLCF/IOA/NTP/Packet.ML --- /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]; diff -r a31419014be5 -r 88366253a09a src/HOLCF/IOA/NTP/Packet.thy --- /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 diff -r a31419014be5 -r 88366253a09a src/HOLCF/IOA/NTP/ROOT.ML --- /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"; diff -r a31419014be5 -r 88366253a09a src/HOLCF/IOA/NTP/Read_me --- /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 + mesg = 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 + + + +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 = + 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 ~= [] + diff -r a31419014be5 -r 88366253a09a src/HOLCF/IOA/NTP/Receiver.ML --- /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]; + + diff -r a31419014be5 -r 88366253a09a src/HOLCF/IOA/NTP/Receiver.thy --- /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 diff -r a31419014be5 -r 88366253a09a src/HOLCF/IOA/NTP/Sender.ML --- /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]; diff -r a31419014be5 -r 88366253a09a src/HOLCF/IOA/NTP/Sender.thy --- /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 diff -r a31419014be5 -r 88366253a09a src/HOLCF/IOA/NTP/Spec.thy --- /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