matita/matita/contribs/lambdadelta/ground_2/steps/rtc_shift.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 "ground_2/xoa/ex_5_4.ma".
  16 include "ground_2/notation/functions/updownarrowstar_1.ma".
  17 include "ground_2/steps/rtc_isrt.ma".
  18
  19 (* RT-TRANSITION COUNTER ****************************************************)
  20
  21 definition shift (c:rtc): rtc ≝ match c with
  22 [ mk_rtc ri rs ti ts ⇒ 〈ri∨rs,0,ti∨ts,0〉 ].
  23
  24 interpretation "shift (rtc)"
  25    'UpDownArrowStar c = (shift c).
  26
  27 (* Basic properties *********************************************************)
  28
  29 lemma shift_rew: ∀ri,rs,ti,ts. 〈ri∨rs,0,ti∨ts,0〉 = ↕*〈ri,rs,ti,ts〉.
  30 normalize //
  31 qed.
  32
  33 lemma shift_O: 𝟘𝟘 = ↕*𝟘𝟘.
  34 // qed.
  35
  36 (* Basic inversion properties ***********************************************)
  37
  38 lemma shift_inv_dx: ∀ri,rs,ti,ts,c. 〈ri,rs,ti,ts〉 = ↕*c →
  39                     ∃∃ri0,rs0,ti0,ts0. (ri0∨rs0) = ri & 0 = rs & (ti0∨ts0) = ti & 0 = ts &
  40                                        〈ri0,rs0,ti0,ts0〉 = c.
  41 #ri #rs #ti #ts * #ri0 #rs0 #ti0 #ts0 <shift_rew #H destruct
  42 /2 width=7 by ex5_4_intro/
  43 qed-.
  44
  45 (* Properties with test for costrained rt-transition counter ****************)
  46
  47 lemma isr_shift: ∀c. 𝐑𝐓❪0,c❫ → 𝐑𝐓❪0,↕*c❫.
  48 #c * #ri #rs #H destruct /2 width=3 by ex1_2_intro/
  49 qed.
  50
  51 (* Inversion properties with test for costrained rt-counter *****************)
  52
  53 lemma isrt_inv_shift: ∀n,c. 𝐑𝐓❪n,↕*c❫ → 𝐑𝐓❪0,c❫ ∧ 0 = n.
  54 #n #c * #ri #rs #H
  55 elim (shift_inv_dx … H) -H #rt0 #rs0 #ti0 #ts0 #_ #_ #H1 #H2 #H3
  56 elim (max_inv_O3 … H1) -H1 /3 width=3 by ex1_2_intro, conj/
  57 qed-.
  58
  59 lemma isr_inv_shift: ∀c. 𝐑𝐓❪0,↕*c❫ → 𝐑𝐓❪0,c❫.
  60 #c #H elim (isrt_inv_shift … H) -H //
  61 qed-.