matita/matita/lib/lambda-delta/syntax/weight.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "lambda-delta/syntax/lenv.ma".
  13
  14 (* WEIGHTS ******************************************************************)
  15
  16 (* the weight of a term *)
  17 let rec tw T ≝ match T with
  18 [ TSort _     ⇒ 1
  19 | TLRef _     ⇒ 1
  20 | TPair _ V T ⇒ tw V + tw T + 1
  21 ].
  22
  23 interpretation "weight (term)" 'Weight T = (tw T).
  24
  25 (* the weight of a local environment *)
  26 let rec lw L ≝ match L with
  27 [ LSort       ⇒ 0
  28 | LPair L _ V ⇒ lw L + #V
  29 ].
  30
  31 interpretation "weight (local environment)" 'Weight L = (lw L).
  32
  33 (* the weight of a closure *)
  34 definition cw: lenv → term → ? ≝ λL,T. #L + #T.
  35
  36 interpretation "weight (closure)" 'Weight L T = (cw L T).
  37
  38 axiom tw_wf_ind: ∀P:term→Prop.
  39                  (∀T2. (∀T1. # T1 < # T2 → P T1) → P T2) →
  40                  ∀T. P T.
  41
  42 axiom cw_wf_ind: ∀P:lenv→term→Prop.
  43                  (∀L2,T2. (∀L1,T1. #[L1,T1] < #[L2,T2] → P L1 T1) → P L2 T2) →
  44                  ∀L,T. P L T.