helm/software/matita/contribs/procedural/CoRN/reals/RealLists.mma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "CoRN.ma".
  18
  19 (* $Id: RealLists.v,v 1.4 2004/04/23 10:01:05 lcf Exp $ *)
  20
  21 include "reals/CReals1.ma".
  22
  23 (* UNEXPORTED
  24 Section Lists
  25 *)
  26
  27 (*#* * Lists of Real Numbers
  28
  29 In some contexts we will need to work with nested existential quantified formulas of the form $\exists_{n\in\NN}\exists_{x_1,\ldots,x_n}P(x_1,\ldots,x_n)$#exists n exists x1,...,xn P(x1,..,xn)#.  One way of formalizing this kind of statement is through quantifying over lists.  In this file we provide some tools for manipulating lists.
  30
  31 Notice that some of the properties listed below only make sense in the context within which we are working.  Unlike in the other lemma files, no care has been taken here to state the lemmas in their most general form, as that would make them very unpractical to use.
  32
  33 %\bigskip%
  34
  35 We start by defining maximum and minimum of lists of reals and two membership predicates. The value of these functions for the empty list is arbitrarily set to 0, but it will be irrelevant, as we will never work with empty lists.
  36 *)
  37
  38 inline procedural "cic:/CoRN/reals/RealLists/maxlist.con" as definition.
  39
  40 inline procedural "cic:/CoRN/reals/RealLists/minlist.con" as definition.
  41
  42 inline procedural "cic:/CoRN/reals/RealLists/member.con" as definition.
  43
  44 (*#*
  45 Sometimes the length of the list has to be restricted; the next definition provides an easy way to do that. *)
  46
  47 inline procedural "cic:/CoRN/reals/RealLists/length_leEq.con" as definition.
  48
  49 (*#* Length is preserved by mapping. *)
  50
  51 (* UNEXPORTED
  52 Implicit Arguments map [A B].
  53 *)
  54
  55 inline procedural "cic:/CoRN/reals/RealLists/map_pres_length.con" as lemma.
  56
  57 (*#*
  58 Often we want to map partial functions through a list; this next operator provides a way to do that, and is proved to be correct. *)
  59
  60 (* UNEXPORTED
  61 Implicit Arguments cons [A].
  62 *)
  63
  64 inline procedural "cic:/CoRN/reals/RealLists/map2.con" as definition.
  65
  66 inline procedural "cic:/CoRN/reals/RealLists/map2_wd.con" as lemma.
  67
  68 inline procedural "cic:/CoRN/reals/RealLists/map2_pres_member.con" as lemma.
  69
  70 (*#*
  71 As [maxlist] and [minlist] are generalizations of [Max] and [Min] to finite sets of real numbers, they have the expected properties: *)
  72
  73 inline procedural "cic:/CoRN/reals/RealLists/maxlist_greater.con" as lemma.
  74
  75 (* begin hide *)
  76
  77 inline procedural "cic:/CoRN/reals/RealLists/Lists/maxlist_aux.con" "Lists__" as definition.
  78
  79 (* end hide *)
  80
  81 inline procedural "cic:/CoRN/reals/RealLists/maxlist_leEq_eps.con" as lemma.
  82
  83 inline procedural "cic:/CoRN/reals/RealLists/maxlist_less.con" as lemma.
  84
  85 inline procedural "cic:/CoRN/reals/RealLists/maxlist_leEq.con" as lemma.
  86
  87 inline procedural "cic:/CoRN/reals/RealLists/minlist_smaller.con" as lemma.
  88
  89 (* begin hide *)
  90
  91 inline procedural "cic:/CoRN/reals/RealLists/Lists/minlist_aux.con" "Lists__" as definition.
  92
  93 (* end hide *)
  94
  95 inline procedural "cic:/CoRN/reals/RealLists/minlist_leEq_eps.con" as lemma.
  96
  97 inline procedural "cic:/CoRN/reals/RealLists/less_minlist.con" as lemma.
  98
  99 inline procedural "cic:/CoRN/reals/RealLists/leEq_minlist.con" as lemma.
 100
 101 (* UNEXPORTED
 102 End Lists
 103 *)
 104