# File Correctness.ML

    (*  Title:      HOLCF/IOA/ABP/Correctness.ML
        ID:         $Id: Correctness.ML,v 1.20 2005/09/03 14:50:22 wenzelm Exp $
        Author:     Olaf Müller
    *)

    Delsimps [split_paired_All,Collect_empty_eq];
    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, rename_set_def, asig_of_def,
       actions_def, exis_elim, srch_trans_def, rsch_trans_def, ch_trans_def,
       trans_of_def] @ asig_projections @ set_lemmas);

    val abschannel_fin = [srch_fin_asig_def, rsch_fin_asig_def,
                          rsch_fin_ioa_def, srch_fin_ioa_def,
                          ch_fin_ioa_def,ch_fin_trans_def,ch_fin_asig_def];
    Addsimps abschannel_fin;

    val impl_ioas =  [sender_ioa_def,receiver_ioa_def];
    val impl_trans = [sender_trans_def,receiver_trans_def];
    val impl_asigs = [sender_asig_def,receiver_asig_def];
    Addcongs [let_weak_cong];
    Addsimps [Let_def, ioa_triple_proj, starts_of_par];

    val env_ioas = [env_ioa_def,env_asig_def,env_trans_def];
    val hom_ioas = env_ioas @ impl_ioas @ impl_trans @ impl_asigs @
                   asig_projections @ set_lemmas;
    Addsimps hom_ioas;

    (* auxiliary function *)
    fun rotate n i = EVERY(replicate n (etac revcut_rl i));

    (* lemmas about reduce *)

    Goal "(reduce(l)=[]) = (l=[])";
    by (induct_tac "l" 1);
    by (auto_tac (claset(), simpset() addsplits [thm"list.split"]));
    val l_iff_red_nil = result();

    Goal "s~=[] --> hd(s)=hd(reduce(s))";
    by (induct_tac "s" 1);
    by (auto_tac (claset(), simpset() addsplits [thm"list.split"]));
    qed"hd_is_reduce_hd";

    (* to be used in the following Lemma *)
    Goal "l~=[] --> reverse(reduce(l))~=[]";
    by (induct_tac "l" 1);
    by (auto_tac (claset(), simpset() addsplits [thm"list.split"]));
    qed_spec_mp "rev_red_not_nil";

    (* shows applicability of the induction hypothesis of the following Lemma 1 *)
    Goal "l~=[] ==> hd(reverse(reduce(a#l))) = hd(reverse(reduce(l)))";
     by (Simp_tac 1);
     by (auto_tac (claset(), HOL_ss addsplits [thm"list.split"]
                                    addsimps (reverse.simps @ [hd_append,
    					  rev_red_not_nil])));
    qed"last_ind_on_first";

    val impl_ss = simpset() delsimps [reduce.reduce_Cons];

    (* Main Lemma 1 for S_pkt in showing that reduce is refinement  *)
    Goal
       "if x=hd(reverse(reduce(l))) & reduce(l)~=[] then   \
    \      reduce(l@[x])=reduce(l) else                  \
    \      reduce(l@[x])=reduce(l)@[x]";
    by (stac split_if 1);
    by (rtac conjI 1);
    (* --> *)
    by (induct_tac "l" 1);
    by (Simp_tac 1);
    by (case_tac "list=[]" 1);
     by (asm_full_simp_tac (simpset() addsimps reverse.simps) 1);
     by (rtac impI 1);
    by (Simp_tac 1);
    by (cut_inst_tac [("l","list")] cons_not_nil 1);
     by (asm_full_simp_tac impl_ss 1);
     by (REPEAT (etac exE 1));
     by (hyp_subst_tac 1);
    by (asm_full_simp_tac (impl_ss addsimps [last_ind_on_first,l_iff_red_nil]) 1);
    (* <-- *)
    by (simp_tac (simpset() addsimps [and_de_morgan_and_absorbe,l_iff_red_nil]) 1);
    by (induct_tac "l" 1);
    by (Simp_tac 1);
    by (case_tac "list=[]" 1);
    by (cut_inst_tac [("l","list")] cons_not_nil 2);
    by (Asm_full_simp_tac 1);
    by (auto_tac (claset(),
    	      impl_ss addsimps [last_ind_on_first,l_iff_red_nil]
                          setloop split_tac [split_if]));
    by (Asm_full_simp_tac 1);
    qed"reduce_hd";

    (* Main Lemma 2 for R_pkt in showing that reduce is refinement *)
    Goal "s~=[] ==>  \
    \    if hd(s)=hd(tl(s)) & tl(s)~=[] then    \
    \      reduce(tl(s))=reduce(s) else      \
    \      reduce(tl(s))=tl(reduce(s))";
    by (cut_inst_tac [("l","s")] cons_not_nil 1);
    by (Asm_full_simp_tac 1);
    by (REPEAT (etac exE 1));
    by (auto_tac (claset(), simpset() addsplits [thm"list.split"]));
    val reduce_tl =result();

    (*******************************************************************
              C h a n n e l   A b s t r a c t i o n
     *******************************************************************)

    Delsplits [split_if];

    Goal "is_weak_ref_map reduce ch_ioa ch_fin_ioa";
    by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
    (* ---------------- main-part ------------------- *)
    by (REPEAT (rtac allI 1));
    by (rtac imp_conj_lemma 1);
    by (induct_tac "a" 1);
    (* ----------------- 2 cases ---------------------*)
    by (ALLGOALS (simp_tac (simpset() delcongs [if_weak_cong]
    				  addsimps [externals_def])));
    (* fst case --------------------------------------*)
     by (rtac impI 1);
     by (rtac disjI2 1);
    by (rtac reduce_hd 1);
    (* snd case --------------------------------------*)
     by (rtac impI 1);
     by (REPEAT (etac conjE 1));
     by (etac disjE 1);
    by (asm_full_simp_tac (simpset() addsimps [l_iff_red_nil]) 1);
    by (etac (hd_is_reduce_hd RS mp) 1);
    by (asm_full_simp_tac (simpset() addsimps [l_iff_red_nil]) 1);
    by (rtac conjI 1);
    by (etac (hd_is_reduce_hd RS mp) 1);
    by (rtac (bool_if_impl_or RS mp) 1);
    by (etac reduce_tl 1);
    qed"channel_abstraction";

    Addsplits [split_if];

    Goal "is_weak_ref_map reduce srch_ioa srch_fin_ioa";
    by (simp_tac (HOL_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def,
     srch_ioa_def,rsch_ioa_def,rename_through_pmap,channel_abstraction]) 1);
    qed"sender_abstraction";

    Goal "is_weak_ref_map reduce rsch_ioa rsch_fin_ioa";
    by (simp_tac (HOL_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def,
     srch_ioa_def,rsch_ioa_def,rename_through_pmap,channel_abstraction]) 1);
    qed"receiver_abstraction";

    (* 3 thms that do not hold generally! The lucky restriction here is
       the absence of internal actions. *)
    Goal "is_weak_ref_map (%id. id) sender_ioa sender_ioa";
    by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
    (* main-part *)
    by (REPEAT (rtac allI 1));
    by (induct_tac "a" 1);
    (* 7 cases *)
    by (ALLGOALS (simp_tac (simpset() addsimps [externals_def])));
    qed"sender_unchanged";

    (* 2 copies of before *)
    Goal "is_weak_ref_map (%id. id) receiver_ioa receiver_ioa";
    by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
    (* main-part *)
    by (REPEAT (rtac allI 1));
    by (induct_tac "a" 1);
    (* 7 cases *)
    by (ALLGOALS(simp_tac (simpset() addsimps [externals_def])));
    qed"receiver_unchanged";

    Goal "is_weak_ref_map (%id. id) env_ioa env_ioa";
    by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
    (* main-part *)
    by (REPEAT (rtac allI 1));
    by (induct_tac "a" 1);
    (* 7 cases *)
    by (ALLGOALS(simp_tac (simpset() addsimps [externals_def])));
    qed"env_unchanged";

    Goal "compatible srch_ioa rsch_ioa";
    by (simp_tac (simpset() addsimps [compatible_def,Int_def]) 1);
    by (rtac set_ext 1);
    by (induct_tac "x" 1);
    by (ALLGOALS(Simp_tac));
    val compat_single_ch = result();

    (* totally the same as before *)
    Goal "compatible srch_fin_ioa rsch_fin_ioa";
    by (simp_tac (simpset() addsimps [compatible_def,Int_def]) 1);
    by (rtac set_ext 1);
    by (induct_tac "x" 1);
    by (ALLGOALS(Simp_tac));
    val compat_single_fin_ch = result();

    val ss =
      simpset() delsimps ([trans_of_def, srch_asig_def,rsch_asig_def,
                          asig_of_def, actions_def, srch_trans_def, rsch_trans_def,
                          srch_ioa_def, srch_fin_ioa_def, rsch_fin_ioa_def,
                          rsch_ioa_def, sender_trans_def,
                          receiver_trans_def] @ set_lemmas);

    Goal "compatible receiver_ioa (srch_ioa || rsch_ioa)";
    by (simp_tac (ss addsimps [compatible_def,asig_of_par,asig_comp_def,
    			   actions_def,Int_def]) 1);
    by (Simp_tac 1);
    by (rtac set_ext 1);
    by (induct_tac "x" 1);
    by (ALLGOALS Simp_tac);
    val compat_rec = result();

    (* 5 proofs totally the same as before *)
    Goal "compatible receiver_ioa (srch_fin_ioa || rsch_fin_ioa)";
    by (simp_tac (ss addsimps [compatible_def,asig_of_par,asig_comp_def,
    			actions_def,Int_def]) 1);
    by (Simp_tac 1);
    by (rtac set_ext 1);
    by (induct_tac "x" 1);
    by (ALLGOALS Simp_tac);
    val compat_rec_fin =result();

    Goal "compatible sender_ioa \
    \      (receiver_ioa || srch_ioa || rsch_ioa)";
    by (simp_tac (ss addsimps [compatible_def,asig_of_par,asig_comp_def,
    			actions_def,Int_def]) 1);
    by (Simp_tac 1);
    by (rtac set_ext 1);
    by (induct_tac "x" 1);
    by (ALLGOALS(Simp_tac));
    val compat_sen=result();

    Goal "compatible sender_ioa\
    \      (receiver_ioa || srch_fin_ioa || rsch_fin_ioa)";
    by (simp_tac (ss addsimps [compatible_def,asig_of_par,asig_comp_def,
    				actions_def,Int_def]) 1);
    by (Simp_tac 1);
    by (rtac set_ext 1);
    by (induct_tac "x" 1);
    by (ALLGOALS(Simp_tac));
    val compat_sen_fin =result();

    Goal "compatible env_ioa\
    \      (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)";
    by (simp_tac (ss addsimps [compatible_def,asig_of_par,asig_comp_def,
    				actions_def,Int_def]) 1);
    by (Simp_tac 1);
    by (rtac set_ext 1);
    by (induct_tac "x" 1);
    by (ALLGOALS(Simp_tac));
    val compat_env=result();

    Goal "compatible env_ioa\
    \      (sender_ioa || receiver_ioa || srch_fin_ioa || rsch_fin_ioa)";
    by (simp_tac (ss addsimps [compatible_def,asig_of_par,asig_comp_def,
    			actions_def,Int_def]) 1);
    by (Simp_tac 1);
    by (rtac set_ext 1);
    by (induct_tac "x" 1);
    by (ALLGOALS Simp_tac);
    val compat_env_fin=result();

    (* lemmata about externals of channels *)
    Goal "externals(asig_of(srch_fin_ioa)) = externals(asig_of(srch_ioa)) &  \
    \ externals(asig_of(rsch_fin_ioa)) = externals(asig_of(rsch_ioa))";
       by (simp_tac (simpset() addsimps [externals_def]) 1);
    val ext_single_ch = result();

    val ext_ss = [externals_of_par,ext_single_ch];
    val compat_ss = [compat_single_ch,compat_single_fin_ch,compat_rec,
             compat_rec_fin,compat_sen,compat_sen_fin,compat_env,compat_env_fin];
    val abstractions = [env_unchanged,sender_unchanged,
              receiver_unchanged,sender_abstraction,receiver_abstraction];

    (************************************************************************
                S o u n d n e s s   o f   A b s t r a c t i o n
    *************************************************************************)

    val ss = simpset() delsimps ([asig_of_def, srch_ioa_def, rsch_ioa_def,
                                 srch_fin_ioa_def, rsch_fin_ioa_def] @
                                impl_ioas @ env_ioas);

    (* FIX: this proof should be done with compositionality on trace level, not on
            weak_ref_map level, as done here with fxg_is_weak_ref_map_of_product_IOA

    Goal "is_weak_ref_map  abs  system_ioa  system_fin_ioa";

    by (simp_tac (impl_ss delsimps ([srch_ioa_def, rsch_ioa_def, srch_fin_ioa_def,
                                     rsch_fin_ioa_def] @ env_ioas @ impl_ioas)
                          addsimps [system_def, system_fin_def, abs_def,
                                    impl_ioa_def, impl_fin_ioa_def, sys_IOA,
                                    sys_fin_IOA]) 1);

    by (REPEAT (EVERY[rtac fxg_is_weak_ref_map_of_product_IOA 1,
                      simp_tac (ss addsimps abstractions) 1,
                      rtac conjI 1]));

    by (ALLGOALS (simp_tac (ss addsimps ext_ss @ compat_ss)));

    qed "system_refinement";

    *)