src/HOL/IOA/ABP/Correctness.ML
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 2513 d708d8cdc8e8
permissions -rw-r--r--
Dep. on Provers/nat_transitive
     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 (cut_inst_tac [("l","list")] cons_not_nil 2);
   141 by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
   142 by (auto_tac (!claset, 
   143 	      impl_ss addsimps [last_ind_on_first,l_iff_red_nil] 
   144                       setloop split_tac [expand_if]));
   145 by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
   146 qed"reduce_hd";
   147 
   148 
   149 (* Main Lemma 2 for R_pkt in showing that reduce is refinement *)
   150 goal Correctness.thy 
   151   "!! s. [| s~=[] |] ==>  \
   152 \    if hd(s)=hd(tl(s)) & tl(s)~=[] then    \
   153 \      reduce(tl(s))=reduce(s) else      \
   154 \      reduce(tl(s))=tl(reduce(s))"; 
   155 by (cut_inst_tac [("l","s")] cons_not_nil 1);
   156 by (Asm_full_simp_tac 1);
   157 by (REPEAT (etac exE 1));
   158 by (Asm_full_simp_tac 1);
   159 by (rtac (expand_if RS ssubst) 1);
   160 by (rtac conjI 1);
   161 by (simp_tac (!simpset addsimps [and_de_morgan_and_absorbe]) 2);
   162 by (Step_tac 1);
   163 by (ALLGOALS (cut_inst_tac [("l","xs")] cons_not_nil));
   164 by (Auto_tac());
   165 val reduce_tl =result();
   166 
   167 
   168 (*******************************************************************
   169           C h a n n e l   A b s t r a c t i o n
   170  *******************************************************************)
   171 
   172 goal Correctness.thy 
   173       "is_weak_pmap reduce ch_ioa ch_fin_ioa";
   174 by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1);
   175 (* ---------------- main-part ------------------- *)
   176 by (REPEAT (rtac allI 1));
   177 by (rtac imp_conj_lemma 1);
   178 by (act.induct_tac "a" 1);
   179 (* ----------------- 2 cases ---------------------*)
   180 by (ALLGOALS (simp_tac (!simpset addsimps [externals_def])));
   181 (* fst case --------------------------------------*)
   182  by (rtac impI 1);
   183  by (rtac disjI2 1);
   184 by (rtac reduce_hd 1);
   185 (* snd case --------------------------------------*)
   186  by (rtac impI 1);
   187  by (REPEAT (etac conjE 1));
   188  by (etac disjE 1);
   189 by (asm_full_simp_tac (!simpset addsimps [l_iff_red_nil]) 1);
   190 by (etac (hd_is_reduce_hd RS mp) 1); 
   191 by (asm_full_simp_tac (!simpset addsimps [l_iff_red_nil]) 1);
   192 by (rtac conjI 1);
   193 by (etac (hd_is_reduce_hd RS mp) 1); 
   194 by (rtac (bool_if_impl_or RS mp) 1);
   195 by (etac reduce_tl 1);
   196 qed"channel_abstraction";
   197 
   198 goal Correctness.thy 
   199       "is_weak_pmap reduce srch_ioa srch_fin_ioa";
   200 by (simp_tac (list_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def,
   201  srch_ioa_def,rsch_ioa_def,rename_through_pmap,channel_abstraction]) 1);
   202 qed"sender_abstraction";
   203 
   204 goal Correctness.thy 
   205       "is_weak_pmap reduce rsch_ioa rsch_fin_ioa";
   206 by (simp_tac (list_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def,
   207  srch_ioa_def,rsch_ioa_def,rename_through_pmap,channel_abstraction]) 1);
   208 qed"receiver_abstraction";
   209 
   210 
   211 (* 3 thms that do not hold generally! The lucky restriction here is 
   212    the absence of internal actions. *)
   213 goal Correctness.thy 
   214       "is_weak_pmap (%id.id) sender_ioa sender_ioa";
   215 by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1);
   216 by (TRY(
   217    (rtac conjI 1) THEN
   218 (* start states *)
   219    (Fast_tac 1)));
   220 (* main-part *)
   221 by (REPEAT (rtac allI 1));
   222 by (rtac imp_conj_lemma 1);
   223 by (Action.action.induct_tac "a" 1);
   224 (* 7 cases *)
   225 by (ALLGOALS (simp_tac ((!simpset addsimps [externals_def]) setloop (split_tac [expand_if]))));
   226 qed"sender_unchanged";
   227 
   228 (* 2 copies of before *)
   229 goal Correctness.thy 
   230       "is_weak_pmap (%id.id) receiver_ioa receiver_ioa";
   231 by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1);
   232 by (TRY(
   233    (rtac conjI 1) THEN
   234  (* start states *)
   235    (Fast_tac 1)));
   236 (* main-part *)
   237 by (REPEAT (rtac allI 1));
   238 by (rtac imp_conj_lemma 1);
   239 by (Action.action.induct_tac "a" 1);
   240 (* 7 cases *)
   241 by (ALLGOALS (simp_tac ((!simpset addsimps [externals_def]) setloop (split_tac [expand_if]))));
   242 qed"receiver_unchanged";
   243 
   244 goal Correctness.thy 
   245       "is_weak_pmap (%id.id) env_ioa env_ioa";
   246 by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1);
   247 by (TRY(
   248    (rtac conjI 1) THEN
   249 (* start states *)
   250    (Fast_tac 1)));
   251 (* main-part *)
   252 by (REPEAT (rtac allI 1));
   253 by (rtac imp_conj_lemma 1);
   254 by (Action.action.induct_tac "a" 1);
   255 (* 7 cases *)
   256 by (ALLGOALS (simp_tac ((!simpset addsimps [externals_def]) setloop (split_tac [expand_if]))));
   257 qed"env_unchanged";
   258 
   259 Delsimps [Collect_False_empty];
   260 
   261 goal Correctness.thy "compat_ioas srch_ioa rsch_ioa"; 
   262 by (simp_tac (!simpset addsimps [compat_ioas_def,compat_asigs_def,Int_def,empty_def]) 1);
   263 by (rtac set_ext 1);
   264 by (Action.action.induct_tac "x" 1);
   265 by (ALLGOALS(Simp_tac));
   266 val compat_single_ch = result();
   267 
   268 (* totally the same as before *)
   269 goal Correctness.thy "compat_ioas srch_fin_ioa rsch_fin_ioa"; 
   270 by (simp_tac (!simpset addsimps [compat_ioas_def,compat_asigs_def,Int_def,empty_def]) 1);
   271 by (rtac set_ext 1);
   272 by (Action.action.induct_tac "x" 1);
   273 by (ALLGOALS(Simp_tac));
   274 val compat_single_fin_ch = result();
   275 
   276 val ss =
   277   !simpset delsimps ([trans_of_def, srch_asig_def,rsch_asig_def,
   278                       asig_of_def, actions_def, srch_trans_def, rsch_trans_def,
   279                       srch_ioa_def, srch_fin_ioa_def, rsch_fin_ioa_def, 
   280                       rsch_ioa_def, Sender.sender_trans_def,
   281                       Receiver.receiver_trans_def] @ set_lemmas);
   282 
   283 goal Correctness.thy "compat_ioas receiver_ioa (srch_ioa || rsch_ioa)";
   284 by (simp_tac (ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,
   285                            asig_of_par,asig_comp_def,actions_def,
   286                            Int_def]) 1);
   287 by (Simp_tac 1);
   288 by (rtac set_ext 1);
   289 by (Action.action.induct_tac "x" 1);
   290 by (ALLGOALS Simp_tac);
   291 by (ALLGOALS(simp_tac (!simpset addsimps [insert_def,Un_def]))); 
   292 by (ALLGOALS(simp_tac (!simpset addsimps [de_morgan,singleton_set])));
   293 val compat_rec = result();
   294 
   295 (* 5 proofs totally the same as before *)
   296 goal Correctness.thy "compat_ioas receiver_ioa (srch_fin_ioa || rsch_fin_ioa)";
   297 by (simp_tac (ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
   298 by (Simp_tac 1);
   299 by (rtac set_ext 1);
   300 by (Action.action.induct_tac "x" 1);
   301 by (ALLGOALS Simp_tac);
   302 by (ALLGOALS(simp_tac (!simpset addsimps [insert_def,Un_def]))); 
   303 by (ALLGOALS(simp_tac (!simpset addsimps [de_morgan,singleton_set])));
   304 val compat_rec_fin =result();
   305 
   306 goal Correctness.thy "compat_ioas sender_ioa \
   307 \      (receiver_ioa || srch_ioa || rsch_ioa)";
   308 by (simp_tac (ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
   309 by (Simp_tac 1);
   310 by (rtac set_ext 1);
   311 by (Action.action.induct_tac "x" 1);
   312 by (ALLGOALS(Simp_tac));
   313 by (ALLGOALS(simp_tac (!simpset addsimps [insert_def,Un_def]))); 
   314 by (ALLGOALS(simp_tac (!simpset addsimps [de_morgan,singleton_set])));
   315 val compat_sen=result();
   316 
   317 goal Correctness.thy "compat_ioas sender_ioa\
   318 \      (receiver_ioa || srch_fin_ioa || rsch_fin_ioa)";
   319 by (simp_tac (ss addsimps [empty_def,  compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
   320 by (Simp_tac 1);
   321 by (rtac set_ext 1);
   322 by (Action.action.induct_tac "x" 1);
   323 by (ALLGOALS(Simp_tac));
   324 by (ALLGOALS(simp_tac (!simpset addsimps [insert_def,Un_def]))); 
   325 by (ALLGOALS(simp_tac (!simpset addsimps [de_morgan,singleton_set])));
   326 val compat_sen_fin =result();
   327 
   328 goal Correctness.thy "compat_ioas env_ioa\
   329 \      (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)";
   330 by (simp_tac (ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
   331 by (Simp_tac 1);
   332 by (rtac set_ext 1);
   333 by (Action.action.induct_tac "x" 1);
   334 by (ALLGOALS(Simp_tac));
   335 by (ALLGOALS(simp_tac (!simpset addsimps [insert_def,Un_def])));
   336 by (ALLGOALS(simp_tac (!simpset addsimps [de_morgan,singleton_set])));
   337 val compat_env=result();
   338 
   339 goal Correctness.thy "compat_ioas env_ioa\
   340 \      (sender_ioa || receiver_ioa || srch_fin_ioa || rsch_fin_ioa)";
   341 by (simp_tac (ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
   342 by (Simp_tac 1);
   343 by (rtac set_ext 1);
   344 by (Action.action.induct_tac "x" 1);
   345 by (ALLGOALS Simp_tac);
   346 by (ALLGOALS(simp_tac (!simpset addsimps [insert_def,Un_def]))); 
   347 by (ALLGOALS(simp_tac (!simpset addsimps [de_morgan,singleton_set])));
   348 val compat_env_fin=result();
   349 
   350 
   351 (* lemmata about externals of channels *)
   352 goal Correctness.thy 
   353  "externals(asig_of(srch_fin_ioa)) = externals(asig_of(srch_ioa)) &  \
   354 \ externals(asig_of(rsch_fin_ioa)) = externals(asig_of(rsch_ioa))";
   355 by (simp_tac (!simpset addsimps [externals_def]) 1);
   356 val ext_single_ch = result();
   357 
   358 
   359 
   360 
   361 
   362 val ext_ss = [externals_of_par,ext_single_ch];
   363 val compat_ss = [compat_single_ch,compat_single_fin_ch,compat_rec,
   364          compat_rec_fin,compat_sen,compat_sen_fin,compat_env,compat_env_fin];
   365 val abstractions = [env_unchanged,sender_unchanged,
   366           receiver_unchanged,sender_abstraction,receiver_abstraction];
   367 
   368 
   369 (************************************************************************
   370             S o u n d n e s s   o f   A b s t r a c t i o n        
   371 *************************************************************************)
   372 
   373 val ss = !simpset delsimps ([asig_of_def, srch_ioa_def, rsch_ioa_def,
   374                              srch_fin_ioa_def, rsch_fin_ioa_def] @
   375                             impl_ioas @ env_ioas);
   376 
   377 goal Correctness.thy 
   378      "is_weak_pmap  abs  system_ioa  system_fin_ioa";
   379 
   380 by (simp_tac (impl_ss delsimps ([srch_ioa_def, rsch_ioa_def, srch_fin_ioa_def,
   381                                  rsch_fin_ioa_def] @ env_ioas @ impl_ioas)
   382                       addsimps [system_def, system_fin_def, abs_def,
   383                                 impl_ioa_def, impl_fin_ioa_def, sys_IOA,
   384                                 sys_fin_IOA]) 1);
   385 
   386 by (REPEAT (EVERY[rtac fxg_is_weak_pmap_of_product_IOA 1, 
   387                   simp_tac (ss addsimps abstractions) 1,
   388                   rtac conjI 1]));
   389 
   390 by (ALLGOALS (simp_tac (ss addsimps ext_ss @ compat_ss))); 
   391 
   392 qed "system_refinement";