# Theory Eta

Up to index of Isabelle/HOL/Lambda

theory Eta
imports ParRed
begin

    (*  Title:      HOL/Lambda/Eta.thy
        ID:         $Id: Eta.thy,v 1.21 2005/09/22 21:56:35 nipkow Exp $
        Author:     Tobias Nipkow and Stefan Berghofer
        Copyright   1995, 2005 TU Muenchen
    *)

    header {* Eta-reduction *}

    theory Eta imports ParRed begin

    subsection {* Definition of eta-reduction and relatives *}

    consts
      free :: "dB => nat => bool"
    primrec
      "free (Var j) i = (j = i)"
      "free (s ° t) i = (free s i ∨ free t i)"
      "free (Abs s) i = free s (i + 1)"

    consts
      eta :: "(dB × dB) set"

    syntax
      "_eta" :: "[dB, dB] => bool"   (infixl "-e>" 50)
      "_eta_rtrancl" :: "[dB, dB] => bool"   (infixl "-e>>" 50)
      "_eta_reflcl" :: "[dB, dB] => bool"   (infixl "-e>=" 50)
    translations
      "s -e> t" == "(s, t) ∈ eta"
      "s -e>> t" == "(s, t) ∈ eta^*"
      "s -e>= t" == "(s, t) ∈ eta^="

    inductive eta
      intros
        eta [simp, intro]: "¬ free s 0 ==> Abs (s ° Var 0) -e> s[dummy/0]"
        appL [simp, intro]: "s -e> t ==> s ° u -e> t ° u"
        appR [simp, intro]: "s -e> t ==> u ° s -e> u ° t"
        abs [simp, intro]: "s -e> t ==> Abs s -e> Abs t"

    inductive_cases eta_cases [elim!]:
      "Abs s -e> z"
      "s ° t -e> u"
      "Var i -e> t"

    subsection "Properties of eta, subst and free"

    lemma subst_not_free [rule_format, simp]:
        "∀i t u. ¬ free s i --> s[t/i] = s[u/i]"
      apply (induct_tac s)
        apply (simp_all add: subst_Var)
      done

    lemma free_lift [simp]:
        "∀i k. free (lift t k) i =
          (i < k ∧ free t i ∨ k < i ∧ free t (i - 1))"
      apply (induct_tac t)
        apply (auto cong: conj_cong)
      apply arith
      done

    lemma free_subst [simp]:
        "∀i k t. free (s[t/k]) i =
          (free s k ∧ free t i ∨ free s (if i < k then i else i + 1))"
      apply (induct_tac s)
        prefer 2
        apply simp
        apply blast
       prefer 2
       apply simp
      apply (simp add: diff_Suc subst_Var split: nat.split)
      done

    lemma free_eta [rule_format]:
        "s -e> t ==> ∀i. free t i = free s i"
      apply (erule eta.induct)
         apply (simp_all cong: conj_cong)
      done

    lemma not_free_eta:
        "[| s -e> t; ¬ free s i |] ==> ¬ free t i"
      apply (simp add: free_eta)
      done

    lemma eta_subst [rule_format, simp]:
        "s -e> t ==> ∀u i. s[u/i] -e> t[u/i]"
      apply (erule eta.induct)
      apply (simp_all add: subst_subst [symmetric])
      done

    theorem lift_subst_dummy: "!!i dummy. ¬ free s i ==> lift (s[dummy/i]) i = s"
      by (induct s) simp_all

    subsection "Confluence of eta"

    lemma square_eta: "square eta eta (eta^=) (eta^=)"
      apply (unfold square_def id_def)
      apply (rule impI [THEN allI [THEN allI]])
      apply simp
      apply (erule eta.induct)
         apply (slowsimp intro: subst_not_free eta_subst free_eta [THEN iffD1])
        apply safe
           prefer 5
           apply (blast intro!: eta_subst intro: free_eta [THEN iffD1])
          apply blast+
      done

    theorem eta_confluent: "confluent eta"
      apply (rule square_eta [THEN square_reflcl_confluent])
      done

    subsection "Congruence rules for eta*"

    lemma rtrancl_eta_Abs: "s -e>> s' ==> Abs s -e>> Abs s'"
      apply (erule rtrancl_induct)
       apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
      done

    lemma rtrancl_eta_AppL: "s -e>> s' ==> s ° t -e>> s' ° t"
      apply (erule rtrancl_induct)
       apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
      done

    lemma rtrancl_eta_AppR: "t -e>> t' ==> s ° t -e>> s ° t'"
      apply (erule rtrancl_induct)
       apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
      done

    lemma rtrancl_eta_App:
        "[| s -e>> s'; t -e>> t' |] ==> s ° t -e>> s' ° t'"
      apply (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtrancl_trans)
      done

    subsection "Commutation of beta and eta"

    lemma free_beta [rule_format]:
        "s -> t ==> ∀i. free t i --> free s i"
      apply (erule beta.induct)
         apply simp_all
      done

    lemma beta_subst [rule_format, intro]:
        "s -> t ==> ∀u i. s[u/i] -> t[u/i]"
      apply (erule beta.induct)
         apply (simp_all add: subst_subst [symmetric])
      done

    lemma subst_Var_Suc [simp]: "∀i. t[Var i/i] = t[Var(i)/i + 1]"
      apply (induct_tac t)
      apply (auto elim!: linorder_neqE simp: subst_Var)
      done

    lemma eta_lift [rule_format, simp]:
        "s -e> t ==> ∀i. lift s i -e> lift t i"
      apply (erule eta.induct)
         apply simp_all
      done

    lemma rtrancl_eta_subst [rule_format]:
        "∀s t i. s -e> t --> u[s/i] -e>> u[t/i]"
      apply (induct_tac u)
        apply (simp_all add: subst_Var)
        apply (blast)
       apply (blast intro: rtrancl_eta_App)
      apply (blast intro!: rtrancl_eta_Abs eta_lift)
      done

    lemma square_beta_eta: "square beta eta (eta^*) (beta^=)"
      apply (unfold square_def)
      apply (rule impI [THEN allI [THEN allI]])
      apply (erule beta.induct)
         apply (slowsimp intro: rtrancl_eta_subst eta_subst)
        apply (blast intro: rtrancl_eta_AppL)
       apply (blast intro: rtrancl_eta_AppR)
      apply simp;
      apply (slowsimp intro: rtrancl_eta_Abs free_beta
        iff del: dB.distinct simp: dB.distinct)    (*23 seconds?*)
      done

    lemma confluent_beta_eta: "confluent (beta ∪ eta)"
      apply (assumption |
        rule square_rtrancl_reflcl_commute confluent_Un
          beta_confluent eta_confluent square_beta_eta)+
      done

    subsection "Implicit definition of eta"

    text {* @{term "Abs (lift s 0 ° Var 0) -e> s"} *}

    lemma not_free_iff_lifted [rule_format]:
        "∀i. (¬ free s i) = (∃t. s = lift t i)"
      apply (induct_tac s)
        apply simp
        apply clarify
        apply (rule iffI)
         apply (erule linorder_neqE)
          apply (rule_tac x = "Var nat" in exI)
          apply simp
         apply (rule_tac x = "Var (nat - 1)" in exI)
         apply simp
        apply clarify
        apply (rule notE)
         prefer 2
         apply assumption
        apply (erule thin_rl)
        apply (case_tac t)
          apply simp
         apply simp
        apply simp
       apply simp
       apply (erule thin_rl)
       apply (erule thin_rl)
       apply (rule allI)
       apply (rule iffI)
        apply (elim conjE exE)
        apply (rename_tac u1 u2)
        apply (rule_tac x = "u1 ° u2" in exI)
        apply simp
       apply (erule exE)
       apply (erule rev_mp)
       apply (case_tac t)
         apply simp
        apply simp
        apply blast
       apply simp
      apply simp
      apply (erule thin_rl)
      apply (rule allI)
      apply (rule iffI)
       apply (erule exE)
       apply (rule_tac x = "Abs t" in exI)
       apply simp
      apply (erule exE)
      apply (erule rev_mp)
      apply (case_tac t)
        apply simp
       apply simp
      apply simp
      apply blast
      done

    theorem explicit_is_implicit:
      "(∀s u. (¬ free s 0) --> R (Abs (s ° Var 0)) (s[u/0])) =
        (∀s. R (Abs (lift s 0 ° Var 0)) s)"
      apply (auto simp add: not_free_iff_lifted)
      done

    subsection {* Parallel eta-reduction *}

    consts
      par_eta :: "(dB × dB) set"

    syntax
      "_par_eta" :: "[dB, dB] => bool"   (infixl "=e>" 50)
    translations
      "s =e> t" == "(s, t) ∈ par_eta"

    syntax (xsymbols)
      "_par_eta" :: "[dB, dB] => bool"   (infixl "=>η" 50)

    inductive par_eta
    intros
      var [simp, intro]: "Var x =>η Var x"
      eta [simp, intro]: "¬ free s 0 ==> s =>η s'==> Abs (s ° Var 0) =>η s'[dummy/0]"
      app [simp, intro]: "s =>η s' ==> t =>η t' ==> s ° t =>η s' ° t'"
      abs [simp, intro]: "s =>η t ==> Abs s =>η Abs t"

    lemma free_par_eta [simp]: assumes eta: "s =>η t"
      shows "!!i. free t i = free s i" using eta
      by induct (simp_all cong: conj_cong)

    lemma par_eta_refl [simp]: "t =>η t"
      by (induct t) simp_all

    lemma par_eta_lift [simp]:
      assumes eta: "s =>η t"
      shows "!!i. lift s i =>η lift t i" using eta
      by induct simp_all

    lemma par_eta_subst [simp]:
      assumes eta: "s =>η t"
      shows "!!u u' i. u =>η u' ==> s[u/i] =>η t[u'/i]" using eta
      by induct (simp_all add: subst_subst [symmetric] subst_Var)

    theorem eta_subset_par_eta: "eta ⊆ par_eta"
      apply (rule subsetI)
      apply clarify
      apply (erule eta.induct)
      apply (blast intro!: par_eta_refl)+
      done

    theorem par_eta_subset_eta: "par_eta ⊆ eta*"
      apply (rule subsetI)
      apply clarify
      apply (erule par_eta.induct)
      apply blast
      apply (rule rtrancl_into_rtrancl)
      apply (rule rtrancl_eta_Abs)
      apply (rule rtrancl_eta_AppL)
      apply assumption
      apply (rule eta.eta)
      apply simp
      apply (rule rtrancl_eta_App)
      apply assumption+
      apply (rule rtrancl_eta_Abs)
      apply assumption
      done

    subsection {* n-ary eta-expansion *}

    consts eta_expand :: "nat => dB => dB"
    primrec
      eta_expand_0: "eta_expand 0 t = t"
      eta_expand_Suc: "eta_expand (Suc n) t = Abs (lift (eta_expand n t) 0 ° Var 0)"

    lemma eta_expand_Suc':
      "!!t. eta_expand (Suc n) t = eta_expand n (Abs (lift t 0 ° Var 0))"
      by (induct n) simp_all

    theorem lift_eta_expand: "lift (eta_expand k t) i = eta_expand k (lift t i)"
      by (induct k) (simp_all add: lift_lift)

    theorem eta_expand_beta:
      assumes u: "u => u'"
      shows "!!t t'. t => t' ==> eta_expand k (Abs t) ° u => t'[u'/0]"
    proof (induct k)
      case 0 with u show ?case by simp
    next
      case (Suc k)
      hence "Abs (lift t (Suc 0)) ° Var 0 => lift t' (Suc 0)[Var 0/0]"
        by (blast intro: par_beta_lift)
      with Suc show ?case by (simp del: eta_expand_Suc add: eta_expand_Suc')
    qed

    theorem eta_expand_red:
      assumes t: "t => t'"
      shows "eta_expand k t => eta_expand k t'"
      by (induct k) (simp_all add: t)

    theorem eta_expand_eta: "!!t t'. t =>η t' ==> eta_expand k t =>η t'"
    proof (induct k)
      case 0
      show ?case by simp
    next
      case (Suc k)
      have "Abs (lift (eta_expand k t) 0 ° Var 0) =>η lift t' 0[arbitrary/0]"
        by (fastsimp intro: par_eta_lift Suc)
      thus ?case by simp
    qed

    subsection {* Elimination rules for parallel eta reduction *}

    theorem par_eta_elim_app: assumes eta: "t =>η u"
      shows "!!u1' u2'. u = u1' ° u2' ==>
        ∃u1 u2 k. t = eta_expand k (u1 ° u2) ∧ u1 =>η u1' ∧ u2 =>η u2'" using eta
    proof induct
      case (app s s' t t')
      have "s ° t = eta_expand 0 (s ° t)" by simp
      with app show ?case by blast
    next
      case (eta dummy s s')
      then obtain u1'' u2'' where s': "s' = u1'' ° u2''"
        by (cases s') (auto simp add: subst_Var free_par_eta [symmetric] split: split_if_asm)
      then have "∃u1 u2 k. s = eta_expand k (u1 ° u2) ∧ u1 =>η u1'' ∧ u2 =>η u2''" by (rule eta)
      then obtain u1 u2 k where s: "s = eta_expand k (u1 ° u2)"
        and u1: "u1 =>η u1''" and u2: "u2 =>η u2''" by iprover
      from u1 u2 eta s' have "¬ free u1 0" and "¬ free u2 0"
        by (simp_all del: free_par_eta add: free_par_eta [symmetric])
      with s have "Abs (s ° Var 0) = eta_expand (Suc k) (u1[dummy/0] ° u2[dummy/0])"
        by (simp del: lift_subst add: lift_subst_dummy lift_eta_expand)
      moreover from u1 par_eta_refl have "u1[dummy/0] =>η u1''[dummy/0]"
        by (rule par_eta_subst)
      moreover from u2 par_eta_refl have "u2[dummy/0] =>η u2''[dummy/0]"
        by (rule par_eta_subst)
      ultimately show ?case using eta s'
        by (simp only: subst.simps dB.simps) blast
    next
      case var thus ?case by simp
    next
      case abs thus ?case by simp
    qed

    theorem par_eta_elim_abs: assumes eta: "t =>η t'"
      shows "!!u'. t' = Abs u' ==>
        ∃u k. t = eta_expand k (Abs u) ∧ u =>η u'" using eta
    proof induct
      case (abs s t)
      have "Abs s = eta_expand 0 (Abs s)" by simp
      with abs show ?case by blast
    next
      case (eta dummy s s')
      then obtain u'' where s': "s' = Abs u''"
        by (cases s') (auto simp add: subst_Var free_par_eta [symmetric] split: split_if_asm)
      then have "∃u k. s = eta_expand k (Abs u) ∧ u =>η u''" by (rule eta)
      then obtain u k where s: "s = eta_expand k (Abs u)" and u: "u =>η u''" by iprover
      from eta u s' have "¬ free u (Suc 0)"
        by (simp del: free_par_eta add: free_par_eta [symmetric])
      with s have "Abs (s ° Var 0) = eta_expand (Suc k) (Abs (u[lift dummy 0/Suc 0]))"
        by (simp del: lift_subst add: lift_eta_expand lift_subst_dummy)
      moreover from u par_eta_refl have "u[lift dummy 0/Suc 0] =>η u''[lift dummy 0/Suc 0]"
        by (rule par_eta_subst)
      ultimately show ?case using eta s' by fastsimp
    next
      case var thus ?case by simp
    next
      case app thus ?case by simp
    qed

    subsection {* Eta-postponement theorem *}

    text {*
    Based on a proof by Masako Takahashi \cite{Takahashi-IandC}.
    *}

    theorem par_eta_beta: "!!s u. s =>η t ==> t => u ==> ∃t'. s => t' ∧ t' =>η u"
    proof (induct t rule: measure_induct [of size, rule_format])
      case (1 t)
      from 1(3)
      show ?case
      proof cases
        case (var n)
        with 1 show ?thesis
          by (auto intro: par_beta_refl)
      next
        case (abs r' r'')
        with 1 have "s =>η Abs r'" by simp
        then obtain r k where s: "s = eta_expand k (Abs r)" and rr: "r =>η r'"
          by (blast dest: par_eta_elim_abs)
        from abs have "size r' < size t" by simp
        with abs(2) rr obtain t' where rt: "r => t'" and t': "t' =>η r''"
          by (blast dest: 1)
        with s abs show ?thesis
          by (auto intro: eta_expand_red eta_expand_eta)
      next
        case (app q' q'' r' r'')
        with 1 have "s =>η q' ° r'" by simp
        then obtain q r k where s: "s = eta_expand k (q ° r)"
          and qq: "q =>η q'" and rr: "r =>η r'"
          by (blast dest: par_eta_elim_app [OF _ refl])
        from app have "size q' < size t" and "size r' < size t" by simp_all
        with app(2,3) qq rr obtain t' t'' where "q => t'" and
          "t' =>η q''" and "r => t''" and "t'' =>η r''"
          by (blast dest: 1)
        with s app show ?thesis
          by (fastsimp intro: eta_expand_red eta_expand_eta)
      next
        case (beta q' q'' r' r'')
        with 1 have "s =>η Abs q' ° r'" by simp
        then obtain q r k k' where s: "s = eta_expand k (eta_expand k' (Abs q) ° r)"
          and qq: "q =>η q'" and rr: "r =>η r'"
          by (blast dest: par_eta_elim_app par_eta_elim_abs)
        from beta have "size q' < size t" and "size r' < size t" by simp_all
        with beta(2,3) qq rr obtain t' t'' where "q => t'" and
          "t' =>η q''" and "r => t''" and "t'' =>η r''"
          by (blast dest: 1)
        with s beta show ?thesis
          by (auto intro: eta_expand_red eta_expand_beta eta_expand_eta par_eta_subst)
      qed
    qed

    theorem eta_postponement': assumes eta: "s -e>> t"
      shows "!!u. t => u ==> ∃t'. s => t' ∧ t' -e>> u"
      using eta [simplified rtrancl_subset
        [OF eta_subset_par_eta par_eta_subset_eta, symmetric]]
    proof induct
      case 1
      thus ?case by blast
    next
      case (2 s' s'' s''')
      from 2 obtain t' where s': "s' => t'" and t': "t' =>η s'''"
        by (auto dest: par_eta_beta)
      from s' obtain t'' where s: "s => t''" and t'': "t'' -e>> t'"
        by (blast dest: 2)
      from par_eta_subset_eta t' have "t' -e>> s'''" ..
      with t'' have "t'' -e>> s'''" by (rule rtrancl_trans)
      with s show ?case by iprover
    qed

    theorem eta_postponement:
      assumes st: "(s, t) ∈ (beta ∪ eta)*"
      shows "(s, t) ∈ eta* O beta*" using st
    proof induct
      case 1
      show ?case by blast
    next
      case (2 s' s'')
      from 2(3) obtain t' where s: "s ->β* t'" and t': "t' -e>> s'" by blast
      from 2(2) show ?case
      proof
        assume "s' -> s''"
        with beta_subset_par_beta have "s' => s''" ..
        with t' obtain t'' where st: "t' => t''" and tu: "t'' -e>> s''"
          by (auto dest: eta_postponement')
        from par_beta_subset_beta st have "t' ->β* t''" ..
        with s have "s ->β* t''" by (rule rtrancl_trans)
        thus ?thesis using tu ..
      next
        assume "s' -e> s''"
        with t' have "t' -e>> s''" ..
        with s show ?thesis ..
      qed
    qed

    end

### Definition of eta-reduction and relatives

lemmas eta_cases:

      [| Abs s -e> z;
         !!dummy s. [| ¬ free s 0; s = s ° Var 0; z = s[dummy/0] |] ==> P;
         !!t. [| s -e> t; z = Abs t |] ==> P |]
      ==> P

      [| s ° t -e> u; !!t. [| s -e> t; u = t ° t |] ==> P;
         !!t. [| t -e> t; u = s ° t |] ==> P |]
      ==> P

      Var i -e> t ==> P

### Properties of eta, subst and free

lemma subst_not_free:

      ¬ free s i ==> s[t/i] = s[u/i]

lemma free_lift:

      ∀i k. free (lift t k) i = (i < k ∧ free t i ∨ k < i ∧ free t (i - 1))

lemma free_subst:

      ∀i k t.
         free (s[t/k]) i = (free s k ∧ free t i ∨ free s (if i < k then i else i + 1))

lemma free_eta:

      s -e> t ==> free t i = free s i

lemma not_free_eta:

      [| s -e> t; ¬ free s i |] ==> ¬ free t i

lemma eta_subst:

      s -e> t ==> s[u/i] -e> t[u/i]

theorem lift_subst_dummy:

      ¬ free s i ==> lift (s[dummy/i]) i = s

### Confluence of eta

lemma square_eta:

      square eta eta (eta=) (eta=)

theorem eta_confluent:

      confluent eta

### Congruence rules for eta*

lemma rtrancl_eta_Abs:

      s -e>> s' ==> Abs s -e>> Abs s'

lemma rtrancl_eta_AppL:

      s -e>> s' ==> s ° t -e>> s' ° t

lemma rtrancl_eta_AppR:

      t -e>> t' ==> s ° t -e>> s ° t'

lemma rtrancl_eta_App:

      [| s -e>> s'; t -e>> t' |] ==> s ° t -e>> s' ° t'

### Commutation of beta and eta

lemma free_beta:

      [| s -> t; free t i |] ==> free s i

lemma beta_subst:

      s -> t ==> s[u/i] -> t[u/i]

lemma subst_Var_Suc:

      ∀i. t[Var i/i] = t[Var i/i + 1]

lemma eta_lift:

      s -e> t ==> lift s i -e> lift t i

lemma rtrancl_eta_subst:

      s -e> t ==> u[s/i] -e>> u[t/i]

lemma square_beta_eta:

      square beta eta (eta*) (beta=)

lemma confluent_beta_eta:

      confluent (beta ∪ eta)

### Implicit definition of eta

lemma not_free_iff_lifted:

      (¬ free s i) = (∃t. s = lift t i)

theorem explicit_is_implicit:

      (∀s u. ¬ free s 0 --> R (Abs (s ° Var 0)) (s[u/0])) =
      (∀s. R (Abs (lift s 0 ° Var 0)) s)

### Parallel eta-reduction

lemma free_par_eta:

      s =e> t ==> free t i = free s i

lemma par_eta_refl:

      t =e> t

lemma par_eta_lift:

      s =e> t ==> lift s i =e> lift t i

lemma par_eta_subst:

      [| s =e> t; u =e> u' |] ==> s[u/i] =e> t[u'/i]

theorem eta_subset_par_eta:

      eta ⊆ par_eta

theorem par_eta_subset_eta:

      par_eta ⊆ eta*

### n-ary eta-expansion

lemma eta_expand_Suc':

      eta_expand (Suc n) t = eta_expand n (Abs (lift t 0 ° Var 0))

theorem lift_eta_expand:

      lift (eta_expand k t) i = eta_expand k (lift t i)

theorem eta_expand_beta:

      [| u => u'; t => t' |] ==> eta_expand k (Abs t) ° u => t'[u'/0]

theorem eta_expand_red:

      t => t' ==> eta_expand k t => eta_expand k t'

theorem eta_expand_eta:

      t =e> t' ==> eta_expand k t =e> t'

### Elimination rules for parallel eta reduction

theorem par_eta_elim_app:

      [| t =e> u; u = u1' ° u2' |]
      ==> ∃u1 u2 k. t = eta_expand k (u1 ° u2) ∧ u1 =e> u1' ∧ u2 =e> u2'

theorem par_eta_elim_abs:

      [| t =e> t'; t' = Abs u' |] ==> ∃u k. t = eta_expand k (Abs u) ∧ u =e> u'

### Eta-postponement theorem

theorem par_eta_beta:

      [| s =e> t; t => u |] ==> ∃t'. s => t' ∧ t' =e> u

theorem eta_postponement':

      [| s -e>> t; t => u |] ==> ∃t'. s => t' ∧ t' -e>> u

theorem eta_postponement:

      (s, t) ∈ (beta ∪ eta)* ==> (s, t) ∈ eta* O beta*