--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IOA/NTP/Abschannel.ML Thu Apr 13 16:57:18 1995 +0200
@@ -0,0 +1,54 @@
+(* Title: HOL/IOA/NTP/Abschannel.ML
+ ID: $Id$
+ Author: Tobias Nipkow and Olaf Mueller
+ Copyright 1994 TU Muenchen
+
+Derived rules
+*)
+
+open Abschannel;
+
+val abschannel_ss = action_ss addsimps
+ ([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]
+ @ Option.option.simps @ act.simps @ asig_projections @ set_lemmas);
+
+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 abschannel_ss 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 abschannel_ss 1);
+qed"in_rsch_asig";
+
+goal Abschannel.thy "srch_ioa = (srch_asig, {{|}}, srch_trans)";
+by (simp_tac (abschannel_ss addsimps [starts_of_def]) 1);
+qed"srch_ioa_thm";
+
+goal Abschannel.thy "rsch_ioa = (rsch_asig, {{|}}, rsch_trans)";
+by (simp_tac (abschannel_ss addsimps [starts_of_def]) 1);
+qed"rsch_ioa_thm";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IOA/NTP/Abschannel.thy Thu Apr 13 16:57:18 1995 +0200
@@ -0,0 +1,103 @@
+(* 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 + Multiset +
+
+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
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IOA/NTP/Action.ML Thu Apr 13 16:57:18 1995 +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 HOL_ss 1);
+
+val action_ss = arith_ss addcongs [result()] addsimps Action.action.simps;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IOA/NTP/Action.thy Thu Apr 13 16:57:18 1995 +0200
@@ -0,0 +1,14 @@
+(* Title: HOL/IOA/NTP/Action.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+The set of all actions of the system
+*)
+
+Action = Packet +
+datatype 'm action = S_msg ('m) | R_msg ('m)
+ | S_pkt ('m packet) | R_pkt ('m packet)
+ | S_ack (bool) | R_ack (bool)
+ | C_m_s | C_m_r | C_r_s | C_r_r ('m)
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IOA/NTP/Correctness.ML Thu Apr 13 16:57:18 1995 +0200
@@ -0,0 +1,116 @@
+(* 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;
+open Spec;
+
+val hom_ss = impl_ss;
+val hom_ioas = [Spec.ioa_def, Spec.trans_def,
+ Sender.sender_trans_def,Receiver.receiver_trans_def]
+ @ impl_ioas;
+
+val hom_ss' = hom_ss addsimps hom_ioas;
+
+val impl_asigs = [Sender.sender_asig_def,Receiver.receiver_asig_def,
+ Abschannel.srch_asig_def,Abschannel.rsch_asig_def];
+
+
+(* 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 (hom_ss addcongs [if_weak_cong]
+ 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 (action_ss addsimps
+ (actions_def :: asig_projections @ set_lemmas))));
+ (* 2 *)
+ by (simp_tac (hom_ss addsimps impl_ioas) 1);
+ by (simp_tac (hom_ss addsimps impl_asigs) 1);
+ by(simp_tac (hom_ss addsimps ([asig_of_par, asig_comp_def]
+ @ asig_projections)) 1);
+ by (simp_tac abschannel_ss 1);
+ (* 1 *)
+ by (simp_tac (hom_ss addsimps impl_ioas) 1);
+ by (simp_tac (hom_ss addsimps impl_asigs) 1);
+ by(simp_tac (hom_ss addsimps ([asig_of_par, asig_comp_def]
+ @ asig_projections)) 1);
+ by (simp_tac abschannel_ss 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 (hom_ss addsimps
+ (Correctness.hom_def::[cancel_restrict,externals_lemma])) 1);
+br conjI 1;
+by(simp_tac (hom_ss addsimps impl_ioas) 1);
+br ballI 1;
+bd CollectD 1;
+by(asm_simp_tac (hom_ss addsimps sels) 1);
+by(REPEAT(rtac allI 1));
+br imp_conj_lemma 1; (* from lemmas.ML *)
+by(Action.action.induct_tac "a" 1);
+by(asm_simp_tac (hom_ss' setloop (split_tac [expand_if])) 1);
+by(forward_tac [inv4] 1);
+by(asm_full_simp_tac (hom_ss addsimps
+ [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1);
+by(simp_tac hom_ss' 1);
+by(simp_tac hom_ss' 1);
+by(simp_tac hom_ss' 1);
+by(simp_tac hom_ss' 1);
+by(simp_tac hom_ss' 1);
+by(simp_tac hom_ss' 1);
+by(simp_tac hom_ss' 1);
+
+by(asm_simp_tac hom_ss' 1);
+by(forward_tac [inv4] 1);
+by(forward_tac [inv2] 1);
+be disjE 1;
+by(asm_simp_tac hom_ss 1);
+by(asm_full_simp_tac (hom_ss addsimps
+ [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1);
+
+by(asm_simp_tac hom_ss' 1);
+by(forward_tac [inv2] 1);
+be disjE 1;
+
+by(forward_tac [inv3] 1);
+by(case_tac "sq(sen(s))=[]" 1);
+
+by(asm_full_simp_tac hom_ss' 1);
+by(fast_tac (HOL_cs addSDs [add_leD1 RS leD]) 1);
+
+by(case_tac "m = hd(sq(sen(s)))" 1);
+
+by(asm_full_simp_tac (hom_ss addsimps
+ [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1);
+
+by(asm_full_simp_tac hom_ss 1);
+by(fast_tac (HOL_cs addSDs [add_leD1 RS leD]) 1);
+
+by(asm_full_simp_tac hom_ss 1);
+result();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IOA/NTP/Correctness.thy Thu Apr 13 16:57:18 1995 +0200
@@ -0,0 +1,21 @@
+(* 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 +
+
+consts
+
+hom :: "'m impl_state => 'm list"
+
+defs
+
+hom_def
+"hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s) \
+\ else ttl(sq(sen s)))"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IOA/NTP/Impl.ML Thu Apr 13 16:57:18 1995 +0200
@@ -0,0 +1,408 @@
+(* Title: HOL/IOA/NTP/Impl.ML
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+The implementation --- Invariants
+*)
+
+open Abschannel;
+
+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,
+ Abschannel.srch_trans_def, Abschannel.rsch_trans_def];
+
+
+val impl_ss = merge_ss(action_ss,list_ss)
+ addcongs [let_weak_cong]
+ addsimps [Let_def, ioa_triple_proj, starts_of_par, trans_of_par4,
+ in_sender_asig, in_receiver_asig, in_srch_asig,
+ in_rsch_asig, count_addm_simp, count_delm_simp,
+ Multiset.countm_empty_def, Multiset.delm_empty_def,
+ (* Multiset.count_def, *) count_empty,
+ Packet.hdr_def, Packet.msg_def];
+
+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 (HOL_ss addsimps
+ [Impl.sen_def,Impl.rec_def,Impl.srch_def,Impl.rsch_def]) 1);
+val impl_ss = impl_ss 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 impl_ss));
+val impl_ss = impl_ss addsimps [result()];
+
+
+(* INVARIANT 1 *)
+val ss = impl_ss addcongs [if_weak_cong] addsimps transitions;
+val abs_ss= merge_ss(ss,abschannel_ss);
+
+goalw Impl.thy impl_ioas "invariant impl_ioa inv1";
+br invariantI 1;
+by(asm_full_simp_tac (impl_ss addsimps
+ [Impl.inv1_def, Impl.hdr_sum_def,
+ Sender.srcvd_def, Sender.ssent_def,
+ Receiver.rsent_def,Receiver.rrcvd_def]) 1);
+
+by(simp_tac (HOL_ss addsimps [fork_lemma,Impl.inv1_def]) 1);
+
+(* Split proof in two *)
+by (rtac conjI 1);
+
+(* First half *)
+by(asm_full_simp_tac (impl_ss addsimps [Impl.inv1_def]) 1);
+br Action.action.induct 1;
+
+val tac = asm_simp_tac (ss addcongs [conj_cong]
+ addsimps [Suc_pred_lemma]
+ setloop (split_tac [expand_if]));
+val tac_abs = asm_simp_tac (abs_ss addcongs [conj_cong]
+ addsimps [Suc_pred_lemma]
+ setloop (split_tac [expand_if]));
+by (EVERY1[tac, tac, tac, tac]);
+by (tac 1);
+by (tac_abs 1);
+
+(* 5 + 1 *)
+
+by (tac 1);
+by (tac_abs 1);
+
+(* 4 + 1 *)
+by(EVERY1[tac, tac, tac, tac]);
+
+
+(* Now the other half *)
+by(asm_full_simp_tac (impl_ss addsimps [Impl.inv1_def]) 1);
+br Action.action.induct 1;
+by(EVERY1[tac, tac]);
+
+(* detour 1 *)
+by (tac 1);
+by (tac_abs 1);
+by (rtac impI 1);
+by (REPEAT (etac conjE 1));
+by (asm_simp_tac (impl_ss addsimps [Impl.hdr_sum_def, Multiset.count_def,
+ Multiset.countm_nonempty_def]
+ setloop (split_tac [expand_if])) 1);
+(* detour 2 *)
+by (tac 1);
+by (tac_abs 1);
+by (rtac impI 1);
+by (REPEAT (etac conjE 1));
+by (asm_full_simp_tac (impl_ss 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 (HOL_ss addsimps [Multiset.count_def]) 1);
+
+by (rtac impI 1);
+by (asm_full_simp_tac (HOL_ss addsimps [neg_flip]) 1);
+by (hyp_subst_tac 1);
+by (rtac countm_spurious_delm 1);
+by (simp_tac HOL_ss 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 (impl_ss addsimps
+ (Impl.inv2_def :: (receiver_projections
+ @ sender_projections @ impl_ioas))) 1);
+
+ by (asm_simp_tac (impl_ss addsimps impl_ioas) 1);
+ by (Action.action.induct_tac "a" 1);
+
+ (* 10 cases. First 4 are simple, since state doesn't change wrt. invariant *)
+ (* 10 *)
+ by (asm_simp_tac (impl_ss addsimps (Impl.inv2_def::transitions)) 1);
+ (* 9 *)
+ by (asm_simp_tac (impl_ss addsimps (Impl.inv2_def::transitions)) 1);
+ (* 8 *)
+ by (asm_simp_tac (impl_ss addsimps (Impl.inv2_def::transitions)) 2);
+ (* 7 *)
+ by (asm_simp_tac (impl_ss addsimps (Impl.inv2_def::transitions)) 3);
+ (* 6 *)
+ by(forward_tac [rewrite_rule [Impl.inv1_def]
+ (inv1 RS invariantE) RS conjunct1] 1);
+ by (asm_full_simp_tac (impl_ss addsimps [leq_imp_leq_suc,Impl.inv2_def]
+ addsimps transitions) 1);
+ (* 5 *)
+ by (asm_full_simp_tac (impl_ss addsimps [leq_imp_leq_suc,Impl.inv2_def]
+ addsimps transitions) 1);
+ (* 4 *)
+ by (forward_tac [rewrite_rule [Impl.inv1_def]
+ (inv1 RS invariantE) RS conjunct1] 1);
+ by (asm_full_simp_tac (impl_ss addsimps [Impl.inv2_def]
+ addsimps transitions) 1);
+ by (fast_tac (HOL_cs addDs [add_leD1,leD]) 1);
+
+ (* 3 *)
+ by (forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE)] 1);
+
+ by (asm_full_simp_tac (impl_ss addsimps
+ (Impl.inv2_def::transitions)) 1);
+ by (fold_tac [rewrite_rule [Packet.hdr_def]Impl.hdr_sum_def]);
+ by (fast_tac (HOL_cs addDs [add_leD1,leD]) 1);
+
+ (* 2 *)
+ by (asm_full_simp_tac (impl_ss addsimps
+ (Impl.inv2_def::transitions)) 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 HOL_ss 1);
+
+ (* 1 *)
+ by (asm_full_simp_tac (impl_ss addsimps
+ (Impl.inv2_def::transitions)) 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 HOL_ss 1);
+qed "inv2";
+
+
+(* INVARIANT 3 *)
+goal Impl.thy "invariant impl_ioa inv3";
+
+ by (rtac invariantI 1);
+ (* Base case *)
+ by (asm_full_simp_tac (impl_ss addsimps
+ (Impl.inv3_def :: (receiver_projections
+ @ sender_projections @ impl_ioas))) 1);
+
+ by (asm_simp_tac (impl_ss addsimps impl_ioas) 1);
+ by (Action.action.induct_tac "a" 1);
+
+ (* 10 *)
+ by (asm_full_simp_tac (impl_ss addsimps
+ (append_cons::not_hd_append::Impl.inv3_def::transitions)
+ setloop (split_tac [expand_if])) 1);
+
+ (* 9 *)
+ by (asm_full_simp_tac (impl_ss addsimps
+ (append_cons::not_hd_append::Impl.inv3_def::transitions)
+ setloop (split_tac [expand_if])) 1);
+
+ (* 8 *)
+ by (asm_full_simp_tac (impl_ss addsimps
+ (append_cons::not_hd_append::Impl.inv3_def::transitions)
+ setloop (split_tac [expand_if])) 1);
+ by (tac_abs 1);
+ by (strip_tac 1 THEN REPEAT (etac conjE 1));
+ by (asm_full_simp_tac (HOL_ss addsimps [cons_imp_not_null]) 1);
+
+
+ by (hyp_subst_tac 1);
+ by (etac exE 1);
+ by (asm_full_simp_tac list_ss 1);
+
+ (* 7 *)
+ by (asm_full_simp_tac (impl_ss addsimps
+ (Suc_pred_lemma::append_cons::not_hd_append::Impl.inv3_def::transitions)
+ setloop (split_tac [expand_if])) 1);
+ by (tac_abs 1);
+ by (fast_tac HOL_cs 1);
+
+ (* 6 *)
+ by (asm_full_simp_tac (impl_ss addsimps
+ (append_cons::not_hd_append::Impl.inv3_def::transitions)
+ setloop (split_tac [expand_if])) 1);
+ (* 5 *)
+ by (asm_full_simp_tac (impl_ss addsimps
+ (append_cons::not_hd_append::Impl.inv3_def::transitions)
+ setloop (split_tac [expand_if])) 1);
+
+ (* 4 *)
+ by (asm_full_simp_tac (impl_ss addsimps
+ (append_cons::not_hd_append::Impl.inv3_def::transitions)
+ setloop (split_tac [expand_if])) 1);
+
+ (* 3 *)
+ by (asm_full_simp_tac (impl_ss addsimps
+ (append_cons::not_hd_append::Impl.inv3_def::transitions)
+ setloop (split_tac [expand_if])) 1);
+
+ (* 2 *)
+ by (asm_full_simp_tac (impl_ss addsimps transitions) 1);
+ by (simp_tac (HOL_ss addsimps [Impl.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 list_ss 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 [Impl.inv1_def]
+ (inv1 RS invariantE) RS conjunct2] 1);
+ by (asm_full_simp_tac (list_ss addsimps
+ [Impl.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 (list_ss addsimps [Packet.hdr_def]) 1);
+ by (rtac countm_props 1);
+ by (simp_tac (list_ss addsimps [Packet.hdr_def]) 1);
+ by (assume_tac 1);
+
+
+ (* 1 *)
+ by (asm_full_simp_tac (impl_ss addsimps
+ (append_cons::not_hd_append::Impl.inv3_def::transitions)
+ setloop (split_tac [expand_if])) 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 list_ss 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 (impl_ss addsimps
+ (Impl.inv4_def :: (receiver_projections
+ @ sender_projections @ impl_ioas))) 1);
+
+ by (asm_simp_tac (impl_ss addsimps impl_ioas) 1);
+ by (Action.action.induct_tac "a" 1);
+
+ (* 10 *)
+ by (asm_full_simp_tac (impl_ss addsimps
+ (append_cons::Impl.inv4_def::transitions)
+ setloop (split_tac [expand_if])) 1);
+
+ (* 9 *)
+ by (asm_full_simp_tac (impl_ss addsimps
+ (append_cons::Impl.inv4_def::transitions)
+ setloop (split_tac [expand_if])) 1);
+
+ (* 8 *)
+ by (asm_full_simp_tac (impl_ss addsimps
+ (append_cons::Impl.inv4_def::transitions)
+ setloop (split_tac [expand_if])) 1);
+ (* 7 *)
+ by (asm_full_simp_tac (impl_ss addsimps
+ (append_cons::Impl.inv4_def::transitions)
+ setloop (split_tac [expand_if])) 1);
+
+ (* 6 *)
+ by (asm_full_simp_tac (impl_ss addsimps
+ (append_cons::Impl.inv4_def::transitions)
+ setloop (split_tac [expand_if])) 1);
+
+ (* 5 *)
+ by (asm_full_simp_tac (impl_ss addsimps
+ (append_cons::Impl.inv4_def::transitions)
+ setloop (split_tac [expand_if])) 1);
+
+ (* 4 *)
+ by (asm_full_simp_tac (impl_ss addsimps
+ (append_cons::Impl.inv4_def::transitions)
+ setloop (split_tac [expand_if])) 1);
+
+ (* 3 *)
+ by (asm_full_simp_tac (impl_ss addsimps
+ (append_cons::Impl.inv4_def::transitions)
+ setloop (split_tac [expand_if])) 1);
+
+ (* 2 *)
+ by (asm_full_simp_tac (impl_ss addsimps
+ (append_cons::Impl.inv4_def::transitions)
+ setloop (split_tac [expand_if])) 1);
+
+ by (strip_tac 1 THEN REPEAT (etac conjE 1));
+ by(forward_tac [rewrite_rule [Impl.inv2_def]
+ (inv2 RS invariantE)] 1);
+
+ by (asm_full_simp_tac list_ss 1);
+
+ (* 1 *)
+ by (asm_full_simp_tac (impl_ss addsimps
+ (append_cons::Impl.inv4_def::transitions)
+ setloop (split_tac [expand_if])) 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 list_ss 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 list_ss 1);
+ by (asm_full_simp_tac arith_ss 1);
+qed "inv4";
+
+
+
+(* rebind them *)
+
+val inv1 = rewrite_rule [Impl.inv1_def] (inv1 RS invariantE);
+val inv2 = rewrite_rule [Impl.inv2_def] (inv2 RS invariantE);
+val inv3 = rewrite_rule [Impl.inv3_def] (inv3 RS invariantE);
+val inv4 = rewrite_rule [Impl.inv4_def] (inv4 RS invariantE);
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IOA/NTP/Impl.thy Thu Apr 13 16:57:18 1995 +0200
@@ -0,0 +1,71 @@
+(* Title: HOL/IOA/NTP/Impl.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+The implementation
+*)
+
+Impl = Sender + Receiver + Abschannel +
+
+types
+
+'m impl_state
+= "'m sender_state * 'm receiver_state * 'm packet multiset * bool multiset"
+(* sender_state * receiver_state * srch_state * rsch_state *)
+
+
+consts
+ impl_ioa :: "('m action, 'm impl_state)ioa"
+ sen :: "'m impl_state => 'm sender_state"
+ rec :: "'m impl_state => 'm receiver_state"
+ srch :: "'m impl_state => 'm packet multiset"
+ rsch :: "'m impl_state => bool multiset"
+ inv1, inv2,
+ inv3, inv4 :: "'m impl_state => bool"
+ hdr_sum :: "'m packet multiset => bool => nat"
+
+defs
+
+ impl_def
+ "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
+
+ sen_def "sen == fst"
+ rec_def "rec == fst o snd"
+ srch_def "srch == fst o snd o snd"
+ rsch_def "rsch == snd o snd o snd"
+
+hdr_sum_def
+ "hdr_sum M b == countm M (%pkt.hdr(pkt) = b)"
+
+(* Lemma 5.1 *)
+inv1_def
+ "inv1(s) == \
+ \ (!b. count (rsent(rec s)) b = count (srcvd(sen s)) b + count (rsch s) b) \
+ \ & (!b. count (ssent(sen s)) b \
+ \ = hdr_sum (rrcvd(rec s)) b + hdr_sum (srch s) b)"
+
+(* Lemma 5.2 *)
+ inv2_def "inv2(s) == \
+\ (rbit(rec(s)) = sbit(sen(s)) & \
+\ ssending(sen(s)) & \
+\ count (rsent(rec s)) (~sbit(sen s)) <= count (ssent(sen s)) (~sbit(sen s)) &\
+\ count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s))) \
+\ | \
+\ (rbit(rec(s)) = (~sbit(sen(s))) & \
+\ rsending(rec(s)) & \
+\ count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s)) &\
+\ count (rsent(rec s)) (sbit(sen s)) <= count (ssent(sen s)) (sbit(sen s)))"
+
+(* Lemma 5.3 *)
+ inv3_def "inv3(s) == \
+\ rbit(rec(s)) = sbit(sen(s)) \
+\ --> (!m. sq(sen(s))=[] | m ~= hd(sq(sen(s))) \
+\ --> count (rrcvd(rec s)) (sbit(sen(s)),m) \
+\ + count (srch s) (sbit(sen(s)),m) \
+\ <= count (rsent(rec s)) (~sbit(sen s)))"
+
+(* Lemma 5.4 *)
+ inv4_def "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) --> sq(sen(s)) ~= []"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IOA/NTP/Lemmas.ML Thu Apr 13 16:57:18 1995 +0200
@@ -0,0 +1,239 @@
+(* 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 (HOL_cs addDs prems) 1);
+qed "imp_conj_lemma";
+
+goal HOL.thy "(P --> (? x. Q(x))) = (? x. P --> Q(x))";
+ by(fast_tac HOL_cs 1);
+qed "imp_ex_equiv";
+
+goal HOL.thy "(A --> B & C) = ((A --> B) & (A --> C))";
+ by (fast_tac HOL_cs 1);
+qed "fork_lemma";
+
+goal HOL.thy "((A --> B) & (C --> B)) = ((A | C) --> B)";
+ by (fast_tac HOL_cs 1);
+qed "imp_or_lem";
+
+goal HOL.thy "(X = (~ Y)) = ((~X) = Y)";
+ by (fast_tac HOL_cs 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 HOL_cs 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 HOL_cs 1);
+qed "imp_false_decompose";
+
+
+(* Sets *)
+val set_lemmas =
+ map (fn s => prove_goal Set.thy s (fn _ => [fast_tac set_cs 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 arith_ss 1));
+val Suc_pred_lemma = store_thm("Suc_pred_lemma", result() RS mp);
+
+goal Arith.thy "x <= y --> x <= Suc(y)";
+ by (rtac impI 1);
+ by (rtac (le_eq_less_or_eq RS iffD2) 1);
+ by (rtac disjI1 1);
+ by (dtac (le_eq_less_or_eq RS iffD1) 1);
+ by (etac disjE 1);
+ by (etac less_SucI 1);
+ by (asm_simp_tac nat_ss 1);
+val leq_imp_leq_suc = store_thm("leq_imp_leq_suc", result() RS mp);
+
+(* Same as previous! *)
+goal Arith.thy "(x::nat)<=y --> x<=Suc(y)";
+ by (simp_tac (arith_ss addsimps [le_eq_less_or_eq]) 1);
+qed "leq_suc";
+
+goal Arith.thy "((m::nat) + n = m + p) = (n = p)";
+ by (nat_ind_tac "m" 1);
+ by (simp_tac arith_ss 1);
+ by (asm_simp_tac arith_ss 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 arith_ss 1);
+ by (asm_simp_tac arith_ss 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 arith_ss 1);
+ by (asm_simp_tac arith_ss 1);
+ by (fast_tac HOL_cs 1);
+qed "nonzero_is_succ";
+
+goal Arith.thy "(m::nat) < n --> m + p < n + p";
+ by (nat_ind_tac "p" 1);
+ by (simp_tac arith_ss 1);
+ by (asm_simp_tac arith_ss 1);
+qed "less_add_same_less";
+
+goal Arith.thy "(x::nat)<= y --> x<=y+k";
+ by (nat_ind_tac "k" 1);
+ by (simp_tac arith_ss 1);
+ by (asm_full_simp_tac (arith_ss addsimps [leq_suc]) 1);
+qed "leq_add_leq";
+
+goal Arith.thy "(x::nat) + y <= z --> x <= z";
+ by (nat_ind_tac "y" 1);
+ by (simp_tac arith_ss 1);
+ by (asm_simp_tac arith_ss 1);
+ by (rtac impI 1);
+ by (dtac Suc_leD 1);
+ by (fast_tac HOL_cs 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 (arith_ss addsimps [le_eq_less_or_eq]) 1);
+ by (safe_tac HOL_cs);
+ 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 (HOL_ss 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 arith_ss 1);
+ by (rtac iffI 1);
+ by (asm_full_simp_tac arith_ss 1);
+ by (fast_tac HOL_cs 1);
+qed "suc_not_zero";
+
+goal Arith.thy "Suc(x) <= y --> (? z. y = Suc(z))";
+ by (rtac impI 1);
+ by (asm_full_simp_tac (arith_ss addsimps [le_eq_less_or_eq]) 1);
+ by (safe_tac HOL_cs);
+ by (fast_tac HOL_cs 2);
+ by (asm_simp_tac (arith_ss addsimps [suc_not_zero]) 1);
+ by (rtac ccontr 1);
+ by (asm_full_simp_tac (arith_ss addsimps [suc_not_zero]) 1);
+ by (hyp_subst_tac 1);
+ by (asm_full_simp_tac arith_ss 1);
+qed "suc_leq_suc";
+
+goal Arith.thy "~0<n --> n = 0";
+ by (nat_ind_tac "n" 1);
+ by (asm_simp_tac arith_ss 1);
+ by (safe_tac HOL_cs);
+ by (asm_full_simp_tac arith_ss 1);
+ by (asm_full_simp_tac arith_ss 1);
+qed "zero_eq";
+
+goal Arith.thy "x < Suc(y) --> x<=y";
+ by (nat_ind_tac "n" 1);
+ by (asm_simp_tac arith_ss 1);
+ by (safe_tac HOL_cs);
+ 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 arith_ss 1);
+ by (asm_simp_tac arith_ss 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 arith_ss 1);
+ by (asm_simp_tac arith_ss 1);
+qed "pred_suc";
+
+goal Arith.thy "(x ~= 0) = (0<x)";
+ by (nat_ind_tac "x" 1);
+ by (simp_tac arith_ss 1);
+ by (asm_simp_tac arith_ss 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 arith_ss 1);
+ by (simp_tac (arith_ss addsimps
+ [Suc_le_mono, le_refl RS (leq_add_leq RS mp)]) 1);
+qed "plus_leq_lem";
+
+(* Lists *)
+
+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";
+
+goal List.thy "(L = (x#rst)) --> (L = []) --> P";
+ by (simp_tac list_ss 1);
+qed "list_cases";
+
+goal List.thy "(? L2. L1 = x#L2) --> (L1 ~= [])";
+ by (strip_tac 1);
+ by (etac exE 1);
+ by (asm_simp_tac list_ss 1);
+qed "cons_imp_not_null";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IOA/NTP/Lemmas.thy Thu Apr 13 16:57:18 1995 +0200
@@ -0,0 +1,9 @@
+(* Title: HOL/IOA/NTP/Lemmas.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+Arithmetic lemmas
+*)
+
+Lemmas = Arith
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IOA/NTP/Multiset.ML Thu Apr 13 16:57:18 1995 +0200
@@ -0,0 +1,84 @@
+(* 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 (arith_ss 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 (arith_ss addsimps [count_addm_simp]
+ setloop (split_tac [expand_if])) 1);
+ by (rtac impI 1);
+ by (rtac (le_refl RS (leq_suc RS mp)) 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 (arith_ss
+ addsimps [Multiset.delm_empty_def,Multiset.countm_empty_def]
+ setloop (split_tac [expand_if])) 1);
+ by (asm_full_simp_tac (arith_ss
+ addsimps [Multiset.delm_nonempty_def,
+ Multiset.countm_nonempty_def]
+ setloop (split_tac [expand_if])) 1);
+ by (safe_tac HOL_cs);
+ by (asm_full_simp_tac HOL_ss 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 (arith_ss addsimps [Multiset.countm_empty_def]) 1);
+ by (simp_tac (arith_ss addsimps[Multiset.countm_nonempty_def]) 1);
+ by (etac (less_eq_add_cong RS mp RS mp) 1);
+ by (asm_full_simp_tac (arith_ss 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 (arith_ss addsimps [Multiset.delm_empty_def,
+ Multiset.countm_empty_def]) 1);
+ by (asm_simp_tac (arith_ss 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 (arith_ss addsimps
+ [Multiset.delm_empty_def,Multiset.count_def,
+ Multiset.countm_empty_def]) 1);
+ by (asm_simp_tac (arith_ss 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 (arith_ss addsimps
+ [Multiset.delm_empty_def,
+ Multiset.countm_empty_def]) 1);
+ by (asm_simp_tac (arith_ss 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";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IOA/NTP/Multiset.thy Thu Apr 13 16:57:18 1995 +0200
@@ -0,0 +1,48 @@
+(* Title: HOL/IOA/NTP/Multiset.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+Axiomatic multisets.
+Should be done as a subtype and moved to a global place.
+*)
+
+Multiset = Arith + "Lemmas" +
+
+types
+
+ 'a multiset
+
+arities
+
+ multiset :: (term) term
+
+consts
+
+ "{|}" :: "'a multiset" ("{|}")
+ addm :: "['a multiset, 'a] => 'a multiset"
+ delm :: "['a multiset, 'a] => 'a multiset"
+ countm :: "['a multiset, 'a => bool] => nat"
+ count :: "['a multiset, 'a] => nat"
+
+rules
+
+delm_empty_def
+ "delm {|} x = {|}"
+
+delm_nonempty_def
+ "delm (addm M x) y == (if x=y then M else addm (delm M y) x)"
+
+countm_empty_def
+ "countm {|} P == 0"
+
+countm_nonempty_def
+ "countm (addm M x) P == countm M P + (if P x then Suc 0 else 0)"
+
+count_def
+ "count M x == countm M (%y.y = x)"
+
+induction
+ "[| P({|}); !!M x. P(M) ==> P(addm M x) |] ==> P(M)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IOA/NTP/Packet.ML Thu Apr 13 16:57:18 1995 +0200
@@ -0,0 +1,13 @@
+(* 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 (HOL_ss addsimps [Packet.hdr_def]) 1);
+qed "eq_packet_imp_eq_hdr";
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IOA/NTP/Packet.thy Thu Apr 13 16:57:18 1995 +0200
@@ -0,0 +1,25 @@
+(* Title: HOL/IOA/NTP/Packet.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+Packets
+*)
+
+Packet = Arith +
+
+types
+
+ 'msg packet = "bool * 'msg"
+
+consts
+
+ hdr :: "'msg packet => bool"
+ msg :: "'msg packet => 'msg"
+
+defs
+
+ hdr_def "hdr == fst"
+ msg_def "msg == snd"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IOA/NTP/Read_me Thu Apr 13 16:57:18 1995 +0200
@@ -0,0 +1,182 @@
+Isabelle Verification of a protocol using IOA.
+
+------------------------------------------------------------------------------
+The theory structure looks like this picture:
+
+ Correctness
+
+ Impl
+
+Sender Receiver Channels Spec
+
+ Action IOA Multisets
+
+ Packet List
+
+ Arith
+
+------------------------------------------------------------------------------
+
+The System.
+
+The system being proved correct is a parallel composition of 4 processes:
+
+ Sender || Schannel || Receiver || Rchannel
+
+Accordingly, the system state is a 4-tuple:
+
+ (Sender_state, Schannel_state, Receiver_state, Rchannel_state)
+
+------------------------------------------------------------------------------
+Packets.
+
+The objects going over the medium from Sender to Receiver are modelled
+with the type
+
+ 'm packet = bool * 'm
+
+This expresses that messages (modelled by polymorphic type "'m") are
+sent with a single header bit. Packet fields are accessed by
+
+ hdr<b,m> = b
+ mesg<b,m> = m
+------------------------------------------------------------------------------
+
+The Sender.
+
+The state of the process "Sender" is a 5-tuple:
+
+ 1. messages : 'm list (* sq *)
+ 2. sent : bool multiset (* ssent *)
+ 3. received : bool multiset (* srcvd *)
+ 4. header : bool (* sbit *)
+ 5. mode : bool (* ssending *)
+
+
+The Receiver.
+
+The state of the process "Receiver" is a 5-tuple:
+
+ 1. messages : 'm list (* rq *)
+ 2. replies : bool multiset (* rsent *)
+ 3. received : 'm packet multiset (* rrcvd *)
+ 4. header : bool (* rbit *)
+ 5. mode : bool (* rsending *)
+
+
+The Channels.
+
+The Sender and Receiver each have a proprietary channel, named
+"Schannel" and "Rchannel" respectively. The messages sent by the Sender
+and Receiver are never lost, but the channels may mix them
+up. Accordingly, multisets are used in modelling the state of the
+channels. The state of "Schannel" is modelled with the following type:
+
+ 'm packet multiset
+
+The state of "Rchannel" is modelled with the following type:
+
+ bool multiset
+
+This expresses that replies from the Receiver are just one bit.
+
+Both Channels are instances of an abstract channel, that is modelled with
+the type
+
+ 'a multiset.
+
+------------------------------------------------------------------------------
+
+The events.
+
+An `execution' of the system is modelled by a sequence of
+
+ <system_state, action, system_state>
+
+transitions. The actions, or events, of the system are described by the
+following ML-style datatype declaration:
+
+ 'm action = S_msg ('m) (* Rqt for Sender to send mesg *)
+ | R_msg ('m) (* Mesg taken from Receiver's queue *)
+ | S_pkt_sr ('m packet) (* Packet arrives in Schannel *)
+ | R_pkt_sr ('m packet) (* Packet leaves Schannel *)
+ | S_pkt_rs (bool) (* Packet arrives in Rchannel *)
+ | R_pkt_rs (bool) (* Packet leaves Rchannel *)
+ | C_m_s (* Change mode in Sender *)
+ | C_m_r (* Change mode in Receiver *)
+ | C_r_s (* Change round in Sender *)
+ | C_r_r ('m) (* Change round in Receiver *)
+
+------------------------------------------------------------------------------
+
+The Specification.
+
+The abstract description of system behaviour is given by defining an
+IO/automaton named "Spec". The state of Spec is a message queue,
+modelled as an "'m list". The only actions performed in the abstract
+system are: "S_msg(m)" (putting message "m" at the end of the queue);
+and "R_msg(m)" (taking message "m" from the head of the queue).
+
+
+------------------------------------------------------------------------------
+
+The Verification.
+
+The verification proceeds by showing that a certain mapping ("hom") from
+the concrete system state to the abstract system state is a `weak
+possibilities map` from "Impl" to "Spec".
+
+
+ hom : (S_state * Sch_state * R_state * Rch_state) -> queue
+
+The verification depends on several system invariants that relate the
+states of the 4 processes. These invariants must hold in all reachable
+states of the system. These invariants are difficult to make sense of;
+however, we attempt to give loose English paraphrases of them.
+
+Invariant 1.
+
+This expresses that no packets from the Receiver to the Sender are
+dropped by Rchannel. The analogous statement for Schannel is also true.
+
+ !b. R.replies b = S.received b + Rch b
+ /\
+ !pkt. S.sent(hdr(pkt)) = R.received(hdr(b)) + Sch(pkt)
+
+
+Invariant 2.
+
+This expresses a complicated relationship about how many messages are
+sent and header bits.
+
+ R.header = S.header
+ /\ S.mode = SENDING
+ /\ R.replies (flip S.header) <= S.sent (flip S.header)
+ /\ S.sent (flip S.header) <= R.replies header
+ OR
+ R.header = flip S.header
+ /\ R.mode = SENDING
+ /\ S.sent (flip S.header) <= R.replies S.header
+ /\ R.replies S.header <= S.sent S.header
+
+
+Invariant 3.
+
+The number of incoming messages in the Receiver plus the number of those
+messages in transit (in Schannel) is not greater than the number of
+replies, provided the message isn't current and the header bits agree.
+
+ let mesg = <S.header, m>
+ in
+ R.header = S.header
+ ==>
+ !m. (S.messages = [] \/ m ~= hd S.messages)
+ ==> R.received mesg + Sch mesg <= R.replies (flip S.header)
+
+
+Invariant 4.
+
+If the headers are opposite, then the Sender queue has a message in it.
+
+ R.header = flip S.header ==> S.messages ~= []
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IOA/NTP/Receiver.ML Thu Apr 13 16:57:18 1995 +0200
@@ -0,0 +1,30 @@
+(* 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 (action_ss addsimps
+ (Receiver.receiver_asig_def :: actions_def ::
+ asig_projections @ set_lemmas)) 1);
+qed "in_receiver_asig";
+
+val receiver_projections =
+ [Receiver.rq_def,
+ Receiver.rsent_def,
+ Receiver.rrcvd_def,
+ Receiver.rbit_def,
+ Receiver.rsending_def];
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IOA/NTP/Receiver.thy Thu Apr 13 16:57:18 1995 +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 + Multiset +
+
+types
+
+'m receiver_state
+= "'m list * bool multiset * 'm packet multiset * bool * bool"
+(* messages #replies #received header mode *)
+
+consts
+
+ receiver_asig :: "'m action signature"
+ receiver_trans:: "('m action, 'm receiver_state)transition set"
+ receiver_ioa :: "('m action, 'm receiver_state)ioa"
+ rq :: "'m receiver_state => 'm list"
+ rsent :: "'m receiver_state => bool multiset"
+ rrcvd :: "'m receiver_state => 'm packet multiset"
+ rbit :: "'m receiver_state => bool"
+ rsending :: "'m receiver_state => bool"
+
+defs
+
+rq_def "rq == fst"
+rsent_def "rsent == fst o snd"
+rrcvd_def "rrcvd == fst o snd o snd"
+rbit_def "rbit == fst o snd o snd o snd"
+rsending_def "rsending == snd o snd o snd o snd"
+
+receiver_asig_def "receiver_asig == \
+\ (UN pkt. {R_pkt(pkt)}, \
+\ (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}), \
+\ insert C_m_r (UN m. {C_r_r(m)}))"
+
+receiver_trans_def "receiver_trans == \
+\ {tr. let s = fst(tr); \
+\ t = snd(snd(tr)) \
+\ in \
+\ case fst(snd(tr)) \
+\ of \
+\ S_msg(m) => False | \
+\ R_msg(m) => rq(s) = (m # rq(t)) & \
+\ rsent(t)=rsent(s) & \
+\ rrcvd(t)=rrcvd(s) & \
+\ rbit(t)=rbit(s) & \
+\ rsending(t)=rsending(s) | \
+\ S_pkt(pkt) => False | \
+\ R_pkt(pkt) => rq(t) = rq(s) & \
+\ rsent(t) = rsent(s) & \
+\ rrcvd(t) = addm (rrcvd s) pkt & \
+\ rbit(t) = rbit(s) & \
+\ rsending(t) = rsending(s) | \
+\ S_ack(b) => b = rbit(s) & \
+\ rq(t) = rq(s) & \
+\ rsent(t) = addm (rsent s) (rbit s) & \
+\ rrcvd(t) = rrcvd(s) & \
+\ rbit(t)=rbit(s) & \
+\ rsending(s) & \
+\ rsending(t) | \
+\ R_ack(b) => False | \
+\ C_m_s => False | \
+\ C_m_r => count (rsent s) (~rbit s) < countm (rrcvd s) (%y.hdr(y)=rbit(s)) & \
+\ rq(t) = rq(s) & \
+\ rsent(t)=rsent(s) & \
+\ rrcvd(t)=rrcvd(s) & \
+\ rbit(t)=rbit(s) & \
+\ rsending(s) & \
+\ ~rsending(t) | \
+\ C_r_s => False | \
+\ C_r_r(m) => count (rsent s) (rbit s) <= countm (rrcvd s) (%y.hdr(y)=rbit(s)) & \
+\ count (rsent s) (~rbit s) < count (rrcvd s) (rbit(s),m) & \
+\ rq(t) = rq(s)@[m] & \
+\ rsent(t)=rsent(s) & \
+\ rrcvd(t)=rrcvd(s) & \
+\ rbit(t) = (~rbit(s)) & \
+\ ~rsending(s) & \
+\ rsending(t)}"
+
+
+receiver_ioa_def "receiver_ioa == \
+\ (receiver_asig, {([],{|},{|},False,False)}, receiver_trans)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IOA/NTP/Sender.ML Thu Apr 13 16:57:18 1995 +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 (action_ss addsimps
+ (Sender.sender_asig_def :: actions_def ::
+ asig_projections @ set_lemmas)) 1);
+qed "in_sender_asig";
+
+val sender_projections =
+ [Sender.sq_def,Sender.ssent_def,Sender.srcvd_def,
+ Sender.sbit_def,Sender.ssending_def];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IOA/NTP/Sender.thy Thu Apr 13 16:57:18 1995 +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 + Multiset + List +
+
+types
+
+'m sender_state = "'m list * bool multiset * bool multiset * bool * bool"
+(* messages #sent #received header mode *)
+
+consts
+
+sender_asig :: "'m action signature"
+sender_trans :: "('m action, 'm sender_state)transition set"
+sender_ioa :: "('m action, 'm sender_state)ioa"
+sq :: "'m sender_state => 'm list"
+ssent,srcvd :: "'m sender_state => bool multiset"
+sbit :: "'m sender_state => bool"
+ssending :: "'m sender_state => bool"
+
+defs
+
+sq_def "sq == fst"
+ssent_def "ssent == fst o snd"
+srcvd_def "srcvd == fst o snd o snd"
+sbit_def "sbit == fst o snd o snd o snd"
+ssending_def "ssending == snd o snd o snd o snd"
+
+sender_asig_def
+ "sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}), \
+\ UN pkt. {S_pkt(pkt)}, \
+\ {C_m_s,C_r_s})"
+
+sender_trans_def "sender_trans == \
+\ {tr. let s = fst(tr); \
+\ t = snd(snd(tr)) \
+\ in case fst(snd(tr)) \
+\ of \
+\ S_msg(m) => sq(t)=sq(s)@[m] & \
+\ ssent(t)=ssent(s) & \
+\ srcvd(t)=srcvd(s) & \
+\ sbit(t)=sbit(s) & \
+\ ssending(t)=ssending(s) | \
+\ R_msg(m) => False | \
+\ S_pkt(pkt) => hdr(pkt) = sbit(s) & \
+\ (? Q. sq(s) = (msg(pkt)#Q)) & \
+\ sq(t) = sq(s) & \
+\ ssent(t) = addm (ssent s) (sbit s) & \
+\ srcvd(t) = srcvd(s) & \
+\ sbit(t) = sbit(s) & \
+\ ssending(s) & \
+\ ssending(t) | \
+\ R_pkt(pkt) => False | \
+\ S_ack(b) => False | \
+\ R_ack(b) => sq(t)=sq(s) & \
+\ ssent(t)=ssent(s) & \
+\ srcvd(t) = addm (srcvd s) b & \
+\ sbit(t)=sbit(s) & \
+\ ssending(t)=ssending(s) | \
+\ C_m_s => count (ssent s) (~sbit s) < count (srcvd s) (~sbit s) & \
+\ sq(t)=sq(s) & \
+\ ssent(t)=ssent(s) & \
+\ srcvd(t)=srcvd(s) & \
+\ sbit(t)=sbit(s) & \
+\ ssending(s) & \
+\ ~ssending(t) | \
+\ C_m_r => False | \
+\ C_r_s => count (ssent s) (sbit s) <= count (srcvd s) (~sbit s) & \
+\ sq(t)=tl(sq(s)) & \
+\ ssent(t)=ssent(s) & \
+\ srcvd(t)=srcvd(s) & \
+\ sbit(t) = (~sbit(s)) & \
+\ ~ssending(s) & \
+\ ssending(t) | \
+\ C_r_r(m) => False}"
+
+sender_ioa_def "sender_ioa == \
+\ (sender_asig, {([],{|},{|},False,True)}, sender_trans)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IOA/NTP/Spec.thy Thu Apr 13 16:57:18 1995 +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