--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/IOA/ROOT.ML Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,4 @@
+goals_limit := 1;
+
+loadpath := "./meta_theory" :: "./example" :: !loadpath;
+use_thy "Correctness";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/IOA/example/Action.ML Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,5 @@
+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/IOA/example/Action.thy Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,6 @@
+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/IOA/example/Channels.ML Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,39 @@
+local
+val SS = action_ss addsimps
+ (Channels.srch_asig_def ::
+ Channels.rsch_asig_def ::
+ actions_def :: asig_projections_def :: set_lemmas)
+in
+val _ = goal Channels.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)";
+
+val _ = by (simp_tac SS 1);
+
+val in_srch_asig = result();
+
+val _ = goal Channels.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)";
+
+val _ = by (simp_tac SS 1);
+
+val in_rsch_asig = result();
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/IOA/example/Channels.thy Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,61 @@
+Channels = IOA + Action + Multiset + "Lemmas" + Packet +
+
+consts
+
+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"
+
+rules
+
+srch_asig_def "srch_asig == <UN pkt. {S_pkt(pkt)}, \
+\ UN pkt. {R_pkt(pkt)}, \
+\ {}>"
+
+rsch_asig_def "rsch_asig == <UN b. {S_ack(b)}, \
+\ UN b. {R_ack(b)}, \
+\ {}>"
+
+srch_trans_def "srch_trans == \
+\ {tr. let s = fst(tr); \
+\ t = snd(snd(tr)) \
+\ in \
+\ case fst(snd(tr)) \
+\ of S_msg(m) => False | \
+\ R_msg(m) => False | \
+\ S_pkt(pkt) => t = addm(s, pkt) | \
+\ R_pkt(pkt) => count(s, pkt) ~= 0 & t = delm(s, pkt) | \
+\ 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}"
+
+rsch_trans_def "rsch_trans == \
+\ {tr. let s = fst(tr); \
+\ t = snd(snd(tr)) \
+\ in \
+\ case fst(snd(tr)) \
+\ of \
+\ S_msg(m) => False | \
+\ R_msg(m) => False | \
+\ S_pkt(pkt) => False | \
+\ R_pkt(pkt) => False | \
+\ S_ack(b) => t = addm(s,b) | \
+\ R_ack(b) => count(s,b) ~= 0 & t = delm(s,b) | \
+\ C_m_s => False | \
+\ C_m_r => False | \
+\ C_r_s => False | \
+\ C_r_r(m) => False}"
+
+
+srch_ioa_def "srch_ioa == <srch_asig, {{|}}, srch_trans>"
+rsch_ioa_def "rsch_ioa == <rsch_asig, {{|}}, rsch_trans>"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/IOA/example/Correctness.ML Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,96 @@
+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,
+ Channels.srch_asig_def,Channels.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 ([asig_projections_def,externals_def,
+ restrict_def,restrict_asig_def,
+ asig_of_par, asig_comp_def, Spec.sig_def]
+ @ impl_ioas @ impl_asigs)) 1);
+ by(Action.action.induct_tac "a" 1);
+ by(ALLGOALS(simp_tac (action_ss addsimps
+ (actions_def :: asig_projections_def :: set_lemmas))));
+val externals_lemma = result();
+
+
+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 [plus_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 [plus_leD1 RS leD]) 1);
+
+by(asm_full_simp_tac hom_ss 1);
+result();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/IOA/example/Correctness.thy Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,15 @@
+Correctness = Solve + Impl + Spec + "Lemmas" +
+
+consts
+
+hom :: "'m impl_state => 'm list"
+
+
+rules
+
+hom_def
+"hom(s) == rq(rec(s)) @ if(rbit(rec(s)) = sbit(sen(s)), \
+\ sq(sen(s)), \
+\ ttl(sq(sen(s))))"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/IOA/example/Impl.ML Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,385 @@
+val impl_ioas =
+ [Impl.impl_def,
+ Sender.sender_ioa_def,
+ Receiver.receiver_ioa_def,
+ Channels.srch_ioa_def,
+ Channels.rsch_ioa_def];
+
+val transitions = [Sender.sender_trans_def, Receiver.receiver_trans_def,
+ Channels.srch_trans_def, Channels.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()];
+
+
+(* Instantiation of a tautology? *)
+goal Packet.thy "!x. x = packet --> hdr(x) = hdr(packet)";
+ by (simp_tac (HOL_ss addsimps [Packet.hdr_def]) 1);
+val eq_packet_imp_eq_hdr = result();
+
+
+(* INVARIANT 1 *)
+val ss = impl_ss addcongs [if_weak_cong] addsimps transitions;
+
+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]));
+
+by(EVERY1[tac, tac, tac, tac, tac, tac, 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 (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 (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 (dmatch_tac [less_leq_less RS mp] 1);
+by (cut_facts_tac [rewrite_rule[Packet.hdr_def]
+ eq_packet_imp_eq_hdr RS countm_props] 1);;
+by (dtac mp 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]);
+
+val inv1 = result();
+
+
+
+(* 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 [plus_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 [plus_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);
+val inv2 = result();
+
+
+(* 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 (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 (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);
+val inv3 = result();
+
+
+
+(* 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_leq_less RS mp RS mp) 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);
+val inv4 = result();
+
+
+
+(* 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/IOA/example/Impl.thy Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,63 @@
+Impl = Sender + Receiver + Channels +
+
+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"
+
+rules
+
+ 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/IOA/example/Lemmas.ML Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,245 @@
+(* Logic *)
+val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
+ by(fast_tac (HOL_cs addDs prems) 1);
+val imp_conj_lemma = result();
+
+goal HOL.thy "(P --> (? x. Q(x))) = (? x. P --> Q(x))";
+ by(fast_tac HOL_cs 1);
+val imp_ex_equiv = result();
+
+goal HOL.thy "(A --> B & C) = ((A --> B) & (A --> C))";
+ by (fast_tac HOL_cs 1);
+val fork_lemma = result();
+
+goal HOL.thy "((A --> B) & (C --> B)) = ((A | C) --> B)";
+ by (fast_tac HOL_cs 1);
+val imp_or_lem = result();
+
+goal HOL.thy "(X = (~ Y)) = ((~X) = Y)";
+ by (fast_tac HOL_cs 1);
+val neg_flip = result();
+
+goal HOL.thy "P --> Q(M) --> Q(if(P,M,N))";
+ by (rtac impI 1);
+ by (rtac impI 1);
+ by (rtac (expand_if RS iffD2) 1);
+ by (fast_tac HOL_cs 1);
+val imp_true_decompose = result();
+
+goal HOL.thy "(~P) --> Q(N) --> Q(if(P,M,N))";
+ by (rtac impI 1);
+ by (rtac impI 1);
+ by (rtac (expand_if RS iffD2) 1);
+ by (fast_tac HOL_cs 1);
+val imp_false_decompose = result();
+
+
+(* 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 = 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 = 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);
+val leq_suc = result();
+
+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);
+val left_plus_cancel = result();
+
+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);
+val left_plus_cancel_inside_succ = result();
+
+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);
+val nonzero_is_succ = result();
+
+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);
+val less_add_same_less = result();
+
+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);
+val leq_add_leq = result();
+
+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);
+val left_add_leq = result();
+
+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);
+val less_add_cong = result();
+
+goal Nat.thy "!!i. [| i < j; j <= k |] ==> i < (k::nat)";
+ by (dtac le_imp_less_or_eq 1);
+ by (fast_tac (HOL_cs addIs [less_trans]) 1);
+val less_leq_less = result();
+
+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);
+val less_eq_add_cong = result();
+
+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);
+val leq_add_left_cong = result();
+
+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);
+val suc_not_zero = result();
+
+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);
+val suc_leq_suc = result();
+
+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);
+val zero_eq = result();
+
+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);
+val less_suc_imp_leq = result();
+
+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);
+val suc_pred_id = result();
+
+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);
+val pred_suc = result();
+
+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);
+val unzero_less = result();
+
+(* Duplicate of earlier lemma! *)
+goal Arith.thy "x<(y::nat) --> y<=z --> x<(z::nat)";
+ by (rtac impI 1); by (rtac impI 1);
+ by (dtac le_imp_less_or_eq 1);
+ by (fast_tac (HOL_cs addIs [less_trans]) 1);
+val less_leq_less = result();
+
+goal Arith.thy "(Suc(n) <= Suc(m)) = (n <= m)";
+ by (simp_tac (arith_ss addsimps [le_eq_less_or_eq]) 1);
+val succ_leq_mono = result();
+
+(* 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
+ [succ_leq_mono, le_refl RS (leq_add_leq RS mp)]) 1);
+val plus_leq_lem = result();
+
+(* Lists *)
+
+goal List.thy "(L @ (x#M)) ~= []";
+ by (list_ind_tac "L" 1);
+ by (simp_tac list_ss 1);
+ by (asm_simp_tac list_ss 1);
+val append_cons = result();
+
+goal List.thy "(X ~= hd(L@M)) = (X ~= if(L = [], hd(M), hd(L)))";
+ by (list_ind_tac "L" 1);
+ by (simp_tac list_ss 1);
+ by (asm_full_simp_tac list_ss 1);
+val not_hd_append = result();
+
+goal List.thy "(L = (x#rst)) --> (L = []) --> P";
+ by (simp_tac list_ss 1);
+val list_cases = result();
+
+goal List.thy "(? L2. L1 = x#L2) --> (L1 ~= [])";
+ by (strip_tac 1);
+ by (etac exE 1);
+ by (asm_simp_tac list_ss 1);
+val cons_imp_not_null = result();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/IOA/example/Lemmas.thy Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,1 @@
+Lemmas = Arith
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/IOA/example/Multiset.ML Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,75 @@
+goalw Multiset.thy [Multiset.count_def, Multiset.countm_empty_def]
+ "count({|},x) = 0";
+ by (rtac refl 1);
+val count_empty = result();
+
+goal Multiset.thy
+ "count(addm(M,x),y) = if(y=x,Suc(count(M,y)),count(M,y))";
+ by (asm_simp_tac (arith_ss addsimps
+ [Multiset.count_def,Multiset.countm_nonempty_def]
+ setloop (split_tac [expand_if])) 1);
+val count_addm_simp = result();
+
+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);
+val count_leq_addm = result();
+
+goalw Multiset.thy [Multiset.count_def]
+ "count(delm(M,x),y) = if(y=x,pred(count(M,y)),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);
+val count_delm_simp = result();
+
+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);
+val countm_props = result();
+
+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);
+val countm_spurious_delm = result();
+
+
+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 = 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);
+val countm_done_delm = result();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/IOA/example/Multiset.thy Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,39 @@
+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,M,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), Suc(0), 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/IOA/example/Packet.thy Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,18 @@
+Packet = Arith +
+
+types
+
+ 'msg packet = "bool * 'msg"
+
+consts
+
+ hdr :: "'msg packet => bool"
+ msg :: "'msg packet => 'msg"
+
+rules
+
+ hdr_def "hdr == fst"
+
+ msg_def "msg == snd"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/IOA/example/Read_me Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,177 @@
+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.
+
+------------------------------------------------------------------------------
+
+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/IOA/example/Receiver.ML Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,24 @@
+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_def :: set_lemmas)) 1);
+val in_receiver_asig = result();
+
+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/IOA/example/Receiver.thy Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,81 @@
+Receiver = List + IOA + Action + Multiset + "Lemmas" +
+
+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"
+
+rules
+
+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/IOA/example/Sender.ML Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,19 @@
+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_def :: set_lemmas)) 1);
+val in_sender_asig = result();
+
+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/IOA/example/Sender.thy Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,77 @@
+Sender = IOA + Action + Multiset + List + "Lemmas" +
+
+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"
+
+rules
+
+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/IOA/example/Spec.thy Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,34 @@
+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"
+
+rules
+
+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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/IOA/meta_theory/Asig.thy Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,36 @@
+Asig = Option +
+
+types
+
+'a signature = "('a set * 'a set * 'a set)"
+
+consts
+ actions,inputs,outputs,internals,externals
+ ::"'action signature => 'action set"
+ is_asig ::"'action signature => bool"
+ mk_ext_asig ::"'action signature => 'action signature"
+
+
+rules
+
+asig_projections_def
+ "inputs = fst & outputs = (fst o snd) & internals = (snd o snd)"
+
+actions_def
+ "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"
+
+externals_def
+ "externals(asig) == (inputs(asig) Un outputs(asig))"
+
+is_asig_def
+ "is_asig(triple) == \
+ \ ((inputs(triple) Int outputs(triple) = {}) & \
+ \ (outputs(triple) Int internals(triple) = {}) & \
+ \ (inputs(triple) Int internals(triple) = {}))"
+
+
+mk_ext_asig_def
+ "mk_ext_asig(triple) == <inputs(triple), outputs(triple), {}>"
+
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/IOA/meta_theory/IOA.ML Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,140 @@
+open IOA Asig;
+
+val exec_rws = [executions_def,is_execution_fragment_def];
+
+goal IOA.thy
+"asig_of(<x,y,z>) = x & starts_of(<x,y,z>) = y & trans_of(<x,y,z>) = z";
+ by (simp_tac (SS addsimps [ioa_projections_def]) 1);
+ val ioa_triple_proj = result();
+
+goalw IOA.thy [ioa_def,state_trans_def,actions_def, is_asig_def]
+ "!!A. [| IOA(A); <s1,a,s2>:trans_of(A) |] ==> a:actions(asig_of(A))";
+ by (REPEAT(etac conjE 1));
+ by (EVERY1[etac allE, etac impE, atac]);
+ by (asm_full_simp_tac SS 1);
+val trans_in_actions = result();
+
+
+goal IOA.thy "filter_oseq(p,filter_oseq(p,s)) = filter_oseq(p,s)";
+ by (simp_tac (SS addsimps [filter_oseq_def]) 1);
+ by (rtac ext 1);
+ by (Option.option.induct_tac "s(i)" 1);
+ by (simp_tac SS 1);
+ by (simp_tac (SS setloop (split_tac [expand_if])) 1);
+val filter_oseq_idemp = result();
+
+goalw IOA.thy [mk_behaviour_def,filter_oseq_def]
+"(mk_behaviour(A, s, n) = None) = \
+\ (s(n)=None | (? a. s(n)=Some(a) & a ~: externals(asig_of(A)))) \
+\ & \
+\ (mk_behaviour(A, s, n) = Some(a)) = \
+\ (s(n)=Some(a) & a : externals(asig_of(A)))";
+ by (Option.option.induct_tac "s(n)" 1);
+ by (ALLGOALS (simp_tac (SS setloop (split_tac [expand_if]))));
+ by (fast_tac HOL_cs 1);
+val mk_behaviour_thm = result();
+
+goalw IOA.thy [reachable_def] "!!A. s:starts_of(A) ==> reachable(A,s)";
+ by (res_inst_tac [("x","<(%i.None),(%i.s)>::('action,'a)execution")] bexI 1);
+ by (simp_tac SS 1);
+ by (asm_simp_tac (SS addsimps exec_rws) 1);
+val reachable_0 = result();
+
+goalw IOA.thy (reachable_def::exec_rws)
+"!!A. [| reachable(A,s); <s,a,t> : trans_of(A) |] ==> reachable(A,t)";
+ by(asm_full_simp_tac SS 1);
+ by(safe_tac set_cs);
+ by(res_inst_tac [("x","<%i.if(i<n,fst(ex,i),if(i=n,Some(a),None)), \
+ \ %i.if(i<Suc(n),snd(ex,i),t)>")] bexI 1);
+ by(res_inst_tac [("x","Suc(n)")] exI 1);
+ by(simp_tac SS 1);
+ by(asm_simp_tac (SS delsimps [less_Suc_eq]) 1);
+ by(REPEAT(rtac allI 1));
+ by(res_inst_tac [("m","na"),("n","n")] (make_elim less_linear) 1);
+ be disjE 1;
+ by(asm_simp_tac SS 1);
+ be disjE 1;
+ by(asm_simp_tac SS 1);
+ by(fast_tac HOL_cs 1);
+ by(forward_tac [less_not_sym] 1);
+ by(asm_simp_tac (SS addsimps [less_not_refl2]) 1);
+val reachable_n = result();
+
+val [p1,p2] = goalw IOA.thy [invariant_def]
+ "[| !!s. s:starts_of(A) ==> P(s); \
+\ !!s t a. [|reachable(A,s); P(s)|] ==> <s,a,t>: trans_of(A) --> P(t) |] \
+\ ==> invariant(A,P)";
+ by (rewrite_goals_tac(reachable_def::Let_def::exec_rws));
+ by (safe_tac set_cs);
+ by (res_inst_tac [("Q","reachable(A,snd(ex,n))")] conjunct1 1);
+ by (nat_ind_tac "n" 1);
+ by (fast_tac (set_cs addIs [p1,reachable_0]) 1);
+ by (eres_inst_tac[("x","n1")]allE 1);
+ by (eres_inst_tac[("P","%x.!a::'action.?Q(x,a)"),
+ ("opt","fst(ex,n1)")] optE 1);
+ by (asm_simp_tac HOL_ss 1);
+ by (safe_tac HOL_cs);
+ by (etac (p2 RS mp) 1);
+ by (ALLGOALS(fast_tac(set_cs addDs [hd Option.option.inject RS iffD1,
+ reachable_n])));
+val invariantI = result();
+
+val [p1,p2] = goal IOA.thy
+ "[| !!s. s : starts_of(A) ==> P(s); \
+\ !!s t a. reachable(A, s) ==> P(s) --> <s,a,t>:trans_of(A) --> P(t) \
+\ |] ==> invariant(A, P)";
+ by (fast_tac (HOL_cs addSIs [invariantI] addSDs [p1,p2]) 1);
+val invariantI1 = result();
+
+val [p1,p2] = goalw IOA.thy [invariant_def]
+"[| invariant(A,P); reachable(A,s) |] ==> P(s)";
+ br(p2 RS (p1 RS spec RS mp))1;
+val invariantE = result();
+
+goal IOA.thy
+"actions(asig_comp(a,b)) = actions(a) Un actions(b)";
+ by(simp_tac (pair_ss addsimps
+ [actions_def,asig_projections_def,asig_comp_def]) 1);
+ by(fast_tac eq_cs 1);
+val actions_asig_comp = result();
+
+goal IOA.thy
+"starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}";
+ by(simp_tac (SS addsimps [par_def,ioa_projections_def]) 1);
+val starts_of_par = result();
+
+(* Every state in an execution is reachable *)
+goalw IOA.thy [reachable_def]
+"!!A. ex:executions(A) ==> !n. reachable(A, snd(ex,n))";
+ by (fast_tac set_cs 1);
+val states_of_exec_reachable = result();
+
+
+goal IOA.thy
+"<s,a,t> : trans_of(A || B || C || D) = \
+\ ((a:actions(asig_of(A)) | a:actions(asig_of(B)) | a:actions(asig_of(C)) | \
+\ a:actions(asig_of(D))) & \
+\ if(a:actions(asig_of(A)), <fst(s),a,fst(t)>:trans_of(A), fst(t)=fst(s)) & \
+\ if(a:actions(asig_of(B)), <fst(snd(s)),a,fst(snd(t))>:trans_of(B), \
+\ fst(snd(t))=fst(snd(s))) & \
+\ if(a:actions(asig_of(C)), \
+\ <fst(snd(snd(s))),a,fst(snd(snd(t)))>:trans_of(C), \
+\ fst(snd(snd(t)))=fst(snd(snd(s)))) & \
+\ if(a:actions(asig_of(D)), \
+\ <snd(snd(snd(s))),a,snd(snd(snd(t)))>:trans_of(D), \
+\ snd(snd(snd(t)))=snd(snd(snd(s)))))";
+ by(simp_tac (SS addsimps [par_def,ioa_projections_def,actions_asig_comp,
+ Pair_fst_snd_eq (* old pair_eq *)]
+ setloop (split_tac [expand_if])) 1);
+val trans_of_par4 = result();
+
+goal IOA.thy "starts_of(restrict(ioa,acts)) = starts_of(ioa) & \
+\ trans_of(restrict(ioa,acts)) = trans_of(ioa) & \
+\ reachable(restrict(ioa,acts),s) = reachable(ioa,s)";
+ by (simp_tac (SS addsimps [ioa_projections_def,is_execution_fragment_def,
+ executions_def,reachable_def,restrict_def]) 1);
+val cancel_restrict = result();
+
+goal IOA.thy "asig_of(A || B) = asig_comp(asig_of(A),asig_of(B))";
+ by(simp_tac (SS addsimps [ioa_projections_def,par_def]) 1);
+val asig_of_par = result();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/IOA/meta_theory/IOA.thy Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,180 @@
+(* The I/O automata of Lynch and Tuttle. *)
+
+IOA = Asig +
+
+types
+ 'a seq = "nat => 'a"
+ 'a oseq = "nat => 'a option"
+ ('a,'b)execution = "'a oseq * 'b seq"
+ ('a,'s)transition = "('s * 'a * 's)"
+ ('a,'s)ioa = "'a signature * 's set * ('a,'s)transition set"
+
+consts
+
+ (* IO automata *)
+ state_trans::"['action signature, ('action,'state)transition set] => bool"
+ asig_of ::"('action,'state)ioa => 'action signature"
+ starts_of ::"('action,'state)ioa => 'state set"
+ trans_of ::"('action,'state)ioa => ('action,'state)transition set"
+ IOA ::"('action,'state)ioa => bool"
+
+ (* Executions, schedules, and behaviours *)
+
+ is_execution_fragment,
+ has_execution ::"[('action,'state)ioa, ('action,'state)execution] => bool"
+ executions :: "('action,'state)ioa => ('action,'state)execution set"
+ mk_behaviour :: "[('action,'state)ioa, 'action oseq] => 'action oseq"
+ reachable :: "[('action,'state)ioa, 'state] => bool"
+ invariant :: "[('action,'state)ioa, 'state=>bool] => bool"
+ has_behaviour :: "[('action,'state)ioa, 'action oseq] => bool"
+ behaviours :: "('action,'state)ioa => 'action oseq set"
+
+ (* Composition of action signatures and automata *)
+ compatible_asigs ::"('a => 'action signature) => bool"
+ asig_composition ::"('a => 'action signature) => 'action signature"
+ compatible_ioas ::"('a => ('action,'state)ioa) => bool"
+ ioa_composition ::"('a => ('action, 'state)ioa) =>('action,'a => 'state)ioa"
+
+ (* binary composition of action signatures and automata *)
+ compat_asigs ::"['action signature, 'action signature] => bool"
+ asig_comp ::"['action signature, 'action signature] => 'action signature"
+ compat_ioas ::"[('action,'state)ioa, ('action,'state)ioa] => bool"
+ "||" ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa" (infixr 10)
+
+ (* Filtering and hiding *)
+ filter_oseq :: "('a => bool) => 'a oseq => 'a oseq"
+
+ restrict_asig :: "['a signature, 'a set] => 'a signature"
+ restrict :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
+
+ (* Notions of correctness *)
+ ioa_implements :: "[('action,'state1)ioa, ('action,'state2)ioa] => bool"
+
+
+rules
+
+state_trans_def
+ "state_trans(asig,R) == \
+ \ (!triple. triple:R --> fst(snd(triple)):actions(asig)) & \
+ \ (!a. (a:inputs(asig)) --> (!s1. ? s2. <s1,a,s2>:R))"
+
+
+ioa_projections_def
+ "asig_of = fst & starts_of = (fst o snd) & trans_of = (snd o snd)"
+
+
+ioa_def
+ "IOA(ioa) == (is_asig(asig_of(ioa)) & \
+ \ (~ starts_of(ioa) = {}) & \
+ \ state_trans(asig_of(ioa),trans_of(ioa)))"
+
+
+(* An execution fragment is modelled with a pair of sequences:
+ * the first is the action options, the second the state sequence.
+ * Finite executions have None actions from some point on.
+ *******)
+is_execution_fragment_def
+ "is_execution_fragment(A,ex) == \
+ \ let act = fst(ex); state = snd(ex) \
+ \ in !n a. (act(n)=None --> state(Suc(n)) = state(n)) & \
+ \ (act(n)=Some(a) --> <state(n),a,state(Suc(n))>:trans_of(A))"
+
+
+executions_def
+ "executions(ioa) == {e. snd(e,0):starts_of(ioa) & \
+\ is_execution_fragment(ioa,e)}"
+
+
+(* Is a state reachable. Using an inductive definition, this could be defined
+ * by the following 2 rules
+ *
+ * x:starts_of(ioa)
+ * ----------------
+ * reachable(ioa,x)
+ *
+ * reachable(ioa,s) & ? <s,a,s'>:trans_of(ioa)
+ * -------------------------------------------
+ * reachable(ioa,s')
+ *
+ * A direkt definition follows.
+ *******************************)
+reachable_def
+ "reachable(ioa,s) == (? ex:executions(ioa). ? n. snd(ex,n) = s)"
+
+
+invariant_def "invariant(A,P) == (!s. reachable(A,s) --> P(s))"
+
+
+(* Restrict the trace to those members of the set s *)
+filter_oseq_def
+ "filter_oseq(p,s) == \
+\ (%i.case s(i) \
+\ of None => None \
+\ | Some(x) => if(p(x),Some(x),None))"
+
+
+mk_behaviour_def
+ "mk_behaviour(ioa) == filter_oseq(%a.a:externals(asig_of(ioa)))"
+
+
+(* Does an ioa have an execution with the given behaviour *)
+has_behaviour_def
+ "has_behaviour(ioa,b) == \
+\ (? ex:executions(ioa). b = mk_behaviour(ioa,fst(ex)))"
+
+
+(* All the behaviours of an ioa *)
+behaviours_def
+ "behaviours(ioa) == {b. has_behaviour(ioa,b)}"
+
+
+compat_asigs_def
+ "compat_asigs (a1,a2) == \
+ \ (((outputs(a1) Int outputs(a2)) = {}) & \
+ \ ((internals(a1) Int actions(a2)) = {}) & \
+ \ ((internals(a2) Int actions(a1)) = {}))"
+
+
+compat_ioas_def
+ "compat_ioas(ioa1,ioa2) == compat_asigs (asig_of(ioa1)) (asig_of(ioa2))"
+
+
+asig_comp_def
+ "asig_comp (a1,a2) == \
+ \ (<(inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)), \
+ \ (outputs(a1) Un outputs(a2)), \
+ \ (internals(a1) Un internals(a2))>)"
+
+
+par_def
+ "(ioa1 || ioa2) == \
+ \ <asig_comp(asig_of(ioa1),asig_of(ioa2)), \
+ \ {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)}, \
+ \ {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) \
+ \ in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) & \
+ \ if(a:actions(asig_of(ioa1)), \
+ \ <fst(s),a,fst(t)>:trans_of(ioa1), \
+ \ fst(t) = fst(s)) \
+ \ & \
+ \ if(a:actions(asig_of(ioa2)), \
+ \ <snd(s),a,snd(t)>:trans_of(ioa2), \
+ \ snd(t) = snd(s))}>"
+
+
+restrict_asig_def
+ "restrict_asig(asig,actns) == \
+\ <inputs(asig) Int actns, outputs(asig) Int actns, \
+\ internals(asig) Un (externals(asig) - actns)>"
+
+
+restrict_def
+ "restrict(ioa,actns) == \
+\ <restrict_asig(asig_of(ioa),actns), starts_of(ioa), trans_of(ioa)>"
+
+
+ioa_implements_def
+ "ioa_implements(ioa1,ioa2) == \
+\ (externals(asig_of(ioa1)) = externals(asig_of(ioa2)) & \
+\ behaviours(ioa1) <= behaviours(ioa2))"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/IOA/meta_theory/Option.ML Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,8 @@
+val option_rws = Let_def :: Option.option.simps;
+val SS = arith_ss addsimps option_rws;
+
+val [prem] = goal Option.thy "P(opt) ==> P(None) | (? x. P(Some(x)))";
+ br (prem RS rev_mp) 1;
+ by (Option.option.induct_tac "opt" 1);
+ by (ALLGOALS(fast_tac HOL_cs));
+val optE = standard(result() RS disjE);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/IOA/meta_theory/Option.thy Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,3 @@
+Option = Arith +
+datatype 'a option = None | Some('a)
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/IOA/meta_theory/Solve.ML Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,45 @@
+open Solve IOA Asig;
+
+val SS = SS addsimps [mk_behaviour_thm,trans_in_actions];
+
+goalw Solve.thy [is_weak_pmap_def,behaviours_def]
+ "!!f. [| IOA(C); IOA(A); externals(asig_of(C)) = externals(asig_of(A)); \
+\ is_weak_pmap(f,C,A) |] ==> behaviours(C) <= behaviours(A)";
+
+ by (simp_tac(SS addsimps [has_behaviour_def])1);
+ by (safe_tac set_cs);
+
+ (* give execution of abstract automata *)
+ by (res_inst_tac[("x","<mk_behaviour(A,fst(ex)),%i.f(snd(ex,i))>")] bexI 1);
+
+ (* Behaviours coincide *)
+ by (asm_simp_tac (SS addsimps [mk_behaviour_def,filter_oseq_idemp])1);
+
+ (* Use lemma *)
+ by (forward_tac [states_of_exec_reachable] 1);
+
+ (* Now show that it's an execution *)
+ by (asm_full_simp_tac(SS addsimps [executions_def]) 1);
+ by (safe_tac set_cs);
+
+ (* Start states map to start states *)
+ by (dtac bspec 1);
+ by (atac 1);
+
+ (* Show that it's an execution fragment *)
+ by (asm_full_simp_tac (SS addsimps [is_execution_fragment_def])1);
+ by (safe_tac HOL_cs);
+
+ (* Cases on whether action is external or not (basically) *)
+ (* 1 *)
+ by (eres_inst_tac [("x","snd(ex,n)")] allE 1);
+ by (eres_inst_tac [("x","snd(ex,Suc(n))")] allE 1);
+ by (eres_inst_tac [("x","aa")] allE 1);
+ by (asm_full_simp_tac SS 1);
+
+ (* 2 *)
+ by (eres_inst_tac [("x","snd(ex,n)")] allE 1);
+ by (eres_inst_tac [("x","snd(ex,Suc(n))")] allE 1);
+ by (eres_inst_tac [("x","a")] allE 1);
+ by (asm_full_simp_tac SS 1);
+val trace_inclusion = result();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/IOA/meta_theory/Solve.thy Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,20 @@
+(* Methods of proof for IOA. *)
+
+Solve = IOA +
+
+consts
+
+ is_weak_pmap :: "['c => 'a, ('action,'c)ioa,('action,'a)ioa] => bool"
+
+rules
+
+is_weak_pmap_def
+ "is_weak_pmap(f,C,A) == \
+\ (!s:starts_of(C). f(s):starts_of(A)) & \
+\ (!s t a. reachable(C,s) & \
+\ <s,a,t>:trans_of(C) \
+\ --> if(a:externals(asig_of(C)), \
+\ <f(s),a,f(t)>:trans_of(A), \
+\ f(s)=f(t)))"
+
+end