<commit_before>(*  Title:      HOL/IOA/NTP/Impl.ML
    ID:         $Id$
    Author:     <NAME> & <NAME>
    Copyright   1994  TU Muenchen

The implementation --- Invariants
*)


Addsimps [Let_def];


open Abschannel Impl;

val impl_ioas =
  [Impl.impl_def,
   Sender.sender_ioa_def, 
   Receiver.receiver_ioa_def, 
   srch_ioa_thm RS eq_reflection,
   rsch_ioa_thm RS eq_reflection];

val transitions = [Sender.sender_trans_def, Receiver.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() addcongs [if_weak_cong]
                   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, Sender.srcvd_def,
             Sender.ssent_def, Receiver.rsent_def,Receiver.rrcvd_def]) 1);

by (simp_tac (simpset() delsimps [trans_of_par4]
                addsimps [fork_lemma,inv1_def]) 1);

(* Split proof in two *)
by (rtac conjI 1); 

(* First half *)
by (asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]
                                 delsplits [split_if]) 1);
by (rtac Action.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 [Impl.inv1_def]
                                 delsplits [split_if]) 1);
by (rtac Action.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 [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[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 [Impl.inv1_def]
                               (inv1 RS invariantE) RS conjunct1] 1);
  (* 6 - 5 *)
  by (EVERY1[tac2,tac2]);

  (* 4 *)
  by (forward_tac [rewrite_rule [Impl.inv1_def]
                                (inv1 RS invariantE) RS conjunct1] 1);
  by (tac2 1);
  by(nat_arith_tac 1);

  (* 3 *)
  by (forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE)] 1);

  by (tac2 1);
  by (fold_tac [rewrite_rule [Packet.hdr_def]Impl.hdr_sum_def]);
  by(nat_arith_tac 1);

  (* 2 *)
  by (tac2 1);
  by (forward_tac [rewrite_rule [Impl.inv1_def]
                               (inv1 RS invariantE) RS conjunct1] 1);
  by (strip_tac 1);
  by (REPEAT (etac conjE 1));
  by (Asm_full_simp_tac 1);
<commit_msg>nat_arith_tac -> arith_tac<commit_after>(*  Title:      HOL/IOA/NTP/Impl.ML
    ID:         $Id$
    Author:     <NAME> & <NAME>
    Copyright   1994  TU Muenchen

The implementation --- Invariants
*)


Addsimps [Let_def];


open Abschannel Impl;

val impl_ioas =
  [Impl.impl_def,
   Sender.sender_ioa_def, 
   Receiver.receiver_ioa_def, 
   srch_ioa_thm RS eq_reflection,
   rsch_ioa_thm RS eq_reflection];

val transitions = [Sender.sender_trans_def, Receiver.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() addcongs [if_weak_cong]
                   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, Sender.srcvd_def,
             Sender.ssent_def, Receiver.rsent_def,Receiver.rrcvd_def]) 1);

by (simp_tac (simpset() delsimps [trans_of_par4]
                addsimps [fork_lemma,inv1_def]) 1);

(* Split proof in two *)
by (rtac conjI 1); 

(* First half *)
by (asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]
                                 delsplits [split_if]) 1);
by (rtac Action.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 [Impl.inv1_def]
                                 delsplits [split_if]) 1);
by (rtac Action.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 [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[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 [Impl.inv1_def]
                               (inv1 RS invariantE) RS conjunct1] 1);
  (* 6 - 5 *)
  by (EVERY1[tac2,tac2]);

  (* 4 *)
  by (forward_tac [rewrite_rule [Impl.inv1_def]
                                (inv1 RS invariantE) RS conjunct1] 1);
  by (tac2 1);
  by(arith_tac 1);

  (* 3 *)
  by (forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE)] 1);

  by (tac2 1);
  by (fold_tac [rewrite_rule [Packet.hdr_def]Impl.hdr_sum_def]);
  by(arith_tac 1);

  (* 2 *)
  by (tac2 1);
  by (forward_tac [rewrite_rule [Impl.inv1_def]
                               (inv1 RS invariantE) RS conjunct1] 1);
  by (strip_tac 1);
  by (REPEAT (etac conjE 1));
  by (Asm_full_simp_tac 1);

{'fraction_non_alphanumeric': 0.13363662212112595, 'fraction_numerical': 0.023504881053928537, 'mean_word_length': 2.5915588835942818, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 8, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 20, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5254550', 'n_tokens_mistral': 4498, 'n_tokens_neox': 4170, 'n_words': 995}