1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* Questo materiale fa parte della tesi: *)
22 (* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
24 (* data ultima modifica 15/11/2007 *)
25 (* ********************************************************************** *)
27 include "freescale/bool_lemmas.ma".
28 include "freescale/nat.ma".
34 nlemma nat_destruct_S_S : ∀n1,n2:nat.S n1 = S n2 → n1 = n2.
36 nchange with (match S n2 with [ O ⇒ False | S a ⇒ n1 = a ]);
42 nlemma nat_destruct_0_S : ∀n:nat.O = S n → False.
44 nchange with (match S n with [ O ⇒ True | S a ⇒ False ]);
50 nlemma nat_destruct_S_0 : ∀n:nat.S n = O → False.
52 nchange with (match S n with [ O ⇒ True | S a ⇒ False ]);
58 nlemma symmetric_eqnat : symmetricT nat bool eq_nat.
65 ##[ ##1: napply (refl_eq ??)
66 ##| ##2: #n3; #H; napply (refl_eq ??)
68 ##| ##2: #n2; #H; #n3;
72 ##[ ##1: napply (refl_eq ??)
73 ##| ##2: #n4; napply (H n4)
78 nlemma eq_to_eqnat : ∀n1,n2:nat.n1 = n2 → eq_nat n1 n2 = true.
84 ##[ ##1: #H; napply (refl_eq ??)
85 ##| ##2: #n3; #H; #H1; nelim (nat_destruct_0_S ? H1)
87 ##| ##2: #n2; #H; #n3; #H1;
88 ncases n3 in H1:(%) ⊢ %;
90 ##[ ##1: #H1; nelim (nat_destruct_S_0 ? H1)
92 napply (H n4 (nat_destruct_S_S ?? H1))
97 nlemma eqnat_to_eq : ∀n1,n2:nat.(eq_nat n1 n2 = true → n1 = n2).
103 ##[ ##1: #H; napply (refl_eq ??)
104 ##| ##2: #n3; #H; #H1; napply (bool_destruct ?? (O = S n3) H1)
106 ##| ##2: #n2; #H; #n3; #H1;
107 ncases n3 in H1:(%) ⊢ %;
109 ##[ ##1: #H1; napply (bool_destruct ?? (S n2 = O) H1)
111 nrewrite > (H n4 H1);
117 nlemma Sn_p_n_to_S_npn : ∀n1,n2.(S n1) + n2 = S (n1 + n2).
120 ##[ ##1: nnormalize; #n2; napply (refl_eq ??)
121 ##| ##2: #n; #H; #n2; nrewrite > (H n2);
122 ncases n in H:(%) ⊢ %;
123 ##[ ##1: nnormalize; #H; napply (refl_eq ??)
124 ##| ##2: #n3; nnormalize; #H; napply (refl_eq ??)
129 nlemma n_p_Sn_to_S_npn : ∀n1,n2.n1 + (S n2) = S (n1 + n2).
132 ##[ ##1: nnormalize; #n2; napply (refl_eq ??)
133 ##| ##2: #n; #H; #n2;
134 nrewrite > (Sn_p_n_to_S_npn n (S n2));
140 nlemma Opn_to_n : ∀n.O + n = n.
141 #n; nnormalize; napply (refl_eq ??).
144 nlemma npO_to_n : ∀n.n + O = n.
147 ##[ ##1: nnormalize; napply (refl_eq ??)
149 nrewrite > (Sn_p_n_to_S_npn n1 O);
155 nlemma symmetric_plusnat : symmetricT nat nat plus.
158 ##[ ##1: #n2; nrewrite > (npO_to_n n2); nnormalize; napply (refl_eq ??)
159 ##| ##2: #n2; #H; #n3;
160 nrewrite > (Sn_p_n_to_S_npn n2 n3);
161 nrewrite > (n_p_Sn_to_S_npn n3 n2);