Theory Quotient_TLList

(*  Title:       Preservation and respectfulness theorems for terminated coinductive lists
    Author:      Andreas Lochbihler
    Maintainer:  Andreas Lochbihler
*)

section ‹Setup for Isabelle's quotient package for terminated lazy lists›

theory Quotient_TLList imports
  TLList
  "HOL-Library.Quotient_Product"
  "HOL-Library.Quotient_Sum"
  "HOL-Library.Quotient_Set"
begin

subsection ‹Rules for the Quotient package›

lemma tmap_id_id [id_simps]:
  "tmap id id = id"
by(simp add: fun_eq_iff tllist.map_id)

declare tllist_all2_eq[id_simps]

lemma case_sum_preserve [quot_preserve]:
  assumes q1: "Quotient3 R1 Abs1 Rep1"
  and q2: "Quotient3 R2 Abs2 Rep2"
  and q3: "Quotient3 R3 Abs3 Rep3"
  shows "((Abs1 ---> Rep2) ---> (Abs3 ---> Rep2) ---> map_sum Rep1 Rep3 ---> Abs2) case_sum = case_sum"
using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] Quotient3_abs_rep[OF q3]
by(simp add: fun_eq_iff split: sum.split)

lemma case_sum_preserve2 [quot_preserve]:
  assumes q: "Quotient3 R Abs Rep"
  shows "((id ---> Rep) ---> (id ---> Rep) ---> id ---> Abs) case_sum = case_sum"
using Quotient3_abs_rep[OF q]
by(auto intro!: ext split: sum.split)

lemma case_prod_preserve [quot_preserve]:
  assumes q1: "Quotient3 R1 Abs1 Rep1"
  and q2: "Quotient3 R2 Abs2 Rep2"
  and q3: "Quotient3 R3 Abs3 Rep3"
  shows "((Abs1 ---> Abs2 ---> Rep3) ---> map_prod Rep1 Rep2 ---> Abs3) case_prod = case_prod"
using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] Quotient3_abs_rep[OF q3]
by(simp add: fun_eq_iff split: prod.split)

lemma case_prod_preserve2 [quot_preserve]:
  assumes q: "Quotient3 R Abs Rep"
  shows "((id ---> id ---> Rep) ---> id ---> Abs) case_prod = case_prod"
using Quotient3_abs_rep[OF q]
by(auto intro!: ext)

lemma id_preserve [quot_preserve]:
  assumes "Quotient3 R Abs Rep"
  shows "(Rep ---> Abs) id = id"
using Quotient3_abs_rep[OF assms]
by(auto intro: ext)

functor tmap: tmap
   by(simp_all add: fun_eq_iff tmap_id_id tllist.map_comp)

lemma reflp_tllist_all2:
  assumes R: "reflp R" and Q: "reflp Q"
  shows "reflp (tllist_all2 R Q)"
proof(rule reflpI)
  fix xs
  show "tllist_all2 R Q xs xs"
    apply(coinduction arbitrary: xs)
    using assms by(auto elim: reflpE)
qed

lemma symp_tllist_all2: "⟦ symp R; symp S ⟧ ⟹ symp (tllist_all2 R S)"
by (rule sympI)(auto 4 3 simp add: tllist_all2_conv_all_tnth elim: sympE dest: lfinite_llength_enat not_lfinite_llength)

lemma transp_tllist_all2: "⟦ transp R; transp S ⟧ ⟹ transp (tllist_all2 R S)"
  by (rule transpI) (rule tllist_all2_trans)

lemma tllist_equivp [quot_equiv]:
  "⟦ equivp R; equivp S ⟧ ⟹ equivp (tllist_all2 R S)"
  by (simp add: equivp_reflp_symp_transp reflp_tllist_all2 symp_tllist_all2 transp_tllist_all2)

declare tllist_all2_eq [simp, id_simps]

lemma tmap_preserve [quot_preserve]:
  assumes q1: "Quotient3 R1 Abs1 Rep1"
  and q2: "Quotient3 R2 Abs2 Rep2"
  and q3: "Quotient3 R3 Abs3 Rep3"
  and q4: "Quotient3 R4 Abs4 Rep4"
  shows "((Abs1 ---> Rep2) ---> (Abs3 ---> Rep4) ---> tmap Rep1 Rep3 ---> tmap Abs2 Abs4) tmap = tmap"
  and "((Abs1 ---> id) ---> (Abs2 ---> id) ---> tmap Rep1 Rep2 ---> id) tmap = tmap"
using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] Quotient3_abs_rep[OF q3] Quotient3_abs_rep[OF q4]
by(simp_all add: fun_eq_iff tllist.map_comp o_def)

lemmas tmap_respect [quot_respect] = tmap_transfer2

lemma Quotient3_tmap_Abs_Rep:
  "⟦Quotient3 R1 Abs1 Rep1; Quotient3 R2 Abs2 Rep2⟧
  ⟹ tmap Abs1 Abs2 (tmap Rep1 Rep2 ts) = ts"
by(drule abs_o_rep)+(simp add: tllist.map_comp tmap_id_id)

lemma Quotient3_tllist_all2_tmap_tmapI:
  assumes q1: "Quotient3 R1 Abs1 Rep1"
  and q2: "Quotient3 R2 Abs2 Rep2"
  shows "tllist_all2 R1 R2 (tmap Rep1 Rep2 ts) (tmap Rep1 Rep2 ts)"
by(coinduction arbitrary: ts)(auto simp add: Quotient3_rep_reflp[OF q1] Quotient3_rep_reflp[OF q2])

lemma tllist_all2_rel:
  assumes q1: "Quotient3 R1 Abs1 Rep1"
  and q2: "Quotient3 R2 Abs2 Rep2"
  shows "tllist_all2 R1 R2 r s ⟷ (tllist_all2 R1 R2 r r ∧ tllist_all2 R1 R2 s s ∧ tmap Abs1 Abs2 r = tmap Abs1 Abs2 s)"
  (is "?lhs ⟷ ?rhs")
proof(intro iffI conjI)
  assume "?lhs"
  thus "tllist_all2 R1 R2 r r"
    apply -
    apply(rule tllist_all2_reflI)
    apply(clarsimp simp add: in_tset_conv_tnth)
    apply(metis tllist_all2_tnthD Quotient3_rel [OF q1])
    apply(metis tllist_all2_tfinite1_terminalD Quotient3_rel [OF q2])
    done

  from ‹?lhs› show "tllist_all2 R1 R2 s s"
    apply -
    apply(rule tllist_all2_reflI)
    apply(clarsimp simp add: in_tset_conv_tnth)
    apply(metis tllist_all2_tnthD2 Quotient3_rel [OF q1])
    apply(metis tllist_all2_tfinite2_terminalD Quotient3_rel [OF q2])
    done

  from ‹?lhs› show "tmap Abs1 Abs2 r = tmap Abs1 Abs2 s"
    unfolding tmap_eq_tmap_conv_tllist_all2
    by(rule tllist_all2_mono)(metis Quotient3_rel[OF q1] Quotient3_rel[OF q2])+
next
  assume "?rhs"
  thus "?lhs"
    unfolding tmap_eq_tmap_conv_tllist_all2
    apply(clarsimp simp add: tllist_all2_conv_all_tnth)
    apply(subst Quotient3_rel[OF q1, symmetric])
    apply(subst Quotient3_rel[OF q2, symmetric])
    apply(auto 4 3 dest: lfinite_llength_enat not_lfinite_llength)
    done
qed

lemma tllist_quotient [quot_thm]:
  "⟦ Quotient3 R1 Abs1 Rep1; Quotient3 R2 Abs2 Rep2 ⟧
  ⟹ Quotient3 (tllist_all2 R1 R2) (tmap Abs1 Abs2) (tmap Rep1 Rep2)"
by(blast intro: Quotient3I dest: Quotient3_tmap_Abs_Rep Quotient3_tllist_all2_tmap_tmapI tllist_all2_rel)

declare [[mapQ3 tllist = (tllist_all2, tllist_quotient)]]

lemma TCons_preserve [quot_preserve]:
  assumes q1: "Quotient3 R1 Abs1 Rep1"
  and q2: "Quotient3 R2 Abs2 Rep2"
  shows "(Rep1 ---> (tmap Rep1 Rep2) ---> (tmap Abs1 Abs2)) TCons = TCons"
using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]
by(simp add: fun_eq_iff tllist.map_comp o_def tmap_id_id[unfolded id_def])

lemmas TCons_respect [quot_respect] = TCons_transfer2

lemma TNil_preserve [quot_preserve]:
  assumes "Quotient3 R2 Abs2 Rep2"
  shows "(Rep2 ---> tmap Abs1 Abs2) TNil = TNil"
using Quotient3_abs_rep[OF assms]
by(simp add: fun_eq_iff)

lemmas TNil_respect [quot_respect] = TNil_transfer2

lemmas tllist_all2_respect [quot_respect] = tllist_all2_transfer

lemma tllist_all2_prs:
  assumes q1: "Quotient3 R1 Abs1 Rep1"
  and q2: "Quotient3 R2 Abs2 Rep2"
  shows "tllist_all2 ((Abs1 ---> Abs1 ---> id) P) ((Abs2 ---> Abs2 ---> id) Q)
                     (tmap Rep1 Rep2 ts) (tmap Rep1 Rep2 ts')
         ⟷ tllist_all2 P Q ts ts'"
  (is "?lhs ⟷ ?rhs")
proof
  assume ?lhs
  thus ?rhs
  proof(coinduct)
    case (tllist_all2 ts ts')
    thus ?case using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]
      by(cases ts)(case_tac [!] ts', auto simp add: tllist_all2_TNil1 tllist_all2_TCons1)
  qed
next
  assume ?rhs
  thus ?lhs
    apply(coinduction arbitrary: ts ts')
    using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]
    by(auto dest: tllist_all2_is_TNilD intro: tllist_all2_tfinite1_terminalD tllist_all2_thdD tllist_all2_ttlI)
qed

lemma tllist_all2_preserve [quot_preserve]:
  assumes "Quotient3 R1 Abs1 Rep1"
  and "Quotient3 R2 Abs2 Rep2"
  shows "((Abs1 ---> Abs1 ---> id) ---> (Abs2 ---> Abs2 ---> id) --->
          tmap Rep1 Rep2 ---> tmap Rep1 Rep2 ---> id) tllist_all2 = tllist_all2"
by(simp add: fun_eq_iff tllist_all2_prs[OF assms])

lemma tllist_all2_preserve2 [quot_preserve]:
  assumes q1: "Quotient3 R1 Abs1 Rep1"
  and q2: "Quotient3 R2 Abs2 Rep2"
  shows "(tllist_all2 ((Rep1 ---> Rep1 ---> id) R1) ((Rep2 ---> Rep2 ---> id) R2)) = (=)"
  by (simp add: fun_eq_iff map_fun_def comp_def Quotient3_rel_rep[OF q1] Quotient3_rel_rep[OF q2]
    tllist_all2_eq)

lemma corec_tllist_preserve [quot_preserve]:
  assumes q1: "Quotient3 R1 Abs1 Rep1"
  and q2: "Quotient3 R2 Abs2 Rep2"
  and q3: "Quotient3 R3 Abs3 Rep3"
  shows "((Abs1 ---> id) ---> (Abs1 ---> Rep2) ---> (Abs1 ---> Rep3) ---> (Abs1 ---> id) ---> (Abs1 ---> tmap Rep3 Rep2) ---> (Abs1 ---> Rep1) ---> Rep1 ---> tmap Abs3 Abs2) corec_tllist = corec_tllist"
  (is "?lhs = ?rhs")
proof(intro ext)
  fix IS_TNIL TNIL THD endORmore TTL_end TTL_more b
  show "?lhs IS_TNIL TNIL THD endORmore TTL_end TTL_more b = ?rhs IS_TNIL TNIL THD endORmore TTL_end TTL_more b"
    by(coinduction arbitrary: b rule: tllist.coinduct_strong)(auto simp add: Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] Quotient3_abs_rep[OF q3] Quotient3_tmap_Abs_Rep[OF q3 q2])
qed

end