# Theory RefCorrectness

Up to index of Isabelle/HOLCF/IOA

theory RefCorrectness
imports RefMappings
uses [RefCorrectness.ML]
begin

    (*  Title:      HOLCF/IOA/meta_theory/RefCorrectness.thy
        ID:         $Id: RefCorrectness.thy,v 1.9 2005/09/02 15:24:01 wenzelm Exp $
        Author:     Olaf Müller
    *)

    header {* Correctness of Refinement Mappings in HOLCF/IOA *}

    theory RefCorrectness
    imports RefMappings
    begin

    consts

      corresp_ex   ::"('a,'s2)ioa => ('s1 => 's2) =>
                      ('a,'s1)execution => ('a,'s2)execution"
      corresp_exC  ::"('a,'s2)ioa => ('s1 => 's2) => ('a,'s1)pairs
                       -> ('s1 => ('a,'s2)pairs)"
      is_fair_ref_map  :: "('s1 => 's2) => ('a,'s1)ioa => ('a,'s2)ioa => bool"

    defs

    corresp_ex_def:
      "corresp_ex A f ex == (f (fst ex),(corresp_exC A f$(snd ex)) (fst ex))"

    corresp_exC_def:
      "corresp_exC A f  == (fix$(LAM h ex. (%s. case ex of
          nil =>  nil
        | x##xs => (flift1 (%pr. (@cex. move A cex (f s) (fst pr) (f (snd pr)))
                                  @@ ((h$xs) (snd pr)))
                            $x) )))"

    is_fair_ref_map_def:
      "is_fair_ref_map f C A ==
           is_ref_map f C A &
           (! ex : executions(C). fair_ex C ex --> fair_ex A (corresp_ex A f ex))"

    axioms
    (* Axioms for fair trace inclusion proof support, not for the correctness proof
       of refinement mappings!
       Note: Everything is superseded by LiveIOA.thy! *)

    corresp_laststate:
      "Finite ex ==> laststate (corresp_ex A f (s,ex)) = f (laststate (s,ex))"

    corresp_Finite:
      "Finite (snd (corresp_ex A f (s,ex))) = Finite ex"

    FromAtoC:
      "fin_often (%x. P (snd x)) (snd (corresp_ex A f (s,ex))) ==> fin_often (%y. P (f (snd y))) ex"

    FromCtoA:
      "inf_often (%y. P (fst y)) ex ==> inf_often (%x. P (fst x)) (snd (corresp_ex A f (s,ex)))"

    (* Proof by case on inf W in ex: If so, ok. If not, only fin W in ex, ie there is
       an index i from which on no W in ex. But W inf enabled, ie at least once after i
       W is enabled. As W does not occur after i and W is enabling_persistent, W keeps
       enabled until infinity, ie. indefinitely *)
    persistent:
      "[|inf_often (%x. Enabled A W (snd x)) ex; en_persistent A W|]
       ==> inf_often (%x. fst x :W) ex | fin_often (%x. ~Enabled A W (snd x)) ex"

    infpostcond:
      "[| is_exec_frag A (s,ex); inf_often (%x. fst x:W) ex|]
        ==> inf_often (% x. set_was_enabled A W (snd x)) ex"

    ML {* use_legacy_bindings (the_context ()) *}

    end

## corresp_ex

theorem corresp_exC_unfold:

      corresp_exC A f =
      (LAM ex.
          (%s. case ex of nil => nil
               | x ## xs =>
                   (FLIFT pr.
                       (SOME cex. move A cex (f s) (fst pr) (f (snd pr))) @@
                       (corresp_exC A f·xs) (snd pr))·x))

theorem corresp_exC_UU:

      (corresp_exC A f·UU) s = UU

theorem corresp_exC_nil:

      (corresp_exC A f·nil) s = nil

theorem corresp_exC_cons:

      (corresp_exC A f·(at>>xs)) s =
      (SOME cex. move A cex (f s) (fst at) (f (snd at))) @@
      (corresp_exC A f·xs) (snd at)

## properties of move

theorem move_is_move:

      [| is_ref_map f C A; reachable C s; s -a--C-> t |]
      ==> move A (SOME x. move A x (f s) a (f t)) (f s) a (f t)

theorem move_subprop1:

      [| is_ref_map f C A; reachable C s; s -a--C-> t |]
      ==> is_exec_frag A (f s, SOME x. move A x (f s) a (f t))

theorem move_subprop2:

      [| is_ref_map f C A; reachable C s; s -a--C-> t |]
      ==> Finite (SOME x. move A x (f s) a (f t))

theorem move_subprop3:

      [| is_ref_map f C A; reachable C s; s -a--C-> t |]
      ==> laststate (f s, SOME x. move A x (f s) a (f t)) = f t

theorem move_subprop4:

      [| is_ref_map f C A; reachable C s; s -a--C-> t |]
      ==> mk_trace A·(SOME x. move A x (f s) a (f t)) =
          (if a ∈ ext A then [a!] else nil)

## Lemmata for <==

theorem mk_traceConc:

      mk_trace C·(ex1.0 @@ ex2.0) = mk_trace C·ex1.0 @@ mk_trace C·ex2.0

theorem lemma_1:

      [| is_ref_map f C A; ext C = ext A |]
      ==> ∀s. reachable C s ∧ is_exec_frag C (s, xs) -->
              mk_trace C·xs = mk_trace A·(snd (corresp_ex A f (s, xs)))

## Lemmata for ==>

theorem lemma_2_1:

      [| Finite xs;
         is_exec_frag A (s, xs) ∧ is_exec_frag A (t, ys) ∧ t = laststate (s, xs) |]
      ==> is_exec_frag A (s, xs @@ ys)

theorem lemma_2:

      is_ref_map f C A
      ==> ∀s. reachable C s ∧ is_exec_frag C (s, xs) -->
              is_exec_frag A (corresp_ex A f (s, xs))

## Main Theorem: T R A C E - I N C L U S I O N

theorem trace_inclusion:

      [| ext C = ext A; is_ref_map f C A |] ==> traces C ⊆ traces A

## Corollary: F A I R T R A C E - I N C L U S I O N

theorem fininf:

      (¬ inf_often P s) = fin_often P s

theorem WF_alt:

      is_wfair A W (s, ex) =
      (fin_often (%x. ¬ Enabled A W (snd x)) ex --> inf_often (%x. fst x ∈ W) ex)

theorem WF_persistent:

      [| is_wfair A W (s, ex); inf_often (%x. Enabled A W (snd x)) ex;
         en_persistent A W |]
      ==> inf_often (%x. fst x ∈ W) ex

theorem fair_trace_inclusion:

      [| is_ref_map f C A; ext C = ext A;
         !!ex. [| ex ∈ executions C; fair_ex C ex |]
               ==> fair_ex A (corresp_ex A f ex) |]
      ==> fairtraces C ⊆ fairtraces A

theorem fair_trace_inclusion2:

      [| inp C = inp A; out C = out A; is_fair_ref_map f C A |]
      ==> fair_implements C A