--- a/IOA/example/Impl.ML Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,392 +0,0 @@
-(* Title: HOL/IOA/example/Impl.ML
- ID: $Id$
- Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
-
-The implementation --- Invariants
-*)
-
-val impl_ioas =
- [Impl.impl_def,
- Sender.sender_ioa_def,
- Receiver.receiver_ioa_def,
- Channels.srch_ioa_def,
- Channels.rsch_ioa_def];
-
-val transitions = [Sender.sender_trans_def, Receiver.receiver_trans_def,
- Channels.srch_trans_def, Channels.rsch_trans_def];
-
-
-val impl_ss = merge_ss(action_ss,list_ss)
- addcongs [let_weak_cong]
- addsimps [Let_def, ioa_triple_proj, starts_of_par, trans_of_par4,
- in_sender_asig, in_receiver_asig, in_srch_asig,
- in_rsch_asig, count_addm_simp, count_delm_simp,
- Multiset.countm_empty_def, Multiset.delm_empty_def,
- (* Multiset.count_def, *) count_empty,
- Packet.hdr_def, Packet.msg_def];
-
-goal Impl.thy
- "fst(x) = sen(x) & \
-\ fst(snd(x)) = rec(x) & \
-\ fst(snd(snd(x))) = srch(x) & \
-\ snd(snd(snd(x))) = rsch(x)";
-by(simp_tac (HOL_ss addsimps
- [Impl.sen_def,Impl.rec_def,Impl.srch_def,Impl.rsch_def]) 1);
-val impl_ss = impl_ss addsimps [result()];
-
-goal Impl.thy "a:actions(sender_asig) \
-\ | a:actions(receiver_asig) \
-\ | a:actions(srch_asig) \
-\ | a:actions(rsch_asig)";
- by(Action.action.induct_tac "a" 1);
- by(ALLGOALS(simp_tac impl_ss));
-val impl_ss = impl_ss addsimps [result()];
-
-
-(* Instantiation of a tautology? *)
-goal Packet.thy "!x. x = packet --> hdr(x) = hdr(packet)";
- by (simp_tac (HOL_ss addsimps [Packet.hdr_def]) 1);
-qed "eq_packet_imp_eq_hdr";
-
-
-(* INVARIANT 1 *)
-val ss = impl_ss addcongs [if_weak_cong] addsimps transitions;
-
-goalw Impl.thy impl_ioas "invariant(impl_ioa,inv1)";
-br invariantI 1;
-by(asm_full_simp_tac (impl_ss addsimps
- [Impl.inv1_def, Impl.hdr_sum_def,
- Sender.srcvd_def, Sender.ssent_def,
- Receiver.rsent_def,Receiver.rrcvd_def]) 1);
-
-by(simp_tac (HOL_ss addsimps [fork_lemma,Impl.inv1_def]) 1);
-
-(* Split proof in two *)
-by (rtac conjI 1);
-
-(* First half *)
-by(asm_full_simp_tac (impl_ss addsimps [Impl.inv1_def]) 1);
-br Action.action.induct 1;
-
-val tac = asm_simp_tac (ss addcongs [conj_cong]
- addsimps [Suc_pred_lemma]
- setloop (split_tac [expand_if]));
-
-by(EVERY1[tac, tac, tac, tac, tac, tac, tac, tac, tac, tac]);
-
-(* Now the other half *)
-by(asm_full_simp_tac (impl_ss addsimps [Impl.inv1_def]) 1);
-br Action.action.induct 1;
-by(EVERY1[tac, tac]);
-
-(* detour 1 *)
-by (tac 1);
-by (rtac impI 1);
-by (REPEAT (etac conjE 1));
-by (asm_simp_tac (impl_ss addsimps [Impl.hdr_sum_def, Multiset.count_def,
- Multiset.countm_nonempty_def]
- setloop (split_tac [expand_if])) 1);
-(* detour 2 *)
-by (tac 1);
-by (rtac impI 1);
-by (REPEAT (etac conjE 1));
-by (asm_full_simp_tac (impl_ss addsimps
- [Impl.hdr_sum_def,
- Multiset.count_def,
- Multiset.countm_nonempty_def,
- Multiset.delm_nonempty_def,
- left_plus_cancel,left_plus_cancel_inside_succ,
- unzero_less]
- setloop (split_tac [expand_if])) 1);
-by (rtac allI 1);
-by (rtac conjI 1);
-by (rtac impI 1);
-by (hyp_subst_tac 1);
-
-by (rtac (pred_suc RS mp RS sym RS iffD2) 1);
-by (dtac less_le_trans 1);
-by (cut_facts_tac [rewrite_rule[Packet.hdr_def]
- eq_packet_imp_eq_hdr RS countm_props] 1);;
-by (assume_tac 1);
-by (assume_tac 1);
-
-by (rtac (countm_done_delm RS mp RS sym) 1);
-by (rtac refl 1);
-by (asm_simp_tac (HOL_ss addsimps [Multiset.count_def]) 1);
-
-by (rtac impI 1);
-by (asm_full_simp_tac (HOL_ss addsimps [neg_flip]) 1);
-by (hyp_subst_tac 1);
-by (rtac countm_spurious_delm 1);
-by (simp_tac HOL_ss 1);
-
-by (EVERY1[tac, tac, tac, tac, tac, tac]);
-
-qed "inv1";
-
-
-
-(* INVARIANT 2 *)
-
- goal Impl.thy "invariant(impl_ioa, inv2)";
-
- by (rtac invariantI1 1);
- (* Base case *)
- by (asm_full_simp_tac (impl_ss addsimps
- (Impl.inv2_def :: (receiver_projections
- @ sender_projections @ impl_ioas))) 1);
-
- by (asm_simp_tac (impl_ss addsimps impl_ioas) 1);
- by (Action.action.induct_tac "a" 1);
-
- (* 10 cases. First 4 are simple, since state doesn't change wrt. invariant *)
- (* 10 *)
- by (asm_simp_tac (impl_ss addsimps (Impl.inv2_def::transitions)) 1);
- (* 9 *)
- by (asm_simp_tac (impl_ss addsimps (Impl.inv2_def::transitions)) 1);
- (* 8 *)
- by (asm_simp_tac (impl_ss addsimps (Impl.inv2_def::transitions)) 2);
- (* 7 *)
- by (asm_simp_tac (impl_ss addsimps (Impl.inv2_def::transitions)) 3);
- (* 6 *)
- by(forward_tac [rewrite_rule [Impl.inv1_def]
- (inv1 RS invariantE) RS conjunct1] 1);
- by (asm_full_simp_tac (impl_ss addsimps [leq_imp_leq_suc,Impl.inv2_def]
- addsimps transitions) 1);
- (* 5 *)
- by (asm_full_simp_tac (impl_ss addsimps [leq_imp_leq_suc,Impl.inv2_def]
- addsimps transitions) 1);
- (* 4 *)
- by (forward_tac [rewrite_rule [Impl.inv1_def]
- (inv1 RS invariantE) RS conjunct1] 1);
- by (asm_full_simp_tac (impl_ss addsimps [Impl.inv2_def]
- addsimps transitions) 1);
- by (fast_tac (HOL_cs addDs [add_leD1,leD]) 1);
-
- (* 3 *)
- by (forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE)] 1);
-
- by (asm_full_simp_tac (impl_ss addsimps
- (Impl.inv2_def::transitions)) 1);
- by (fold_tac [rewrite_rule [Packet.hdr_def]Impl.hdr_sum_def]);
- by (fast_tac (HOL_cs addDs [add_leD1,leD]) 1);
-
- (* 2 *)
- by (asm_full_simp_tac (impl_ss addsimps
- (Impl.inv2_def::transitions)) 1);
- by(forward_tac [rewrite_rule [Impl.inv1_def]
- (inv1 RS invariantE) RS conjunct1] 1);
- by (rtac impI 1);
- by (rtac impI 1);
- by (REPEAT (etac conjE 1));
- by (dres_inst_tac [("k","count(rsch(s), ~ sbit(sen(s)))")]
- (standard(leq_add_leq RS mp)) 1);
- by (asm_full_simp_tac HOL_ss 1);
-
- (* 1 *)
- by (asm_full_simp_tac (impl_ss addsimps
- (Impl.inv2_def::transitions)) 1);
- by(forward_tac [rewrite_rule [Impl.inv1_def]
- (inv1 RS invariantE) RS conjunct2] 1);
- by (rtac impI 1);
- by (rtac impI 1);
- by (REPEAT (etac conjE 1));
- by (fold_tac [rewrite_rule[Packet.hdr_def]Impl.hdr_sum_def]);
- by (dres_inst_tac [("k","hdr_sum(srch(s), sbit(sen(s)))")]
- (standard(leq_add_leq RS mp)) 1);
- by (asm_full_simp_tac HOL_ss 1);
-qed "inv2";
-
-
-(* INVARIANT 3 *)
-goal Impl.thy "invariant(impl_ioa, inv3)";
-
- by (rtac invariantI 1);
- (* Base case *)
- by (asm_full_simp_tac (impl_ss addsimps
- (Impl.inv3_def :: (receiver_projections
- @ sender_projections @ impl_ioas))) 1);
-
- by (asm_simp_tac (impl_ss addsimps impl_ioas) 1);
- by (Action.action.induct_tac "a" 1);
-
- (* 10 *)
- by (asm_full_simp_tac (impl_ss addsimps
- (append_cons::not_hd_append::Impl.inv3_def::transitions)
- setloop (split_tac [expand_if])) 1);
-
- (* 9 *)
- by (asm_full_simp_tac (impl_ss addsimps
- (append_cons::not_hd_append::Impl.inv3_def::transitions)
- setloop (split_tac [expand_if])) 1);
-
- (* 8 *)
- by (asm_full_simp_tac (impl_ss addsimps
- (append_cons::not_hd_append::Impl.inv3_def::transitions)
- setloop (split_tac [expand_if])) 1);
- by (strip_tac 1 THEN REPEAT (etac conjE 1));
- by (asm_full_simp_tac (HOL_ss addsimps [cons_imp_not_null]) 1);
- by (hyp_subst_tac 1);
- by (etac exE 1);
- by (asm_full_simp_tac list_ss 1);
-
- (* 7 *)
- by (asm_full_simp_tac (impl_ss addsimps
- (Suc_pred_lemma::append_cons::not_hd_append::Impl.inv3_def::transitions)
- setloop (split_tac [expand_if])) 1);
- by (fast_tac HOL_cs 1);
-
- (* 6 *)
- by (asm_full_simp_tac (impl_ss addsimps
- (append_cons::not_hd_append::Impl.inv3_def::transitions)
- setloop (split_tac [expand_if])) 1);
- (* 5 *)
- by (asm_full_simp_tac (impl_ss addsimps
- (append_cons::not_hd_append::Impl.inv3_def::transitions)
- setloop (split_tac [expand_if])) 1);
-
- (* 4 *)
- by (asm_full_simp_tac (impl_ss addsimps
- (append_cons::not_hd_append::Impl.inv3_def::transitions)
- setloop (split_tac [expand_if])) 1);
-
- (* 3 *)
- by (asm_full_simp_tac (impl_ss addsimps
- (append_cons::not_hd_append::Impl.inv3_def::transitions)
- setloop (split_tac [expand_if])) 1);
-
- (* 2 *)
- by (asm_full_simp_tac (impl_ss addsimps transitions) 1);
- by (simp_tac (HOL_ss addsimps [Impl.inv3_def]) 1);
- by (strip_tac 1 THEN REPEAT (etac conjE 1));
- by (rtac (imp_or_lem RS iffD2) 1);
- by (rtac impI 1);
- by (forward_tac [rewrite_rule [Impl.inv2_def] (inv2 RS invariantE)] 1);
- by (asm_full_simp_tac list_ss 1);
- by (REPEAT (etac conjE 1));
- by (res_inst_tac [("j","count(ssent(sen(s)),~ sbit(sen(s)))"),
- ("k","count(rsent(rec(s)), sbit(sen(s)))")] le_trans 1);
- by (forward_tac [rewrite_rule [Impl.inv1_def]
- (inv1 RS invariantE) RS conjunct2] 1);
- by (asm_full_simp_tac (list_ss addsimps
- [Impl.hdr_sum_def, Multiset.count_def]) 1);
- by (rtac (less_eq_add_cong RS mp RS mp) 1);
- by (rtac countm_props 1);
- by (simp_tac (list_ss addsimps [Packet.hdr_def]) 1);
- by (rtac countm_props 1);
- by (simp_tac (list_ss addsimps [Packet.hdr_def]) 1);
- by (assume_tac 1);
-
-
- (* 1 *)
- by (asm_full_simp_tac (impl_ss addsimps
- (append_cons::not_hd_append::Impl.inv3_def::transitions)
- setloop (split_tac [expand_if])) 1);
- by (strip_tac 1 THEN REPEAT (etac conjE 1));
- by (rtac (imp_or_lem RS iffD2) 1);
- by (rtac impI 1);
- by (forward_tac [rewrite_rule [Impl.inv2_def] (inv2 RS invariantE)] 1);
- by (asm_full_simp_tac list_ss 1);
- by (REPEAT (etac conjE 1));
- by (dtac mp 1);
- by (assume_tac 1);
- by (etac allE 1);
- by (dtac (imp_or_lem RS iffD1) 1);
- by (dtac mp 1);
- by (assume_tac 1);
- by (assume_tac 1);
-qed "inv3";
-
-
-
-(* INVARIANT 4 *)
-
-goal Impl.thy "invariant(impl_ioa, inv4)";
-
- by (rtac invariantI 1);
- (* Base case *)
- by (asm_full_simp_tac (impl_ss addsimps
- (Impl.inv4_def :: (receiver_projections
- @ sender_projections @ impl_ioas))) 1);
-
- by (asm_simp_tac (impl_ss addsimps impl_ioas) 1);
- by (Action.action.induct_tac "a" 1);
-
- (* 10 *)
- by (asm_full_simp_tac (impl_ss addsimps
- (append_cons::Impl.inv4_def::transitions)
- setloop (split_tac [expand_if])) 1);
-
- (* 9 *)
- by (asm_full_simp_tac (impl_ss addsimps
- (append_cons::Impl.inv4_def::transitions)
- setloop (split_tac [expand_if])) 1);
-
- (* 8 *)
- by (asm_full_simp_tac (impl_ss addsimps
- (append_cons::Impl.inv4_def::transitions)
- setloop (split_tac [expand_if])) 1);
- (* 7 *)
- by (asm_full_simp_tac (impl_ss addsimps
- (append_cons::Impl.inv4_def::transitions)
- setloop (split_tac [expand_if])) 1);
-
- (* 6 *)
- by (asm_full_simp_tac (impl_ss addsimps
- (append_cons::Impl.inv4_def::transitions)
- setloop (split_tac [expand_if])) 1);
-
- (* 5 *)
- by (asm_full_simp_tac (impl_ss addsimps
- (append_cons::Impl.inv4_def::transitions)
- setloop (split_tac [expand_if])) 1);
-
- (* 4 *)
- by (asm_full_simp_tac (impl_ss addsimps
- (append_cons::Impl.inv4_def::transitions)
- setloop (split_tac [expand_if])) 1);
-
- (* 3 *)
- by (asm_full_simp_tac (impl_ss addsimps
- (append_cons::Impl.inv4_def::transitions)
- setloop (split_tac [expand_if])) 1);
-
- (* 2 *)
- by (asm_full_simp_tac (impl_ss addsimps
- (append_cons::Impl.inv4_def::transitions)
- setloop (split_tac [expand_if])) 1);
-
- by (strip_tac 1 THEN REPEAT (etac conjE 1));
- by(forward_tac [rewrite_rule [Impl.inv2_def]
- (inv2 RS invariantE)] 1);
-
- by (asm_full_simp_tac list_ss 1);
-
- (* 1 *)
- by (asm_full_simp_tac (impl_ss addsimps
- (append_cons::Impl.inv4_def::transitions)
- setloop (split_tac [expand_if])) 1);
- by (strip_tac 1 THEN REPEAT (etac conjE 1));
- by (rtac ccontr 1);
- by(forward_tac [rewrite_rule [Impl.inv2_def]
- (inv2 RS invariantE)] 1);
- by(forward_tac [rewrite_rule [Impl.inv3_def]
- (inv3 RS invariantE)] 1);
- by (asm_full_simp_tac list_ss 1);
- by (eres_inst_tac [("x","m")] allE 1);
- by (dtac less_le_trans 1);
- by (dtac (left_add_leq RS mp) 1);
- by (asm_full_simp_tac list_ss 1);
- by (asm_full_simp_tac arith_ss 1);
-qed "inv4";
-
-
-
-(* rebind them *)
-
-val inv1 = rewrite_rule [Impl.inv1_def] (inv1 RS invariantE);
-val inv2 = rewrite_rule [Impl.inv2_def] (inv2 RS invariantE);
-val inv3 = rewrite_rule [Impl.inv3_def] (inv3 RS invariantE);
-val inv4 = rewrite_rule [Impl.inv4_def] (inv4 RS invariantE);
-