src/HOL/HOLCF/IOA/NTP/Correctness.thy
author huffman
Sat Nov 27 16:08:10 2010 -0800 (2010-11-27)
changeset 40774 0437dbc127b3
parent 35215 src/HOLCF/IOA/NTP/Correctness.thy@a03462cbf86f
child 42151 4da4fc77664b
permissions -rw-r--r--
moved directory src/HOLCF to src/HOL/HOLCF;
added HOLCF theories to src/HOL/IsaMakefile;
     1 (*  Title:      HOL/IOA/NTP/Correctness.thy
     2     Author:     Tobias Nipkow & Konrad Slind
     3 *)
     4 
     5 header {* The main correctness proof: Impl implements Spec *}
     6 
     7 theory Correctness
     8 imports Impl Spec
     9 begin
    10 
    11 definition
    12   hom :: "'m impl_state => 'm list" where
    13   "hom s = rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s)
    14                          else tl(sq(sen s)))"
    15 
    16 declaration {* fn _ =>
    17   (* repeated from Traces.ML *)
    18   Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")
    19 *}
    20 
    21 lemmas hom_ioas = Spec.ioa_def Spec.trans_def sender_trans_def receiver_trans_def impl_ioas
    22   and impl_asigs = sender_asig_def receiver_asig_def srch_asig_def rsch_asig_def
    23 
    24 declare split_paired_All [simp del]
    25 
    26 
    27 text {*
    28   A lemma about restricting the action signature of the implementation
    29   to that of the specification.
    30 *}
    31 
    32 lemma externals_lemma: 
    33  "a:externals(asig_of(Automata.restrict impl_ioa (externals spec_sig))) =  
    34   (case a of                   
    35       S_msg(m) => True         
    36     | R_msg(m) => True         
    37     | S_pkt(pkt) => False   
    38     | R_pkt(pkt) => False   
    39     | S_ack(b) => False     
    40     | R_ack(b) => False     
    41     | C_m_s => False           
    42     | C_m_r => False           
    43     | C_r_s => False           
    44     | C_r_r(m) => False)"
    45  apply (simp (no_asm) add: externals_def restrict_def restrict_asig_def Spec.sig_def asig_projections)
    46 
    47   apply (induct_tac "a")
    48   apply (simp_all (no_asm) add: actions_def asig_projections)
    49   txt {* 2 *}
    50   apply (simp (no_asm) add: impl_ioas)
    51   apply (simp (no_asm) add: impl_asigs)
    52   apply (simp (no_asm) add: asig_of_par asig_comp_def asig_projections)
    53   apply (simp (no_asm) add: "transitions"(1) unfold_renaming)
    54   txt {* 1 *}
    55   apply (simp (no_asm) add: impl_ioas)
    56   apply (simp (no_asm) add: impl_asigs)
    57   apply (simp (no_asm) add: asig_of_par asig_comp_def asig_projections)
    58   done
    59 
    60 lemmas sels = sbit_def sq_def ssending_def rbit_def rq_def rsending_def
    61 
    62 
    63 text {* Proof of correctness *}
    64 lemma ntp_correct:
    65   "is_weak_ref_map hom (Automata.restrict impl_ioa (externals spec_sig)) spec_ioa"
    66 apply (unfold Spec.ioa_def is_weak_ref_map_def)
    67 apply (simp (no_asm) cong del: if_weak_cong split del: split_if add: Correctness.hom_def
    68   cancel_restrict externals_lemma)
    69 apply (rule conjI)
    70  apply (simp (no_asm) add: hom_ioas)
    71  apply (simp (no_asm_simp) add: sels)
    72 apply (rule allI)+
    73 apply (rule imp_conj_lemma)
    74 
    75 apply (induct_tac "a")
    76 apply (simp_all (no_asm_simp) add: hom_ioas)
    77 apply (frule inv4)
    78 apply force
    79 
    80 apply (frule inv4)
    81 apply (frule inv2)
    82 apply (erule disjE)
    83 apply (simp (no_asm_simp))
    84 apply force
    85 
    86 apply (frule inv2)
    87 apply (erule disjE)
    88 
    89 apply (frule inv3)
    90 apply (case_tac "sq (sen (s))=[]")
    91 
    92 apply (simp add: hom_ioas)
    93 apply (blast dest!: add_leD1 [THEN leD])
    94 
    95 apply (case_tac "m = hd (sq (sen (s)))")
    96 
    97 apply force
    98 
    99 apply simp
   100 apply (blast dest!: add_leD1 [THEN leD])
   101 
   102 apply simp
   103 done
   104 
   105 end