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