Library clock
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_jfla_def.
Require Import abstraction_jfla_aux.
Require Import abstraction_jfla_prop.
Inductive clock : Set :=
| Clk_ibw : ibw -> clock
| Clk_not : ibw -> clock
| Clk_on : clock -> clock -> clock
.
Fixpoint ibw_of_clock (c: clock) { struct c } :=
match c with
| Clk_ibw w => w
| Clk_not w => not w
| Clk_on c1 c2 => on (ibw_of_clock c1) (ibw_of_clock c2)
end.
Inductive clock_absj : Set :=
| Clk_absj_ibw : abstractionj -> clock_absj
| Clk_absj_not : abstractionj -> clock_absj
| Clk_absj_on : clock_absj -> clock_absj -> clock_absj
.
Fixpoint clock_absj_of_clock (abs: ibw -> abstractionj) (c: clock) { struct c } :=
match c with
| Clk_ibw w => Clk_absj_ibw (abs w)
| Clk_not w => Clk_absj_not (abs w)
| Clk_on c1 c2 => Clk_absj_on (clock_absj_of_clock abs c1) (clock_absj_of_clock abs c2)
end.
Fixpoint absj_of_clock_absj (c: clock_absj) { struct c } :=
match c with
| Clk_absj_ibw a => a
| Clk_absj_not a => not_absj (absj_std a)
| Clk_absj_on ac1 ac2 =>
on_absj_alt (absj_std (absj_of_clock_absj ac1)) (absj_std (absj_of_clock_absj ac2))
end.
Property absj_of_clock_absj_well_formed_abstractionj_compat:
forall c: clock,
forall abs: ibw -> abstractionj,
forall H_abs:
(forall w: ibw, well_formed_abstractionj (abs w)),
well_formed_abstractionj (absj_of_clock_absj (clock_absj_of_clock abs c)).
Proof.
induction c.
simpl; auto.
simpl.
intros abs H_wf.
apply not_absj_well_formed_abstractionj_compat.
apply pre_not_absj_std_well_formed_abstractionj_compat; auto.
simpl.
intros.
apply on_absj_alt_well_formed_abstractionj_compat; auto;
apply pre_not_absj_std_well_formed_abstractionj_compat; auto.
Qed.
Property absj_of_clock_absj_correctness:
forall c: clock,
forall abs: ibw -> abstractionj,
forall H_abs:
(forall w: ibw, well_formed_abstractionj (abs w) /\ in_abstractionj w (abs w)),
in_abstractionj (ibw_of_clock c) (absj_of_clock_absj (clock_absj_of_clock abs c)).
Proof.
intros c abs H_abs.
induction c.
simpl.
destruct (H_abs i) as [H_wf H_in_abs].
assumption.
simpl.
destruct (H_abs i) as [H_wf H_in_abs].
apply not_std_correctness; auto.
simpl.
assert (H_wf_c1:
well_formed_abstractionj
(absj_of_clock_absj (clock_absj_of_clock abs c1))).
apply absj_of_clock_absj_well_formed_abstractionj_compat;
intro w;
destruct (H_abs w) as [H_wf H_in_abs];
assumption.
assert (H_wf_c2:
well_formed_abstractionj
(absj_of_clock_absj (clock_absj_of_clock abs c2))).
apply absj_of_clock_absj_well_formed_abstractionj_compat;
intro w;
destruct (H_abs w) as [H_wf H_in_abs];
assumption.
assert (H_wf_same_c1:
well_formed_abstractionj
(absj_std (absj_of_clock_absj (clock_absj_of_clock abs c1)))).
apply pre_not_absj_std_well_formed_abstractionj_compat; auto;
assumption.
assert (H_wf_same_c2:
well_formed_abstractionj
(absj_std (absj_of_clock_absj (clock_absj_of_clock abs c2)))).
apply pre_not_absj_std_well_formed_abstractionj_compat; auto;
assumption.
apply on_absj_alt_correctness; auto;
try solve [ simpl; rewrite Pmult_comm; reflexivity ].
apply (absj_equal_correctness H_wf_c1 H_wf_same_c1);
auto;
apply absj_std_correctness.
apply (absj_equal_correctness H_wf_c2 H_wf_same_c2);
auto;
apply absj_std_correctness.
Qed.
Definition prec_clock (c1: clock) (c2: clock) :=
prec (ibw_of_clock c1) (ibw_of_clock c2).
Definition prec_absj_clock (c1: clock_absj) (c2: clock_absj) :=
prec_absj (absj_of_clock_absj c1) (absj_of_clock_absj c2).
Property prec_absj_clock_correctness:
forall c1 c2: clock,
forall abs: ibw -> abstractionj,
forall H_abs:
(forall w: ibw, well_formed_abstractionj (abs w) /\ in_abstractionj w (abs w)),
prec_absj_clock (clock_absj_of_clock abs c1) (clock_absj_of_clock abs c2) ->
prec_clock c1 c2.
Proof.
intros c1 c2 abs H_abs H_prec_absj.
unfold prec_clock.
unfold prec_absj_clock in H_prec_absj.
unfold prec_absj in H_prec_absj.
apply H_prec_absj;
apply absj_of_clock_absj_correctness; auto.
Qed.