src/HOLCF/IOA/NTP/Correctness.thy
author wenzelm
Wed, 19 Mar 2008 22:47:35 +0100
changeset 26339 7825c83c9eff
parent 25131 2c8caac48ade
child 35174 e15040ae75d7
permissions -rw-r--r--
eliminated change_claset/simpset;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     1
(*  Title:      HOL/IOA/NTP/Correctness.thy
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     2
    ID:         $Id$
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     3
    Author:     Tobias Nipkow & Konrad Slind
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     4
*)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     5
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     6
header {* The main correctness proof: Impl implements Spec *}
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     7
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     8
theory Correctness
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     9
imports Impl Spec
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    10
begin
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    11
25131
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19739
diff changeset
    12
definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19739
diff changeset
    13
  hom :: "'m impl_state => 'm list" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19739
diff changeset
    14
  "hom s = rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s)
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19739
diff changeset
    15
                         else tl(sq(sen s)))"
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    16
26339
7825c83c9eff eliminated change_claset/simpset;
wenzelm
parents: 25131
diff changeset
    17
declaration {* fn _ =>
7825c83c9eff eliminated change_claset/simpset;
wenzelm
parents: 25131
diff changeset
    18
  (* repeated from Traces.ML *)
7825c83c9eff eliminated change_claset/simpset;
wenzelm
parents: 25131
diff changeset
    19
  Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")
19739
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    20
*}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    21
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    22
lemmas hom_ioas = Spec.ioa_def Spec.trans_def sender_trans_def receiver_trans_def impl_ioas
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    23
  and impl_asigs = sender_asig_def receiver_asig_def srch_asig_def rsch_asig_def
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    24
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    25
declare split_paired_All [simp del]
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    26
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    27
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    28
text {*
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    29
  A lemma about restricting the action signature of the implementation
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    30
  to that of the specification.
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    31
*}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    32
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    33
lemma externals_lemma: 
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    34
 "a:externals(asig_of(Automata.restrict impl_ioa (externals spec_sig))) =  
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    35
  (case a of                   
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    36
      S_msg(m) => True         
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    37
    | R_msg(m) => True         
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    38
    | S_pkt(pkt) => False   
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    39
    | R_pkt(pkt) => False   
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    40
    | S_ack(b) => False     
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    41
    | R_ack(b) => False     
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    42
    | C_m_s => False           
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    43
    | C_m_r => False           
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    44
    | C_r_s => False           
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    45
    | C_r_r(m) => False)"
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    46
 apply (simp (no_asm) add: externals_def restrict_def restrict_asig_def Spec.sig_def asig_projections)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    47
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    48
  apply (induct_tac "a")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    49
  apply (simp_all (no_asm) add: actions_def asig_projections)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    50
  txt {* 2 *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    51
  apply (simp (no_asm) add: impl_ioas)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    52
  apply (simp (no_asm) add: impl_asigs)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    53
  apply (simp (no_asm) add: asig_of_par asig_comp_def asig_projections)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    54
  apply (simp (no_asm) add: "transitions" unfold_renaming)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    55
  txt {* 1 *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    56
  apply (simp (no_asm) add: impl_ioas)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    57
  apply (simp (no_asm) add: impl_asigs)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    58
  apply (simp (no_asm) add: asig_of_par asig_comp_def asig_projections)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    59
  done
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    60
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    61
lemmas sels = sbit_def sq_def ssending_def rbit_def rq_def rsending_def
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    62
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    63
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    64
text {* Proof of correctness *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    65
lemma ntp_correct:
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    66
  "is_weak_ref_map hom (Automata.restrict impl_ioa (externals spec_sig)) spec_ioa"
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    67
apply (unfold Spec.ioa_def is_weak_ref_map_def)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    68
apply (simp (no_asm) cong del: if_weak_cong split del: split_if add: Correctness.hom_def
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    69
  cancel_restrict externals_lemma)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    70
apply (rule conjI)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    71
 apply (simp (no_asm) add: hom_ioas)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    72
 apply (simp (no_asm_simp) add: sels)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    73
apply (rule allI)+
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    74
apply (rule imp_conj_lemma)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    75
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    76
apply (induct_tac "a")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    77
apply (simp_all (no_asm_simp) add: hom_ioas)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    78
apply (frule inv4)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    79
apply force
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    80
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    81
apply (frule inv4)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    82
apply (frule inv2)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    83
apply (erule disjE)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    84
apply (simp (no_asm_simp))
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    85
apply force
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    86
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    87
apply (frule inv2)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    88
apply (erule disjE)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    89
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    90
apply (frule inv3)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    91
apply (case_tac "sq (sen (s))=[]")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    92
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    93
apply (simp add: hom_ioas)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    94
apply (blast dest!: add_leD1 [THEN leD])
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    95
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    96
apply (case_tac "m = hd (sq (sen (s)))")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    97
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    98
apply force
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    99
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   100
apply simp
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   101
apply (blast dest!: add_leD1 [THEN leD])
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   102
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   103
apply simp
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   104
done
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
   105
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   106
end