(* begin hide *)
Reset Initial.

Open Scope type_scope.
(* end hide *)



(** * Subsets *)


Definition Subset (X : Type) := X -> Prop.

Definition Contained (X : Type) (X1 X2 : Subset X) :=
  forall x, X1 x -> X2 x.

Definition eq_Subset (X : Type) (X1 X2 : Subset X) :=
  Contained X X1 X2 /\ Contained X X2 X1.

Definition Union (X : Type) (X1 X2 : Subset X) (x : X) := X1 x \/ X2 x.

Definition Intersect (X : Type) (X1 X2 : Subset X) (x : X) := X1 x /\ X2 x.

Definition Emptyset (X : Type) (x : X) := False.


Definition eq_ext (A B : Type) (f g : A -> B) :=
  forall a, f a = g a.




(** * Definitions *)


(** Variables and Events *)

Parameter Var : Set.
Axiom Var_dec : forall x y : Var, {x = y} + {x <> y}.
Parameter Event : Set.
Axiom Event_dec : forall e e' : Event, {e = e'} + {e <> e'}.

Definition Object := Var + Event.


(** Values *)

Parameter Val : Set.
Axiom Val_dec : forall x y : Val, {x = y} + {x <> y}.


(** Configurations *)

Parameter Conf : Set.
Axiom Conf_dec : forall c c' : Conf, {c = c'} + {c <> c'}.


(** Environments *)

Definition Memory := Var -> Val.
Definition eq_Memory := eq_ext Var Val.

Definition update (m : Memory) (x : Var) (v : Val) : Memory :=
  fun y : Var => match Var_dec x y with
    | left _ => v
    | right _ => m y
  end.


(** Transfert functions *)

Definition Phi := (Conf * Memory) -> (Conf * (Subset Event) * Memory) -> Prop.
Axiom Phi_dec : forall phi : Phi, forall (a : Conf * Memory)
                                         (a' : Conf * (Subset Event) * Memory),
      	          phi a a' \/ ~ phi a a'.

Definition eq_Phi (phi phi' : Phi) := forall a a', (phi a a' <-> phi' a a').


(** Processes *)

Record Process : Type := mkProcess
  { R : Subset Object ;
    W : Subset Object ;
    C : Subset Conf   ;
    phi : Phi }.


(** Systems *)

Record System : Type := mkSystem
  { L : Subset Object ;
    P : Subset Process }.

(** Variables and Events read by a System *)
Definition Sys_Read (S : System) (o : Object) : Prop :=
  exists p, S.(P) p /\ p.(R) o.

(** Variables and Events written by a System *)
Definition Sys_Write (S : System) (o : Object) : Prop :=
  exists p, S.(P) p /\ p.(W) o.

(** Events of a System *)
Definition Sys_Events (S : System) (e : Event) : Prop :=
  Sys_Read S (inr Var e) \/ Sys_Write S (inr Var e).

(** Variables of a System *)
Definition Sys_Vars (S : System) (x : Var) : Prop :=
  Sys_Read S (inl Event x) \/ Sys_Write S (inl Event x).

(** Variables and Events of a System *)
Definition Sys_Objects (S : System) : Object -> Prop :=
  Union Object (Sys_Read S) (Sys_Write S).


(** * Encapsulation and Assembly *)

Definition Encapsulation (S : System) (X : Subset Object) : System :=
  mkSystem X S.(P).

Definition Assembly (S1 S2 : System) : System :=
  mkSystem (Union Object S1.(L) S2.(L)) (Union Process S1.(P) S2.(P)).




(** * Semantics *)


Record SysConf : Type := mkSysConf
  { Cs : Process -> Conf ;
    E  : Subset Event }.

Record State : Type := mkState
  { r : SysConf ;
    m : Memory }.

Definition Trace := nat -> State.

Parameter Sched : SysConf -> SysConf -> Prop. (* Scheduler *)

Inductive Transition (S : System) (st st' : State) : Prop :=
| Univers_Trans :
    (* same configurations for local processes,
       same notified local events,
       same values for local variables *)
    (forall p, S.(P) p -> (st.(r).(Cs) p) = (st'.(r).(Cs) p)) ->
    (forall e, S.(L) (inr Var e)   -> (st.(r).(E) e <-> st'.(r).(E) e)) ->
    (forall x, S.(L) (inl Event x) -> (st.(m) x = st'.(m) x)) ->
      Transition S st st'
| Local_Trans :
    (* a local process is executed *)
    forall p E_p,
      S.(P) p ->
      p.(phi) (st.(r).(Cs) p, st.(m)) (st'.(r).(Cs) p, E_p, st'.(m)) ->
      (forall p', p' <> p -> st.(r).(Cs) p' = st'.(r).(Cs) p') ->
      eq_Subset Event st'.(r).(E) (Union Event st.(r).(E) E_p) ->
        Transition S st st'
| Sched_Trans :
    (* the Scheduler is executed ; memory stays the same *)
    Sched st.(r) st'.(r) -> eq_Memory st.(m) st'.(m) ->
      Transition S st st'.

Definition Sem (S : System) (t : Trace) : Prop :=
  forall i, Transition S (t i) (t (i+1)%nat).


(** ** Read and Written Variables and Events *)

(** Semantically Read Variables by a Process *)
Definition Proc_Sem_Read_Var (p : Process) (x : Var) : Prop :=
  exists c : Conf, exists m : Memory,
  exists c' : Conf, exists E' : Subset Event, exists m' : Memory,
  exists v : Val,
    p.(C) c /\ p.(C) c' /\ p.(phi) (c, m) (c', E', m') /\
    ~ (p.(phi) (c, update m x v) (c', E', m')).

(** Semantically Read Events by a Process *)
Definition Proc_Sem_Read_Event (p : Process) (e : Event) : Prop :=
  exists C1  : Process -> Conf, exists E1  : Subset Event,
  exists C2 : Process -> Conf, exists E2 : Subset Event,
    p.(C) (C1 p) /\ p.(C) (C2 p) /\
    Sched (mkSysConf C1 (fun e' => ((e' = e) \/ E1 e')))
          (mkSysConf C2 E2) /\
    forall (C3 C4 : Process -> Conf) (E4 : Subset Event),
      C3 p = C1 p -> Sched (mkSysConf C3 E1) (mkSysConf C4 E4) ->
        C4 p <> C2 p.

(** Semantically Written Variables by a Process *)
Definition Proc_Sem_Write_Var (p : Process) (x : Var) : Prop :=
  exists c : Conf, exists m : Memory,
  exists c' : Conf, exists E' : Subset Event, exists m' : Memory,
    p.(C) c /\ p.(C) c' /\ p.(phi) (c, m) (c', E', m') /\ m x <> m' x.

(** Semantically Written Events by a Process *)
Definition Proc_Sem_Write_Event (p : Process) (e : Event) : Prop :=
  exists c : Conf, exists m : Memory,
  exists c' : Conf, exists E' : Subset Event, exists m' : Memory,
    p.(C) c /\ p.(C) c' /\ p.(phi) (c, m) (c', E', m') /\ E' e.

(** Semantically Read Variables and Events by a Process *)
Definition Proc_Sem_Read (p : Process) (o : Object) : Prop :=
  match o with
| inl x => Proc_Sem_Read_Var p x
| inr e => Proc_Sem_Read_Event p e
end.

(** Semantically Written Variables and Events by a Process *)
Definition Proc_Sem_Write (p : Process) (o : Object) : Prop :=
  match o with
| inl x => Proc_Sem_Write_Var p x
| inr e => Proc_Sem_Write_Event p e
end.

(** Semantically Read Variables and Events by a System *)
Definition Sys_Sem_Read (S : System) (o : Object) : Prop :=
  exists p, S.(P) p /\ Proc_Sem_Read p o.

(** Semantically Written Variables and Events by a System *)
Definition Sys_Sem_Write (S : System) (o : Object) : Prop :=
  exists p, S.(P) p /\ Proc_Sem_Write p o.


(** ** Well-formed Processes *)

Definition Is_Process (p : Process) : Prop :=
  (Contained Object (Proc_Sem_Read p) p.(R)) /\
  (Contained Object (Proc_Sem_Write p) p.(W)) /\
  (forall (c c' : Conf) (m m' : Memory) (E : Subset Event),
    p.(phi) (c, m) (c', E, m') -> p.(C) c /\ p.(C) c').

(** ** Well-formed Systems *)

Definition Is_System (S : System) : Prop :=
  forall p, S.(P) p -> Is_Process p.


(** ** Assembly condition *)

Definition Assemblable (S S' : System) : Prop :=
  eq_Subset Object (Intersect Object S.(L) (Sys_Write S')) (Emptyset Object) /\
  eq_Subset Object (Intersect Object S'.(L) (Sys_Write S)) (Emptyset Object) /\
  eq_Subset Process (Intersect Process S.(P) S'.(P)) (Emptyset Process).




(** * Encapsulation Theorem *)

Theorem Encapsulation_Sem :
  forall (S : System) (X Y : Subset Object), Is_System S ->
    Contained Trace (Sem (Encapsulation S (Union Object X Y)))
                    (Sem (Encapsulation S X)).

Proof.

unfold Sem, Intersect, Contained, Union, Encapsulation in |- *.
intros S X Y H_S t H_t i.
destruct (H_t i)
 as [H_P H_E H_X| p E_p H_S_p H_p_phi H_p' H_E| H_Sched H_Mem].
 apply Univers_Trans.
  intros p H_p; apply (H_P p); assumption.
 intros e H_e; apply H_E.
   simpl in |- *; left; assumption.
 intros x H_x; apply H_X.
   simpl in |- *; left; assumption.
apply (Local_Trans (mkSystem X (P S)) (t i) (t (i + 1)%nat) p E_p);
 assumption.
apply Sched_Trans; assumption.

Qed.



(** * Assembly Theorem *)

Theorem Assembly_Sem :
  forall (S S' : System), Is_System S -> Is_System S' -> Assemblable S S' ->
    eq_Subset Trace (Sem (Assembly S S')) (Intersect Trace (Sem S) (Sem S')).

Proof.

unfold eq_Subset, Sem, Intersect, Contained, Emptyset, Assembly, Union
 in |- *.
intros S S' H_S H_S' H_SS'.
set
 (SS' :=
  mkSystem (fun x0 : Object => L S x0 \/ L S' x0)
    (fun x0 : Process => P S x0 \/ P S' x0)) in |- *.
split; intro T.
 intro Trans_SS'; split; intro i;
  destruct (Trans_SS' i)
   as [H_Confs H_Event H_Var| p E_p H_p H_phi H_p' H_E_p| H_Sched H_Mem].
  apply Univers_Trans.
   intros p H_p; apply H_Confs; left; assumption.
  intros e H_e; apply H_Event; left; assumption.
  intros x H_x; apply H_Var; left; assumption.
 destruct H_p as [H_p| H_p].
  apply (Local_Trans S (T i) (T (i + 1)%nat) p E_p); assumption.
 apply Univers_Trans.
  intros p' H_S_p'; apply H_p'; destruct H_SS' as (H1, H2);
   destruct H2 as (H2, H_P).
    unfold eq_Subset in H_P; unfold Contained in H_P;
     destruct H_P as (H_P1, H_P2); unfold Intersect in H_P1.
    intro Hpp'.
    apply (H_P1 p).
    split; [ rewrite <- Hpp' in |- * | idtac ]; assumption.
 unfold eq_Subset, Union, Contained in H_E_p;
  destruct H_E_p as (H_E_p1, H_E_p2).
   intros e H_e; split; intro H_T.
  apply H_E_p2; left; assumption.
 destruct (H_E_p1 e H_T).
  assumption.
 unfold Assemblable, eq_Subset, Intersect, Sys_Write, Contained in H_SS'.
   destruct H_SS' as (H_S_L, Temp); destruct Temp as (H_S'_L, H_Processes).
   destruct (H_S' p H_p) as (H_p_R, Temp); destruct Temp as (H_p_W, H_p_C).
   unfold Contained in H_p_W.
   assert (Proc_Sem_Write p (inr Var e)).
  exists (Cs (r (T i)) p); exists (m (T i));
   exists (Cs (r (T (i + 1)%nat)) p); exists E_p; exists (m (T (i + 1)%nat)).
    split.
   destruct
    (H_p_C (Cs (r (T i)) p) (Cs (r (T (i + 1)%nat)) p) 
       (m (T i)) (m (T (i + 1)%nat)) E_p); assumption.
  split.
   destruct
    (H_p_C (Cs (r (T i)) p) (Cs (r (T (i + 1)%nat)) p) 
       (m (T i)) (m (T (i + 1)%nat)) E_p); assumption.
  split.
   assumption.
  assumption.
 destruct H_S_L as (H_S_L1, H_S_L2); elim (H_S_L1 (inr Var e)).
   split.
  assumption.
 exists p; split.
  assumption.
 exact (H_p_W (inr Var e) H0).
 intros x H_x.
   unfold Assemblable, eq_Subset, Intersect, Sys_Write, Contained in H_SS'.
   destruct H_SS' as (H_S_L, Temp); destruct Temp as (H_S'_L, H_Processes).
   destruct (H_S' p H_p) as (H_p_R, Temp); destruct Temp as (H_p_W, H_p_C).
   unfold Contained in H_p_W.
   assert (~ W p (inl Event x)).
  intro H_p_W_x.
    destruct H_S_L as (H_S_L1, H_S_L2); elim (H_S_L1 (inl Event x)).
    split.
   assumption.
  exists p; split; assumption.
 assert (~ Proc_Sem_Write_Var p x).
  intro H'; elim H.
    apply (H_p_W (inl Event x)); assumption.
 destruct (Val_dec (m (T i) x) (m (T (i + 1)%nat) x)).
  assumption.
 elim H0; exists (Cs (r (T i)) p); exists (m (T i));
  exists (Cs (r (T (i + 1)%nat)) p); exists E_p; exists (m (T (i + 1)%nat)).
   split.
  destruct
   (H_p_C (Cs (r (T i)) p) (Cs (r (T (i + 1)%nat)) p) 
      (m (T i)) (m (T (i + 1)%nat)) E_p); assumption.
 split.
  destruct
   (H_p_C (Cs (r (T i)) p) (Cs (r (T (i + 1)%nat)) p) 
      (m (T i)) (m (T (i + 1)%nat)) E_p); assumption.
 split; assumption.
 apply Sched_Trans; assumption.
 apply Univers_Trans.
  intros p H_p; apply H_Confs; right; assumption.
 intros e H_e; apply H_Event; right; assumption.
 intros x H_x; apply H_Var; right; assumption.
 destruct H_p as [H_p| H_p].
  apply Univers_Trans.
   intros p' H_S'_p'; apply H_p'; destruct H_SS' as (H1, H2);
    destruct H2 as (H2, H_P).
     unfold eq_Subset in H_P; unfold Contained in H_P;
      destruct H_P as (H_P1, H_P2); unfold Intersect in H_P1.
     intro Hpp'.
     apply (H_P1 p).
     split; [ idtac | rewrite <- Hpp' in |- * ]; assumption.
  unfold eq_Subset, Union, Contained in H_E_p;
   destruct H_E_p as (H_E_p1, H_E_p2).
    intros e H_e; split; intro H_T.
   apply H_E_p2; left; assumption.
  destruct (H_E_p1 e H_T).
   assumption.
  unfold Assemblable, eq_Subset, Intersect, Sys_Write, Contained in H_SS'.
    destruct H_SS' as (H_S_L, Temp); destruct Temp as (H_S'_L, H_Processes).
    destruct (H_S p H_p) as (H_p_R, Temp); destruct Temp as (H_p_W, H_p_C).
    unfold Contained in H_p_W.
    assert (Proc_Sem_Write p (inr Var e)).
   exists (Cs (r (T i)) p); exists (m (T i));
    exists (Cs (r (T (i + 1)%nat)) p); exists E_p; 
    exists (m (T (i + 1)%nat)).
     split.
    destruct
     (H_p_C (Cs (r (T i)) p) (Cs (r (T (i + 1)%nat)) p) 
        (m (T i)) (m (T (i + 1)%nat)) E_p); assumption.
   split.
    destruct
     (H_p_C (Cs (r (T i)) p) (Cs (r (T (i + 1)%nat)) p) 
        (m (T i)) (m (T (i + 1)%nat)) E_p); assumption.
   split.
    assumption.
   assumption.
  destruct H_S'_L as (H_S'_L1, H_S'_L2); elim (H_S'_L1 (inr Var e)).
    split.
   assumption.
  exists p; split.
   assumption.
  exact (H_p_W (inr Var e) H0).
  intros x H_x.
    unfold Assemblable, eq_Subset, Intersect, Sys_Write, Contained in H_SS'.
    destruct H_SS' as (H_S_L, Temp); destruct Temp as (H_S'_L, H_Processes).
    destruct (H_S p H_p) as (H_p_R, Temp); destruct Temp as (H_p_W, H_p_C).
    unfold Contained in H_p_W.
    assert (~ W p (inl Event x)).
   intro H_p_W_x.
     destruct H_S'_L as (H_S'_L1, H_S'_L2); elim (H_S'_L1 (inl Event x)).
     split.
    assumption.
   exists p; split; assumption.
  assert (~ Proc_Sem_Write_Var p x).
   intro H'; elim H.
     apply (H_p_W (inl Event x)); assumption.
  destruct (Val_dec (m (T i) x) (m (T (i + 1)%nat) x)).
   assumption.
  elim H0; exists (Cs (r (T i)) p); exists (m (T i));
   exists (Cs (r (T (i + 1)%nat)) p); exists E_p; exists (m (T (i + 1)%nat)).
    split.
   destruct
    (H_p_C (Cs (r (T i)) p) (Cs (r (T (i + 1)%nat)) p) 
       (m (T i)) (m (T (i + 1)%nat)) E_p); assumption.
  split.
   destruct
    (H_p_C (Cs (r (T i)) p) (Cs (r (T (i + 1)%nat)) p) 
       (m (T i)) (m (T (i + 1)%nat)) E_p); assumption.
  split; assumption.
 apply (Local_Trans S' (T i) (T (i + 1)%nat) p E_p); assumption.
 apply Sched_Trans; assumption.
intros H i; destruct H as (Trans_S, Trans_S').
  destruct (Trans_S i)
   as [H_S_P H_S_E H_S_X| p E_p H_p H_phi H_p' H_E| H_Sched H_Mem].
 destruct (Trans_S' i)
  as [H_S'_P H_S'_E H_S'_X| p E_p H_p H_phi H_p' H_E| H_Sched H_Mem].
  apply Univers_Trans.
   intros p H_p; destruct H_p as [H_p| H_p].
    exact (H_S_P p H_p).
   exact (H_S'_P p H_p).
  intros e H_e; destruct H_e as [H_e| H_e].
   exact (H_S_E e H_e).
  exact (H_S'_E e H_e).
  intros x H_x; destruct H_x as [H_x| H_x].
   exact (H_S_X x H_x).
  exact (H_S'_X x H_x).
 apply (Local_Trans SS' (T i) (T (i + 1)%nat) p E_p); try right; assumption.
 apply Sched_Trans; assumption.
apply (Local_Trans SS' (T i) (T (i + 1)%nat) p E_p); try left; assumption.
apply Sched_Trans; assumption.

Qed.



(*
(************)
(* Observer *)
(************)


Definition InterfaceState (I : Subset Object) (st : State) (st' : State) :
  Prop :=
  (forall x, I (inl Event x) -> st.(m) x = st'.(m) x) /\
  (forall e, I (inr Var e) -> (st.(r).(E) e <-> st'.(r).(E) e)).

Definition InterfaceTrace (I : Subset Object) (t : Trace) (t' : Trace) :
  Prop :=
  forall i, InterfaceState I (t i) (t' i).

Definition InterfaceTraces (I : Subset Object) (T : Subset Trace) (t : Trace) :
  Prop :=
  exists t', T t' /\ InterfaceTrace I t' t.

Definition InterfaceSystem (I : Subset Object) (S : System) (t : Trace) :
  Prop :=
  InterfaceTraces I (Sem S) t.

(* S observes S' *)
Definition Observe (S S' : System) : Prop := 
  eq_Subset Object (Intersect Object (Sys_Write S) (Sys_Objects S'))
                   (Emptyset Object).


Lemma eq_nat_dec : forall n n' : nat, {n = n'} + {n <> n'}.
Proof.

intro n; induction n; intro n'; destruct n'.
 left; reflexivity.
right; intro H;  discriminate H.
right; intro H;  discriminate H.
destruct (IHn n') as [H_n'| H_n'];
 [ left; rewrite H_n' in |- *; reflexivity
 | right; intro H_S; apply H_n'; inversion H_S;  subst; reflexivity ].
Qed.


Lemma Observe_Sem :
  forall S S_O, Is_System S -> Is_System S_O ->
  Assemblable S S_O -> Observe S_O S ->
    eq_Subset _ (InterfaceSystem (Sys_Objects S) S)
                (InterfaceSystem (Sys_Objects S) (Assembly S S_O)).
Proof.

unfold Observe, InterfaceSystem, InterfaceTraces, InterfaceTrace,
 InterfaceState, eq_Subset, Contained in |- *.
intros S S_O H_S H_S_O H_S_S_O H_O.
split.
 intros t H_t'; destruct H_t' as (t', H_t'); destruct H_t' as (H_t', Hi_t').

exists
  (fun i => match i with
   | 0 => t' 0
   | S i' => (match H_t' i' with
	      | _ => t' 0
      	      end)
   end).

Focus 2.

intros t H_t'; destruct H_t' as (t', H_t'); destruct H_t' as (H_t', Hi_t').
  exists t'.
  split.
 destruct (Assembly_Sem S S_O H_S H_S_O H_S_S_O) as (H1, H2).
   unfold Contained, Intersect in H1.
   destruct (H1 t' H_t'); assumption.
intro i; split;
 [ intros x H_x | intros e H_e; split; [ intro H_e_t' | intro H_e_t ] ];
 destruct (Hi_t' i) as (H, H').
 exact (H x H_x).
destruct (H' e H_e) as (H1, H2); exact (H1 H_e_t').
destruct (H' e H_e) as (H1, H2); exact (H2 H_e_t).

Show.
Qed.
*)