1(*  Title:      HOL/Proofs/Lambda/Standardization.thy
2    Author:     Stefan Berghofer
3    Copyright   2005 TU Muenchen
4*)
5
6section \<open>Standardization\<close>
7
8theory Standardization
9imports NormalForm
10begin
11
12text \<open>
13Based on lecture notes by Ralph Matthes @{cite "Matthes-ESSLLI2000"},
14original proof idea due to Ralph Loader @{cite Loader1998}.
15\<close>
16
17
18subsection \<open>Standard reduction relation\<close>
19
20declare listrel_mono [mono_set]
21
22inductive
23  sred :: "dB \<Rightarrow> dB \<Rightarrow> bool"  (infixl "\<rightarrow>\<^sub>s" 50)
24  and sredlist :: "dB list \<Rightarrow> dB list \<Rightarrow> bool"  (infixl "[\<rightarrow>\<^sub>s]" 50)
25where
26  "s [\<rightarrow>\<^sub>s] t \<equiv> listrelp (\<rightarrow>\<^sub>s) s t"
27| Var: "rs [\<rightarrow>\<^sub>s] rs' \<Longrightarrow> Var x \<degree>\<degree> rs \<rightarrow>\<^sub>s Var x \<degree>\<degree> rs'"
28| Abs: "r \<rightarrow>\<^sub>s r' \<Longrightarrow> ss [\<rightarrow>\<^sub>s] ss' \<Longrightarrow> Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> ss'"
29| Beta: "r[s/0] \<degree>\<degree> ss \<rightarrow>\<^sub>s t \<Longrightarrow> Abs r \<degree> s \<degree>\<degree> ss \<rightarrow>\<^sub>s t"
30
31lemma refl_listrelp: "\<forall>x\<in>set xs. R x x \<Longrightarrow> listrelp R xs xs"
32  by (induct xs) (auto intro: listrelp.intros)
33
34lemma refl_sred: "t \<rightarrow>\<^sub>s t"
35  by (induct t rule: Apps_dB_induct) (auto intro: refl_listrelp sred.intros)
36
37lemma refl_sreds: "ts [\<rightarrow>\<^sub>s] ts"
38  by (simp add: refl_sred refl_listrelp)
39
40lemma listrelp_conj1: "listrelp (\<lambda>x y. R x y \<and> S x y) x y \<Longrightarrow> listrelp R x y"
41  by (erule listrelp.induct) (auto intro: listrelp.intros)
42
43lemma listrelp_conj2: "listrelp (\<lambda>x y. R x y \<and> S x y) x y \<Longrightarrow> listrelp S x y"
44  by (erule listrelp.induct) (auto intro: listrelp.intros)
45
46lemma listrelp_app:
47  assumes xsys: "listrelp R xs ys"
48  shows "listrelp R xs' ys' \<Longrightarrow> listrelp R (xs @ xs') (ys @ ys')" using xsys
49  by (induct arbitrary: xs' ys') (auto intro: listrelp.intros)
50
51lemma lemma1:
52  assumes r: "r \<rightarrow>\<^sub>s r'" and s: "s \<rightarrow>\<^sub>s s'"
53  shows "r \<degree> s \<rightarrow>\<^sub>s r' \<degree> s'" using r
54proof induct
55  case (Var rs rs' x)
56  then have "rs [\<rightarrow>\<^sub>s] rs'" by (rule listrelp_conj1)
57  moreover have "[s] [\<rightarrow>\<^sub>s] [s']" by (iprover intro: s listrelp.intros)
58  ultimately have "rs @ [s] [\<rightarrow>\<^sub>s] rs' @ [s']" by (rule listrelp_app)
59  hence "Var x \<degree>\<degree> (rs @ [s]) \<rightarrow>\<^sub>s Var x \<degree>\<degree> (rs' @ [s'])" by (rule sred.Var)
60  thus ?case by (simp only: app_last)
61next
62  case (Abs r r' ss ss')
63  from Abs(3) have "ss [\<rightarrow>\<^sub>s] ss'" by (rule listrelp_conj1)
64  moreover have "[s] [\<rightarrow>\<^sub>s] [s']" by (iprover intro: s listrelp.intros)
65  ultimately have "ss @ [s] [\<rightarrow>\<^sub>s] ss' @ [s']" by (rule listrelp_app)
66  with \<open>r \<rightarrow>\<^sub>s r'\<close> have "Abs r \<degree>\<degree> (ss @ [s]) \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> (ss' @ [s'])"
67    by (rule sred.Abs)
68  thus ?case by (simp only: app_last)
69next
70  case (Beta r u ss t)
71  hence "r[u/0] \<degree>\<degree> (ss @ [s]) \<rightarrow>\<^sub>s t \<degree> s'" by (simp only: app_last)
72  hence "Abs r \<degree> u \<degree>\<degree> (ss @ [s]) \<rightarrow>\<^sub>s t \<degree> s'" by (rule sred.Beta)
73  thus ?case by (simp only: app_last)
74qed
75
76lemma lemma1':
77  assumes ts: "ts [\<rightarrow>\<^sub>s] ts'"
78  shows "r \<rightarrow>\<^sub>s r' \<Longrightarrow> r \<degree>\<degree> ts \<rightarrow>\<^sub>s r' \<degree>\<degree> ts'" using ts
79  by (induct arbitrary: r r') (auto intro: lemma1)
80
81lemma lemma2_1:
82  assumes beta: "t \<rightarrow>\<^sub>\<beta> u"
83  shows "t \<rightarrow>\<^sub>s u" using beta
84proof induct
85  case (beta s t)
86  have "Abs s \<degree> t \<degree>\<degree> [] \<rightarrow>\<^sub>s s[t/0] \<degree>\<degree> []" by (iprover intro: sred.Beta refl_sred)
87  thus ?case by simp
88next
89  case (appL s t u)
90  thus ?case by (iprover intro: lemma1 refl_sred)
91next
92  case (appR s t u)
93  thus ?case by (iprover intro: lemma1 refl_sred)
94next
95  case (abs s t)
96  hence "Abs s \<degree>\<degree> [] \<rightarrow>\<^sub>s Abs t \<degree>\<degree> []" by (iprover intro: sred.Abs listrelp.Nil)
97  thus ?case by simp
98qed
99
100lemma listrelp_betas:
101  assumes ts: "listrelp (\<rightarrow>\<^sub>\<beta>\<^sup>*) ts ts'"
102  shows "\<And>t t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> t \<degree>\<degree> ts \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<degree>\<degree> ts'" using ts
103  by induct auto
104
105lemma lemma2_2:
106  assumes t: "t \<rightarrow>\<^sub>s u"
107  shows "t \<rightarrow>\<^sub>\<beta>\<^sup>* u" using t
108  by induct (auto dest: listrelp_conj2
109    intro: listrelp_betas apps_preserves_beta converse_rtranclp_into_rtranclp)
110
111lemma sred_lift:
112  assumes s: "s \<rightarrow>\<^sub>s t"
113  shows "lift s i \<rightarrow>\<^sub>s lift t i" using s
114proof (induct arbitrary: i)
115  case (Var rs rs' x)
116  hence "map (\<lambda>t. lift t i) rs [\<rightarrow>\<^sub>s] map (\<lambda>t. lift t i) rs'"
117    by induct (auto intro: listrelp.intros)
118  thus ?case by (cases "x < i") (auto intro: sred.Var)
119next
120  case (Abs r r' ss ss')
121  from Abs(3) have "map (\<lambda>t. lift t i) ss [\<rightarrow>\<^sub>s] map (\<lambda>t. lift t i) ss'"
122    by induct (auto intro: listrelp.intros)
123  thus ?case by (auto intro: sred.Abs Abs)
124next
125  case (Beta r s ss t)
126  thus ?case by (auto intro: sred.Beta)
127qed
128
129lemma lemma3:
130  assumes r: "r \<rightarrow>\<^sub>s r'"
131  shows "s \<rightarrow>\<^sub>s s' \<Longrightarrow> r[s/x] \<rightarrow>\<^sub>s r'[s'/x]" using r
132proof (induct arbitrary: s s' x)
133  case (Var rs rs' y)
134  hence "map (\<lambda>t. t[s/x]) rs [\<rightarrow>\<^sub>s] map (\<lambda>t. t[s'/x]) rs'"
135    by induct (auto intro: listrelp.intros Var)
136  moreover have "Var y[s/x] \<rightarrow>\<^sub>s Var y[s'/x]"
137  proof (cases "y < x")
138    case True thus ?thesis by simp (rule refl_sred)
139  next
140    case False
141    thus ?thesis
142      by (cases "y = x") (auto simp add: Var intro: refl_sred)
143  qed
144  ultimately show ?case by simp (rule lemma1')
145next
146  case (Abs r r' ss ss')
147  from Abs(4) have "lift s 0 \<rightarrow>\<^sub>s lift s' 0" by (rule sred_lift)
148  hence "r[lift s 0/Suc x] \<rightarrow>\<^sub>s r'[lift s' 0/Suc x]" by (fast intro: Abs.hyps)
149  moreover from Abs(3) have "map (\<lambda>t. t[s/x]) ss [\<rightarrow>\<^sub>s] map (\<lambda>t. t[s'/x]) ss'"
150    by induct (auto intro: listrelp.intros Abs)
151  ultimately show ?case by simp (rule sred.Abs)
152next
153  case (Beta r u ss t)
154  thus ?case by (auto simp add: subst_subst intro: sred.Beta)
155qed
156
157lemma lemma4_aux:
158  assumes rs: "listrelp (\<lambda>t u. t \<rightarrow>\<^sub>s u \<and> (\<forall>r. u \<rightarrow>\<^sub>\<beta> r \<longrightarrow> t \<rightarrow>\<^sub>s r)) rs rs'"
159  shows "rs' => ss \<Longrightarrow> rs [\<rightarrow>\<^sub>s] ss" using rs
160proof (induct arbitrary: ss)
161  case Nil
162  thus ?case by cases (auto intro: listrelp.Nil)
163next
164  case (Cons x y xs ys)
165  note Cons' = Cons
166  show ?case
167  proof (cases ss)
168    case Nil with Cons show ?thesis by simp
169  next
170    case (Cons y' ys')
171    hence ss: "ss = y' # ys'" by simp
172    from Cons Cons' have "y \<rightarrow>\<^sub>\<beta> y' \<and> ys' = ys \<or> y' = y \<and> ys => ys'" by simp
173    hence "x # xs [\<rightarrow>\<^sub>s] y' # ys'"
174    proof
175      assume H: "y \<rightarrow>\<^sub>\<beta> y' \<and> ys' = ys"
176      with Cons' have "x \<rightarrow>\<^sub>s y'" by blast
177      moreover from Cons' have "xs [\<rightarrow>\<^sub>s] ys" by (iprover dest: listrelp_conj1)
178      ultimately have "x # xs [\<rightarrow>\<^sub>s] y' # ys" by (rule listrelp.Cons)
179      with H show ?thesis by simp
180    next
181      assume H: "y' = y \<and> ys => ys'"
182      with Cons' have "x \<rightarrow>\<^sub>s y'" by blast
183      moreover from H have "xs [\<rightarrow>\<^sub>s] ys'" by (blast intro: Cons')
184      ultimately show ?thesis by (rule listrelp.Cons)
185    qed
186    with ss show ?thesis by simp
187  qed
188qed
189
190lemma lemma4:
191  assumes r: "r \<rightarrow>\<^sub>s r'"
192  shows "r' \<rightarrow>\<^sub>\<beta> r'' \<Longrightarrow> r \<rightarrow>\<^sub>s r''" using r
193proof (induct arbitrary: r'')
194  case (Var rs rs' x)
195  then obtain ss where rs: "rs' => ss" and r'': "r'' = Var x \<degree>\<degree> ss"
196    by (blast dest: head_Var_reduction)
197  from Var(1) rs have "rs [\<rightarrow>\<^sub>s] ss" by (rule lemma4_aux)
198  hence "Var x \<degree>\<degree> rs \<rightarrow>\<^sub>s Var x \<degree>\<degree> ss" by (rule sred.Var)
199  with r'' show ?case by simp
200next
201  case (Abs r r' ss ss')
202  from \<open>Abs r' \<degree>\<degree> ss' \<rightarrow>\<^sub>\<beta> r''\<close> show ?case
203  proof
204    fix s
205    assume r'': "r'' = s \<degree>\<degree> ss'"
206    assume "Abs r' \<rightarrow>\<^sub>\<beta> s"
207    then obtain r''' where s: "s = Abs r'''" and r''': "r' \<rightarrow>\<^sub>\<beta> r'''" by cases auto
208    from r''' have "r \<rightarrow>\<^sub>s r'''" by (blast intro: Abs)
209    moreover from Abs have "ss [\<rightarrow>\<^sub>s] ss'" by (iprover dest: listrelp_conj1)
210    ultimately have "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s Abs r''' \<degree>\<degree> ss'" by (rule sred.Abs)
211    with r'' s show "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s r''" by simp
212  next
213    fix rs'
214    assume "ss' => rs'"
215    with Abs(3) have "ss [\<rightarrow>\<^sub>s] rs'" by (rule lemma4_aux)
216    with \<open>r \<rightarrow>\<^sub>s r'\<close> have "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> rs'" by (rule sred.Abs)
217    moreover assume "r'' = Abs r' \<degree>\<degree> rs'"
218    ultimately show "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s r''" by simp
219  next
220    fix t u' us'
221    assume "ss' = u' # us'"
222    with Abs(3) obtain u us where
223      ss: "ss = u # us" and u: "u \<rightarrow>\<^sub>s u'" and us: "us [\<rightarrow>\<^sub>s] us'"
224      by cases (auto dest!: listrelp_conj1)
225    have "r[u/0] \<rightarrow>\<^sub>s r'[u'/0]" using Abs(1) and u by (rule lemma3)
226    with us have "r[u/0] \<degree>\<degree> us \<rightarrow>\<^sub>s r'[u'/0] \<degree>\<degree> us'" by (rule lemma1')
227    hence "Abs r \<degree> u \<degree>\<degree> us \<rightarrow>\<^sub>s r'[u'/0] \<degree>\<degree> us'" by (rule sred.Beta)
228    moreover assume "Abs r' = Abs t" and "r'' = t[u'/0] \<degree>\<degree> us'"
229    ultimately show "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s r''" using ss by simp
230  qed
231next
232  case (Beta r s ss t)
233  show ?case
234    by (rule sred.Beta) (rule Beta)+
235qed
236
237lemma rtrancl_beta_sred:
238  assumes r: "r \<rightarrow>\<^sub>\<beta>\<^sup>* r'"
239  shows "r \<rightarrow>\<^sub>s r'" using r
240  by induct (iprover intro: refl_sred lemma4)+
241
242
243subsection \<open>Leftmost reduction and weakly normalizing terms\<close>
244
245inductive
246  lred :: "dB \<Rightarrow> dB \<Rightarrow> bool"  (infixl "\<rightarrow>\<^sub>l" 50)
247  and lredlist :: "dB list \<Rightarrow> dB list \<Rightarrow> bool"  (infixl "[\<rightarrow>\<^sub>l]" 50)
248where
249  "s [\<rightarrow>\<^sub>l] t \<equiv> listrelp (\<rightarrow>\<^sub>l) s t"
250| Var: "rs [\<rightarrow>\<^sub>l] rs' \<Longrightarrow> Var x \<degree>\<degree> rs \<rightarrow>\<^sub>l Var x \<degree>\<degree> rs'"
251| Abs: "r \<rightarrow>\<^sub>l r' \<Longrightarrow> Abs r \<rightarrow>\<^sub>l Abs r'"
252| Beta: "r[s/0] \<degree>\<degree> ss \<rightarrow>\<^sub>l t \<Longrightarrow> Abs r \<degree> s \<degree>\<degree> ss \<rightarrow>\<^sub>l t"
253
254lemma lred_imp_sred:
255  assumes lred: "s \<rightarrow>\<^sub>l t"
256  shows "s \<rightarrow>\<^sub>s t" using lred
257proof induct
258  case (Var rs rs' x)
259  then have "rs [\<rightarrow>\<^sub>s] rs'"
260    by induct (iprover intro: listrelp.intros)+
261  then show ?case by (rule sred.Var)
262next
263  case (Abs r r')
264  from \<open>r \<rightarrow>\<^sub>s r'\<close>
265  have "Abs r \<degree>\<degree> [] \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> []" using listrelp.Nil
266    by (rule sred.Abs)
267  then show ?case by simp
268next
269  case (Beta r s ss t)
270  from \<open>r[s/0] \<degree>\<degree> ss \<rightarrow>\<^sub>s t\<close>
271  show ?case by (rule sred.Beta)
272qed
273
274inductive WN :: "dB => bool"
275  where
276    Var: "listsp WN rs \<Longrightarrow> WN (Var n \<degree>\<degree> rs)"
277  | Lambda: "WN r \<Longrightarrow> WN (Abs r)"
278  | Beta: "WN ((r[s/0]) \<degree>\<degree> ss) \<Longrightarrow> WN ((Abs r \<degree> s) \<degree>\<degree> ss)"
279
280lemma listrelp_imp_listsp1:
281  assumes H: "listrelp (\<lambda>x y. P x) xs ys"
282  shows "listsp P xs" using H
283  by induct auto
284
285lemma listrelp_imp_listsp2:
286  assumes H: "listrelp (\<lambda>x y. P y) xs ys"
287  shows "listsp P ys" using H
288  by induct auto
289
290lemma lemma5:
291  assumes lred: "r \<rightarrow>\<^sub>l r'"
292  shows "WN r" and "NF r'" using lred
293  by induct
294    (iprover dest: listrelp_conj1 listrelp_conj2
295     listrelp_imp_listsp1 listrelp_imp_listsp2 intro: WN.intros
296     NF.intros [simplified listall_listsp_eq])+
297
298lemma lemma6:
299  assumes wn: "WN r"
300  shows "\<exists>r'. r \<rightarrow>\<^sub>l r'" using wn
301proof induct
302  case (Var rs n)
303  then have "\<exists>rs'. rs [\<rightarrow>\<^sub>l] rs'"
304    by induct (iprover intro: listrelp.intros)+
305  then show ?case by (iprover intro: lred.Var)
306qed (iprover intro: lred.intros)+
307
308lemma lemma7:
309  assumes r: "r \<rightarrow>\<^sub>s r'"
310  shows "NF r' \<Longrightarrow> r \<rightarrow>\<^sub>l r'" using r
311proof induct
312  case (Var rs rs' x)
313  from \<open>NF (Var x \<degree>\<degree> rs')\<close> have "listall NF rs'"
314    by cases simp_all
315  with Var(1) have "rs [\<rightarrow>\<^sub>l] rs'"
316  proof induct
317    case Nil
318    show ?case by (rule listrelp.Nil)
319  next
320    case (Cons x y xs ys)
321    hence "x \<rightarrow>\<^sub>l y" and "xs [\<rightarrow>\<^sub>l] ys" by simp_all
322    thus ?case by (rule listrelp.Cons)
323  qed
324  thus ?case by (rule lred.Var)
325next
326  case (Abs r r' ss ss')
327  from \<open>NF (Abs r' \<degree>\<degree> ss')\<close>
328  have ss': "ss' = []" by (rule Abs_NF)
329  from Abs(3) have ss: "ss = []" using ss'
330    by cases simp_all
331  from ss' Abs have "NF (Abs r')" by simp
332  hence "NF r'" by cases simp_all
333  with Abs have "r \<rightarrow>\<^sub>l r'" by simp
334  hence "Abs r \<rightarrow>\<^sub>l Abs r'" by (rule lred.Abs)
335  with ss ss' show ?case by simp
336next
337  case (Beta r s ss t)
338  hence "r[s/0] \<degree>\<degree> ss \<rightarrow>\<^sub>l t" by simp
339  thus ?case by (rule lred.Beta)
340qed
341
342lemma WN_eq: "WN t = (\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t')"
343proof
344  assume "WN t"
345  then have "\<exists>t'. t \<rightarrow>\<^sub>l t'" by (rule lemma6)
346  then obtain t' where t': "t \<rightarrow>\<^sub>l t'" ..
347  then have NF: "NF t'" by (rule lemma5)
348  from t' have "t \<rightarrow>\<^sub>s t'" by (rule lred_imp_sred)
349  then have "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" by (rule lemma2_2)
350  with NF show "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" by iprover
351next
352  assume "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'"
353  then obtain t' where t': "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and NF: "NF t'"
354    by iprover
355  from t' have "t \<rightarrow>\<^sub>s t'" by (rule rtrancl_beta_sred)
356  then have "t \<rightarrow>\<^sub>l t'" using NF by (rule lemma7)
357  then show "WN t" by (rule lemma5)
358qed
359
360end
361