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

The main correctness proof: Impl implements Spec
*)

(* repeated from Traces.ML *)
claset_ref() := claset() delSWrapper "split_all_tac";


val hom_ioas = [Spec.ioa_def, Spec.trans_def,
                Sender.sender_trans_def,Receiver.receiver_trans_def]
               @ impl_ioas;

val impl_asigs = [Sender.sender_asig_def,Receiver.receiver_asig_def,
                  Abschannel.srch_asig_def,Abschannel.rsch_asig_def];

(* Two simpsets: - simpset() is basic, ss' unfolds hom_ioas *)

Delsimps [split_paired_All];

val ss' = (simpset() addsimps hom_ioas);


(* A lemma about restricting the action signature of the implementation
 * to that of the specification.
 ****************************)
Goal
 "a:externals(asig_of(restrict impl_ioa (externals spec_sig))) = \
\ (case a of                  \
\     S_msg(m) => True        \
\   | R_msg(m) => True        \
\   | S_pkt(pkt) => False  \
\   | R_pkt(pkt) => False  \
\   | S_ack(b) => False    \
\   | R_ack(b) => False    \
\   | C_m_s => False          \
\   | C_m_r => False          \
\   | C_r_s => False          \
\   | C_r_r(m) => False)";
 by (simp_tac (simpset() addsimps ([externals_def, restrict_def,
                            restrict_asig_def, Spec.sig_def]
                            @asig_projections)) 1);

  by (induct_tac "a" 1);
  by (ALLGOALS(simp_tac (simpset() addsimps [actions_def]@asig_projections)));
 (* 2 *)
  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 (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 [Spec.ioa_def, is_weak_ref_map_def]
  "is_weak_ref_map hom (restrict impl_ioa (externals spec_sig)) spec_ioa";
by (simp_tac (simpset() delsplits [split_if] addsimps 
    [Correctness.hom_def, cancel_restrict, externals_lemma]) 1);
by (rtac conjI 1);
 by (simp_tac ss' 1);
 by (asm_simp_tac (simpset() addsimps sels) 1);
by (REPEAT(rtac allI 1));
by (rtac imp_conj_lemma 1);   (* from lemmas.ML *)

by (induct_tac "a"  1);
by (asm_simp_tac (ss' addsplits [split_if]) 1);
by (forward_tac [inv4] 1);
by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1);
by (simp_tac ss' 1);
by (simp_tac ss' 1);
by (simp_tac ss' 1);
by (simp_tac ss' 1);
by (simp_tac ss' 1);
by (simp_tac ss' 1);
by (simp_tac ss' 1);

by (asm_simp_tac ss' 1);
by (forward_tac [inv4] 1);
by (forward_tac [inv2] 1);
by (etac disjE 1);
by (Asm_simp_tac 1);
by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1);

by (asm_simp_tac ss' 1);
by (forward_tac [inv2] 1);
by (etac disjE 1);

by (forward_tac [inv3] 1);
by (case_tac "sq(sen(s))=[]" 1);

by (asm_full_simp_tac ss' 1);
by (fast_tac (claset() addSDs [add_leD1 RS leD]) 1);

by (case_tac "m = hd(sq(sen(s)))" 1);

by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1);

by (Asm_full_simp_tac 1);
by (fast_tac (claset() addSDs [add_leD1 RS leD]) 1);

by (Asm_full_simp_tac 1);
qed"ntp_correct";
<commit_msg>qualified the name "restrict" since Fun.restrict exists too<commit_after>(*  Title:      HOL/IOA/NTP/Correctness.ML
    ID:         $Id$
    Author:     <NAME> & <NAME>
    Copyright   1994  TU Muenchen

The main correctness proof: Impl implements Spec
*)

(* repeated from Traces.ML *)
claset_ref() := claset() delSWrapper "split_all_tac";


val hom_ioas = [Spec.ioa_def, Spec.trans_def,
                Sender.sender_trans_def,Receiver.receiver_trans_def]
               @ impl_ioas;

val impl_asigs = [Sender.sender_asig_def,Receiver.receiver_asig_def,
                  Abschannel.srch_asig_def,Abschannel.rsch_asig_def];

(* Two simpsets: - simpset() is basic, ss' unfolds hom_ioas *)

Delsimps [split_paired_All];

val ss' = (simpset() addsimps hom_ioas);


(* A lemma about restricting the action signature of the implementation
 * to that of the specification.
 ****************************)
Goal
 "a:externals(asig_of(Automata.restrict impl_ioa (externals spec_sig))) = \
\ (case a of                  \
\     S_msg(m) => True        \
\   | R_msg(m) => True        \
\   | S_pkt(pkt) => False  \
\   | R_pkt(pkt) => False  \
\   | S_ack(b) => False    \
\   | R_ack(b) => False    \
\   | C_m_s => False          \
\   | C_m_r => False          \
\   | C_r_s => False          \
\   | C_r_r(m) => False)";
 by (simp_tac (simpset() addsimps ([externals_def, restrict_def,
                            restrict_asig_def, Spec.sig_def]
                            @asig_projections)) 1);

  by (induct_tac "a" 1);
  by (ALLGOALS(simp_tac (simpset() addsimps [actions_def]@asig_projections)));
 (* 2 *)
  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 (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 [Spec.ioa_def, is_weak_ref_map_def]
  "is_weak_ref_map hom (Automata.restrict impl_ioa (externals spec_sig))  \
\                  spec_ioa";
by (simp_tac (simpset() delsplits [split_if] addsimps 
    [Correctness.hom_def, cancel_restrict, externals_lemma]) 1);
by (rtac conjI 1);
 by (simp_tac ss' 1);
 by (asm_simp_tac (simpset() addsimps sels) 1);
by (REPEAT(rtac allI 1));
by (rtac imp_conj_lemma 1);   (* from lemmas.ML *)

by (induct_tac "a"  1);
by (asm_simp_tac (ss' addsplits [split_if]) 1);
by (forward_tac [inv4] 1);
by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1);
by (simp_tac ss' 1);
by (simp_tac ss' 1);
by (simp_tac ss' 1);
by (simp_tac ss' 1);
by (simp_tac ss' 1);
by (simp_tac ss' 1);
by (simp_tac ss' 1);

by (asm_simp_tac ss' 1);
by (forward_tac [inv4] 1);
by (forward_tac [inv2] 1);
by (etac disjE 1);
by (Asm_simp_tac 1);
by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1);

by (asm_simp_tac ss' 1);
by (forward_tac [inv2] 1);
by (etac disjE 1);

by (forward_tac [inv3] 1);
by (case_tac "sq(sen(s))=[]" 1);

by (asm_full_simp_tac ss' 1);
by (fast_tac (claset() addSDs [add_leD1 RS leD]) 1);

by (case_tac "m = hd(sq(sen(s)))" 1);

by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1);

by (Asm_full_simp_tac 1);
by (fast_tac (claset() addSDs [add_leD1 RS leD]) 1);

by (Asm_full_simp_tac 1);
qed"ntp_correct";

{'fraction_non_alphanumeric': 0.14991648106904232, 'fraction_numerical': 0.01586859688195991, 'mean_word_length': 3.432449105490438, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 27, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3930347', 'n_tokens_mistral': 3207, 'n_tokens_neox': 3042, 'n_words': 709}