source: Deliverables/D4.1/Matita/Nat.ma @ 228

Last change on this file since 228 was 228, checked in by mulligan, 10 years ago

Conjunction, disjunction and 'xorjunction' implemented on bitvectors.
Lots of supporting datatypes. Vectors.ma includes some diabolical
dependent type hackery due to Wilmer.

File size: 2.2 KB
Line 
1include "Cartesian.ma".
2include "Maybe.ma".
3include "Bool.ma".
4
5include "logic/pts.ma".
6include "Plogic/equality.ma".
7
8ninductive Nat: Type[0] ≝
9  Z: Nat
10| S: Nat → Nat.
11
12nlet rec plus (n: Nat) (o: Nat) on n ≝
13  match n with
14    [ Z ⇒ o
15    | S p ⇒ S (plus p o)
16    ].
17   
18notation "n break + m"
19  right associative with precedence 52
20  for @{ 'plus $n $m }.
21 
22interpretation "Nat plus" 'plus n m = (plus n m).
23   
24nlet rec minus (n: Nat) (o: Nat) on n ≝
25  match n with
26    [ Z ⇒ Z
27    | S p ⇒
28      match o with
29        [ Z ⇒ S p
30        | S q ⇒ minus p q
31        ]
32    ].
33   
34notation "n break - m"
35  right associative with precedence 47
36  for @{ 'minus $n $m }.
37 
38interpretation "Nat minus" 'minus n m = (minus n m).
39   
40nlet rec multiplication (n: Nat) (o: Nat) on n ≝
41  match n with
42    [ Z ⇒ Z
43    | S p ⇒ o + (multiplication p o)
44    ].
45   
46notation "n break * m"
47  right associative with precedence 47
48  for @{ 'multiplication $n $m }.
49 
50interpretation "Nat multiplication" 'times n m = (multiplication n m).
51
52nlemma plus_zero:
53  ∀n: Nat.
54    n + Z = n.
55  #n.
56  nelim n.
57  nnormalize.
58  @.
59  #N H.
60  nnormalize.
61  nrewrite > H.
62  @.
63nqed.
64
65nlemma plus_associative:
66  ∀m, n, o: Nat.
67    (m + n) + o = m + (n + o).
68  #m n o.
69  nelim m.
70  nnormalize.
71  @.
72  #N H.
73  nnormalize.
74  nrewrite > H.
75  @.
76nqed.
77
78nlemma succ_plus:
79  ∀m, n: Nat.
80    S(m + n) = m + S(n).
81  #m n.
82  nelim m.
83  nnormalize.
84  @.
85  #N H.
86  nnormalize.
87  nrewrite > H.
88  @.
89nqed.
90
91nlemma plus_symmetrical:
92  ∀m, n: Nat.
93    m + n = n + m.
94  #m n.
95  nelim m.
96  nnormalize.
97  nelim n.
98  nnormalize.
99  @.
100  #N H.
101  nnormalize.
102  nrewrite < H.
103  @.
104  #N H.
105  nnormalize.
106  nrewrite > H.
107  napplyS succ_plus.
108nqed.
109
110nlemma multiplication_zero:
111  ∀m: Nat.
112    m * Z = Z.
113  #m.
114  nelim m.
115  nnormalize.
116  @.
117  #N H.
118  nnormalize.
119  nrewrite > H.
120  @.
121nqed.
122
123nlemma multiplication_succ:
124  ∀m, n: Nat.
125    m * S(n) = m + (m * n).
126  #m n.
127  nelim m.
128  nnormalize.
129  @.
130  #N H.
131  nnormalize.
132  napplyS plus_symmetrical.
133nqed.
134
135nlemma multiplication_symmetrical:
136  ∀m, n: Nat.
137    m * n = n * m.
138  #m n.
139  nelim m.
140  nnormalize.
141  nelim n.
142  nnormalize.
143  @.
144  #N H.
145  nnormalize.
146  nrewrite < H.
147  @.
148  #N H.
149  nnormalize.
150  nrewrite > H.
151  napplyS multiplication_succ.
152nqed.
153 
Note: See TracBrowser for help on using the repository browser.