77 fix e T' u i assume uNF: "NF u" and uT: "e \<turnstile> u : T" |
77 fix e T' u i assume uNF: "NF u" and uT: "e \<turnstile> u : T" |
78 { |
78 { |
79 case (App ts x e_ T'_ u_ i_) |
79 case (App ts x e_ T'_ u_ i_) |
80 assume "e\<langle>i:T\<rangle> \<turnstile> Var x \<degree>\<degree> ts : T'" |
80 assume "e\<langle>i:T\<rangle> \<turnstile> Var x \<degree>\<degree> ts : T'" |
81 then obtain Us |
81 then obtain Us |
82 where varT: "e\<langle>i:T\<rangle> \<turnstile> Var x : Us \<Rrightarrow> T'" |
82 where varT: "e\<langle>i:T\<rangle> \<turnstile> Var x : Us \<Rrightarrow> T'" |
83 and argsT: "e\<langle>i:T\<rangle> \<tturnstile> ts : Us" |
83 and argsT: "e\<langle>i:T\<rangle> \<tturnstile> ts : Us" |
84 by (rule var_app_typesE) |
84 by (rule var_app_typesE) |
85 from nat_eq_dec show "\<exists>t'. (Var x \<degree>\<degree> ts)[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" |
85 from nat_eq_dec show "\<exists>t'. (Var x \<degree>\<degree> ts)[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" |
86 proof |
86 proof |
87 assume eq: "x = i" |
87 assume eq: "x = i" |
88 show ?thesis |
88 show ?thesis |
89 proof (cases ts) |
89 proof (cases ts) |
90 case Nil |
90 case Nil |
91 with eq have "(Var x \<degree>\<degree> [])[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* u" by simp |
91 with eq have "(Var x \<degree>\<degree> [])[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* u" by simp |
92 with Nil and uNF show ?thesis by simp iprover |
92 with Nil and uNF show ?thesis by simp iprover |
93 next |
93 next |
94 case (Cons a as) |
94 case (Cons a as) |
95 with argsT obtain T'' Ts where Us: "Us = T'' # Ts" |
95 with argsT obtain T'' Ts where Us: "Us = T'' # Ts" |
96 by (cases Us) (rule FalseE, simp+, erule that) |
96 by (cases Us) (rule FalseE, simp+, erule that) |
97 from varT and Us have varT: "e\<langle>i:T\<rangle> \<turnstile> Var x : T'' \<Rightarrow> Ts \<Rrightarrow> T'" |
97 from varT and Us have varT: "e\<langle>i:T\<rangle> \<turnstile> Var x : T'' \<Rightarrow> Ts \<Rrightarrow> T'" |
98 by simp |
98 by simp |
99 from varT eq have T: "T = T'' \<Rightarrow> Ts \<Rrightarrow> T'" by cases auto |
99 from varT eq have T: "T = T'' \<Rightarrow> Ts \<Rrightarrow> T'" by cases auto |
100 with uT have uT': "e \<turnstile> u : T'' \<Rightarrow> Ts \<Rrightarrow> T'" by simp |
100 with uT have uT': "e \<turnstile> u : T'' \<Rightarrow> Ts \<Rrightarrow> T'" by simp |
101 from argsT Us Cons have argsT': "e\<langle>i:T\<rangle> \<tturnstile> as : Ts" by simp |
101 from argsT Us Cons have argsT': "e\<langle>i:T\<rangle> \<tturnstile> as : Ts" by simp |
102 from argsT Us Cons have argT: "e\<langle>i:T\<rangle> \<turnstile> a : T''" by simp |
102 from argsT Us Cons have argT: "e\<langle>i:T\<rangle> \<turnstile> a : T''" by simp |
103 from argT uT refl have aT: "e \<turnstile> a[u/i] : T''" by (rule subst_lemma) |
103 from argT uT refl have aT: "e \<turnstile> a[u/i] : T''" by (rule subst_lemma) |
104 from App and Cons have "listall ?R as" by simp (iprover dest: listall_conj2) |
104 from App and Cons have "listall ?R as" by simp (iprover dest: listall_conj2) |
105 with lift_preserves_beta' lift_NF uNF uT argsT' |
105 with lift_preserves_beta' lift_NF uNF uT argsT' |
106 have "\<exists>as'. \<forall>j. Var j \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as \<rightarrow>\<^sub>\<beta>\<^sup>* |
106 have "\<exists>as'. \<forall>j. Var j \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as \<rightarrow>\<^sub>\<beta>\<^sup>* |
107 Var j \<degree>\<degree> map (\<lambda>t. lift t 0) as' \<and> |
107 Var j \<degree>\<degree> map (\<lambda>t. lift t 0) as' \<and> |
108 NF (Var j \<degree>\<degree> map (\<lambda>t. lift t 0) as')" by (rule norm_list) |
108 NF (Var j \<degree>\<degree> map (\<lambda>t. lift t 0) as')" by (rule norm_list) |
109 then obtain as' where |
109 then obtain as' where |
110 asred: "Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as \<rightarrow>\<^sub>\<beta>\<^sup>* |
110 asred: "Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as \<rightarrow>\<^sub>\<beta>\<^sup>* |
111 Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as'" |
111 Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as'" |
112 and asNF: "NF (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')" by iprover |
112 and asNF: "NF (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')" by iprover |
113 from App and Cons have "?R a" by simp |
113 from App and Cons have "?R a" by simp |
114 with argT and uNF and uT have "\<exists>a'. a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a' \<and> NF a'" |
114 with argT and uNF and uT have "\<exists>a'. a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a' \<and> NF a'" |
115 by iprover |
115 by iprover |
116 then obtain a' where ared: "a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a'" and aNF: "NF a'" by iprover |
116 then obtain a' where ared: "a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a'" and aNF: "NF a'" by iprover |
117 from uNF have "NF (lift u 0)" by (rule lift_NF) |
117 from uNF have "NF (lift u 0)" by (rule lift_NF) |
118 hence "\<exists>u'. lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u' \<and> NF u'" by (rule app_Var_NF) |
118 hence "\<exists>u'. lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u' \<and> NF u'" by (rule app_Var_NF) |
119 then obtain u' where ured: "lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u'" and u'NF: "NF u'" |
119 then obtain u' where ured: "lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u'" and u'NF: "NF u'" |
120 by iprover |
120 by iprover |
121 from T and u'NF have "\<exists>ua. u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua \<and> NF ua" |
121 from T and u'NF have "\<exists>ua. u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua \<and> NF ua" |
122 proof (rule MI1) |
122 proof (rule MI1) |
123 have "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 \<degree> Var 0 : Ts \<Rrightarrow> T'" |
123 have "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 \<degree> Var 0 : Ts \<Rrightarrow> T'" |
124 proof (rule typing.App) |
124 proof (rule typing.App) |
125 from uT' show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 : T'' \<Rightarrow> Ts \<Rrightarrow> T'" by (rule lift_type) |
125 from uT' show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 : T'' \<Rightarrow> Ts \<Rrightarrow> T'" by (rule lift_type) |
126 show "e\<langle>0:T''\<rangle> \<turnstile> Var 0 : T''" by (rule typing.Var) simp |
126 show "e\<langle>0:T''\<rangle> \<turnstile> Var 0 : T''" by (rule typing.Var) simp |
127 qed |
127 qed |
128 with ured show "e\<langle>0:T''\<rangle> \<turnstile> u' : Ts \<Rrightarrow> T'" by (rule subject_reduction') |
128 with ured show "e\<langle>0:T''\<rangle> \<turnstile> u' : Ts \<Rrightarrow> T'" by (rule subject_reduction') |
129 from ared aT show "e \<turnstile> a' : T''" by (rule subject_reduction') |
129 from ared aT show "e \<turnstile> a' : T''" by (rule subject_reduction') |
130 show "NF a'" by fact |
130 show "NF a'" by fact |
131 qed |
131 qed |
132 then obtain ua where uared: "u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" and uaNF: "NF ua" |
132 then obtain ua where uared: "u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" and uaNF: "NF ua" |
133 by iprover |
133 by iprover |
134 from ared have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* (lift u 0 \<degree> Var 0)[a'/0]" |
134 from ared have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* (lift u 0 \<degree> Var 0)[a'/0]" |
135 by (rule subst_preserves_beta2') |
135 by (rule subst_preserves_beta2') |
136 also from ured have "(lift u 0 \<degree> Var 0)[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* u'[a'/0]" |
136 also from ured have "(lift u 0 \<degree> Var 0)[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* u'[a'/0]" |
137 by (rule subst_preserves_beta') |
137 by (rule subst_preserves_beta') |
138 also note uared |
138 also note uared |
139 finally have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" . |
139 finally have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" . |
140 hence uared': "u \<degree> a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" by simp |
140 hence uared': "u \<degree> a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" by simp |
141 from T asNF _ uaNF have "\<exists>r. (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r \<and> NF r" |
141 from T asNF _ uaNF have "\<exists>r. (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r \<and> NF r" |
142 proof (rule MI2) |
142 proof (rule MI2) |
143 have "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as : T'" |
143 have "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as : T'" |
144 proof (rule list_app_typeI) |
144 proof (rule list_app_typeI) |
145 show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 : Ts \<Rrightarrow> T'" by (rule typing.Var) simp |
145 show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 : Ts \<Rrightarrow> T'" by (rule typing.Var) simp |
146 from uT argsT' have "e \<tturnstile> map (\<lambda>t. t[u/i]) as : Ts" |
146 from uT argsT' have "e \<tturnstile> map (\<lambda>t. t[u/i]) as : Ts" |
147 by (rule substs_lemma) |
147 by (rule substs_lemma) |
148 hence "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> map (\<lambda>t. lift t 0) (map (\<lambda>t. t[u/i]) as) : Ts" |
148 hence "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> map (\<lambda>t. lift t 0) (map (\<lambda>t. t[u/i]) as) : Ts" |
149 by (rule lift_types) |
149 by (rule lift_types) |
150 thus "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> map (\<lambda>t. lift (t[u/i]) 0) as : Ts" |
150 thus "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> map (\<lambda>t. lift (t[u/i]) 0) as : Ts" |
151 by (simp_all add: map_compose [symmetric] o_def) |
151 by (simp_all add: map_compose [symmetric] o_def) |
152 qed |
152 qed |
153 with asred show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as' : T'" |
153 with asred show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as' : T'" |
154 by (rule subject_reduction') |
154 by (rule subject_reduction') |
155 from argT uT refl have "e \<turnstile> a[u/i] : T''" by (rule subst_lemma) |
155 from argT uT refl have "e \<turnstile> a[u/i] : T''" by (rule subst_lemma) |
156 with uT' have "e \<turnstile> u \<degree> a[u/i] : Ts \<Rrightarrow> T'" by (rule typing.App) |
156 with uT' have "e \<turnstile> u \<degree> a[u/i] : Ts \<Rrightarrow> T'" by (rule typing.App) |
157 with uared' show "e \<turnstile> ua : Ts \<Rrightarrow> T'" by (rule subject_reduction') |
157 with uared' show "e \<turnstile> ua : Ts \<Rrightarrow> T'" by (rule subject_reduction') |
158 qed |
158 qed |
159 then obtain r where rred: "(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r" |
159 then obtain r where rred: "(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r" |
160 and rnf: "NF r" by iprover |
160 and rnf: "NF r" by iprover |
161 from asred have |
161 from asred have |
162 "(Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as)[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* |
162 "(Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as)[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* |
163 (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[u \<degree> a[u/i]/0]" |
163 (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[u \<degree> a[u/i]/0]" |
164 by (rule subst_preserves_beta') |
164 by (rule subst_preserves_beta') |
165 also from uared' have "(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* |
165 also from uared' have "(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* |
166 (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0]" by (rule subst_preserves_beta2') |
166 (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0]" by (rule subst_preserves_beta2') |
167 also note rred |
167 also note rred |
168 finally have "(Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as)[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r" . |
168 finally have "(Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as)[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r" . |
169 with rnf Cons eq show ?thesis |
169 with rnf Cons eq show ?thesis |
170 by (simp add: map_compose [symmetric] o_def) iprover |
170 by (simp add: map_compose [symmetric] o_def) iprover |
171 qed |
171 qed |
172 next |
172 next |
173 assume neq: "x \<noteq> i" |
173 assume neq: "x \<noteq> i" |
174 from App have "listall ?R ts" by (iprover dest: listall_conj2) |
174 from App have "listall ?R ts" by (iprover dest: listall_conj2) |
175 with TrueI TrueI uNF uT argsT |
175 with TrueI TrueI uNF uT argsT |
176 have "\<exists>ts'. \<forall>j. Var j \<degree>\<degree> map (\<lambda>t. t[u/i]) ts \<rightarrow>\<^sub>\<beta>\<^sup>* Var j \<degree>\<degree> ts' \<and> |
176 have "\<exists>ts'. \<forall>j. Var j \<degree>\<degree> map (\<lambda>t. t[u/i]) ts \<rightarrow>\<^sub>\<beta>\<^sup>* Var j \<degree>\<degree> ts' \<and> |
177 NF (Var j \<degree>\<degree> ts')" (is "\<exists>ts'. ?ex ts'") |
177 NF (Var j \<degree>\<degree> ts')" (is "\<exists>ts'. ?ex ts'") |
178 by (rule norm_list [of "\<lambda>t. t", simplified]) |
178 by (rule norm_list [of "\<lambda>t. t", simplified]) |
179 then obtain ts' where NF: "?ex ts'" .. |
179 then obtain ts' where NF: "?ex ts'" .. |
180 from nat_le_dec show ?thesis |
180 from nat_le_dec show ?thesis |
181 proof |
181 proof |
182 assume "i < x" |
182 assume "i < x" |
183 with NF show ?thesis by simp iprover |
183 with NF show ?thesis by simp iprover |
184 next |
184 next |
185 assume "\<not> (i < x)" |
185 assume "\<not> (i < x)" |
186 with NF neq show ?thesis by (simp add: subst_Var) iprover |
186 with NF neq show ?thesis by (simp add: subst_Var) iprover |
187 qed |
187 qed |
188 qed |
188 qed |
189 next |
189 next |
190 case (Abs r e_ T'_ u_ i_) |
190 case (Abs r e_ T'_ u_ i_) |
191 assume absT: "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'" |
191 assume absT: "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'" |
192 then obtain R S where "e\<langle>0:R\<rangle>\<langle>Suc i:T\<rangle> \<turnstile> r : S" by (rule abs_typeE) simp |
192 then obtain R S where "e\<langle>0:R\<rangle>\<langle>Suc i:T\<rangle> \<turnstile> r : S" by (rule abs_typeE) simp |
193 moreover have "NF (lift u 0)" using `NF u` by (rule lift_NF) |
193 moreover have "NF (lift u 0)" using `NF u` by (rule lift_NF) |
194 moreover have "e\<langle>0:R\<rangle> \<turnstile> lift u 0 : T" using uT by (rule lift_type) |
194 moreover have "e\<langle>0:R\<rangle> \<turnstile> lift u 0 : T" using uT by (rule lift_type) |
195 ultimately have "\<exists>t'. r[lift u 0/Suc i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" by (rule Abs) |
195 ultimately have "\<exists>t'. r[lift u 0/Suc i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" by (rule Abs) |
196 thus "\<exists>t'. Abs r[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" |
196 thus "\<exists>t'. Abs r[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" |
197 by simp (iprover intro: rtrancl_beta_Abs NF.Abs) |
197 by simp (iprover intro: rtrancl_beta_Abs NF.Abs) |
198 } |
198 } |
199 qed |
199 qed |
200 qed |
200 qed |
201 |
201 |
202 |
202 |