--- 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,
--- 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";
--- 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)
--- 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();
--- 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]
--- 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 --> 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
--- 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
--- 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
--- 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];
--- 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
--- 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 =
--- 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
--- 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 =
--- 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
--- 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*)
+