merged

--- a/src/HOL/Finite_Set.thy	Mon Jul 21 20:57:47 2014 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Jul 22 08:07:47 2014 +0200
@@ -733,6 +733,11 @@
   then show ?thesis by simp
 qed
 
+lemma fold_set_union_disj:
+  assumes "finite A" "finite B" "A \<inter> B = {}"
+  shows "Finite_Set.fold f z (A \<union> B) = Finite_Set.fold f (Finite_Set.fold f z A) B"
+using assms(2,1,3) by induction simp_all
+
 end
 
 text{* Other properties of @{const fold}: *}

--- a/src/HOL/Lifting_Set.thy	Mon Jul 21 20:57:47 2014 +0200
+++ b/src/HOL/Lifting_Set.thy	Tue Jul 22 08:07:47 2014 +0200
@@ -266,6 +266,12 @@
   shows "((A ===> B) ===> rel_set B ===> rel_set A) vimage vimage"
   unfolding vimage_def[abs_def] by transfer_prover
 
+lemma Image_parametric [transfer_rule]:
+  assumes "bi_unique A"
+  shows "(rel_set (rel_prod A B) ===> rel_set A ===> rel_set B) op `` op ``"
+by(intro rel_funI rel_setI)
+  (force dest: rel_setD1 bi_uniqueDr[OF assms], force dest: rel_setD2 bi_uniqueDl[OF assms])
+
 end
 
 lemma (in comm_monoid_set) F_parametric [transfer_rule]:

--- a/src/HOL/List.thy	Mon Jul 21 20:57:47 2014 +0200
+++ b/src/HOL/List.thy	Tue Jul 22 08:07:47 2014 +0200
@@ -6883,6 +6883,11 @@
   unfolding listsum_def[abs_def]
   by transfer_prover
 
+lemma rtrancl_parametric [transfer_rule]:
+  assumes [transfer_rule]: "bi_unique A" "bi_total A"
+  shows "(rel_set (rel_prod A A) ===> rel_set (rel_prod A A)) rtrancl rtrancl"
+unfolding rtrancl_def by transfer_prover
+
 end
 
 end

--- a/src/HOL/Transfer.thy	Mon Jul 21 20:57:47 2014 +0200
+++ b/src/HOL/Transfer.thy	Tue Jul 22 08:07:47 2014 +0200
@@ -536,6 +536,45 @@
   shows "((A ===> op=) ===> A ===> A ===> op=) eq_onp eq_onp"
 unfolding eq_onp_def[abs_def] by transfer_prover
 
+lemma rtranclp_parametric [transfer_rule]:
+  assumes "bi_unique A" "bi_total A"
+  shows "((A ===> A ===> op =) ===> A ===> A ===> op =) rtranclp rtranclp"
+proof(rule rel_funI iffI)+
+  fix R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and R' x y x' y'
+  assume R: "(A ===> A ===> op =) R R'" and "A x x'"
+  {
+    assume "R\<^sup>*\<^sup>* x y" "A y y'"
+    thus "R'\<^sup>*\<^sup>* x' y'"
+    proof(induction arbitrary: y')
+      case base
+      with `bi_unique A` `A x x'` have "x' = y'" by(rule bi_uniqueDr)
+      thus ?case by simp
+    next
+      case (step y z z')
+      from `bi_total A` obtain y' where "A y y'" unfolding bi_total_def by blast
+      hence "R'\<^sup>*\<^sup>* x' y'" by(rule step.IH)
+      moreover from R `A y y'` `A z z'` `R y z`
+      have "R' y' z'" by(auto dest: rel_funD)
+      ultimately show ?case ..
+    qed
+  next
+    assume "R'\<^sup>*\<^sup>* x' y'" "A y y'"
+    thus "R\<^sup>*\<^sup>* x y"
+    proof(induction arbitrary: y)
+      case base
+      with `bi_unique A` `A x x'` have "x = y" by(rule bi_uniqueDl)
+      thus ?case by simp
+    next
+      case (step y' z' z)
+      from `bi_total A` obtain y where "A y y'" unfolding bi_total_def by blast
+      hence "R\<^sup>*\<^sup>* x y" by(rule step.IH)
+      moreover from R `A y y'` `A z z'` `R' y' z'`
+      have "R y z" by(auto dest: rel_funD)
+      ultimately show ?case ..
+    qed
+  }
+qed
+
 end
 
 end