# HG changeset patch
# User clasohm
# Date 783773409 -3600
# Node ID fd1be45b64bfeedf63b66cb5f5d59185edf1f9db
# Parent  722bf1319be568e0c06f8ce1db4be43bf8031f44
added IOA to isabelle/HOL

diff -r 722bf1319be5 -r fd1be45b64bf IOA/ROOT.ML
--- /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";
diff -r 722bf1319be5 -r fd1be45b64bf IOA/example/Action.ML
--- /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;
diff -r 722bf1319be5 -r fd1be45b64bf IOA/example/Action.thy
--- /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
diff -r 722bf1319be5 -r fd1be45b64bf IOA/example/Channels.ML
--- /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;
diff -r 722bf1319be5 -r fd1be45b64bf IOA/example/Channels.thy
--- /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
diff -r 722bf1319be5 -r fd1be45b64bf IOA/example/Correctness.ML
--- /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();
diff -r 722bf1319be5 -r fd1be45b64bf IOA/example/Correctness.thy
--- /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
diff -r 722bf1319be5 -r fd1be45b64bf IOA/example/Impl.ML
--- /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);
+
diff -r 722bf1319be5 -r fd1be45b64bf IOA/example/Impl.thy
--- /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
diff -r 722bf1319be5 -r fd1be45b64bf IOA/example/Lemmas.ML
--- /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();
diff -r 722bf1319be5 -r fd1be45b64bf IOA/example/Lemmas.thy
--- /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
diff -r 722bf1319be5 -r fd1be45b64bf IOA/example/Multiset.ML
--- /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();
diff -r 722bf1319be5 -r fd1be45b64bf IOA/example/Multiset.thy
--- /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
diff -r 722bf1319be5 -r fd1be45b64bf IOA/example/Packet.thy
--- /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
diff -r 722bf1319be5 -r fd1be45b64bf IOA/example/Read_me
--- /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 ~= []
+
diff -r 722bf1319be5 -r fd1be45b64bf IOA/example/Receiver.ML
--- /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];
+
+
diff -r 722bf1319be5 -r fd1be45b64bf IOA/example/Receiver.thy
--- /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
diff -r 722bf1319be5 -r fd1be45b64bf IOA/example/Sender.ML
--- /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];
diff -r 722bf1319be5 -r fd1be45b64bf IOA/example/Sender.thy
--- /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
diff -r 722bf1319be5 -r fd1be45b64bf IOA/example/Spec.thy
--- /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
diff -r 722bf1319be5 -r fd1be45b64bf IOA/meta_theory/Asig.thy
--- /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 
diff -r 722bf1319be5 -r fd1be45b64bf IOA/meta_theory/IOA.ML
--- /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();
diff -r 722bf1319be5 -r fd1be45b64bf IOA/meta_theory/IOA.thy
--- /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 
diff -r 722bf1319be5 -r fd1be45b64bf IOA/meta_theory/Option.ML
--- /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);
diff -r 722bf1319be5 -r fd1be45b64bf IOA/meta_theory/Option.thy
--- /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
diff -r 722bf1319be5 -r fd1be45b64bf IOA/meta_theory/Solve.ML
--- /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();
diff -r 722bf1319be5 -r fd1be45b64bf IOA/meta_theory/Solve.thy
--- /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