src/HOLCF/IOA/ABP/Correctness.thy
author wenzelm
Mon Sep 06 19:13:10 2010 +0200 (2010-09-06)
changeset 39159 0dec18004e75
parent 39120 dd0431961507
child 39302 d7728f65b353
permissions -rw-r--r--
more antiquotations;
     1 (*  Title:      HOLCF/IOA/ABP/Correctness.thy
     2     Author:     Olaf Müller
     3 *)
     4 
     5 header {* The main correctness proof: System_fin implements System *}
     6 
     7 theory Correctness
     8 imports IOA Env Impl Impl_finite
     9 uses "Check.ML"
    10 begin
    11 
    12 primrec reduce :: "'a list => 'a list"
    13 where
    14   reduce_Nil:  "reduce [] = []"
    15 | reduce_Cons: "reduce(x#xs) =
    16                  (case xs of
    17                      [] => [x]
    18                |   y#ys => (if (x=y)
    19                               then reduce xs
    20                               else (x#(reduce xs))))"
    21 
    22 definition
    23   abs where
    24     "abs  =
    25       (%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))),
    26        (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))"
    27 
    28 definition
    29   system_ioa :: "('m action, bool * 'm impl_state)ioa" where
    30   "system_ioa = (env_ioa || impl_ioa)"
    31 
    32 definition
    33   system_fin_ioa :: "('m action, bool * 'm impl_state)ioa" where
    34   "system_fin_ioa = (env_ioa || impl_fin_ioa)"
    35 
    36 
    37 axiomatization where
    38   sys_IOA: "IOA system_ioa" and
    39   sys_fin_IOA: "IOA system_fin_ioa"
    40 
    41 
    42 
    43 declare split_paired_All [simp del] Collect_empty_eq [simp del]
    44 
    45 lemmas [simp] =
    46   srch_asig_def rsch_asig_def rsch_ioa_def srch_ioa_def ch_ioa_def
    47   ch_asig_def srch_actions_def rsch_actions_def rename_def rename_set_def asig_of_def
    48   actions_def exis_elim srch_trans_def rsch_trans_def ch_trans_def
    49   trans_of_def asig_projections set_lemmas
    50 
    51 lemmas abschannel_fin [simp] =
    52   srch_fin_asig_def rsch_fin_asig_def
    53   rsch_fin_ioa_def srch_fin_ioa_def
    54   ch_fin_ioa_def ch_fin_trans_def ch_fin_asig_def
    55 
    56 lemmas impl_ioas = sender_ioa_def receiver_ioa_def
    57   and impl_trans = sender_trans_def receiver_trans_def
    58   and impl_asigs = sender_asig_def receiver_asig_def
    59 
    60 declare let_weak_cong [cong]
    61 declare ioa_triple_proj [simp] starts_of_par [simp]
    62 
    63 lemmas env_ioas = env_ioa_def env_asig_def env_trans_def
    64 lemmas hom_ioas =
    65   env_ioas [simp] impl_ioas [simp] impl_trans [simp] impl_asigs [simp]
    66   asig_projections set_lemmas
    67 
    68 
    69 subsection {* lemmas about reduce *}
    70 
    71 lemma l_iff_red_nil: "(reduce l = []) = (l = [])"
    72   by (induct l) (auto split: list.split)
    73 
    74 lemma hd_is_reduce_hd: "s ~= [] --> hd s = hd (reduce s)"
    75   by (induct s) (auto split: list.split)
    76 
    77 text {* to be used in the following Lemma *}
    78 lemma rev_red_not_nil [rule_format]:
    79     "l ~= [] --> reverse (reduce l) ~= []"
    80   by (induct l) (auto split: list.split)
    81 
    82 text {* shows applicability of the induction hypothesis of the following Lemma 1 *}
    83 lemma last_ind_on_first:
    84     "l ~= [] ==> hd (reverse (reduce (a # l))) = hd (reverse (reduce l))"
    85   apply simp
    86   apply (tactic {* auto_tac (@{claset},
    87     HOL_ss addsplits [@{thm list.split}]
    88     addsimps (@{thms reverse.simps} @ [@{thm hd_append}, @{thm rev_red_not_nil}])) *})
    89   done
    90 
    91 text {* Main Lemma 1 for @{text "S_pkt"} in showing that reduce is refinement. *}
    92 lemma reduce_hd:
    93    "if x=hd(reverse(reduce(l))) & reduce(l)~=[] then
    94        reduce(l@[x])=reduce(l) else
    95        reduce(l@[x])=reduce(l)@[x]"
    96 apply (simplesubst split_if)
    97 apply (rule conjI)
    98 txt {* @{text "-->"} *}
    99 apply (induct_tac "l")
   100 apply (simp (no_asm))
   101 apply (case_tac "list=[]")
   102  apply simp
   103  apply (rule impI)
   104 apply (simp (no_asm))
   105 apply (cut_tac l = "list" in cons_not_nil)
   106  apply (simp del: reduce_Cons)
   107  apply (erule exE)+
   108  apply hypsubst
   109 apply (simp del: reduce_Cons add: last_ind_on_first l_iff_red_nil)
   110 txt {* @{text "<--"} *}
   111 apply (simp (no_asm) add: and_de_morgan_and_absorbe l_iff_red_nil)
   112 apply (induct_tac "l")
   113 apply (simp (no_asm))
   114 apply (case_tac "list=[]")
   115 apply (cut_tac [2] l = "list" in cons_not_nil)
   116 apply simp
   117 apply (auto simp del: reduce_Cons simp add: last_ind_on_first l_iff_red_nil split: split_if)
   118 apply simp
   119 done
   120 
   121 
   122 text {* Main Lemma 2 for R_pkt in showing that reduce is refinement. *}
   123 lemma reduce_tl: "s~=[] ==>
   124      if hd(s)=hd(tl(s)) & tl(s)~=[] then
   125        reduce(tl(s))=reduce(s) else
   126        reduce(tl(s))=tl(reduce(s))"
   127 apply (cut_tac l = "s" in cons_not_nil)
   128 apply simp
   129 apply (erule exE)+
   130 apply (auto split: list.split)
   131 done
   132 
   133 
   134 subsection {* Channel Abstraction *}
   135 
   136 declare split_if [split del]
   137 
   138 lemma channel_abstraction: "is_weak_ref_map reduce ch_ioa ch_fin_ioa"
   139 apply (simp (no_asm) add: is_weak_ref_map_def)
   140 txt {* main-part *}
   141 apply (rule allI)+
   142 apply (rule imp_conj_lemma)
   143 apply (induct_tac "a")
   144 txt {* 2 cases *}
   145 apply (simp_all (no_asm) cong del: if_weak_cong add: externals_def)
   146 txt {* fst case *}
   147  apply (rule impI)
   148  apply (rule disjI2)
   149 apply (rule reduce_hd)
   150 txt {* snd case *}
   151  apply (rule impI)
   152  apply (erule conjE)+
   153  apply (erule disjE)
   154 apply (simp add: l_iff_red_nil)
   155 apply (erule hd_is_reduce_hd [THEN mp])
   156 apply (simp add: l_iff_red_nil)
   157 apply (rule conjI)
   158 apply (erule hd_is_reduce_hd [THEN mp])
   159 apply (rule bool_if_impl_or [THEN mp])
   160 apply (erule reduce_tl)
   161 done
   162 
   163 declare split_if [split]
   164 
   165 lemma sender_abstraction: "is_weak_ref_map reduce srch_ioa srch_fin_ioa"
   166 apply (tactic {*
   167   simp_tac (HOL_ss addsimps [@{thm srch_fin_ioa_def}, @{thm rsch_fin_ioa_def},
   168     @{thm srch_ioa_def}, @{thm rsch_ioa_def}, @{thm rename_through_pmap},
   169     @{thm channel_abstraction}]) 1 *})
   170 done
   171 
   172 lemma receiver_abstraction: "is_weak_ref_map reduce rsch_ioa rsch_fin_ioa"
   173 apply (tactic {*
   174   simp_tac (HOL_ss addsimps [@{thm srch_fin_ioa_def}, @{thm rsch_fin_ioa_def},
   175     @{thm srch_ioa_def}, @{thm rsch_ioa_def}, @{thm rename_through_pmap},
   176     @{thm channel_abstraction}]) 1 *})
   177 done
   178 
   179 
   180 text {* 3 thms that do not hold generally! The lucky restriction here is
   181    the absence of internal actions. *}
   182 lemma sender_unchanged: "is_weak_ref_map (%id. id) sender_ioa sender_ioa"
   183 apply (simp (no_asm) add: is_weak_ref_map_def)
   184 txt {* main-part *}
   185 apply (rule allI)+
   186 apply (induct_tac a)
   187 txt {* 7 cases *}
   188 apply (simp_all (no_asm) add: externals_def)
   189 done
   190 
   191 text {* 2 copies of before *}
   192 lemma receiver_unchanged: "is_weak_ref_map (%id. id) receiver_ioa receiver_ioa"
   193 apply (simp (no_asm) add: is_weak_ref_map_def)
   194 txt {* main-part *}
   195 apply (rule allI)+
   196 apply (induct_tac a)
   197 txt {* 7 cases *}
   198 apply (simp_all (no_asm) add: externals_def)
   199 done
   200 
   201 lemma env_unchanged: "is_weak_ref_map (%id. id) env_ioa env_ioa"
   202 apply (simp (no_asm) add: is_weak_ref_map_def)
   203 txt {* main-part *}
   204 apply (rule allI)+
   205 apply (induct_tac a)
   206 txt {* 7 cases *}
   207 apply (simp_all (no_asm) add: externals_def)
   208 done
   209 
   210 
   211 lemma compat_single_ch: "compatible srch_ioa rsch_ioa"
   212 apply (simp add: compatible_def Int_def)
   213 apply (rule set_ext)
   214 apply (induct_tac x)
   215 apply simp_all
   216 done
   217 
   218 text {* totally the same as before *}
   219 lemma compat_single_fin_ch: "compatible srch_fin_ioa rsch_fin_ioa"
   220 apply (simp add: compatible_def Int_def)
   221 apply (rule set_ext)
   222 apply (induct_tac x)
   223 apply simp_all
   224 done
   225 
   226 lemmas del_simps = trans_of_def srch_asig_def rsch_asig_def
   227   asig_of_def actions_def srch_trans_def rsch_trans_def srch_ioa_def
   228   srch_fin_ioa_def rsch_fin_ioa_def rsch_ioa_def sender_trans_def
   229   receiver_trans_def set_lemmas
   230 
   231 lemma compat_rec: "compatible receiver_ioa (srch_ioa || rsch_ioa)"
   232 apply (simp del: del_simps
   233   add: compatible_def asig_of_par asig_comp_def actions_def Int_def)
   234 apply simp
   235 apply (rule set_ext)
   236 apply (induct_tac x)
   237 apply simp_all
   238 done
   239 
   240 text {* 5 proofs totally the same as before *}
   241 lemma compat_rec_fin: "compatible receiver_ioa (srch_fin_ioa || rsch_fin_ioa)"
   242 apply (simp del: del_simps
   243   add: compatible_def asig_of_par asig_comp_def actions_def Int_def)
   244 apply simp
   245 apply (rule set_ext)
   246 apply (induct_tac x)
   247 apply simp_all
   248 done
   249 
   250 lemma compat_sen: "compatible sender_ioa
   251        (receiver_ioa || srch_ioa || rsch_ioa)"
   252 apply (simp del: del_simps
   253   add: compatible_def asig_of_par asig_comp_def actions_def Int_def)
   254 apply simp
   255 apply (rule set_ext)
   256 apply (induct_tac x)
   257 apply simp_all
   258 done
   259 
   260 lemma compat_sen_fin: "compatible sender_ioa
   261        (receiver_ioa || srch_fin_ioa || rsch_fin_ioa)"
   262 apply (simp del: del_simps
   263   add: compatible_def asig_of_par asig_comp_def actions_def Int_def)
   264 apply simp
   265 apply (rule set_ext)
   266 apply (induct_tac x)
   267 apply simp_all
   268 done
   269 
   270 lemma compat_env: "compatible env_ioa
   271        (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
   272 apply (simp del: del_simps
   273   add: compatible_def asig_of_par asig_comp_def actions_def Int_def)
   274 apply simp
   275 apply (rule set_ext)
   276 apply (induct_tac x)
   277 apply simp_all
   278 done
   279 
   280 lemma compat_env_fin: "compatible env_ioa
   281        (sender_ioa || receiver_ioa || srch_fin_ioa || rsch_fin_ioa)"
   282 apply (simp del: del_simps
   283   add: compatible_def asig_of_par asig_comp_def actions_def Int_def)
   284 apply simp
   285 apply (rule set_ext)
   286 apply (induct_tac x)
   287 apply simp_all
   288 done
   289 
   290 
   291 text {* lemmata about externals of channels *}
   292 lemma ext_single_ch: "externals(asig_of(srch_fin_ioa)) = externals(asig_of(srch_ioa)) &
   293     externals(asig_of(rsch_fin_ioa)) = externals(asig_of(rsch_ioa))"
   294   by (simp add: externals_def)
   295 
   296 
   297 subsection {* Soundness of Abstraction *}
   298 
   299 lemmas ext_simps = externals_of_par ext_single_ch
   300   and compat_simps = compat_single_ch compat_single_fin_ch compat_rec
   301     compat_rec_fin compat_sen compat_sen_fin compat_env compat_env_fin
   302   and abstractions = env_unchanged sender_unchanged
   303     receiver_unchanged sender_abstraction receiver_abstraction
   304 
   305 
   306 (* FIX: this proof should be done with compositionality on trace level, not on
   307         weak_ref_map level, as done here with fxg_is_weak_ref_map_of_product_IOA
   308 
   309 Goal "is_weak_ref_map  abs  system_ioa  system_fin_ioa"
   310 
   311 by (simp_tac (impl_ss delsimps ([srch_ioa_def, rsch_ioa_def, srch_fin_ioa_def,
   312                                  rsch_fin_ioa_def] @ env_ioas @ impl_ioas)
   313                       addsimps [system_def, system_fin_def, abs_def,
   314                                 impl_ioa_def, impl_fin_ioa_def, sys_IOA,
   315                                 sys_fin_IOA]) 1);
   316 
   317 by (REPEAT (EVERY[rtac fxg_is_weak_ref_map_of_product_IOA 1,
   318                   simp_tac (ss addsimps abstractions) 1,
   319                   rtac conjI 1]));
   320 
   321 by (ALLGOALS (simp_tac (ss addsimps ext_ss @ compat_ss)));
   322 
   323 qed "system_refinement";
   324 *)
   325 
   326 end