| products/sources/formale sprachen/Isabelle/HOL/Hahn_Banach/document/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: horizontal_criterion_line.pvs Sprache: PVSOriginal von: PVS© |
|
||||||
|
%-----------------------------------------------------------------------------
% Constant sequences, both finite and infinite, defined as coalgebraic % datatypes. % % 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_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 ¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
