-
Notifications
You must be signed in to change notification settings - Fork 10
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Terminated lists + small changes to utp_timed_rea_designs.thy and utp_cml.thy #6
base: master
Are you sure you want to change the base?
Conversation
… type is a trace algebra. Minor contributions in utp_timed_rea_designs.thy.
Merge remote-tracking branch 'origin/master' into pedro
I think I may need to revisit how the proofs about monoids and the core definition of the type is distributed amongst the files. Should the monoid lemmas be moved into Monoid_extra.thy instead? UPDATE: I think it is fine, I just need to make sure "Monoid_Extra" is "Monoid_extra", and include "Library_extra/Terminated_lists.thy" in utp_imports. I'll commit the changes and update this pull request. |
Added Terminated_lists.thy to utp_imports.
UTP-Imports builds fine now. |
Initial version of datatype for Circus Time theory.
Putting this pull request on hold before merging back from master or core into my branch with the latest changes. |
Adjusted Terminated_lists.thy to track adjusted names in Monoid_extra.thy.
…f type classes pre_trace, trace and the removed left_cancel_monoid law.
I've successfully reproved the instantiations of terminated lists based on the refined type classes of pre_trace and trace. Now I'm on the way to updating utp_circus_time.thy to use the new type I've envisioned. When this is done I'll be asking for a review again :-) |
Terminated Lists
Here is my initial commit of the little auxiliary theory of terminated lists. For now I'm not including the Coinductive AFP theory where (infinite) Terminated Lists are defined. If it becomes necessary I think we can include it in the future? There's also a brief mention of terminated lists in the Isabelle document about datatypes.
I call generalised terminated lists (type:
('a,'b) gtlist
) those whose Nil type'a
is arbitrary (like in the Coinductive theory), while those where the Nil type is the same as that of the elements I call them 'standard terminated lists''b stlist
. By making this restriction it is easy to define plus, ord, diff, etc via type classes. Ideally it could also be shown that given agtlist
together with a function that maps from'a => 'b
we could also define a plus operator and get the same results.For a
'b stlist
given that the parametrised type is of sortordered_cancel_monoid_diff
we also get a type that satisfies the laws inordered_cancel_monoid_diff
. I observe that the difference operator when applied to pairs of (trace,refusal) will yield the diff function of Circus Time Actions nicely.Let me know what you think. I'm going to use this as a basis to encode the Circus Time theory.
Timed Reactive Designs
I updated
is-idle
like we discussed last week. I changed the definition ofWait d
as discussed and proved thatWait 0 = Skip
. There are more results I plan to add here.CML
I proved a few lemmas about the functions refusals and events. Nothing major here, I was just playing around with the CML trace model to understand it better.