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 "labelled_sequential_computation.ma".
16 include "labelled_hap_reduction.ma".
18 (* KASHIMA'S "HAP" COMPUTATION (LABELLED MULTISTEP) *************************)
20 (* Note: this is the "head in application" computation of:
21 R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000).
23 definition lhap: pseq → relation term ≝ lstar … lhap1.
25 interpretation "labelled 'hap' computation"
26 'HApStar M p N = (lhap p M N).
28 notation "hvbox( M break ⓗ⇀* [ term 46 p ] break term 46 N )"
29 non associative with precedence 45
30 for @{ 'HApStar $M $p $N }.
32 lemma lhap_step_rc: ∀p,M1,M2. M1 ⓗ⇀[p] M2 → M1 ⓗ⇀*[p::◊] M2.
36 lemma lhap_inv_nil: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → ◊ = s → M1 = M2.
37 /2 width=5 by lstar_inv_nil/
40 lemma lhap_inv_cons: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → ∀q,r. q::r = s →
41 ∃∃M. M1 ⓗ⇀[q] M & M ⓗ⇀*[r] M2.
42 /2 width=3 by lstar_inv_cons/
45 lemma lhap_inv_step_rc: ∀p,M1,M2. M1 ⓗ⇀*[p::◊] M2 → M1 ⓗ⇀[p] M2.
46 /2 width=1 by lstar_inv_step/
49 lemma lhap_lift: ∀s. liftable (lhap s).
53 lemma lhap_inv_lift: ∀s. deliftable_sn (lhap s).
54 /3 width=3 by lstar_deliftable_sn, lhap1_inv_lift/
57 lemma lhap_dsubst: ∀s. dsubstable_dx (lhap s).
61 theorem lhap_mono: ∀s. singlevalued … (lhap s).
62 /3 width=7 by lstar_singlevalued, lhap1_mono/
65 theorem lhap_trans: ∀s1,M1,M. M1 ⓗ⇀*[s1] M →
66 ∀s2,M2. M ⓗ⇀*[s2] M2 → M1 ⓗ⇀*[s1@s2] M2.
67 /2 width=3 by lstar_trans/
70 lemma lhap_appl: ∀s,B,A1,A2. A1 ⓗ⇀*[s] A2 → @B.A1 ⓗ⇀*[dx:::s] @B.A2.
71 #s #B #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /3 width=3/
74 lemma head_lsreds_lhap: ∀s,M1,M2. M1 ⇀*[s] M2 → is_head s → M1 ⓗ⇀*[s] M2.
75 #s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 //
76 #a #s #M1 #M #HM1 #_ #IHM2 * /3 width=3/
79 lemma lhap_inv_head: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → is_head s.
80 #s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 //
81 #p #s #M1 #M #HM1 #_ #IHM2
82 lapply (lhap1_inv_head … HM1) -HM1 /2 width=1/
85 lemma lhap_inv_lsreds: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → M1 ⇀*[s] M2.
86 #s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 //
87 #p #s #M1 #M #HM1 #_ #IHM2
88 lapply (lhap1_inv_lsred … HM1) -HM1 /2 width=3/