equal
deleted
inserted
replaced
368 case (eta dummy s s') |
368 case (eta dummy s s') |
369 then obtain u1'' u2'' where s': "s' = u1'' \<degree> u2''" |
369 then obtain u1'' u2'' where s': "s' = u1'' \<degree> u2''" |
370 by (cases s') (auto simp add: subst_Var free_par_eta [symmetric] split: split_if_asm) |
370 by (cases s') (auto simp add: subst_Var free_par_eta [symmetric] split: split_if_asm) |
371 then have "\<exists>u1 u2 k. s = eta_expand k (u1 \<degree> u2) \<and> u1 \<Rightarrow>\<^sub>\<eta> u1'' \<and> u2 \<Rightarrow>\<^sub>\<eta> u2''" by (rule eta) |
371 then have "\<exists>u1 u2 k. s = eta_expand k (u1 \<degree> u2) \<and> u1 \<Rightarrow>\<^sub>\<eta> u1'' \<and> u2 \<Rightarrow>\<^sub>\<eta> u2''" by (rule eta) |
372 then obtain u1 u2 k where s: "s = eta_expand k (u1 \<degree> u2)" |
372 then obtain u1 u2 k where s: "s = eta_expand k (u1 \<degree> u2)" |
373 and u1: "u1 \<Rightarrow>\<^sub>\<eta> u1''" and u2: "u2 \<Rightarrow>\<^sub>\<eta> u2''" by rules |
373 and u1: "u1 \<Rightarrow>\<^sub>\<eta> u1''" and u2: "u2 \<Rightarrow>\<^sub>\<eta> u2''" by iprover |
374 from u1 u2 eta s' have "\<not> free u1 0" and "\<not> free u2 0" |
374 from u1 u2 eta s' have "\<not> free u1 0" and "\<not> free u2 0" |
375 by (simp_all del: free_par_eta add: free_par_eta [symmetric]) |
375 by (simp_all del: free_par_eta add: free_par_eta [symmetric]) |
376 with s have "Abs (s \<degree> Var 0) = eta_expand (Suc k) (u1[dummy/0] \<degree> u2[dummy/0])" |
376 with s have "Abs (s \<degree> Var 0) = eta_expand (Suc k) (u1[dummy/0] \<degree> u2[dummy/0])" |
377 by (simp del: lift_subst add: lift_subst_dummy lift_eta_expand) |
377 by (simp del: lift_subst add: lift_subst_dummy lift_eta_expand) |
378 moreover from u1 par_eta_refl have "u1[dummy/0] \<Rightarrow>\<^sub>\<eta> u1''[dummy/0]" |
378 moreover from u1 par_eta_refl have "u1[dummy/0] \<Rightarrow>\<^sub>\<eta> u1''[dummy/0]" |
397 next |
397 next |
398 case (eta dummy s s') |
398 case (eta dummy s s') |
399 then obtain u'' where s': "s' = Abs u''" |
399 then obtain u'' where s': "s' = Abs u''" |
400 by (cases s') (auto simp add: subst_Var free_par_eta [symmetric] split: split_if_asm) |
400 by (cases s') (auto simp add: subst_Var free_par_eta [symmetric] split: split_if_asm) |
401 then have "\<exists>u k. s = eta_expand k (Abs u) \<and> u \<Rightarrow>\<^sub>\<eta> u''" by (rule eta) |
401 then have "\<exists>u k. s = eta_expand k (Abs u) \<and> u \<Rightarrow>\<^sub>\<eta> u''" by (rule eta) |
402 then obtain u k where s: "s = eta_expand k (Abs u)" and u: "u \<Rightarrow>\<^sub>\<eta> u''" by rules |
402 then obtain u k where s: "s = eta_expand k (Abs u)" and u: "u \<Rightarrow>\<^sub>\<eta> u''" by iprover |
403 from eta u s' have "\<not> free u (Suc 0)" |
403 from eta u s' have "\<not> free u (Suc 0)" |
404 by (simp del: free_par_eta add: free_par_eta [symmetric]) |
404 by (simp del: free_par_eta add: free_par_eta [symmetric]) |
405 with s have "Abs (s \<degree> Var 0) = eta_expand (Suc k) (Abs (u[lift dummy 0/Suc 0]))" |
405 with s have "Abs (s \<degree> Var 0) = eta_expand (Suc k) (Abs (u[lift dummy 0/Suc 0]))" |
406 by (simp del: lift_subst add: lift_eta_expand lift_subst_dummy) |
406 by (simp del: lift_subst add: lift_eta_expand lift_subst_dummy) |
407 moreover from u par_eta_refl have "u[lift dummy 0/Suc 0] \<Rightarrow>\<^sub>\<eta> u''[lift dummy 0/Suc 0]" |
407 moreover from u par_eta_refl have "u[lift dummy 0/Suc 0] \<Rightarrow>\<^sub>\<eta> u''[lift dummy 0/Suc 0]" |
479 by (auto dest: par_eta_beta) |
479 by (auto dest: par_eta_beta) |
480 from s' obtain t'' where s: "s => t''" and t'': "t'' -e>> t'" |
480 from s' obtain t'' where s: "s => t''" and t'': "t'' -e>> t'" |
481 by (blast dest: 2) |
481 by (blast dest: 2) |
482 from par_eta_subset_eta t' have "t' -e>> s'''" .. |
482 from par_eta_subset_eta t' have "t' -e>> s'''" .. |
483 with t'' have "t'' -e>> s'''" by (rule rtrancl_trans) |
483 with t'' have "t'' -e>> s'''" by (rule rtrancl_trans) |
484 with s show ?case by rules |
484 with s show ?case by iprover |
485 qed |
485 qed |
486 |
486 |
487 theorem eta_postponement: |
487 theorem eta_postponement: |
488 assumes st: "(s, t) \<in> (beta \<union> eta)\<^sup>*" |
488 assumes st: "(s, t) \<in> (beta \<union> eta)\<^sup>*" |
489 shows "(s, t) \<in> eta\<^sup>* O beta\<^sup>*" using st |
489 shows "(s, t) \<in> eta\<^sup>* O beta\<^sup>*" using st |