%-----------------------------------------------------------------------------
% Additional induction rules for sequences of countable length.
%
% Author: Jerry James <[email protected]>
%
% 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
¤ Dauer der Verarbeitung: 0.3 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
|
