# HG changeset patch
# User immler
# Date 1530087483 -7200
# Node ID 1bad081651628e4f4b8dfc75948efd1434d0017a
# Parent  9d78b02b55060e37e4f77e7d0993d59a4d1a6a40
added lemmas and transfer rules

diff -r 9d78b02b5506 -r 1bad08165162 src/HOL/Finite_Set.thy
--- 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"}.
diff -r 9d78b02b5506 -r 1bad08165162 src/HOL/Lifting_Set.thy
--- 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]:
diff -r 9d78b02b5506 -r 1bad08165162 src/HOL/Transfer.thy
--- 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"