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