This is a follow-up to the discussion from the Frama-C mailing list to bring standard inductive lists to Frama-C WP plugin.
Replaced an axiomatic definition of lists with the standard Why3 one:
- used standard Why3 list modules;
- replaced a declared list type with the standard one;
- provided definitions of all previously specified list functions except for
repeat_box; - replaced all axioms with lemmas except for those related to
repeat_box; - proved all new lemmas with Alt-Ergo and Isabelle/HOL;
- added Why3 session with Why3 realization files and associated Isabelle/HOL theories.
Facts nth_cons and nth_concat received a new premise for the index 0 <= k. All other facts have been kept intact.