# Theory Correctness

Up to index of Isabelle/HOLCF/IOA/NTP

theory Correctness
imports Impl Spec
uses [Correctness.ML]
begin

    (*  Title:      HOL/IOA/NTP/Correctness.thy
        ID:         $Id: Correctness.thy,v 1.6 2005/09/03 14:50:24 wenzelm Exp $
        Author:     Tobias Nipkow & Konrad Slind
    *)

    header {* The main correctness proof: Impl implements Spec *}

    theory Correctness
    imports Impl Spec
    begin

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

    ML {* use_legacy_bindings (the_context ()) *}

    end

theorem externals_lemma:

      (a ∈ ext (restrict impl_ioa (externals spec_sig))) =
      (case a of S_msg m => True | R_msg m => True | _ => False)

theorem ntp_correct:

      is_weak_ref_map hom (restrict impl_ioa (externals spec_sig)) spec_ioa