theory Inductive_Quotients
  imports Main
begin

subsection \<open>Restricted quotient predicate\<close>

definition "Quotient' X R Abs Rep T \<longleftrightarrow>
  (\<forall>a. \<forall>b\<in>X. T a b \<longrightarrow> Abs a = b) \<and>
  (\<forall>b\<in>X. T (Rep b) b) \<and>
  (\<forall>x y. R x y \<longrightarrow> (Abs x \<in> X \<longleftrightarrow> Abs y \<in> X)) \<and>
  (\<forall>x y. Abs x \<in> X \<longrightarrow> R x y = (T x (Abs x) \<and> T y (Abs y) \<and> Abs x = Abs y))"

lemma Quotient_Quotient':
  assumes "Quotient R Abs Rep T"
  shows "Quotient' X R Abs Rep T"
  using assms unfolding Quotient_alt_def Quotient'_def
  by simp

lemma Quotient'_UNIV:
  assumes "Quotient' UNIV R Abs Rep T"
  shows "Quotient R Abs Rep T"
  using assms unfolding Quotient_alt_def Quotient'_def
  by simp

lemma Quotient'_Union:
  assumes "\<forall>X\<in>M. Quotient' X R Abs Rep T"
  shows "Quotient' (\<Union>M) R Abs Rep T"
  using assms unfolding Quotient'_def
  by fast

lemma Quotient'_union:
  assumes "Quotient' X R Abs Rep T" and "Quotient' Y R Abs Rep T"
  shows "Quotient' (X \<union> Y) R Abs Rep T"
  using assms unfolding Quotient'_def
  by fast

(*TODO: There is probably a nicer (or more general) way to express this idea.*)
lemma Quotient'_inject:
  assumes "Quotient' X (BNF_Def.vimage2p g g R) (f' \<circ> Abs \<circ> g) (g' \<circ> Rep \<circ> f) (BNF_Def.vimage2p g f T)"
    and "\<forall>a. \<forall>x\<in>X. T a (f x) \<longrightarrow> (\<exists>y. a = g y)"
    and "f \<circ> f' \<circ> Abs \<circ> g = Abs \<circ> g"
    and "g \<circ> g' \<circ> Rep \<circ> f = Rep \<circ> f"
    and "\<forall>a b. \<forall>x\<in>X. R a b \<longrightarrow> (Abs a = f x \<or> Abs b = f x) \<longrightarrow> (\<exists>y z. a = g y \<and> b = g z)"
  shows "Quotient' (f ` X) R Abs Rep T"
  using assms unfolding Quotient'_def BNF_Def.vimage2p_def comp_def
  (*SLOW!*)
  apply (safe)
         apply (metis)
        apply (metis)
       apply (smt image_iff)
      apply (smt image_iff)
     apply (smt)
    apply (smt)
   apply (smt)
  apply (metis)
  done

text \<open>BNF example — a refined version of @{thm fun_quotient}:\<close>

lemma Quotient'_fun:
  assumes "Quotient R1 Abs1 Rep1 T1"
    and "Quotient' X R2 Abs2 Rep2 T2"
  shows "Quotient' {f. range f \<subseteq> X} (rel_fun R1 R2) (map_fun Rep1 Abs2) (map_fun Abs1 Rep2) (rel_fun T1 T2)"
  using assms unfolding Quotient_alt_def2 Quotient'_def rel_fun_def fun_eq_iff map_fun_apply
  apply (safe)
         apply (metis UNIV_I image_subset_iff)
        apply (metis UNIV_I image_subset_iff)
       apply (metis image_subset_iff)
      apply (metis image_subset_iff)
     apply (metis UNIV_I image_subset_iff)
    apply (metis UNIV_I image_subset_iff)
   apply (metis UNIV_I image_subset_iff)
  apply (smt UNIV_I image_subset_iff)
  done


subsection \<open>Example\<close>

datatype 'a T = L | N "'a \<Rightarrow> 'a T"

inductive rel_T :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a T \<Rightarrow> 'b T \<Rightarrow> bool"
  for R
  where
    "rel_T R L L"
  | "rel_fun R (rel_T R) f g \<Longrightarrow> rel_T R (N f) (N g)"

primrec map_T :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b T \<Rightarrow> 'a T"
  where
    "map_T u L = L"
  | "map_T u (N f) = N (map_T u o f o u)"

definition "apply_T_ctors S = {L} \<union> {N f | f. range f \<subseteq> S}"

lemma mono_apply_T_ctors: "mono apply_T_ctors"
  unfolding apply_T_ctors_def
  by (auto intro: monoI)

lemma lfp_apply_T_ctors: "lfp apply_T_ctors = UNIV"
proof -
  have "UNIV \<subseteq> lfp apply_T_ctors" proof (rule lfp_greatest)
    fix S :: "'b T set"
    have closed: "x \<in> S" if ctors: "L \<in> S" "{N f | f. range f \<subseteq> S} \<subseteq> S" for x
    proof (induction x)
      case L
      show ?case using ctors by blast
    next
      case (N x)
      then show ?case using ctors by blast
    qed
    assume "apply_T_ctors S \<subseteq> S"
    then show "UNIV \<subseteq> S"
      unfolding apply_T_ctors_def
      using closed by blast
  qed
  then show ?thesis by blast
qed

lemma Quotient'_T:
  assumes inner: "Quotient R Abs Rep T"
  shows "Quotient' UNIV (rel_T R) (map_T Rep) (map_T Abs) (rel_T T)" (is "?Q UNIV")
proof -
  have "?Q (lfp apply_T_ctors)"
    using mono_apply_T_ctors
  proof (rule lfp_ordinal_induct_set)
    fix S
    assume IH: "?Q S"

    have Q_L: "?Q {L}"
      unfolding Quotient'_def
      by (fastforce elim: rel_T.cases intro: rel_T.intros)

    have "inj N" by (auto intro: injI)

    have rel_T_R: "BNF_Def.vimage2p N N (rel_T R) = rel_fun R (rel_T R)"
      unfolding BNF_Def.vimage2p_def
      by (blast elim: rel_T.cases intro: rel_T.intros)
    have map_T_Rep: "inv N \<circ> map_T Rep \<circ> N = map_fun Rep (map_T Rep)"
      by (simp add: inv_f_f[OF \<open>inj N\<close>] comp_def map_fun_def[abs_def])
    have map_T_Rep': "N \<circ> inv N \<circ> map_T Rep \<circ> N = map_T Rep \<circ> N"
      by (simp add: inv_f_f[OF \<open>inj N\<close>] comp_def map_fun_def[abs_def])
    have map_T_Abs: "inv N \<circ> map_T Abs \<circ> N = map_fun Abs (map_T Abs)"
      by (simp add: inv_f_f[OF \<open>inj N\<close>] comp_def map_fun_def[abs_def])
    have map_T_Abs': "N \<circ> inv N \<circ> map_T Abs \<circ> N = map_T Abs \<circ> N"
      by (simp add: inv_f_f[OF \<open>inj N\<close>] comp_def map_fun_def[abs_def])
    have rel_T_T: "BNF_Def.vimage2p N N (rel_T T) = rel_fun T (rel_T T)"
      unfolding BNF_Def.vimage2p_def
      by (blast elim: rel_T.cases intro: rel_T.intros)

    have "Quotient' {f. range f \<subseteq> S} (BNF_Def.vimage2p N N (rel_T R))
                    (inv N \<circ> map_T Rep \<circ> N) (inv N \<circ> map_T Abs \<circ> N)
                    (BNF_Def.vimage2p N N (rel_T T))"
      unfolding rel_T_R map_T_Rep map_T_Abs rel_T_T
      using inner IH by (rule Quotient'_fun)
    then have "?Q (N ` {f. range f \<subseteq> S})"
      using map_T_Rep' map_T_Abs'
      by (auto intro!: Quotient'_inject elim: rel_T.cases)
    then have Q_N: "?Q {N f | f. range f \<subseteq> S}"
      unfolding setcompr_eq_image .

    from Q_L Q_N show "?Q (apply_T_ctors S)"
      unfolding apply_T_ctors_def
      by (rule Quotient'_union)+
  next
    (*TODO: Derived induction rule for Quotient' (lfp _) *)
    fix M
    assume "\<forall>S\<in>M. ?Q S"
    then show "?Q (\<Union>M)" by (rule Quotient'_Union)
  qed

  then show ?thesis unfolding lfp_apply_T_ctors .
qed

corollary Quotient_T [quot_map]:
  assumes "Quotient R Abs Rep T"
  shows "Quotient (rel_T R) (map_T Rep) (map_T Abs) (rel_T T)"
  using assms Quotient'_T
  by (blast intro: Quotient'_UNIV)

end