%----------------------------------------------------------------------------- % Additional induction rules for sequences of countable length. % % 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_induction[T: TYPE]: THEORY BEGIN
IMPORTING csequence_nth[T]
t: VAR T
n, m: VAR nat
cseq: VAR csequence
fseq: VAR finite_csequence
iseq: VAR infinite_csequence
p: VAR pred[T]
sp: VAR pred[csequence]
% Shorthand to make the definitions below more comprehensible. % This predicate says that p holds at index n, if index n is valid.
p_if_exists(p, cseq, n): MACRO bool =
index?(cseq)(n) IMPLIES p(nth(cseq, n))
% Weak induction over the elements: general / finite sequence case
cseq_induction: THEOREM FORALL cseq, p:
p_if_exists(p, cseq, 0) AND
(FORALL n:
p_if_exists(p, cseq, n) IMPLIES p_if_exists(p, cseq, n + 1)) IMPLIES every(p)(cseq)
% Weak induction over the elements: infinite sequence case
cseq_infinite_induction: THEOREM FORALL iseq, p:
p(nth(iseq, 0)) AND
(FORALL n: p(nth(iseq, n)) IMPLIES p(nth(iseq, n + 1))) IMPLIES every(p)(iseq)
% Strong induction over the elements: general / finite sequence case
CSEQ_induction: THEOREM FORALL cseq, p:
(FORALL n:
(FORALL m: m < n IMPLIES p_if_exists(p, cseq, m)) IMPLIES
p_if_exists(p, cseq, n)) IMPLIES every(p)(cseq)
% Strong induction over the elements: infinite sequence case
CSEQ_infinite_induction: THEOREM FORALL iseq, p:
(FORALL n:
(FORALL m: m < n IMPLIES p(nth(iseq, m))) IMPLIES
p(nth(iseq, n))) IMPLIES every(p)(iseq)
% Weak induction over all finite sequences
finite_sequence_induction: THEOREM FORALL sp:
sp(empty_cseq) AND
(FORALL n:
(FORALL fseq: length(fseq) = n IMPLIES sp(fseq)) IMPLIES
(FORALL fseq: length(fseq) = n + 1 IMPLIES sp(fseq))) IMPLIES (FORALL fseq: sp(fseq))
% Strong induction over all finite sequences
FINITE_SEQUENCE_induction: THEOREM FORALL sp:
(FORALL n:
(FORALL fseq: length(fseq) < n IMPLIES sp(fseq)) IMPLIES
(FORALL fseq: length(fseq) = n IMPLIES sp(fseq))) IMPLIES (FORALL fseq: sp(fseq))
% Weak induction over all sequences. This is only useful when the property % in question is trivially satisfied by all infinite sequences.
sequence_induction: THEOREM FORALL sp:
sp(empty_cseq) AND
(FORALL iseq: sp(iseq)) AND
(FORALL n:
(FORALL fseq: length(fseq) = n IMPLIES sp(fseq)) IMPLIES
(FORALL fseq: length(fseq) = n + 1 IMPLIES sp(fseq))) IMPLIES (FORALL cseq: sp(cseq))
% Strong induction over all sequences.
SEQUENCE_induction: THEOREM FORALL sp:
(FORALL iseq: sp(iseq)) AND
(FORALL n:
(FORALL fseq: length(fseq) < n IMPLIES sp(fseq)) IMPLIES
(FORALL fseq: length(fseq) = n IMPLIES sp(fseq))) IMPLIES (FORALL cseq: sp(cseq))
END csequence_induction
¤ 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.12Bemerkung:
(vorverarbeitet)
¤
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
