1(* Title: HOL/Proofs/Lambda/Eta.thy 2 Author: Tobias Nipkow and Stefan Berghofer 3 Copyright 1995, 2005 TU Muenchen 4*) 5 6section \<open>Eta-reduction\<close> 7 8theory Eta imports ParRed begin 9 10 11subsection \<open>Definition of eta-reduction and relatives\<close> 12 13primrec 14 free :: "dB => nat => bool" 15where 16 "free (Var j) i = (j = i)" 17 | "free (s \<degree> t) i = (free s i \<or> free t i)" 18 | "free (Abs s) i = free s (i + 1)" 19 20inductive 21 eta :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<eta>" 50) 22where 23 eta [simp, intro]: "\<not> free s 0 ==> Abs (s \<degree> Var 0) \<rightarrow>\<^sub>\<eta> s[dummy/0]" 24 | appL [simp, intro]: "s \<rightarrow>\<^sub>\<eta> t ==> s \<degree> u \<rightarrow>\<^sub>\<eta> t \<degree> u" 25 | appR [simp, intro]: "s \<rightarrow>\<^sub>\<eta> t ==> u \<degree> s \<rightarrow>\<^sub>\<eta> u \<degree> t" 26 | abs [simp, intro]: "s \<rightarrow>\<^sub>\<eta> t ==> Abs s \<rightarrow>\<^sub>\<eta> Abs t" 27 28abbreviation 29 eta_reds :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<eta>\<^sup>*" 50) where 30 "s \<rightarrow>\<^sub>\<eta>\<^sup>* t == eta\<^sup>*\<^sup>* s t" 31 32abbreviation 33 eta_red0 :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<eta>\<^sup>=" 50) where 34 "s \<rightarrow>\<^sub>\<eta>\<^sup>= t == eta\<^sup>=\<^sup>= s t" 35 36inductive_cases eta_cases [elim!]: 37 "Abs s \<rightarrow>\<^sub>\<eta> z" 38 "s \<degree> t \<rightarrow>\<^sub>\<eta> u" 39 "Var i \<rightarrow>\<^sub>\<eta> t" 40 41 42subsection \<open>Properties of \<open>eta\<close>, \<open>subst\<close> and \<open>free\<close>\<close> 43 44lemma subst_not_free [simp]: "\<not> free s i \<Longrightarrow> s[t/i] = s[u/i]" 45 by (induct s arbitrary: i t u) (simp_all add: subst_Var) 46 47lemma free_lift [simp]: 48 "free (lift t k) i = (i < k \<and> free t i \<or> k < i \<and> free t (i - 1))" 49 apply (induct t arbitrary: i k) 50 apply (auto cong: conj_cong) 51 done 52 53lemma free_subst [simp]: 54 "free (s[t/k]) i = 55 (free s k \<and> free t i \<or> free s (if i < k then i else i + 1))" 56 apply (induct s arbitrary: i k t) 57 prefer 2 58 apply simp 59 apply blast 60 prefer 2 61 apply simp 62 apply (simp add: diff_Suc subst_Var split: nat.split) 63 done 64 65lemma free_eta: "s \<rightarrow>\<^sub>\<eta> t ==> free t i = free s i" 66 by (induct arbitrary: i set: eta) (simp_all cong: conj_cong) 67 68lemma not_free_eta: 69 "[| s \<rightarrow>\<^sub>\<eta> t; \<not> free s i |] ==> \<not> free t i" 70 by (simp add: free_eta) 71 72lemma eta_subst [simp]: 73 "s \<rightarrow>\<^sub>\<eta> t ==> s[u/i] \<rightarrow>\<^sub>\<eta> t[u/i]" 74 by (induct arbitrary: u i set: eta) (simp_all add: subst_subst [symmetric]) 75 76theorem lift_subst_dummy: "\<not> free s i \<Longrightarrow> lift (s[dummy/i]) i = s" 77 by (induct s arbitrary: i dummy) simp_all 78 79 80subsection \<open>Confluence of \<open>eta\<close>\<close> 81 82lemma square_eta: "square eta eta (eta\<^sup>=\<^sup>=) (eta\<^sup>=\<^sup>=)" 83 apply (unfold square_def id_def) 84 apply (rule impI [THEN allI [THEN allI]]) 85 apply (erule eta.induct) 86 apply (slowsimp intro: subst_not_free eta_subst free_eta [THEN iffD1]) 87 apply safe 88 prefer 5 89 apply (blast intro!: eta_subst intro: free_eta [THEN iffD1]) 90 apply blast+ 91 done 92 93theorem eta_confluent: "confluent eta" 94 apply (rule square_eta [THEN square_reflcl_confluent]) 95 done 96 97 98subsection \<open>Congruence rules for \<open>eta\<^sup>*\<close>\<close> 99 100lemma rtrancl_eta_Abs: "s \<rightarrow>\<^sub>\<eta>\<^sup>* s' ==> Abs s \<rightarrow>\<^sub>\<eta>\<^sup>* Abs s'" 101 by (induct set: rtranclp) 102 (blast intro: rtranclp.rtrancl_into_rtrancl)+ 103 104lemma rtrancl_eta_AppL: "s \<rightarrow>\<^sub>\<eta>\<^sup>* s' ==> s \<degree> t \<rightarrow>\<^sub>\<eta>\<^sup>* s' \<degree> t" 105 by (induct set: rtranclp) 106 (blast intro: rtranclp.rtrancl_into_rtrancl)+ 107 108lemma rtrancl_eta_AppR: "t \<rightarrow>\<^sub>\<eta>\<^sup>* t' ==> s \<degree> t \<rightarrow>\<^sub>\<eta>\<^sup>* s \<degree> t'" 109 by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+ 110 111lemma rtrancl_eta_App: 112 "[| s \<rightarrow>\<^sub>\<eta>\<^sup>* s'; t \<rightarrow>\<^sub>\<eta>\<^sup>* t' |] ==> s \<degree> t \<rightarrow>\<^sub>\<eta>\<^sup>* s' \<degree> t'" 113 by (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtranclp_trans) 114 115 116subsection \<open>Commutation of \<open>beta\<close> and \<open>eta\<close>\<close> 117 118lemma free_beta: 119 "s \<rightarrow>\<^sub>\<beta> t ==> free t i \<Longrightarrow> free s i" 120 by (induct arbitrary: i set: beta) auto 121 122lemma beta_subst [intro]: "s \<rightarrow>\<^sub>\<beta> t ==> s[u/i] \<rightarrow>\<^sub>\<beta> t[u/i]" 123 by (induct arbitrary: u i set: beta) (simp_all add: subst_subst [symmetric]) 124 125lemma subst_Var_Suc [simp]: "t[Var i/i] = t[Var(i)/i + 1]" 126 by (induct t arbitrary: i) (auto elim!: linorder_neqE simp: subst_Var) 127 128lemma eta_lift [simp]: "s \<rightarrow>\<^sub>\<eta> t ==> lift s i \<rightarrow>\<^sub>\<eta> lift t i" 129 by (induct arbitrary: i set: eta) simp_all 130 131lemma rtrancl_eta_subst: "s \<rightarrow>\<^sub>\<eta> t \<Longrightarrow> u[s/i] \<rightarrow>\<^sub>\<eta>\<^sup>* u[t/i]" 132 apply (induct u arbitrary: s t i) 133 apply (simp_all add: subst_Var) 134 apply blast 135 apply (blast intro: rtrancl_eta_App) 136 apply (blast intro!: rtrancl_eta_Abs eta_lift) 137 done 138 139lemma rtrancl_eta_subst': 140 fixes s t :: dB 141 assumes eta: "s \<rightarrow>\<^sub>\<eta>\<^sup>* t" 142 shows "s[u/i] \<rightarrow>\<^sub>\<eta>\<^sup>* t[u/i]" using eta 143 by induct (iprover intro: eta_subst)+ 144 145lemma rtrancl_eta_subst'': 146 fixes s t :: dB 147 assumes eta: "s \<rightarrow>\<^sub>\<eta>\<^sup>* t" 148 shows "u[s/i] \<rightarrow>\<^sub>\<eta>\<^sup>* u[t/i]" using eta 149 by induct (iprover intro: rtrancl_eta_subst rtranclp_trans)+ 150 151lemma square_beta_eta: "square beta eta (eta\<^sup>*\<^sup>*) (beta\<^sup>=\<^sup>=)" 152 apply (unfold square_def) 153 apply (rule impI [THEN allI [THEN allI]]) 154 apply (erule beta.induct) 155 apply (slowsimp intro: rtrancl_eta_subst eta_subst) 156 apply (blast intro: rtrancl_eta_AppL) 157 apply (blast intro: rtrancl_eta_AppR) 158 apply simp 159 apply (slowsimp intro: rtrancl_eta_Abs free_beta 160 iff del: dB.distinct simp: dB.distinct) (*23 seconds?*) 161 done 162 163lemma confluent_beta_eta: "confluent (sup beta eta)" 164 apply (assumption | 165 rule square_rtrancl_reflcl_commute confluent_Un 166 beta_confluent eta_confluent square_beta_eta)+ 167 done 168 169 170subsection \<open>Implicit definition of \<open>eta\<close>\<close> 171 172text \<open>@{term "Abs (lift s 0 \<degree> Var 0) \<rightarrow>\<^sub>\<eta> s"}\<close> 173 174lemma not_free_iff_lifted: 175 "(\<not> free s i) = (\<exists>t. s = lift t i)" 176 apply (induct s arbitrary: i) 177 apply simp 178 apply (rule iffI) 179 apply (erule linorder_neqE) 180 apply (rename_tac nat a, rule_tac x = "Var nat" in exI) 181 apply simp 182 apply (rename_tac nat a, rule_tac x = "Var (nat - 1)" in exI) 183 apply simp 184 apply clarify 185 apply (rule notE) 186 prefer 2 187 apply assumption 188 apply (erule thin_rl) 189 apply (case_tac t) 190 apply simp 191 apply simp 192 apply simp 193 apply simp 194 apply (erule thin_rl) 195 apply (erule thin_rl) 196 apply (rule iffI) 197 apply (elim conjE exE) 198 apply (rename_tac u1 u2) 199 apply (rule_tac x = "u1 \<degree> u2" in exI) 200 apply simp 201 apply (erule exE) 202 apply (erule rev_mp) 203 apply (case_tac t) 204 apply simp 205 apply simp 206 apply blast 207 apply simp 208 apply simp 209 apply (erule thin_rl) 210 apply (rule iffI) 211 apply (erule exE) 212 apply (rule_tac x = "Abs t" in exI) 213 apply simp 214 apply (erule exE) 215 apply (erule rev_mp) 216 apply (case_tac t) 217 apply simp 218 apply simp 219 apply simp 220 apply blast 221 done 222 223theorem explicit_is_implicit: 224 "(\<forall>s u. (\<not> free s 0) --> R (Abs (s \<degree> Var 0)) (s[u/0])) = 225 (\<forall>s. R (Abs (lift s 0 \<degree> Var 0)) s)" 226 by (auto simp add: not_free_iff_lifted) 227 228 229subsection \<open>Eta-postponement theorem\<close> 230 231text \<open> 232 Based on a paper proof due to Andreas Abel. 233 Unlike the proof by Masako Takahashi @{cite "Takahashi-IandC"}, it does not 234 use parallel eta reduction, which only seems to complicate matters unnecessarily. 235\<close> 236 237theorem eta_case: 238 fixes s :: dB 239 assumes free: "\<not> free s 0" 240 and s: "s[dummy/0] => u" 241 shows "\<exists>t'. Abs (s \<degree> Var 0) => t' \<and> t' \<rightarrow>\<^sub>\<eta>\<^sup>* u" 242proof - 243 from s have "lift (s[dummy/0]) 0 => lift u 0" by (simp del: lift_subst) 244 with free have "s => lift u 0" by (simp add: lift_subst_dummy del: lift_subst) 245 hence "Abs (s \<degree> Var 0) => Abs (lift u 0 \<degree> Var 0)" by simp 246 moreover have "\<not> free (lift u 0) 0" by simp 247 hence "Abs (lift u 0 \<degree> Var 0) \<rightarrow>\<^sub>\<eta> lift u 0[dummy/0]" 248 by (rule eta.eta) 249 hence "Abs (lift u 0 \<degree> Var 0) \<rightarrow>\<^sub>\<eta>\<^sup>* u" by simp 250 ultimately show ?thesis by iprover 251qed 252 253theorem eta_par_beta: 254 assumes st: "s \<rightarrow>\<^sub>\<eta> t" 255 and tu: "t => u" 256 shows "\<exists>t'. s => t' \<and> t' \<rightarrow>\<^sub>\<eta>\<^sup>* u" using tu st 257proof (induct arbitrary: s) 258 case (var n) 259 thus ?case by (iprover intro: par_beta_refl) 260next 261 case (abs s' t) 262 note abs' = this 263 from \<open>s \<rightarrow>\<^sub>\<eta> Abs s'\<close> show ?case 264 proof cases 265 case (eta s'' dummy) 266 from abs have "Abs s' => Abs t" by simp 267 with eta have "s''[dummy/0] => Abs t" by simp 268 with \<open>\<not> free s'' 0\<close> have "\<exists>t'. Abs (s'' \<degree> Var 0) => t' \<and> t' \<rightarrow>\<^sub>\<eta>\<^sup>* Abs t" 269 by (rule eta_case) 270 with eta show ?thesis by simp 271 next 272 case (abs r) 273 from \<open>r \<rightarrow>\<^sub>\<eta> s'\<close> 274 obtain t' where r: "r => t'" and t': "t' \<rightarrow>\<^sub>\<eta>\<^sup>* t" by (iprover dest: abs') 275 from r have "Abs r => Abs t'" .. 276 moreover from t' have "Abs t' \<rightarrow>\<^sub>\<eta>\<^sup>* Abs t" by (rule rtrancl_eta_Abs) 277 ultimately show ?thesis using abs by simp iprover 278 qed 279next 280 case (app u u' t t') 281 from \<open>s \<rightarrow>\<^sub>\<eta> u \<degree> t\<close> show ?case 282 proof cases 283 case (eta s' dummy) 284 from app have "u \<degree> t => u' \<degree> t'" by simp 285 with eta have "s'[dummy/0] => u' \<degree> t'" by simp 286 with \<open>\<not> free s' 0\<close> have "\<exists>r. Abs (s' \<degree> Var 0) => r \<and> r \<rightarrow>\<^sub>\<eta>\<^sup>* u' \<degree> t'" 287 by (rule eta_case) 288 with eta show ?thesis by simp 289 next 290 case (appL s') 291 from \<open>s' \<rightarrow>\<^sub>\<eta> u\<close> 292 obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* u'" by (iprover dest: app) 293 from s' and app have "s' \<degree> t => r \<degree> t'" by simp 294 moreover from r have "r \<degree> t' \<rightarrow>\<^sub>\<eta>\<^sup>* u' \<degree> t'" by (simp add: rtrancl_eta_AppL) 295 ultimately show ?thesis using appL by simp iprover 296 next 297 case (appR s') 298 from \<open>s' \<rightarrow>\<^sub>\<eta> t\<close> 299 obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* t'" by (iprover dest: app) 300 from s' and app have "u \<degree> s' => u' \<degree> r" by simp 301 moreover from r have "u' \<degree> r \<rightarrow>\<^sub>\<eta>\<^sup>* u' \<degree> t'" by (simp add: rtrancl_eta_AppR) 302 ultimately show ?thesis using appR by simp iprover 303 qed 304next 305 case (beta u u' t t') 306 from \<open>s \<rightarrow>\<^sub>\<eta> Abs u \<degree> t\<close> show ?case 307 proof cases 308 case (eta s' dummy) 309 from beta have "Abs u \<degree> t => u'[t'/0]" by simp 310 with eta have "s'[dummy/0] => u'[t'/0]" by simp 311 with \<open>\<not> free s' 0\<close> have "\<exists>r. Abs (s' \<degree> Var 0) => r \<and> r \<rightarrow>\<^sub>\<eta>\<^sup>* u'[t'/0]" 312 by (rule eta_case) 313 with eta show ?thesis by simp 314 next 315 case (appL s') 316 from \<open>s' \<rightarrow>\<^sub>\<eta> Abs u\<close> show ?thesis 317 proof cases 318 case (eta s'' dummy) 319 have "Abs (lift u 1) = lift (Abs u) 0" by simp 320 also from eta have "\<dots> = s''" by (simp add: lift_subst_dummy del: lift_subst) 321 finally have s: "s = Abs (Abs (lift u 1) \<degree> Var 0) \<degree> t" using appL and eta by simp 322 from beta have "lift u 1 => lift u' 1" by simp 323 hence "Abs (lift u 1) \<degree> Var 0 => lift u' 1[Var 0/0]" 324 using par_beta.var .. 325 hence "Abs (Abs (lift u 1) \<degree> Var 0) \<degree> t => lift u' 1[Var 0/0][t'/0]" 326 using \<open>t => t'\<close> .. 327 with s have "s => u'[t'/0]" by simp 328 thus ?thesis by iprover 329 next 330 case (abs r) 331 from \<open>r \<rightarrow>\<^sub>\<eta> u\<close> 332 obtain r'' where r: "r => r''" and r'': "r'' \<rightarrow>\<^sub>\<eta>\<^sup>* u'" by (iprover dest: beta) 333 from r and beta have "Abs r \<degree> t => r''[t'/0]" by simp 334 moreover from r'' have "r''[t'/0] \<rightarrow>\<^sub>\<eta>\<^sup>* u'[t'/0]" 335 by (rule rtrancl_eta_subst') 336 ultimately show ?thesis using abs and appL by simp iprover 337 qed 338 next 339 case (appR s') 340 from \<open>s' \<rightarrow>\<^sub>\<eta> t\<close> 341 obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* t'" by (iprover dest: beta) 342 from s' and beta have "Abs u \<degree> s' => u'[r/0]" by simp 343 moreover from r have "u'[r/0] \<rightarrow>\<^sub>\<eta>\<^sup>* u'[t'/0]" 344 by (rule rtrancl_eta_subst'') 345 ultimately show ?thesis using appR by simp iprover 346 qed 347qed 348 349theorem eta_postponement': 350 assumes eta: "s \<rightarrow>\<^sub>\<eta>\<^sup>* t" and beta: "t => u" 351 shows "\<exists>t'. s => t' \<and> t' \<rightarrow>\<^sub>\<eta>\<^sup>* u" using eta beta 352proof (induct arbitrary: u) 353 case base 354 thus ?case by blast 355next 356 case (step s' s'' s''') 357 then obtain t' where s': "s' => t'" and t': "t' \<rightarrow>\<^sub>\<eta>\<^sup>* s'''" 358 by (auto dest: eta_par_beta) 359 from s' obtain t'' where s: "s => t''" and t'': "t'' \<rightarrow>\<^sub>\<eta>\<^sup>* t'" using step 360 by blast 361 from t'' and t' have "t'' \<rightarrow>\<^sub>\<eta>\<^sup>* s'''" by (rule rtranclp_trans) 362 with s show ?case by iprover 363qed 364 365theorem eta_postponement: 366 assumes "(sup beta eta)\<^sup>*\<^sup>* s t" 367 shows "(beta\<^sup>*\<^sup>* OO eta\<^sup>*\<^sup>*) s t" using assms 368proof induct 369 case base 370 show ?case by blast 371next 372 case (step s' s'') 373 from step(3) obtain t' where s: "s \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and t': "t' \<rightarrow>\<^sub>\<eta>\<^sup>* s'" by blast 374 from step(2) show ?case 375 proof 376 assume "s' \<rightarrow>\<^sub>\<beta> s''" 377 with beta_subset_par_beta have "s' => s''" .. 378 with t' obtain t'' where st: "t' => t''" and tu: "t'' \<rightarrow>\<^sub>\<eta>\<^sup>* s''" 379 by (auto dest: eta_postponement') 380 from par_beta_subset_beta st have "t' \<rightarrow>\<^sub>\<beta>\<^sup>* t''" .. 381 with s have "s \<rightarrow>\<^sub>\<beta>\<^sup>* t''" by (rule rtranclp_trans) 382 thus ?thesis using tu .. 383 next 384 assume "s' \<rightarrow>\<^sub>\<eta> s''" 385 with t' have "t' \<rightarrow>\<^sub>\<eta>\<^sup>* s''" .. 386 with s show ?thesis .. 387 qed 388qed 389 390end 391