Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Correctness.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/HOLCF/IOA/NTP/Correctness.thy
    Author:     Tobias Nipkow & Konrad Slind
*)

section \<open>The main correctness proof: Impl implements Spec\<close>

theory Correctness
imports Impl Spec
begin

definition
  hom :: "'m impl_state => 'm list" where
  "hom s = rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s)
                         else tl(sq(sen s)))"

setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close>

lemmas hom_ioas = Spec.ioa_def Spec.trans_def sender_trans_def receiver_trans_def impl_ioas
  and impl_asigs = sender_asig_def receiver_asig_def srch_asig_def rsch_asig_def

declare split_paired_All [simp del]

text \<open>
  A lemma about restricting the action signature of the implementation
  to that of the specification.
\<close>

lemma externals_lemma:
"a\externals(asig_of(Automata.restrict impl_ioa (externals spec_sig))) =
  (case a of
      S_msg(m) \<Rightarrow> True
    | R_msg(m) \<Rightarrow> True
    | S_pkt(pkt) \<Rightarrow> False
    | R_pkt(pkt) \<Rightarrow> False
    | S_ack(b) \<Rightarrow> False
    | R_ack(b) \<Rightarrow> False
    | C_m_s \<Rightarrow> False
    | C_m_r \<Rightarrow> False
    | C_r_s \<Rightarrow> False
    | C_r_r(m) \<Rightarrow> False)"
apply (simp (no_asm) add: externals_def restrict_def restrict_asig_def Spec.sig_def asig_projections)

  apply (induct_tac "a")
  apply (simp_all (no_asm) add: actions_def asig_projections)
  txt \<open>2\<close>
  apply (simp (no_asm) add: impl_ioas)
  apply (simp (no_asm) add: impl_asigs)
  apply (simp (no_asm) add: asig_of_par asig_comp_def asig_projections)
  apply (simp (no_asm) add: "transitions"(1) unfold_renaming)
  txt \<open>1\<close>
  apply (simp (no_asm) add: impl_ioas)
  apply (simp (no_asm) add: impl_asigs)
  apply (simp (no_asm) add: asig_of_par asig_comp_def asig_projections)
  done

lemmas sels = sbit_def sq_def ssending_def rbit_def rq_def rsending_def

text \<open>Proof of correctness\<close>
lemma ntp_correct:
  "is_weak_ref_map hom (Automata.restrict impl_ioa (externals spec_sig)) spec_ioa"
apply (unfold Spec.ioa_def is_weak_ref_map_def)
apply (simp (no_asm) cong del: if_weak_cong split del: if_split add: Correctness.hom_def
  cancel_restrict externals_lemma)
apply (rule conjI)
apply (simp (no_asm) add: hom_ioas)
apply (simp (no_asm_simp) add: sels)
apply (rule allI)+
apply (rule imp_conj_lemma)

apply (induct_tac "a")
apply (simp_all (no_asm_simp) add: hom_ioas)
apply (frule inv4)
apply force

apply (frule inv4)
apply (frule inv2)
apply (erule disjE)
apply (simp (no_asm_simp))
apply force

apply (frule inv2)
apply (erule disjE)

apply (frule inv3)
apply (case_tac "sq (sen (s))=[]")

apply (simp add: hom_ioas)
apply (blast dest!: add_leD1 [THEN leD])

apply (rename_tac m, case_tac "m = hd (sq (sen (s)))")

apply force

apply simp
apply (blast dest!: add_leD1 [THEN leD])

apply simp
done

end

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.