diff -r 722bf1319be5 -r fd1be45b64bf IOA/example/Impl.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/IOA/example/Impl.ML Wed Nov 02 11:50:09 1994 +0100 @@ -0,0 +1,385 @@ +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); +val eq_packet_imp_eq_hdr = result(); + + +(* 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 (dmatch_tac [less_leq_less RS mp] 1); +by (cut_facts_tac [rewrite_rule[Packet.hdr_def] + eq_packet_imp_eq_hdr RS countm_props] 1);; +by (dtac mp 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]); + +val inv1 = result(); + + + +(* 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 [plus_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 [plus_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); +val inv2 = result(); + + +(* 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); +val inv3 = result(); + + + +(* 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_leq_less RS mp RS mp) 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); +val inv4 = result(); + + + +(* 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); +