]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/ng_assembly/num/bitrigesim.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / ng_assembly / num / bitrigesim.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 (* BITRIGESIMALI *)
27 (* ************* *)
28
29 ninductive bitrigesim : Type ≝
30   t00: bitrigesim
31 | t01: bitrigesim
32 | t02: bitrigesim
33 | t03: bitrigesim
34 | t04: bitrigesim
35 | t05: bitrigesim
36 | t06: bitrigesim
37 | t07: bitrigesim
38 | t08: bitrigesim
39 | t09: bitrigesim
40 | t0A: bitrigesim
41 | t0B: bitrigesim
42 | t0C: bitrigesim
43 | t0D: bitrigesim
44 | t0E: bitrigesim
45 | t0F: bitrigesim
46 | t10: bitrigesim
47 | t11: bitrigesim
48 | t12: bitrigesim
49 | t13: bitrigesim
50 | t14: bitrigesim
51 | t15: bitrigesim
52 | t16: bitrigesim
53 | t17: bitrigesim
54 | t18: bitrigesim
55 | t19: bitrigesim
56 | t1A: bitrigesim
57 | t1B: bitrigesim
58 | t1C: bitrigesim
59 | t1D: bitrigesim
60 | t1E: bitrigesim
61 | t1F: bitrigesim.
62
63 (* operatore = *)
64 ndefinition eq_bit ≝
65 λt1,t2:bitrigesim.
66  match t1 with
67   [ t00 ⇒ match t2 with [ t00 ⇒ true | _ ⇒ false ] | t01 ⇒ match t2 with [ t01 ⇒ true | _ ⇒ false ]
68   | t02 ⇒ match t2 with [ t02 ⇒ true | _ ⇒ false ] | t03 ⇒ match t2 with [ t03 ⇒ true | _ ⇒ false ]
69   | t04 ⇒ match t2 with [ t04 ⇒ true | _ ⇒ false ] | t05 ⇒ match t2 with [ t05 ⇒ true | _ ⇒ false ]
70   | t06 ⇒ match t2 with [ t06 ⇒ true | _ ⇒ false ] | t07 ⇒ match t2 with [ t07 ⇒ true | _ ⇒ false ]
71   | t08 ⇒ match t2 with [ t08 ⇒ true | _ ⇒ false ] | t09 ⇒ match t2 with [ t09 ⇒ true | _ ⇒ false ]
72   | t0A ⇒ match t2 with [ t0A ⇒ true | _ ⇒ false ] | t0B ⇒ match t2 with [ t0B ⇒ true | _ ⇒ false ]
73   | t0C ⇒ match t2 with [ t0C ⇒ true | _ ⇒ false ] | t0D ⇒ match t2 with [ t0D ⇒ true | _ ⇒ false ]
74   | t0E ⇒ match t2 with [ t0E ⇒ true | _ ⇒ false ] | t0F ⇒ match t2 with [ t0F ⇒ true | _ ⇒ false ]
75   | t10 ⇒ match t2 with [ t10 ⇒ true | _ ⇒ false ] | t11 ⇒ match t2 with [ t11 ⇒ true | _ ⇒ false ]
76   | t12 ⇒ match t2 with [ t12 ⇒ true | _ ⇒ false ] | t13 ⇒ match t2 with [ t13 ⇒ true | _ ⇒ false ]
77   | t14 ⇒ match t2 with [ t14 ⇒ true | _ ⇒ false ] | t15 ⇒ match t2 with [ t15 ⇒ true | _ ⇒ false ]
78   | t16 ⇒ match t2 with [ t16 ⇒ true | _ ⇒ false ] | t17 ⇒ match t2 with [ t17 ⇒ true | _ ⇒ false ]
79   | t18 ⇒ match t2 with [ t18 ⇒ true | _ ⇒ false ] | t19 ⇒ match t2 with [ t19 ⇒ true | _ ⇒ false ]
80   | t1A ⇒ match t2 with [ t1A ⇒ true | _ ⇒ false ] | t1B ⇒ match t2 with [ t1B ⇒ true | _ ⇒ false ]
81   | t1C ⇒ match t2 with [ t1C ⇒ true | _ ⇒ false ] | t1D ⇒ match t2 with [ t1D ⇒ true | _ ⇒ false ]
82   | t1E ⇒ match t2 with [ t1E ⇒ true | _ ⇒ false ] | t1F ⇒ match t2 with [ t1F ⇒ true | _ ⇒ false ]
83   ].
84
85 (* iteratore sui bitrigesimali *)
86 ndefinition forall_bit ≝ λP.
87  P t00 ⊗ P t01 ⊗ P t02 ⊗ P t03 ⊗ P t04 ⊗ P t05 ⊗ P t06 ⊗ P t07 ⊗
88  P t08 ⊗ P t09 ⊗ P t0A ⊗ P t0B ⊗ P t0C ⊗ P t0D ⊗ P t0E ⊗ P t0F ⊗
89  P t10 ⊗ P t11 ⊗ P t12 ⊗ P t13 ⊗ P t14 ⊗ P t15 ⊗ P t16 ⊗ P t17 ⊗
90  P t18 ⊗ P t19 ⊗ P t1A ⊗ P t1B ⊗ P t1C ⊗ P t1D ⊗ P t1E ⊗ P t1F.
91
92 (* operatore successore *)
93 ndefinition succ_bit ≝
94 λn.match n with
95  [ t00 ⇒ t01 | t01 ⇒ t02 | t02 ⇒ t03 | t03 ⇒ t04 | t04 ⇒ t05 | t05 ⇒ t06 | t06 ⇒ t07 | t07 ⇒ t08
96  | t08 ⇒ t09 | t09 ⇒ t0A | t0A ⇒ t0B | t0B ⇒ t0C | t0C ⇒ t0D | t0D ⇒ t0E | t0E ⇒ t0F | t0F ⇒ t10
97  | t10 ⇒ t11 | t11 ⇒ t12 | t12 ⇒ t13 | t13 ⇒ t14 | t14 ⇒ t15 | t15 ⇒ t16 | t16 ⇒ t17 | t17 ⇒ t18
98  | t18 ⇒ t19 | t19 ⇒ t1A | t1A ⇒ t1B | t1B ⇒ t1C | t1C ⇒ t1D | t1D ⇒ t1E | t1E ⇒ t1F | t1F ⇒ t00
99  ].
100
101 (* bitrigesimali ricorsivi *)
102 ninductive rec_bitrigesim : bitrigesim → Type ≝
103   bi_O : rec_bitrigesim t00
104 | bi_S : ∀n.rec_bitrigesim n → rec_bitrigesim (succ_bit n).
105
106 (* bitrigesimali → bitrigesimali ricorsivi *)
107 ndefinition bit_to_recbit ≝
108 λn.match n return λx.rec_bitrigesim x with
109  [ t00 ⇒ bi_O
110  | t01 ⇒ bi_S ? bi_O
111  | t02 ⇒ bi_S ? (bi_S ? bi_O)
112  | t03 ⇒ bi_S ? (bi_S ? (bi_S ? bi_O))
113  | t04 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))
114  | t05 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))
115  | t06 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))
116  | t07 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))
117  | t08 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
118          bi_O)))))))
119  | t09 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
120         (bi_S ? bi_O))))))))
121  | t0A ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
122         (bi_S ? (bi_S ? bi_O)))))))))
123  | t0B ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
124         (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))
125  | t0C ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
126         (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))
127  | t0D ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
128         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))
129  | t0E ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
130         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))
131  | t0F ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
132         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))
133  | t10 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
134         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
135          bi_O)))))))))))))))
136  | t11 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
137         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
138         (bi_S ? bi_O))))))))))))))))
139  | t12 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
140         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
141         (bi_S ? (bi_S ? bi_O)))))))))))))))))
142  | t13 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
143         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
144         (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))
145  | t14 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
146         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
147         (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))))))))
148  | t15 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
149         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
150         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))))
151  | t16 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
152         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
153         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))))))))))
154  | t17 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
155         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
156         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))))))
157  | t18 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
158         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
159         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
160          bi_O)))))))))))))))))))))))
161  | t19 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
162         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
163         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
164         (bi_S ? bi_O))))))))))))))))))))))))
165  | t1A ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
166         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
167         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
168         (bi_S ? (bi_S ? bi_O)))))))))))))))))))))))))
169  | t1B ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
170         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
171         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
172         (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))))))))))
173  | t1C ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
174         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
175         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
176         (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))))))))))))))))
177  | t1D ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
178         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
179         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
180         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))))))))))))
181  | t1E ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
182         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
183         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
184         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))))))))))))))))))
185  | t1F ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
186         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
187         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
188         (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))))))))))))))
189  ].