helm/software/matita/contribs/dama/dama/models/list_support.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 include "list/list.ma".
  16
  17 interpretation "list nth" 'nth = (nth _).
  18 interpretation "list nth" 'nth_appl l d i = (nth _ l d i).
  19 notation "'nth'" with precedence 90 for @{'nth}.
  20 notation < "'nth' \nbsp term 90 l \nbsp term 90 d \nbsp term 90 i"
  21 with precedence 69 for @{'nth_appl $l $d $i}.
  22
  23 definition make_list ≝
  24   λA:Type.λdef:nat→A.
  25     let rec make_list (n:nat) on n ≝
  26       match n with [ O ⇒ nil ? | S m ⇒ def m :: make_list m]
  27     in make_list.
  28
  29 interpretation "'mk_list' appl" 'mk_list_appl f n = (make_list _ f n).
  30 interpretation "'mk_list'" 'mk_list = (make_list _).
  31 notation "'mk_list'" with precedence 90 for @{'mk_list}.
  32 notation < "'mk_list' \nbsp term 90 f \nbsp term 90 n"
  33 with precedence 69 for @{'mk_list_appl $f $n}.
  34
  35 notation "'len'" with precedence 90 for @{'len}.
  36 interpretation "len" 'len = (length _).
  37 notation < "'len' \nbsp term 90 l" with precedence 69 for @{'len_appl $l}.
  38 interpretation "len appl" 'len_appl l = (length _ l).
  39
  40 lemma len_mk_list : ∀T:Type.∀f:nat→T.∀n.len (mk_list f n) = n.
  41 intros; elim n; [reflexivity] simplify; rewrite > H; reflexivity;
  42 qed.
  43