--- 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.
--- 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.
--- 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