]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/tests/reduction_old_preamble.ma
splitting files
[helm.git] / matita / matita / tests / reduction_old_preamble.ma
1
2 inductive exadecim : Type ≝
3   x0: exadecim
4 | x1: exadecim
5 | x2: exadecim
6 | x3: exadecim
7 | x4: exadecim
8 | x5: exadecim
9 | x6: exadecim
10 | x7: exadecim
11 | x8: exadecim
12 | x9: exadecim
13 | xA: exadecim
14 | xB: exadecim
15 | xC: exadecim
16 | xD: exadecim
17 | xE: exadecim
18 | xF: exadecim.
19
20 inductive bool : Type ≝ true :bool | false : bool .
21
22 (* operatore = *)
23 definition eq_ex ≝
24 λe1,e2:exadecim.
25  match e1 with
26   [ x0 ⇒ match e2 with [ x0 ⇒ true  | _ ⇒ false ]
27   | x1 ⇒ match e2 with [ x1 ⇒ true  | _ ⇒ false ]
28   | x2 ⇒ match e2 with [ x2 ⇒ true  | _ ⇒ false ]
29   | x3 ⇒ match e2 with [ x3 ⇒ true  | _ ⇒ false ]
30   | x4 ⇒ match e2 with [ x4 ⇒ true  | _ ⇒ false ]
31   | x5 ⇒ match e2 with [ x5 ⇒ true  | _ ⇒ false ]
32   | x6 ⇒ match e2 with [ x6 ⇒ true  | _ ⇒ false ]
33   | x7 ⇒ match e2 with [ x7 ⇒ true  | _ ⇒ false ]
34   | x8 ⇒ match e2 with [ x8 ⇒ true  | _ ⇒ false ]
35   | x9 ⇒ match e2 with [ x9 ⇒ true  | _ ⇒ false ]
36   | xA ⇒ match e2 with [ xA ⇒ true  | _ ⇒ false ]
37   | xB ⇒ match e2 with [ xB ⇒ true  | _ ⇒ false ]
38   | xC ⇒ match e2 with [ xC ⇒ true  | _ ⇒ false ]
39   | xD ⇒ match e2 with [ xD ⇒ true  | _ ⇒ false ]
40   | xE ⇒ match e2 with [ xE ⇒ true  | _ ⇒ false ]
41   | xF ⇒ match e2 with [ xF ⇒ true  | _ ⇒ false ]
42   ].
43
44 definition succ_ex ≝
45 λe:exadecim.
46  match e with
47   [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
48   | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ].
49
50
51 record byte8 : Type ≝
52  {
53  b8h: exadecim;
54  b8l: exadecim
55  }.
56  
57 notation "〈x,y〉" non associative with precedence 80
58  for @{ 'mk_byte8 $x $y }.
59 interpretation "mk_byte8" 'mk_byte8 x y = (mk_byte8 x y).
60
61 definition andb ≝ λa,b.match a with [ true ⇒ b | _ ⇒ false ].
62
63 definition eq_b8 ≝ λb1,b2:byte8.andb (eq_ex (b8h b1) (b8h b2))  (eq_ex (b8l b1) (b8l b2)).
64 definition succ_b8 ≝
65 λb:byte8.match eq_ex (b8l b) xF with
66  [ true ⇒ mk_byte8 (succ_ex (b8h b)) (succ_ex (b8l b))
67  | false ⇒ mk_byte8 (b8h b) (succ_ex (b8l b)) ]. 
68
69 record word16 : Type ≝
70  {
71  w16h: byte8;
72  w16l: byte8
73  }.
74
75 (* \langle \rangle *)
76 notation "〈x:y〉" non associative with precedence 80
77  for @{ 'mk_word16 $x $y }.
78 interpretation "mk_word16" 'mk_word16 x y = (mk_word16 x y).
79
80
81
82 definition succ_w16 ≝
83 λw:word16.
84   match eq_b8 (w16l w) (mk_byte8 xF xF) with
85  [ true ⇒ mk_word16 (succ_b8 (w16h w)) (succ_b8 (w16l w))
86  | false ⇒ mk_word16 (w16h w) (succ_b8 (w16l w)) ].
87
88 inductive eq (A:Type) (a:A) : A → Prop ≝ refl_eq : eq A a a.
89
90 interpretation "aa" 'eq t a b = (eq t a b).
91
92