matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.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 "apps_2/functional/rtm.ma".
  16
  17 (* REDUCTION AND TYPE MACHINE ***********************************************)
  18
  19 (* transitions *)
  20 inductive rtm_step: relation rtm ≝
  21 | rtm_ldrop : ∀G,u,E,I,t,D,V,S,i.
  22               rtm_step (mk_rtm G u (E. ④{I} {t, D, V}) S (#(i + 1)))
  23                        (mk_rtm G u E S (#i))
  24 | rtm_ldelta: ∀G,u,E,t,D,V,S.
  25               rtm_step (mk_rtm G u (E. ④{Abbr} {t, D, V}) S (#0))
  26                        (mk_rtm G u D S V)
  27 | rtm_ltype : ∀G,u,E,t,D,V,S.
  28               rtm_step (mk_rtm G u (E. ④{Abst} {t, D, V}) S (#0))
  29                        (mk_rtm G u D S V)
  30 | rtm_gdrop : ∀G,I,V,u,E,S,p. p < |G| →
  31               rtm_step (mk_rtm (G. ⓑ{I} V) u E S (§p))
  32                        (mk_rtm G u E S (§p))
  33 | rtm_gdelta: ∀G,V,u,E,S,p. p = |G| →
  34               rtm_step (mk_rtm (G. ⓓV) u E S (§p))
  35                        (mk_rtm G u E S V)
  36 | rtm_gtype : ∀G,V,u,E,S,p. p = |G| →
  37               rtm_step (mk_rtm (G. ⓛV) u E S (§p))
  38                        (mk_rtm G u E S V)
  39 | rtm_eps   : ∀G,u,E,S,W,T.
  40               rtm_step (mk_rtm G u E S (ⓝW. T))
  41                        (mk_rtm G u E S T)
  42 | rtm_appl  : ∀G,u,E,S,V,T.
  43               rtm_step (mk_rtm G u E S (ⓐV. T))
  44                        (mk_rtm G u E ({E, V} @ S) T)
  45 | rtm_beta  : ∀G,u,E,D,V,S,W,T.
  46               rtm_step (mk_rtm G u E ({D, V} @ S) (+ⓛW. T))
  47                        (mk_rtm G u (E. ④{Abbr} {u, D, V}) S T)
  48 | rtm_push  : ∀G,u,E,W,T.
  49               rtm_step (mk_rtm G u E (⟠) (+ⓛW. T))
  50                        (mk_rtm G (u + 1) (E. ④{Abst} {u, E, W}) (⟠) T)
  51 | rtm_theta : ∀G,u,E,S,V,T.
  52               rtm_step (mk_rtm G u E S (+ⓓV. T))
  53                        (mk_rtm G u (E. ④{Abbr} {u, E, V}) S T)
  54 .
  55
  56 interpretation "sequential reduction (RTM)"
  57    'SRed O1 O2 = (rtm_step O1 O2).