# HG changeset patch
# User Andreas Lochbihler
# Date 1405957889 -7200
# Node ID 7ef939f89776909629074768da060c40fcfb343f
# Parent  56ed992b6d65b1f7d9f2296b9cdcfa47ae1058a2
add parametricity lemmas

diff -r 56ed992b6d65 -r 7ef939f89776 src/HOL/Lifting_Set.thy
--- 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]:
diff -r 56ed992b6d65 -r 7ef939f89776 src/HOL/List.thy
--- 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
diff -r 56ed992b6d65 -r 7ef939f89776 src/HOL/Transfer.thy
--- 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