CristalCaveGem » LustreC

/*@ axiomatic Stream {

  @ type stream<A> = Tick(A, stream<A>);

  @ logic A nth<A> (integer i, stream<A> s);

  @ axiom nth_0<A>: \forall A v; \forall stream<A> ss; nth(0, Tick(v, ss)) == v;

  @ axiom nth_S<A> : \forall integer i; i > 0 ==> \forall A v; \forall stream<A> ss; nth(i, Tick(v, ss)) == nth(i-1, ss);

  @ logic stream<A> lift0<A> (A c) = Tick (c, lift0 (c));

  @ logic stream<boolean> _arrow<A> = Tick (\true, lift0 (\false));

  @ logic stream<A> ite<A> (stream<boolean> s_if, stream<A> s_then, stream<A> s_else);

  @ axiom ite_def<A>: \forall boolean v_if; \forall stream<boolean> ss_if;

                      \forall A v_then; \forall stream<A> ss_then;

                      \forall A v_else; \forall stream<A> ss_else;

                      ite(Tick(v_if, ss_if), Tick(v_then, ss_then), Tick(v_else, ss_else)) ==

      Tick((v_if)?(v_then):(v_else), ite(ss_if, ss_then, ss_else));

  @ logic stream<A> pre<A> (stream<A> s);

  @ axiom pre_def<A>: \forall integer i; \forall stream<A> s;

                      i >= 0 ==> nth(1+i, pre (s)) == nth(i, s);

  @ logic stream<A> when<A> (stream<boolean> s_clock, stream<A> s_sample);

  @ axiom when_def<A>: \forall integer i; \forall stream<boolean> c; \forall stream<A> s;

                       i >= 0 ==> nth (i, c) == \true ==> nth (i, when (c, s)) == nth (i, s);

  //Boolean operators

  @ logic stream<boolean> bnot (stream<boolean> b);

  @ axiom bnot_def: \forall boolean b; \forall stream<boolean> s;

                    bnot (Tick (b, s)) == Tick (!b, bnot (s));

  @ logic stream<boolean> band (stream<boolean> b1, stream<boolean> b2);

  @ axiom band_def: \forall boolean b1; \forall stream<boolean> s1; \forall boolean b2; \forall stream<boolean> s2;

                    band (Tick (b1, s1), Tick (b2, s2)) == Tick (b1 && b2, band (s1, s2));

  @ logic stream<boolean> bor (stream<boolean> b1, stream<boolean> b2);

  @ axiom bor_def: \forall boolean b1; \forall stream<boolean> s1; \forall boolean b2; \forall stream<boolean> s2;

                    bor (Tick (b1, s1), Tick (b2, s2)) == Tick (b1 || b2, bor (s1, s2));

  //Relational operators

  @ logic stream<boolean> eq<A> (stream<A> s1, stream<A> s2);

  @ axiom eq_def<A>: \forall A v1; \forall stream<A> s1; \forall A v2; \forall stream<A> s2;

                    eq (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 == v2, eq (s1, s2));

  @ logic stream<boolean> inf (stream<real> s1, stream<real> s2);

  @ axiom inf_def<A>: \forall real v1; \forall stream<real> s1; \forall real v2; \forall stream<real> s2;

                    inf (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 < v2, inf (s1, s2));

  @ logic stream<boolean> infeq (stream<real> s1, stream<real> s2) = bor (eq (s1, s2), inf(s1, s2));

  //Real operators:

  @ logic stream<real> plus (stream<real> s1, stream<real> s2);

  @ axiom plus_def<A>: \forall real v1; \forall stream<real> s1; \forall real v2; \forall stream<real> s2;

                    plus (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 + v2, plus (s1, s2));

  @ logic stream<real> minus (stream<real> s1, stream<real> s2);

  @ axiom minus_def<A>: \forall real v1; \forall stream<real> s1; \forall real v2; \forall stream<real> s2;

                    minus (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 - v2, minus (s1, s2));

  @ logic stream<real> mult (stream<real> s1, stream<real> s2);

  @ axiom mult_def<A>: \forall real v1; \forall stream<real> s1; \forall real v2; \forall stream<real> s2;

                    mult (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 * v2, mult (s1, s2));

  @ logic stream<real> div (stream<real> s1, stream<real> s2);

  //Integer operators:

  @ logic stream<integer> iplus (stream<integer> s1, stream<integer> s2);

  @ axiom iplus_def<A>: \forall integer v1; \forall stream<integer> s1; \forall integer v2; \forall stream<integer> s2;

                    iplus (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 + v2, iplus (s1, s2));

  @ logic stream<integer> iminus (stream<integer> s1, stream<integer> s2);

  @ axiom iminus_def<A>: \forall integer v1; \forall stream<integer> s1; \forall integer v2; \forall stream<integer> s2;

                    iminus (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 - v2, iminus (s1, s2));

  @ logic stream<integer> imult (stream<integer> s1, stream<integer> s2);

  @ axiom imult_def<A>: \forall integer v1; \forall stream<integer> s1; \forall integer v2; \forall stream<integer> s2;

                    imult (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 * v2, imult (s1, s2));

  @ logic stream<integer> idiv (stream<integer> s1, stream<integer> s2);

  @ axiom idiv_def<A>: \forall integer v1; \forall stream<integer> s1; \forall integer v2; \forall stream<integer> s2;

                    idiv (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 / v2, idiv (s1, s2));

  @ logic stream<integer> imod (stream<integer> s1, stream<integer> s2);

  @ axiom imod_def<A>: \forall integer v1; \forall stream<integer> s1; \forall integer v2; \forall stream<integer> s2;

                    imod (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 % v2, imod (s1, s2));

@ lemma prout: \forall stream<boolean> s; bnot (bnot (s)) == s;

@ lemma eq_obs_int: \forall stream<integer> s1; \forall stream<integer> s2;

                     (\forall integer i; i >= 0 ==> nth (i, s1) == nth (i, s2)) <==> (s1 == s2);

}

*/

// logic stream<int> apply1_int (stream<int> arg, int func(int ));

// axiom apply1_int_def: \forall int v; \forall stream<int> ss; \forall int func(int);

//                        apply1_int (Tick (v, ss), func) == Tick (func(v), apply1_int (ss, func));

// lemma eq_obs<A>: \forall stream<A> s1; \forall stream<A> s2;

//                   (\forall integer i; i >= 0 ==> nth (i, s1) == nth (i, s2)) <==> (s1 == s2);