--- a/src/Doc/Datatypes/Datatypes.thy Fri Feb 28 22:23:43 2020 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Fri Feb 28 21:23:11 2020 +0100
@@ -3117,7 +3117,7 @@
\<^rail>\<open>
@@{command lift_bnf} target? lb_options? \<newline>
@{syntax tyargs} name wit_terms? \<newline>
- ('via' thm)? @{syntax map_rel_pred}?
+ ('via' thm thm?)? @{syntax map_rel_pred}?
;
@{syntax_def lb_options}: '(' ((@{syntax plugins} | 'no_warn_wits' | 'no_warn_transfer') + ',') ')'
;
@@ -3132,7 +3132,9 @@
\emph{raw type}) using the @{command quotient_type}. To achieve this, it lifts the BNF
structure on the raw type to the abstract type following a \<^term>\<open>type_definition\<close> or a
\<^term>\<open>Quotient\<close> theorem. The theorem is usually inferred from the type, but can
-also be explicitly supplied by means of the optional \<open>via\<close> clause. In
+also be explicitly supplied by means of the optional \<open>via\<close> clause. In case of quotients, it
+is sometimes also necessary to supply a second theorem of the form \<^term>\<open>reflp eq\<close>,
+that expresses the reflexivity (and thus totality) of the equivalence relation. In
addition, custom names for the set functions, the map function, the predicator, and the relator,
as well as nonemptiness witnesses can be specified.
--- a/src/HOL/Datatype_Examples/Dlist.thy Fri Feb 28 22:23:43 2020 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,81 +0,0 @@
-theory Dlist imports
- "HOL-Library.Confluent_Quotient"
-begin
-
-context begin
-
-qualified definition dlist_eq where "dlist_eq = BNF_Def.vimage2p remdups remdups (=)"
-
-lemma equivp_dlist_eq: "equivp dlist_eq"
- unfolding dlist_eq_def by(rule equivp_vimage2p)(rule identity_equivp)
-
-quotient_type 'a dlist = "'a list" / dlist_eq
- by (rule equivp_dlist_eq)
-
-qualified inductive double :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
- "double (xs @ ys) (xs @ x # ys)" if "x \<in> set ys"
-
-qualified lemma strong_confluentp_double: "strong_confluentp double"
-proof
- fix xs ys zs :: "'a list"
- assume ys: "double xs ys" and zs: "double xs zs"
- consider (left) as y bs z cs where "xs = as @ bs @ cs" "ys = as @ y # bs @ cs" "zs = as @ bs @ z # cs" "y \<in> set (bs @ cs)" "z \<in> set cs"
- | (right) as y bs z cs where "xs = as @ bs @ cs" "ys = as @ bs @ y # cs" "zs = as @ z # bs @ cs" "y \<in> set cs" "z \<in> set (bs @ cs)"
- proof -
- show thesis using ys zs
- by(clarsimp simp add: double.simps append_eq_append_conv2)(auto intro: that)
- qed
- then show "\<exists>us. double\<^sup>*\<^sup>* ys us \<and> double\<^sup>=\<^sup>= zs us"
- proof cases
- case left
- let ?us = "as @ y # bs @ z # cs"
- have "double ys ?us" "double zs ?us" using left
- by(auto 4 4 simp add: double.simps)(metis append_Cons append_assoc)+
- then show ?thesis by blast
- next
- case right
- let ?us = "as @ z # bs @ y # cs"
- have "double ys ?us" "double zs ?us" using right
- by(auto 4 4 simp add: double.simps)(metis append_Cons append_assoc)+
- then show ?thesis by blast
- qed
-qed
-
-qualified lemma double_Cons1 [simp]: "double xs (x # xs)" if "x \<in> set xs"
- using double.intros[of x xs "[]"] that by simp
-
-qualified lemma double_Cons_same [simp]: "double xs ys \<Longrightarrow> double (x # xs) (x # ys)"
- by(auto simp add: double.simps Cons_eq_append_conv)
-
-qualified lemma doubles_Cons_same: "double\<^sup>*\<^sup>* xs ys \<Longrightarrow> double\<^sup>*\<^sup>* (x # xs) (x # ys)"
- by(induction rule: rtranclp_induct)(auto intro: rtranclp.rtrancl_into_rtrancl)
-
-qualified lemma remdups_into_doubles: "double\<^sup>*\<^sup>* (remdups xs) xs"
- by(induction xs)(auto intro: doubles_Cons_same rtranclp.rtrancl_into_rtrancl)
-
-qualified lemma dlist_eq_into_doubles: "dlist_eq \<le> equivclp double"
- by(auto 4 4 simp add: dlist_eq_def vimage2p_def
- intro: equivclp_trans converse_rtranclp_into_equivclp rtranclp_into_equivclp remdups_into_doubles)
-
-qualified lemma factor_double_map: "double (map f xs) ys \<Longrightarrow> \<exists>zs. dlist_eq xs zs \<and> ys = map f zs"
- by(auto simp add: double.simps dlist_eq_def vimage2p_def map_eq_append_conv)
- (metis list.simps(9) map_append remdups.simps(2) remdups_append2)
-
-qualified lemma dlist_eq_set_eq: "dlist_eq xs ys \<Longrightarrow> set xs = set ys"
- by(simp add: dlist_eq_def vimage2p_def)(metis set_remdups)
-
-qualified lemma dlist_eq_map_respect: "dlist_eq xs ys \<Longrightarrow> dlist_eq (map f xs) (map f ys)"
- by(clarsimp simp add: dlist_eq_def vimage2p_def)(metis remdups_map_remdups)
-
-qualified lemma confluent_quotient_dlist:
- "confluent_quotient double dlist_eq dlist_eq dlist_eq dlist_eq dlist_eq (map fst) (map snd) (map fst) (map snd) list_all2 list_all2 list_all2 set set"
- by(unfold_locales)(auto intro: strong_confluentp_imp_confluentp strong_confluentp_double dest: factor_double_map dlist_eq_into_doubles[THEN predicate2D] dlist_eq_set_eq simp add: list.in_rel list.rel_compp dlist_eq_map_respect equivp_dlist_eq equivp_imp_transp)
-
-lift_bnf 'a dlist
- subgoal for A B by(rule confluent_quotient.subdistributivity[OF confluent_quotient_dlist])
- subgoal by(force dest: dlist_eq_set_eq intro: equivp_reflp[OF equivp_dlist_eq])
- done
-
-end
-
-end
--- a/src/HOL/Library/Dlist.thy Fri Feb 28 22:23:43 2020 +0100
+++ b/src/HOL/Library/Dlist.thy Fri Feb 28 21:23:11 2020 +0100
@@ -1,10 +1,10 @@
-(* Author: Florian Haftmann, TU Muenchen
+(* Author: Florian Haftmann, TU Muenchen
Author: Andreas Lochbihler, ETH Zurich *)
section \<open>Lists with elements distinct as canonical example for datatype invariants\<close>
theory Dlist
-imports Main
+imports Confluent_Quotient
begin
subsection \<open>The type of distinct lists\<close>
@@ -15,6 +15,28 @@
show "[] \<in> {xs. distinct xs}" by simp
qed
+context begin
+
+qualified definition dlist_eq where "dlist_eq = BNF_Def.vimage2p remdups remdups (=)"
+
+qualified lemma equivp_dlist_eq: "equivp dlist_eq"
+ unfolding dlist_eq_def by(rule equivp_vimage2p)(rule identity_equivp)
+
+qualified definition abs_dlist :: "'a list \<Rightarrow> 'a dlist" where "abs_dlist = Abs_dlist o remdups"
+
+definition qcr_dlist :: "'a list \<Rightarrow> 'a dlist \<Rightarrow> bool" where "qcr_dlist x y \<longleftrightarrow> y = abs_dlist x"
+
+qualified lemma Quotient_dlist_remdups: "Quotient dlist_eq abs_dlist list_of_dlist qcr_dlist"
+ unfolding Quotient_def dlist_eq_def qcr_dlist_def vimage2p_def abs_dlist_def
+ by (auto simp add: fun_eq_iff Abs_dlist_inject
+ list_of_dlist[simplified] list_of_dlist_inverse distinct_remdups_id)
+
+end
+
+locale Quotient_dlist begin
+setup_lifting Dlist.Quotient_dlist_remdups Dlist.equivp_dlist_eq[THEN equivp_reflp2]
+end
+
setup_lifting type_definition_dlist
lemma dlist_eq_iff:
@@ -184,7 +206,7 @@
show thesis
proof (cases xs)
case Nil with dxs
- have "dxs = Dlist.empty" by (simp add: Dlist.empty_def)
+ have "dxs = Dlist.empty" by (simp add: Dlist.empty_def)
with empty show ?thesis .
next
case (Cons x xs)
@@ -210,135 +232,92 @@
context begin
-qualified fun wpull :: "('a \<times> 'b) list \<Rightarrow> ('b \<times> 'c) list \<Rightarrow> ('a \<times> 'c) list"
-where
- "wpull [] ys = []"
-| "wpull xs [] = []"
-| "wpull ((a, b) # xs) ((b', c) # ys) =
- (if b \<in> snd ` set xs then
- (a, the (map_of (rev ((b', c) # ys)) b)) # wpull xs ((b', c) # ys)
- else if b' \<in> fst ` set ys then
- (the (map_of (map prod.swap (rev ((a, b) # xs))) b'), c) # wpull ((a, b) # xs) ys
- else (a, c) # wpull xs ys)"
-
-qualified lemma wpull_eq_Nil_iff [simp]: "wpull xs ys = [] \<longleftrightarrow> xs = [] \<or> ys = []"
-by(cases "(xs, ys)" rule: wpull.cases) simp_all
+qualified inductive double :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
+ "double (xs @ ys) (xs @ x # ys)" if "x \<in> set ys"
-qualified lemma wpull_induct
- [consumes 1,
- case_names Nil left[xs eq in_set IH] right[xs ys eq in_set IH] step[xs ys eq IH] ]:
- assumes eq: "remdups (map snd xs) = remdups (map fst ys)"
- and Nil: "P [] []"
- and left: "\<And>a b xs b' c ys.
- \<lbrakk> b \<in> snd ` set xs; remdups (map snd xs) = remdups (map fst ((b', c) # ys));
- (b, the (map_of (rev ((b', c) # ys)) b)) \<in> set ((b', c) # ys); P xs ((b', c) # ys) \<rbrakk>
- \<Longrightarrow> P ((a, b) # xs) ((b', c) # ys)"
- and right: "\<And>a b xs b' c ys.
- \<lbrakk> b \<notin> snd ` set xs; b' \<in> fst ` set ys;
- remdups (map snd ((a, b) # xs)) = remdups (map fst ys);
- (the (map_of (map prod.swap (rev ((a, b) #xs))) b'), b') \<in> set ((a, b) # xs);
- P ((a, b) # xs) ys \<rbrakk>
- \<Longrightarrow> P ((a, b) # xs) ((b', c) # ys)"
- and step: "\<And>a b xs c ys.
- \<lbrakk> b \<notin> snd ` set xs; b \<notin> fst ` set ys; remdups (map snd xs) = remdups (map fst ys);
- P xs ys \<rbrakk>
- \<Longrightarrow> P ((a, b) # xs) ((b, c) # ys)"
- shows "P xs ys"
-using eq
-proof(induction xs ys rule: wpull.induct)
- case 1 thus ?case by(simp add: Nil)
-next
- case 2 thus ?case by(simp split: if_split_asm)
-next
- case Cons: (3 a b xs b' c ys)
- let ?xs = "(a, b) # xs" and ?ys = "(b', c) # ys"
- consider (xs) "b \<in> snd ` set xs" | (ys) "b \<notin> snd ` set xs" "b' \<in> fst ` set ys"
- | (step) "b \<notin> snd ` set xs" "b' \<notin> fst ` set ys" by auto
- thus ?case
+qualified lemma strong_confluentp_double: "strong_confluentp double"
+proof
+ fix xs ys zs :: "'a list"
+ assume ys: "double xs ys" and zs: "double xs zs"
+ consider (left) as y bs z cs where "xs = as @ bs @ cs" "ys = as @ y # bs @ cs" "zs = as @ bs @ z # cs" "y \<in> set (bs @ cs)" "z \<in> set cs"
+ | (right) as y bs z cs where "xs = as @ bs @ cs" "ys = as @ bs @ y # cs" "zs = as @ z # bs @ cs" "y \<in> set cs" "z \<in> set (bs @ cs)"
+ proof -
+ show thesis using ys zs
+ by(clarsimp simp add: double.simps append_eq_append_conv2)(auto intro: that)
+ qed
+ then show "\<exists>us. double\<^sup>*\<^sup>* ys us \<and> double\<^sup>=\<^sup>= zs us"
proof cases
- case xs
- with Cons.prems have eq: "remdups (map snd xs) = remdups (map fst ?ys)" by auto
- from xs eq have "b \<in> fst ` set ?ys" by (metis list.set_map set_remdups)
- hence "map_of (rev ?ys) b \<noteq> None" unfolding map_of_eq_None_iff by auto
- then obtain c' where "map_of (rev ?ys) b = Some c'" by blast
- then have "(b, the (map_of (rev ?ys) b)) \<in> set ?ys" by(auto dest: map_of_SomeD split: if_split_asm)
- from xs eq this Cons.IH(1)[OF xs eq] show ?thesis by(rule left)
+ case left
+ let ?us = "as @ y # bs @ z # cs"
+ have "double ys ?us" "double zs ?us" using left
+ by(auto 4 4 simp add: double.simps)(metis append_Cons append_assoc)+
+ then show ?thesis by blast
next
- case ys
- from ys Cons.prems have eq: "remdups (map snd ?xs) = remdups (map fst ys)" by auto
- from ys eq have "b' \<in> snd ` set ?xs" by (metis list.set_map set_remdups)
- hence "map_of (map prod.swap (rev ?xs)) b' \<noteq> None"
- unfolding map_of_eq_None_iff by(auto simp add: image_image)
- then obtain a' where "map_of (map prod.swap (rev ?xs)) b' = Some a'" by blast
- then have "(the (map_of (map prod.swap (rev ?xs)) b'), b') \<in> set ?xs"
- by(auto dest: map_of_SomeD split: if_split_asm)
- from ys eq this Cons.IH(2)[OF ys eq] show ?thesis by(rule right)
- next
- case *: step
- hence "remdups (map snd xs) = remdups (map fst ys)" "b = b'" using Cons.prems by auto
- from * this(1) Cons.IH(3)[OF * this(1)] show ?thesis unfolding \<open>b = b'\<close> by(rule step)
+ case right
+ let ?us = "as @ z # bs @ y # cs"
+ have "double ys ?us" "double zs ?us" using right
+ by(auto 4 4 simp add: double.simps)(metis append_Cons append_assoc)+
+ then show ?thesis by blast
qed
qed
-qualified lemma set_wpull_subset:
- assumes "remdups (map snd xs) = remdups (map fst ys)"
- shows "set (wpull xs ys) \<subseteq> set xs O set ys"
-using assms by(induction xs ys rule: wpull_induct) auto
+qualified lemma double_Cons1 [simp]: "double xs (x # xs)" if "x \<in> set xs"
+ using double.intros[of x xs "[]"] that by simp
+
+qualified lemma double_Cons_same [simp]: "double xs ys \<Longrightarrow> double (x # xs) (x # ys)"
+ by(auto simp add: double.simps Cons_eq_append_conv)
-qualified lemma set_fst_wpull:
- assumes "remdups (map snd xs) = remdups (map fst ys)"
- shows "fst ` set (wpull xs ys) = fst ` set xs"
-using assms by(induction xs ys rule: wpull_induct)(auto intro: rev_image_eqI)
+qualified lemma doubles_Cons_same: "double\<^sup>*\<^sup>* xs ys \<Longrightarrow> double\<^sup>*\<^sup>* (x # xs) (x # ys)"
+ by(induction rule: rtranclp_induct)(auto intro: rtranclp.rtrancl_into_rtrancl)
+
+qualified lemma remdups_into_doubles: "double\<^sup>*\<^sup>* (remdups xs) xs"
+ by(induction xs)(auto intro: doubles_Cons_same rtranclp.rtrancl_into_rtrancl)
+
+qualified lemma dlist_eq_into_doubles: "Dlist.dlist_eq \<le> equivclp double"
+ by(auto 4 4 simp add: Dlist.dlist_eq_def vimage2p_def
+ intro: equivclp_trans converse_rtranclp_into_equivclp rtranclp_into_equivclp remdups_into_doubles)
-qualified lemma set_snd_wpull:
- assumes "remdups (map snd xs) = remdups (map fst ys)"
- shows "snd ` set (wpull xs ys) = snd ` set ys"
-using assms by(induction xs ys rule: wpull_induct)(auto intro: rev_image_eqI)
-
-qualified lemma wpull:
- assumes "distinct xs"
- and "distinct ys"
- and "set xs \<subseteq> {(x, y). R x y}"
- and "set ys \<subseteq> {(x, y). S x y}"
- and eq: "remdups (map snd xs) = remdups (map fst ys)"
- shows "\<exists>zs. distinct zs \<and> set zs \<subseteq> {(x, y). (R OO S) x y} \<and>
- remdups (map fst zs) = remdups (map fst xs) \<and> remdups (map snd zs) = remdups (map snd ys)"
-proof(intro exI conjI)
- let ?zs = "remdups (wpull xs ys)"
- show "distinct ?zs" by simp
- show "set ?zs \<subseteq> {(x, y). (R OO S) x y}" using assms(3-4) set_wpull_subset[OF eq] by fastforce
- show "remdups (map fst ?zs) = remdups (map fst xs)" unfolding remdups_map_remdups using eq
- by(induction xs ys rule: wpull_induct)(auto simp add: set_fst_wpull intro: rev_image_eqI)
- show "remdups (map snd ?zs) = remdups (map snd ys)" unfolding remdups_map_remdups using eq
- by(induction xs ys rule: wpull_induct)(auto simp add: set_snd_wpull intro: rev_image_eqI)
-qed
+qualified lemma factor_double_map: "double (map f xs) ys \<Longrightarrow> \<exists>zs. Dlist.dlist_eq xs zs \<and> ys = map f zs"
+ by(auto simp add: double.simps Dlist.dlist_eq_def vimage2p_def map_eq_append_conv)
+ (metis list.simps(9) map_append remdups.simps(2) remdups_append2)
+
+qualified lemma dlist_eq_set_eq: "Dlist.dlist_eq xs ys \<Longrightarrow> set xs = set ys"
+ by(simp add: Dlist.dlist_eq_def vimage2p_def)(metis set_remdups)
-qualified lift_definition set :: "'a dlist \<Rightarrow> 'a set" is List.set .
-
-qualified lemma map_transfer [transfer_rule]:
- "(rel_fun (=) (rel_fun (pcr_dlist (=)) (pcr_dlist (=)))) (\<lambda>f x. remdups (List.map f x)) Dlist.map"
-by(simp add: rel_fun_def dlist.pcr_cr_eq cr_dlist_def Dlist.map_def remdups_remdups)
+qualified lemma dlist_eq_map_respect: "Dlist.dlist_eq xs ys \<Longrightarrow> Dlist.dlist_eq (map f xs) (map f ys)"
+ by(clarsimp simp add: Dlist.dlist_eq_def vimage2p_def)(metis remdups_map_remdups)
-bnf "'a dlist"
- map: Dlist.map
- sets: set
- bd: natLeq
- wits: Dlist.empty
-unfolding OO_Grp_alt mem_Collect_eq
-subgoal by(rule ext)(simp add: dlist_eq_iff)
-subgoal by(rule ext)(simp add: dlist_eq_iff remdups_map_remdups)
-subgoal by(simp add: dlist_eq_iff set_def cong: list.map_cong)
-subgoal by(simp add: set_def fun_eq_iff)
-subgoal by(simp add: natLeq_card_order)
-subgoal by(simp add: natLeq_cinfinite)
-subgoal by(rule ordLess_imp_ordLeq)(simp add: finite_iff_ordLess_natLeq[symmetric] set_def)
-subgoal by(rule predicate2I)(transfer; auto simp add: wpull)
-subgoal by(simp add: set_def)
-done
+qualified lemma confluent_quotient_dlist:
+ "confluent_quotient double Dlist.dlist_eq Dlist.dlist_eq Dlist.dlist_eq Dlist.dlist_eq Dlist.dlist_eq
+ (map fst) (map snd) (map fst) (map snd) list_all2 list_all2 list_all2 set set"
+ by(unfold_locales)(auto intro: strong_confluentp_imp_confluentp strong_confluentp_double
+ dest: factor_double_map dlist_eq_into_doubles[THEN predicate2D] dlist_eq_set_eq
+ simp add: list.in_rel list.rel_compp dlist_eq_map_respect Dlist.equivp_dlist_eq equivp_imp_transp)
+
lifting_update dlist.lifting
lifting_forget dlist.lifting
end
+context begin
+interpretation Quotient_dlist: Quotient_dlist .
+
+lift_bnf (plugins del: code) 'a dlist
+ subgoal for A B by(rule confluent_quotient.subdistributivity[OF Dlist.confluent_quotient_dlist])
+ subgoal by(force dest: Dlist.dlist_eq_set_eq intro: equivp_reflp[OF Dlist.equivp_dlist_eq])
+ done
+
+qualified lemma list_of_dlist_transfer[transfer_rule]:
+ "bi_unique R \<Longrightarrow> (rel_fun (Quotient_dlist.pcr_dlist R) (list_all2 R)) remdups list_of_dlist"
+ unfolding rel_fun_def Quotient_dlist.pcr_dlist_def qcr_dlist_def Dlist.abs_dlist_def
+ by (auto simp: Abs_dlist_inverse intro!: remdups_transfer[THEN rel_funD])
+
+lemma list_of_dlist_map_dlist[simp]:
+ "list_of_dlist (map_dlist f xs) = remdups (map f (list_of_dlist xs))"
+ by transfer (auto simp: remdups_map_remdups)
+
end
+
+
+end
--- a/src/HOL/Quotient.thy Fri Feb 28 22:23:43 2020 +0100
+++ b/src/HOL/Quotient.thy Fri Feb 28 21:23:11 2020 +0100
@@ -842,8 +842,18 @@
lemma Quotient_Quotient3: "Quotient R Abs Rep T \<Longrightarrow> Quotient3 R Abs Rep"
unfolding Quotient_def Quotient3_def by blast
-lemma bnf_lift_Quotient_equivp: "Quotient R Abs Rep T \<and> equivp R \<Longrightarrow> True"
- by auto
+lemma Quotient_reflp_imp_equivp: "Quotient R Abs Rep T \<Longrightarrow> reflp R \<Longrightarrow> equivp R"
+ using Quotient_symp Quotient_transp equivpI by blast
+
+lemma Quotient_eq_onp_typedef:
+ "Quotient (eq_onp P) Abs Rep cr \<Longrightarrow> type_definition Rep Abs {x. P x}"
+ unfolding Quotient_def eq_onp_def
+ by unfold_locales auto
+
+lemma Quotient_eq_onp_type_copy:
+ "Quotient (=) Abs Rep cr \<Longrightarrow> type_definition Rep Abs UNIV"
+ unfolding Quotient_def eq_onp_def
+ by unfold_locales auto
ML_file "Tools/BNF/bnf_lift.ML"
@@ -853,7 +863,6 @@
relcompp_mem_Grp_neq_bot comp_projr_Inr in_rel_sum_in_image_projr subset_rel_sumI
relcompp_eq_Grp_neq_bot rel_fun_rel_OO1 rel_fun_rel_OO2 rel_sum_eq2_nonempty rel_sum_eq3_nonempty
hypsubst equivp_add_relconj Grp_conversep_eq_onp Grp_conversep_nonempty relcomppI2 rel_conj_eq_onp
- bnf_lift_Quotient_equivp Quotient_Quotient3
+ Quotient_reflp_imp_equivp Quotient_Quotient3
end
-
--- a/src/HOL/ROOT Fri Feb 28 22:23:43 2020 +0100
+++ b/src/HOL/ROOT Fri Feb 28 21:23:11 2020 +0100
@@ -825,7 +825,6 @@
Milner_Tofte
Stream_Processor
Cyclic_List
- Dlist
Free_Idempotent_Monoid
LDL
TLList
--- a/src/HOL/Tools/BNF/bnf_lift.ML Fri Feb 28 22:23:43 2020 +0100
+++ b/src/HOL/Tools/BNF/bnf_lift.ML Fri Feb 28 21:23:11 2020 +0100
@@ -24,12 +24,12 @@
local_theory -> local_theory
val lift_bnf:
((((lift_bnf_option list * (binding option * (string * sort option)) list) *
- string) * term list option) * thm option) * (binding * binding * binding) ->
+ string) * term list option) * thm list option) * (binding * binding * binding) ->
({context: Proof.context, prems: thm list} -> tactic) list ->
local_theory -> local_theory
val lift_bnf_cmd:
((((lift_bnf_option list * (binding option * (string * string option)) list) *
- string) * string list) * (Facts.ref * Token.src list) option) *
+ string) * string list) * (Facts.ref * Token.src list) list option) *
(binding * binding * binding) -> local_theory -> Proof.state
end
@@ -47,7 +47,7 @@
| No_Warn_Wits
| No_Warn_Transfer;
-datatype lift_thm = Typedef of thm | Quotient of thm
+datatype equiv_thm = Typedef | Quotient of thm
(** Util **)
@@ -327,7 +327,7 @@
fun mk_crel_def quot_thm =
(case thm of
Quotient equiv => @{thm Quotient_crel_quotient} OF [quot_thm, equiv]
- | Typedef _ => hd ([quot_thm] RL @{thms Quotient_crel_typedef Quotient_crel_typecopy}));
+ | Typedef => hd ([quot_thm] RL @{thms Quotient_crel_typedef Quotient_crel_typecopy}));
fun no_quotient _ = [Pretty.para ("No quotient theorem has been registered for " ^
Binding.name_of (name_of_bnf bnf_G) ^ "."),
Pretty.para "Use setup_lifting to register a quotient or type definition theorem."];
@@ -686,14 +686,13 @@
val (bnf_G, lthy) = morph_bnf_defs unfold_morphism bnf_G
|> (fn bnf => note_bnf_defs bnf lthy);
- val setup_lifting_thm = Typedef thm;
val quiet = exists (fn No_Warn_Transfer => true | _ => false) opts;
val transfer_consts = mk_typedef_transfer_tacs bnf_F bnf_G
{map_closed=map_closed_thm,typedef=thm} old_defs map_raw rel_raw pred_raw sets_F;
in
lthy |> BNF_Def.register_bnf plugins AbsT_name bnf_G |>
- mk_transfer_thms quiet bnf_F bnf_G AbsT_name transfer_consts setup_lifting_thm
+ mk_transfer_thms quiet bnf_F bnf_G AbsT_name transfer_consts Typedef
{abs=typ_subst_atomic (alphas ~~ alphas') AbsT, rep=RepT, Ds0=map TFree Ds0,
deads = deads, alphas=alphas, betas=alphas', gammas=betas, deltas=betas'} defs
end
@@ -832,7 +831,7 @@
end;
-fun quotient_bnf (equiv_thm, quot_thm) _ wits specs map_b rel_b pred_b opts lthy =
+fun quotient_bnf (equiv_thm, quot_thm) wits specs map_b rel_b pred_b opts lthy =
let
(* extract rep_G and abs_G *)
val (equiv_rel, abs_G, rep_G) = strip3 quot_thm;
@@ -1968,35 +1967,70 @@
local
fun prepare_common prepare_name prepare_sort prepare_term prepare_thm
- (((((plugins, raw_specs), raw_absT_name), raw_wits), xthm_opt), (map_b, rel_b, pred_b)) lthy =
+ (((((plugins, raw_specs), raw_absT_name), raw_wits), xthms_opt), (map_b, rel_b, pred_b)) lthy =
let
val absT_name = prepare_name lthy raw_absT_name;
- val input_thm =
- (case xthm_opt of
- SOME xthm => prepare_thm lthy xthm
- | NONE => Typedef.get_info lthy absT_name |> hd |> snd |> #type_definition);
+ fun bad_input input =
+ Pretty.chunks [Pretty.para ("Expected theorem(s) of either form:"),
+ Pretty.item [Pretty.enum "," "" "" [Syntax.pretty_term lthy @{term "Quotient R Abs Rep T"},
+ Syntax.pretty_term lthy @{term "reflp R"}]],
+ Pretty.item [Syntax.pretty_term lthy @{term "Quotient R Abs Rep T"}],
+ Pretty.item [Syntax.pretty_term lthy @{term "type_definition Rep Abs A"}],
+ Pretty.para ("Got"), Pretty.enum "," "" "" (map (Thm.pretty_thm lthy) input)]
+ |> Pretty.string_of
+ |> error;
+
+ fun no_refl qthm =
+ Pretty.chunks [Pretty.para ("Could not find a reflexivity rule for the Quotient theorem:"),
+ Pretty.item [Thm.pretty_thm lthy qthm],
+ Pretty.para ("Try supplying a reflexivity theorem manually or registering it in setup_lifting.")]
+ |> Pretty.string_of
+ |> error;
+
+ fun find_equiv_thm_via_Quotient qthm =
+ let
+ val refl_thms = Lifting_Info.get_reflexivity_rules lthy
+ |> map (unfold_thms lthy @{thms reflp_eq[symmetric]});
+ in
+ (case refl_thms RL [qthm RS @{thm Quotient_reflp_imp_equivp}] of
+ [] => no_refl qthm
+ | thm :: _ => thm)
+ end;
+
+ val (lift_thm, equiv_thm) =
+ (case Option.map (prepare_thm lthy) xthms_opt of
+ SOME (thms as [qthm, _]) =>
+ (case try (fn thms => @{thm Quotient_reflp_imp_equivp} OF thms) thms of
+ SOME equiv_thm => (qthm RS @{thm Quotient_Quotient3}, Quotient equiv_thm)
+ | NONE => bad_input thms)
+ | SOME [thm] =>
+ (case try (fn thm => thm RS @{thm Quotient_Quotient3}) thm of
+ SOME qthm => (qthm, Quotient (find_equiv_thm_via_Quotient thm))
+ | NONE => if can (fn thm => thm RS @{thm type_definition.Rep}) thm
+ then (thm, Typedef)
+ else bad_input [thm])
+ | NONE => (case Lifting_Info.lookup_quotients lthy absT_name of
+ SOME {quot_thm = qthm, ...} =>
+ let
+ val qthm = Thm.transfer' lthy qthm;
+ in
+ case [qthm] RL @{thms Quotient_eq_onp_typedef Quotient_eq_onp_type_copy} of
+ thm :: _ => (thm, Typedef)
+ | _ => (qthm RS @{thm Quotient_Quotient3},
+ Quotient (find_equiv_thm_via_Quotient qthm))
+ end
+ | NONE => (Typedef.get_info lthy absT_name |> hd |> snd |> #type_definition, Typedef))
+ | SOME thms => bad_input thms);
val wits = (Option.map o map) (prepare_term lthy) raw_wits;
val specs =
map (apsnd (apsnd (the_default @{sort type} o Option.map (prepare_sort lthy)))) raw_specs;
- val which_bnf = (case (xthm_opt, Quotient_Info.lookup_quotients lthy absT_name) of
- (NONE, SOME qs) => quotient_bnf (#equiv_thm qs, #quot_thm qs)
- | (SOME _, _) =>
- if can (fn thm => thm RS @{thm bnf_lift_Quotient_equivp}) input_thm
- then quotient_bnf (input_thm RS conjunct2, input_thm RS conjunct1 RS @{thm Quotient_Quotient3})
- else if can (fn thm => thm RS @{thm type_definition.Rep}) input_thm
- then typedef_bnf
- else Pretty.chunks [Pretty.para ("Expected theorem of either form:"),
- Pretty.item [Syntax.pretty_term lthy @{term "Quotient R Abs Rep T \<and> equivp R"}],
- Pretty.item [Syntax.pretty_term lthy @{term "type_definition Rep Abs A"}],
- Pretty.para ("Got"), Pretty.item [Thm.pretty_thm lthy input_thm]]
- |> Pretty.string_of
- |> error
- | _ => typedef_bnf);
-
+ val which_bnf = (case equiv_thm of
+ Quotient thm => quotient_bnf (thm, lift_thm)
+ | Typedef => typedef_bnf lift_thm);
in
- which_bnf input_thm wits specs map_b rel_b pred_b plugins lthy
+ which_bnf wits specs map_b rel_b pred_b plugins lthy
end;
fun prepare_lift_bnf prepare_name prepare_sort prepare_term prepare_thm =
@@ -2022,7 +2056,7 @@
val lift_bnf_cmd =
prepare_lift_bnf
(fst o dest_Type oo Proof_Context.read_type_name {proper = true, strict = false})
- Syntax.read_sort Syntax.read_term (singleton o Attrib.eval_thms);
+ Syntax.read_sort Syntax.read_term Attrib.eval_thms;
fun lift_bnf args tacs =
prepare_solve (K I) (K I) (K I) (K I) (K tacs) args;
@@ -2032,14 +2066,16 @@
val copy_bnf =
apfst (apfst (rpair NONE))
+ #> apfst (apsnd (Option.map single))
#> prepare_solve (K I) (K I) (K I) (K I)
(fn n => replicate n copy_bnf_tac);
val copy_bnf_cmd =
apfst (apfst (rpair NONE))
+ #> apfst (apsnd (Option.map single))
#> prepare_solve
(fst o dest_Type oo Proof_Context.read_type_name {proper = true, strict = false})
- Syntax.read_sort Syntax.read_term (singleton o Attrib.eval_thms)
+ Syntax.read_sort Syntax.read_term Attrib.eval_thms
(fn n => replicate n copy_bnf_tac);
end;
@@ -2068,6 +2104,7 @@
val parse_copy_opts = parse_common_opts Scan.fail;
val parse_xthm = Scan.option (Parse.reserved "via" |-- Parse.thm);
+val parse_xthms = Scan.option (Parse.reserved "via" |-- Parse.thms1);
in
@@ -2077,7 +2114,7 @@
Outer_Syntax.local_theory_to_proof @{command_keyword lift_bnf}
"register a quotient type/subtype of a bounded natural functor (BNF) as a BNF"
((parse_lift_opts -- parse_type_args_named_constrained -- Parse.type_const -- parse_wits --
- parse_xthm -- parse_map_rel_pred_bindings) >> lift_bnf_cmd);
+ parse_xthms -- parse_map_rel_pred_bindings) >> lift_bnf_cmd);
val _ =
Outer_Syntax.local_theory @{command_keyword copy_bnf}