1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basic_2/notation/relations/predtywhead_4.ma".
16 include "static_2/syntax/item_sh.ma".
17 include "static_2/syntax/lenv.ma".
18 include "static_2/syntax/genv.ma".
20 (* WHD NORMAL TERMS FOR UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ****)
22 inductive cwhx (h:sh) (G:genv): relation2 lenv term ≝
23 | cwhx_sort: ∀L,s. cwhx h G L (⋆s)
24 | cwhx_abst: ∀p,L,W,T. cwhx h G L (ⓛ{p}W.T)
25 | cwhx_ldef: ∀L,V,T. cwhx h G (L.ⓓV) T → cwhx h G L (-ⓓV.T)
29 "whd normality for unbound context-sensitive parallel rt-transition (term)"
30 'PRedTyWHead h G L T = (cwhx h G L T).
32 (* Basic inversion lemmas ***************************************************)
34 fact cwhx_inv_lref_aux (h) (G):
35 ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ →
38 [ #L #s #i #H destruct
39 | #p #L #W #T #i #H destruct
40 | #L #V #T #_ #i #H destruct
44 lemma cwhx_inv_lref (h) (G):
45 ∀L,i. ⦃G,L⦄ ⊢ ⬈[h] 𝐖𝐇⦃#i⦄ → ⊥.
46 /2 width=7 by cwhx_inv_lref_aux/ qed-.
48 fact cwhx_inv_gref_aux (h) (G):
49 ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ →
52 [ #L #s #l #H destruct
53 | #p #L #W #T #l #H destruct
54 | #L #V #T #_ #l #H destruct
58 lemma cwhx_inv_gref (h) (G):
59 ∀L,l. ⦃G,L⦄ ⊢ ⬈[h] 𝐖𝐇⦃§l⦄ → ⊥.
60 /2 width=7 by cwhx_inv_gref_aux/ qed-.
62 fact cwhx_inv_abbr_aux (h) (G):
63 ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ →
66 [ #L #s #X1 #X2 #H destruct
67 | #p #L #W #T #X1 #X2 #H destruct
68 | #L #V #T #_ #X1 #X2 #H destruct
72 lemma cwhx_inv_abbr (h) (G):
73 ∀Y,V,T. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃+ⓓV.T⦄ → ⊥.
74 /2 width=8 by cwhx_inv_abbr_aux/ qed-.
76 fact cwhx_inv_ldef_aux (h) (G):
77 ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ →
78 ∀V,T. X = -ⓓV.T → ⦃G,Y.ⓓV⦄ ⊢ ⬈[h] 𝐖𝐇⦃T⦄.
80 [ #L #s #X1 #X2 #H destruct
81 | #p #L #W #T #X1 #X2 #H destruct
82 | #L #V #T #HT #X1 #X2 #H destruct //
86 lemma cwhx_inv_ldef (h) (G):
87 ∀Y,V,T. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃-ⓓV.T⦄ → ⦃G,Y.ⓓV⦄ ⊢ ⬈[h] 𝐖𝐇⦃T⦄.
88 /2 width=3 by cwhx_inv_ldef_aux/ qed-.
90 fact cwhx_inv_appl_aux (h) (G):
91 ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ →
94 [ #L #s #X1 #X2 #H destruct
95 | #p #L #W #T #X1 #X2 #H destruct
96 | #L #V #T #_ #X1 #X2 #H destruct
100 lemma cwhx_inv_appl (h) (G):
101 ∀Y,V,T. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃ⓐV.T⦄ → ⊥.
102 /2 width=8 by cwhx_inv_appl_aux/ qed-.
104 fact cwhx_inv_cast_aux (h) (G):
105 ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ →
108 [ #L #s #X1 #X2 #H destruct
109 | #p #L #W #T #X1 #X2 #H destruct
110 | #L #V #T #_ #X1 #X2 #H destruct
114 lemma cwhx_inv_cast (h) (G):
115 ∀Y,U,T. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃ⓝU.T⦄ → ⊥.
116 /2 width=8 by cwhx_inv_cast_aux/ qed-.