Maxime Lesourd authored 5 years ago and Björn Brandenburg committed 5 years ago

- Added unfolding lemmas to basic_facts/ideal
- Fixed proofs depending on the previous definition using unfolding lemmas

The changes follow the discussion in Paris.

This avoids the need to use @-notation when establishing platform
properties (e.g., in facts about ideal schedules).

Thanks to Maxime for the suggestion.

Rationale: reserve the behavior folder for trace-based semantics.

These lemmas really constitute an analysis of the basic consequences
arising from the chosen semantics and hence logically belong to the
"analysis" part of Prosa.

To allow reasoning about an entire class of types of schedules /
processor modules, it's useful to have named definitions for various
invariants that processor models ensure. Let's collect these centrally
where we introduce processor models and schedules.

simplify structure of behavior, move arrival_sequence and schedule to toplevel, move task and sequential to model