# HG changeset patch
# User traytel
# Date 1575936399 -3600
# Node ID 0c454a5d125d78aa730e549c8ab316556847c3d1
# Parent  35a92ce0b94e8824eee048a6af44a24cf7455df8
NEWS, CONTRIBUTORS, and documentation

diff -r 35a92ce0b94e -r 0c454a5d125d CONTRIBUTORS
--- a/CONTRIBUTORS	Tue Dec 10 01:06:39 2019 +0100
+++ b/CONTRIBUTORS	Tue Dec 10 01:06:39 2019 +0100
@@ -6,6 +6,10 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* December 2019:
+  Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel
+  Extension of lift_bnf to support quotient types.
+
 * October 2019: Maximilian Schäffeler
   Port of the HOL Light decision procedure for metric spaces.
 
diff -r 35a92ce0b94e -r 0c454a5d125d NEWS
--- a/NEWS	Tue Dec 10 01:06:39 2019 +0100
+++ b/NEWS	Tue Dec 10 01:06:39 2019 +0100
@@ -59,6 +59,11 @@
 
 *** HOL ***
 
+* Improvements of the "lift_bnf" command:
+  - Add support for quotient types.
+  - Generate transfer rules for the lifted map/set/rel/pred
+    constants (theorems "<type>.<constant>_transfer_raw").
+
 * Term_XML.Encode/Decode.term uses compact representation of Const
 "typargs" from the given declaration environment. This also makes more
 sense for translations to lambda-calculi with explicit polymorphism.
diff -r 35a92ce0b94e -r 0c454a5d125d src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Tue Dec 10 01:06:39 2019 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Tue Dec 10 01:06:39 2019 +0100
@@ -2918,9 +2918,9 @@
 \<^file>\<open>~~/src/HOL/Library/Multiset.thy\<close> for further examples of BNF
 registration, some of which feature custom witnesses.
 
-For many typedefs, lifting the BNF structure from the raw type to the abstract
-type can be done uniformly. This is the task of the @{command lift_bnf} command.
-Using @{command lift_bnf}, the above registration of \<^typ>\<open>('d, 'a) fn\<close> as a
+For many typedefs and quotient types, lifting the BNF structure from the raw typ
+to the abstract type can be done uniformly. This is the task of the @{command lift_bnf}
+command. Using @{command lift_bnf}, the above registration of \<^typ>\<open>('d, 'a) fn\<close> as a
 BNF becomes much shorter:
 \<close>
 
@@ -2929,7 +2929,7 @@
     begin
 (*>*)
     lift_bnf (*<*)(no_warn_wits) (*>*)('d, 'a) fn
-      by auto
+      by force+
 (*<*)
     end
 (*>*)
@@ -2961,7 +2961,7 @@
 
 text \<open>\blankline\<close>
 
-    copy_bnf ('a, 'z) point_ext
+    copy_bnf (*<*)(no_warn_transfer) (*>*)('a, 'z) point_ext
 
 text \<open>
 In the general case, the proof obligations generated by @{command lift_bnf} are
@@ -2978,7 +2978,7 @@
 \<^term>\<open>zs :: ('a \<times> 'b) list\<close>.
 \<close>
 
-    lift_bnf (*<*)(no_warn_wits) (*>*)'a nonempty_list
+    lift_bnf (*<*)(no_warn_wits,no_warn_transfer) (*>*)'a nonempty_list
     proof -
       fix f (*<*):: "'a \<Rightarrow> 'c"(*>*)and xs :: "'a list"
       assume "xs \<in> {xs. xs \<noteq> []}"
@@ -2987,10 +2987,73 @@
     next
       fix zs :: "('a \<times> 'b) list"
       assume "map fst zs \<in> {xs. xs \<noteq> []}" "map snd zs \<in> {xs. xs \<noteq> []}"
-      then show "zs \<in> {xs. xs \<noteq> []}"
-        by (cases zs (*<*)rule: list.exhaust(*>*)) auto
+      then show "\<exists>zs'\<in>{xs. xs \<noteq> []}.
+            set zs' \<subseteq> set zs \<and>
+            map fst zs' = map fst zs \<and>
+            map snd zs' = map snd zs"
+        by (cases zs (*<*)rule: list.exhaust(*>*)) (auto intro!: exI[of _ zs])
     qed
 
+text \<open>The @{command lift_bnf} command also supports quotient types. Here is an example
+that defines the option type as a quotient of the sum type. The proof obligations
+generated by @{command lift_bnf} for quotients are different from the ones for typedefs.\<close>
+
+    inductive ignore_Inl :: "'a + 'a \<Rightarrow> 'a + 'a \<Rightarrow> bool" where
+      "ignore_Inl (Inl x) (Inl y)"
+    | "ignore_Inl (Inr x) (Inr x)"
+
+    (*<*)
+    inductive_simps ignore_Inl_simps[simp]:
+      "ignore_Inl (Inl x) y"
+      "ignore_Inl (Inr x') y"
+      "ignore_Inl y (Inl x)"
+      "ignore_Inl y (Inr x')"
+    (*>*)
+
+    lemma ignore_Inl_equivp:
+      "ignore_Inl x x"
+      "ignore_Inl x y \<Longrightarrow> ignore_Inl y x"
+      "ignore_Inl x y \<Longrightarrow> ignore_Inl y z \<Longrightarrow> ignore_Inl x z"
+      by (cases x; cases y; cases z; auto)+
+
+    quotient_type 'a myoption = "'a + 'a" / ignore_Inl
+      unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
+      by (blast intro: ignore_Inl_equivp)
+
+    lift_bnf 'a myoption (*<*)[wits: "Inl undefined :: 'a + 'a"](*>*)
+
+    proof (intro rel_funI)
+      fix f g :: "'a \<Rightarrow> 'b" and x y :: "'a + 'a"
+      assume "f = g" "ignore_Inl x y"
+      then show "ignore_Inl (map_sum f f x) (map_sum g g y)"
+        by (cases x; cases y) auto
+    next
+      fix P :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and Q :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
+      assume "P OO Q \<noteq> bot"
+      then show "rel_sum P P OO ignore_Inl OO rel_sum Q Q
+         \<le> ignore_Inl OO rel_sum (P OO Q) (P OO Q) OO ignore_Inl"
+        by (fastforce(*<*) elim!: ignore_Inl.cases simp add: relcompp_apply fun_eq_iff rel_sum.simps(*>*))
+    next
+      fix S :: "'a set set"
+      let ?eq = "{(x, x'). ignore_Inl x x'}"
+      let ?in = "\<lambda>A. {x. Basic_BNFs.setl x \<union> Basic_BNFs.setr x \<subseteq> A}"
+      assume "S \<noteq> {}" "\<Inter> S \<noteq> {}"
+      show "(\<Inter>A\<in>S. ?eq `` ?in A) \<subseteq> ?eq `` ?in (\<Inter> S)"
+      proof (intro subsetI)
+        fix x
+        assume "x \<in> (\<Inter>A\<in>S. ?eq `` ?in A)"
+        with \<open>\<Inter> S \<noteq> {}\<close> show "x \<in> ?eq `` ?in (\<Inter> S)"
+          by (cases x) (fastforce(*<*) dest!: spec[where x="Inl _"](*>*))+
+      qed
+    (*<*)next
+      fix a :: 'a
+      assume "a \<in> (\<Inter>mx\<in>{mx. ignore_Inl (map_sum Inr Inr (Inl undefined)) mx}.
+        \<Union> (Basic_BNFs.setr ` (Basic_BNFs.setl mx \<union> Basic_BNFs.setr mx)))"
+      then show False
+        by (auto simp: setr.simps)(*>*)
+    qed
+
+
 text \<open>
 The next example declares a BNF axiomatically. This can be convenient for
 reasoning abstractly about an arbitrary BNF. The @{command bnf_axiomatization}
@@ -3059,7 +3122,7 @@
     @{syntax tyargs} name wit_terms?  \<newline>
     ('via' thm)? @{syntax map_rel_pred}?
   ;
-  @{syntax_def lb_options}: '(' ((@{syntax plugins} | 'no_warn_wits') + ',') ')'
+  @{syntax_def lb_options}: '(' ((@{syntax plugins} | 'no_warn_wits' | 'no_warn_transfer') + ',') ')'
   ;
   @{syntax_def wit_terms}: '[' 'wits' ':' terms ']'
 \<close>
@@ -3068,8 +3131,10 @@
 \noindent
 The @{command lift_bnf} command registers as a BNF an existing type (the
 \emph{abstract type}) that was defined as a subtype of a BNF (the \emph{raw
-type}) using the @{command typedef} command. To achieve this, it lifts the BNF
-structure on the raw type to the abstract type following a \<^term>\<open>type_definition\<close> theorem. The theorem is usually inferred from the type, but can
+type}) using the @{command typedef} command or as a quotient type of a BNF (also, the
+\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
 addition, custom names for the set functions, the map function, the predicator, and the relator,
 as well as nonemptiness witnesses can be specified.
@@ -3090,8 +3155,11 @@
 \end{matharray}
 
 \<^rail>\<open>
-  @@{command copy_bnf} target? ('(' @{syntax plugins} ')')? \<newline>
+  @@{command copy_bnf} target? cb_options? \<newline>
     @{syntax tyargs} name ('via' thm)? @{syntax map_rel_pred}?
+  ;
+  @{syntax_def cb_options}: '(' ((@{syntax plugins} | 'no_warn_transfer') + ',') ')'
+
 \<close>
 \medskip