]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/ng_assembly/num/oct.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / ng_assembly / num / oct.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 (* OTTALI *)
27 (* ****** *)
28
29 ninductive oct : Type ≝
30   o0: oct
31 | o1: oct
32 | o2: oct
33 | o3: oct
34 | o4: oct
35 | o5: oct
36 | o6: oct
37 | o7: oct.
38
39 (* iteratore sugli ottali *)
40 ndefinition forall_oct ≝ λP.
41  P o0 ⊗ P o1 ⊗ P o2 ⊗ P o3 ⊗ P o4 ⊗ P o5 ⊗ P o6 ⊗ P o7.
42
43 (* operatore = *)
44 ndefinition eq_oct ≝
45 λn1,n2:oct.
46  match n1 with
47   [ o0 ⇒ match n2 with [ o0 ⇒ true  | _ ⇒ false ]
48   | o1 ⇒ match n2 with [ o1 ⇒ true  | _ ⇒ false ] 
49   | o2 ⇒ match n2 with [ o2 ⇒ true  | _ ⇒ false ]
50   | o3 ⇒ match n2 with [ o3 ⇒ true  | _ ⇒ false ] 
51   | o4 ⇒ match n2 with [ o4 ⇒ true  | _ ⇒ false ]  
52   | o5 ⇒ match n2 with [ o5 ⇒ true  | _ ⇒ false ] 
53   | o6 ⇒ match n2 with [ o6 ⇒ true  | _ ⇒ false ]  
54   | o7 ⇒ match n2 with [ o7 ⇒ true  | _ ⇒ false ] 
55   ].
56
57 (* operatore and *)
58 ndefinition and_oct ≝
59 λe1,e2:oct.match e1 with
60  [ o0 ⇒ match e2 with
61   [ o0 ⇒ o0 | o1 ⇒ o0 | o2 ⇒ o0 | o3 ⇒ o0 
62   | o4 ⇒ o0 | o5 ⇒ o0 | o6 ⇒ o0 | o7 ⇒ o0 ]
63  | o1 ⇒ match e2 with
64   [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o0 | o3 ⇒ o1 
65   | o4 ⇒ o0 | o5 ⇒ o1 | o6 ⇒ o0 | o7 ⇒ o1 ]
66  | o2 ⇒ match e2 with
67   [ o0 ⇒ o0 | o1 ⇒ o0 | o2 ⇒ o2 | o3 ⇒ o2 
68   | o4 ⇒ o0 | o5 ⇒ o0 | o6 ⇒ o2 | o7 ⇒ o2 ]
69  | o3 ⇒ match e2 with
70   [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o2 | o3 ⇒ o3 
71   | o4 ⇒ o0 | o5 ⇒ o1 | o6 ⇒ o2 | o7 ⇒ o3 ]
72  | o4 ⇒ match e2 with
73   [ o0 ⇒ o0 | o1 ⇒ o0 | o2 ⇒ o0 | o3 ⇒ o0 
74   | o4 ⇒ o4 | o5 ⇒ o4 | o6 ⇒ o4 | o7 ⇒ o4 ]
75  | o5 ⇒ match e2 with
76   [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o0 | o3 ⇒ o1 
77   | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o4 | o7 ⇒ o5 ]
78  | o6 ⇒ match e2 with
79   [ o0 ⇒ o0 | o1 ⇒ o0 | o2 ⇒ o2 | o3 ⇒ o2 
80   | o4 ⇒ o4 | o5 ⇒ o4 | o6 ⇒ o6 | o7 ⇒ o6 ]
81  | o7 ⇒ match e2 with
82   [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o2 | o3 ⇒ o3 
83   | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o6 | o7 ⇒ o7 ]
84  ]. 
85
86 (* operatore or *)
87 ndefinition or_oct ≝
88 λe1,e2:oct.match e1 with
89  [ o0 ⇒ match e2 with
90   [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o2 | o3 ⇒ o3 
91   | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o6 | o7 ⇒ o7 ]
92  | o1 ⇒ match e2 with
93   [ o0 ⇒ o1 | o1 ⇒ o1 | o2 ⇒ o3 | o3 ⇒ o3 
94   | o4 ⇒ o5 | o5 ⇒ o5 | o6 ⇒ o7 | o7 ⇒ o7 ]
95  | o2 ⇒ match e2 with
96   [ o0 ⇒ o2 | o1 ⇒ o3 | o2 ⇒ o2 | o3 ⇒ o3 
97   | o4 ⇒ o6 | o5 ⇒ o7 | o6 ⇒ o6 | o7 ⇒ o7 ]
98  | o3 ⇒ match e2 with
99   [ o0 ⇒ o3 | o1 ⇒ o3 | o2 ⇒ o3 | o3 ⇒ o3 
100   | o4 ⇒ o7 | o5 ⇒ o7 | o6 ⇒ o7 | o7 ⇒ o7 ]
101  | o4 ⇒ match e2 with
102   [ o0 ⇒ o4 | o1 ⇒ o5 | o2 ⇒ o6 | o3 ⇒ o7 
103   | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o6 | o7 ⇒ o7 ]
104  | o5 ⇒ match e2 with
105   [ o0 ⇒ o5 | o1 ⇒ o5 | o2 ⇒ o7 | o3 ⇒ o7 
106   | o4 ⇒ o5 | o5 ⇒ o5 | o6 ⇒ o7 | o7 ⇒ o7 ]
107  | o6 ⇒ match e2 with
108   [ o0 ⇒ o6 | o1 ⇒ o7 | o2 ⇒ o6 | o3 ⇒ o7 
109   | o4 ⇒ o6 | o5 ⇒ o7 | o6 ⇒ o6 | o7 ⇒ o7 ]
110  | o7 ⇒ match e2 with
111   [ o0 ⇒ o7 | o1 ⇒ o7 | o2 ⇒ o7 | o3 ⇒ o7 
112   | o4 ⇒ o7 | o5 ⇒ o7 | o6 ⇒ o7 | o7 ⇒ o7 ]
113  ].
114
115 (* operatore xor *)
116 ndefinition xor_oct ≝
117 λe1,e2:oct.match e1 with
118  [ o0 ⇒ match e2 with
119   [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o2 | o3 ⇒ o3 
120   | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o6 | o7 ⇒ o7 ] 
121  | o1 ⇒ match e2 with
122   [ o0 ⇒ o1 | o1 ⇒ o0 | o2 ⇒ o3 | o3 ⇒ o2 
123   | o4 ⇒ o5 | o5 ⇒ o4 | o6 ⇒ o7 | o7 ⇒ o6 ] 
124  | o2 ⇒ match e2 with
125   [ o0 ⇒ o2 | o1 ⇒ o3 | o2 ⇒ o0 | o3 ⇒ o1 
126   | o4 ⇒ o6 | o5 ⇒ o7 | o6 ⇒ o4 | o7 ⇒ o5 ] 
127  | o3 ⇒ match e2 with
128   [ o0 ⇒ o3 | o1 ⇒ o2 | o2 ⇒ o1 | o3 ⇒ o0 
129   | o4 ⇒ o7 | o5 ⇒ o6 | o6 ⇒ o5 | o7 ⇒ o4 ] 
130  | o4 ⇒ match e2 with
131   [ o0 ⇒ o4 | o1 ⇒ o5 | o2 ⇒ o6 | o3 ⇒ o7 
132   | o4 ⇒ o0 | o5 ⇒ o1 | o6 ⇒ o2 | o7 ⇒ o3 ] 
133  | o5 ⇒ match e2 with
134   [ o0 ⇒ o5 | o1 ⇒ o4 | o2 ⇒ o7 | o3 ⇒ o6 
135   | o4 ⇒ o1 | o5 ⇒ o0 | o6 ⇒ o3 | o7 ⇒ o2 ] 
136  | o6 ⇒ match e2 with
137   [ o0 ⇒ o6 | o1 ⇒ o7 | o2 ⇒ o4 | o3 ⇒ o5 
138   | o4 ⇒ o2 | o5 ⇒ o3 | o6 ⇒ o0 | o7 ⇒ o1 ] 
139  | o7 ⇒ match e2 with
140   [ o0 ⇒ o7 | o1 ⇒ o6 | o2 ⇒ o5 | o3 ⇒ o4 
141   | o4 ⇒ o3 | o5 ⇒ o2 | o6 ⇒ o1 | o7 ⇒ o0 ] 
142  ].
143
144 (* operatore successore *)
145 ndefinition succ_oct ≝
146 λn.match n with
147  [ o0 ⇒ o1 | o1 ⇒ o2 | o2 ⇒ o3 | o3 ⇒ o4 | o4 ⇒ o5 | o5 ⇒ o6 | o6 ⇒ o7 | o7 ⇒ o0 ].
148
149 (* ottali ricorsivi *)
150 ninductive rec_oct : oct → Type ≝
151   oc_O : rec_oct o0
152 | oc_S : ∀n.rec_oct n → rec_oct (succ_oct n).
153
154 (* ottali → ottali ricorsivi *)
155 ndefinition oct_to_recoct ≝
156 λn.match n return λx.rec_oct x with
157  [ o0 ⇒ oc_O
158  | o1 ⇒ oc_S ? oc_O
159  | o2 ⇒ oc_S ? (oc_S ? oc_O)
160  | o3 ⇒ oc_S ? (oc_S ? (oc_S ? oc_O))
161  | o4 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O)))
162  | o5 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O))))
163  | o6 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O)))))
164  | o7 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O))))))
165  ].