| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/co_structures/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 2 kB |
|
Impressum csequence_constant.pvs Sprache: PVS |
|||||||||
|
%-----------------------------------------------------------------------------
% Constant sequences, both finite and infinite, defined as coalgebraic % datatypes. % % Author: Jerry James <loganjerry@gmail.com> % % This file and its accompanying proof file are distributed under the CC0 1.0 % Universal license: http://creativecommons.org/publicdomain/zero/1.0/. % % Version history: % 2007 Feb 14: PVS 4.0 version % 2011 May 6: PVS 5.0 version % 2013 Jan 14: PVS 6.0 version %----------------------------------------------------------------------------- csequence_constant[T: TYPE]: THEORY BEGIN IMPORTING csequence_singleton[T], csequence_codt_coreduce[T, T] t: VAR T p: VAR pred[T] n, m: VAR nat % The finite sequence consisting of n copies of a single element constant_cseq(t, n): RECURSIVE finite_csequence = IF n = 0 THEN empty_cseq ELSE add(t, constant_cseq(t, n - 1)) ENDIF MEASURE n constant_cseq_empty: THEOREM FORALL t, n: empty?(constant_cseq(t, n)) IFF n = 0 constant_cseq_1: THEOREM FORALL t: constant_cseq(t, 1) = singleton_cseq(t) constant_cseq_first: THEOREM FORALL t, n: n > 0 IMPLIES first(constant_cseq(t, n)) = t constant_cseq_rest: THEOREM FORALL t, n: n > 0 IMPLIES rest(constant_cseq(t, n)) = constant_cseq(t, n - 1) constant_cseq_length: THEOREM FORALL t, n: length(constant_cseq(t, n)) = n constant_cseq_index: THEOREM FORALL t, n, m: index?(constant_cseq(t, n))(m) IFF m < n constant_cseq_nth: THEOREM FORALL t, n, (m: below[n]): nth(constant_cseq(t, n), m) = t constant_cseq_add: THEOREM FORALL t, n: add(t, constant_cseq(t, n)) = constant_cseq(t, n + 1) constant_cseq_last: THEOREM FORALL t, n: n > 0 IMPLIES last(constant_cseq(t, n)) = t constant_cseq_some: THEOREM FORALL t, n, p: some(p)(constant_cseq(t, n)) IFF n > 0 AND p(t) constant_cseq_every: THEOREM FORALL t, n, p: every(p)(constant_cseq(t, n)) IFF n = 0 OR p(t) % The infinite sequence consisting of a single element constant_cseq_struct(t): csequence_struct[T, T] = inj_add(t, t) constant_cseq(t): infinite_csequence = coreduce(constant_cseq_struct)(t) constant_cseq_inf_first: THEOREM FORALL t: first(constant_cseq(t)) = t constant_cseq_inf_rest: THEOREM FORALL t: rest(constant_cseq(t)) = constant_cseq(t) constant_cseq_inf_nth: THEOREM FORALL t, n: nth(constant_cseq(t), n) = t constant_cseq_inf_add: THEOREM FORALL t, n: add(t, constant_cseq(t)) = constant_cseq(t) constant_cseq_inf_some: THEOREM FORALL t, p: some(p)(constant_cseq(t)) IFF p(t) constant_cseq_inf_every: THEOREM FORALL t, p: every(p)(constant_cseq(t)) IFF p(t) END csequence_constant ¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.0Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28