Up to index of Isabelle/HOLCF/IOA
theory Abstraction(* 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
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)))
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))
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
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
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
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)
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