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