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