--- a/src/HOL/Finite_Set.thy Tue Jun 26 23:39:28 2018 +0200
+++ b/src/HOL/Finite_Set.thy Wed Jun 27 10:18:03 2018 +0200
@@ -715,9 +715,45 @@
inductive_cases empty_fold_graphE [elim!]: "fold_graph f z {} x"
+lemma fold_graph_closed_lemma:
+ "fold_graph f z A x \<and> x \<in> B"
+ if "fold_graph g z A x"
+ "\<And>a b. a \<in> A \<Longrightarrow> b \<in> B \<Longrightarrow> f a b = g a b"
+ "\<And>a b. a \<in> A \<Longrightarrow> b \<in> B \<Longrightarrow> g a b \<in> B"
+ "z \<in> B"
+ using that(1-3)
+proof (induction rule: fold_graph.induct)
+ case (insertI x A y)
+ have "fold_graph f z A y" "y \<in> B"
+ unfolding atomize_conj
+ by (rule insertI.IH) (auto intro: insertI.prems)
+ then have "g x y \<in> B" and f_eq: "f x y = g x y"
+ by (auto simp: insertI.prems)
+ moreover have "fold_graph f z (insert x A) (f x y)"
+ by (rule fold_graph.insertI; fact)
+ ultimately
+ show ?case
+ by (simp add: f_eq)
+qed (auto intro!: that)
+
+lemma fold_graph_closed_eq:
+ "fold_graph f z A = fold_graph g z A"
+ if "\<And>a b. a \<in> A \<Longrightarrow> b \<in> B \<Longrightarrow> f a b = g a b"
+ "\<And>a b. a \<in> A \<Longrightarrow> b \<in> B \<Longrightarrow> g a b \<in> B"
+ "z \<in> B"
+ using fold_graph_closed_lemma[of f z A _ B g] fold_graph_closed_lemma[of g z A _ B f] that
+ by auto
+
definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"
where "fold f z A = (if finite A then (THE y. fold_graph f z A y) else z)"
+lemma fold_closed_eq: "fold f z A = fold g z A"
+ if "\<And>a b. a \<in> A \<Longrightarrow> b \<in> B \<Longrightarrow> f a b = g a b"
+ "\<And>a b. a \<in> A \<Longrightarrow> b \<in> B \<Longrightarrow> g a b \<in> B"
+ "z \<in> B"
+ unfolding Finite_Set.fold_def
+ by (subst fold_graph_closed_eq[where B=B and g=g]) (auto simp: that)
+
text \<open>
A tempting alternative for the definiens is
@{term "if finite A then THE y. fold_graph f z A y else e"}.
--- a/src/HOL/Lifting_Set.thy Tue Jun 26 23:39:28 2018 +0200
+++ b/src/HOL/Lifting_Set.thy Wed Jun 27 10:18:03 2018 +0200
@@ -215,6 +215,12 @@
shows "(rel_set A ===> rel_set A ===> (=)) (\<subseteq>) (\<subseteq>)"
unfolding subset_eq [abs_def] by transfer_prover
+lemma strict_subset_transfer [transfer_rule]:
+ includes lifting_syntax
+ assumes [transfer_rule]: "bi_unique A"
+ shows "(rel_set A ===> rel_set A ===> (=)) (\<subset>) (\<subset>)"
+ unfolding subset_not_subset_eq by transfer_prover
+
declare right_total_UNIV_transfer[transfer_rule]
lemma UNIV_transfer [transfer_rule]:
@@ -259,6 +265,20 @@
by (rule rel_funI, erule (1) bi_unique_rel_set_lemma)
(simp add: card_image)
+lemma vimage_right_total_transfer[transfer_rule]:
+ includes lifting_syntax
+ assumes [transfer_rule]: "bi_unique B" "right_total A"
+ shows "((A ===> B) ===> rel_set B ===> rel_set A) (\<lambda>f X. f -` X \<inter> Collect (Domainp A)) vimage"
+proof -
+ let ?vimage = "(\<lambda>f B. {x. f x \<in> B \<and> Domainp A x})"
+ have "((A ===> B) ===> rel_set B ===> rel_set A) ?vimage vimage"
+ unfolding vimage_def
+ by transfer_prover
+ also have "?vimage = (\<lambda>f X. f -` X \<inter> Collect (Domainp A))"
+ by auto
+ finally show ?thesis .
+qed
+
lemma vimage_parametric [transfer_rule]:
assumes [transfer_rule]: "bi_total A" "bi_unique B"
shows "((A ===> B) ===> rel_set B ===> rel_set A) vimage vimage"
@@ -270,6 +290,12 @@
by (intro rel_funI rel_setI)
(force dest: rel_setD1 bi_uniqueDr[OF assms], force dest: rel_setD2 bi_uniqueDl[OF assms])
+lemma inj_on_transfer[transfer_rule]:
+ "((A ===> B) ===> rel_set A ===> (=)) inj_on inj_on"
+ if [transfer_rule]: "bi_unique A" "bi_unique B"
+ unfolding inj_on_def
+ by transfer_prover
+
end
lemma (in comm_monoid_set) F_parametric [transfer_rule]:
--- a/src/HOL/Transfer.thy Tue Jun 26 23:39:28 2018 +0200
+++ b/src/HOL/Transfer.thy Wed Jun 27 10:18:03 2018 +0200
@@ -439,6 +439,13 @@
using assms unfolding right_total_def Ball_def rel_fun_def Domainp_iff[abs_def]
by fast
+lemma right_total_fun_eq_transfer:
+ includes lifting_syntax
+ assumes [transfer_rule]: "right_total A" "bi_unique B"
+ shows "((A ===> B) ===> (A ===> B) ===> (=)) (\<lambda>f g. \<forall>x\<in>Collect(Domainp A). f x = g x) (=)"
+ unfolding fun_eq_iff
+ by transfer_prover
+
lemma All_transfer [transfer_rule]:
assumes "bi_total A"
shows "((A ===> (=)) ===> (=)) All All"