11 |
11 |
12 subsection {* Lambda-terms in de Bruijn notation and substitution *} |
12 subsection {* Lambda-terms in de Bruijn notation and substitution *} |
13 |
13 |
14 datatype dB = |
14 datatype dB = |
15 Var nat |
15 Var nat |
16 | App dB dB (infixl "$" 200) |
16 | App dB dB (infixl "\<degree>" 200) |
17 | Abs dB |
17 | Abs dB |
18 |
|
19 syntax (symbols) |
|
20 App :: "dB => dB => dB" (infixl "\<^sub>\<degree>" 200) |
|
21 |
18 |
22 consts |
19 consts |
23 subst :: "[dB, dB, nat] => dB" ("_[_'/_]" [300, 0, 0] 300) |
20 subst :: "[dB, dB, nat] => dB" ("_[_'/_]" [300, 0, 0] 300) |
24 lift :: "[dB, nat] => dB" |
21 lift :: "[dB, nat] => dB" |
25 |
22 |
26 primrec |
23 primrec |
27 "lift (Var i) k = (if i < k then Var i else Var (i + 1))" |
24 "lift (Var i) k = (if i < k then Var i else Var (i + 1))" |
28 "lift (s $ t) k = lift s k $ lift t k" |
25 "lift (s \<degree> t) k = lift s k \<degree> lift t k" |
29 "lift (Abs s) k = Abs (lift s (k + 1))" |
26 "lift (Abs s) k = Abs (lift s (k + 1))" |
30 |
27 |
31 primrec (* FIXME base names *) |
28 primrec (* FIXME base names *) |
32 subst_Var: "(Var i)[s/k] = |
29 subst_Var: "(Var i)[s/k] = |
33 (if k < i then Var (i - 1) else if i = k then s else Var i)" |
30 (if k < i then Var (i - 1) else if i = k then s else Var i)" |
34 subst_App: "(t $ u)[s/k] = t[s/k] $ u[s/k]" |
31 subst_App: "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]" |
35 subst_Abs: "(Abs t)[s/k] = Abs (t[lift s 0 / k+1])" |
32 subst_Abs: "(Abs t)[s/k] = Abs (t[lift s 0 / k+1])" |
36 |
33 |
37 declare subst_Var [simp del] |
34 declare subst_Var [simp del] |
38 |
35 |
39 text {* Optimized versions of @{term subst} and @{term lift}. *} |
36 text {* Optimized versions of @{term subst} and @{term lift}. *} |
42 substn :: "[dB, dB, nat] => dB" |
39 substn :: "[dB, dB, nat] => dB" |
43 liftn :: "[nat, dB, nat] => dB" |
40 liftn :: "[nat, dB, nat] => dB" |
44 |
41 |
45 primrec |
42 primrec |
46 "liftn n (Var i) k = (if i < k then Var i else Var (i + n))" |
43 "liftn n (Var i) k = (if i < k then Var i else Var (i + n))" |
47 "liftn n (s $ t) k = liftn n s k $ liftn n t k" |
44 "liftn n (s \<degree> t) k = liftn n s k \<degree> liftn n t k" |
48 "liftn n (Abs s) k = Abs (liftn n s (k + 1))" |
45 "liftn n (Abs s) k = Abs (liftn n s (k + 1))" |
49 |
46 |
50 primrec |
47 primrec |
51 "substn (Var i) s k = |
48 "substn (Var i) s k = |
52 (if k < i then Var (i - 1) else if i = k then liftn k s 0 else Var i)" |
49 (if k < i then Var (i - 1) else if i = k then liftn k s 0 else Var i)" |
53 "substn (t $ u) s k = substn t s k $ substn u s k" |
50 "substn (t \<degree> u) s k = substn t s k \<degree> substn u s k" |
54 "substn (Abs t) s k = Abs (substn t s (k + 1))" |
51 "substn (Abs t) s k = Abs (substn t s (k + 1))" |
55 |
52 |
56 |
53 |
57 subsection {* Beta-reduction *} |
54 subsection {* Beta-reduction *} |
58 |
55 |
66 "s -> t" == "(s, t) \<in> beta" |
63 "s -> t" == "(s, t) \<in> beta" |
67 "s ->> t" == "(s, t) \<in> beta^*" |
64 "s ->> t" == "(s, t) \<in> beta^*" |
68 |
65 |
69 inductive beta |
66 inductive beta |
70 intros |
67 intros |
71 beta [simp, intro!]: "Abs s $ t -> s[t/0]" |
68 beta [simp, intro!]: "Abs s \<degree> t -> s[t/0]" |
72 appL [simp, intro!]: "s -> t ==> s $ u -> t $ u" |
69 appL [simp, intro!]: "s -> t ==> s \<degree> u -> t \<degree> u" |
73 appR [simp, intro!]: "s -> t ==> u $ s -> u $ t" |
70 appR [simp, intro!]: "s -> t ==> u \<degree> s -> u \<degree> t" |
74 abs [simp, intro!]: "s -> t ==> Abs s -> Abs t" |
71 abs [simp, intro!]: "s -> t ==> Abs s -> Abs t" |
75 |
72 |
76 inductive_cases beta_cases [elim!]: |
73 inductive_cases beta_cases [elim!]: |
77 "Var i -> t" |
74 "Var i -> t" |
78 "Abs r -> s" |
75 "Abs r -> s" |
79 "s $ t -> u" |
76 "s \<degree> t -> u" |
80 |
77 |
81 declare if_not_P [simp] not_less_eq [simp] |
78 declare if_not_P [simp] not_less_eq [simp] |
82 -- {* don't add @{text "r_into_rtrancl[intro!]"} *} |
79 -- {* don't add @{text "r_into_rtrancl[intro!]"} *} |
83 |
80 |
84 |
81 |
89 apply (erule rtrancl_induct) |
86 apply (erule rtrancl_induct) |
90 apply (blast intro: rtrancl_into_rtrancl)+ |
87 apply (blast intro: rtrancl_into_rtrancl)+ |
91 done |
88 done |
92 |
89 |
93 lemma rtrancl_beta_AppL: |
90 lemma rtrancl_beta_AppL: |
94 "s ->> s' ==> s $ t ->> s' $ t" |
91 "s ->> s' ==> s \<degree> t ->> s' \<degree> t" |
95 apply (erule rtrancl_induct) |
92 apply (erule rtrancl_induct) |
96 apply (blast intro: rtrancl_into_rtrancl)+ |
93 apply (blast intro: rtrancl_into_rtrancl)+ |
97 done |
94 done |
98 |
95 |
99 lemma rtrancl_beta_AppR: |
96 lemma rtrancl_beta_AppR: |
100 "t ->> t' ==> s $ t ->> s $ t'" |
97 "t ->> t' ==> s \<degree> t ->> s \<degree> t'" |
101 apply (erule rtrancl_induct) |
98 apply (erule rtrancl_induct) |
102 apply (blast intro: rtrancl_into_rtrancl)+ |
99 apply (blast intro: rtrancl_into_rtrancl)+ |
103 done |
100 done |
104 |
101 |
105 lemma rtrancl_beta_App [intro]: |
102 lemma rtrancl_beta_App [intro]: |
106 "[| s ->> s'; t ->> t' |] ==> s $ t ->> s' $ t'" |
103 "[| s ->> s'; t ->> t' |] ==> s \<degree> t ->> s' \<degree> t'" |
107 apply (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR |
104 apply (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR |
108 intro: rtrancl_trans) |
105 intro: rtrancl_trans) |
109 done |
106 done |
110 |
107 |
111 |
108 |