# Theory Correctness

Up to index of Isabelle/HOLCF/IOA/ABP

theory Correctness
imports IOA Env Impl Impl_finite
uses [Correctness.ML]
begin

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

    header {* The main correctness proof: System_fin implements System *}

    theory Correctness
    imports IOA Env Impl Impl_finite
    begin

    consts

    reduce           :: "'a list => 'a list"

    abs              :: 'c
    system_ioa       :: "('m action, bool * 'm impl_state)ioa"
    system_fin_ioa   :: "('m action, bool * 'm impl_state)ioa"

    primrec
      reduce_Nil:  "reduce [] = []"
      reduce_Cons: "reduce(x#xs) =
                     (case xs of
                         [] => [x]
                   |   y#ys => (if (x=y)
                                  then reduce xs
                                  else (x#(reduce xs))))"

    defs

    system_def:
      "system_ioa == (env_ioa || impl_ioa)"

    system_fin_def:
      "system_fin_ioa == (env_ioa || impl_fin_ioa)"

    abs_def: "abs  ==
            (%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))),
             (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))"

    axioms

      sys_IOA:     "IOA system_ioa"
      sys_fin_IOA: "IOA system_fin_ioa"

    ML {* use_legacy_bindings (the_context ()) *}

    end

theorem hd_is_reduce_hd:

      s ≠ [] --> hd s = hd (reduce s)

theorem rev_red_not_nil:

      l ≠ [] ==> reverse (reduce l) ≠ []

theorem last_ind_on_first:

      l ≠ [] ==> hd (reverse (reduce (a # l))) = hd (reverse (reduce l))

theorem reduce_hd:

      if x = hd (reverse (reduce l)) ∧ reduce l ≠ [] then reduce (l @ [x]) = reduce l
      else reduce (l @ [x]) = reduce l @ [x]

theorem channel_abstraction:

      is_weak_ref_map reduce ch_ioa ch_fin_ioa

theorem sender_abstraction:

      is_weak_ref_map reduce srch_ioa srch_fin_ioa

theorem receiver_abstraction:

      is_weak_ref_map reduce rsch_ioa rsch_fin_ioa

theorem sender_unchanged:

      is_weak_ref_map (%id. id) sender_ioa sender_ioa

theorem receiver_unchanged:

      is_weak_ref_map (%id. id) receiver_ioa receiver_ioa

theorem env_unchanged:

      is_weak_ref_map (%id. id) env_ioa env_ioa