matita/matita/contribs/lambdadelta/apps_2/models/tm_props.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 "basic_2/rt_equivalence/cpcs_drops.ma".
  16 include "basic_2/rt_equivalence/cpcs_cpcs.ma".
  17 include "apps_2/functional/mf_lifts.ma".
  18 include "apps_2/functional/mf_cpr.ma".
  19 include "apps_2/models/model_props.ma".
  20 include "apps_2/models/tm_vpush.ma".
  21
  22 (* TERM MODEL ***************************************************************)
  23
  24 lemma cpcs_repl (h) (G) (L): replace_2 … (cpcs h G L) (cpcs h G L) (cpcs h G L).
  25 /3 width=5 by cpcs_trans, cpcs_sym/ qed-.
  26 (*
  27 lemma pippo (h) (gv) (lv) (T): ■[gv,lv]T = ⟦T⟧{TM h}[gv,lv].
  28 // qed.
  29
  30 lemma tm_mi (h) (gv1) (gv2) (lv1) (lv2) (p) (W) (T):
  31             ⟦W⟧[gv1,lv1] ≗{TM h} ⟦W⟧[gv2,lv2] →
  32             (∀d. ⟦T⟧[gv1,⫯[0←d]lv1] ≗ ⟦T⟧[gv2,⫯[0←d]lv2]) →
  33             ⟦ⓛ[p]W.T⟧[gv1,lv1] ≗ ⟦ⓛ[p]W.T⟧[gv2,lv2].
  34 #h #gv1 #gv2 #lv1 #lv2 #p #W #T #HW #HT
  35 >tm_ti_bind >tm_ti_bind
  36 @(cpcs_bind1 … HW)
  37
  38
  39
  40 <pippo in ⊢ (????%?); >(mf_comp … T) in ⊢ (????%?);
  41 [2: @tm_vpush_vlift_join_O
  42
  43 <pippo in ⊢ (????%?);
  44
  45 lapply (HT (#0)) -HT #HT
  46 *)
  47
  48 lemma tm_md (h) (p) (gv) (lv) (V) (T):
  49             ⓓ[p]V.⟦T⟧{TM h}[⇡[0]gv,⇡[0←#0]lv] ≗{TM h} V⊕{TM h}[p]⟦T⟧{TM h}[gv,⫯{TM h}[0←V]lv].
  50 #h #p #gv #lv #V #T
  51 >tm_co_rw >(mf_lifts_basic_SO_dx T 0)
  52 >(mf_comp … T) in ⊢ (???%);
  53 [2: @tm_vpush_vlift_join_O |4: @exteq_refl |3,5: skip ]
  54 /6 width=4 by mf_delta_drops, cpcs_bind1, cpc_cpcs, drops_refl, or_introl/
  55 qed.
  56
  57 lemma tm_mz (h) (V) (T): V ⊕[Ⓣ] T ≗{TM h} T.
  58 /4 width=3 by cpc_cpcs, cpm_zeta, or_introl/ qed.
  59
  60 lemma tm_me (h) (gv) (lv) (U) (T):
  61             ⟦ⓝU.T⟧[gv,lv] ≗{TM h} ⟦T⟧[gv,lv].
  62 /4 width=1 by cpc_cpcs, cpm_eps, or_introl/ qed.
  63
  64 lemma tm_mb (h) (p) (gv) (lv) (d) (W) (T):
  65             d@⟦ⓛ[p]W.T⟧[gv,lv] ≗{TM h} d⊕[p]⟦T⟧[gv,⫯[0←d]lv].
  66 #h #p #gv #lv #d #W #T
  67 @cpcs_repl [5: @tm_md |4: /4 width=2 by cpc_cpcs, cpm_beta, or_intror/ |1,2: skip ]
  68 /5 width=1 by cpcs_bind1, cpc_cpcs, cpm_eps, or_introl/
  69 qed.
  70
  71 lemma ti_mh (h) (p) (d1) (d2) (d3):
  72             d1@(d2⊕[p]d3) ≗{TM h} d2⊕[p](d1@d3).
  73 /4 width=3 by cpc_cpcs, cpm_theta, or_introl/ qed.
  74
  75 definition is_tm (h): is_model (TM h) ≝ mk_is_model …. //
  76 [ @cpcs_repl
  77 | #p #V1 #V2 #HV #T1 #T2 #HT
  78   @(cpcs_bind1 … HV) @(cpcs_lifts_bi … HT)
  79   /2 width=5 by drops_drop/
  80 | #V1 #V2 #HV #T1 #T2 #HT
  81   @(cpcs_flat … HV … HT)
  82 |
  83 ].