Lvc.IL.Events
Require Import List.
Require Export Util Relations Relations2 Val Exp AutoIndTac.
Set Implicit Arguments.
Definition external := nat.
Inductive extern :=
ExternI {
extern_fnc : external;
extern_args : list val;
extern_res : val
}.
Inductive event :=
| EvtExtern (call:extern)
| EvtTau.
Definition internally_deterministic {X : Type} (R : X → event → X → Prop)
:= ∀ x y x1 x2, R x EvtTau x1 → R x y x2 → x1 = x2 ∧ y = EvtTau.
Definition externally_determined {X : Type} (R : X → event → X → Prop)
:= ∀ x e x1 x2, R x e x1 → R x e x2 → x1 = x2.
Definition filter_tau (o:event) (L:list event) : list event :=
match o with
| EvtTau ⇒ L
| e ⇒ e :: L
end.
Lemma filter_tau_nil evt B
: (filter_tau evt nil ++ B)%list = filter_tau evt B.
Lemma filter_tau_app evt A B
: (filter_tau evt A ++ B)%list = filter_tau evt (A ++ B).
Inductive plus2 (X : Type) (R : X → event → X → Prop)
: X → list event → X → Prop :=
plus2O x y x´ el
: R x y x´
→ el = (filter_tau y nil)
→ plus2 R x el x´
| plus2S x y x´ yl z el
: R x y x´
→ el = (filter_tau y yl)
→ plus2 R x´ yl z
→ plus2 R x el z.
Inductive star2 (X : Type) (R : X → event → X → Prop) : X → list event → X → Prop :=
star2_refl : ∀ x : X, star2 R x nil x
| S_star2 : ∀ y x x´ yl z, R x y x´ → star2 R x´ yl z → star2 R x (filter_tau y yl) z.
Lemma star2_plus2_plus2
: ∀ (X : Type) R (x y z : X) A B,
star2 R x A y → plus2 R y B z → plus2 R x (A++B) z.
Lemma star2_trans
: ∀ (X : Type) R (x y z : X) A B,
star2 R x A y → star2 R y B z → star2 R x (A++B) z.
Lemma plus2_destr_nil
: ∀ (X : Type) R (x z : X),
plus2 R x nil z → ∃ y : X, R x EvtTau y ∧ star2 R y nil z.
Lemma star2_plus2
: ∀ (X : Type) (R: X → event → X → Prop) (x y z : X),
R x EvtTau y → star2 R y nil z → plus2 R x nil z.
Lemma star2_reach X (R:X → event → X → Prop) σ1 σ2a σ2b
: star2 R σ1 nil σ2a
→ star2 R σ1 nil σ2b
→ internally_deterministic R
→ (star2 R σ2a nil σ2b ∨ star2 R σ2b nil σ2a).
Lemma star2_reach_normal X (R:X → event → X → Prop) σ1 σ2a σ2b
: star2 R σ1 nil σ2a
→ star2 R σ1 nil σ2b
→ internally_deterministic R
→ normal2 R σ2a
→ star2 R σ2b nil σ2a.
Lemma star2_reach_normal2 X (R:X → event → X → Prop) σ1 σ2a σ2b
: star2 R σ1 nil σ2a
→ star2 R σ1 nil σ2b
→ internally_deterministic R
→ normal2 R σ2a
→ normal2 R σ2b
→ σ2a = σ2b.
Lemma plus2_reach X (R:X → event → X → Prop) σ1 σ2a σ2b
: plus2 R σ1 nil σ2a
→ plus2 R σ1 nil σ2b
→ internally_deterministic R
→ (star2 R σ2a nil σ2b ∨ star2 R σ2b nil σ2a).
Inductive star2n (X : Type) (R : X → event → X → Prop) : nat → X → list event → X → Prop :=
star2n_refl : ∀ x : X, star2n R 0 x nil x
| S_star2n n : ∀ y x x´ yl z,
R x y x´
→ star2n R n x´ yl z
→ star2n R (S n) x (filter_tau y yl) z.
Inductive plus2n (X : Type) (R : X → event → X → Prop)
: nat → X → list event → X → Prop :=
plus2nO x y x´ el
: R x y x´
→ el = (filter_tau y nil)
→ plus2n R 0 x el x´
| plus2nS n x y x´ yl z el
: R x y x´
→ el = (filter_tau y yl)
→ plus2n R n x´ yl z
→ plus2n R (S n) x el z.
Lemma plus2_plus2n X (R: X → event → X → Prop) x A y
: plus2 R x A y
→ ∃ n, plus2n R n x A y.
Lemma star2n_star2 X (R: X → event → X → Prop) x A y n
: star2n R n x A y
→ star2 R x A y.
Lemma plus2n_star2n X (R: X → event → X → Prop) x A y n
: plus2n R n x A y
→ star2n R (S n) x A y.
Lemma star2_star2n X (R: X → event → X → Prop) x A y
: star2 R x A y
→ ∃ n, star2n R n x A y.
Lemma star2n_reach X (R:X → event → X → Prop) σ1 σ2a σ2b n n´
: star2n R n σ1 nil σ2a
→ star2n R n´ σ1 nil σ2b
→ internally_deterministic R
→ (star2n R (n´-n) σ2a nil σ2b ∨ star2n R (n-n´) σ2b nil σ2a).
Lemma plus2_star2 X R (x y:X) A
: plus2 R x A y
→ star2 R x A y.
Lemma star2_normal X R (x y:X)
: star2 R x nil y
→ normal2 R x
→ x = y.
Lemma star2_reach_silent_step (X : Type) (R:X → event → X → Prop) (x y z : X)
: R x EvtTau y
→ star2 R x nil z
→ internally_deterministic R
→ x = z ∨ star2 R y nil z.
Require Export Util Relations Relations2 Val Exp AutoIndTac.
Set Implicit Arguments.
Definition external := nat.
Inductive extern :=
ExternI {
extern_fnc : external;
extern_args : list val;
extern_res : val
}.
Inductive event :=
| EvtExtern (call:extern)
| EvtTau.
Definition internally_deterministic {X : Type} (R : X → event → X → Prop)
:= ∀ x y x1 x2, R x EvtTau x1 → R x y x2 → x1 = x2 ∧ y = EvtTau.
Definition externally_determined {X : Type} (R : X → event → X → Prop)
:= ∀ x e x1 x2, R x e x1 → R x e x2 → x1 = x2.
Definition filter_tau (o:event) (L:list event) : list event :=
match o with
| EvtTau ⇒ L
| e ⇒ e :: L
end.
Lemma filter_tau_nil evt B
: (filter_tau evt nil ++ B)%list = filter_tau evt B.
Lemma filter_tau_app evt A B
: (filter_tau evt A ++ B)%list = filter_tau evt (A ++ B).
Inductive plus2 (X : Type) (R : X → event → X → Prop)
: X → list event → X → Prop :=
plus2O x y x´ el
: R x y x´
→ el = (filter_tau y nil)
→ plus2 R x el x´
| plus2S x y x´ yl z el
: R x y x´
→ el = (filter_tau y yl)
→ plus2 R x´ yl z
→ plus2 R x el z.
Inductive star2 (X : Type) (R : X → event → X → Prop) : X → list event → X → Prop :=
star2_refl : ∀ x : X, star2 R x nil x
| S_star2 : ∀ y x x´ yl z, R x y x´ → star2 R x´ yl z → star2 R x (filter_tau y yl) z.
Lemma star2_plus2_plus2
: ∀ (X : Type) R (x y z : X) A B,
star2 R x A y → plus2 R y B z → plus2 R x (A++B) z.
Lemma star2_trans
: ∀ (X : Type) R (x y z : X) A B,
star2 R x A y → star2 R y B z → star2 R x (A++B) z.
Lemma plus2_destr_nil
: ∀ (X : Type) R (x z : X),
plus2 R x nil z → ∃ y : X, R x EvtTau y ∧ star2 R y nil z.
Lemma star2_plus2
: ∀ (X : Type) (R: X → event → X → Prop) (x y z : X),
R x EvtTau y → star2 R y nil z → plus2 R x nil z.
Lemma star2_reach X (R:X → event → X → Prop) σ1 σ2a σ2b
: star2 R σ1 nil σ2a
→ star2 R σ1 nil σ2b
→ internally_deterministic R
→ (star2 R σ2a nil σ2b ∨ star2 R σ2b nil σ2a).
Lemma star2_reach_normal X (R:X → event → X → Prop) σ1 σ2a σ2b
: star2 R σ1 nil σ2a
→ star2 R σ1 nil σ2b
→ internally_deterministic R
→ normal2 R σ2a
→ star2 R σ2b nil σ2a.
Lemma star2_reach_normal2 X (R:X → event → X → Prop) σ1 σ2a σ2b
: star2 R σ1 nil σ2a
→ star2 R σ1 nil σ2b
→ internally_deterministic R
→ normal2 R σ2a
→ normal2 R σ2b
→ σ2a = σ2b.
Lemma plus2_reach X (R:X → event → X → Prop) σ1 σ2a σ2b
: plus2 R σ1 nil σ2a
→ plus2 R σ1 nil σ2b
→ internally_deterministic R
→ (star2 R σ2a nil σ2b ∨ star2 R σ2b nil σ2a).
Inductive star2n (X : Type) (R : X → event → X → Prop) : nat → X → list event → X → Prop :=
star2n_refl : ∀ x : X, star2n R 0 x nil x
| S_star2n n : ∀ y x x´ yl z,
R x y x´
→ star2n R n x´ yl z
→ star2n R (S n) x (filter_tau y yl) z.
Inductive plus2n (X : Type) (R : X → event → X → Prop)
: nat → X → list event → X → Prop :=
plus2nO x y x´ el
: R x y x´
→ el = (filter_tau y nil)
→ plus2n R 0 x el x´
| plus2nS n x y x´ yl z el
: R x y x´
→ el = (filter_tau y yl)
→ plus2n R n x´ yl z
→ plus2n R (S n) x el z.
Lemma plus2_plus2n X (R: X → event → X → Prop) x A y
: plus2 R x A y
→ ∃ n, plus2n R n x A y.
Lemma star2n_star2 X (R: X → event → X → Prop) x A y n
: star2n R n x A y
→ star2 R x A y.
Lemma plus2n_star2n X (R: X → event → X → Prop) x A y n
: plus2n R n x A y
→ star2n R (S n) x A y.
Lemma star2_star2n X (R: X → event → X → Prop) x A y
: star2 R x A y
→ ∃ n, star2n R n x A y.
Lemma star2n_reach X (R:X → event → X → Prop) σ1 σ2a σ2b n n´
: star2n R n σ1 nil σ2a
→ star2n R n´ σ1 nil σ2b
→ internally_deterministic R
→ (star2n R (n´-n) σ2a nil σ2b ∨ star2n R (n-n´) σ2b nil σ2a).
Lemma plus2_star2 X R (x y:X) A
: plus2 R x A y
→ star2 R x A y.
Lemma star2_normal X R (x y:X)
: star2 R x nil y
→ normal2 R x
→ x = y.
Lemma star2_reach_silent_step (X : Type) (R:X → event → X → Prop) (x y z : X)
: R x EvtTau y
→ star2 R x nil z
→ internally_deterministic R
→ x = z ∨ star2 R y nil z.