helm/software/matita/contribs/procedural/CoRN/algebra/Expon.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: Expon.v,v 1.5 2004/04/23 10:00:54 lcf Exp $ *)
  20
  21 (*#* printing [^^] %\ensuremath{\hat{\ }}% #^# *)
  22
  23 include "algebra/COrdCauchy.ma".
  24
  25 include "tactics/Transparent_algebra.ma".
  26
  27 (*#* *Exponentiation
  28 **More properties about [nexp]
  29 %\begin{convention}% Let [R] be an ordered field.
  30 %\end{convention}%
  31 *)
  32
  33 (* UNEXPORTED
  34 Section More_Nexp
  35 *)
  36
  37 (* UNEXPORTED
  38 cic:/CoRN/algebra/Expon/More_Nexp/R.var
  39 *)
  40
  41 inline procedural "cic:/CoRN/algebra/Expon/nexp_resp_ap_zero.con" as lemma.
  42
  43 (* UNEXPORTED
  44 Hint Resolve nexp_resp_ap_zero: algebra.
  45 *)
  46
  47 inline procedural "cic:/CoRN/algebra/Expon/nexp_distr_div.con" as lemma.
  48
  49 inline procedural "cic:/CoRN/algebra/Expon/nexp_distr_div'.con" as lemma.
  50
  51 inline procedural "cic:/CoRN/algebra/Expon/small_nexp_resp_lt.con" as lemma.
  52
  53 inline procedural "cic:/CoRN/algebra/Expon/great_nexp_resp_lt.con" as lemma.
  54
  55 inline procedural "cic:/CoRN/algebra/Expon/small_nexp_resp_le.con" as lemma.
  56
  57 inline procedural "cic:/CoRN/algebra/Expon/great_nexp_resp_le.con" as lemma.
  58
  59 inline procedural "cic:/CoRN/algebra/Expon/nexp_resp_leEq.con" as lemma.
  60
  61 inline procedural "cic:/CoRN/algebra/Expon/nexp_resp_leEq_one.con" as lemma.
  62
  63 inline procedural "cic:/CoRN/algebra/Expon/nexp_resp_leEq_neg_even.con" as lemma.
  64
  65 inline procedural "cic:/CoRN/algebra/Expon/nexp_resp_leEq_neg_odd.con" as lemma.
  66
  67 inline procedural "cic:/CoRN/algebra/Expon/nexp_distr_recip.con" as lemma.
  68
  69 (* UNEXPORTED
  70 Hint Resolve nexp_distr_recip: algebra.
  71 *)
  72
  73 inline procedural "cic:/CoRN/algebra/Expon/nexp_even_nonneg.con" as lemma.
  74
  75 inline procedural "cic:/CoRN/algebra/Expon/nexp_resp_le'.con" as lemma.
  76
  77 inline procedural "cic:/CoRN/algebra/Expon/nexp_resp_le.con" as lemma.
  78
  79 inline procedural "cic:/CoRN/algebra/Expon/bin_less_un.con" as lemma.
  80
  81 (* UNEXPORTED
  82 End More_Nexp
  83 *)
  84
  85 (* UNEXPORTED
  86 Hint Resolve nexp_distr_div nexp_distr_recip: algebra.
  87 *)
  88
  89 (* UNEXPORTED
  90 Implicit Arguments nexp_resp_ap_zero [R x].
  91 *)
  92
  93 (*#* **Definition of [zexp]: integer exponentiation
  94 %\begin{convention}% Let [R] be an ordered field.
  95 %\end{convention}%
  96 *)
  97
  98 (* UNEXPORTED
  99 Section Zexp_def
 100 *)
 101
 102 (* UNEXPORTED
 103 cic:/CoRN/algebra/Expon/Zexp_def/R.var
 104 *)
 105
 106 (*#*
 107 It would be nicer to define [zexp] using [caseZdiff], but we already
 108 have most properties now.
 109 *)
 110
 111 inline procedural "cic:/CoRN/algebra/Expon/zexp.con" as definition.
 112
 113 (* UNEXPORTED
 114 End Zexp_def
 115 *)
 116
 117 (* UNEXPORTED
 118 Implicit Arguments zexp [R].
 119 *)
 120
 121 (* NOTATION
 122 Notation "( x [//] Hx ) [^^] n" := (zexp x Hx n) (at level 0).
 123 *)
 124
 125 (*#* **Properties of [zexp]
 126 %\begin{convention}% Let [R] be an ordered field.
 127 %\end{convention}%
 128 *)
 129
 130 (* UNEXPORTED
 131 Section Zexp_properties
 132 *)
 133
 134 (* UNEXPORTED
 135 cic:/CoRN/algebra/Expon/Zexp_properties/R.var
 136 *)
 137
 138 inline procedural "cic:/CoRN/algebra/Expon/zexp_zero.con" as lemma.
 139
 140 (* UNEXPORTED
 141 Hint Resolve zexp_zero: algebra.
 142 *)
 143
 144 inline procedural "cic:/CoRN/algebra/Expon/zexp_nexp.con" as lemma.
 145
 146 (* UNEXPORTED
 147 Hint Resolve zexp_nexp: algebra.
 148 *)
 149
 150 inline procedural "cic:/CoRN/algebra/Expon/zexp_inv_nexp.con" as lemma.
 151
 152 (* UNEXPORTED
 153 Hint Resolve zexp_inv_nexp: algebra.
 154 *)
 155
 156 inline procedural "cic:/CoRN/algebra/Expon/zexp_inv_nexp'.con" as lemma.
 157
 158 (* UNEXPORTED
 159 Hint Resolve zexp_inv_nexp': algebra.
 160 *)
 161
 162 inline procedural "cic:/CoRN/algebra/Expon/zexp_strext.con" as lemma.
 163
 164 inline procedural "cic:/CoRN/algebra/Expon/zexp_wd.con" as lemma.
 165
 166 (* UNEXPORTED
 167 Hint Resolve zexp_wd: algebra_c.
 168 *)
 169
 170 inline procedural "cic:/CoRN/algebra/Expon/zexp_plus1.con" as lemma.
 171
 172 (* UNEXPORTED
 173 Hint Resolve zexp_plus1: algebra.
 174 *)
 175
 176 inline procedural "cic:/CoRN/algebra/Expon/zexp_resp_ap_zero.con" as lemma.
 177
 178 (* UNEXPORTED
 179 Hint Resolve zexp_resp_ap_zero: algebra.
 180 *)
 181
 182 inline procedural "cic:/CoRN/algebra/Expon/zexp_inv.con" as lemma.
 183
 184 (* UNEXPORTED
 185 Hint Resolve zexp_inv: algebra.
 186 *)
 187
 188 inline procedural "cic:/CoRN/algebra/Expon/zexp_inv1.con" as lemma.
 189
 190 (* UNEXPORTED
 191 Hint Resolve zexp_inv1: algebra.
 192 *)
 193
 194 inline procedural "cic:/CoRN/algebra/Expon/zexp_plus.con" as lemma.
 195
 196 (* UNEXPORTED
 197 Hint Resolve zexp_plus: algebra.
 198 *)
 199
 200 inline procedural "cic:/CoRN/algebra/Expon/zexp_minus.con" as lemma.
 201
 202 (* UNEXPORTED
 203 Hint Resolve zexp_minus: algebra.
 204 *)
 205
 206 inline procedural "cic:/CoRN/algebra/Expon/one_zexp.con" as lemma.
 207
 208 (* UNEXPORTED
 209 Hint Resolve one_zexp: algebra.
 210 *)
 211
 212 inline procedural "cic:/CoRN/algebra/Expon/mult_zexp.con" as lemma.
 213
 214 (* UNEXPORTED
 215 Hint Resolve mult_zexp: algebra.
 216 *)
 217
 218 inline procedural "cic:/CoRN/algebra/Expon/zexp_mult.con" as lemma.
 219
 220 (* UNEXPORTED
 221 Hint Resolve zexp_mult: algebra.
 222 *)
 223
 224 inline procedural "cic:/CoRN/algebra/Expon/zexp_two.con" as lemma.
 225
 226 (* UNEXPORTED
 227 Hint Resolve zexp_two: algebra.
 228 *)
 229
 230 inline procedural "cic:/CoRN/algebra/Expon/inv_zexp_even.con" as lemma.
 231
 232 (* UNEXPORTED
 233 Hint Resolve inv_zexp_even: algebra.
 234 *)
 235
 236 inline procedural "cic:/CoRN/algebra/Expon/inv_zexp_two.con" as lemma.
 237
 238 (* UNEXPORTED
 239 Hint Resolve inv_zexp_two: algebra.
 240 *)
 241
 242 inline procedural "cic:/CoRN/algebra/Expon/inv_zexp_odd.con" as lemma.
 243
 244 inline procedural "cic:/CoRN/algebra/Expon/zexp_one.con" as lemma.
 245
 246 (* UNEXPORTED
 247 Hint Resolve zexp_one: algebra.
 248 *)
 249
 250 inline procedural "cic:/CoRN/algebra/Expon/zexp_funny.con" as lemma.
 251
 252 (* UNEXPORTED
 253 Hint Resolve zexp_funny: algebra.
 254 *)
 255
 256 inline procedural "cic:/CoRN/algebra/Expon/zexp_funny'.con" as lemma.
 257
 258 (* UNEXPORTED
 259 Hint Resolve zexp_funny': algebra.
 260 *)
 261
 262 inline procedural "cic:/CoRN/algebra/Expon/zexp_pos.con" as lemma.
 263
 264 (* UNEXPORTED
 265 End Zexp_properties
 266 *)
 267
 268 (* UNEXPORTED
 269 Hint Resolve nexp_resp_ap_zero zexp_zero zexp_nexp zexp_inv_nexp
 270   zexp_inv_nexp' zexp_plus1 zexp_resp_ap_zero zexp_inv zexp_inv1 zexp_plus
 271   zexp_minus one_zexp mult_zexp zexp_mult zexp_two inv_zexp_even inv_zexp_two
 272   zexp_one zexp_funny zexp_funny': algebra.
 273 *)
 274
 275 (* UNEXPORTED
 276 Hint Resolve zexp_wd: algebra_c.
 277 *)
 278
 279 (* UNEXPORTED
 280 Section Root_Unique
 281 *)
 282
 283 (* UNEXPORTED
 284 cic:/CoRN/algebra/Expon/Root_Unique/R.var
 285 *)
 286
 287 inline procedural "cic:/CoRN/algebra/Expon/root_unique.con" as lemma.
 288
 289 inline procedural "cic:/CoRN/algebra/Expon/root_one.con" as lemma.
 290
 291 (* UNEXPORTED
 292 End Root_Unique
 293 *)
 294