Theory NU_Equ

(*<*)
theory NU_Equ
imports NU_PreEqu
begin
(*>*)

section ‹Equality›

text ‹
  Proves various facts about the equivalence relation.
›

lemma equ_refl: 
  shows "nabla ⊢ t ≈ t"
  by(induct t, auto simp add: ds_def)


lemma equ_dec_pi:
  assumes "nabla ⊢ swap pi t1 ≈ swap pi t2"
  shows "nabla ⊢ t1 ≈ t2"
proof-
  have i: "nabla ⊢ swap (rev pi) (swap pi t1) ≈ t1"
    "nabla ⊢ swap (rev pi) (swap pi t2) ≈ t2"
    using rev_pi_pi_equ by auto
  then have "nabla ⊢ swap (rev pi) (swap pi t1) ≈ swap (rev pi) (swap pi t2)"
    using equ_equivariance assms by simp
  then show ?thesis using i equ_symm equ_trans by meson 
qed

lemma equ_involutive_left: 
  shows "nabla ⊢ swap (rev pi) (swap pi t1) ≈ t2 = nabla ⊢ t1 ≈ t2"
proof(auto)
  have i: "nabla ⊢ t1 ≈ swap (rev pi) (swap pi t1)"
    using rev_pi_pi_equ equ_symm by blast
  show "nabla ⊢ swap (rev pi) (swap pi t1) ≈ t2 ⟹ nabla ⊢ t1 ≈ t2"
    using i equ_trans by blast
  show "nabla ⊢ t1 ≈ t2 ⟹ nabla ⊢ swap (rev pi) (swap pi t1) ≈ t2"
    using i equ_trans equ_symm by blast
qed

lemma equ_pi_to_left: 
  shows "nabla ⊢ swap (rev pi) t1 ≈ t2 = nabla ⊢ t1 ≈ swap pi t2"
proof

  {assume i: "nabla ⊢ swap (rev pi) t1 ≈ t2"
  have "nabla ⊢ swap pi (swap (rev pi) t1) ≈ swap pi t2"
    using equ_equivariance[OF i, of pi] by simp
  then show "nabla ⊢ t1 ≈ swap pi t2"
    using equ_involutive_left[of nabla ‹rev pi› t1 ‹swap pi t2›] rev_rev_ident[of pi]
    by simp}

  {assume i: "nabla ⊢ t1 ≈ swap pi t2"
  have ii: "nabla ⊢ swap (rev pi) t1 ≈ swap (rev pi) (swap pi t2)"
    using equ_equivariance[OF i, of ‹rev pi›] by simp
  then have iii: "nabla ⊢ swap (rev pi) (swap pi t2) ≈ swap (rev pi) t1"
    using equ_symm[OF ii] by simp
  then have iv: "nabla ⊢ t2 ≈ swap (rev pi) t1"
    using equ_involutive_left[of nabla pi t2 ‹swap (rev pi) t1›] by simp
  then show "nabla ⊢ swap (rev pi) t1 ≈ t2"
    using equ_symm[OF iv] by simp}

qed
    
lemma equ_pi_to_right: 
  shows "nabla⊢t1 ≈ swap (rev pi) t2 = nabla⊢swap pi t1≈t2"
proof
  {assume i: "nabla ⊢ t1 ≈ swap (rev pi) t2"
    then show "nabla ⊢ swap pi t1 ≈  t2"
      using equ_involutive_left equ_dec_pi by blast}
  {assume ii: "nabla ⊢ swap pi t1 ≈ t2"
    then show "nabla ⊢ t1 ≈ swap (rev pi) t2"
      using equ_involutive_left equ_equivariance by blast}
qed

lemma equ_involutive_right: 
  shows "nabla ⊢ t1 ≈ swap (rev pi) (swap pi t2) = nabla ⊢ t1 ≈ t2"
  using equ_dec_pi[of nabla pi t1 t2] equ_equivariance[of nabla t1 t2 pi] 
    equ_pi_to_right[of nabla t1 pi ‹swap pi t2›]
  by auto

lemma equ_pi1_pi2_add: 
  assumes "∀a∈ ds pi1 pi2. nabla⊢a♯t"
  shows "nabla⊢swap pi1 t ≈ swap pi2 t"
proof-
  have "nabla ⊢ t ≈ swap (rev pi1 @ pi2) t" 
    using assms ds_rev equ_pi_right by simp
  hence "nabla ⊢ t ≈ swap (rev pi1) (swap pi2 t)"
    using swap_append by auto
  then show "nabla⊢swap pi1 t ≈ swap pi2 t"
    using equ_pi_to_right by simp
qed

lemma pi_right_equ: 
  assumes "nabla ⊢ t ≈ swap pi t"
  shows "∀a∈ ds [] pi. nabla ⊢ a ♯ t"
  using assms pi_right_equ_help by blast

lemma equ_pi1_pi2_dec:  
  assumes "nabla ⊢ swap pi1 t ≈ swap pi2 t"
  shows "∀ a ∈ ds pi1 pi2. nabla⊢a ♯ t"
proof-
  have "nabla ⊢ t ≈ swap ((rev pi1) @ pi2) t"
    using assms equ_pi_to_right swap_append by simp
  then show "∀ a ∈ ds pi1 pi2. nabla⊢a ♯ t"
    using pi_right_equ ds_rev[of pi1 pi2] by simp
qed

lemma equ_weak: 
  assumes "nabla1 ⊢ t1 ≈ t2"
  shows "(nabla1 ∪ nabla2) ⊢ t1 ≈ t2"
  using assms by (erule_tac equ.induct) (auto simp add: fresh_weak)

text ‹
  No term can be equal to one of its proper subterm.
›

lemma psub_trm_not_equ: 
  shows "∀ t2 ∈ psub_trms t1. (¬(∃ pi. (nabla ⊢ t1 ≈ swap pi t2)))"
proof
  fix t2
  assume i: "t2 ∈ psub_trms t1"
  show "¬ (∃pi. nabla ⊢ t1 ≈ swap pi t2)"
  proof
    assume "∃pi. nabla ⊢ t1 ≈ swap pi t2"
    then obtain pi where H:
      "nabla ⊢ t1 ≈ swap pi t2" by blast

    from equ_depth[OF H]
    have "depth t1 = depth (swap pi t2)"
      by simp
    hence "depth t1 = depth t2" 
      by simp
    moreover have "depth t2 < depth t1"
      using i depth_psub_trms 
      by simp

    ultimately show False by auto
  qed
qed


(*<*)
end 
(*>*)