]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/ng_assembly/num/quatern.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / ng_assembly / num / quatern.ma
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 (* ********************************************************************** *)
16 (*                          Progetto FreeScale                            *)
17 (*                                                                        *)
18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
19 (*   Sviluppo: 2008-2010                                                  *)
20 (*                                                                        *)
21 (* ********************************************************************** *)
22
23 include "num/bool.ma".
24
25 (* ********** *)
26 (* QUATERNARI *)
27 (* ********** *)
28
29 ninductive quatern : Type ≝
30   q0 : quatern
31 | q1 : quatern
32 | q2 : quatern
33 | q3 : quatern.
34
35 (* operatore = *)
36 ndefinition eq_qu ≝
37 λn1,n2:quatern.
38  match n1 with
39   [ q0 ⇒ match n2 with [ q0 ⇒ true | _ ⇒ false ]
40   | q1 ⇒ match n2 with [ q1 ⇒ true | _ ⇒ false ]
41   | q2 ⇒ match n2 with [ q2 ⇒ true | _ ⇒ false ]
42   | q3 ⇒ match n2 with [ q3 ⇒ true | _ ⇒ false ]
43   ].
44
45 (* iteratore sui quaternari *)
46 ndefinition forall_qu ≝ λP.
47  P q0 ⊗ P q1 ⊗ P q2 ⊗ P q3.
48
49 (* operatore successorre *)
50 ndefinition succ_qu ≝
51 λn.match n with
52  [ q0 ⇒ q1 | q1 ⇒ q2 | q2 ⇒ q3 | q3 ⇒ q0 ].
53
54 (* quaternari ricorsivi *)
55 ninductive rec_quatern : quatern → Type ≝
56   qu_O : rec_quatern q0
57 | qu_S : ∀n.rec_quatern n → rec_quatern (succ_qu n).
58
59 (* quaternari → quaternari ricorsivi *)
60 ndefinition qu_to_recqu ≝
61 λn.match n return λx.rec_quatern x with
62  [ q0 ⇒ qu_O
63  | q1 ⇒ qu_S ? qu_O
64  | q2 ⇒ qu_S ? (qu_S ? qu_O)
65  | q3 ⇒ qu_S ? (qu_S ? (qu_S ? qu_O))
66  ].