helm/software/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