source: Deliverables/D4.1/Matita/Exponential.ma @ 257

Last change on this file since 257 was 257, checked in by mulligan, 9 years ago

Added exponential functions for nats. Working on operational semantics of processor.

File size: 2.3 KB
Line 
1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* Exponential.ma: Exponential (raising to a power) over the natural numbers. *)
3(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
4
5include "Nat.ma".
6
7include "Equality.ma".
8include "Connectives.ma".
9
10(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
11(* Syntax.                                                                    *)
12(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
13
14notation "hvbox(n^m)"
15  left associative with precedence 52
16  for @{ 'exponential $n $m }.
17
18(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
19(* Exponential.                                                               *)
20(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
21
22nlet rec exponential (m: Nat) (n: Nat) on n ≝
23  match n with
24    [ Z ⇒ S (Z)
25    | S o ⇒ m * (exponential m o)
26    ].
27   
28(* DPM Bug: Matita's standard notation gets in the way here.  Cannot use
29            'exponential instead of 'exp.                                     *)
30interpretation "Nat exponential" 'exp n m = (exponential n m).
31
32(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
33(* Lemmas.                                                                    *)
34(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
35
36nlemma exponential_zero_succ_zero:
37  ∀n: Nat.
38    ¬(n = Z) → n^Z = (S Z).
39  #n.
40  nelim n.
41  //.
42  #N H.
43  //.
44nqed.
45
46nlemma exponential_succ_zero_neutral:
47  ∀n: Nat.
48    n^(S Z) = n.
49  #n.
50  nelim n.
51  //.
52  #N H.
53  nnormalize.
54  nrewrite > (multiplication_succ_zero_right_neutral ?).
55  @.
56nqed.
57
58nlemma succ_zero_exponential_succ_zero:
59  ∀m: Nat.
60    (S Z)^m = S Z.
61  #m.
62  nelim m.
63  //.
64  #N H.
65  nnormalize.
66  nrewrite > H.
67  nrewrite > (plus_zero ?).
68  @.
69nqed.
70
71naxiom exponential_addition_exponential_multiplication:
72  ∀m, n, o: Nat.
73    (m^n) * (m^o) = m^(n + o).
74
75(*
76nlemma exponential_exponential_multiplication:
77  ∀m, n, o: Nat.
78    (m^n)^o = m^(n × o).
79  #m n o.
80  nelim n.
81  nnormalize.
82  //.
83  #N H.
84  nnormalize.
85  nrewrite > H.
86  nrewrite < (exponential_addition_exponential_multiplication m o (N × o)).
87  nrewrite < H.
88*)
Note: See TracBrowser for help on using the repository browser.