# Theory Abstraction

Up to index of Isabelle/HOLCF/IOA

theory Abstraction
imports LiveIOA
uses [Abstraction.ML]
begin

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

    header {* Abstraction Theory -- tailored for I/O automata *}

    theory Abstraction
    imports LiveIOA
    begin

    defaultsort type

    consts

      cex_abs      ::"('s1 => 's2) => ('a,'s1)execution => ('a,'s2)execution"
      cex_absSeq   ::"('s1 => 's2) => ('a option,'s1)transition Seq => ('a option,'s2)transition Seq"

      is_abstraction ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool"

      weakeningIOA       :: "('a,'s2)ioa => ('a,'s1)ioa => ('s1 => 's2) => bool"
      temp_weakening     :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool"
      temp_strengthening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool"

      state_weakening       :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool"
      state_strengthening   :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool"

      is_live_abstraction  :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool"

    defs

    is_abstraction_def:
      "is_abstraction f C A ==
       (!s:starts_of(C). f(s):starts_of(A)) &
       (!s t a. reachable C s & s -a--C-> t
                --> (f s) -a--A-> (f t))"

    is_live_abstraction_def:
      "is_live_abstraction h CL AM ==
          is_abstraction h (fst CL) (fst AM) &
          temp_weakening (snd AM) (snd CL) h"

    cex_abs_def:
      "cex_abs f ex == (f (fst ex), Map (%(a,t). (a,f t))$(snd ex))"

    (* equals cex_abs on Sequneces -- after ex2seq application -- *)
    cex_absSeq_def:
      "cex_absSeq f == % s. Map (%(s,a,t). (f s,a,f t))$s"

    weakeningIOA_def:
       "weakeningIOA A C h == ! ex. ex : executions C --> cex_abs h ex : executions A"

    temp_weakening_def:
       "temp_weakening Q P h == temp_strengthening (.~ Q) (.~ P) h"

    temp_strengthening_def:
       "temp_strengthening Q P h == ! ex. (cex_abs h ex |== Q) --> (ex |== P)"

    state_weakening_def:
      "state_weakening Q P h == state_strengthening (.~Q) (.~P) h"

    state_strengthening_def:
      "state_strengthening Q P h == ! s t a.  Q (h(s),a,h(t)) --> P (s,a,t)"

    axioms

    (* thm about ex2seq which is not provable by induction as ex2seq is not continous *)
    ex2seq_abs_cex:
      "ex2seq (cex_abs h ex) = cex_absSeq h (ex2seq ex)"

    (* analog to the proved thm strength_Box - proof skipped as trivial *)
    weak_Box:
    "temp_weakening P Q h
     ==> temp_weakening ([] P) ([] Q) h"

    (* analog to the proved thm strength_Next - proof skipped as trivial *)
    weak_Next:
    "temp_weakening P Q h
     ==> temp_weakening (Next P) (Next Q) h"

    ML {* use_legacy_bindings (the_context ()) *}

    end

## cex_abs

theorem cex_abs_UU:

      cex_abs f (s, UU) = (f s, UU)

theorem cex_abs_nil:

      cex_abs f (s, nil) = (f s, nil)

theorem cex_abs_cons:

      cex_abs f (s, (a, t)>>ex) = (f s, (a, f t)>>snd (cex_abs f (t, ex)))

## lemmas

theorem temp_weakening_def2:

      temp_weakening Q P h = (∀ex. (ex |== P) --> (cex_abs h ex |== Q))

theorem state_weakening_def2:

      state_weakening Q P h = (∀s t a. P (s, a, t) --> Q (h s, a, h t))

## Abstraction Rules for Properties

theorem exec_frag_abstraction:

      [| is_abstraction h C A; reachable C s ∧ is_exec_frag C (s, xs) |]
      ==> is_exec_frag A (cex_abs h (s, xs))

theorem abs_is_weakening:

      is_abstraction h C A ==> weakeningIOA A C h

theorem AbsRuleT1:

      [| is_abstraction h C A; validIOA A Q; temp_strengthening Q P h |]
      ==> validIOA C P

theorem IMPLIES_temp_sat:

      (ex |== P --> Q) = ((ex |== P) --> (ex |== Q))

theorem AND_temp_sat:

      (ex |== P ∧ Q) = ((ex |== P) ∧ (ex |== Q))

theorem OR_temp_sat:

      (ex |== P ∨ Q) = ((ex |== P) ∨ (ex |== Q))

theorem NOT_temp_sat:

      (ex |== ¬ P) = (¬ (ex |== P))

theorem AbsRuleT2:

      [| is_live_abstraction h (C, L) (A, M); validLIOA (A, M) Q;
         temp_strengthening Q P h |]
      ==> validLIOA (C, L) P

theorem AbsRuleTImprove:

      [| is_live_abstraction h (C, L) (A, M); validLIOA (A, M) (H1.0 --> Q);
         temp_strengthening Q P h; temp_weakening H1.0 H2.0 h;
         validLIOA (C, L) H2.0 |]
      ==> validLIOA (C, L) P

## Correctness of safe abstraction

theorem abstraction_is_ref_map:

      is_abstraction h C A ==> is_ref_map h C A

theorem abs_safety:

      [| inp C = inp A; out C = out A; is_abstraction h C A |] ==> C =<| A

## Correctness of life abstraction

theorem traces_coincide_abs:

      ext C = ext A ==> mk_trace C·xs = mk_trace A·(snd (cex_abs f (s, xs)))

theorem abs_liveness:

      [| inp C = inp A; out C = out A; is_live_abstraction h (C, M) (A, L) |]
      ==> live_implements (C, M) (A, L)

theorem implements_trans:

      [| A =<| B; B =<| C |] ==> A =<| C

## Abstraction Rules for Automata

theorem AbsRuleA1:

      [| inp C = inp A; out C = out A; inp Q = inp P; out Q = out P;
         is_abstraction h1.0 C A; A =<| Q; is_abstraction h2.0 Q P |]
      ==> C =<| P

theorem AbsRuleA2:

      [| inp C = inp A; out C = out A; inp Q = inp P; out Q = out P;
         is_live_abstraction h1.0 (C, LC) (A, LA); live_implements (A, LA) (Q, LQ);
         is_live_abstraction h2.0 (Q, LQ) (P, LP) |]
      ==> live_implements (C, LC) (P, LP)

## Localizing Temporal Strengthenings and Weakenings

theorem strength_AND:

      [| temp_strengthening P1.0 Q1.0 h; temp_strengthening P2.0 Q2.0 h |]
      ==> temp_strengthening (P1.0 ∧ P2.0) (Q1.0 ∧ Q2.0) h

theorem strength_OR:

      [| temp_strengthening P1.0 Q1.0 h; temp_strengthening P2.0 Q2.0 h |]
      ==> temp_strengthening (P1.0 ∨ P2.0) (Q1.0 ∨ Q2.0) h

theorem strength_NOT:

      temp_weakening P Q h ==> temp_strengthening (¬ P) (¬ Q) h

theorem strength_IMPLIES:

      [| temp_weakening P1.0 Q1.0 h; temp_strengthening P2.0 Q2.0 h |]
      ==> temp_strengthening (P1.0 --> P2.0) (Q1.0 --> Q2.0) h

theorem weak_AND:

      [| temp_weakening P1.0 Q1.0 h; temp_weakening P2.0 Q2.0 h |]
      ==> temp_weakening (P1.0 ∧ P2.0) (Q1.0 ∧ Q2.0) h

theorem weak_OR:

      [| temp_weakening P1.0 Q1.0 h; temp_weakening P2.0 Q2.0 h |]
      ==> temp_weakening (P1.0 ∨ P2.0) (Q1.0 ∨ Q2.0) h

theorem weak_NOT:

      temp_strengthening P Q h ==> temp_weakening (¬ P) (¬ Q) h

theorem weak_IMPLIES:

      [| temp_strengthening P1.0 Q1.0 h; temp_weakening P2.0 Q2.0 h |]
      ==> temp_weakening (P1.0 --> P2.0) (Q1.0 --> Q2.0) h

theorem UU_is_Conc:

      (UU = x @@ y) = (x = UU ∨ x = nil ∧ y = UU)

theorem ex2seqConc:

      [| Finite s1.0; s ≠ nil ∧ s ≠ UU ∧ ex2seq ex = s1.0 @@ s |]
      ==> ∃ex'. s = ex2seq ex'

theorem ex2seq_tsuffix:

      tsuffix s (ex2seq ex) ==> ∃ex'. s = ex2seq ex'

theorem Mapnil:

      (Map f·s = nil) = (s = nil)

theorem MapUU:

      (Map f·s = UU) = (s = UU)

theorem cex_absSeq_tsuffix:

      tsuffix s t ==> tsuffix (cex_absSeq h s) (cex_absSeq h t)

theorem strength_Box:

      temp_strengthening P Q h ==> temp_strengthening ([] P) ([] Q) h

theorem strength_Init:

      state_strengthening P Q h ==> temp_strengthening <P> <Q> h

theorem TL_ex2seq_UU:

      (TL·(ex2seq (cex_abs h ex)) = UU) = (TL·(ex2seq ex) = UU)

theorem TL_ex2seq_nil:

      (TL·(ex2seq (cex_abs h ex)) = nil) = (TL·(ex2seq ex) = nil)

theorem MapTL:

      Map f·(TL·s) = TL·(Map f·s)

theorem cex_absSeq_TL:

      cex_absSeq h (TL·s) = TL·(cex_absSeq h s)

theorem TLex2seq:

      [| snd ex ≠ UU; snd ex ≠ nil |] ==> ∃ex'. TL·(ex2seq ex) = ex2seq ex'

theorem ex2seqnilTL:

      (TL·(ex2seq ex) ≠ nil) = (snd ex ≠ nil ∧ snd ex ≠ UU)

theorem strength_Next:

      temp_strengthening P Q h ==> temp_strengthening (Next P) (Next Q) h

theorem weak_Init:

      state_weakening P Q h ==> temp_weakening <P> <Q> h

theorem strength_Diamond:

      temp_strengthening P Q h ==> temp_strengthening (<> P) (<> Q) h

theorem strength_Leadsto:

      [| temp_weakening P1.0 P2.0 h; temp_strengthening Q1.0 Q2.0 h |]
      ==> temp_strengthening (P1.0 ~> Q1.0) (P2.0 ~> Q2.0) h

theorem weak_Diamond:

      temp_weakening P Q h ==> temp_weakening (<> P) (<> Q) h

theorem weak_Leadsto:

      [| temp_strengthening P1.0 P2.0 h; temp_weakening Q1.0 Q2.0 h |]
      ==> temp_weakening (P1.0 ~> Q1.0) (P2.0 ~> Q2.0) h

theorem weak_WF:

      (!!s. Enabled A acts (h s) ==> Enabled C acts s)
      ==> temp_weakening (WF A acts) (WF C acts) h

theorem weak_SF:

      (!!s. Enabled A acts (h s) ==> Enabled C acts s)
      ==> temp_weakening (SF A acts) (SF C acts) h