# HG changeset patch # User mueller # Date 816260817 -3600 # Node ID 9a449a91425d10a41090d3630531d1541b417c0c # Parent 6c29cfab679c90140b68f9df63dfebb4cb2b740a *** empty log message *** diff -r 6c29cfab679c -r 9a449a91425d src/HOL/IOA/ABP/Correctness.ML --- a/src/HOL/IOA/ABP/Correctness.ML Sun Nov 12 16:29:12 1995 +0100 +++ b/src/HOL/IOA/ABP/Correctness.ML Mon Nov 13 12:06:57 1995 +0100 @@ -12,6 +12,7 @@ by (fast_tac HOL_cs 1); qed"exis_elim"; +Delsimps [split_paired_All]; 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, diff -r 6c29cfab679c -r 9a449a91425d src/HOL/IOA/NTP/Abschannel.ML --- a/src/HOL/IOA/NTP/Abschannel.ML Sun Nov 12 16:29:12 1995 +0100 +++ b/src/HOL/IOA/NTP/Abschannel.ML Mon Nov 13 12:06:57 1995 +0100 @@ -8,11 +8,11 @@ open Abschannel; -Addsimps - ([srch_asig_def, rsch_asig_def, rsch_ioa_def, srch_ioa_def, ch_ioa_def, +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, asig_of_def, actions_def, srch_trans_def, rsch_trans_def, ch_trans_def,starts_of_def, - trans_of_def] @ asig_projections @ set_lemmas); + trans_of_def] @ asig_projections; goal Abschannel.thy "S_msg(m) ~: actions(srch_asig) & \ @@ -25,7 +25,7 @@ \ C_m_r ~: actions(srch_asig) & \ \ C_r_s ~: actions(srch_asig) & C_r_r(m) ~: actions(srch_asig)"; -by(Simp_tac 1); +by(simp_tac (!simpset addsimps unfold_renaming) 1); qed"in_srch_asig"; goal Abschannel.thy @@ -40,14 +40,14 @@ \ C_r_s ~: actions(rsch_asig) & \ \ C_r_r(m) ~: actions(rsch_asig)"; -by(Simp_tac 1); +by(simp_tac (!simpset addsimps unfold_renaming) 1); qed"in_rsch_asig"; goal Abschannel.thy "srch_ioa = (srch_asig, {{|}}, srch_trans)"; -by (Simp_tac 1); +by(simp_tac (!simpset addsimps unfold_renaming) 1); qed"srch_ioa_thm"; goal Abschannel.thy "rsch_ioa = (rsch_asig, {{|}}, rsch_trans)"; -by (Simp_tac 1); +by(simp_tac (!simpset addsimps unfold_renaming) 1); qed"rsch_ioa_thm"; diff -r 6c29cfab679c -r 9a449a91425d src/HOL/IOA/NTP/Abschannel.thy --- a/src/HOL/IOA/NTP/Abschannel.thy Sun Nov 12 16:29:12 1995 +0100 +++ b/src/HOL/IOA/NTP/Abschannel.thy Mon Nov 13 12:06:57 1995 +0100 @@ -6,7 +6,7 @@ The (faulty) transmission channel (both directions) *) -Abschannel = IOA + Action + Multiset + +Abschannel = IOA + Action + datatype ('a)act = S('a) | R('a) diff -r 6c29cfab679c -r 9a449a91425d src/HOL/IOA/NTP/Correctness.ML --- a/src/HOL/IOA/NTP/Correctness.ML Sun Nov 12 16:29:12 1995 +0100 +++ b/src/HOL/IOA/NTP/Correctness.ML Mon Nov 13 12:06:57 1995 +0100 @@ -6,29 +6,21 @@ The main correctness proof: Impl implements Spec *) -open Impl; -open Spec; + +open Impl Spec; val hom_ioas = [Spec.ioa_def, Spec.trans_def, Sender.sender_trans_def,Receiver.receiver_trans_def] @ impl_ioas; -Addsimps hom_ioas; - val impl_asigs = [Sender.sender_asig_def,Receiver.receiver_asig_def, - Abschannel.srch_asig_def,Abschannel.rsch_asig_def]; + Abschannel.srch_asig_def,Abschannel.rsch_asig_def]; -val ss = - !simpset delsimps ([trans_of_def, starts_of_def, srch_asig_def,rsch_asig_def, - asig_of_def, actions_def, srch_trans_def, rsch_trans_def, - impl_def, srch_ioa_thm, rsch_ioa_thm, srch_ioa_def, - rsch_ioa_def, Sender.sender_trans_def, - Receiver.receiver_trans_def] @ set_lemmas); +(* Two simpsets: - !simpset is basic, ss' unfolds hom_ioas *) -val ss' = !simpset delsimps [trans_of_def, srch_asig_def, rsch_asig_def, - srch_trans_def, rsch_trans_def, asig_of_def, - actions_def] - addcongs [let_weak_cong]; +Delsimps [split_paired_All]; + +val ss' = (!simpset addsimps hom_ioas); (* A lemma about restricting the action signature of the implementation @@ -47,44 +39,50 @@ \ | C_m_r => False \ \ | C_r_s => False \ \ | C_r_r(m) => False)"; - by(simp_tac (ss addcongs [if_weak_cong] - addsimps ([externals_def, restrict_def, - restrict_asig_def, Spec.sig_def])) 1); + by(simp_tac (!simpset 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 (ss addsimps (actions_def :: set_lemmas)))); + by(ALLGOALS(simp_tac (!simpset addsimps [actions_def]@asig_projections))); (* 2 *) - by (simp_tac (ss addsimps impl_ioas) 1); - by (simp_tac (ss addsimps impl_asigs) 1); - by (simp_tac (ss addsimps ([asig_of_par, asig_comp_def])) 1); - by (simp_tac (!simpset delsimps [srch_ioa_thm, rsch_ioa_thm, Let_def]) 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); + by (simp_tac rename_ss 1); (* 1 *) - by (simp_tac (ss addsimps impl_ioas) 1); - by (simp_tac (ss addsimps impl_asigs) 1); - by (simp_tac (ss addsimps ([asig_of_par, asig_comp_def])) 1); - by (simp_tac (!simpset delsimps [srch_ioa_thm, rsch_ioa_thm, Let_def]) 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 = [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 (ss delsimps [trans_def] addsimps - (Correctness.hom_def::[cancel_restrict,externals_lemma])) 1); +by(simp_tac (!simpset addsimps + [Correctness.hom_def, + cancel_restrict,externals_lemma]) 1); br conjI 1; -by(simp_tac (ss addsimps impl_ioas) 1); +by(simp_tac ss' 1); br ballI 1; bd CollectD 1; by(asm_simp_tac (!simpset 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 (ss' setloop (split_tac [expand_if])) 1); by(forward_tac [inv4] 1); -by(asm_full_simp_tac (ss addsimps [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1); +by(asm_full_simp_tac (!simpset addsimps + [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1); by(simp_tac ss' 1); by(simp_tac ss' 1); by(simp_tac ss' 1); @@ -97,8 +95,8 @@ by(forward_tac [inv4] 1); by(forward_tac [inv2] 1); be disjE 1; -by(asm_simp_tac ss 1); -by(asm_full_simp_tac (ss addsimps [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1); +by(Asm_simp_tac 1); +by(asm_full_simp_tac (!simpset addsimps [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1); by(asm_simp_tac ss' 1); by(forward_tac [inv2] 1); @@ -112,11 +110,11 @@ by(case_tac "m = hd(sq(sen(s)))" 1); -by(asm_full_simp_tac (ss addsimps +by(asm_full_simp_tac (!simpset addsimps [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1); -by(asm_full_simp_tac ss 1); +by(Asm_full_simp_tac 1); by(fast_tac (HOL_cs addSDs [add_leD1 RS leD]) 1); -by(asm_full_simp_tac ss 1); +by(Asm_full_simp_tac 1); result(); diff -r 6c29cfab679c -r 9a449a91425d src/HOL/IOA/NTP/Impl.ML --- a/src/HOL/IOA/NTP/Impl.ML Sun Nov 12 16:29:12 1995 +0100 +++ b/src/HOL/IOA/NTP/Impl.ML Mon Nov 13 12:06:57 1995 +0100 @@ -6,7 +6,10 @@ The implementation --- Invariants *) -open Abschannel; + + + +open Abschannel Impl; val impl_ioas = [Impl.impl_def, @@ -16,15 +19,13 @@ rsch_ioa_thm RS eq_reflection]; val transitions = [Sender.sender_trans_def, Receiver.receiver_trans_def, - Abschannel.srch_trans_def, Abschannel.rsch_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, 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]; + in_rsch_asig]; +Addcongs [let_weak_cong]; goal Impl.thy "fst(x) = sen(x) & \ @@ -32,7 +33,7 @@ \ fst(snd(snd(x))) = srch(x) & \ \ snd(snd(snd(x))) = rsch(x)"; by(simp_tac (!simpset addsimps - [Impl.sen_def,Impl.rec_def,Impl.srch_def,Impl.rsch_def]) 1); + [sen_def,rec_def,srch_def,rsch_def]) 1); Addsimps [result()]; goal Impl.thy "a:actions(sender_asig) \ @@ -40,74 +41,83 @@ \ | a:actions(srch_asig) \ \ | a:actions(rsch_asig)"; by(Action.action.induct_tac "a" 1); - by(ALLGOALS (simp_tac (!simpset - delsimps [actions_def,srch_asig_def,rsch_asig_def]))); + 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 addcongs [if_weak_cong] + addsimps transitions); +val rename_ss = (ss addsimps unfold_renaming); + + + +val tac = asm_simp_tac ((ss addcongs [conj_cong]) + setloop (split_tac [expand_if])); +val tac_ren = asm_simp_tac ((rename_ss addcongs [conj_cong]) + setloop (split_tac [expand_if])); + + (* INVARIANT 1 *) -val ss = !simpset addcongs [let_weak_cong] delsimps - [trans_of_def, starts_of_def, srch_asig_def, rsch_asig_def, - asig_of_def, actions_def, srch_trans_def, rsch_trans_def]; goalw Impl.thy impl_ioas "invariant impl_ioa inv1"; br invariantI 1; -by(asm_full_simp_tac (ss - addsimps [Impl.inv1_def, Impl.hdr_sum_def, Sender.srcvd_def, +by(asm_full_simp_tac (!simpset + addsimps [inv1_def, hdr_sum_def, Sender.srcvd_def, Sender.ssent_def, Receiver.rsent_def,Receiver.rrcvd_def]) 1); -by(simp_tac (ss delsimps [trans_of_par4] - addsimps [fork_lemma,Impl.inv1_def]) 1); +by(simp_tac (!simpset delsimps [trans_of_par4] + addsimps [fork_lemma,inv1_def]) 1); (* Split proof in two *) -by (rtac conjI 1); +by (rtac conjI 1); (* First half *) -by(asm_full_simp_tac (ss addsimps [Impl.inv1_def]) 1); +by(asm_full_simp_tac (!simpset addsimps [Impl.inv1_def]) 1); br Action.action.induct 1; -val tac = asm_simp_tac (ss delsimps [srch_ioa_def, rsch_ioa_def] - addcongs [if_weak_cong, conj_cong] - addsimps (Suc_pred_lemma :: transitions) - setloop (split_tac [expand_if])); -val tac_abs = asm_simp_tac (!simpset - delsimps [srch_asig_def, rsch_asig_def, actions_def, - srch_trans_def, rsch_trans_def] - addcongs [if_weak_cong, conj_cong] - addsimps (Suc_pred_lemma :: transitions) - setloop (split_tac [expand_if])); by (EVERY1[tac, tac, tac, tac]); by (tac 1); -by (tac_abs 1); +by (tac_ren 1); (* 5 + 1 *) by (tac 1); -by (tac_abs 1); +by (tac_ren 1); (* 4 + 1 *) by(EVERY1[tac, tac, tac, tac]); (* Now the other half *) -by(asm_full_simp_tac (ss addsimps [Impl.inv1_def]) 1); +by(asm_full_simp_tac (!simpset addsimps [Impl.inv1_def]) 1); br Action.action.induct 1; by(EVERY1[tac, tac]); (* detour 1 *) by (tac 1); -by (tac_abs 1); +by (tac_ren 1); by (rtac impI 1); by (REPEAT (etac conjE 1)); -by (asm_simp_tac (ss addsimps [Impl.hdr_sum_def, Multiset.count_def, - Multiset.countm_nonempty_def] - setloop (split_tac [expand_if])) 1); +by (asm_simp_tac (!simpset addsimps [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 (tac_ren 1); by (rtac impI 1); by (REPEAT (etac conjE 1)); -by (asm_full_simp_tac (ss addsimps [Impl.hdr_sum_def, +by (asm_full_simp_tac (!simpset addsimps [Impl.hdr_sum_def, Multiset.count_def, Multiset.countm_nonempty_def, Multiset.delm_nonempty_def, @@ -128,10 +138,10 @@ by (rtac (countm_done_delm RS mp RS sym) 1); by (rtac refl 1); -by (asm_simp_tac (ss addsimps [Multiset.count_def]) 1); +by (asm_simp_tac (!simpset addsimps [Multiset.count_def]) 1); by (rtac impI 1); -by (asm_full_simp_tac (ss addsimps [neg_flip]) 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); @@ -148,55 +158,41 @@ by (rtac invariantI1 1); (* Base case *) - by (asm_full_simp_tac (ss addsimps (Impl.inv2_def :: - (receiver_projections - @ sender_projections @ impl_ioas))) + by (asm_full_simp_tac (!simpset addsimps (inv2_def :: + (receiver_projections + @ sender_projections @ impl_ioas))) 1); - by (asm_simp_tac (ss addsimps impl_ioas) 1); + by (asm_simp_tac (!simpset 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 (ss delsimps [srch_ioa_def, rsch_ioa_def] - addsimps (Impl.inv2_def::transitions)) 1); - (* 9 *) - by (asm_simp_tac (ss delsimps [srch_ioa_def, rsch_ioa_def] - addsimps (Impl.inv2_def::transitions)) 1); - (* 8 *) - by (asm_simp_tac (ss delsimps [srch_ioa_def, rsch_ioa_def] - addsimps (Impl.inv2_def::transitions)) 2); - (* 7 *) - by (asm_simp_tac (ss delsimps [srch_ioa_def, rsch_ioa_def] - addsimps (Impl.inv2_def::transitions)) 3); + (* 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 [Impl.inv1_def] (inv1 RS invariantE) RS conjunct1] 1); - by (asm_full_simp_tac (ss delsimps [srch_ioa_def, rsch_ioa_def] - addsimps ([leq_imp_leq_suc,Impl.inv2_def] - @ transitions)) 1); - (* 5 *) - by (asm_full_simp_tac (ss delsimps [srch_ioa_def, rsch_ioa_def] - addsimps ([leq_imp_leq_suc,Impl.inv2_def] - @ transitions)) 1); + (* 6 - 5 *) + by (EVERY1[tac2,tac2]); + (* 4 *) by (forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE) RS conjunct1] 1); - by (asm_full_simp_tac (ss delsimps [srch_ioa_def, rsch_ioa_def] - addsimps (Impl.inv2_def :: transitions)) 1); + by (tac2 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 (ss delsimps [srch_ioa_def, rsch_ioa_def] - addsimps (Impl.inv2_def :: transitions)) 1); + by (tac2 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 (ss delsimps [srch_ioa_def, rsch_ioa_def] - addsimps (Impl.inv2_def :: transitions)) 1); + by (tac2 1); by(forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE) RS conjunct1] 1); by (rtac impI 1); @@ -204,11 +200,10 @@ 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 ss 1); + by (Asm_full_simp_tac 1); (* 1 *) - by (asm_full_simp_tac (ss delsimps [srch_ioa_def, rsch_ioa_def] - addsimps (Impl.inv2_def :: transitions)) 1); + by (tac2 1); by(forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE) RS conjunct2] 1); by (rtac impI 1); @@ -217,103 +212,74 @@ 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 ss 1); + by (Asm_full_simp_tac 1); qed "inv2"; (* INVARIANT 3 *) -val ss = ss delsimps [srch_ioa_def, rsch_ioa_def, Packet.hdr_def]; - goal Impl.thy "invariant impl_ioa inv3"; by (rtac invariantI 1); (* Base case *) - by (asm_full_simp_tac (ss addsimps + by (asm_full_simp_tac (!simpset addsimps (Impl.inv3_def :: (receiver_projections @ sender_projections @ impl_ioas))) 1); - by (asm_simp_tac (ss addsimps impl_ioas) 1); + by (asm_simp_tac (!simpset addsimps impl_ioas) 1); by (Action.action.induct_tac "a" 1); - (* 10 *) - by (asm_full_simp_tac (ss - addsimps (append_cons::not_hd_append::Impl.inv3_def::transitions) - setloop (split_tac [expand_if])) 1); +val tac3 = asm_full_simp_tac (ss addsimps [inv3_def] + setloop (split_tac [expand_if])); + + (* 10 - 8 *) - (* 9 *) - by (asm_full_simp_tac (ss - addsimps (append_cons::not_hd_append::Impl.inv3_def::transitions) - setloop (split_tac [expand_if])) 1); - - (* 8 *) - by (asm_full_simp_tac (ss - addsimps (append_cons::not_hd_append::Impl.inv3_def::transitions) - setloop (split_tac [expand_if])) 1); - by (tac_abs 1); + by (EVERY1[tac3,tac3,tac3]); + + by (tac_ren 1); by (strip_tac 1 THEN REPEAT (etac conjE 1)); - by (asm_full_simp_tac (ss addsimps [cons_imp_not_null]) 1); - by (hyp_subst_tac 1); by (etac exE 1); by (Asm_full_simp_tac 1); (* 7 *) - by (asm_full_simp_tac (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 (tac3 1); + by (tac_ren 1); by (fast_tac HOL_cs 1); - (* 6 *) - by (asm_full_simp_tac (ss addsimps - (append_cons::not_hd_append::Impl.inv3_def::transitions) - setloop (split_tac [expand_if])) 1); - (* 5 *) - by (asm_full_simp_tac (ss addsimps - (append_cons::not_hd_append::Impl.inv3_def::transitions) - setloop (split_tac [expand_if])) 1); - (* 4 *) - by (asm_full_simp_tac (ss addsimps - (append_cons::not_hd_append::Impl.inv3_def::transitions) - setloop (split_tac [expand_if])) 1); + (* 6 - 3 *) - (* 3 *) - by (asm_full_simp_tac (ss addsimps - (append_cons::not_hd_append::Impl.inv3_def::transitions) - setloop (split_tac [expand_if])) 1); + by (EVERY1[tac3,tac3,tac3,tac3]); (* 2 *) - by (asm_full_simp_tac (ss addsimps transitions) 1); - by (simp_tac (ss addsimps [Impl.inv3_def]) 1); + 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_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 ss 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 [Impl.inv1_def] + by (forward_tac [rewrite_rule [inv1_def] (inv1 RS invariantE) RS conjunct2] 1); - by (asm_full_simp_tac (ss addsimps - [Impl.hdr_sum_def, Multiset.count_def]) 1); + by (asm_full_simp_tac (!simpset addsimps + [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 (ss addsimps [Packet.hdr_def]) 1); + by (Simp_tac 1); by (rtac countm_props 1); - by (simp_tac (ss addsimps [Packet.hdr_def]) 1); + by (Simp_tac 1); by (assume_tac 1); (* 1 *) - by (asm_full_simp_tac (ss addsimps - (append_cons::not_hd_append::Impl.inv3_def::transitions) - setloop (split_tac [expand_if])) 1); + by (tac3 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 ss 1); + by (Asm_full_simp_tac 1); by (REPEAT (etac conjE 1)); by (dtac mp 1); by (assume_tac 1); @@ -331,57 +297,30 @@ by (rtac invariantI 1); (* Base case *) - by (asm_full_simp_tac (ss addsimps + by (asm_full_simp_tac (!simpset addsimps (Impl.inv4_def :: (receiver_projections @ sender_projections @ impl_ioas))) 1); - by (asm_simp_tac (ss addsimps impl_ioas) 1); + by (asm_simp_tac (!simpset addsimps impl_ioas) 1); by (Action.action.induct_tac "a" 1); - (* 10 *) - by (asm_full_simp_tac (ss addsimps (append_cons::Impl.inv4_def::transitions) - setloop (split_tac [expand_if])) 1); - - (* 9 *) - by (asm_full_simp_tac (ss addsimps (append_cons::Impl.inv4_def::transitions) - setloop (split_tac [expand_if])) 1); - - (* 8 *) - by (asm_full_simp_tac (ss addsimps (append_cons::Impl.inv4_def::transitions) - setloop (split_tac [expand_if])) 1); - (* 7 *) - by (asm_full_simp_tac (ss addsimps (append_cons::Impl.inv4_def::transitions) - setloop (split_tac [expand_if])) 1); +val tac4 = asm_full_simp_tac (ss addsimps [inv4_def] + setloop (split_tac [expand_if])); - (* 6 *) - by (asm_full_simp_tac (ss addsimps (append_cons::Impl.inv4_def::transitions) - setloop (split_tac [expand_if])) 1); - - (* 5 *) - by (asm_full_simp_tac (ss addsimps (append_cons::Impl.inv4_def::transitions) - setloop (split_tac [expand_if])) 1); - - (* 4 *) - by (asm_full_simp_tac (ss addsimps (append_cons::Impl.inv4_def::transitions) - setloop (split_tac [expand_if])) 1); - - (* 3 *) - by (asm_full_simp_tac (ss addsimps (append_cons::Impl.inv4_def::transitions) - setloop (split_tac [expand_if])) 1); - - (* 2 *) - by (asm_full_simp_tac (ss addsimps (append_cons::Impl.inv4_def::transitions) - setloop (split_tac [expand_if])) 1); - + (* 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 [Impl.inv2_def] (inv2 RS invariantE)] 1); - + by (tac4 1); by (Asm_full_simp_tac 1); (* 1 *) - by (asm_full_simp_tac (ss addsimps (append_cons::Impl.inv4_def::transitions) - setloop (split_tac [expand_if])) 1); + by (tac4 1); by (strip_tac 1 THEN REPEAT (etac conjE 1)); by (rtac ccontr 1); by(forward_tac [rewrite_rule [Impl.inv2_def] diff -r 6c29cfab679c -r 9a449a91425d src/HOL/IOA/NTP/Lemmas.ML --- a/src/HOL/IOA/NTP/Lemmas.ML Sun Nov 12 16:29:12 1995 +0100 +++ b/src/HOL/IOA/NTP/Lemmas.ML Mon Nov 13 12:06:57 1995 +0100 @@ -59,21 +59,6 @@ by (REPEAT(Simp_tac 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 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 (!simpset 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 1); @@ -102,7 +87,7 @@ goal Arith.thy "(x::nat)<= y --> x<=y+k"; by (nat_ind_tac "k" 1); by (Simp_tac 1); - by (asm_full_simp_tac (!simpset addsimps [leq_suc]) 1); + by (Asm_full_simp_tac 1); qed "leq_add_leq"; goal Arith.thy "(x::nat) + y <= z --> x <= z"; @@ -167,10 +152,6 @@ by (safe_tac HOL_cs); by (fast_tac HOL_cs 2); by (asm_simp_tac (!simpset addsimps [suc_not_zero]) 1); - by (rtac ccontr 1); - by (asm_full_simp_tac (!simpset addsimps [suc_not_zero]) 1); - by (hyp_subst_tac 1); - by (Asm_full_simp_tac 1); qed "suc_leq_suc"; goal Arith.thy "~0 n = 0"; @@ -229,12 +210,6 @@ 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"; +Addsimps ([append_cons,not_hd_append,Suc_pred_lemma] @ set_lemmas); \ No newline at end of file diff -r 6c29cfab679c -r 9a449a91425d src/HOL/IOA/NTP/Multiset.ML --- a/src/HOL/IOA/NTP/Multiset.ML Sun Nov 12 16:29:12 1995 +0100 +++ b/src/HOL/IOA/NTP/Multiset.ML Mon Nov 13 12:06:57 1995 +0100 @@ -22,8 +22,6 @@ goal Multiset.thy "count M y <= count (addm M x) y"; by (simp_tac (!simpset 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] @@ -82,3 +80,8 @@ suc_pred_id] setloop (split_tac [expand_if])) 1); qed "countm_done_delm"; + + +Addsimps [count_addm_simp, count_delm_simp, + Multiset.countm_empty_def, Multiset.delm_empty_def, + count_empty]; \ No newline at end of file diff -r 6c29cfab679c -r 9a449a91425d src/HOL/IOA/NTP/Multiset.thy --- a/src/HOL/IOA/NTP/Multiset.thy Sun Nov 12 16:29:12 1995 +0100 +++ b/src/HOL/IOA/NTP/Multiset.thy Mon Nov 13 12:06:57 1995 +0100 @@ -7,7 +7,7 @@ Should be done as a subtype and moved to a global place. *) -Multiset = Arith + "Lemmas" + +Multiset = Arith + Lemmas + types diff -r 6c29cfab679c -r 9a449a91425d src/HOL/IOA/NTP/Packet.ML --- a/src/HOL/IOA/NTP/Packet.ML Sun Nov 12 16:29:12 1995 +0100 +++ b/src/HOL/IOA/NTP/Packet.ML Mon Nov 13 12:06:57 1995 +0100 @@ -10,4 +10,6 @@ (* Instantiation of a tautology? *) goal Packet.thy "!x. x = packet --> hdr(x) = hdr(packet)"; by (simp_tac (!simpset addsimps [Packet.hdr_def]) 1); -qed "eq_packet_imp_eq_hdr"; \ No newline at end of file +qed "eq_packet_imp_eq_hdr"; + +Addsimps [Packet.hdr_def,Packet.msg_def]; diff -r 6c29cfab679c -r 9a449a91425d src/HOL/IOA/NTP/Packet.thy --- a/src/HOL/IOA/NTP/Packet.thy Sun Nov 12 16:29:12 1995 +0100 +++ b/src/HOL/IOA/NTP/Packet.thy Mon Nov 13 12:06:57 1995 +0100 @@ -6,7 +6,7 @@ Packets *) -Packet = Arith + +Packet = Arith + Multiset + types diff -r 6c29cfab679c -r 9a449a91425d src/HOL/IOA/NTP/Receiver.ML --- a/src/HOL/IOA/NTP/Receiver.ML Sun Nov 12 16:29:12 1995 +0100 +++ b/src/HOL/IOA/NTP/Receiver.ML Mon Nov 13 12:06:57 1995 +0100 @@ -16,7 +16,7 @@ \ C_r_s ~: actions(receiver_asig) & \ \ C_r_r(m) : actions(receiver_asig)"; by(simp_tac (!simpset addsimps (Receiver.receiver_asig_def :: actions_def :: - asig_projections @ set_lemmas)) 1); + asig_projections)) 1); qed "in_receiver_asig"; val receiver_projections = diff -r 6c29cfab679c -r 9a449a91425d src/HOL/IOA/NTP/Receiver.thy --- a/src/HOL/IOA/NTP/Receiver.thy Sun Nov 12 16:29:12 1995 +0100 +++ b/src/HOL/IOA/NTP/Receiver.thy Mon Nov 13 12:06:57 1995 +0100 @@ -6,7 +6,7 @@ The implementation: receiver *) -Receiver = List + IOA + Action + Multiset + +Receiver = List + IOA + Action + types diff -r 6c29cfab679c -r 9a449a91425d src/HOL/IOA/NTP/Sender.ML --- a/src/HOL/IOA/NTP/Sender.ML Sun Nov 12 16:29:12 1995 +0100 +++ b/src/HOL/IOA/NTP/Sender.ML Mon Nov 13 12:06:57 1995 +0100 @@ -17,7 +17,7 @@ \ C_r_r(m) ~: actions(sender_asig)"; by(simp_tac (!simpset addsimps (Sender.sender_asig_def :: actions_def :: - asig_projections @ set_lemmas)) 1); + asig_projections)) 1); qed "in_sender_asig"; val sender_projections = diff -r 6c29cfab679c -r 9a449a91425d src/HOL/IOA/NTP/Sender.thy --- a/src/HOL/IOA/NTP/Sender.thy Sun Nov 12 16:29:12 1995 +0100 +++ b/src/HOL/IOA/NTP/Sender.thy Mon Nov 13 12:06:57 1995 +0100 @@ -6,7 +6,7 @@ The implementation: sender *) -Sender = IOA + Action + Multiset + List + +Sender = IOA + Action + List + types diff -r 6c29cfab679c -r 9a449a91425d src/HOL/IOA/ROOT_NTP.ML --- a/src/HOL/IOA/ROOT_NTP.ML Sun Nov 12 16:29:12 1995 +0100 +++ b/src/HOL/IOA/ROOT_NTP.ML Mon Nov 13 12:06:57 1995 +0100 @@ -33,4 +33,6 @@ loadpath := ["IOA/meta_theory","IOA/NTP"]; use_thy "Correctness"; + make_chart (); (*make HTML chart*) +