Re: [isabelle] Lifting and datatypes with dead arguments



Hi Andrei,

Thank you for working through the proof! It seems like the transfer of the
equivalence relation is the trickiest part, which was the missing piece in
my own attempt at proving this.

I would also like to generalise the quotient mapping to arbitrary nested
BNFs, but I don't see how that would work based on your solution.

I recently talked to Andreas Lochbihler about the problem, and he suggested
a fixed-point induction. I have now implemented that idea (see attached
theory), using a version of the Quotient predicate which is restricted to
some subset of the abstract type. I think that it is promising, because the
core of the proof is compositional with respect to the functor structure.
I have not tried to scale it to larger examples, though.

Do you think that this is a worthwhile path towards automation, or do you
have something different in mind?

Cheers,
Joshua
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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.