--- a/src/HOL/Lifting_Set.thy Mon Jul 21 17:51:11 2014 +0200
+++ b/src/HOL/Lifting_Set.thy Mon Jul 21 17:51:29 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 17:51:11 2014 +0200
+++ b/src/HOL/List.thy Mon Jul 21 17:51:29 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 17:51:11 2014 +0200
+++ b/src/HOL/Transfer.thy Mon Jul 21 17:51:29 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