]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/ng_assembly/freescale/oct.ma
freescale porting, work in progress
[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / 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: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
19 (*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
20 (*                                                                        *)
21 (* ********************************************************************** *)
22
23 include "freescale/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 (* operatore = *)
40 ndefinition eq_oct ≝
41 λn1,n2:oct.
42  match n1 with
43   [ o0 ⇒ match n2 with [ o0 ⇒ true  | _ ⇒ false ]
44   | o1 ⇒ match n2 with [ o1 ⇒ true  | _ ⇒ false ] 
45   | o2 ⇒ match n2 with [ o2 ⇒ true  | _ ⇒ false ]
46   | o3 ⇒ match n2 with [ o3 ⇒ true  | _ ⇒ false ] 
47   | o4 ⇒ match n2 with [ o4 ⇒ true  | _ ⇒ false ]  
48   | o5 ⇒ match n2 with [ o5 ⇒ true  | _ ⇒ false ] 
49   | o6 ⇒ match n2 with [ o6 ⇒ true  | _ ⇒ false ]  
50   | o7 ⇒ match n2 with [ o7 ⇒ true  | _ ⇒ false ] 
51   ].
52
53 (* iteratore sugli ottali *)
54 ndefinition forall_oct ≝ λP.
55  P o0 ⊗ P o1 ⊗ P o2 ⊗ P o3 ⊗ P o4 ⊗ P o5 ⊗ P o6 ⊗ P o7.
56
57 (* operatore successore *)
58 ndefinition succ_oct ≝
59 λn.match n with
60  [ o0 ⇒ o1 | o1 ⇒ o2 | o2 ⇒ o3 | o3 ⇒ o4 | o4 ⇒ o5 | o5 ⇒ o6 | o6 ⇒ o7 | o7 ⇒ o0 ].
61
62 (* ottali ricorsivi *)
63 ninductive rec_oct : oct → Type ≝
64   oc_O : rec_oct o0
65 | oc_S : ∀n.rec_oct n → rec_oct (succ_oct n).
66
67 (* ottali → ottali ricorsivi *)
68 ndefinition oct_to_recoct ≝
69 λn.match n return λx.rec_oct x with
70  [ o0 ⇒ oc_O
71  | o1 ⇒ oc_S ? oc_O
72  | o2 ⇒ oc_S ? (oc_S ? oc_O)
73  | o3 ⇒ oc_S ? (oc_S ? (oc_S ? oc_O))
74  | o4 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O)))
75  | o5 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O))))
76  | o6 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O)))))
77  | o7 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O))))))
78  ].