src/HOLCF/IOA/ABP/Correctness.ML
author paulson
Thu Feb 19 18:24:08 2004 +0100 (2004-02-19)
changeset 14401 477380c74c1d
parent 13898 9410d2eb9563
child 14981 e73f8140af78
permissions -rw-r--r--
removal of the legacy ML structure List
     1 (*  Title:      HOLCF/IOA/ABP/Correctness.ML
     2     ID:         $Id$
     3     Author:     Olaf Müller
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 *)
     6 
     7 
     8 goal Abschannel.thy "(? x. x=P & Q(x)) = Q(P)";
     9 by (Fast_tac 1);
    10 qed"exis_elim";
    11 
    12 Delsimps [split_paired_All,Collect_empty_eq];
    13 Addsimps 
    14  ([srch_asig_def, rsch_asig_def, rsch_ioa_def, srch_ioa_def, ch_ioa_def, 
    15    ch_asig_def, srch_actions_def, rsch_actions_def, rename_def, rename_set_def, asig_of_def, 
    16    actions_def, exis_elim, srch_trans_def, rsch_trans_def, ch_trans_def, 
    17    trans_of_def] @ asig_projections @ set_lemmas);
    18 
    19 val abschannel_fin = [srch_fin_asig_def, rsch_fin_asig_def, 
    20                       rsch_fin_ioa_def, srch_fin_ioa_def, 
    21                       ch_fin_ioa_def,ch_fin_trans_def,ch_fin_asig_def];
    22 Addsimps abschannel_fin;
    23 
    24 val impl_ioas =  [Sender.sender_ioa_def,Receiver.receiver_ioa_def];
    25 val impl_trans = [Sender.sender_trans_def,Receiver.receiver_trans_def];
    26 val impl_asigs = [Sender.sender_asig_def,Receiver.receiver_asig_def];
    27 Addcongs [let_weak_cong];
    28 Addsimps [Let_def, ioa_triple_proj, starts_of_par];
    29 
    30 val env_ioas = [Env.env_ioa_def,Env.env_asig_def,Env.env_trans_def];
    31 val hom_ioas = env_ioas @ impl_ioas @ impl_trans @ impl_asigs @ 
    32                asig_projections @ set_lemmas;
    33 Addsimps hom_ioas;
    34 
    35 
    36 
    37 (* auxiliary function *)
    38 fun rotate n i = EVERY(replicate n (etac revcut_rl i));
    39 
    40 (* lemmas about reduce *)
    41 
    42 Goal "(reduce(l)=[]) = (l=[])";  
    43 by (induct_tac "l" 1);
    44 by (auto_tac (claset(), simpset() addsplits [thm"list.split"]));
    45 val l_iff_red_nil = result();
    46 
    47 Goal "s~=[] --> hd(s)=hd(reduce(s))";
    48 by (induct_tac "s" 1);
    49 by (auto_tac (claset(), simpset() addsplits [thm"list.split"]));
    50 qed"hd_is_reduce_hd";
    51 
    52 (* to be used in the following Lemma *)
    53 Goal "l~=[] --> reverse(reduce(l))~=[]";
    54 by (induct_tac "l" 1);
    55 by (auto_tac (claset(), simpset() addsplits [thm"list.split"]));
    56 qed_spec_mp "rev_red_not_nil";
    57 
    58 (* shows applicability of the induction hypothesis of the following Lemma 1 *)
    59 Goal "l~=[] ==> hd(reverse(reduce(a#l))) = hd(reverse(reduce(l)))";
    60  by (Simp_tac 1);
    61  by (auto_tac (claset(), HOL_ss addsplits [thm"list.split"]
    62                                 addsimps [reverse_Cons,hd_append,
    63 					  rev_red_not_nil]));
    64 qed"last_ind_on_first";
    65 
    66 val impl_ss = simpset() delsimps [reduce_Cons];
    67 
    68 (* Main Lemma 1 for S_pkt in showing that reduce is refinement  *) 
    69 Goal 
    70    "if x=hd(reverse(reduce(l))) & reduce(l)~=[] then   \
    71 \      reduce(l@[x])=reduce(l) else                  \
    72 \      reduce(l@[x])=reduce(l)@[x]"; 
    73 by (stac split_if 1);
    74 by (rtac conjI 1);
    75 (* --> *)
    76 by (induct_tac "l" 1);
    77 by (Simp_tac 1);
    78 by (case_tac "list=[]" 1);
    79  by (asm_full_simp_tac (simpset() addsimps [reverse_Nil,reverse_Cons]) 1);
    80  by (rtac impI 1);
    81 by (Simp_tac 1);
    82 by (cut_inst_tac [("l","list")] cons_not_nil 1);
    83  by (asm_full_simp_tac impl_ss 1);
    84  by (REPEAT (etac exE 1));
    85  by (hyp_subst_tac 1);
    86 by (asm_full_simp_tac (impl_ss addsimps [last_ind_on_first,l_iff_red_nil]) 1);
    87 (* <-- *)
    88 by (simp_tac (simpset() addsimps [and_de_morgan_and_absorbe,l_iff_red_nil]) 1);
    89 by (induct_tac "l" 1);
    90 by (Simp_tac 1);
    91 by (case_tac "list=[]" 1);
    92 by (cut_inst_tac [("l","list")] cons_not_nil 2);
    93 by (Asm_full_simp_tac 1);
    94 by (auto_tac (claset(), 
    95 	      impl_ss addsimps [last_ind_on_first,l_iff_red_nil] 
    96                       setloop split_tac [split_if]));
    97 by (Asm_full_simp_tac 1);
    98 qed"reduce_hd";
    99 
   100 
   101 (* Main Lemma 2 for R_pkt in showing that reduce is refinement *)
   102 Goal "s~=[] ==>  \
   103 \    if hd(s)=hd(tl(s)) & tl(s)~=[] then    \
   104 \      reduce(tl(s))=reduce(s) else      \
   105 \      reduce(tl(s))=tl(reduce(s))"; 
   106 by (cut_inst_tac [("l","s")] cons_not_nil 1);
   107 by (Asm_full_simp_tac 1);
   108 by (REPEAT (etac exE 1));
   109 by (auto_tac (claset(), simpset() addsplits [thm"list.split"]));
   110 val reduce_tl =result();
   111 
   112 
   113 (*******************************************************************
   114           C h a n n e l   A b s t r a c t i o n
   115  *******************************************************************)
   116 
   117 Delsplits [split_if]; 
   118 
   119 Goal "is_weak_ref_map reduce ch_ioa ch_fin_ioa";
   120 by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
   121 (* ---------------- main-part ------------------- *)
   122 by (REPEAT (rtac allI 1));
   123 by (rtac imp_conj_lemma 1);
   124 by (induct_tac "a" 1);
   125 (* ----------------- 2 cases ---------------------*)
   126 by (ALLGOALS (simp_tac (simpset() delcongs [if_weak_cong]
   127 				  addsimps [externals_def])));
   128 (* fst case --------------------------------------*)
   129  by (rtac impI 1);
   130  by (rtac disjI2 1);
   131 by (rtac reduce_hd 1);
   132 (* snd case --------------------------------------*)
   133  by (rtac impI 1);
   134  by (REPEAT (etac conjE 1));
   135  by (etac disjE 1);
   136 by (asm_full_simp_tac (simpset() addsimps [l_iff_red_nil]) 1);
   137 by (etac (hd_is_reduce_hd RS mp) 1); 
   138 by (asm_full_simp_tac (simpset() addsimps [l_iff_red_nil]) 1);
   139 by (rtac conjI 1);
   140 by (etac (hd_is_reduce_hd RS mp) 1); 
   141 by (rtac (bool_if_impl_or RS mp) 1);
   142 by (etac reduce_tl 1);
   143 qed"channel_abstraction";
   144 
   145 Addsplits [split_if]; 
   146 
   147 Goal "is_weak_ref_map reduce srch_ioa srch_fin_ioa";
   148 by (simp_tac (HOL_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def,
   149  srch_ioa_def,rsch_ioa_def,rename_through_pmap,channel_abstraction]) 1);
   150 qed"sender_abstraction";
   151 
   152 Goal "is_weak_ref_map reduce rsch_ioa rsch_fin_ioa";
   153 by (simp_tac (HOL_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def,
   154  srch_ioa_def,rsch_ioa_def,rename_through_pmap,channel_abstraction]) 1);
   155 qed"receiver_abstraction";
   156 
   157 
   158 (* 3 thms that do not hold generally! The lucky restriction here is 
   159    the absence of internal actions. *)
   160 Goal "is_weak_ref_map (%id. id) sender_ioa sender_ioa";
   161 by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
   162 (* main-part *)
   163 by (REPEAT (rtac allI 1));
   164 by (induct_tac "a" 1);
   165 (* 7 cases *)
   166 by (ALLGOALS (simp_tac (simpset() addsimps [externals_def])));
   167 qed"sender_unchanged";
   168 
   169 (* 2 copies of before *)
   170 Goal "is_weak_ref_map (%id. id) receiver_ioa receiver_ioa";
   171 by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
   172 (* main-part *)
   173 by (REPEAT (rtac allI 1));
   174 by (induct_tac "a" 1);
   175 (* 7 cases *)
   176 by (ALLGOALS(simp_tac (simpset() addsimps [externals_def])));
   177 qed"receiver_unchanged";
   178 
   179 Goal "is_weak_ref_map (%id. id) env_ioa env_ioa";
   180 by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
   181 (* main-part *)
   182 by (REPEAT (rtac allI 1));
   183 by (induct_tac "a" 1);
   184 (* 7 cases *)
   185 by (ALLGOALS(simp_tac (simpset() addsimps [externals_def])));
   186 qed"env_unchanged";
   187 
   188 
   189 Goal "compatible srch_ioa rsch_ioa"; 
   190 by (simp_tac (simpset() addsimps [compatible_def,Int_def]) 1);
   191 by (rtac set_ext 1);
   192 by (induct_tac "x" 1);
   193 by (ALLGOALS(Simp_tac));
   194 val compat_single_ch = result();
   195 
   196 (* totally the same as before *)
   197 Goal "compatible srch_fin_ioa rsch_fin_ioa"; 
   198 by (simp_tac (simpset() addsimps [compatible_def,Int_def]) 1);
   199 by (rtac set_ext 1);
   200 by (induct_tac "x" 1);
   201 by (ALLGOALS(Simp_tac));
   202 val compat_single_fin_ch = result();
   203 
   204 val ss =
   205   simpset() delsimps ([trans_of_def, srch_asig_def,rsch_asig_def,
   206                       asig_of_def, actions_def, srch_trans_def, rsch_trans_def,
   207                       srch_ioa_def, srch_fin_ioa_def, rsch_fin_ioa_def, 
   208                       rsch_ioa_def, Sender.sender_trans_def,
   209                       Receiver.receiver_trans_def] @ set_lemmas);
   210 
   211 Goal "compatible receiver_ioa (srch_ioa || rsch_ioa)";
   212 by (simp_tac (ss addsimps [compatible_def,asig_of_par,asig_comp_def,
   213 			   actions_def,Int_def]) 1);
   214 by (Simp_tac 1);
   215 by (rtac set_ext 1);
   216 by (induct_tac "x" 1);
   217 by (ALLGOALS Simp_tac);
   218 val compat_rec = result();
   219 
   220 (* 5 proofs totally the same as before *)
   221 Goal "compatible receiver_ioa (srch_fin_ioa || rsch_fin_ioa)";
   222 by (simp_tac (ss addsimps [compatible_def,asig_of_par,asig_comp_def,
   223 			actions_def,Int_def]) 1);
   224 by (Simp_tac 1);
   225 by (rtac set_ext 1);
   226 by (induct_tac "x" 1);
   227 by (ALLGOALS Simp_tac);
   228 val compat_rec_fin =result();
   229 
   230 Goal "compatible sender_ioa \
   231 \      (receiver_ioa || srch_ioa || rsch_ioa)";
   232 by (simp_tac (ss addsimps [compatible_def,asig_of_par,asig_comp_def,
   233 			actions_def,Int_def]) 1);
   234 by (Simp_tac 1);
   235 by (rtac set_ext 1);
   236 by (induct_tac "x" 1);
   237 by (ALLGOALS(Simp_tac));
   238 val compat_sen=result();
   239 
   240 Goal "compatible sender_ioa\
   241 \      (receiver_ioa || srch_fin_ioa || rsch_fin_ioa)";
   242 by (simp_tac (ss addsimps [compatible_def,asig_of_par,asig_comp_def,
   243 				actions_def,Int_def]) 1);
   244 by (Simp_tac 1);
   245 by (rtac set_ext 1);
   246 by (induct_tac "x" 1);
   247 by (ALLGOALS(Simp_tac));
   248 val compat_sen_fin =result();
   249 
   250 Goal "compatible env_ioa\
   251 \      (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)";
   252 by (simp_tac (ss addsimps [compatible_def,asig_of_par,asig_comp_def,
   253 				actions_def,Int_def]) 1);
   254 by (Simp_tac 1);
   255 by (rtac set_ext 1);
   256 by (induct_tac "x" 1);
   257 by (ALLGOALS(Simp_tac));
   258 val compat_env=result();
   259 
   260 Goal "compatible env_ioa\
   261 \      (sender_ioa || receiver_ioa || srch_fin_ioa || rsch_fin_ioa)";
   262 by (simp_tac (ss addsimps [compatible_def,asig_of_par,asig_comp_def,
   263 			actions_def,Int_def]) 1);
   264 by (Simp_tac 1);
   265 by (rtac set_ext 1);
   266 by (induct_tac "x" 1);
   267 by (ALLGOALS Simp_tac);
   268 val compat_env_fin=result();
   269 
   270 
   271 (* lemmata about externals of channels *)
   272 Goal "externals(asig_of(srch_fin_ioa)) = externals(asig_of(srch_ioa)) &  \
   273 \ externals(asig_of(rsch_fin_ioa)) = externals(asig_of(rsch_ioa))";
   274    by (simp_tac (simpset() addsimps [externals_def]) 1);
   275 val ext_single_ch = result();
   276 
   277 
   278 
   279 
   280 
   281 val ext_ss = [externals_of_par,ext_single_ch];
   282 val compat_ss = [compat_single_ch,compat_single_fin_ch,compat_rec,
   283          compat_rec_fin,compat_sen,compat_sen_fin,compat_env,compat_env_fin];
   284 val abstractions = [env_unchanged,sender_unchanged,
   285           receiver_unchanged,sender_abstraction,receiver_abstraction];
   286 
   287 
   288 (************************************************************************
   289             S o u n d n e s s   o f   A b s t r a c t i o n        
   290 *************************************************************************)
   291 
   292 val ss = simpset() delsimps ([asig_of_def, srch_ioa_def, rsch_ioa_def,
   293                              srch_fin_ioa_def, rsch_fin_ioa_def] @
   294                             impl_ioas @ env_ioas);
   295 
   296 (* FIX: this proof should be done with compositionality on trace level, not on 
   297         weak_ref_map level, as done here with fxg_is_weak_ref_map_of_product_IOA 
   298 
   299 Goal "is_weak_ref_map  abs  system_ioa  system_fin_ioa";
   300 
   301 by (simp_tac (impl_ss delsimps ([srch_ioa_def, rsch_ioa_def, srch_fin_ioa_def,
   302                                  rsch_fin_ioa_def] @ env_ioas @ impl_ioas)
   303                       addsimps [system_def, system_fin_def, abs_def,
   304                                 impl_ioa_def, impl_fin_ioa_def, sys_IOA,
   305                                 sys_fin_IOA]) 1);
   306 
   307 by (REPEAT (EVERY[rtac fxg_is_weak_ref_map_of_product_IOA 1, 
   308                   simp_tac (ss addsimps abstractions) 1,
   309                   rtac conjI 1]));
   310 
   311 by (ALLGOALS (simp_tac (ss addsimps ext_ss @ compat_ss))); 
   312 
   313 qed "system_refinement";
   314 
   315 
   316 *)