# Theory Correctness

Up to index of Isabelle/HOLCF/IOA/Storage

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

    (*  Title:      HOL/IOA/example/Correctness.thy
        ID:         $Id: Correctness.thy,v 1.5 2005/09/03 14:50:25 wenzelm Exp $
        Author:     Olaf Müller
    *)

    header {* Correctness Proof *}

    theory Correctness
    imports SimCorrectness Spec Impl
    begin

    defaultsort type

    constdefs
      sim_relation   :: "((nat * bool) * (nat set * bool)) set"
      "sim_relation == {qua. let c = fst qua; a = snd qua ;
                                 k = fst c;   b = snd c;
                                 used = fst a; c = snd a
                             in
                             (! l:used. l < k) & b=c }"

    ML {* use_legacy_bindings (the_context ()) *}

    end

theorem issimulation:

      is_simulation sim_relation impl_ioa spec_ioa

theorem implementation:

      impl_ioa =<| spec_ioa