# HG changeset patch # User wenzelm # Date 1148756431 -7200 # Node ID c58ef2aa5430072ecb01d298f37e2a65174c2bf8 # Parent 1ac610922636b55694bac77890b414a4da1dd806 removed legacy ML scripts; diff -r 1ac610922636 -r c58ef2aa5430 src/HOLCF/IOA/NTP/Abschannel.ML --- a/src/HOLCF/IOA/NTP/Abschannel.ML Sat May 27 19:49:36 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,55 +0,0 @@ -(* Title: HOL/IOA/NTP/Abschannel.ML - ID: $Id$ - Author: Olaf Mueller - -Derived rules. -*) - -val unfold_renaming = - [srch_asig_def, rsch_asig_def, rsch_ioa_def, srch_ioa_def, ch_ioa_def, - ch_asig_def, srch_actions_def, rsch_actions_def, rename_def, rename_set_def, asig_of_def, - actions_def, srch_trans_def, rsch_trans_def, ch_trans_def,starts_of_def, - trans_of_def] @ asig_projections; - -Goal - "S_msg(m) ~: actions(srch_asig) & \ - \ R_msg(m) ~: actions(srch_asig) & \ - \ S_pkt(pkt) : actions(srch_asig) & \ - \ R_pkt(pkt) : actions(srch_asig) & \ - \ S_ack(b) ~: actions(srch_asig) & \ - \ R_ack(b) ~: actions(srch_asig) & \ - \ C_m_s ~: actions(srch_asig) & \ - \ C_m_r ~: actions(srch_asig) & \ - \ C_r_s ~: actions(srch_asig) & C_r_r(m) ~: actions(srch_asig)"; - -by (simp_tac (simpset() addsimps unfold_renaming) 1); -qed"in_srch_asig"; - -Goal - "S_msg(m) ~: actions(rsch_asig) & \ - \ R_msg(m) ~: actions(rsch_asig) & \ - \ S_pkt(pkt) ~: actions(rsch_asig) & \ - \ R_pkt(pkt) ~: actions(rsch_asig) & \ - \ S_ack(b) : actions(rsch_asig) & \ - \ R_ack(b) : actions(rsch_asig) & \ - \ C_m_s ~: actions(rsch_asig) & \ - \ C_m_r ~: actions(rsch_asig) & \ - \ C_r_s ~: actions(rsch_asig) & \ - \ C_r_r(m) ~: actions(rsch_asig)"; - -by (simp_tac (simpset() addsimps unfold_renaming) 1); -qed"in_rsch_asig"; - -Goal "srch_ioa = \ -\ (srch_asig, {{|}}, srch_trans,srch_wfair,srch_sfair)"; -by (simp_tac (simpset() addsimps [srch_asig_def,srch_trans_def, asig_of_def, trans_of_def, - wfair_of_def, sfair_of_def,srch_wfair_def,srch_sfair_def]) 1); -by (simp_tac (simpset() addsimps unfold_renaming) 1); -qed"srch_ioa_thm"; - -Goal "rsch_ioa = \ -\ (rsch_asig, {{|}}, rsch_trans,rsch_wfair,rsch_sfair)"; -by (simp_tac (simpset() addsimps [rsch_asig_def,rsch_trans_def, asig_of_def, trans_of_def, - wfair_of_def, sfair_of_def,rsch_wfair_def,rsch_sfair_def]) 1); -by (simp_tac (simpset() addsimps unfold_renaming) 1); -qed"rsch_ioa_thm"; diff -r 1ac610922636 -r c58ef2aa5430 src/HOLCF/IOA/NTP/Abschannel.thy --- a/src/HOLCF/IOA/NTP/Abschannel.thy Sat May 27 19:49:36 2006 +0200 +++ b/src/HOLCF/IOA/NTP/Abschannel.thy Sat May 27 21:00:31 2006 +0200 @@ -94,6 +94,48 @@ C_r_s => None | C_r_r(m) => None" -ML {* use_legacy_bindings (the_context ()) *} +lemmas unfold_renaming = + srch_asig_def rsch_asig_def rsch_ioa_def srch_ioa_def ch_ioa_def + ch_asig_def srch_actions_def rsch_actions_def rename_def rename_set_def asig_of_def + actions_def srch_trans_def rsch_trans_def ch_trans_def starts_of_def + trans_of_def asig_projections + +lemma in_srch_asig: + "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 add: unfold_renaming) + +lemma in_rsch_asig: + "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 add: unfold_renaming) + +lemma srch_ioa_thm: "srch_ioa = + (srch_asig, {{|}}, srch_trans,srch_wfair,srch_sfair)" +apply (simp (no_asm) add: srch_asig_def srch_trans_def asig_of_def trans_of_def wfair_of_def sfair_of_def srch_wfair_def srch_sfair_def) +apply (simp (no_asm) add: unfold_renaming) +done + +lemma rsch_ioa_thm: "rsch_ioa = + (rsch_asig, {{|}}, rsch_trans,rsch_wfair,rsch_sfair)" +apply (simp (no_asm) add: rsch_asig_def rsch_trans_def asig_of_def trans_of_def wfair_of_def sfair_of_def rsch_wfair_def rsch_sfair_def) +apply (simp (no_asm) add: unfold_renaming) +done end diff -r 1ac610922636 -r c58ef2aa5430 src/HOLCF/IOA/NTP/Action.thy --- a/src/HOLCF/IOA/NTP/Action.thy Sat May 27 19:49:36 2006 +0200 +++ b/src/HOLCF/IOA/NTP/Action.thy Sat May 27 21:00:31 2006 +0200 @@ -14,6 +14,4 @@ | S_ack bool | R_ack bool | C_m_s | C_m_r | C_r_s | C_r_r 'm -ML {* use_legacy_bindings (the_context ()) *} - end diff -r 1ac610922636 -r c58ef2aa5430 src/HOLCF/IOA/NTP/Correctness.ML --- a/src/HOLCF/IOA/NTP/Correctness.ML Sat May 27 19:49:36 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,105 +0,0 @@ -(* Title: HOL/IOA/NTP/Correctness.ML - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind -*) - -(* repeated from Traces.ML *) -change_claset (fn cs => cs delSWrapper "split_all_tac"); - - -val hom_ioas = [thm "Spec.ioa_def", thm "Spec.trans_def", - sender_trans_def,receiver_trans_def] - @ impl_ioas; - -val impl_asigs = [sender_asig_def,receiver_asig_def, - srch_asig_def,rsch_asig_def]; - -(* Two simpsets: - simpset() is basic, ss' unfolds hom_ioas *) - -Delsimps [split_paired_All]; - -val ss' = (simpset() addsimps hom_ioas); - - -(* A lemma about restricting the action signature of the implementation - * to that of the specification. - ****************************) -Goal - "a:externals(asig_of(Automata.restrict impl_ioa (externals spec_sig))) = \ -\ (case a of \ -\ S_msg(m) => True \ -\ | R_msg(m) => True \ -\ | S_pkt(pkt) => False \ -\ | R_pkt(pkt) => False \ -\ | S_ack(b) => False \ -\ | R_ack(b) => False \ -\ | C_m_s => False \ -\ | C_m_r => False \ -\ | C_r_s => False \ -\ | C_r_r(m) => False)"; - by (simp_tac (simpset() addsimps ([externals_def, restrict_def, - restrict_asig_def, thm "Spec.sig_def"] - @asig_projections)) 1); - - by (induct_tac "a" 1); - by (ALLGOALS(simp_tac (simpset() addsimps [actions_def]@asig_projections))); - (* 2 *) - by (simp_tac (simpset() addsimps impl_ioas) 1); - by (simp_tac (simpset() addsimps impl_asigs) 1); - by (simp_tac (simpset() addsimps - [asig_of_par, asig_comp_def]@asig_projections) 1); - by (simp_tac rename_ss 1); - (* 1 *) - by (simp_tac (simpset() addsimps impl_ioas) 1); - by (simp_tac (simpset() addsimps impl_asigs) 1); - by (simp_tac (simpset() addsimps - [asig_of_par, asig_comp_def]@asig_projections) 1); -qed "externals_lemma"; - - -val sels = [sbit_def, sq_def, ssending_def, - rbit_def, rq_def, rsending_def]; - - -(* Proof of correctness *) -Goalw [thm "Spec.ioa_def", is_weak_ref_map_def] - "is_weak_ref_map hom (Automata.restrict impl_ioa (externals spec_sig)) \ -\ spec_ioa"; -by (simp_tac (simpset() delcongs [if_weak_cong] delsplits [split_if] - addsimps [thm "Correctness.hom_def", cancel_restrict, - externals_lemma]) 1); -by (rtac conjI 1); - by (simp_tac ss' 1); - by (asm_simp_tac (simpset() addsimps sels) 1); -by (REPEAT(rtac allI 1)); -by (rtac imp_conj_lemma 1); (* from lemmas.ML *) - -by (induct_tac "a" 1); -by (ALLGOALS (asm_simp_tac ss')); -by (ftac inv4 1); -by (Force_tac 1); - -by (ftac inv4 1); -by (ftac inv2 1); -by (etac disjE 1); -by (Asm_simp_tac 1); -by (Force_tac 1); - -by (ftac inv2 1); -by (etac disjE 1); - -by (ftac inv3 1); -by (case_tac "sq(sen(s))=[]" 1); - -by (asm_full_simp_tac ss' 1); -by (blast_tac (claset() addSDs [add_leD1 RS leD]) 1); - -by (case_tac "m = hd(sq(sen(s)))" 1); - -by (Force_tac 1); - -by (Asm_full_simp_tac 1); -by (blast_tac (claset() addSDs [add_leD1 RS leD]) 1); - -by (Asm_full_simp_tac 1); -qed"ntp_correct"; diff -r 1ac610922636 -r c58ef2aa5430 src/HOLCF/IOA/NTP/Correctness.thy --- a/src/HOLCF/IOA/NTP/Correctness.thy Sat May 27 19:49:36 2006 +0200 +++ b/src/HOLCF/IOA/NTP/Correctness.thy Sat May 27 21:00:31 2006 +0200 @@ -14,6 +14,93 @@ "hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s) else tl(sq(sen s)))" -ML {* use_legacy_bindings (the_context ()) *} +ML_setup {* +(* repeated from Traces.ML *) +change_claset (fn cs => cs delSWrapper "split_all_tac") +*} + +lemmas hom_ioas = Spec.ioa_def Spec.trans_def sender_trans_def receiver_trans_def impl_ioas + and impl_asigs = sender_asig_def receiver_asig_def srch_asig_def rsch_asig_def + +declare split_paired_All [simp del] + + +text {* + A lemma about restricting the action signature of the implementation + to that of the specification. +*} + +lemma externals_lemma: + "a:externals(asig_of(Automata.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)" + apply (simp (no_asm) add: externals_def restrict_def restrict_asig_def Spec.sig_def asig_projections) + + apply (induct_tac "a") + apply (simp_all (no_asm) add: actions_def asig_projections) + txt {* 2 *} + apply (simp (no_asm) add: impl_ioas) + apply (simp (no_asm) add: impl_asigs) + apply (simp (no_asm) add: asig_of_par asig_comp_def asig_projections) + apply (simp (no_asm) add: "transitions" unfold_renaming) + txt {* 1 *} + apply (simp (no_asm) add: impl_ioas) + apply (simp (no_asm) add: impl_asigs) + apply (simp (no_asm) add: asig_of_par asig_comp_def asig_projections) + done + +lemmas sels = sbit_def sq_def ssending_def rbit_def rq_def rsending_def + + +text {* Proof of correctness *} +lemma ntp_correct: + "is_weak_ref_map hom (Automata.restrict impl_ioa (externals spec_sig)) spec_ioa" +apply (unfold Spec.ioa_def is_weak_ref_map_def) +apply (simp (no_asm) cong del: if_weak_cong split del: split_if add: Correctness.hom_def + cancel_restrict externals_lemma) +apply (rule conjI) + apply (simp (no_asm) add: hom_ioas) + apply (simp (no_asm_simp) add: sels) +apply (rule allI)+ +apply (rule imp_conj_lemma) + +apply (induct_tac "a") +apply (simp_all (no_asm_simp) add: hom_ioas) +apply (frule inv4) +apply force + +apply (frule inv4) +apply (frule inv2) +apply (erule disjE) +apply (simp (no_asm_simp)) +apply force + +apply (frule inv2) +apply (erule disjE) + +apply (frule inv3) +apply (case_tac "sq (sen (s))=[]") + +apply (simp add: hom_ioas) +apply (blast dest!: add_leD1 [THEN leD]) + +apply (case_tac "m = hd (sq (sen (s)))") + +apply force + +apply simp +apply (blast dest!: add_leD1 [THEN leD]) + +apply simp +done end diff -r 1ac610922636 -r c58ef2aa5430 src/HOLCF/IOA/NTP/Impl.ML --- a/src/HOLCF/IOA/NTP/Impl.ML Sat May 27 19:49:36 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,315 +0,0 @@ -(* Title: HOL/IOA/NTP/Impl.ML - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind - -The implementation --- Invariants. -*) - - -Addsimps [Let_def, le_SucI]; - - -val impl_ioas = - [impl_def, - sender_ioa_def, - receiver_ioa_def, - srch_ioa_thm RS eq_reflection, - rsch_ioa_thm RS eq_reflection]; - -val transitions = [sender_trans_def, receiver_trans_def, - srch_trans_def, rsch_trans_def]; - - -Addsimps [ioa_triple_proj, starts_of_par, trans_of_par4, - in_sender_asig, in_receiver_asig, in_srch_asig, - in_rsch_asig]; -Addcongs [let_weak_cong]; - -Goal - "fst(x) = sen(x) & \ -\ fst(snd(x)) = rec(x) & \ -\ fst(snd(snd(x))) = srch(x) & \ -\ snd(snd(snd(x))) = rsch(x)"; -by (simp_tac (simpset() addsimps - [sen_def,rec_def,srch_def,rsch_def]) 1); -Addsimps [result()]; - -Goal "a:actions(sender_asig) \ -\ | a:actions(receiver_asig) \ -\ | a:actions(srch_asig) \ -\ | a:actions(rsch_asig)"; - by (induct_tac "a" 1); - by (ALLGOALS (Simp_tac)); -Addsimps [result()]; - -Delsimps [split_paired_All]; - - -(* Three Simp_sets in different sizes ----------------------------------------------- - -1) simpset() does not unfold the transition relations -2) ss unfolds transition relations -3) renname_ss unfolds transitions and the abstract channel *) - - -val ss = (simpset() addsimps transitions); -val rename_ss = (ss addsimps unfold_renaming); - -val tac = asm_simp_tac (ss addcongs [conj_cong] addsplits [split_if]); -val tac_ren = asm_simp_tac (rename_ss addcongs [conj_cong] addsplits [split_if]); - - - -(* INVARIANT 1 *) - -Goalw impl_ioas "invariant impl_ioa inv1"; -by (rtac invariantI 1); -by (asm_full_simp_tac (simpset() - addsimps [inv1_def, hdr_sum_def, srcvd_def, - ssent_def, rsent_def,rrcvd_def]) 1); - -by (simp_tac (simpset() delsimps [trans_of_par4] - addsimps [imp_conjR,inv1_def]) 1); - -(* Split proof in two *) -by (rtac conjI 1); - -(* First half *) -by (asm_full_simp_tac (simpset() addsimps [thm "Impl.inv1_def"] - delsplits [split_if]) 1); -by (rtac action.induct 1); - -by (EVERY1[tac, tac, tac, tac]); -by (tac 1); -by (tac_ren 1); - -(* 5 + 1 *) - -by (tac 1); -by (tac_ren 1); - -(* 4 + 1 *) -by (EVERY1[tac, tac, tac, tac]); - - -(* Now the other half *) -by (asm_full_simp_tac (simpset() addsimps [thm "Impl.inv1_def"] - delsplits [split_if]) 1); -by (rtac action.induct 1); -by (EVERY1[tac, tac]); - -(* detour 1 *) -by (tac 1); -by (tac_ren 1); -by (rtac impI 1); -by (REPEAT (etac conjE 1)); -by (asm_simp_tac (simpset() addsimps [hdr_sum_def, Multiset.count_def, - Multiset.countm_nonempty_def] - addsplits [split_if]) 1); -(* detour 2 *) -by (tac 1); -by (tac_ren 1); -by (rtac impI 1); -by (REPEAT (etac conjE 1)); -by (asm_full_simp_tac (simpset() addsimps [thm "Impl.hdr_sum_def", - Multiset.count_def, - Multiset.countm_nonempty_def, - Multiset.delm_nonempty_def] - addsplits [split_if]) 1); -by (rtac allI 1); -by (rtac conjI 1); -by (rtac impI 1); -by (hyp_subst_tac 1); -by (rtac (pred_suc RS iffD1) 1); -by (dtac less_le_trans 1); -by (cut_facts_tac [rewrite_rule[thm "Packet.hdr_def"] - eq_packet_imp_eq_hdr RS countm_props] 1);; -by (assume_tac 1); -by (assume_tac 1); - -by (rtac (countm_done_delm RS mp RS sym) 1); -by (rtac refl 1); -by (asm_simp_tac (simpset() addsimps [Multiset.count_def]) 1); - -by (rtac impI 1); -by (asm_full_simp_tac (simpset() addsimps [neg_flip]) 1); -by (hyp_subst_tac 1); -by (rtac countm_spurious_delm 1); -by (Simp_tac 1); - -by (EVERY1[tac, tac, tac, tac, tac, tac]); - -qed "inv1"; - - - -(* INVARIANT 2 *) - -Goal "invariant impl_ioa inv2"; - - by (rtac invariantI1 1); - (* Base case *) - by (asm_full_simp_tac (simpset() addsimps (inv2_def :: - (receiver_projections - @ sender_projections @ impl_ioas))) - 1); - - by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1); - by (induct_tac "a" 1); - - (* 10 cases. First 4 are simple, since state doesn't change *) - -val tac2 = asm_full_simp_tac (ss addsimps [inv2_def]); - - (* 10 - 7 *) - by (EVERY1[tac2,tac2,tac2,tac2]); - (* 6 *) - by (forward_tac [rewrite_rule [thm "Impl.inv1_def"] - (inv1 RS invariantE) RS conjunct1] 1); - (* 6 - 5 *) - by (EVERY1[tac2,tac2]); - - (* 4 *) - by (forward_tac [rewrite_rule [thm "Impl.inv1_def"] - (inv1 RS invariantE) RS conjunct1] 1); - by (tac2 1); - - (* 3 *) - by (forward_tac [rewrite_rule [thm "Impl.inv1_def"] (inv1 RS invariantE)] 1); - - by (tac2 1); - by (fold_tac [rewrite_rule [thm "Packet.hdr_def"] (thm "Impl.hdr_sum_def")]); - by (arith_tac 1); - - (* 2 *) - by (tac2 1); - by (forward_tac [rewrite_rule [thm "Impl.inv1_def"] - (inv1 RS invariantE) RS conjunct1] 1); - by (strip_tac 1); - by (REPEAT (etac conjE 1)); - by (Asm_full_simp_tac 1); - - (* 1 *) - by (tac2 1); - by (forward_tac [rewrite_rule [thm "Impl.inv1_def"] - (inv1 RS invariantE) RS conjunct2] 1); - by (strip_tac 1); - by (REPEAT (etac conjE 1)); - by (fold_tac [rewrite_rule[thm "Packet.hdr_def"] (thm "Impl.hdr_sum_def")]); - by (Asm_full_simp_tac 1); -qed "inv2"; - - -(* INVARIANT 3 *) - -Goal "invariant impl_ioa inv3"; - - by (rtac invariantI 1); - (* Base case *) - by (asm_full_simp_tac (simpset() addsimps - (thm "Impl.inv3_def" :: (receiver_projections - @ sender_projections @ impl_ioas))) 1); - - by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1); - by (induct_tac "a" 1); - -val tac3 = asm_full_simp_tac (ss addsimps [inv3_def]); - - (* 10 - 8 *) - - by (EVERY1[tac3,tac3,tac3]); - - by (tac_ren 1); - by (strip_tac 1 THEN REPEAT (etac conjE 1)); - by (hyp_subst_tac 1); - by (etac exE 1); - by (Asm_full_simp_tac 1); - - (* 7 *) - by (tac3 1); - by (tac_ren 1); - by (Force_tac 1); - - (* 6 - 3 *) - - by (EVERY1[tac3,tac3,tac3,tac3]); - - (* 2 *) - by (asm_full_simp_tac ss 1); - by (simp_tac (simpset() addsimps [inv3_def]) 1); - by (strip_tac 1 THEN REPEAT (etac conjE 1)); - by (rtac (imp_disjL RS iffD1) 1); - by (rtac impI 1); - by (forward_tac [rewrite_rule [thm "Impl.inv2_def"] (inv2 RS invariantE)] 1); - by (Asm_full_simp_tac 1); - by (REPEAT (etac conjE 1)); - by (res_inst_tac [("j","count (ssent(sen s)) (~sbit(sen s))"), - ("k","count (rsent(rec s)) (sbit(sen s))")] le_trans 1); - by (forward_tac [rewrite_rule [inv1_def] - (inv1 RS invariantE) RS conjunct2] 1); - by (asm_full_simp_tac (simpset() addsimps - [hdr_sum_def, Multiset.count_def]) 1); - by (rtac add_le_mono 1); - by (rtac countm_props 1); - by (Simp_tac 1); - by (rtac countm_props 1); - by (Simp_tac 1); - by (assume_tac 1); - - (* 1 *) - by (tac3 1); - by (strip_tac 1 THEN REPEAT (etac conjE 1)); - by (rtac (imp_disjL RS iffD1) 1); - by (rtac impI 1); - by (forward_tac [rewrite_rule [thm "Impl.inv2_def"] (inv2 RS invariantE)] 1); - by (Asm_full_simp_tac 1); -qed "inv3"; - - -(* INVARIANT 4 *) - -Goal "invariant impl_ioa inv4"; - - by (rtac invariantI 1); - (* Base case *) - by (asm_full_simp_tac (simpset() addsimps - (thm "Impl.inv4_def" :: (receiver_projections - @ sender_projections @ impl_ioas))) 1); - - by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1); - by (induct_tac "a" 1); - -val tac4 = asm_full_simp_tac (ss addsimps [inv4_def]); - - (* 10 - 2 *) - - by (EVERY1[tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4]); - - (* 2 b *) - - by (strip_tac 1 THEN REPEAT (etac conjE 1)); - by (forward_tac [rewrite_rule [thm "Impl.inv2_def"] - (inv2 RS invariantE)] 1); - by (Asm_full_simp_tac 1); - - (* 1 *) - by (tac4 1); - by (strip_tac 1 THEN REPEAT (etac conjE 1)); - by (rtac ccontr 1); - by (forward_tac [rewrite_rule [thm "Impl.inv2_def"] - (inv2 RS invariantE)] 1); - by (forward_tac [rewrite_rule [thm "Impl.inv3_def"] - (inv3 RS invariantE)] 1); - by (Asm_full_simp_tac 1); - by (eres_inst_tac [("x","m")] allE 1); - by (Asm_full_simp_tac 1); -qed "inv4"; - - -(* rebind them *) - -val inv1 = rewrite_rule [thm "Impl.inv1_def"] (inv1 RS invariantE); -val inv2 = rewrite_rule [thm "Impl.inv2_def"] (inv2 RS invariantE); -val inv3 = rewrite_rule [thm "Impl.inv3_def"] (inv3 RS invariantE); -val inv4 = rewrite_rule [thm "Impl.inv4_def"] (inv4 RS invariantE); diff -r 1ac610922636 -r c58ef2aa5430 src/HOLCF/IOA/NTP/Impl.thy --- a/src/HOLCF/IOA/NTP/Impl.thy Sat May 27 19:49:36 2006 +0200 +++ b/src/HOLCF/IOA/NTP/Impl.thy Sat May 27 21:00:31 2006 +0200 @@ -9,11 +9,9 @@ imports Sender Receiver Abschannel begin -types - -'m impl_state -= "'m sender_state * 'm receiver_state * 'm packet multiset * bool multiset" -(* sender_state * receiver_state * srch_state * rsch_state *) +types 'm impl_state + = "'m sender_state * 'm receiver_state * 'm packet multiset * bool multiset" + (* sender_state * receiver_state * srch_state * rsch_state *) consts @@ -29,7 +27,6 @@ hdr_sum :: "'m packet multiset => bool => nat" defs - impl_def: "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)" @@ -71,6 +68,300 @@ (* Lemma 5.4 *) inv4_def: "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) --> sq(sen(s)) ~= []" -ML {* use_legacy_bindings (the_context ()) *} + +subsection {* Invariants *} + +declare Let_def [simp] le_SucI [simp] + +lemmas impl_ioas = + impl_def sender_ioa_def receiver_ioa_def srch_ioa_thm [THEN eq_reflection] + rsch_ioa_thm [THEN eq_reflection] + +lemmas "transitions" = + sender_trans_def receiver_trans_def srch_trans_def rsch_trans_def + + +lemmas [simp] = + ioa_triple_proj starts_of_par trans_of_par4 in_sender_asig + in_receiver_asig in_srch_asig in_rsch_asig + +declare let_weak_cong [cong] + +lemma [simp]: + "fst(x) = sen(x)" + "fst(snd(x)) = rec(x)" + "fst(snd(snd(x))) = srch(x)" + "snd(snd(snd(x))) = rsch(x)" + by (simp_all add: sen_def rec_def srch_def rsch_def) + +lemma [simp]: + "a:actions(sender_asig) + | a:actions(receiver_asig) + | a:actions(srch_asig) + | a:actions(rsch_asig)" + by (induct a) simp_all + +declare split_paired_All [simp del] + + +(* Three Simp_sets in different sizes +---------------------------------------------- + +1) simpset() does not unfold the transition relations +2) ss unfolds transition relations +3) renname_ss unfolds transitions and the abstract channel *) + +ML {* +val ss = simpset() addsimps thms "transitions"; +val rename_ss = ss addsimps thms "unfold_renaming"; + +val tac = asm_simp_tac (ss addcongs [conj_cong] addsplits [split_if]) +val tac_ren = asm_simp_tac (rename_ss addcongs [conj_cong] addsplits [split_if]) +*} + + +subsubsection {* Invariant 1 *} + +lemma inv1: "invariant impl_ioa inv1" + +apply (unfold impl_ioas) +apply (rule invariantI) +apply (simp add: inv1_def hdr_sum_def srcvd_def ssent_def rsent_def rrcvd_def) + +apply (simp (no_asm) del: trans_of_par4 add: imp_conjR inv1_def) + +txt {* Split proof in two *} +apply (rule conjI) + +(* First half *) +apply (simp add: Impl.inv1_def split del: split_if) +apply (induct_tac a) + +apply (tactic "EVERY1[tac, tac, tac, tac]") +apply (tactic "tac 1") +apply (tactic "tac_ren 1") + +txt {* 5 + 1 *} + +apply (tactic "tac 1") +apply (tactic "tac_ren 1") + +txt {* 4 + 1 *} +apply (tactic {* EVERY1[tac, tac, tac, tac] *}) + + +txt {* Now the other half *} +apply (simp add: Impl.inv1_def split del: split_if) +apply (induct_tac a) +apply (tactic "EVERY1 [tac, tac]") + +txt {* detour 1 *} +apply (tactic "tac 1") +apply (tactic "tac_ren 1") +apply (rule impI) +apply (erule conjE)+ +apply (simp (no_asm_simp) add: hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def + split add: split_if) +txt {* detour 2 *} +apply (tactic "tac 1") +apply (tactic "tac_ren 1") +apply (rule impI) +apply (erule conjE)+ +apply (simp add: Impl.hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def + Multiset.delm_nonempty_def split add: split_if) +apply (rule allI) +apply (rule conjI) +apply (rule impI) +apply hypsubst +apply (rule pred_suc [THEN iffD1]) +apply (drule less_le_trans) +apply (cut_tac eq_packet_imp_eq_hdr [unfolded Packet.hdr_def, THEN countm_props]) +apply assumption +apply assumption + +apply (rule countm_done_delm [THEN mp, symmetric]) +apply (rule refl) +apply (simp (no_asm_simp) add: Multiset.count_def) + +apply (rule impI) +apply (simp add: neg_flip) +apply hypsubst +apply (rule countm_spurious_delm) +apply (simp (no_asm)) + +apply (tactic "EVERY1 [tac, tac, tac, tac, tac, tac]") + +done + + + +subsubsection {* INVARIANT 2 *} + +lemma inv2: "invariant impl_ioa inv2" + + apply (rule invariantI1) + txt {* Base case *} + apply (simp add: inv2_def receiver_projections sender_projections impl_ioas) + + apply (simp (no_asm_simp) add: impl_ioas split del: split_if) + apply (induct_tac "a") + + txt {* 10 cases. First 4 are simple, since state doesn't change *} + +ML {* val tac2 = asm_full_simp_tac (ss addsimps [thm "inv2_def"]) *} + + txt {* 10 - 7 *} + apply (tactic "EVERY1 [tac2,tac2,tac2,tac2]") + txt {* 6 *} + apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"] + (thm "inv1" RS invariantE) RS conjunct1] 1 *}) + + txt {* 6 - 5 *} + apply (tactic "EVERY1 [tac2,tac2]") + + txt {* 4 *} + apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"] + (thm "inv1" RS invariantE) RS conjunct1] 1 *}) + apply (tactic "tac2 1") + + txt {* 3 *} + apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"] + (thm "inv1" RS invariantE)] 1 *}) + + apply (tactic "tac2 1") + apply (tactic {* fold_tac [rewrite_rule [thm "Packet.hdr_def"] (thm "Impl.hdr_sum_def")] *}) + apply arith + + txt {* 2 *} + apply (tactic "tac2 1") + apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"] + (thm "inv1" RS invariantE) RS conjunct1] 1 *}) + apply (intro strip) + apply (erule conjE)+ + apply simp + + txt {* 1 *} + apply (tactic "tac2 1") + apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"] + (thm "inv1" RS invariantE) RS conjunct2] 1 *}) + apply (intro strip) + apply (erule conjE)+ + apply (tactic {* fold_tac [rewrite_rule[thm "Packet.hdr_def"] (thm "Impl.hdr_sum_def")] *}) + apply simp + + done + + +subsubsection {* INVARIANT 3 *} + +lemma inv3: "invariant impl_ioa inv3" + + apply (rule invariantI) + txt {* Base case *} + apply (simp add: Impl.inv3_def receiver_projections sender_projections impl_ioas) + + apply (simp (no_asm_simp) add: impl_ioas split del: split_if) + apply (induct_tac "a") + +ML {* val tac3 = asm_full_simp_tac (ss addsimps [thm "inv3_def"]) *} + + txt {* 10 - 8 *} + + apply (tactic "EVERY1[tac3,tac3,tac3]") + + apply (tactic "tac_ren 1") + apply (intro strip, (erule conjE)+) + apply hypsubst + apply (erule exE) + apply simp + + txt {* 7 *} + apply (tactic "tac3 1") + apply (tactic "tac_ren 1") + apply force + + txt {* 6 - 3 *} + + apply (tactic "EVERY1[tac3,tac3,tac3,tac3]") + + txt {* 2 *} + apply (tactic "asm_full_simp_tac ss 1") + apply (simp (no_asm) add: inv3_def) + apply (intro strip, (erule conjE)+) + apply (rule imp_disjL [THEN iffD1]) + apply (rule impI) + apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv2_def"] + (thm "inv2" RS invariantE)] 1 *}) + apply simp + apply (erule conjE)+ + apply (rule_tac j = "count (ssent (sen s)) (~sbit (sen s))" and + k = "count (rsent (rec s)) (sbit (sen s))" in le_trans) + apply (tactic {* forward_tac [rewrite_rule [thm "inv1_def"] + (thm "inv1" RS invariantE) RS conjunct2] 1 *}) + apply (simp add: hdr_sum_def Multiset.count_def) + apply (rule add_le_mono) + apply (rule countm_props) + apply (simp (no_asm)) + apply (rule countm_props) + apply (simp (no_asm)) + apply assumption + + txt {* 1 *} + apply (tactic "tac3 1") + apply (intro strip, (erule conjE)+) + apply (rule imp_disjL [THEN iffD1]) + apply (rule impI) + apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv2_def"] + (thm "inv2" RS invariantE)] 1 *}) + apply simp + done + + +subsubsection {* INVARIANT 4 *} + +lemma inv4: "invariant impl_ioa inv4" + + apply (rule invariantI) + txt {* Base case *} + apply (simp add: Impl.inv4_def receiver_projections sender_projections impl_ioas) + + apply (simp (no_asm_simp) add: impl_ioas split del: split_if) + apply (induct_tac "a") + +ML {* val tac4 = asm_full_simp_tac (ss addsimps [thm "inv4_def"]) *} + + txt {* 10 - 2 *} + + apply (tactic "EVERY1[tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4]") + + txt {* 2 b *} + + apply (intro strip, (erule conjE)+) + apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv2_def"] + (thm "inv2" RS invariantE)] 1 *}) + apply simp + + txt {* 1 *} + apply (tactic "tac4 1") + apply (intro strip, (erule conjE)+) + apply (rule ccontr) + apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv2_def"] + (thm "inv2" RS invariantE)] 1 *}) + apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv3_def"] + (thm "inv3" RS invariantE)] 1 *}) + apply simp + apply (erule_tac x = "m" in allE) + apply simp + done + + +text {* rebind them *} + +ML_setup {* +bind_thm ("inv1", rewrite_rule [thm "Impl.inv1_def"] (thm "inv1" RS thm "invariantE")); +bind_thm ("inv2", rewrite_rule [thm "Impl.inv2_def"] (thm "inv2" RS thm "invariantE")); +bind_thm ("inv3", rewrite_rule [thm "Impl.inv3_def"] (thm "inv3" RS thm "invariantE")); +bind_thm ("inv4", rewrite_rule [thm "Impl.inv4_def"] (thm "inv4" RS thm "invariantE")); +*} end diff -r 1ac610922636 -r c58ef2aa5430 src/HOLCF/IOA/NTP/Lemmas.ML --- a/src/HOLCF/IOA/NTP/Lemmas.ML Sat May 27 19:49:36 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,29 +0,0 @@ -(* Title: HOL/IOA/NTP/Lemmas.ML - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind -*) - -(* Logic *) - -Goal "(X = (~ Y)) = ((~X) = Y)"; - by (Fast_tac 1); -qed "neg_flip"; - - -(* Sets *) -val set_lemmas = - map (fn s => prove_goal Main.thy s (fn _ => [Fast_tac 1])) - ["f(x) : (UN x. {f(x)})", - "f x y : (UN x y. {f x y})", - "!!a. (!x. a ~= f(x)) ==> a ~: (UN x. {f(x)})", - "!!a. (!x y. a ~= f x y) ==> a ~: (UN x y. {f x y})"]; - - -(* Arithmetic *) - -Goal "0 (x - 1 = y) = (x = Suc(y))"; -by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [nat.split]) 1); -qed "pred_suc"; - - -Addsimps (hd_append :: set_lemmas); diff -r 1ac610922636 -r c58ef2aa5430 src/HOLCF/IOA/NTP/Lemmas.thy --- a/src/HOLCF/IOA/NTP/Lemmas.thy Sat May 27 19:49:36 2006 +0200 +++ b/src/HOLCF/IOA/NTP/Lemmas.thy Sat May 27 21:00:31 2006 +0200 @@ -7,5 +7,27 @@ imports Main begin +subsubsection {* Logic *} + +lemma neg_flip: "(X = (~ Y)) = ((~X) = Y)" + by blast + + +subsection {* Sets *} + +lemma set_lemmas: + "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})" + by auto + + +subsection {* Arithmetic *} + +lemma pred_suc: "0 (x - 1 = y) = (x = Suc(y))" + by (simp add: diff_Suc split add: nat.split) + +lemmas [simp] = hd_append set_lemmas + end - diff -r 1ac610922636 -r c58ef2aa5430 src/HOLCF/IOA/NTP/Multiset.ML --- a/src/HOLCF/IOA/NTP/Multiset.ML Sat May 27 19:49:36 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,77 +0,0 @@ -(* Title: HOL/IOA/NTP/Multiset.ML - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind - -Axiomatic multisets. -Should be done as a subtype and moved to a global place. -*) - -Goalw [Multiset.count_def, Multiset.countm_empty_def] - "count {|} x = 0"; - by (rtac refl 1); -qed "count_empty"; - -Goal - "count (addm M x) y = (if y=x then Suc(count M y) else count M y)"; - by (asm_simp_tac (simpset() addsimps - [Multiset.count_def,Multiset.countm_nonempty_def]) 1); -qed "count_addm_simp"; - -Goal "count M y <= count (addm M x) y"; - by (simp_tac (simpset() addsimps [count_addm_simp]) 1); -qed "count_leq_addm"; - -Goalw [Multiset.count_def] - "count (delm M x) y = (if y=x then count M y - 1 else count M y)"; -by (res_inst_tac [("M","M")] Multiset.induction 1); -by (asm_simp_tac (simpset() - addsimps [Multiset.delm_empty_def,Multiset.countm_empty_def]) 1); -by (asm_full_simp_tac (simpset() - addsimps [Multiset.delm_nonempty_def, - Multiset.countm_nonempty_def]) 1); -by Safe_tac; -by (Asm_full_simp_tac 1); -qed "count_delm_simp"; - -Goal "!!M. (!x. P(x) --> Q(x)) ==> (countm M P <= countm M Q)"; -by (res_inst_tac [("M","M")] Multiset.induction 1); - by (simp_tac (simpset() addsimps [Multiset.countm_empty_def]) 1); -by (simp_tac (simpset() addsimps[Multiset.countm_nonempty_def]) 1); -by Auto_tac; -qed "countm_props"; - -Goal "!!P. ~P(obj) ==> countm M P = countm (delm M obj) P"; - by (res_inst_tac [("M","M")] Multiset.induction 1); - by (simp_tac (simpset() addsimps [Multiset.delm_empty_def, - Multiset.countm_empty_def]) 1); - by (asm_simp_tac (simpset() addsimps[Multiset.countm_nonempty_def, - Multiset.delm_nonempty_def]) 1); -qed "countm_spurious_delm"; - - -Goal "!!P. P(x) ==> 0 0 0 countm (delm M x) P = countm M P - 1"; - by (res_inst_tac [("M","M")] Multiset.induction 1); - by (simp_tac (simpset() addsimps - [Multiset.delm_empty_def, - Multiset.countm_empty_def]) 1); - by (asm_simp_tac (simpset() addsimps - [count_addm_simp,Multiset.delm_nonempty_def, - Multiset.countm_nonempty_def,pos_count_imp_pos_countm]) 1); - by (Auto_tac); -qed "countm_done_delm"; - - -Addsimps [count_addm_simp, count_delm_simp, - Multiset.countm_empty_def, Multiset.delm_empty_def, - count_empty]; diff -r 1ac610922636 -r c58ef2aa5430 src/HOLCF/IOA/NTP/Multiset.thy --- a/src/HOLCF/IOA/NTP/Multiset.thy Sat May 27 19:49:36 2006 +0200 +++ b/src/HOLCF/IOA/NTP/Multiset.thy Sat May 27 21:00:31 2006 +0200 @@ -40,8 +40,57 @@ "induction": "[| P({|}); !!M x. P(M) ==> P(addm M x) |] ==> P(M)" -ML {* use_text Context.ml_output true - ("structure Multiset = struct " ^ legacy_bindings (the_context ()) ^ " end") *} -ML {* open Multiset *} +lemma count_empty: + "count {|} x = 0" + by (simp add: Multiset.count_def Multiset.countm_empty_def) + +lemma count_addm_simp: + "count (addm M x) y = (if y=x then Suc(count M y) else count M y)" + by (simp add: Multiset.count_def Multiset.countm_nonempty_def) + +lemma count_leq_addm: "count M y <= count (addm M x) y" + by (simp add: count_addm_simp) + +lemma count_delm_simp: + "count (delm M x) y = (if y=x then count M y - 1 else count M y)" +apply (unfold Multiset.count_def) +apply (rule_tac M = "M" in Multiset.induction) +apply (simp (no_asm_simp) add: Multiset.delm_empty_def Multiset.countm_empty_def) +apply (simp add: Multiset.delm_nonempty_def Multiset.countm_nonempty_def) +apply safe +apply simp +done + +lemma countm_props: "!!M. (!x. P(x) --> Q(x)) ==> (countm M P <= countm M Q)" +apply (rule_tac M = "M" in Multiset.induction) + apply (simp (no_asm) add: Multiset.countm_empty_def) +apply (simp (no_asm) add: Multiset.countm_nonempty_def) +apply auto +done + +lemma countm_spurious_delm: "!!P. ~P(obj) ==> countm M P = countm (delm M obj) P" + apply (rule_tac M = "M" in Multiset.induction) + apply (simp (no_asm) add: Multiset.delm_empty_def Multiset.countm_empty_def) + apply (simp (no_asm_simp) add: Multiset.countm_nonempty_def Multiset.delm_nonempty_def) + done + + +lemma pos_count_imp_pos_countm [rule_format (no_asm)]: "!!P. P(x) ==> 0 0 0 countm (delm M x) P = countm M P - 1" + apply (rule_tac M = "M" in Multiset.induction) + apply (simp (no_asm) add: Multiset.delm_empty_def Multiset.countm_empty_def) + apply (simp (no_asm_simp) add: count_addm_simp Multiset.delm_nonempty_def Multiset.countm_nonempty_def pos_count_imp_pos_countm) + apply auto + done + + +declare count_addm_simp [simp] count_delm_simp [simp] + Multiset.countm_empty_def [simp] Multiset.delm_empty_def [simp] count_empty [simp] end diff -r 1ac610922636 -r c58ef2aa5430 src/HOLCF/IOA/NTP/Packet.ML --- a/src/HOLCF/IOA/NTP/Packet.ML Sat May 27 19:49:36 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,13 +0,0 @@ -(* Title: HOL/IOA/NTP/Packet.ML - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind - -Packets. -*) - -(* Instantiation of a tautology? *) -Goal "!x. x = packet --> hdr(x) = hdr(packet)"; - by (simp_tac (simpset() addsimps [hdr_def]) 1); -qed "eq_packet_imp_eq_hdr"; - -Addsimps [hdr_def,msg_def]; diff -r 1ac610922636 -r c58ef2aa5430 src/HOLCF/IOA/NTP/Packet.thy --- a/src/HOLCF/IOA/NTP/Packet.thy Sat May 27 19:49:36 2006 +0200 +++ b/src/HOLCF/IOA/NTP/Packet.thy Sat May 27 21:00:31 2006 +0200 @@ -18,6 +18,11 @@ msg :: "'msg packet => 'msg" "msg == snd" -ML {* use_legacy_bindings (the_context ()) *} + +text {* Instantiation of a tautology? *} +lemma eq_packet_imp_eq_hdr: "!x. x = packet --> hdr(x) = hdr(packet)" + by simp + +declare hdr_def [simp] msg_def [simp] end diff -r 1ac610922636 -r c58ef2aa5430 src/HOLCF/IOA/NTP/ROOT.ML --- a/src/HOLCF/IOA/NTP/ROOT.ML Sat May 27 19:49:36 2006 +0200 +++ b/src/HOLCF/IOA/NTP/ROOT.ML Sat May 27 21:00:31 2006 +0200 @@ -7,6 +7,4 @@ Mueller. *) -goals_limit := 1; - -time_use_thy "Correctness"; +use_thy "Correctness"; diff -r 1ac610922636 -r c58ef2aa5430 src/HOLCF/IOA/NTP/Receiver.ML --- a/src/HOLCF/IOA/NTP/Receiver.ML Sat May 27 19:49:36 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,26 +0,0 @@ -(* Title: HOL/IOA/NTP/Receiver.ML - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind -*) - -Goal - "S_msg(m) ~: actions(receiver_asig) & \ -\ R_msg(m) : actions(receiver_asig) & \ -\ S_pkt(pkt) ~: actions(receiver_asig) & \ -\ R_pkt(pkt) : actions(receiver_asig) & \ -\ S_ack(b) : actions(receiver_asig) & \ -\ R_ack(b) ~: actions(receiver_asig) & \ -\ C_m_s ~: actions(receiver_asig) & \ -\ C_m_r : actions(receiver_asig) & \ -\ C_r_s ~: actions(receiver_asig) & \ -\ C_r_r(m) : actions(receiver_asig)"; - by (simp_tac (simpset() addsimps (receiver_asig_def :: actions_def :: - asig_projections)) 1); -qed "in_receiver_asig"; - -val receiver_projections = - [rq_def, - rsent_def, - rrcvd_def, - rbit_def, - rsending_def]; diff -r 1ac610922636 -r c58ef2aa5430 src/HOLCF/IOA/NTP/Receiver.thy --- a/src/HOLCF/IOA/NTP/Receiver.thy Sat May 27 19:49:36 2006 +0200 +++ b/src/HOLCF/IOA/NTP/Receiver.thy Sat May 27 21:00:31 2006 +0200 @@ -87,6 +87,19 @@ receiver_ioa_def: "receiver_ioa == (receiver_asig, {([],{|},{|},False,False)}, receiver_trans,{},{})" -ML {* use_legacy_bindings (the_context ()) *} +lemma in_receiver_asig: + "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_all add: receiver_asig_def actions_def asig_projections) + +lemmas receiver_projections = rq_def rsent_def rrcvd_def rbit_def rsending_def end diff -r 1ac610922636 -r c58ef2aa5430 src/HOLCF/IOA/NTP/Sender.ML --- a/src/HOLCF/IOA/NTP/Sender.ML Sat May 27 19:49:36 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,24 +0,0 @@ -(* Title: HOL/IOA/NTP/Sender.ML - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind -*) - -Goal - "S_msg(m) : actions(sender_asig) & \ -\ R_msg(m) ~: actions(sender_asig) & \ -\ S_pkt(pkt) : actions(sender_asig) & \ -\ R_pkt(pkt) ~: actions(sender_asig) & \ -\ S_ack(b) ~: actions(sender_asig) & \ -\ R_ack(b) : actions(sender_asig) & \ -\ C_m_s : actions(sender_asig) & \ -\ C_m_r ~: actions(sender_asig) & \ -\ C_r_s : actions(sender_asig) & \ -\ C_r_r(m) ~: actions(sender_asig)"; -by (simp_tac (simpset() addsimps - (sender_asig_def :: actions_def :: - asig_projections)) 1); -qed "in_sender_asig"; - -val sender_projections = - [sq_def,ssent_def,srcvd_def, - sbit_def,ssending_def]; diff -r 1ac610922636 -r c58ef2aa5430 src/HOLCF/IOA/NTP/Sender.thy --- a/src/HOLCF/IOA/NTP/Sender.thy Sat May 27 19:49:36 2006 +0200 +++ b/src/HOLCF/IOA/NTP/Sender.thy Sat May 27 21:00:31 2006 +0200 @@ -83,6 +83,19 @@ sender_ioa_def: "sender_ioa == (sender_asig, {([],{|},{|},False,True)}, sender_trans,{},{})" -ML {* use_legacy_bindings (the_context ()) *} +lemma in_sender_asig: + "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_all add: sender_asig_def actions_def asig_projections) + +lemmas sender_projections = sq_def ssent_def srcvd_def sbit_def ssending_def end diff -r 1ac610922636 -r c58ef2aa5430 src/HOLCF/IOA/NTP/Spec.thy --- a/src/HOLCF/IOA/NTP/Spec.thy Sat May 27 19:49:36 2006 +0200 +++ b/src/HOLCF/IOA/NTP/Spec.thy Sat May 27 21:00:31 2006 +0200 @@ -40,6 +40,4 @@ ioa_def: "spec_ioa == (spec_sig, {[]}, spec_trans,{},{})" -ML {* use_legacy_bindings (the_context ()) *} - end diff -r 1ac610922636 -r c58ef2aa5430 src/HOLCF/IsaMakefile --- a/src/HOLCF/IsaMakefile Sat May 27 19:49:36 2006 +0200 +++ b/src/HOLCF/IsaMakefile Sat May 27 21:00:31 2006 +0200 @@ -116,13 +116,10 @@ IOA-NTP: IOA $(LOG)/IOA-NTP.gz -$(LOG)/IOA-NTP.gz: $(OUT)/IOA IOA/NTP/Abschannel.ML \ - IOA/NTP/Abschannel.thy IOA/NTP/Action.thy \ - IOA/NTP/Correctness.ML IOA/NTP/Correctness.thy IOA/NTP/Impl.ML \ - IOA/NTP/Impl.thy IOA/NTP/Lemmas.ML IOA/NTP/Lemmas.thy \ - IOA/NTP/Multiset.ML IOA/NTP/Multiset.thy IOA/NTP/Packet.ML \ - IOA/NTP/Packet.thy IOA/NTP/ROOT.ML IOA/NTP/Receiver.ML \ - IOA/NTP/Receiver.thy IOA/NTP/Sender.ML IOA/NTP/Sender.thy \ +$(LOG)/IOA-NTP.gz: $(OUT)/IOA \ + IOA/NTP/Abschannel.thy IOA/NTP/Action.thy IOA/NTP/Correctness.thy \ + IOA/NTP/Impl.thy IOA/NTP/Lemmas.thy IOA/NTP/Multiset.thy \ + IOA/NTP/Packet.thy IOA/NTP/ROOT.ML IOA/NTP/Receiver.thy IOA/NTP/Sender.thy \ IOA/NTP/Spec.thy @cd IOA; $(ISATOOL) usedir $(OUT)/IOA NTP