matita/matita/contribs/lambdadelta/ground_2/steps/rtc_max.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_6_8.ma".
  16 include "ground_2/steps/rtc.ma".
  17
  18 (* RT-TRANSITION COUNTER ****************************************************)
  19
  20 definition max (c1:rtc) (c2:rtc): rtc ≝ match c1 with [
  21    mk_rtc ri1 rs1 ti1 ts1 ⇒ match c2 with [
  22       mk_rtc ri2 rs2 ti2 ts2 ⇒ 〈ri1∨ri2,rs1∨rs2,ti1∨ti2,ts1∨ts2〉
  23    ]
  24 ].
  25
  26 interpretation "maximum (rtc)"
  27    'or c1 c2 = (max c1 c2).
  28
  29 (* Basic properties *********************************************************)
  30
  31 lemma max_rew: ∀ri1,ri2,rs1,rs2,ti1,ti2,ts1,ts2.
  32                  〈ri1∨ri2,rs1∨rs2,ti1∨ti2,ts1∨ts2〉 =
  33                  (〈ri1,rs1,ti1,ts1〉 ∨ 〈ri2,rs2,ti2,ts2〉).
  34 // qed.
  35
  36 lemma max_O_dx: ∀c. c = (c ∨ 𝟘𝟘).
  37 * #ri #rs #ti #ts <max_rew //
  38 qed.
  39
  40 lemma max_idem: ∀c. c = (c ∨ c).
  41 * #ri #rs #ti #ts <max_rew //
  42 qed.
  43
  44 (* Basic inversion properties ***********************************************)
  45
  46 lemma max_inv_dx: ∀ri,rs,ti,ts,c1,c2. 〈ri,rs,ti,ts〉 = (c1 ∨ c2) →
  47                   ∃∃ri1,rs1,ti1,ts1,ri2,rs2,ti2,ts2.
  48                   (ri1∨ri2) = ri & (rs1∨rs2) = rs & (ti1∨ti2) = ti & (ts1∨ts2) = ts &
  49                   〈ri1,rs1,ti1,ts1〉 = c1 & 〈ri2,rs2,ti2,ts2〉 = c2.
  50 #ri #rs #ti #ts * #ri1 #rs1 #ti1 #ts1 * #ri2 #rs2 #ti2 #ts2
  51 <max_rew #H destruct /2 width=14 by ex6_8_intro/
  52 qed-.
  53
  54 (* Main Properties **********************************************************)
  55
  56 theorem max_assoc: associative … max.
  57 * #ri1 #rs1 #ti1 #ts1 * #ri2 #rs2 #ti2 #ts2 * #ri3 #rs3 #ti3 #ts3
  58 <max_rew <max_rew //
  59 qed.