Library clock_expr

Set Implicit Arguments.

Require Import Bool.
Require Import ZArith.
Require Import QArith.
Require Import Omega.
Require Import misc.
Require Import ibw_def.
Require Import ibw_aux.
Require Import ibw_prop.
Require Import abstraction_phd_def.
Require Import abstraction_phd_aux.
Require Import abstraction_phd_prop.

Inductive clock_expr : Set :=
| Clk_ibw : ibw -> clock_expr
| Clk_not : ibw -> clock_expr
| Clk_on : clock_expr -> clock_expr -> clock_expr
.

Fixpoint ibw_of_clock_expr (c: clock_expr) { struct c } :=
  match c with
  | Clk_ibw w => w
  | Clk_not w => not w
  | Clk_on ce1 ce2 => on (ibw_of_clock_expr ce1) (ibw_of_clock_expr ce2)
  end.

Inductive abs_expr : Set :=
| Abs_ibw : abstraction_phd -> abs_expr
| Abs_not : abstraction_phd -> abs_expr
| Abs_on : abs_expr -> abs_expr -> abs_expr
.

Fixpoint abs_expr_of_clock_expr (abs_of_ibw: ibw -> abstraction_phd) (ce: clock_expr) { struct ce } :=
  match ce with
  | Clk_ibw w => Abs_ibw (abs_of_ibw w)
  | Clk_not w => Abs_not (abs_of_ibw w)
  | Clk_on ce1 ce2 => Abs_on (abs_expr_of_clock_expr abs_of_ibw ce1) (abs_expr_of_clock_expr abs_of_ibw ce2)
  end.

Fixpoint abstraction_phd_of_abs_expr (ce: abs_expr) { struct ce } :=
  match ce with
  | Abs_ibw a => a
  | Abs_not a => not_abs (abs_std a)
  | Abs_on ace1 ace2 =>
    on_abs (abs_std (abstraction_phd_of_abs_expr ace1)) (abs_std (abstraction_phd_of_abs_expr ace2))
  end.

Lemma abstraction_phd_of_abs_expr_well_formed_abstraction_phd_compat:
  forall ce: clock_expr,
  forall abs_of_ibw: ibw -> abstraction_phd,
  forall H_abs:
    (forall w: ibw, well_formed_abstraction_phd (abs_of_ibw w)),
  well_formed_abstraction_phd (abstraction_phd_of_abs_expr (abs_expr_of_clock_expr abs_of_ibw ce)).
Proof.
  induction ce.
    simpl; auto.

    simpl.
    intros abs_of_ibw H_wf.
    apply not_abs_well_formed_abstraction_phd_compat.
    assert (H_eq: abs_equal (abs_of_ibw i) (abs_std (abs_of_ibw i))).
      apply abs_equal_abs_std_non_empty.
    apply (well_formed_abstraction_phd_abs_equal_compat H_eq).
    apply H_wf.

    simpl.
    intros.
    apply on_abs_well_formed_abstraction_phd_compat; auto.
      assert (H_eq: abs_equal (abstraction_phd_of_abs_expr (abs_expr_of_clock_expr abs_of_ibw ce1)) (abs_std (abstraction_phd_of_abs_expr (abs_expr_of_clock_expr abs_of_ibw ce1)))).
        apply abs_equal_abs_std_non_empty.
      apply (well_formed_abstraction_phd_abs_equal_compat H_eq).
      apply IHce1.
      apply H_abs.
      assert (H_eq: abs_equal (abstraction_phd_of_abs_expr (abs_expr_of_clock_expr abs_of_ibw ce2)) (abs_std (abstraction_phd_of_abs_expr (abs_expr_of_clock_expr abs_of_ibw ce2)))).
        apply abs_equal_abs_std_non_empty.
      apply (well_formed_abstraction_phd_abs_equal_compat H_eq).
      apply IHce2.
      apply H_abs.
Qed.

Property abstraction_phd_of_abs_expr_correctness:
  forall ce: clock_expr,
  forall abs_of_ibw: ibw -> abstraction_phd,
  forall H_abs:
    (forall w: ibw, well_formed_abstraction_phd (abs_of_ibw w) /\ in_abstraction_phd w (abs_of_ibw w)),
  in_abstraction_phd (ibw_of_clock_expr ce) (abstraction_phd_of_abs_expr (abs_expr_of_clock_expr abs_of_ibw ce)).
Proof.
  intros ce abs_of_ibw H_abs.
  induction ce.
    simpl.
    destruct (H_abs i) as [H_wf H_in_abs].
    assumption.

    simpl.
    destruct (H_abs i) as [H_wf H_in_abs].
    assert (H_wf_not: well_formed_abstraction_phd (not_abs (abs_of_ibw i))).
      apply not_abs_well_formed_abstraction_phd_compat.
      assumption.
    apply (abs_equal_correctness H_wf_not); auto.
      apply not_abs_well_formed_abstraction_phd_compat.
      assert (H_eq: abs_equal (abs_of_ibw i) (abs_std (abs_of_ibw i))).
        apply abs_equal_abs_std_non_empty.
      apply (well_formed_abstraction_phd_abs_equal_compat H_eq).
      assumption.

      apply not_abs_correctness_aux; auto.

      apply not_abs_eq_compat.
      apply abs_equal_abs_std_non_empty.

    simpl.
    assert (H_wf_ce1:
      well_formed_abstraction_phd
        (abstraction_phd_of_abs_expr (abs_expr_of_clock_expr abs_of_ibw ce1))).
        apply abstraction_phd_of_abs_expr_well_formed_abstraction_phd_compat;
        intro w;
        destruct (H_abs w) as [H_wf H_in_abs];
        assumption.
    assert (H_wf_ce2:
      well_formed_abstraction_phd
        (abstraction_phd_of_abs_expr (abs_expr_of_clock_expr abs_of_ibw ce2))).
        apply abstraction_phd_of_abs_expr_well_formed_abstraction_phd_compat;
        intro w;
        destruct (H_abs w) as [H_wf H_in_abs];
        assumption.
    assert (H_wf_std_ce1: well_formed_abstraction_phd
      (abs_std (abstraction_phd_of_abs_expr (abs_expr_of_clock_expr abs_of_ibw ce1)))).
      assert (H_eq: abs_equal (abstraction_phd_of_abs_expr (abs_expr_of_clock_expr abs_of_ibw ce1)) (abs_std (abstraction_phd_of_abs_expr (abs_expr_of_clock_expr abs_of_ibw ce1)))).
        apply abs_equal_abs_std_non_empty.
      apply (well_formed_abstraction_phd_abs_equal_compat H_eq).
      assumption.
    assert (H_wf_std_ce2: well_formed_abstraction_phd
      (abs_std (abstraction_phd_of_abs_expr (abs_expr_of_clock_expr abs_of_ibw ce2)))).
      assert (H_eq: abs_equal (abstraction_phd_of_abs_expr (abs_expr_of_clock_expr abs_of_ibw ce2)) (abs_std (abstraction_phd_of_abs_expr (abs_expr_of_clock_expr abs_of_ibw ce2)))).
        apply abs_equal_abs_std_non_empty.
      apply (well_formed_abstraction_phd_abs_equal_compat H_eq).
      assumption.
    apply on_abs_correctness_aux; auto.
      apply (abs_equal_correctness H_wf_ce1); auto.
      apply abs_equal_abs_std_non_empty.

      apply (abs_equal_correctness H_wf_ce2); auto.
      apply abs_equal_abs_std_non_empty.
Qed.

Definition prec_clock (ce1: clock_expr) (ce2: clock_expr) :=
  prec (ibw_of_clock_expr ce1) (ibw_of_clock_expr ce2).

Definition prec_abs_clock (ce1: abs_expr) (ce2: abs_expr) :=
  prec_abs (abstraction_phd_of_abs_expr ce1) (abstraction_phd_of_abs_expr ce2).

Property prec_abs_clock_correctness:
  forall ce1 ce2: clock_expr,
  forall abs_of_ibw: ibw -> abstraction_phd,
  forall H_abs:
    (forall w: ibw, well_formed_abstraction_phd (abs_of_ibw w) /\ in_abstraction_phd w (abs_of_ibw w)),
  prec_abs_clock (abs_expr_of_clock_expr abs_of_ibw ce1) (abs_expr_of_clock_expr abs_of_ibw ce2) ->
  prec_clock ce1 ce2.
Proof.
  intros ce1 ce2 abs H_abs H_prec_abs.
  unfold prec_clock.
  unfold prec_abs_clock in H_prec_abs.
  unfold prec_abs in H_prec_abs.
  apply H_prec_abs;
    apply abstraction_phd_of_abs_expr_correctness; auto.
Qed.

Definition sync_clock (ce1: clock_expr) (ce2: clock_expr) :=
  sync (ibw_of_clock_expr ce1) (ibw_of_clock_expr ce2).

Definition sync_abs_clock (ce1: abs_expr) (ce2: abs_expr) :=
  sync_abs (abstraction_phd_of_abs_expr ce1) (abstraction_phd_of_abs_expr ce2).

Property sync_abs_clock_correctness:
  forall ce1 ce2: clock_expr,
  forall abs_of_ibw: ibw -> abstraction_phd,
  forall H_abs:
    (forall w: ibw, well_formed_abstraction_phd (abs_of_ibw w) /\ in_abstraction_phd w (abs_of_ibw w)),
  sync_abs_clock (abs_expr_of_clock_expr abs_of_ibw ce1) (abs_expr_of_clock_expr abs_of_ibw ce2) ->
  sync_clock ce1 ce2.
Proof.
  intros ce1 ce2 abs H_abs H_sync_abs.
  unfold sync_clock.
  unfold sync_abs_clock in H_sync_abs.
  unfold sync_abs in H_sync_abs.
  apply H_sync_abs;
    apply abstraction_phd_of_abs_expr_correctness; auto.
Qed.

Definition adaptability_clock (ce1: clock_expr) (ce2: clock_expr) :=
  adaptability (ibw_of_clock_expr ce1) (ibw_of_clock_expr ce2).

Definition adaptability_abs_clock (ce1: abs_expr) (ce2: abs_expr) :=
  adaptability_abs (abstraction_phd_of_abs_expr ce1) (abstraction_phd_of_abs_expr ce2).

Property adaptability_abs_clock_correctness:
  forall ce1 ce2: clock_expr,
  forall abs_of_ibw: ibw -> abstraction_phd,
  forall H_abs:
    (forall w: ibw, well_formed_abstraction_phd (abs_of_ibw w) /\ in_abstraction_phd w (abs_of_ibw w)),
  adaptability_abs_clock (abs_expr_of_clock_expr abs_of_ibw ce1) (abs_expr_of_clock_expr abs_of_ibw ce2) ->
  adaptability_clock ce1 ce2.
Proof.
  intros ce1 ce2 abs H_abs H_adaptability_abs.
  unfold adaptability_clock.
  unfold adaptability_abs_clock in H_adaptability_abs.
  unfold adaptability_abs in H_adaptability_abs.
  apply H_adaptability_abs;
    apply abstraction_phd_of_abs_expr_correctness; auto.
Qed.