machine[S, I, O: TYPE+]: THEORY BEGIN % machine is the type of deterministic state machines % with state space S, input I, output O machine: TYPE = [# delta : [S, I -> S], output: [S -> O] #] n: VAR nat s: VAR S m: VAR machine inp_seq: VAR sequence[I] % sequence[I] is [nat->I], so inp_seq is an infinite sequence of inputs % trace(m)(s,inp_seq) is the infinite sequence of states of machine m % with inital state s and input sequence inp_seq trace(m)(s, inp_seq)(n): RECURSIVE S = IF n = 0 THEN s ELSE delta(m)(trace(m)(s,inp_seq)(n-1), inp_seq(n)) ENDIF MEASURE n % out(m,s, inp_seq) is the infinite sequence of outputs of machine m % with inital state s and input sequence inp_seq out(m)(s, inp_seq): sequence[O] = output(m) o trace(m)(s, inp_seq) END machine machine_equiv[S1, S2, I, O: TYPE+]: THEORY BEGIN IMPORTING machine rho: VAR [S1 -> S2] % (surjective?[S1, S2]) m1: VAR machine[S1, I, O] m2: VAR machine[S2, I, O] trace_refines(m1, rho, m2): bool = FORALL (s1:S1, inp:I): rho(delta(m1)(s1,inp)) = delta(m2)(rho(s1), inp) output_refines(m1, rho, m2): bool = FORALL (s1: S1): output(m1)(s1) = output(m2)(rho(s1)) % don't try to prove the lemmas below, but try to prove those in tripmeter.pvs trace_equiv: LEMMA trace_refines(m1, rho, m2) => (FORALL (n: nat, s1: S1, inp_seq: sequence[I]): map(rho)(trace(m1)(s1,inp_seq))(n) = trace(m2)(rho(s1),inp_seq)(n)) output_equiv: LEMMA trace_refines(m1, rho, m2) & output_refines(m1, rho, m2) => FORALL (n:nat, s1: S1, inp_seq: sequence[I]): map(output(m1))(trace(m1)(s1,inp_seq))(n) = map(output(m2))(trace(m2)(rho(s1),inp_seq))(n) output_equiv_again: LEMMA trace_refines(m1, rho, m2) & output_refines(m1, rho, m2) => FORALL (s1: S1, inp_seq: sequence[I]): map(output(m1))(trace(m1)(s1,inp_seq)) = map(output(m2))(trace(m2)(rho(s1),inp_seq)) % The lemmas above are much easier to prove if we re-define % trace as follows: % % trace(m)(s, inp_seq)(n): RECURSIVE S = % IF n = 0 THEN s % ELSE trace(m)(delta(m)(s, inp_seq(n)), inp_seq)(n - 1) ENDIF % MEASURE n END machine_equiv