# HG changeset patch
# User Andreas Lochbihler
# Date 1423663401 -3600
# Node ID 860fb1c6555302106b6a7fe167beb9f9245c2d70
# Parent  0c5c5ad5d2e009f3cd3e2fef62062e31034c4d09
more transfer rules

diff -r 0c5c5ad5d2e0 -r 860fb1c65553 src/HOL/Option.thy
--- a/src/HOL/Option.thy	Wed Feb 11 14:45:10 2015 +0100
+++ b/src/HOL/Option.thy	Wed Feb 11 15:03:21 2015 +0100
@@ -77,6 +77,7 @@
   "(\<And>x. x \<in> set_option y \<Longrightarrow> P x x) \<Longrightarrow> rel_option P y y"
 by(cases y) auto
 
+
 subsubsection {* Operations *}
 
 lemma ospec [dest]: "(ALL x:set_option A. P x) ==> A = Some x ==> P x"
@@ -261,6 +262,10 @@
     Option.bind Option.bind"
   unfolding rel_fun_def split_option_all by simp
 
+lemma pred_option_parametric [transfer_rule]:
+  "((A ===> op =) ===> rel_option A ===> op =) pred_option pred_option"
+by(rule rel_funI)+(auto simp add: rel_option_unfold is_none_def dest: rel_funD)
+
 end
 
 
diff -r 0c5c5ad5d2e0 -r 860fb1c65553 src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Wed Feb 11 14:45:10 2015 +0100
+++ b/src/HOL/Transfer.thy	Wed Feb 11 15:03:21 2015 +0100
@@ -533,13 +533,35 @@
 by fast+
 
 lemma right_unique_transfer [transfer_rule]:
-  assumes [transfer_rule]: "right_total A"
-  assumes [transfer_rule]: "right_total B"
-  assumes [transfer_rule]: "bi_unique B"
-  shows "((A ===> B ===> op=) ===> implies) right_unique right_unique"
-using assms unfolding right_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
+  "\<lbrakk> right_total A; right_total B; bi_unique B \<rbrakk>
+  \<Longrightarrow> ((A ===> B ===> op=) ===> implies) right_unique right_unique"
+unfolding right_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
 by metis
 
+lemma left_total_parametric [transfer_rule]:
+  assumes [transfer_rule]: "bi_total A" "bi_total B"
+  shows "((A ===> B ===> op =) ===> op =) left_total left_total"
+unfolding left_total_def[abs_def] by transfer_prover
+
+lemma right_total_parametric [transfer_rule]:
+  assumes [transfer_rule]: "bi_total A" "bi_total B"
+  shows "((A ===> B ===> op =) ===> op =) right_total right_total"
+unfolding right_total_def[abs_def] by transfer_prover
+
+lemma left_unique_parametric [transfer_rule]:
+  assumes [transfer_rule]: "bi_unique A" "bi_total A" "bi_total B"
+  shows "((A ===> B ===> op =) ===> op =) left_unique left_unique"
+unfolding left_unique_def[abs_def] by transfer_prover
+
+lemma prod_pred_parametric [transfer_rule]:
+  "((A ===> op =) ===> (B ===> op =) ===> rel_prod A B ===> op =) pred_prod pred_prod"
+unfolding pred_prod_def[abs_def] Basic_BNFs.fsts_def Basic_BNFs.snds_def fstsp.simps sndsp.simps 
+by simp transfer_prover
+
+lemma apfst_parametric [transfer_rule]:
+  "((A ===> B) ===> rel_prod A C ===> rel_prod B C) apfst apfst"
+unfolding apfst_def[abs_def] by transfer_prover
+
 lemma rel_fun_eq_eq_onp: "(op= ===> eq_onp P) = eq_onp (\<lambda>f. \<forall>x. P(f x))"
 unfolding eq_onp_def rel_fun_def by auto
 
@@ -591,6 +613,11 @@
   }
 qed
 
+lemma right_unique_parametric [transfer_rule]:
+  assumes [transfer_rule]: "bi_total A" "bi_unique B" "bi_total B"
+  shows "((A ===> B ===> op =) ===> op =) right_unique right_unique"
+unfolding right_unique_def[abs_def] by transfer_prover
+
 end
 
 end