Last change
on this file since 297 was
268,
checked in by sacerdot, 10 years ago

 notation moved to proper places
 new function split on Vectors

File size:
2.0 KB

Rev  Line  

[257]  1  (* ===================================== *) 

 2  (* Exponential.ma: Exponential (raising to a power) over the natural numbers. *) 

 3  (* ===================================== *) 

 4  

 5  include "Nat.ma". 

 6  

[268]  7  include "Plogic/equality.ma". 

[257]  8  include "Connectives.ma". 

 9  

 10  (* ===================================== *) 

 11  (* Exponential. *) 

 12  (* ===================================== *) 

 13  

 14  nlet rec exponential (m: Nat) (n: Nat) on n ≝ 

 15  match n with 

 16  [ Z ⇒ S (Z) 

 17   S o ⇒ m * (exponential m o) 

 18  ]. 

 19  

 20  (* DPM Bug: Matita's standard notation gets in the way here. Cannot use 

 21  'exponential instead of 'exp. *) 

 22  interpretation "Nat exponential" 'exp n m = (exponential n m). 

 23  

 24  (* ===================================== *) 

 25  (* Lemmas. *) 

 26  (* ===================================== *) 

 27  

 28  nlemma exponential_zero_succ_zero: 

 29  ∀n: Nat. 

 30  ¬(n = Z) → n^Z = (S Z). 

 31  #n. 

 32  nelim n. 

 33  //. 

 34  #N H. 

 35  //. 

 36  nqed. 

 37  

 38  nlemma exponential_succ_zero_neutral: 

 39  ∀n: Nat. 

 40  n^(S Z) = n. 

 41  #n. 

 42  nelim n. 

 43  //. 

 44  #N H. 

 45  nnormalize. 

 46  nrewrite > (multiplication_succ_zero_right_neutral ?). 

 47  @. 

 48  nqed. 

 49  

 50  nlemma succ_zero_exponential_succ_zero: 

 51  ∀m: Nat. 

 52  (S Z)^m = S Z. 

 53  #m. 

 54  nelim m. 

 55  //. 

 56  #N H. 

 57  nnormalize. 

 58  nrewrite > H. 

 59  nrewrite > (plus_zero ?). 

 60  @. 

 61  nqed. 

 62  

 63  naxiom exponential_addition_exponential_multiplication: 

 64  ∀m, n, o: Nat. 

 65  (m^n) * (m^o) = m^(n + o). 

 66  

 67  (* 

 68  nlemma exponential_exponential_multiplication: 

 69  ∀m, n, o: Nat. 

 70  (m^n)^o = m^(n × o). 

 71  #m n o. 

 72  nelim n. 

 73  nnormalize. 

 74  //. 

 75  #N H. 

 76  nnormalize. 

 77  nrewrite > H. 

 78  nrewrite < (exponential_addition_exponential_multiplication m o (N × o)). 

 79  nrewrite < H. 

[263]  80  *) 

Note: See
TracBrowser
for help on using the repository browser.