--- 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";
--- 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
--- 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
--- 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";
--- 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
--- 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);
--- 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
--- 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 ==> (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);
--- 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 ==> (x - 1 = y) = (x = Suc(y))"
+ by (simp add: diff_Suc split add: nat.split)
+
+lemmas [simp] = hd_append set_lemmas
+
end
-
--- 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<count M x --> 0<countm M P";
- by (res_inst_tac [("M","M")] Multiset.induction 1);
- by (simp_tac (simpset() addsimps
- [Multiset.delm_empty_def,Multiset.count_def,
- Multiset.countm_empty_def]) 1);
- by (asm_simp_tac (simpset() addsimps
- [Multiset.count_def,Multiset.delm_nonempty_def,
- Multiset.countm_nonempty_def]) 1);
-qed_spec_mp "pos_count_imp_pos_countm";
-
-Goal
- "!!P. P(x) ==> 0<count M x --> 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];
--- 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<count M x --> 0<countm M P"
+ apply (rule_tac M = "M" in Multiset.induction)
+ apply (simp (no_asm) add: Multiset.delm_empty_def Multiset.count_def Multiset.countm_empty_def)
+ apply (simp (no_asm_simp) add: Multiset.count_def Multiset.delm_nonempty_def Multiset.countm_nonempty_def)
+ done
+
+lemma countm_done_delm:
+ "!!P. P(x) ==> 0<count M x --> 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
--- 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];
--- 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
--- 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";
--- 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];
--- 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
--- 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];
--- 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
--- 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
--- 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