# HG changeset patch # User mueller # Date 862394010 -7200 # Node ID 3e8d80cdd3e7da60dafdffb3658f80e6708d19f0 # Parent 3c4fc62d494cb2bd5e252b79820d539fa476132e removed -- new version in HOLCF/IOA/NTP; diff -r 3c4fc62d494c -r 3e8d80cdd3e7 src/HOL/IOA/NTP/Abschannel.ML --- a/src/HOL/IOA/NTP/Abschannel.ML Wed Apr 30 11:51:28 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,53 +0,0 @@ -(* Title: HOL/IOA/NTP/Abschannel.ML - ID: $Id$ - Author: Tobias Nipkow and 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 3c4fc62d494c -r 3e8d80cdd3e7 src/HOL/IOA/NTP/Abschannel.thy --- a/src/HOL/IOA/NTP/Abschannel.thy Wed Apr 30 11:51:28 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,103 +0,0 @@ -(* Title: HOL/IOA/NTP/Abschannel.thy - ID: $Id$ - Author: Tobias Nipkow and Olaf Mueller - Copyright 1994 TU Muenchen - -The (faulty) transmission channel (both directions) -*) - -Abschannel = IOA + Action + - -datatype ('a)act = S('a) | R('a) - -consts - -ch_asig :: 'a act signature - -ch_trans :: ('a act, 'a multiset)transition set - -ch_ioa :: ('a act, 'a multiset)ioa - -rsch_actions :: 'm action => bool act option -srch_actions :: "'m action =>(bool * 'm) act 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 (act) == - case act 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 (act) == - case act 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 3c4fc62d494c -r 3e8d80cdd3e7 src/HOL/IOA/NTP/Action.ML --- a/src/HOL/IOA/NTP/Action.ML Wed Apr 30 11:51:28 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,13 +0,0 @@ -(* 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 3c4fc62d494c -r 3e8d80cdd3e7 src/HOL/IOA/NTP/Action.thy --- a/src/HOL/IOA/NTP/Action.thy Wed Apr 30 11:51:28 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,14 +0,0 @@ -(* 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 3c4fc62d494c -r 3e8d80cdd3e7 src/HOL/IOA/NTP/Correctness.ML --- a/src/HOL/IOA/NTP/Correctness.ML Wed Apr 30 11:51:28 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,115 +0,0 @@ -(* Title: HOL/IOA/NTP/Correctness.ML - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind - Copyright 1994 TU Muenchen - -The main correctness proof: Impl implements Spec -*) - - -open Impl 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, Solve.is_weak_pmap_def] - "is_weak_pmap 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 3c4fc62d494c -r 3e8d80cdd3e7 src/HOL/IOA/NTP/Correctness.thy --- a/src/HOL/IOA/NTP/Correctness.thy Wed Apr 30 11:51:28 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,17 +0,0 @@ -(* 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 = Solve + 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 3c4fc62d494c -r 3e8d80cdd3e7 src/HOL/IOA/NTP/Impl.ML --- a/src/HOL/IOA/NTP/Impl.ML Wed Apr 30 11:51:28 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,344 +0,0 @@ -(* Title: HOL/IOA/NTP/Impl.ML - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind - Copyright 1994 TU Muenchen - -The implementation --- Invariants -*) - - - - -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 3c4fc62d494c -r 3e8d80cdd3e7 src/HOL/IOA/NTP/Impl.thy --- a/src/HOL/IOA/NTP/Impl.thy Wed Apr 30 11:51:28 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,71 +0,0 @@ -(* 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 3c4fc62d494c -r 3e8d80cdd3e7 src/HOL/IOA/NTP/Lemmas.ML --- a/src/HOL/IOA/NTP/Lemmas.ML Wed Apr 30 11:51:28 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,210 +0,0 @@ -(* 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 3c4fc62d494c -r 3e8d80cdd3e7 src/HOL/IOA/NTP/Lemmas.thy --- a/src/HOL/IOA/NTP/Lemmas.thy Wed Apr 30 11:51:28 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -(* Title: HOL/IOA/NTP/Lemmas.thy - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind - Copyright 1994 TU Muenchen - -Arithmetic lemmas -*) - -Lemmas = Arith diff -r 3c4fc62d494c -r 3e8d80cdd3e7 src/HOL/IOA/NTP/Multiset.ML --- a/src/HOL/IOA/NTP/Multiset.ML Wed Apr 30 11:51:28 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,87 +0,0 @@ -(* 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 3c4fc62d494c -r 3e8d80cdd3e7 src/HOL/IOA/NTP/Multiset.thy --- a/src/HOL/IOA/NTP/Multiset.thy Wed Apr 30 11:51:28 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,48 +0,0 @@ -(* 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 3c4fc62d494c -r 3e8d80cdd3e7 src/HOL/IOA/NTP/Packet.ML --- a/src/HOL/IOA/NTP/Packet.ML Wed Apr 30 11:51:28 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,15 +0,0 @@ -(* 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 3c4fc62d494c -r 3e8d80cdd3e7 src/HOL/IOA/NTP/Packet.thy --- a/src/HOL/IOA/NTP/Packet.thy Wed Apr 30 11:51:28 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,23 +0,0 @@ -(* 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 3c4fc62d494c -r 3e8d80cdd3e7 src/HOL/IOA/NTP/ROOT.ML --- a/src/HOL/IOA/NTP/ROOT.ML Wed Apr 30 11:51:28 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,35 +0,0 @@ -(* Title: HOL/IOA/NTP/ROOT.ML - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind - Copyright 1994 TU Muenchen - -This is the ROOT file for the theory of I/O-Automata (NTP subdirectory). -The formalization is by a semantic model of I/O-Automata. -For details see - -@inproceedings{Nipkow-Slind-IOA, -author={Tobias Nipkow and Konrad Slind}, -title={{I/O} Automata in {Isabelle/HOL}}, -booktitle={Proc.\ TYPES Workshop 1994}, -publisher=Springer, -series=LNCS, -note={To appear}} -ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz - -and - -@inproceedings{Mueller-Nipkow, -author={Olaf M\"uller and Tobias Nipkow}, -title={Combining Model Checking and Deduction for {I/O}-Automata}, -booktitle={Proc.\ TACAS Workshop}, -organization={Aarhus University, BRICS report}, -year=1995} -ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz - -Should be executed in the subdirectory HOL/IOA/NTP. -*) - -goals_limit := 1; - -loadpath := [".", "../meta_theory"]; -use_thy "Correctness"; diff -r 3c4fc62d494c -r 3e8d80cdd3e7 src/HOL/IOA/NTP/Read_me --- a/src/HOL/IOA/NTP/Read_me Wed Apr 30 11:51:28 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,182 +0,0 @@ -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 3c4fc62d494c -r 3e8d80cdd3e7 src/HOL/IOA/NTP/Receiver.ML --- a/src/HOL/IOA/NTP/Receiver.ML Wed Apr 30 11:51:28 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,29 +0,0 @@ -(* 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 3c4fc62d494c -r 3e8d80cdd3e7 src/HOL/IOA/NTP/Receiver.thy --- a/src/HOL/IOA/NTP/Receiver.thy Wed Apr 30 11:51:28 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,89 +0,0 @@ -(* 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 3c4fc62d494c -r 3e8d80cdd3e7 src/HOL/IOA/NTP/Sender.ML --- a/src/HOL/IOA/NTP/Sender.ML Wed Apr 30 11:51:28 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,25 +0,0 @@ -(* 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 3c4fc62d494c -r 3e8d80cdd3e7 src/HOL/IOA/NTP/Sender.thy --- a/src/HOL/IOA/NTP/Sender.thy Wed Apr 30 11:51:28 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,85 +0,0 @@ -(* 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 3c4fc62d494c -r 3e8d80cdd3e7 src/HOL/IOA/NTP/Spec.thy --- a/src/HOL/IOA/NTP/Spec.thy Wed Apr 30 11:51:28 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,42 +0,0 @@ -(* 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