1(*  Title:      HOL/Proofs/Lambda/Lambda.thy
2    Author:     Tobias Nipkow
3    Copyright   1995 TU Muenchen
4*)
5
6section \<open>Basic definitions of Lambda-calculus\<close>
7
8theory Lambda
9imports Main
10begin
11
12declare [[syntax_ambiguity_warning = false]]
13
14
15subsection \<open>Lambda-terms in de Bruijn notation and substitution\<close>
16
17datatype dB =
18    Var nat
19  | App dB dB (infixl "\<degree>" 200)
20  | Abs dB
21
22primrec
23  lift :: "[dB, nat] => dB"
24where
25    "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
26  | "lift (s \<degree> t) k = lift s k \<degree> lift t k"
27  | "lift (Abs s) k = Abs (lift s (k + 1))"
28
29primrec
30  subst :: "[dB, dB, nat] => dB"  ("_[_'/_]" [300, 0, 0] 300)
31where (* FIXME base names *)
32    subst_Var: "(Var i)[s/k] =
33      (if k < i then Var (i - 1) else if i = k then s else Var i)"
34  | 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])"
36
37declare subst_Var [simp del]
38
39text \<open>Optimized versions of \<^term>\<open>subst\<close> and \<^term>\<open>lift\<close>.\<close>
40
41primrec
42  liftn :: "[nat, dB, nat] => dB"
43where
44    "liftn n (Var i) k = (if i < k then Var i else Var (i + n))"
45  | "liftn n (s \<degree> t) k = liftn n s k \<degree> liftn n t k"
46  | "liftn n (Abs s) k = Abs (liftn n s (k + 1))"
47
48primrec
49  substn :: "[dB, dB, nat] => dB"
50where
51    "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)"
53  | "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))"
55
56
57subsection \<open>Beta-reduction\<close>
58
59inductive beta :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
60  where
61    beta [simp, intro!]: "Abs s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
62  | appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
63  | appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
64  | abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs s \<rightarrow>\<^sub>\<beta> Abs t"
65
66abbreviation
67  beta_reds :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50) where
68  "s \<rightarrow>\<^sub>\<beta>\<^sup>* t == beta\<^sup>*\<^sup>* s t"
69
70inductive_cases beta_cases [elim!]:
71  "Var i \<rightarrow>\<^sub>\<beta> t"
72  "Abs r \<rightarrow>\<^sub>\<beta> s"
73  "s \<degree> t \<rightarrow>\<^sub>\<beta> u"
74
75declare if_not_P [simp] not_less_eq [simp]
76  \<comment> \<open>don't add \<open>r_into_rtrancl[intro!]\<close>\<close>
77
78
79subsection \<open>Congruence rules\<close>
80
81lemma rtrancl_beta_Abs [intro!]:
82    "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> Abs s \<rightarrow>\<^sub>\<beta>\<^sup>* Abs s'"
83  by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
84
85lemma rtrancl_beta_AppL:
86    "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t"
87  by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
88
89lemma rtrancl_beta_AppR:
90    "t \<rightarrow>\<^sub>\<beta>\<^sup>* t' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s \<degree> t'"
91  by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
92
93lemma rtrancl_beta_App [intro]:
94    "[| s \<rightarrow>\<^sub>\<beta>\<^sup>* s'; t \<rightarrow>\<^sub>\<beta>\<^sup>* t' |] ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'"
95  by (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR intro: rtranclp_trans)
96
97
98subsection \<open>Substitution-lemmas\<close>
99
100lemma subst_eq [simp]: "(Var k)[u/k] = u"
101  by (simp add: subst_Var)
102
103lemma subst_gt [simp]: "i < j ==> (Var j)[u/i] = Var (j - 1)"
104  by (simp add: subst_Var)
105
106lemma subst_lt [simp]: "j < i ==> (Var j)[u/i] = Var j"
107  by (simp add: subst_Var)
108
109lemma lift_lift:
110    "i < k + 1 \<Longrightarrow> lift (lift t i) (Suc k) = lift (lift t k) i"
111  by (induct t arbitrary: i k) auto
112
113lemma lift_subst [simp]:
114    "j < i + 1 \<Longrightarrow> lift (t[s/j]) i = (lift t (i + 1)) [lift s i / j]"
115  by (induct t arbitrary: i j s)
116    (simp_all add: diff_Suc subst_Var lift_lift split: nat.split)
117
118lemma lift_subst_lt:
119    "i < j + 1 \<Longrightarrow> lift (t[s/j]) i = (lift t i) [lift s i / j + 1]"
120  by (induct t arbitrary: i j s) (simp_all add: subst_Var lift_lift)
121
122lemma subst_lift [simp]:
123    "(lift t k)[s/k] = t"
124  by (induct t arbitrary: k s) simp_all
125
126lemma subst_subst:
127    "i < j + 1 \<Longrightarrow> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"
128  by (induct t arbitrary: i j u v)
129    (simp_all add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt
130      split: nat.split)
131
132
133subsection \<open>Equivalence proof for optimized substitution\<close>
134
135lemma liftn_0 [simp]: "liftn 0 t k = t"
136  by (induct t arbitrary: k) (simp_all add: subst_Var)
137
138lemma liftn_lift [simp]: "liftn (Suc n) t k = lift (liftn n t k) k"
139  by (induct t arbitrary: k) (simp_all add: subst_Var)
140
141lemma substn_subst_n [simp]: "substn t s n = t[liftn n s 0 / n]"
142  by (induct t arbitrary: n) (simp_all add: subst_Var)
143
144theorem substn_subst_0: "substn t s 0 = t[s/0]"
145  by simp
146
147
148subsection \<open>Preservation theorems\<close>
149
150text \<open>Not used in Church-Rosser proof, but in Strong
151  Normalization. \medskip\<close>
152
153theorem subst_preserves_beta [simp]:
154    "r \<rightarrow>\<^sub>\<beta> s ==> r[t/i] \<rightarrow>\<^sub>\<beta> s[t/i]"
155  by (induct arbitrary: t i set: beta) (simp_all add: subst_subst [symmetric])
156
157theorem subst_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> r[t/i] \<rightarrow>\<^sub>\<beta>\<^sup>* s[t/i]"
158  apply (induct set: rtranclp)
159   apply (rule rtranclp.rtrancl_refl)
160  apply (erule rtranclp.rtrancl_into_rtrancl)
161  apply (erule subst_preserves_beta)
162  done
163
164theorem lift_preserves_beta [simp]:
165    "r \<rightarrow>\<^sub>\<beta> s ==> lift r i \<rightarrow>\<^sub>\<beta> lift s i"
166  by (induct arbitrary: i set: beta) auto
167
168theorem lift_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> lift r i \<rightarrow>\<^sub>\<beta>\<^sup>* lift s i"
169  apply (induct set: rtranclp)
170   apply (rule rtranclp.rtrancl_refl)
171  apply (erule rtranclp.rtrancl_into_rtrancl)
172  apply (erule lift_preserves_beta)
173  done
174
175theorem subst_preserves_beta2 [simp]: "r \<rightarrow>\<^sub>\<beta> s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
176  apply (induct t arbitrary: r s i)
177    apply (simp add: subst_Var r_into_rtranclp)
178   apply (simp add: rtrancl_beta_App)
179  apply (simp add: rtrancl_beta_Abs)
180  done
181
182theorem subst_preserves_beta2': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
183  apply (induct set: rtranclp)
184   apply (rule rtranclp.rtrancl_refl)
185  apply (erule rtranclp_trans)
186  apply (erule subst_preserves_beta2)
187  done
188
189end
190