helm/software/matita/contribs/ng_assembly/common/list.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Ultima modifica: 05/08/2009                                          *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "common/theory.ma".
  24
  25 (* *************** *)
  26 (* LISTE GENERICHE *)
  27 (* *************** *)
  28
  29 ninductive list (A:Type) : Type ≝
  30   nil: list A
  31 | cons: A → list A → list A.
  32
  33 nlet rec append A (l1: list A) l2 on l1 ≝
  34  match l1 with
  35   [ nil ⇒ l2
  36   | (cons hd tl) ⇒ cons A hd (append A tl l2) ].
  37
  38 notation "hvbox(hd break :: tl)"
  39   right associative with precedence 47
  40   for @{'cons $hd $tl}.
  41
  42 notation "[ list0 x sep ; ]"
  43   non associative with precedence 90
  44   for ${fold right @'nil rec acc @{'cons $x $acc}}.
  45
  46 notation "hvbox(l1 break @ l2)"
  47   right associative with precedence 47
  48   for @{'append $l1 $l2 }.
  49
  50 interpretation "nil" 'nil = (nil ?).
  51 interpretation "cons" 'cons hd tl = (cons ? hd tl).
  52 interpretation "append" 'append l1 l2 = (append ? l1 l2).
  53
  54 (* ************** *)
  55 (* NON-EMPTY LIST *)
  56 (* ************** *)
  57
  58 (* lista non vuota *)
  59 ninductive ne_list (A:Type) : Type ≝
  60   | ne_nil: A → ne_list A
  61   | ne_cons: A → ne_list A → ne_list A.
  62
  63 (* append *)
  64 nlet rec ne_append (A:Type) (l1,l2:ne_list A) on l1 ≝
  65  match l1 with
  66   [ ne_nil hd ⇒ ne_cons A hd l2
  67   | ne_cons hd tl ⇒ ne_cons A hd (ne_append A tl l2) ].
  68
  69 notation "hvbox(hd break §§ tl)"
  70   right associative with precedence 46
  71   for @{'ne_cons $hd $tl}.
  72
  73 (* \laquo \raquo *)
  74 notation "« list0 x sep ; break £ y break »"
  75   non associative with precedence 90
  76   for ${fold right @{'ne_nil $y } rec acc @{'ne_cons $x $acc}}.
  77
  78 notation "hvbox(l1 break & l2)"
  79   right associative with precedence 47
  80   for @{'ne_append $l1 $l2 }.
  81
  82 interpretation "ne_nil" 'ne_nil hd = (ne_nil ? hd).
  83 interpretation "ne_cons" 'ne_cons hd tl = (ne_cons ? hd tl).
  84 interpretation "ne_append" 'ne_append l1 l2 = (ne_append ? l1 l2).