*To*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Lifting and datatypes with dead arguments*From*: Joshua Schneider <dev at jshs.de>*Date*: Mon, 27 Mar 2017 17:44:28 +0200*In-reply-to*: <VI1PR0101MB214361006458F90C2C958EB2B7300@VI1PR0101MB2143.eurprd01.prod.exchangelabs.com>*Mail-followup-to*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*References*: <20170324090804.GA2107@jshs-laptop.fritz.box> <VI1PR0101MB214361006458F90C2C958EB2B7300@VI1PR0101MB2143.eurprd01.prod.exchangelabs.com>*User-agent*: Mutt/1.8.0 (2017-02-23)

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

**Follow-Ups**:**Re: [isabelle] Lifting and datatypes with dead arguments***From:*Andrei Popescu

**References**:**[isabelle] Lifting and datatypes with dead arguments***From:*Joshua Schneider

**Re: [isabelle] Lifting and datatypes with dead arguments***From:*Andrei Popescu

- Previous by Date: Re: [isabelle] Isabell HOLCF tutorial
- Next by Date: Re: [isabelle] Lifting and datatypes with dead arguments
- Previous by Thread: Re: [isabelle] Lifting and datatypes with dead arguments
- Next by Thread: Re: [isabelle] Lifting and datatypes with dead arguments
- Cl-isabelle-users March 2017 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list