--- 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";
-
--- 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
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
--- 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()];
--- 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
--- 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";
--- 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
--- 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);
--- 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
--- 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 --> 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);
--- 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
--- 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<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];
--- 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
--- 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];
--- 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
--- 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";
--- 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,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 ~= []
-
--- 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];
-
-
--- 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
--- 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];
--- 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
--- 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