Library Copland.Term_system
Copland specific event systems.
Construct an event system from an annotated term, place, and
evidence.
Fixpoint ev_sys (t: AnnoTerm) p e: EvSys Ev :=
match t with
| aasp (i, j) x ⇒ leaf (i, j) (asp_event i x p e)
| aatt (i, j) q x ⇒
before (i, j)
(leaf (i, S i) (req i p q e))
(before (S i, j)
(ev_sys x q e)
(leaf (pred j, j) (rpy (pred j) p q (aeval x q e))))
| alseq r x y ⇒ before r (ev_sys x p e)
(ev_sys y p (aeval x p e))
| abseq (i, j) s x y ⇒
before (i, j)
(leaf (i, S i)
(split i p e (sp (fst s) e)
(sp (snd s) e)))
(before (S i, j)
(before (S i, (pred j))
(ev_sys x p (sp (fst s) e))
(ev_sys y p (sp (snd s) e)))
(leaf ((pred j), j)
(join (pred j) p
(aeval x p (sp (fst s) e))
(aeval y p (sp (snd s) e))
(ss (aeval x p (sp (fst s) e))
(aeval y p (sp (snd s) e))))))
| abpar (i, j) s x y ⇒
before (i, j)
(leaf (i, S i)
(split i p e (sp (fst s) e)
(sp (snd s) e)))
(before (S i, j)
(merge (S i, (pred j))
(ev_sys x p (sp (fst s) e))
(ev_sys y p (sp (snd s) e)))
(leaf ((pred j), j)
(join (pred j) p
(aeval x p (sp (fst s) e))
(aeval y p (sp (snd s) e))
(pp (aeval x p (sp (fst s) e))
(aeval y p (sp (snd s) e))))))
end.
Lemma evsys_range:
∀ t p e,
es_range (ev_sys t p e) = range t.
Lemma well_structured_evsys:
∀ t p e,
well_formed t →
well_structured ev (ev_sys t p e).
The events in the event system correspond to the events associated
with a term, a place, and some evidence.
Maximal events are unique.
Lemma supreme_unique:
∀ t p e,
well_formed t →
∃ ! v, supreme (ev_sys t p e) v.
Lemma evsys_max_unique:
∀ t p e,
well_formed t →
unique (supreme (ev_sys t p e)) (max (ev_sys t p e)).
Maximal event evidence output matches aeval.
Definition out_ev v :=
match v with
| copy _ _ e ⇒ e
| kmeas _ _ _ _ e ⇒ e
| umeas _ _ _ _ e ⇒ e
| sign _ _ _ e ⇒ e
| hash _ _ _ e ⇒ e
| req _ _ _ e ⇒ e
| rpy _ _ _ e ⇒ e
| split _ _ _ _ e ⇒ e
| join _ _ _ _ e ⇒ e
end.
Lemma max_eval:
∀ t p e,
well_formed t →
out_ev (max (ev_sys t p e)) = aeval t p e.
lseq is associative relative to the event semantics