43 "Var i -e> t" |
43 "Var i -e> t" |
44 |
44 |
45 |
45 |
46 subsection "Properties of eta, subst and free" |
46 subsection "Properties of eta, subst and free" |
47 |
47 |
48 lemma subst_not_free [rule_format, simp]: |
48 lemma subst_not_free [simp]: "\<not> free s i \<Longrightarrow> s[t/i] = s[u/i]" |
49 "\<forall>i t u. \<not> free s i --> s[t/i] = s[u/i]" |
49 by (induct s fixing: i t u) (simp_all add: subst_Var) |
50 apply (induct_tac s) |
|
51 apply (simp_all add: subst_Var) |
|
52 done |
|
53 |
50 |
54 lemma free_lift [simp]: |
51 lemma free_lift [simp]: |
55 "\<forall>i k. free (lift t k) i = |
52 "free (lift t k) i = (i < k \<and> free t i \<or> k < i \<and> free t (i - 1))" |
56 (i < k \<and> free t i \<or> k < i \<and> free t (i - 1))" |
53 apply (induct t fixing: i k) |
57 apply (induct_tac t) |
|
58 apply (auto cong: conj_cong) |
54 apply (auto cong: conj_cong) |
59 apply arith |
55 apply arith |
60 done |
56 done |
61 |
57 |
62 lemma free_subst [simp]: |
58 lemma free_subst [simp]: |
63 "\<forall>i k t. free (s[t/k]) i = |
59 "free (s[t/k]) i = |
64 (free s k \<and> free t i \<or> free s (if i < k then i else i + 1))" |
60 (free s k \<and> free t i \<or> free s (if i < k then i else i + 1))" |
65 apply (induct_tac s) |
61 apply (induct s fixing: i k t) |
66 prefer 2 |
62 prefer 2 |
67 apply simp |
63 apply simp |
68 apply blast |
64 apply blast |
69 prefer 2 |
65 prefer 2 |
70 apply simp |
66 apply simp |
71 apply (simp add: diff_Suc subst_Var split: nat.split) |
67 apply (simp add: diff_Suc subst_Var split: nat.split) |
72 done |
68 done |
73 |
69 |
74 lemma free_eta [rule_format]: |
70 lemma free_eta: "s -e> t ==> (!!i. free t i = free s i)" |
75 "s -e> t ==> \<forall>i. free t i = free s i" |
71 by (induct set: eta) (simp_all cong: conj_cong) |
76 apply (erule eta.induct) |
|
77 apply (simp_all cong: conj_cong) |
|
78 done |
|
79 |
72 |
80 lemma not_free_eta: |
73 lemma not_free_eta: |
81 "[| s -e> t; \<not> free s i |] ==> \<not> free t i" |
74 "[| s -e> t; \<not> free s i |] ==> \<not> free t i" |
82 apply (simp add: free_eta) |
75 by (simp add: free_eta) |
83 done |
76 |
84 |
77 lemma eta_subst [simp]: |
85 lemma eta_subst [rule_format, simp]: |
78 "s -e> t ==> (!!u i. s[u/i] -e> t[u/i])" |
86 "s -e> t ==> \<forall>u i. s[u/i] -e> t[u/i]" |
79 by (induct set: eta) (simp_all add: subst_subst [symmetric]) |
87 apply (erule eta.induct) |
80 |
88 apply (simp_all add: subst_subst [symmetric]) |
81 theorem lift_subst_dummy: "\<not> free s i \<Longrightarrow> lift (s[dummy/i]) i = s" |
89 done |
82 by (induct s fixing: i dummy) simp_all |
90 |
|
91 theorem lift_subst_dummy: "\<And>i dummy. \<not> free s i \<Longrightarrow> lift (s[dummy/i]) i = s" |
|
92 by (induct s) simp_all |
|
93 |
83 |
94 |
84 |
95 subsection "Confluence of eta" |
85 subsection "Confluence of eta" |
96 |
86 |
97 lemma square_eta: "square eta eta (eta^=) (eta^=)" |
87 lemma square_eta: "square eta eta (eta^=) (eta^=)" |
112 |
102 |
113 |
103 |
114 subsection "Congruence rules for eta*" |
104 subsection "Congruence rules for eta*" |
115 |
105 |
116 lemma rtrancl_eta_Abs: "s -e>> s' ==> Abs s -e>> Abs s'" |
106 lemma rtrancl_eta_Abs: "s -e>> s' ==> Abs s -e>> Abs s'" |
117 apply (erule rtrancl_induct) |
107 by (induct set: rtrancl) |
118 apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+ |
108 (blast intro: rtrancl_refl rtrancl_into_rtrancl)+ |
119 done |
|
120 |
109 |
121 lemma rtrancl_eta_AppL: "s -e>> s' ==> s \<degree> t -e>> s' \<degree> t" |
110 lemma rtrancl_eta_AppL: "s -e>> s' ==> s \<degree> t -e>> s' \<degree> t" |
122 apply (erule rtrancl_induct) |
111 by (induct set: rtrancl) |
123 apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+ |
112 (blast intro: rtrancl_refl rtrancl_into_rtrancl)+ |
124 done |
|
125 |
113 |
126 lemma rtrancl_eta_AppR: "t -e>> t' ==> s \<degree> t -e>> s \<degree> t'" |
114 lemma rtrancl_eta_AppR: "t -e>> t' ==> s \<degree> t -e>> s \<degree> t'" |
127 apply (erule rtrancl_induct) |
115 by (induct set: rtrancl) (blast intro: rtrancl_refl rtrancl_into_rtrancl)+ |
128 apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+ |
|
129 done |
|
130 |
116 |
131 lemma rtrancl_eta_App: |
117 lemma rtrancl_eta_App: |
132 "[| s -e>> s'; t -e>> t' |] ==> s \<degree> t -e>> s' \<degree> t'" |
118 "[| s -e>> s'; t -e>> t' |] ==> s \<degree> t -e>> s' \<degree> t'" |
133 apply (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtrancl_trans) |
119 by (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtrancl_trans) |
134 done |
|
135 |
120 |
136 |
121 |
137 subsection "Commutation of beta and eta" |
122 subsection "Commutation of beta and eta" |
138 |
123 |
139 lemma free_beta [rule_format]: |
124 lemma free_beta: |
140 "s -> t ==> \<forall>i. free t i --> free s i" |
125 "s -> t ==> (!!i. free t i \<Longrightarrow> free s i)" |
141 apply (erule beta.induct) |
126 by (induct set: beta) auto |
142 apply simp_all |
127 |
143 done |
128 lemma beta_subst [intro]: "s -> t ==> (!!u i. s[u/i] -> t[u/i])" |
144 |
129 by (induct set: beta) (simp_all add: subst_subst [symmetric]) |
145 lemma beta_subst [rule_format, intro]: |
130 |
146 "s -> t ==> \<forall>u i. s[u/i] -> t[u/i]" |
131 lemma subst_Var_Suc [simp]: "t[Var i/i] = t[Var(i)/i + 1]" |
147 apply (erule beta.induct) |
132 by (induct t fixing: i) (auto elim!: linorder_neqE simp: subst_Var) |
148 apply (simp_all add: subst_subst [symmetric]) |
133 |
149 done |
134 lemma eta_lift [simp]: "s -e> t ==> (!!i. lift s i -e> lift t i)" |
150 |
135 by (induct set: eta) simp_all |
151 lemma subst_Var_Suc [simp]: "\<forall>i. t[Var i/i] = t[Var(i)/i + 1]" |
136 |
152 apply (induct_tac t) |
137 lemma rtrancl_eta_subst: "s -e> t \<Longrightarrow> u[s/i] -e>> u[t/i]" |
153 apply (auto elim!: linorder_neqE simp: subst_Var) |
138 apply (induct u fixing: s t i) |
154 done |
|
155 |
|
156 lemma eta_lift [rule_format, simp]: |
|
157 "s -e> t ==> \<forall>i. lift s i -e> lift t i" |
|
158 apply (erule eta.induct) |
|
159 apply simp_all |
|
160 done |
|
161 |
|
162 lemma rtrancl_eta_subst [rule_format]: |
|
163 "\<forall>s t i. s -e> t --> u[s/i] -e>> u[t/i]" |
|
164 apply (induct_tac u) |
|
165 apply (simp_all add: subst_Var) |
139 apply (simp_all add: subst_Var) |
166 apply (blast) |
140 apply blast |
167 apply (blast intro: rtrancl_eta_App) |
141 apply (blast intro: rtrancl_eta_App) |
168 apply (blast intro!: rtrancl_eta_Abs eta_lift) |
142 apply (blast intro!: rtrancl_eta_Abs eta_lift) |
169 done |
143 done |
170 |
144 |
171 lemma square_beta_eta: "square beta eta (eta^*) (beta^=)" |
145 lemma square_beta_eta: "square beta eta (eta^*) (beta^=)" |
189 |
163 |
190 subsection "Implicit definition of eta" |
164 subsection "Implicit definition of eta" |
191 |
165 |
192 text {* @{term "Abs (lift s 0 \<degree> Var 0) -e> s"} *} |
166 text {* @{term "Abs (lift s 0 \<degree> Var 0) -e> s"} *} |
193 |
167 |
194 lemma not_free_iff_lifted [rule_format]: |
168 lemma not_free_iff_lifted: |
195 "\<forall>i. (\<not> free s i) = (\<exists>t. s = lift t i)" |
169 "(\<not> free s i) = (\<exists>t. s = lift t i)" |
196 apply (induct_tac s) |
170 apply (induct s fixing: i) |
197 apply simp |
171 apply simp |
198 apply clarify |
|
199 apply (rule iffI) |
172 apply (rule iffI) |
200 apply (erule linorder_neqE) |
173 apply (erule linorder_neqE) |
201 apply (rule_tac x = "Var nat" in exI) |
174 apply (rule_tac x = "Var nat" in exI) |
202 apply simp |
175 apply simp |
203 apply (rule_tac x = "Var (nat - 1)" in exI) |
176 apply (rule_tac x = "Var (nat - 1)" in exI) |
268 var [simp, intro]: "Var x \<Rightarrow>\<^sub>\<eta> Var x" |
238 var [simp, intro]: "Var x \<Rightarrow>\<^sub>\<eta> Var x" |
269 eta [simp, intro]: "\<not> free s 0 \<Longrightarrow> s \<Rightarrow>\<^sub>\<eta> s'\<Longrightarrow> Abs (s \<degree> Var 0) \<Rightarrow>\<^sub>\<eta> s'[dummy/0]" |
239 eta [simp, intro]: "\<not> free s 0 \<Longrightarrow> s \<Rightarrow>\<^sub>\<eta> s'\<Longrightarrow> Abs (s \<degree> Var 0) \<Rightarrow>\<^sub>\<eta> s'[dummy/0]" |
270 app [simp, intro]: "s \<Rightarrow>\<^sub>\<eta> s' \<Longrightarrow> t \<Rightarrow>\<^sub>\<eta> t' \<Longrightarrow> s \<degree> t \<Rightarrow>\<^sub>\<eta> s' \<degree> t'" |
240 app [simp, intro]: "s \<Rightarrow>\<^sub>\<eta> s' \<Longrightarrow> t \<Rightarrow>\<^sub>\<eta> t' \<Longrightarrow> s \<degree> t \<Rightarrow>\<^sub>\<eta> s' \<degree> t'" |
271 abs [simp, intro]: "s \<Rightarrow>\<^sub>\<eta> t \<Longrightarrow> Abs s \<Rightarrow>\<^sub>\<eta> Abs t" |
241 abs [simp, intro]: "s \<Rightarrow>\<^sub>\<eta> t \<Longrightarrow> Abs s \<Rightarrow>\<^sub>\<eta> Abs t" |
272 |
242 |
273 lemma free_par_eta [simp]: assumes eta: "s \<Rightarrow>\<^sub>\<eta> t" |
243 lemma free_par_eta [simp]: |
274 shows "\<And>i. free t i = free s i" using eta |
244 assumes eta: "s \<Rightarrow>\<^sub>\<eta> t" |
275 by induct (simp_all cong: conj_cong) |
245 shows "free t i = free s i" using eta |
|
246 by (induct fixing: i) (simp_all cong: conj_cong) |
276 |
247 |
277 lemma par_eta_refl [simp]: "t \<Rightarrow>\<^sub>\<eta> t" |
248 lemma par_eta_refl [simp]: "t \<Rightarrow>\<^sub>\<eta> t" |
278 by (induct t) simp_all |
249 by (induct t) simp_all |
279 |
250 |
280 lemma par_eta_lift [simp]: |
251 lemma par_eta_lift [simp]: |
281 assumes eta: "s \<Rightarrow>\<^sub>\<eta> t" |
252 assumes eta: "s \<Rightarrow>\<^sub>\<eta> t" |
282 shows "\<And>i. lift s i \<Rightarrow>\<^sub>\<eta> lift t i" using eta |
253 shows "lift s i \<Rightarrow>\<^sub>\<eta> lift t i" using eta |
283 by induct simp_all |
254 by (induct fixing: i) simp_all |
284 |
255 |
285 lemma par_eta_subst [simp]: |
256 lemma par_eta_subst [simp]: |
286 assumes eta: "s \<Rightarrow>\<^sub>\<eta> t" |
257 assumes eta: "s \<Rightarrow>\<^sub>\<eta> t" |
287 shows "\<And>u u' i. u \<Rightarrow>\<^sub>\<eta> u' \<Longrightarrow> s[u/i] \<Rightarrow>\<^sub>\<eta> t[u'/i]" using eta |
258 shows "u \<Rightarrow>\<^sub>\<eta> u' \<Longrightarrow> s[u/i] \<Rightarrow>\<^sub>\<eta> t[u'/i]" using eta |
288 by induct (simp_all add: subst_subst [symmetric] subst_Var) |
259 by (induct fixing: u u' i) (simp_all add: subst_subst [symmetric] subst_Var) |
289 |
260 |
290 theorem eta_subset_par_eta: "eta \<subseteq> par_eta" |
261 theorem eta_subset_par_eta: "eta \<subseteq> par_eta" |
291 apply (rule subsetI) |
262 apply (rule subsetI) |
292 apply clarify |
263 apply clarify |
293 apply (erule eta.induct) |
264 apply (erule eta.induct) |
318 primrec |
289 primrec |
319 eta_expand_0: "eta_expand 0 t = t" |
290 eta_expand_0: "eta_expand 0 t = t" |
320 eta_expand_Suc: "eta_expand (Suc n) t = Abs (lift (eta_expand n t) 0 \<degree> Var 0)" |
291 eta_expand_Suc: "eta_expand (Suc n) t = Abs (lift (eta_expand n t) 0 \<degree> Var 0)" |
321 |
292 |
322 lemma eta_expand_Suc': |
293 lemma eta_expand_Suc': |
323 "\<And>t. eta_expand (Suc n) t = eta_expand n (Abs (lift t 0 \<degree> Var 0))" |
294 "eta_expand (Suc n) t = eta_expand n (Abs (lift t 0 \<degree> Var 0))" |
324 by (induct n) simp_all |
295 by (induct n fixing: t) simp_all |
325 |
296 |
326 theorem lift_eta_expand: "lift (eta_expand k t) i = eta_expand k (lift t i)" |
297 theorem lift_eta_expand: "lift (eta_expand k t) i = eta_expand k (lift t i)" |
327 by (induct k) (simp_all add: lift_lift) |
298 by (induct k) (simp_all add: lift_lift) |
328 |
299 |
329 theorem eta_expand_beta: |
300 theorem eta_expand_beta: |
330 assumes u: "u => u'" |
301 assumes u: "u => u'" |
331 shows "\<And>t t'. t => t' \<Longrightarrow> eta_expand k (Abs t) \<degree> u => t'[u'/0]" |
302 shows "t => t' \<Longrightarrow> eta_expand k (Abs t) \<degree> u => t'[u'/0]" |
332 proof (induct k) |
303 proof (induct k fixing: t t') |
333 case 0 with u show ?case by simp |
304 case 0 with u show ?case by simp |
334 next |
305 next |
335 case (Suc k) |
306 case (Suc k) |
336 hence "Abs (lift t (Suc 0)) \<degree> Var 0 => lift t' (Suc 0)[Var 0/0]" |
307 hence "Abs (lift t (Suc 0)) \<degree> Var 0 => lift t' (Suc 0)[Var 0/0]" |
337 by (blast intro: par_beta_lift) |
308 by (blast intro: par_beta_lift) |
356 |
327 |
357 |
328 |
358 subsection {* Elimination rules for parallel eta reduction *} |
329 subsection {* Elimination rules for parallel eta reduction *} |
359 |
330 |
360 theorem par_eta_elim_app: assumes eta: "t \<Rightarrow>\<^sub>\<eta> u" |
331 theorem par_eta_elim_app: assumes eta: "t \<Rightarrow>\<^sub>\<eta> u" |
361 shows "\<And>u1' u2'. u = u1' \<degree> u2' \<Longrightarrow> |
332 shows "u = u1' \<degree> u2' \<Longrightarrow> |
362 \<exists>u1 u2 k. t = eta_expand k (u1 \<degree> u2) \<and> u1 \<Rightarrow>\<^sub>\<eta> u1' \<and> u2 \<Rightarrow>\<^sub>\<eta> u2'" using eta |
333 \<exists>u1 u2 k. t = eta_expand k (u1 \<degree> u2) \<and> u1 \<Rightarrow>\<^sub>\<eta> u1' \<and> u2 \<Rightarrow>\<^sub>\<eta> u2'" using eta |
363 proof induct |
334 proof (induct fixing: u1' u2') |
364 case (app s s' t t') |
335 case (app s s' t t') |
365 have "s \<degree> t = eta_expand 0 (s \<degree> t)" by simp |
336 have "s \<degree> t = eta_expand 0 (s \<degree> t)" by simp |
366 with app show ?case by blast |
337 with app show ?case by blast |
367 next |
338 next |
368 case (eta dummy s s') |
339 case (eta dummy s s') |
386 next |
357 next |
387 case abs thus ?case by simp |
358 case abs thus ?case by simp |
388 qed |
359 qed |
389 |
360 |
390 theorem par_eta_elim_abs: assumes eta: "t \<Rightarrow>\<^sub>\<eta> t'" |
361 theorem par_eta_elim_abs: assumes eta: "t \<Rightarrow>\<^sub>\<eta> t'" |
391 shows "\<And>u'. t' = Abs u' \<Longrightarrow> |
362 shows "t' = Abs u' \<Longrightarrow> |
392 \<exists>u k. t = eta_expand k (Abs u) \<and> u \<Rightarrow>\<^sub>\<eta> u'" using eta |
363 \<exists>u k. t = eta_expand k (Abs u) \<and> u \<Rightarrow>\<^sub>\<eta> u'" using eta |
393 proof induct |
364 proof (induct fixing: u') |
394 case (abs s t) |
365 case (abs s t) |
395 have "Abs s = eta_expand 0 (Abs s)" by simp |
366 have "Abs s = eta_expand 0 (Abs s)" by simp |
396 with abs show ?case by blast |
367 with abs show ?case by blast |
397 next |
368 next |
398 case (eta dummy s s') |
369 case (eta dummy s s') |
465 by (auto intro: eta_expand_red eta_expand_beta eta_expand_eta par_eta_subst) |
437 by (auto intro: eta_expand_red eta_expand_beta eta_expand_eta par_eta_subst) |
466 qed |
438 qed |
467 qed |
439 qed |
468 |
440 |
469 theorem eta_postponement': assumes eta: "s -e>> t" |
441 theorem eta_postponement': assumes eta: "s -e>> t" |
470 shows "\<And>u. t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' -e>> u" |
442 shows "t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' -e>> u" |
471 using eta [simplified rtrancl_subset |
443 using eta [simplified rtrancl_subset |
472 [OF eta_subset_par_eta par_eta_subset_eta, symmetric]] |
444 [OF eta_subset_par_eta par_eta_subset_eta, symmetric]] |
473 proof induct |
445 proof (induct fixing: u) |
474 case 1 |
446 case 1 |
475 thus ?case by blast |
447 thus ?case by blast |
476 next |
448 next |
477 case (2 s' s'' s''') |
449 case (2 s' s'' s''') |
478 from 2 obtain t' where s': "s' => t'" and t': "t' \<Rightarrow>\<^sub>\<eta> s'''" |
450 from 2 obtain t' where s': "s' => t'" and t': "t' \<Rightarrow>\<^sub>\<eta> s'''" |