]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/apps_2/models/tm_props.ma
update in delayed-updating
[helm.git] / 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 ].